diff options
author | Tim King <taking@cs.nyu.edu> | 2010-02-03 19:25:50 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-02-03 19:25:50 +0000 |
commit | 14b035cd792b43ec1dc5655882378631235732ff (patch) | |
tree | 4f2c0cfe5836872e617a6a0e6a2036512cc84dee /src/prop/prop_engine.h | |
parent | 480b791976b2916148ef95c48c00280b404c32e2 (diff) |
I hacked in a temporary way to restart minisat for multiple queries.
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r-- | src/prop/prop_engine.h | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index f356c9e0b..9f5f9dac1 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -52,7 +52,7 @@ class PropEngine { * and to start from scratch everytime. (Avoid push/pop problems?) * Is this right? */ - CVC4::prop::minisat::SimpSolver d_sat; + CVC4::prop::minisat::Solver * d_sat; std::map<Node, CVC4::prop::minisat::Lit> d_atom2lit; @@ -64,6 +64,21 @@ class PropEngine { */ void registerAtom(const Node & n, CVC4::prop::minisat::Lit l); + /** + * Flags whether the solver may need to have its state reset before + * solving occurs + */ + bool d_restartMayBeNeeded; + + /** + * Cleans existing state in the PropEngine and reinitializes the state. + */ + void restart(); + + /** + * Keeps track of all of the assertions that need to be made. + */ + std::vector<Node> d_assertionList; CVC4::prop::minisat::Lit requestFreshLit(); |