projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6935324) | patch
Single driver for both sequential and portfolio
authorKshitij Bansal <kshitij@cs.nyu.edu>
Sat, 8 Sep 2012 14:25:25 +0000 (14:25 +0000)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Sat, 8 Sep 2012 14:25:25 +0000 (14:25 +0000)
commitcfa9e2cbbdf77a325791b5548b41093a0781311c
treee843d38afe4b197a2dd81316998477cedac26c52tree
parent6935324f45bd7f2c735ca4120a9e800ef8903442commit | diff
Single driver for both sequential and portfolio

A "command executer" layer between parsing commands and invoking them.

New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
16 files changed:
src/expr/command.cpp diff | blob | history
src/expr/command.h diff | blob | history
src/expr/expr_template.cpp diff | blob | history
src/main/Makefile.am diff | blob | history
src/main/command_executer.cpp [new file with mode: 0644] blob
src/main/command_executer.h [new file with mode: 0644] blob
src/main/command_executer_portfolio.cpp [new file with mode: 0644] blob
src/main/command_executer_portfolio.h [new file with mode: 0644] blob
src/main/driver.cpp [deleted file] blob | history
src/main/driver_portfolio.cpp [deleted file] blob | history
src/main/driver_unified.cpp [new file with mode: 0644] blob
src/main/portfolio.cpp diff | blob | history
src/main/portfolio.h diff | blob | history
src/main/portfolio_util.cpp [new file with mode: 0644] blob
src/main/portfolio_util.h [new file with mode: 0644] blob
src/prop/prop_engine.cpp diff | blob | history