diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-12 23:41:12 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-12 23:41:12 +0000 |
commit | 856567b63c56b238db8a5bb84ad0da7990c1f1eb (patch) | |
tree | ab2a453f926b56070c39b9afba02dba7ba59858d /src | |
parent | 20b3dabb4823ede8147a08a47f8d909980414bee (diff) |
Fixing unnecessary construction of NOT nodes when generating conflict clauses and:
* adding the smallest test case (eq_diamond23.smt) that memouts in 50s
* adding the initial attributes black box test
Diffstat (limited to 'src')
-rw-r--r-- | src/prop/sat.h | 20 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 5 |
2 files changed, 12 insertions, 13 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index f29436b97..7844008e8 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -174,23 +174,19 @@ SatVariable SatSolver::newVar(bool theoryAtom) { } void SatSolver::theoryCheck(SatClause& conflict) { - // Run the thoery checks - d_theoryEngine->check(theory::Theory::FULL_EFFORT); - // Try to get the conflict - Node conflictNode = d_theoryEngine->getConflict(); - // If the conflict is there, construct the conflict clause - if (!conflictNode.isNull()) { + // Try theory propagation + if (!d_theoryEngine->check(theory::Theory::FULL_EFFORT)) { + // We have a conflict, get it + Node conflictNode = d_theoryEngine->getConflict(); Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl; + // Go through the literals and construct the conflict clause Node::const_iterator literal_it = conflictNode.begin(); Node::const_iterator literal_end = conflictNode.end(); while (literal_it != literal_end) { - // Get the node and construct it's negation - Node literalNode = (*literal_it); - Node negated = literalNode.getKind() == kind::NOT ? literalNode[0] : literalNode.notNode(); // Get the literal corresponding to the node - SatLiteral l = d_cnfStream->getLiteral(negated); - // Add to the conflict clause and continue - conflict.push(l); + SatLiteral l = d_cnfStream->getLiteral(*literal_it); + // Add the negation to the conflict clause and continue + conflict.push(~l); literal_it ++; } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0b1afe748..cb0158dfe 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -254,7 +254,8 @@ public: * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ - inline void check(theory::Theory::Effort effort) { + inline bool check(theory::Theory::Effort effort) { + bool ok = true; try { //d_bool.check(effort); d_uf.check(effort); @@ -263,7 +264,9 @@ public: //d_bv.check(effort); } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; + ok = false; } + return ok; } /** |