diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
commit | 45a138c326da72890bf889a3670aad503ef4aa1e (patch) | |
tree | fa0c9a8497d0b33f78a9f19212152a61392825cc /src/prop/prop_engine.cpp | |
parent | 8c0b2d6db32103268f84d89c0d0545c7eb504069 (diff) |
Partial merge from kind-backend branch, including Minisat and CNF work to
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 7d0353122..2538e6d0c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -232,6 +232,10 @@ void PropEngine::pop() { Debug("prop") << "pop()" << endl; } +bool PropEngine::isRunning() const { + return d_inCheckSat; +} + void PropEngine::interrupt() throw(ModalException) { if(! d_inCheckSat) { throw ModalException("SAT solver is not currently solving anything; " @@ -247,5 +251,49 @@ void PropEngine::spendResource() throw() { // TODO implement me } +bool PropEngine::properExplanation(TNode node, TNode expl) const { + if(! d_cnfStream->hasLiteral(node)) { + Trace("properExplanation") << "properExplanation(): Failing because node " + << "being explained doesn't have a SAT literal ?!" << std::endl + << "properExplanation(): The node is: " << node << std::endl; + return false; + } + + SatLiteral nodeLit = d_cnfStream->getLiteral(node); + + for(TNode::kinded_iterator i = expl.begin(kind::AND), + i_end = expl.end(kind::AND); + i != i_end; + ++i) { + if(! d_cnfStream->hasLiteral(*i)) { + Trace("properExplanation") << "properExplanation(): Failing because one of explanation " + << "nodes doesn't have a SAT literal" << std::endl + << "properExplanation(): The explanation node is: " << *i << std::endl; + return false; + } + + SatLiteral iLit = d_cnfStream->getLiteral(*i); + + if(iLit == nodeLit) { + Trace("properExplanation") << "properExplanation(): Failing because the node" << std::endl + << "properExplanation(): " << node << std::endl + << "properExplanation(): cannot be made to explain itself!" << std::endl; + return false; + } + + if(! d_satSolver->properExplanation(nodeLit, iLit)) { + Trace("properExplanation") << "properExplanation(): SAT solver told us that node" << std::endl + << "properExplanation(): " << *i << std::endl + << "properExplanation(): is not part of a proper explanation node for" << std::endl + << "properExplanation(): " << node << std::endl + << "properExplanation(): Perhaps it one of the two isn't assigned or the explanation" << std::endl + << "properExplanation(): node wasn't propagated before the node being explained" << std::endl; + return false; + } + } + + return true; +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ |