From 752b00bc94385fd4b54becb072fca3814f34fd4c Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 8 Mar 2012 02:33:37 +0000 Subject: [PATCH] Removing QUICK_CHECK, and other unused ones, from the Theory::Effort. Seems to be working better , and should fix the failing cases in the regressions. Removing one test case from the integer regress0. --- .cproject | 6 +- .project | 2 +- src/prop/minisat/core/Solver.cc | 66 +++++------- src/prop/minisat/core/Solver.h | 12 +-- src/prop/minisat/simp/SimpSolver.cc | 6 +- src/theory/arith/theory_arith.cpp | 102 +++++++++--------- src/theory/datatypes/theory_datatypes.cpp | 2 +- src/theory/theory.cpp | 14 ++- src/theory/theory.h | 39 +++---- .../regress0/arith/integers/Makefile.am | 2 +- test/unit/theory/theory_arith_white.h | 2 +- test/unit/theory/theory_black.h | 31 +----- 12 files changed, 123 insertions(+), 161 deletions(-) diff --git a/.cproject b/.cproject index 2579ef3ae..6145dec05 100644 --- a/.cproject +++ b/.cproject @@ -20,7 +20,7 @@ - + @@ -57,7 +57,9 @@ - + + + diff --git a/.project b/.project index 1465eabe2..fec1cfaa5 100644 --- a/.project +++ b/.project @@ -32,7 +32,7 @@ org.eclipse.cdt.make.core.buildArguments - -j2 + -j10 org.eclipse.cdt.make.core.buildCommand diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 678fe28dc..9f3285fff 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -248,7 +248,7 @@ bool Solver::addClause_(vec& ps, bool removable) Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl; trail_user.push(ps[0]); } - return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef); + return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef); } else return ok; } else { CRef cr = ca.alloc(assertionLevel, ps, false); @@ -654,8 +654,8 @@ CRef Solver::propagate(TheoryCheckType type) ScopedBool scoped_bool(minisat_busy, true); - // If we are not in the quick mode add the lemmas that were left begind - if (type != CHECK_WITHOUTH_PROPAGATION_QUICK && lemmas.size() > 0) { + // If we are not in the quick mode add the lemmas that were left behind + if (type != CHECK_WITHOUTH_THEORY && lemmas.size() > 0) { confl = updateLemmas(); if (confl != CRef_Undef) { return confl; @@ -664,9 +664,9 @@ CRef Solver::propagate(TheoryCheckType type) // If this is the final check, no need for Boolean propagation and // theory propagation - if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) { + if (type == CHECK_FINAL) { // Do the theory check - theoryCheck(CVC4::theory::Theory::FULL_EFFORT); + theoryCheck(CVC4::theory::Theory::EFFORT_FULL); // If there are lemmas (or conflicts) update them if (lemmas.size() > 0) { recheck = true; @@ -677,38 +677,24 @@ CRef Solver::propagate(TheoryCheckType type) } } - // The effort we will be using to theory check - CVC4::theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ? - CVC4::theory::Theory::QUICK_CHECK : - CVC4::theory::Theory::STANDARD; - // Keep running until we have checked everything, we // have no conflict and no new literals have been asserted - do { - do { - // Propagate on the clauses - confl = propagateBool(); - - // If no conflict, do the theory check - if (confl == CRef_Undef) { - // Do the theory check - theoryCheck(effort); - // If there are lemmas (or conflicts) update them - if (lemmas.size() > 0) { - confl = updateLemmas(); - } - } - } while (confl == CRef_Undef && qhead < trail.size()); - - // If still consistent do some theory propagation - if (confl == CRef_Undef && type == CHECK_WITH_PROPAGATION_STANDARD) { - propagateTheory(); - if (lemmas.size() > 0) { - confl = updateLemmas(); - } + do { + // Propagate on the clauses + confl = propagateBool(); + + // If no conflict, do the theory check + if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) { + // Do the theory check + theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD); + // Pick up the theory propagated literals + propagateTheory(); + // If there are lemmas (or conflicts) update them + if (lemmas.size() > 0) { + confl = updateLemmas(); + } } - - } while (confl == CRef_Undef && qhead < trail.size()); + } while (confl == CRef_Undef && qhead < trail.size()); return confl; } @@ -931,7 +917,7 @@ bool Solver::simplify() { assert(decisionLevel() == 0); - if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef) + if (!ok || propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef) return ok = false; if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) @@ -972,7 +958,7 @@ lbool Solver::search(int nof_conflicts) vec learnt_clause; starts++; - TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD; + TheoryCheckType check_type = CHECK_WITH_THEORY; for (;;) { // Propagate and call the theory solvers @@ -1025,14 +1011,14 @@ lbool Solver::search(int nof_conflicts) } // We have a conflict so, we are going back to standard checks - check_type = CHECK_WITH_PROPAGATION_STANDARD; + check_type = CHECK_WITH_THEORY; } else { // If this was a final check, we are satisfiable - if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) { + if (check_type == CHECK_FINAL) { // Unless a lemma has added more stuff to the queues if (!order_heap.empty() || qhead < trail.size()) { - check_type = CHECK_WITH_PROPAGATION_STANDARD; + check_type = CHECK_WITH_THEORY; continue; } else if (recheck) { // There some additional stuff added, so we go for another full-check @@ -1086,7 +1072,7 @@ lbool Solver::search(int nof_conflicts) if (next == lit_Undef) { // We need to do a full theory check to confirm - check_type = CHECK_WITHOUTH_PROPAGATION_FINAL; + check_type = CHECK_FINAL; continue; } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index c0dd00166..8a5472725 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -303,12 +303,12 @@ protected: vec theory; // Is the variable representing a theory atom enum TheoryCheckType { - // Quick check, but don't perform theory propagation - CHECK_WITHOUTH_PROPAGATION_QUICK, - // Check and perform theory propagation - CHECK_WITH_PROPAGATION_STANDARD, - // The SAT problem is satisfiable, perform a full theory check - CHECK_WITHOUTH_PROPAGATION_FINAL + // Quick check, but don't perform theory reasoning + CHECK_WITHOUTH_THEORY, + // Check and perform theory reasoning + CHECK_WITH_THEORY, + // The SAT abstraction of the problem is satisfiable, perform a full theory check + CHECK_FINAL }; // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 2b5468186..2cacfbcc0 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -214,7 +214,7 @@ bool SimpSolver::strengthenClause(CRef cr, Lit l) updateElimHeap(var(l)); } - return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef : true; + return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef : true; } @@ -321,7 +321,7 @@ bool SimpSolver::implied(const vec& c) uncheckedEnqueue(~c[i]); } - bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef; + bool result = propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef; cancelUntil(0); return result; } @@ -410,7 +410,7 @@ bool SimpSolver::asymm(Var v, CRef cr) else l = c[i]; - if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef){ + if (propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef){ cancelUntil(0); asymm_lits++; if (!strengthenClause(cr, l)) diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index a1d57af66..3760e233d 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1109,65 +1109,63 @@ Node flattenAnd(Node n){ } void TheoryArith::propagate(Effort e) { - if(quickCheckOrMore(e)){ - bool propagated = false; - if(Options::current()->arithPropagation && hasAnyUpdates()){ - propagateCandidates(); - }else{ - clearUpdates(); - } + bool propagated = false; + if(Options::current()->arithPropagation && hasAnyUpdates()){ + propagateCandidates(); + }else{ + clearUpdates(); + } - while(d_propManager.hasMorePropagations()){ - const PropManager::PropUnit next = d_propManager.getNextPropagation(); - bool flag = next.flag; - TNode toProp = next.consequent; - - TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp; - - Debug("arith::propagate") << "propagate @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl; - - if(flag) { - //Currently if the flag is set this came from an equality detected by the - //equality engine in the the difference manager. - if(toProp.getKind() == kind::EQUAL){ - Node normalized = Rewriter::rewrite(toProp); - Node notNormalized = normalized.notNode(); - - if(d_diseq.find(notNormalized) == d_diseq.end()){ - d_out->propagate(toProp); - propagated = true; - }else{ - Node exp = d_differenceManager.explain(toProp); - Node lp = flattenAnd(exp.andNode(notNormalized)); - Debug("arith::propagate") << "propagate conflict" << lp << endl; - d_out->conflict(lp); - - propagated = true; - break; - } - }else{ + while(d_propManager.hasMorePropagations()){ + const PropManager::PropUnit next = d_propManager.getNextPropagation(); + bool flag = next.flag; + TNode toProp = next.consequent; + + TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp; + + Debug("arith::propagate") << "propagate @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl; + + if(flag) { + //Currently if the flag is set this came from an equality detected by the + //equality engine in the the difference manager. + if(toProp.getKind() == kind::EQUAL){ + Node normalized = Rewriter::rewrite(toProp); + Node notNormalized = normalized.notNode(); + + if(d_diseq.find(notNormalized) == d_diseq.end()){ d_out->propagate(toProp); propagated = true; + }else{ + Node exp = d_differenceManager.explain(toProp); + Node lp = flattenAnd(exp.andNode(notNormalized)); + Debug("arith::propagate") << "propagate conflict" << lp << endl; + d_out->conflict(lp); + + propagated = true; + break; } - }else if(inContextAtom(atom)){ - Node satValue = d_valuation.getSatValue(toProp); - AlwaysAssert(satValue.isNull()); - propagated = true; - d_out->propagate(toProp); }else{ - //Not clear if this is a good time to do this or not... - Debug("arith::propagate") << "Atom is not in context" << toProp << endl; -#warning "enable remove atom in database" - //d_atomDatabase.removeAtom(atom); + d_out->propagate(toProp); + propagated = true; } + }else if(inContextAtom(atom)){ + Node satValue = d_valuation.getSatValue(toProp); + AlwaysAssert(satValue.isNull()); + propagated = true; + d_out->propagate(toProp); + }else{ + //Not clear if this is a good time to do this or not... + Debug("arith::propagate") << "Atom is not in context" << toProp << endl; +#warning "enable remove atom in database" + //d_atomDatabase.removeAtom(atom); } + } - if(!propagated){ - //Opportunistically export previous conflicts - while(d_simplex.hasMoreLemmas()){ - Node lemma = d_simplex.popLemma(); - d_out->lemma(lemma); - } + if(!propagated){ + //Opportunistically export previous conflicts + while(d_simplex.hasMoreLemmas()){ + Node lemma = d_simplex.popLemma(); + d_out->lemma(lemma); } } } @@ -1387,7 +1385,7 @@ void TheoryArith::presolve(){ } d_learner.clear(); - check(FULL_EFFORT); + check(EFFORT_FULL); } EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 174513c72..6e0d45948 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -228,7 +228,7 @@ void TheoryDatatypes::check(Effort e) { } } - if( e == FULL_EFFORT ) { + if( e == EFFORT_FULL ) { Debug("datatypes-split") << "Check for splits " << e << endl; //do splitting for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 76aabeb1f..0404bda3b 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -31,14 +31,12 @@ TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF; std::ostream& operator<<(std::ostream& os, Theory::Effort level){ switch(level){ - case Theory::MIN_EFFORT: - os << "MIN_EFFORT"; break; - case Theory::QUICK_CHECK: - os << "QUICK_CHECK"; break; - case Theory::STANDARD: - os << "STANDARD"; break; - case Theory::FULL_EFFORT: - os << "FULL_EFFORT"; break; + case Theory::EFFORT_STANDARD: + os << "EFFORT_STANDARD"; break; + case Theory::EFFORT_FULL: + os << "EFFORT_FULL"; break; + case Theory::EFFORT_COMBINATION: + os << "EFFORT_COMBINATION"; break; default: Unreachable(); } diff --git a/src/theory/theory.h b/src/theory/theory.h index 35c81239f..1451568ab 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -241,7 +241,7 @@ public: * Returns the ID of the theory responsible for the given node. */ static inline TheoryId theoryOf(TNode node) { - Trace("theory") << "theoryOf(" << node << ")" << std::endl; + Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl; // Constants, variables, 0-ary constructors if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) { return theoryOf(node.getType()); @@ -298,28 +298,29 @@ public: * with FULL_EFFORT. */ enum Effort { - MIN_EFFORT = 0, - QUICK_CHECK = 10, - STANDARD = 50, - FULL_EFFORT = 100, - COMBINATION = 150 + /** + * Standard effort where theory need not do anything + */ + EFFORT_STANDARD = 50, + /** + * Full effort requires the theory make sure its assertions are satisfiable or not + */ + EFFORT_FULL = 100, + /** + * Combination effort means that the individual theories are already satisfied, and + * it is time to put some effort into propagation of shared term equalities + */ + EFFORT_COMBINATION = 150 };/* enum Effort */ - // simple, useful predicates for effort values - static inline bool minEffortOnly(Effort e) CVC4_CONST_FUNCTION - { return e == MIN_EFFORT; } - static inline bool quickCheckOrMore(Effort e) CVC4_CONST_FUNCTION - { return e >= QUICK_CHECK; } - static inline bool quickCheckOnly(Effort e) CVC4_CONST_FUNCTION - { return e >= QUICK_CHECK && e < STANDARD; } static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION - { return e >= STANDARD; } + { return e >= EFFORT_STANDARD; } static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION - { return e >= STANDARD && e < FULL_EFFORT; } + { return e >= EFFORT_STANDARD && e < EFFORT_FULL; } static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION - { return e == FULL_EFFORT; } + { return e == EFFORT_FULL; } static inline bool combination(Effort e) CVC4_CONST_FUNCTION - { return e == COMBINATION; } + { return e == EFFORT_COMBINATION; } /** * Get the id for this Theory. @@ -409,12 +410,12 @@ public: * - throw an exception * - or call get() until done() is true. */ - virtual void check(Effort level = FULL_EFFORT) { } + virtual void check(Effort level = EFFORT_FULL) { } /** * T-propagate new literal assignments in the current context. */ - virtual void propagate(Effort level = FULL_EFFORT) { } + virtual void propagate(Effort level = EFFORT_FULL) { } /** * Return an explanation for the literal represented by parameter n diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index ccfeb51f1..d55e12fbc 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -18,7 +18,6 @@ TESTS = \ arith-int-013.cvc \ arith-int-022.cvc \ arith-int-024.cvc \ - arith-int-041.cvc \ arith-int-042.cvc \ arith-int-042.min.cvc \ arith-int-047.cvc \ @@ -66,6 +65,7 @@ EXTRA_DIST = $(TESTS) \ arith-int-038.cvc \ arith-int-039.cvc \ arith-int-040.cvc \ + arith-int-041.cvc \ arith-int-043.cvc \ arith-int-044.cvc \ arith-int-045.cvc \ diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 4787dfd21..41d370aac 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -64,7 +64,7 @@ class TheoryArithWhite : public CxxTest::TestSuite { public: - TheoryArithWhite() : d_level(Theory::FULL_EFFORT), d_zero(0), d_one(1), debug(false) {} + TheoryArithWhite() : d_level(Theory::EFFORT_FULL), d_zero(0), d_one(1), debug(false) {} void fakeTheoryEnginePreprocess(TNode inp){ Node rewrite = inp; //FIXME this needs to enforce that inp is fully rewritten already! diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 76385219d..a737772ed 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -181,38 +181,15 @@ public: } void testEffort(){ - Theory::Effort m = Theory::MIN_EFFORT; - Theory::Effort q = Theory::QUICK_CHECK; - Theory::Effort s = Theory::STANDARD; - Theory::Effort f = Theory::FULL_EFFORT; - - TS_ASSERT( Theory::minEffortOnly(m)); - TS_ASSERT(!Theory::minEffortOnly(q)); - TS_ASSERT(!Theory::minEffortOnly(s)); - TS_ASSERT(!Theory::minEffortOnly(f)); - - TS_ASSERT(!Theory::quickCheckOnly(m)); - TS_ASSERT( Theory::quickCheckOnly(q)); - TS_ASSERT(!Theory::quickCheckOnly(s)); - TS_ASSERT(!Theory::quickCheckOnly(f)); - - TS_ASSERT(!Theory::standardEffortOnly(m)); - TS_ASSERT(!Theory::standardEffortOnly(q)); + Theory::Effort s = Theory::EFFORT_STANDARD; + Theory::Effort f = Theory::EFFORT_FULL; + TS_ASSERT( Theory::standardEffortOnly(s)); TS_ASSERT(!Theory::standardEffortOnly(f)); - TS_ASSERT(!Theory::fullEffort(m)); - TS_ASSERT(!Theory::fullEffort(q)); TS_ASSERT(!Theory::fullEffort(s)); TS_ASSERT( Theory::fullEffort(f)); - TS_ASSERT(!Theory::quickCheckOrMore(m)); - TS_ASSERT( Theory::quickCheckOrMore(q)); - TS_ASSERT( Theory::quickCheckOrMore(s)); - TS_ASSERT( Theory::quickCheckOrMore(f)); - - TS_ASSERT(!Theory::standardEffortOrMore(m)); - TS_ASSERT(!Theory::standardEffortOrMore(q)); TS_ASSERT( Theory::standardEffortOrMore(s)); TS_ASSERT( Theory::standardEffortOrMore(f)); } @@ -225,7 +202,7 @@ public: TS_ASSERT(!d_dummy->doneWrapper()); - d_dummy->check(Theory::FULL_EFFORT); + d_dummy->check(Theory::EFFORT_FULL); TS_ASSERT(d_dummy->doneWrapper()); } -- 2.30.2