diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-12 19:41:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-12 19:41:04 +0000 |
commit | 20b3dabb4823ede8147a08a47f8d909980414bee (patch) | |
tree | 6d6ea617bef8d840de8f8ff737e00acadb6675f9 /src/prop/sat.h | |
parent | 3cf73e344987c2449943ca3a97054565eb9d5726 (diff) |
* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,
DecisionEngine, and Theory. These are triggered from the SmtEngine
dtor before the other engines are deleted. This is important
because of potential issues with outstanding TNodes in Theory
implementations (which fail if the destruction is done in the wrong
order, in certain cases).
* Favor "FactQueueResetter" instead of clearAssertionQueues() for
resetting facts queue in Theory implementations.
* Better theory-rewriting code.
* Minor cleanups.
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r-- | src/prop/sat.h | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index ec38bb019..f29436b97 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -77,8 +77,10 @@ public: inline size_t operator()(const SatLiteral& literal) const; }; - inline SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, context::Context* context, - const Options* options); + inline SatSolver(PropEngine* propEngine, + TheoryEngine* theoryEngine, + context::Context* context, + const Options* options); inline ~SatSolver(); @@ -93,8 +95,6 @@ public: inline void enqueueTheoryLiteral(const SatLiteral& l); inline void setCnfStream(CnfStream* cnfStream); - - inline void clearAssertionQueues(); }; }/* CVC4::prop namespace */ @@ -135,7 +135,8 @@ inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) { return out; } -size_t SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const { +inline size_t +SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const { return (size_t) minisat::toInt(literal); } @@ -208,11 +209,6 @@ void SatSolver::setCnfStream(CnfStream* cnfStream) { d_cnfStream = cnfStream; } - -void SatSolver::clearAssertionQueues() { - d_theoryEngine->clearAssertionQueues(); -} - }/* CVC4::prop namespace */ }/* CVC4 namespace */ |