From d1acfe81a013d1f8960bd0267dcd685185ffc785 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 27 May 2010 20:34:18 +0000 Subject: [PATCH] Preregistration has been turned on. Highly experimental eager splitting support has been added. Also a few bug fixes to Tableau. --- src/prop/cnf_stream.cpp | 7 ++- src/theory/arith/tableau.h | 20 +++++++-- src/theory/arith/theory_arith.cpp | 56 +++++++++++++++++++++--- src/theory/arith/theory_arith.h | 6 ++- src/theory/booleans/theory_bool.h | 11 ++++- src/theory/output_channel.h | 20 ++++++--- src/theory/theory_engine.cpp | 3 +- src/theory/theory_engine.h | 17 ++++--- test/regress/regress0/Makefile.am | 1 + test/regress/regress0/ite_real_valid.smt | 8 ++++ test/unit/theory/theory_black.h | 14 +++--- test/unit/theory/theory_uf_white.h | 13 +++--- 12 files changed, 140 insertions(+), 36 deletions(-) create mode 100644 test/regress/regress0/ite_real_valid.smt diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 51ae695cf..a245eb469 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -359,6 +359,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) { } if(somethingChanged) { + rewrite = nodeManager->mkNode(node.getKind(), newChildren); nodeManager->setAttribute(node, IteRewriteAttr(), rewrite); return rewrite; @@ -399,7 +400,11 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) { case AND: return handleAnd(node); default: - return handleAtom(handleNonAtomicNode(node)); + { + Node atomic = handleNonAtomicNode(node); + AlwaysAssert(isCached(atomic) || atomic.isAtomic()); + return toCNF(atomic); + } } } diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 7237c3a54..fa0712e7e 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -36,6 +36,7 @@ public: //TODO Assert(d_x_i.getType() == REAL); Assert(sum.getKind() == PLUS); + Rational zero(0,1); for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){ TNode pair = *iter; @@ -48,7 +49,10 @@ public: //TODO Assert(var_i.getKind() == REAL); Assert(!has(var_i)); d_nonbasic.insert(var_i); - d_coeffs[var_i] = coeff.getConst(); + Rational q = coeff.getConst(); + d_coeffs[var_i] = q; + Assert(q != zero); + Assert(d_coeffs[var_i] != zero); } } @@ -66,12 +70,13 @@ public: bool has(TNode x_j){ CoefficientTable::iterator x_jPos = d_coeffs.find(x_j); - return x_jPos != d_coeffs.end(); } Rational& lookup(TNode x_j){ - return d_coeffs[x_j]; + CoefficientTable::iterator x_jPos = d_coeffs.find(x_j); + Assert(x_jPos != d_coeffs.end()); + return (*x_jPos).second; } void pivot(TNode x_j){ @@ -89,17 +94,22 @@ public: TNode nb = *nonbasicIter; d_coeffs[nb] = d_coeffs[nb] * negInverseA_rs; } + } void subsitute(Row& row_s){ TNode x_s = row_s.basicVar(); Assert(has(x_s)); + Assert(d_nonbasic.find(x_s) != d_nonbasic.end()); Assert(x_s != d_x_i); + Rational zero(0,1); Rational a_rs = lookup(x_s); + Assert(a_rs != zero); d_coeffs.erase(x_s); + d_nonbasic.erase(x_s); for(std::set::iterator iter = row_s.d_nonbasic.begin(); iter != row_s.d_nonbasic.end(); @@ -108,6 +118,10 @@ public: Rational a_sj = a_rs * row_s.lookup(x_j); if(has(x_j)){ d_coeffs[x_j] = d_coeffs[x_j] + a_sj; + if(d_coeffs[x_j] == zero){ + d_coeffs.erase(x_j); + d_nonbasic.erase(x_j); + } }else{ d_nonbasic.insert(x_j); d_coeffs[x_j] = a_sj; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6ff74f0f9..08b609ba4 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -29,6 +29,10 @@ using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::arith; +struct EagerSplittingTag {}; +typedef expr::Attribute EagerlySplitUpon; + + TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : Theory(c, out), d_preprocessed(c), @@ -47,6 +51,29 @@ TheoryArith::~TheoryArith(){ } } +void TheoryArith::preRegisterTerm(TNode n) { + Debug("arith_preregister") << "arith: begin TheoryArith::preRegisterTerm(" + << n << ")" << endl; + + if(n.getKind() == EQUAL){ + if(!n.getAttribute(EagerlySplitUpon())){ + TNode left = n[0]; + TNode right = n[1]; + + Node lt = NodeManager::currentNM()->mkNode(LT, left,right); + Node gt = NodeManager::currentNM()->mkNode(GT, left,right); + Node eagerSplit = NodeManager::currentNM()->mkNode(OR, n, lt, gt); + + d_splits.push_back(eagerSplit); + + n.setAttribute(EagerlySplitUpon(), true); + d_out->augmentingLemma(eagerSplit); + } + } + + Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm(" + << n << ")" << endl; +} bool isBasicSum(TNode n){ if(n.getKind() != kind::PLUS) return false; @@ -220,11 +247,13 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){ TNode x_j = *basicIter; Row* row_j = d_tableau.lookup(x_j); - Rational& a_ji = row_j->lookup(x_i); + if(row_j->has(x_i)){ + Rational& a_ji = row_j->lookup(x_i); - DeltaRational assignment = d_partialModel.getAssignment(x_j); - DeltaRational nAssignment = assignment+(diff * a_ji); - d_partialModel.setAssignment(x_j, nAssignment); + DeltaRational assignment = d_partialModel.getAssignment(x_j); + DeltaRational nAssignment = assignment+(diff * a_ji); + d_partialModel.setAssignment(x_j, nAssignment); + } } d_partialModel.setAssignment(x_i, v); @@ -252,7 +281,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ TNode x_k = *basicIter; Row* row_k = d_tableau.lookup(x_k); - if(x_k != x_i){ + if(x_k != x_i && row_k->has(x_j)){ DeltaRational a_kj = row_k->lookup(x_j); DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + theta; d_partialModel.setAssignment(x_k, nextAssignment); @@ -321,7 +350,9 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 d_partialModel.beginRecordingAssignments(); while(true){ TNode x_i = selectSmallestInconsistentVar(); + Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl; if(x_i == Node::null()){ + Debug("arith_update") << "No inconsistent variables" << endl; d_partialModel.stopRecordingAssignments(false); return Node::null(); //sat } @@ -509,6 +540,8 @@ void TheoryArith::check(Effort level){ if(possibleConflict != Node::null()){ Debug("arith") << "Found a conflict " << possibleConflict << endl; d_out->conflict(possibleConflict); + }else{ + Debug("arith") << "No conflict found" << endl; } } @@ -516,22 +549,33 @@ void TheoryArith::check(Effort level){ bool enqueuedCaseSplit = false; typedef context::CDList::const_iterator diseq_iterator; for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){ + Node assertion = *i; + Debug("arith") << "splitting" << assertion << endl; TNode eq = assertion[0]; TNode x_i = eq[0]; TNode c_i = eq[1]; DeltaRational constant = c_i.getConst(); + Debug("arith") << "broken apart" << endl; if(d_partialModel.getAssignment(x_i) == constant){ + Debug("arith") << "here" << endl; enqueuedCaseSplit = true; Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i); Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i); Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt); //d_out->enqueueCaseSplits(caseSplit); + Debug("arith") << "finished" << caseSplit << endl; } + Debug("arith") << "end of for loop" << endl; + } + Debug("arith") << "finished" << endl; + if(enqueuedCaseSplit){ //d_out->caseSplit(); - Warning() << "Outstanding case split in theory arith" << endl; + //Warning() << "Outstanding case split in theory arith" << endl; } } + Debug("arith") << "TheoryArith::check end" << std::endl; + } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 7bfa535a8..1d6cca5cc 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -38,6 +38,10 @@ class TheoryArith : public Theory { private: /* Chopping block begins */ + std::vector d_splits; + //This stores the eager splits sent out of the theory. + //TODO get rid of this. + context::CDList d_preprocessed; //TODO This is currently needed to save preprocessed nodes that may not //currently have an outisde reference. Get rid of when preprocessing is occuring @@ -65,7 +69,7 @@ public: Node rewrite(TNode n); - void preRegisterTerm(TNode n) { Unimplemented(); } + void preRegisterTerm(TNode n); void registerTerm(TNode n); void check(Effort e); void propagate(Effort e) { Unimplemented(); } diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index eb6e84c39..b39663449 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -31,11 +31,18 @@ public: Theory(c, out) { } - void preRegisterTerm(TNode n) { Unimplemented(); } - void registerTerm(TNode n) { Unimplemented(); } + void preRegisterTerm(TNode n) { + Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl; + Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl; + } + void registerTerm(TNode n) { + Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl; + Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl; + } void check(Effort e) { Unimplemented(); } void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } + }; }/* CVC4::theory::booleans namespace */ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 54fa71808..08a3353e6 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -18,6 +18,7 @@ #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H #define __CVC4__THEORY__OUTPUT_CHANNEL_H +#include "util/Assert.h" #include "theory/interrupted.h" namespace CVC4 { @@ -53,7 +54,7 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint() throw(Interrupted) { + virtual void safePoint() throw(Interrupted, AssertionException) { } /** @@ -66,7 +67,7 @@ public: * * @param safe - whether it is safe to be interrupted */ - virtual void conflict(TNode n, bool safe = false) throw(Interrupted) = 0; + virtual void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; /** * Propagate a theory literal. @@ -75,7 +76,7 @@ public: * * @param safe - whether it is safe to be interrupted */ - virtual void propagate(TNode n, bool safe = false) throw(Interrupted) = 0; + virtual void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -84,7 +85,16 @@ public: * @param n - a theory lemma valid at decision level 0 * @param safe - whether it is safe to be interrupted */ - virtual void lemma(TNode n, bool safe = false) throw(Interrupted) = 0; + virtual void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; + + /** + * Tell the core to add the following valid lemma as if it were a user assertion. + * This should NOT be called during solving, only preprocessing. + * + * @param n - a theory lemma valid to be asserted + * @param safe - whether it is safe to be interrupted + */ + virtual void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; /** * Provide an explanation in response to an explanation request. @@ -92,7 +102,7 @@ public: * @param n - an explanation * @param safe - whether it is safe to be interrupted */ - virtual void explanation(TNode n, bool safe = false) throw(Interrupted) = 0; + virtual void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; };/* class OutputChannel */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d29195011..5af64c5dd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -32,8 +32,7 @@ typedef expr::Attribute PreRegistered; Node TheoryEngine::preprocess(TNode t) { Node top = rewrite(t); - Debug("rewrite") << "rewrote: " << t << "\nto : " << top << "\n"; - return top; + Debug("rewrite") << "rewrote: " << t << endl << "to : " << top << endl; list toReg; toReg.push_back(top); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e85e66e99..00336a1e3 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -68,7 +68,7 @@ class TheoryEngine { d_conflictNode(context) { } - void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted) { + void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; d_conflictNode = conflictNode; if(safe) { @@ -76,14 +76,16 @@ class TheoryEngine { } } - void propagate(TNode, bool) throw(theory::Interrupted) { + void propagate(TNode, bool) throw(theory::Interrupted, AssertionException) { } - void lemma(TNode node, bool) throw(theory::Interrupted) { + void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { d_engine->newLemma(node); } - - void explanation(TNode, bool) throw(theory::Interrupted) { + void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { + d_engine->newAugmentingLemma(node); + } + void explanation(TNode, bool) throw(theory::Interrupted, AssertionException) { } }; @@ -289,7 +291,10 @@ public: inline void newLemma(TNode node) { d_propEngine->assertLemma(node); } - + inline void newAugmentingLemma(TNode node) { + Node preprocessed = preprocess(node); + d_propEngine->assertFormula(preprocessed); + } /** * Returns the last conflict (if any). */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index e0061dcd9..515d496f5 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -11,6 +11,7 @@ TESTS = \ flet.smt \ flet2.smt \ ite_real_int_type.smt \ + ite_real_valid.smt \ let.smt \ let2.smt \ simple2.smt \ diff --git a/test/regress/regress0/ite_real_valid.smt b/test/regress/regress0/ite_real_valid.smt new file mode 100644 index 000000000..eeaaa17e0 --- /dev/null +++ b/test/regress/regress0/ite_real_valid.smt @@ -0,0 +1,8 @@ +(benchmark ite_real_valid +:logic QF_LRA +:status unsat +:extrafuns ((x Real)) +:extrapreds ((b)) +:formula + (not (implies (= x (ite b 0 1)) (>= x 0))) +) diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index e0dfd7aa8..0443b7b8e 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -47,20 +47,24 @@ public: ~TestOutputChannel() {} - void safePoint() throw(Interrupted) {} + void safePoint() throw(Interrupted, AssertionException) {} - void conflict(TNode n, bool safe = false) throw(Interrupted) { + void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) throw(Interrupted) { + void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) { push(PROPAGATE, n); } - void lemma(TNode n, bool safe = false) throw(Interrupted) { + void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){ push(LEMMA, n); } - void explanation(TNode n, bool safe = false) throw(Interrupted) { + void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){ + Unreachable(); + } + + void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) { push(EXPLANATION, n); } diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index 6b14a38d5..8be56bc79 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -48,20 +48,23 @@ public: ~TestOutputChannel() {} - void safePoint() throw(Interrupted) {} + void safePoint() throw(Interrupted, AssertionException) {} - void conflict(TNode n, bool safe = false) throw(Interrupted) { + void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) throw(Interrupted) { + void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) { push(PROPOGATE, n); } - void lemma(TNode n, bool safe = false) throw(Interrupted) { + void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) { push(LEMMA, n); } - void explanation(TNode n, bool safe = false) throw(Interrupted) { + void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){ + Unreachable(); + } + void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) { push(EXPLANATION, n); } -- 2.30.2