diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-29 10:57:50 -0400 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-29 10:57:50 -0400 |
commit | b58cff5e8757712e2b42e7ab61a7c70dab030e30 (patch) | |
tree | c830e8c34209631943229befae60e5cb326d57ee | |
parent | a36ff27dc3196f6d337699d9bb8ee9418b4270d5 (diff) | |
parent | 602265cbcddc50e84c57cd5e8836c88503cf29e0 (diff) |
Merge branch 'master' of github.com:CVC4/CVC4
45 files changed, 4091 insertions, 497 deletions
diff --git a/src/cvc4.i b/src/cvc4.i index ebb8cbd63..965452b84 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -66,6 +66,8 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %template(vectorDatatypeType) std::vector< CVC4::DatatypeType >; %template(vectorSExpr) std::vector< CVC4::SExpr >; %template(vectorString) std::vector< std::string >; +%template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >; +%template(pairStringType) std::pair< std::string, CVC4::Type >; %template(setType) std::set< CVC4::Type >; %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >; diff --git a/src/expr/command.i b/src/expr/command.i index 6085a444f..76c8fa674 100644 --- a/src/expr/command.i +++ b/src/expr/command.i @@ -54,6 +54,12 @@ // getNext() just allows C++ iterator access from Java-side next(), make it private %javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private"; +// map the types appropriately +%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject"; +%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; +%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; +%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; } + #endif /* SWIGJAVA */ %include "expr/command.h" diff --git a/src/expr/expr.i b/src/expr/expr.i index 92ab517b1..977345a63 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -72,6 +72,12 @@ namespace CVC4 { // getNext() just allows C++ iterator access from Java-side next(), make it private %javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Expr>::getNext() "private"; +// map the types appropriately +%typemap(jni) CVC4::Expr::const_iterator::value_type "jobject"; +%typemap(jtype) CVC4::Expr::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr"; +%typemap(jstype) CVC4::Expr::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr"; +%typemap(javaout) CVC4::Expr::const_iterator::value_type { return $jnicall; } + #endif /* SWIGJAVA */ %include "expr/expr.h" diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 16f9ba917..4d9cbc60d 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -39,6 +39,9 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) case kind::BUILTIN: typeNode = nodeManager->builtinOperatorType(); break; + case kind::BITVECTOR_EXTRACT_OP : + typeNode = nodeManager->builtinOperatorType(); + break; ${typerules} diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index bb9a9e417..32eaff355 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -167,6 +167,20 @@ void ArrayInfo::setRIntro1Applied(const TNode a) { } +void ArrayInfo::setModelRep(const TNode a, const TNode b) { + Assert(a.getType().isArray()); + Info* temp_info; + CNodeInfoMap::iterator it = info_map.find(a); + if(it == info_map.end()) { + temp_info = new Info(ct, bck); + temp_info->modelRep = b; + info_map[a] = temp_info; + } else { + (*it).second->modelRep = b; + } + +} + /** * Returns the information associated with TNode a */ @@ -200,6 +214,16 @@ const bool ArrayInfo::rIntro1Applied(const TNode a) const return false; } +const TNode ArrayInfo::getModelRep(const TNode a) const +{ + CNodeInfoMap::const_iterator it = info_map.find(a); + + if(it!= info_map.end()) { + return (*it).second->modelRep; + } + return TNode(); +} + const CTNodeList* ArrayInfo::getIndices(const TNode a) const{ CNodeInfoMap::const_iterator it = info_map.find(a); if(it!= info_map.end()) { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 13fae2ae5..10c15fd0e 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -63,11 +63,12 @@ class Info { public: context::CDO<bool> isNonLinear; context::CDO<bool> rIntro1Applied; + context::CDO<TNode> modelRep; CTNodeList* indices; CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false) { + Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()) { indices = new(true)CTNodeList(c); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); @@ -209,6 +210,7 @@ public: void setNonLinear(const TNode a); void setRIntro1Applied(const TNode a); + void setModelRep(const TNode a, const TNode rep); /** * Returns the information associated with TNode a @@ -220,6 +222,8 @@ public: const bool rIntro1Applied(const TNode a) const; + const TNode getModelRep(const TNode a) const; + const CTNodeList* getIndices(const TNode a) const; const CTNodeList* getStores(const TNode a) const; diff --git a/src/theory/arrays/options b/src/theory/arrays/options index 755cf239c..8a971cfe8 100644 --- a/src/theory/arrays/options +++ b/src/theory/arrays/options @@ -11,4 +11,10 @@ option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-wr option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination) +option arraysModelBased --arrays-model-based bool :default false :read-write + turn on model-based arrray solver + +option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write + turn on eager index splitting for generated array lemmas + endmodule diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index dcf4813fc..783929f97 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -48,7 +48,7 @@ const bool d_solveWrite2 = false; // These are now options //bool d_useNonLinearOpt = true; //bool d_lazyRIntro1 = true; -const bool d_eagerIndexSplitting = true; + //bool d_eagerIndexSplitting = false; TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, qe), @@ -58,6 +58,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_numExplain("theory::arrays::number of explanations", 0), d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), + d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0), + d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0), + d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0), + d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0), d_checkTimer("theory::arrays::checkTime"), d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"), d_ppFacts(u), @@ -79,8 +83,11 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_sharedOther(c), d_sharedTerms(c, false), d_reads(c), + d_skolemIndex(c, 0), d_decisionRequests(c), - d_permRef(c) + d_permRef(c), + d_modelConstraints(c), + d_inCheckModel(false) { StatisticsRegistry::registerStat(&d_numRow); StatisticsRegistry::registerStat(&d_numExt); @@ -88,6 +95,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC StatisticsRegistry::registerStat(&d_numExplain); StatisticsRegistry::registerStat(&d_numNonLinear); StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits); + StatisticsRegistry::registerStat(&d_numGetModelValSplits); + StatisticsRegistry::registerStat(&d_numGetModelValConflicts); + StatisticsRegistry::registerStat(&d_numSetModelValSplits); + StatisticsRegistry::registerStat(&d_numSetModelValConflicts); StatisticsRegistry::registerStat(&d_checkTimer); d_true = NodeManager::currentNM()->mkConst<bool>(true); @@ -119,6 +130,10 @@ TheoryArrays::~TheoryArrays() { StatisticsRegistry::unregisterStat(&d_numExplain); StatisticsRegistry::unregisterStat(&d_numNonLinear); StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits); + StatisticsRegistry::unregisterStat(&d_numGetModelValSplits); + StatisticsRegistry::unregisterStat(&d_numGetModelValConflicts); + StatisticsRegistry::unregisterStat(&d_numSetModelValSplits); + StatisticsRegistry::unregisterStat(&d_numSetModelValConflicts); StatisticsRegistry::unregisterStat(&d_checkTimer); } @@ -140,6 +155,128 @@ bool TheoryArrays::ppDisequal(TNode a, TNode b) { Rewriter::rewrite(a.eqNode(b)) == d_false); } + +Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck) +{ + if (!solve1) { + return term; + } + if (term[0].getKind() != kind::STORE && + term[1].getKind() != kind::STORE) { + return term; + } + TNode left = term[0]; + TNode right = term[1]; + int leftWrites = 0, rightWrites = 0; + + // Count nested writes + TNode e1 = left; + while (e1.getKind() == kind::STORE) { + ++leftWrites; + e1 = e1[0]; + } + + TNode e2 = right; + while (e2.getKind() == kind::STORE) { + ++rightWrites; + e2 = e2[0]; + } + + if (rightWrites > leftWrites) { + TNode tmp = left; + left = right; + right = tmp; + int tmpWrites = leftWrites; + leftWrites = rightWrites; + rightWrites = tmpWrites; + } + + NodeManager* nm = NodeManager::currentNM(); + if (rightWrites == 0) { + if (e1 != e2) { + return term; + } + // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF + // + // read(store, index_n) = v_n & + // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} & + // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} & + // ... + // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1 + // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0 + TNode write_i, write_j, index_i, index_j; + Node conc; + NodeBuilder<> result(kind::AND); + int i, j; + write_i = left; + for (i = leftWrites-1; i >= 0; --i) { + index_i = write_i[1]; + + // build: [index_i /= index_n && index_i /= index_(n-1) && + // ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i + write_j = left; + { + NodeBuilder<> hyp(kind::AND); + for (j = leftWrites - 1; j > i; --j) { + index_j = write_j[1]; + if (!ppCheck || !ppDisequal(index_i, index_j)) { + Node hyp2(index_i.getType() == nm->booleanType()? + index_i.iffNode(index_j) : index_i.eqNode(index_j)); + hyp << hyp2.notNode(); + } + write_j = write_j[0]; + } + + Node r1 = nm->mkNode(kind::SELECT, e1, index_i); + conc = (r1.getType() == nm->booleanType())? + r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]); + if (hyp.getNumChildren() != 0) { + if (hyp.getNumChildren() == 1) { + conc = hyp.getChild(0).impNode(conc); + } + else { + r1 = hyp; + conc = r1.impNode(conc); + } + } + + // And into result + result << conc; + + // Prepare for next iteration + write_i = write_i[0]; + } + } + Assert(result.getNumChildren() > 0); + if (result.getNumChildren() == 1) { + return result.getChild(0); + } + return result; + } + else { + if (!solve2) { + return term; + } + // store(...) = store(a,i,v) ==> + // store(store(...),i,select(a,i)) = a && select(store(...),i)=v + Node l = left; + Node tmp; + NodeBuilder<> nb(kind::AND); + while (right.getKind() == kind::STORE) { + tmp = nm->mkNode(kind::SELECT, l, right[1]); + nb << tmp.eqNode(right[2]); + tmp = nm->mkNode(kind::SELECT, right[0], right[1]); + l = nm->mkNode(kind::STORE, l, right[1], tmp); + right = right[0]; + } + nb << solveWrite(l.eqNode(right), solve1, solve2, ppCheck); + return nb; + } + Unreachable(); + return term; +} + + Node TheoryArrays::ppRewrite(TNode term) { if (!d_preprocess) return term; d_ppEqualityEngine.addTerm(term); @@ -163,115 +300,7 @@ Node TheoryArrays::ppRewrite(TNode term) { break; } case kind::EQUAL: { - if (!d_solveWrite) break; - if (term[0].getKind() == kind::STORE || - term[1].getKind() == kind::STORE) { - TNode left = term[0]; - TNode right = term[1]; - int leftWrites = 0, rightWrites = 0; - - // Count nested writes - TNode e1 = left; - while (e1.getKind() == kind::STORE) { - ++leftWrites; - e1 = e1[0]; - } - - TNode e2 = right; - while (e2.getKind() == kind::STORE) { - ++rightWrites; - e2 = e2[0]; - } - - if (rightWrites > leftWrites) { - TNode tmp = left; - left = right; - right = tmp; - int tmpWrites = leftWrites; - leftWrites = rightWrites; - rightWrites = tmpWrites; - } - - NodeManager* nm = NodeManager::currentNM(); - if (rightWrites == 0) { - if (e1 == e2) { - // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF - // - // read(store, index_n) = v_n & - // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} & - // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} & - // ... - // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1 - // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0 - TNode write_i, write_j, index_i, index_j; - Node conc; - NodeBuilder<> result(kind::AND); - int i, j; - write_i = left; - for (i = leftWrites-1; i >= 0; --i) { - index_i = write_i[1]; - - // build: [index_i /= index_n && index_i /= index_(n-1) && - // ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i - write_j = left; - { - NodeBuilder<> hyp(kind::AND); - for (j = leftWrites - 1; j > i; --j) { - index_j = write_j[1]; - if (!ppDisequal(index_i, index_j)) { - Node hyp2(index_i.getType() == nm->booleanType()? - index_i.iffNode(index_j) : index_i.eqNode(index_j)); - hyp << hyp2.notNode(); - } - write_j = write_j[0]; - } - - Node r1 = nm->mkNode(kind::SELECT, e1, index_i); - conc = (r1.getType() == nm->booleanType())? - r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]); - if (hyp.getNumChildren() != 0) { - if (hyp.getNumChildren() == 1) { - conc = hyp.getChild(0).impNode(conc); - } - else { - r1 = hyp; - conc = r1.impNode(conc); - } - } - - // And into result - result << conc; - - // Prepare for next iteration - write_i = write_i[0]; - } - } - Assert(result.getNumChildren() > 0); - if (result.getNumChildren() == 1) { - return result.getChild(0); - } - return result; - } - break; - } - else { - if (!d_solveWrite2) break; - // store(...) = store(a,i,v) ==> - // store(store(...),i,select(a,i)) = a && select(store(...),i)=v - Node l = left; - Node tmp; - NodeBuilder<> nb(kind::AND); - while (right.getKind() == kind::STORE) { - tmp = nm->mkNode(kind::SELECT, l, right[1]); - nb << tmp.eqNode(right[2]); - tmp = nm->mkNode(kind::SELECT, right[0], right[1]); - l = nm->mkNode(kind::STORE, l, right[1], tmp); - right = right[0]; - } - nb << l.eqNode(right); - return nb; - } - } + return solveWrite(term, d_solveWrite, d_solveWrite2, true); break; } default: @@ -330,6 +359,9 @@ bool TheoryArrays::propagate(TNode literal) } // Propagate away + if (d_inCheckModel && getSatContext()->getLevel() != d_topLevel) { + return true; + } bool ok = d_out->propagate(literal); if (!ok) { d_conflict = true; @@ -453,6 +485,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) d_infoMap.addStore(node, node); d_infoMap.addInStore(a, node); + d_infoMap.setModelRep(node, node); checkStore(node); break; @@ -554,6 +587,7 @@ void TheoryArrays::computeCareGraph() } } } + if (options::arraysModelBased()) return; if (d_sharedTerms) { vector< pair<TNode, TNode> > currentPairs; @@ -821,7 +855,40 @@ void TheoryArrays::presolve() ///////////////////////////////////////////////////////////////////////////// +Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual) +{ + Node skolem; + std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref); + if (it == d_skolemCache.end()) { + NodeManager* nm = NodeManager::currentNM(); + skolem = nm->mkSkolem(name, type, comment); + d_skolemCache[ref] = skolem; + } + else { + skolem = (*it).second; + if (d_equalityEngine.hasTerm(ref) && + d_equalityEngine.hasTerm(skolem) && + d_equalityEngine.areEqual(ref, skolem)) { + makeEqual = false; + } + } + preRegisterTermInternal(skolem); + if (makeEqual) { + Node d = skolem.eqNode(ref); + Debug("arrays-model-based") << "Asserting skolem equality " << d << endl; + d_equalityEngine.assertEquality(d, true, d_true); + Assert(!d_conflict); + d_skolemAssertions.push_back(d); + d_skolemIndex = d_skolemIndex + 1; + } + return skolem; +} + + void TheoryArrays::check(Effort e) { + if (done() && !fullEffort(e)) { + return; + } TimerStat::CodeTimer codeTimer(d_checkTimer); while (!done() && !d_conflict) @@ -852,13 +919,18 @@ void TheoryArrays::check(Effort e) { switch (fact.getKind()) { case kind::EQUAL: d_equalityEngine.assertEquality(fact, true, fact); + if (!fact[0].getType().isArray()) { + d_modelConstraints.push_back(fact); + } break; case kind::SELECT: d_equalityEngine.assertPredicate(fact, true, fact); + d_modelConstraints.push_back(fact); break; case kind::NOT: if (fact[0].getKind() == kind::SELECT) { d_equalityEngine.assertPredicate(fact[0], false, fact); + d_modelConstraints.push_back(fact); } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1], false)) { // Assert the dis-equality d_equalityEngine.assertEquality(fact[0], false, fact); @@ -867,16 +939,7 @@ void TheoryArrays::check(Effort e) { if(fact[0][0].getType().isArray() && !d_conflict) { NodeManager* nm = NodeManager::currentNM(); TypeNode indexType = fact[0][0].getType()[0]; - TNode k; - std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact); - if (it == d_diseqCache.end()) { - Node newk = nm->mkSkolem("array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays"); - d_diseqCache[fact] = newk; - k = newk; - } - else { - k = (*it).second; - } + TNode k = getSkolem(fact,"array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays", false); Node ak = nm->mkNode(kind::SELECT, fact[0][0], k); Node bk = nm->mkNode(kind::SELECT, fact[0][1], k); @@ -887,6 +950,9 @@ void TheoryArrays::check(Effort e) { d_out->lemma(lemma); ++d_numExt; } + else { + d_modelConstraints.push_back(fact); + } } break; default: @@ -894,8 +960,11 @@ void TheoryArrays::check(Effort e) { } } - // If in conflict, output the conflict - if(!d_eagerLemmas && fullEffort(e) && !d_conflict) { + if (options::arraysModelBased() && !d_conflict && (options::arraysEagerIndexSplitting() || fullEffort(e))) { + checkModel(e); + } + + if(!d_eagerLemmas && fullEffort(e) && !d_conflict && !options::arraysModelBased()) { // generate the lemmas on the worklist Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n"; dischargeLemmas(); @@ -905,43 +974,754 @@ void TheoryArrays::check(Effort e) { } -Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions) +void TheoryArrays::convertNodeToAssumptions(TNode node, vector<TNode>& assumptions, TNode nodeSkip) +{ + Assert(node.getKind() == kind::AND); + for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) { + if ((*child_it).getKind() == kind::AND) { + convertNodeToAssumptions(*child_it, assumptions, nodeSkip); + } + else if (*child_it != nodeSkip) { + assumptions.push_back(*child_it); + } + } +} + + +void TheoryArrays::preRegisterStores(TNode s) +{ + if (d_equalityEngine.hasTerm(s)) { + return; + } + if (s.getKind() == kind::STORE) { + preRegisterStores(s[0]); + preRegisterTermInternal(s); + } +} + + +void TheoryArrays::checkModel(Effort e) +{ + d_inCheckModel = true; + d_topLevel = getSatContext()->getLevel(); + Assert(d_skolemIndex == 0); + Assert(d_skolemAssertions.empty()); + Assert(d_lemmas.empty()); + + if (fullEffort(e)) { + // Add constraints for shared terms + context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(), shared_it2; + Node modelVal, modelVal2, d; + vector<TNode> assumptions; + for (; shared_it != shared_it_end; ++shared_it) { + if ((*shared_it).getType().isArray()) { + continue; + } + if ((*shared_it).isConst()) { + modelVal = (*shared_it); + } + else { + modelVal = d_valuation.getModelValue(*shared_it); + if (modelVal.isNull()) { + continue; + } + } + Assert(modelVal.isConst()); + for (shared_it2 = shared_it, ++shared_it2; shared_it2 != shared_it_end; ++shared_it2) { + if ((*shared_it2).getType() != (*shared_it).getType()) { + continue; + } + if ((*shared_it2).isConst()) { + modelVal2 = (*shared_it2); + } + else { + modelVal2 = d_valuation.getModelValue(*shared_it2); + if (modelVal2.isNull()) { + continue; + } + } + Assert(modelVal2.isConst()); + d = (*shared_it).eqNode(*shared_it2); + if (modelVal != modelVal2) { + d = d.notNode(); + } + if (!setModelVal(d, d_true, false, true, assumptions)) { + assumptions.push_back(d); + d_lemmas.push_back(mkAnd(assumptions, true)); + goto finish; + } + assumptions.clear(); + } + } + } + { + // TODO: record and replay decisions + int baseLevel = getSatContext()->getLevel(); + unsigned constraintIdx; + Node assertion, assertionToCheck; + vector<TNode> assumptions; + while (true) { + int level = getSatContext()->getLevel(); + d_getModelValCache.clear(); + for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) { + assertion = d_modelConstraints[constraintIdx]; + if (getModelValRec(assertion) != d_true) { + break; + } + } + getSatContext()->popto(level); + if (constraintIdx == d_modelConstraints.size()) { + break; + } + + if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) { + assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false); + if (assertionToCheck.getKind() == kind::AND && + assertionToCheck[assertionToCheck.getNumChildren()-1].getKind() == kind::EQUAL) { + TNode s = assertionToCheck[assertionToCheck.getNumChildren()-1][0]; + preRegisterStores(s); + } + } + else { + assertionToCheck = assertion; + } + // TODO: try not collecting assumptions the first time + while (!setModelVal(assertionToCheck, d_true, false, true, assumptions)) { + restart: + if (assertion.getKind() == kind::EQUAL) { + d_equalityEngine.explainEquality(assertion[0], assertion[1], true, assumptions); + } + else { + assumptions.push_back(assertion); + } +#ifdef CVC4_ASSERTIONS + std::set<TNode> validAssumptions; + context::CDList<Assertion>::const_iterator assert_it2 = facts_begin(); + for (; assert_it2 != facts_end(); ++assert_it2) { + validAssumptions.insert(*assert_it2); + } + for (unsigned i = 0; i < d_decisions.size(); ++i) { + validAssumptions.insert(d_decisions[i]); + } +#endif + std::set<TNode> all; + std::set<TNode> explained; + unsigned i = 0; + TNode t; + for (; i < assumptions.size(); ++i) { + t = assumptions[i]; + if (t == d_true) { + continue; + } + if (t.getKind() == kind::AND) { + for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) { + Assert(validAssumptions.find(*child_it) != validAssumptions.end()); + all.insert(*child_it); + } + } + // Expand explanation resulting from propagating a ROW lemma + else if (t.getKind() == kind::OR) { + if ((explained.find(t) == explained.end())) { + Assert(t[1].getKind() == kind::EQUAL); + d_equalityEngine.explainEquality(t[1][0], t[1][1], false, assumptions); + explained.insert(t); + } + continue; + } + else { + Assert(validAssumptions.find(t) != validAssumptions.end()); + all.insert(t); + } + } + // d_lemmas.push_back(mkAnd(assumptions, true)); + + bool eq = false; + Node decision, explanation; + while (!d_decisions.empty()) { + getSatContext()->pop(); + decision = d_decisions.back(); + d_decisions.pop_back(); + if (all.find(decision) != all.end()) { + if (getSatContext()->getLevel() < baseLevel) { + if (all.size() == 1) { + d_lemmas.push_back(decision.negate()); + } + else { + NodeBuilder<> disjunction(kind::OR); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + disjunction << (*it).negate(); + ++it; + } + d_lemmas.push_back(disjunction); + } + goto finish; + } + all.erase(decision); + eq = false; + if (decision.getKind() == kind::NOT) { + decision = decision[0]; + eq = true; + } + while (getSatContext()->getLevel() != baseLevel && all.find(d_decisions.back()) == all.end()) { + getSatContext()->pop(); + d_decisions.pop_back(); + } + break; + } + else { + decision = Node(); + } + } + if (all.size() == 0) { + explanation = d_true; + } + if (all.size() == 1) { + // All the same, or just one + explanation = *(all.begin()); + } + else { + NodeBuilder<> conjunction(kind::AND); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++it; + } + explanation = conjunction; + d_permRef.push_back(explanation); + } + if (decision.isNull()) { + // d_lemmas.pop_back(); + d_conflictNode = explanation; + d_conflict = true; + break; + } + d_equalityEngine.assertEquality(decision, eq, explanation); + if (!eq) decision = decision.notNode(); + Debug("arrays-model-based") << "Asserting learned literal " << decision << " with explanation " << explanation << endl; + if (d_conflict) { + assumptions.clear(); + convertNodeToAssumptions(d_conflictNode, assumptions, TNode()); + assertion = d_true; + goto restart; + } + assumptions.clear(); + + // Reassert skolems if necessary + Node d; + while (d_skolemIndex < d_skolemAssertions.size()) { + d = d_skolemAssertions[d_skolemIndex]; + Assert(isLeaf(d[0])); + if (!d_equalityEngine.hasTerm(d[0])) { + preRegisterTermInternal(d[0]); + } + if (d[0].getType().isArray()) { + Assert(d[1].getKind() == kind::STORE); + if (d[1][0].getKind() == kind::STORE) { + if (!d_equalityEngine.hasTerm(d[1][0][0])) { + preRegisterTermInternal(d[1][0][0]); + } + if (!d_equalityEngine.hasTerm(d[1][0][2])) { + preRegisterTermInternal(d[1][0][2]); + } + } + if (!d_equalityEngine.hasTerm(d[1][0])) { + preRegisterTermInternal(d[1][0]); + } + if (!d_equalityEngine.hasTerm(d[1][2])) { + preRegisterTermInternal(d[1][2]); + } + if (!d_equalityEngine.hasTerm(d[1])) { + preRegisterTermInternal(d[1]); + } + } + Debug("arrays-model-based") << "Re-asserting skolem equality " << d << endl; + d_equalityEngine.assertEquality(d, true, d_true); + Assert(!d_conflict); + if (!d[0].getType().isArray()) { + if (!setModelVal(d[1], d[0], false, true, assumptions)) { + assertion = d_true; + goto restart; + } + assumptions.clear(); + } + d_skolemIndex = d_skolemIndex + 1; + } + } + if (d_conflict) { + break; + } + // Assert(getModelVal(assertion) == d_true); + assumptions.clear(); + } +#ifdef CVC4_ASSERTIONS + if (!d_conflict) { + context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); + for (; assert_it != assert_it_end; ++assert_it) { + Assert(getModelVal(*assert_it) == d_true); + } + } +#endif + } + finish: + while (!d_decisions.empty()) { + Assert(!d_conflict); + getSatContext()->pop(); + d_decisions.pop_back(); + } + d_skolemAssertions.clear(); + d_skolemIndex = 0; + while (!d_lemmas.empty()) { + Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl; + d_out->lemma(d_lemmas.back()); + d_lemmas.pop_back(); + } + Assert(getSatContext()->getLevel() == d_topLevel); + if (d_conflict) { + Node tmp = d_conflictNode; + d_out->conflict(tmp); + } + d_inCheckModel = false; +} + + +Node TheoryArrays::getModelVal(TNode node) +{ + int level = getSatContext()->getLevel(); + d_getModelValCache.clear(); + Node ret = getModelValRec(node); + getSatContext()->popto(level); + return ret; +} + + +Node TheoryArrays::getModelValRec(TNode node) +{ + if (node.isConst()) { + return node; + } + NodeMap::iterator it = d_getModelValCache.find(node); + if (it != d_getModelValCache.end()) { + return (*it).second; + } + Node val; + switch (node.getKind()) { + case kind::NOT: + val = getModelValRec(node[0]) == d_true ? d_false : d_true; + break; + case kind::AND: { + val = d_true; + for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) { + if (getModelValRec(*child_it) != d_true) { + val = d_false; + break; + } + } + break; + } + case kind::IMPLIES: + if (getModelValRec(node[0]) == d_false) { + val = d_true; + } + else { + val = getModelValRec(node[1]); + } + case kind::EQUAL: + val = getModelValRec(node[0]); + val = (val == getModelValRec(node[1])) ? d_true : d_false; + break; + case kind::SELECT: { + NodeManager* nm = NodeManager::currentNM(); + Node indexVal = getModelValRec(node[1]); + val = Rewriter::rewrite(nm->mkNode(kind::SELECT, node[0], indexVal)); + if (val.isConst()) { + break; + } + val = Rewriter::rewrite(nm->mkNode(kind::SELECT, getModelValRec(node[0]), indexVal)); + Assert(val.isConst()); + break; + } + case kind::STORE: { + NodeManager* nm = NodeManager::currentNM(); + val = getModelValRec(node[0]); + val = Rewriter::rewrite(nm->mkNode(kind::STORE, val, getModelValRec(node[1]), getModelValRec(node[2]))); + Assert(val.isConst()); + break; + } + default: { + Assert(isLeaf(node)); + TNode eRep = d_equalityEngine.getRepresentative(node); + if (eRep.isConst()) { + val = eRep; + break; + } + TNode rep = d_infoMap.getModelRep(eRep); + if (!rep.isNull()) { + // TODO: check for loop here + val = getModelValRec(rep); + } + else { + NodeMap::iterator it = d_lastVal.find(eRep); + if (it != d_lastVal.end()) { + val = (*it).second; + if (!d_equalityEngine.hasTerm(val) || + !d_equalityEngine.areDisequal(eRep, val, true)) { + getSatContext()->push(); + ++d_numGetModelValSplits; + d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true); + if (!d_conflict) { + break; + } + ++d_numGetModelValConflicts; + getSatContext()->pop(); + } + } + + TypeEnumerator te(eRep.getType()); + val = *te; + while (true) { + if (!d_equalityEngine.hasTerm(val) || + !d_equalityEngine.areDisequal(eRep, val, true)) { + getSatContext()->push(); + ++d_numGetModelValSplits; + d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true); + if (!d_conflict) { + d_lastVal[eRep] = val; + break; + } + ++d_numGetModelValConflicts; + getSatContext()->pop(); + } + ++te; + if (te.isFinished()) { + Assert(false); + // TODO: conflict + break; + } + val = *te; + } + } + break; + } + } + d_getModelValCache[node] = val; + return val; +} + + +bool TheoryArrays::hasLoop(TNode node, TNode target) +{ + if (node == target) { + return true; + } + + if (isLeaf(node)) { + TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node)); + if (!rep.isNull()) { + return hasLoop(rep, target); + } + return false; + } + + for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) { + if (hasLoop(*child_it, target)) { + return true; + } + } + + return false; +} + + +// Return true iff it we were able to modify model so that value of node has same value as val +bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, vector<TNode>& assumptions) +{ + Assert(!d_conflict); + if (node == val) { + return !invert; + } + if (node.isConst()) { + if (invert) { + return (val.isConst() && node != val); + } + return val == node; + } + switch(node.getKind()) { + case kind::NOT: + Assert(val == d_true || val == d_false); + return setModelVal(node[0], val, !invert, explain, assumptions); + break; + case kind::AND: { + Assert(val == d_true || val == d_false); + if (val == d_false) { + invert = !invert; + } + int i; + for(i = node.getNumChildren()-1; i >=0; --i) { + if (setModelVal(node[i], d_true, invert, explain, assumptions) == invert) { + return invert; + } + } + return !invert; + } + case kind::IMPLIES: + Assert(val == d_true || val == d_false); + if (val == d_false) { + invert = !invert; + } + if (setModelVal(node[0], d_false, invert, explain, assumptions) == !invert) { + return !invert; + } + if (setModelVal(node[1], d_true, invert, explain, assumptions) == !invert) { + return !invert; + } + return invert; + case kind::EQUAL: + Assert(val == d_true || val == d_false); + if (val == d_false) { + invert = !invert; + } + if (node[0].isConst()) { + return setModelVal(node[1], node[0], invert, explain, assumptions); + } + else { + return setModelVal(node[0], node[1], invert, explain, assumptions); + } + case kind::SELECT: { + TNode s = node[0]; + Node index = node[1]; + + while (s.getKind() == kind::STORE) { + if (setModelVal(s[1].eqNode(index), d_true, false, explain, assumptions)) { + if (setModelVal(s[2].eqNode(val), d_true, invert, explain, assumptions)) { + return true; + } + // Now try to set the indices to be disequal + if (!setModelVal(s[1].eqNode(index), d_false, false, explain, assumptions)) { + return false; + } + Unreachable(); + } + s = s[0]; + } + TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(s)); + NodeManager* nm = NodeManager::currentNM(); + if (!rep.isNull()) { + // TODO: check for loop + if (explain) { + d_equalityEngine.explainEquality(s, rep, true, assumptions); + } + return setModelVal(nm->mkNode(kind::SELECT, rep, index), val, invert, explain, assumptions); + } + if (val.getKind() == kind::SELECT && val[0].getKind() == kind::STORE) { + return setModelVal(val, nm->mkNode(kind::SELECT, s, index), invert, explain, assumptions); + } + + // Solve equation for s: select(s,index) op val --> s = store(s',i',v') /\ index = i' /\ v' op val + Node newVarArr = getSkolem(s, "array_model_arr_var_$$", s.getType(), "a new array variable from the theory of arrays", false); + Assert(d_infoMap.getModelRep(d_equalityEngine.getRepresentative(newVarArr)).isNull()); + Node lookup; + bool checkIndex1 = false, checkIndex2 = false, checkIndex3 = false; + if (!isLeaf(index)) { + index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays"); + if (!index.getType().isArray()) { + checkIndex1 = true; + } + } + lookup = nm->mkNode(kind::SELECT, s, index); + Node newVarVal = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false); + + Node newVarVal2; + Node index2; + TNode saveVal = val; + if (val.getKind() == kind::SELECT && val[0] == s) { + // Special case: select(s,index) = select(s,j): solution becomes s = store(store(s',j,v'),index,w') /\ v' = w' + index2 = val[1]; + if (!isLeaf(index2)) { + index2 = getSkolem(val, "array_model_index_$$", index2.getType(), "a new index variable from the theory of arrays"); + if (!index2.getType().isArray()) { + checkIndex2 = true; + } + } + if (invert) { + checkIndex3 = true; + } + lookup = nm->mkNode(kind::SELECT, s, index2); + newVarVal2 = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false); + newVarArr = nm->mkNode(kind::STORE, newVarArr, index2, newVarVal2); + preRegisterTermInternal(newVarArr); + val = newVarVal2; + } + + Node d = nm->mkNode(kind::STORE, newVarArr, index, newVarVal); + preRegisterTermInternal(d); + d = s.eqNode(d); + Debug("arrays-model-based") << "Asserting array skolem equality " << d << endl; + d_equalityEngine.assertEquality(d, true, d_true); + d_skolemAssertions.push_back(d); + d_skolemIndex = d_skolemIndex + 1; + Assert(!d_conflict); + if (checkIndex1) { + if (!setModelVal(node[1], index, false, explain, assumptions)) { + return false; + } + } + if (checkIndex2) { + if (!setModelVal(saveVal[1], index2, false, explain, assumptions)) { + return false; + } + } + if (checkIndex3) { + if (!setModelVal(index2, index, true, explain, assumptions)) { + return false; + } + } + return setModelVal(newVarVal, val, invert, explain, assumptions); + } + case kind::STORE: + if (val.getKind() != kind::STORE) { + return setModelVal(val, node, invert, explain, assumptions); + } + Unreachable(); + break; + default: { + Assert(isLeaf(node)); + TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node)); + if (!rep.isNull()) { + // Assume this array equation has already been dealt with - otherwise, it shouldn't have a rep + return true; + } + if (val.getKind() == kind::SELECT) { + return setModelVal(val, node, invert, explain, assumptions); + } + if (d_equalityEngine.hasTerm(node) && + d_equalityEngine.hasTerm(val)) { + if ((!invert && d_equalityEngine.areDisequal(node, val, true)) || + (invert && d_equalityEngine.areEqual(node, val))) { + if (explain) { + d_equalityEngine.explainEquality(node, val, invert, assumptions); + } + return false; + } + if ((!invert && d_equalityEngine.areEqual(node, val)) || + (invert && d_equalityEngine.areDisequal(node, val, true))) { + return true; + } + } + getSatContext()->push(); + Node d = node.eqNode(val); + d_decisions.push_back(invert ? d.notNode() : d); + d_equalityEngine.assertEquality(d, !invert, d_decisions.back()); + Debug("arrays-model-based") << "Asserting " << d_decisions.back() << " with explanation " << d_decisions.back() << endl; + ++d_numSetModelValSplits; + if (d_conflict) { + ++d_numSetModelValConflicts; + Debug("arrays-model-based") << "...which results in a conflict!" << endl; + d = d_decisions.back(); + unsigned sz = assumptions.size(); + convertNodeToAssumptions(d_conflictNode, assumptions, d); + unsigned sz2 = assumptions.size(); + Assert(sz2 > sz); + Node explanation; + if (sz2 == sz+1) { + explanation = assumptions[sz]; + } + else { + NodeBuilder<> conjunction(kind::AND); + for (unsigned i = sz; i < sz2; ++i) { + conjunction << assumptions[i]; + } + explanation = conjunction; + } + // assumptions.push_back(d); + // d_lemmas.push_back(mkAnd(assumptions, true, sz)); + // while (assumptions.size() > sz2) { + // assumptions.pop_back(); + // } + getSatContext()->pop(); + d_decisions.pop_back(); + d_permRef.push_back(explanation); + d = d.negate(); + Debug("arrays-model-based") << "Asserting learned literal " << d << " with explanation " << explanation << endl; + bool eq = true; + if (d.getKind() == kind::NOT) { + d = d[0]; + eq = false; + } + d_equalityEngine.assertEquality(d, eq, explanation); + if (d_conflict) { + Assert(false); + } + return false; + } + return true; + } + } + Unreachable(); + return false; +} + + +Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned startIndex) { Assert(conjunctions.size() > 0); std::set<TNode> all; std::set<TNode> explained; - unsigned i = 0; + unsigned i = startIndex; TNode t; for (; i < conjunctions.size(); ++i) { t = conjunctions[i]; - - // Expand explanation resulting from propagating a ROW lemma - if (t.getKind() == kind::OR) { + if (t == d_true) { + continue; + } + else if (t.getKind() == kind::AND) { + for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) { + if (*child_it == d_true) { + continue; + } + all.insert(*child_it); + } + } + else if (t.getKind() == kind::OR) { + // Expand explanation resulting from propagating a ROW lemma if ((explained.find(t) == explained.end())) { Assert(t[1].getKind() == kind::EQUAL); d_equalityEngine.explainEquality(t[1][0], t[1][1], false, conjunctions); explained.insert(t); } - continue; } - all.insert(t); + else { + all.insert(t); + } } if (all.size() == 0) { - return d_true; + return invert ? d_false : d_true; } if (all.size() == 1) { // All the same, or just one - return *(all.begin()); + if (invert) { + return (*(all.begin())).negate(); + } + else { + return *(all.begin()); + } } - NodeBuilder<> conjunction(kind::AND); + NodeBuilder<> conjunction(invert ? kind::OR : kind::AND); std::set<TNode>::const_iterator it = all.begin(); std::set<TNode>::const_iterator it_end = all.end(); while (it != it_end) { - conjunction << *it; + if (invert) { + conjunction << (*it).negate(); + } + else { + conjunction << *it; + } ++ it; } @@ -951,6 +1731,7 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions) void TheoryArrays::setNonLinear(TNode a) { + if (options::arraysModelBased()) return; if (d_infoMap.isNonLinear(a)) return; Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; @@ -1063,6 +1844,86 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b) } +Node TheoryArrays::removeRepLoops(TNode a, TNode rep) +{ + if (rep.getKind() != kind::STORE) { + Assert(isLeaf(rep)); + TNode tmp = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(rep)); + if (!tmp.isNull()) { + Node tmp2 = removeRepLoops(a, tmp); + if (tmp != tmp2) { + return tmp2; + } + } + return rep; + } + + Node s = removeRepLoops(a, rep[0]); + bool changed = (s != rep[0]); + + Node index = rep[1]; + Node value = rep[2]; + Node lookup; + + // TODO: Change to hasLoop? + if (!isLeaf(index)) { + changed = true; + index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays", false); + if (!d_equalityEngine.hasTerm(index) || + !d_equalityEngine.hasTerm(rep[1]) || + !d_equalityEngine.areEqual(rep[1], index)) { + Node d = index.eqNode(rep[1]); + Debug("arrays-model-based") << "Asserting skolem equality " << d << endl; + d_equalityEngine.assertEquality(d, true, d_true); + d_modelConstraints.push_back(d); + } + } + if (!isLeaf(value)) { + changed = true; + value = getSkolem(value, "array_model_var_$$", value.getType(), "a new value variable from the theory of arrays", false); + if (!d_equalityEngine.hasTerm(value) || + !d_equalityEngine.hasTerm(rep[2]) || + !d_equalityEngine.areEqual(rep[2], value)) { + Node d = value.eqNode(rep[2]); + Debug("arrays-model-based") << "Asserting skolem equality " << d << endl; + d_equalityEngine.assertEquality(d, true, d_true); + d_modelConstraints.push_back(d); + } + } + if (changed) { + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::STORE, s, index, value); + } + return rep; +} + + +Node TheoryArrays::expandStores(TNode s, vector<TNode>& assumptions, bool checkLoop, TNode a, TNode loopRep) +{ + if (s.getKind() != kind::STORE) { + Assert(isLeaf(s)); + TNode tmp = d_equalityEngine.getRepresentative(s); + if (checkLoop && tmp == a) { + // Loop detected + d_equalityEngine.explainEquality(s, loopRep, true, assumptions); + return loopRep; + } + tmp = d_infoMap.getModelRep(tmp); + if (!tmp.isNull()) { + d_equalityEngine.explainEquality(s, tmp, true, assumptions); + return expandStores(tmp, assumptions, checkLoop, a, loopRep); + } + return s; + } + Node tmp = expandStores(s[0], assumptions, checkLoop, a, loopRep); + if (tmp != s[0]) { + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::STORE, tmp, s[1], s[2]); + } + return s; +} + + void TheoryArrays::mergeArrays(TNode a, TNode b) { // Note: a is the new representative @@ -1085,7 +1946,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) checkRIntro1(b, a); } - if (options::arraysOptimizeLinear()) { + if (options::arraysOptimizeLinear() && !options::arraysModelBased()) { bool aNL = d_infoMap.isNonLinear(a); bool bNL = d_infoMap.isNonLinear(b); if (aNL) { @@ -1120,6 +1981,74 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) checkRowLemmas(a,b); checkRowLemmas(b,a); + if (options::arraysModelBased()) { + TNode repA = d_infoMap.getModelRep(a); + Assert(repA.isNull() || d_equalityEngine.areEqual(a, repA)); + TNode repB = d_infoMap.getModelRep(b); + Assert(repB.isNull() || d_equalityEngine.areEqual(a, repB)); + Node rep; + bool done = false; + if (repA.isNull()) { + if (repB.isNull()) { + done = true; + } + else { + rep = repB; + } + } + else { + if (repB.isNull()) { + rep = repA; + } + else { + vector<TNode> assumptions; + rep = expandStores(repA, assumptions, true, a, repB); + if (rep != repA) { + Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl; + d_infoMap.setModelRep(a, rep); + Node reason = mkAnd(assumptions); + d_permRef.push_back(reason); + d_equalityEngine.assertEquality(repA.eqNode(rep), true, reason); + } + d_modelConstraints.push_back(rep.eqNode(repB)); + done = true; + } + } + if (!done) { + // 1. Check for store loop + TNode s = rep; + while (true) { + Assert(s.getKind() == kind::STORE); + while (s.getKind() == kind::STORE) { + s = s[0]; + } + Assert(isLeaf(s)); + TNode tmp = d_equalityEngine.getRepresentative(s); + if (tmp == a) { + d_modelConstraints.push_back(s.eqNode(rep)); + rep = TNode(); + break; + } + tmp = d_infoMap.getModelRep(tmp); + if (tmp.isNull()) { + break; + } + s = tmp; + } + if (!rep.isNull()) { + Node repOrig = rep; + rep = removeRepLoops(a, rep); + if (repOrig != rep) { + d_equalityEngine.assertEquality(repOrig.eqNode(rep), true, d_true); + } + } + if (rep != repA) { + Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl; + d_infoMap.setModelRep(a, rep); + } + } + } + // merge info adds the list of the 2nd argument to the first d_infoMap.mergeInfo(a, b); @@ -1139,6 +2068,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) void TheoryArrays::checkStore(TNode a) { + if (options::arraysModelBased()) return; Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n"; if(Trace.isOn("arrays-cri")) { @@ -1168,6 +2098,7 @@ void TheoryArrays::checkStore(TNode a) { void TheoryArrays::checkRowForIndex(TNode i, TNode a) { + if (options::arraysModelBased()) return; Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n"; Trace("arrays-cri")<<" index "<<i<<"\n"; @@ -1211,6 +2142,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) // look for new ROW lemmas void TheoryArrays::checkRowLemmas(TNode a, TNode b) { + if (options::arraysModelBased()) return; Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n"; if(Trace.isOn("arrays-crl")) d_infoMap.getInfo(a)->print(); @@ -1323,7 +2255,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } // Prefer equality between indexes so as not to introduce new read terms - if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) { + if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) { Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); getOutputChannel().requirePhase(i_eq_j, true); d_decisionRequests.push(i_eq_j); @@ -1494,7 +2426,9 @@ void TheoryArrays::conflict(TNode a, TNode b) { } else { d_conflictNode = explain(a.eqNode(b)); } - d_out->conflict(d_conflictNode); + if (!d_inCheckModel) { + d_out->conflict(d_conflictNode); + } d_conflict = true; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 172482e71..b659a8e68 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -115,6 +115,14 @@ class TheoryArrays : public Theory { IntStat d_numNonLinear; /** splits on array variables */ IntStat d_numSharedArrayVarSplits; + /** splits in getModelVal */ + IntStat d_numGetModelValSplits; + /** conflicts in getModelVal */ + IntStat d_numGetModelValConflicts; + /** splits in setModelVal */ + IntStat d_numSetModelValSplits; + /** conflicts in setModelVal */ + IntStat d_numSetModelValConflicts; /** time spent in check() */ TimerStat d_checkTimer; @@ -152,6 +160,7 @@ class TheoryArrays : public Theory { Node preprocessTerm(TNode term); Node recursivePreprocessTerm(TNode term); bool ppDisequal(TNode a, TNode b); + Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck); public: @@ -339,17 +348,24 @@ class TheoryArrays : public Theory { CDNodeSet d_sharedOther; context::CDO<bool> d_sharedTerms; context::CDList<TNode> d_reads; - std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache; + std::hash_map<Node, Node, NodeHashFunction> d_skolemCache; + context::CDO<unsigned> d_skolemIndex; + std::vector<Node> d_skolemAssertions; // The decision requests we have for the core context::CDQueue<Node> d_decisionRequests; // List of nodes that need permanent references in this context context::CDList<Node> d_permRef; + context::CDList<Node> d_modelConstraints; + std::vector<Node> d_lemmas; - Node mkAnd(std::vector<TNode>& conjunctions); + Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); + Node mkAnd(std::vector<TNode>& conjunctions, bool invert = false, unsigned startIndex = 0); void setNonLinear(TNode a); void checkRIntro1(TNode a, TNode b); + Node removeRepLoops(TNode a, TNode rep); + Node expandStores(TNode s, std::vector<TNode>& assumptions, bool checkLoop = false, TNode a = TNode(), TNode b = TNode()); void mergeArrays(TNode a, TNode b); void checkStore(TNode a); void checkRowForIndex(TNode i, TNode a); @@ -357,6 +373,21 @@ class TheoryArrays : public Theory { void queueRowLemma(RowLemmaType lem); void dischargeLemmas(); + std::vector<Node> d_decisions; + bool d_inCheckModel; + int d_topLevel; + void convertNodeToAssumptions(TNode node, std::vector<TNode>& assumptions, TNode nodeSkip); + void preRegisterStores(TNode s); + void checkModel(Effort e); + bool hasLoop(TNode node, TNode target); + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_getModelValCache; + NodeMap d_lastVal; + Node getModelVal(TNode node); + Node getModelValRec(TNode node); + bool setModelVal(TNode node, TNode val, bool invert, + bool explain, std::vector<TNode>& assumptions); + public: eq::EqualityEngine* getEqualityEngine() { diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index ab6382770..a70521791 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -13,12 +13,18 @@ libbv_la_SOURCES = \ bitblaster.h \ bitblaster.cpp \ bv_subtheory.h \ - bv_subtheory_eq.h \ - bv_subtheory_eq.cpp \ + bv_subtheory_core.h \ + bv_subtheory_core.cpp \ bv_subtheory_bitblast.h \ bv_subtheory_bitblast.cpp \ + bv_subtheory_inequality.h \ + bv_subtheory_inequality.cpp \ + bv_inequality_graph.h \ + bv_inequality_graph.cpp \ bitblast_strategies.h \ bitblast_strategies.cpp \ + slicer.h \ + slicer.cpp \ theory_bv.h \ theory_bv.cpp \ theory_bv_rewrite_rules.h \ diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 4f5325e10..d3a54a3e4 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -412,16 +412,43 @@ bool Bitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } -Node Bitblaster::getVarValue(TNode a) { +bool Bitblaster::hasValue(TNode a) { Assert (d_termCache.find(a) != d_termCache.end()); Bits bits = d_termCache[a]; + for (int i = bits.size() -1; i >= 0; --i) { + SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { + SatLiteral bit = d_cnfStream->getLiteral(bits[i]); + bit_value = d_satSolver->value(bit); + if (bit_value == SAT_VALUE_UNKNOWN) + return false; + } else { + return false; + } + } + return true; +} +/** + * Returns the value a is currently assigned to in the SAT solver + * or null if the value is completely unassigned. + * + * @param a + * + * @return + */ +Node Bitblaster::getVarValue(TNode a) { + if (d_termCache.find(a) == d_termCache.end()) { + Assert(isSharedTerm(a)); + return Node(); + } + Bits bits = d_termCache[a]; Integer value(0); for (int i = bits.size() -1; i >= 0; --i) { SatValue bit_value; if (d_cnfStream->hasLiteral(bits[i])) { SatLiteral bit = d_cnfStream->getLiteral(bits[i]); bit_value = d_satSolver->value(bit); - Assert (bit_value != SAT_VALUE_UNKNOWN); + Assert (bit_value != SAT_VALUE_UNKNOWN); } else { // the bit is unconstrainted so we can give it an arbitrary value bit_value = SAT_VALUE_FALSE; @@ -436,8 +463,12 @@ void Bitblaster::collectModelInfo(TheoryModel* m) { __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin(); for (; it!= d_variables.end(); ++it) { TNode var = *it; - if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { + if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { Node const_value = getVarValue(var); + if(const_value == Node()) { + // if the value is unassigned just set it to zero + const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + } Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " << var << " " << const_value << "))\n"; diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 21b389508..84a67e884 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -124,7 +124,8 @@ class Bitblaster { // division is bitblasted in terms of constraints // so it needs to use private bitblaster interface void bbUdiv(TNode node, Bits& bits); - void bbUrem(TNode node, Bits& bits); + void bbUrem(TNode node, Bits& bits); + bool hasValue(TNode a); public: void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division void bbTerm(TNode node, Bits& bits); @@ -164,9 +165,9 @@ public: } bool isSharedTerm(TNode node); -private: - +private: + class Statistics { public: IntStat d_numTermClauses, d_numAtomClauses; diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp new file mode 100644 index 000000000..499d362a9 --- /dev/null +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -0,0 +1,466 @@ +/********************* */ +/*! \file bv_inequality_graph.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A graph representation of the currently asserted bv inequalities. + ** + ** A graph representation of the currently asserted bv inequalities. + **/ + +#include "theory/bv/bv_inequality_graph.h" +#include "theory/bv/theory_bv_utils.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; + +const TermId CVC4::theory::bv::UndefinedTermId = -1; +const ReasonId CVC4::theory::bv::UndefinedReasonId = -1; +const ReasonId CVC4::theory::bv::AxiomReasonId = -2; + + +bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) { + Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; + + TermId id_a = registerTerm(a); + TermId id_b = registerTerm(b); + ReasonId id_reason = registerReason(reason); + + Assert (!(isConst(id_a) && isConst(id_b))); + BitVector a_val = getValue(id_a); + BitVector b_val = getValue(id_b); + + unsigned bitwidth = utils::getSize(a); + BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u); + + if (a_val + diff < a_val) { + // we have an overflow + std::vector<ReasonId> conflict; + conflict.push_back(id_reason); + computeExplanation(UndefinedTermId, id_a, conflict); + setConflict(conflict); + return false; + } + + if (a_val + diff <= b_val) { + // the inequality is true in the current partial model + // we still add the edge because it may not be true later (cardinality) + addEdge(id_a, id_b, strict, id_reason); + return true; + } + + if (isConst(id_b) && a_val + diff > b_val) { + // we must be in a conflict since a has the minimum value that + // satisifes the constraints + std::vector<ReasonId> conflict; + conflict.push_back(id_reason); + computeExplanation(UndefinedTermId, id_a, conflict); + Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant UB \n"; + setConflict(conflict); + return false; + } + + // add the inequality edge + addEdge(id_a, id_b, strict, id_reason); + BFSQueue queue(&d_modelValues); + Assert (hasModelValue(id_a)); + queue.push(id_a); + return processQueue(queue, id_a); +} + +bool InequalityGraph::updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed) { + BitVector lower_bound = new_mv.value; + + if (isConst(id)) { + if (getValue(id) < lower_bound) { + Debug("bv-inequality") << "Conflict: constant " << getValue(id) << "\n"; + std::vector<ReasonId> conflict; + TermId parent = new_mv.parent; + ReasonId reason = new_mv.reason; + conflict.push_back(reason); + computeExplanation(UndefinedTermId, parent, conflict); + Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant\n"; + setConflict(conflict); + return false; + } + } else { + // if not constant we can try to update the value + if (getValue(id) < lower_bound) { + // if we are updating the term we started with we must be in a cycle + if (id == start) { + TermId parent = new_mv.parent; + ReasonId reason = new_mv.reason; + std::vector<TermId> conflict; + conflict.push_back(reason); + computeExplanation(id, parent, conflict); + Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; + setConflict(conflict); + return false; + } + Debug("bv-inequality-internal") << "Updating " << getTermNode(id) + << " from " << getValue(id) << "\n" + << " to " << lower_bound << "\n"; + changed = true; + setModelValue(id, new_mv); + } + } + return true; +} + +bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) { + while (!queue.empty()) { + TermId current = queue.top(); + queue.pop(); + Debug("bv-inequality-internal") << "InequalityGraph::processQueue proceessing " << getTermNode(current) << "\n"; + + BitVector current_value = getValue(current); + + unsigned size = getBitwidth(current); + const BitVector zero(size, 0u); + const BitVector one(size, 1u); + + const Edges& edges = getEdges(current); + for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) { + TermId next = it->next; + ReasonId reason = it->reason; + + const BitVector increment = it->strict ? one : zero; + const BitVector next_lower_bound = current_value + increment; + + if (next_lower_bound < current_value) { + // it means we have an overflow and hence a conflict + std::vector<TermId> conflict; + conflict.push_back(it->reason); + computeExplanation(start, current, conflict); + Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; + setConflict(conflict); + return false; + } + + ModelValue new_mv(next_lower_bound, current, reason); + bool updated = false; + if (!updateValue(next, new_mv, start, updated)) { + return false; + } + + if (next == start) { + // we know what we didn't update start or we would have had a conflict + // this means we are in a cycle where all the values are forced to be equal + Debug("bv-inequality-internal") << "InequalityGraph::processQueue equal cycle."; + continue; + } + + if (!updated) { + // if we didn't update current we don't need to add to the queue it's children + Debug("bv-inequality-internal") << " unchanged " << getTermNode(next) << "\n"; + continue; + } + + queue.push(next); + Debug("bv-inequality-internal") << " enqueue " << getTermNode(next) << "\n"; + } + } + return true; +} + +void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation) { + if(Debug.isOn("bv-inequality")) { + if (from == UndefinedTermId) { + Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(to) << "\n"; + } else { + Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(from) <<" => " + << getTermNode(to) << "\n"; + } + } + + TermIdSet seen; + + while(hasReason(to) && from != to && !seen.count(to)) { + seen.insert(to); + const ModelValue& exp = getModelValue(to); + Assert (exp.reason != UndefinedReasonId); + explanation.push_back(exp.reason); + Assert (exp.parent != UndefinedTermId); + to = exp.parent; + Debug("bv-inequality-internal") << " parent: " << getTermNode(to) << "\n" + << " reason: " << getReasonNode(exp.reason) << "\n"; + } +} + +void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) { + Debug("bv-inequality-internal") << "InequalityGraph::addEdge " << getTermNode(a) << " => " << getTermNode(b) << "\n" + << " strict ? " << strict << "\n"; + Edges& edges = getEdges(a); + InequalityEdge new_edge(b, strict, reason); + edges.push_back(new_edge); + d_undoStack.push_back(std::make_pair(a, new_edge)); + d_undoStackIndex = d_undoStackIndex + 1; +} + +void InequalityGraph::initializeModelValue(TNode node) { + TermId id = getTermId(node); + Assert (!hasModelValue(id)); + bool isConst = node.getKind() == kind::CONST_BITVECTOR; + unsigned size = utils::getSize(node); + BitVector value = isConst? node.getConst<BitVector>() : BitVector(size, 0u); + setModelValue(id, ModelValue(value, UndefinedTermId, UndefinedReasonId)); +} + +bool InequalityGraph::isRegistered(TNode term) const { + return d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end(); +} + +TermId InequalityGraph::registerTerm(TNode term) { + if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) { + TermId id = d_termNodeToIdMap[term]; + if (!hasModelValue(id)) { + // we could have backtracked and + initializeModelValue(term); + } + return id; + } + + // store in node mapping + TermId id = d_termNodes.size(); + Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << " => id"<< id << "\n"; + + d_termNodes.push_back(term); + d_termNodeToIdMap[term] = id; + + // create InequalityNode + unsigned size = utils::getSize(term); + + bool isConst = term.getKind() == kind::CONST_BITVECTOR; + InequalityNode ineq = InequalityNode(id, size, isConst); + + Assert (d_ineqNodes.size() == id); + d_ineqNodes.push_back(ineq); + + Assert (d_ineqEdges.size() == id); + d_ineqEdges.push_back(Edges()); + + initializeModelValue(term); + + return id; +} + +ReasonId InequalityGraph::registerReason(TNode reason) { + if (d_reasonToIdMap.find(reason) != d_reasonToIdMap.end()) { + return d_reasonToIdMap[reason]; + } + ReasonId id = d_reasonNodes.size(); + d_reasonNodes.push_back(reason); + d_reasonToIdMap[reason] = id; + return id; +} + +TNode InequalityGraph::getReasonNode(ReasonId id) const { + Assert (d_reasonNodes.size() > id); + return d_reasonNodes[id]; +} + +TNode InequalityGraph::getTermNode(TermId id) const { + Assert (d_termNodes.size() > id); + return d_termNodes[id]; +} + +TermId InequalityGraph::getTermId(TNode node) const { + Assert (d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end()); + return d_termNodeToIdMap.find(node)->second; +} + +void InequalityGraph::setConflict(const std::vector<ReasonId>& conflict) { + Assert (!d_inConflict); + d_inConflict = true; + d_conflict.clear(); + for (unsigned i = 0; i < conflict.size(); ++i) { + if (conflict[i] != AxiomReasonId) { + d_conflict.push_back(getReasonNode(conflict[i])); + } + } + if (Debug.isOn("bv-inequality")) { + Debug("bv-inequality") << "InequalityGraph::setConflict \n"; + for (unsigned i = 0; i < d_conflict.size(); ++i) { + Debug("bv-inequality") << " " << d_conflict[i] <<"\n"; + } + } +} + +void InequalityGraph::getConflict(std::vector<TNode>& conflict) { + for (unsigned i = 0; i < d_conflict.size(); ++i) { + conflict.push_back(d_conflict[i]); + } +} + +void InequalityGraph::setModelValue(TermId term, const ModelValue& mv) { + d_modelValues[term] = mv; +} + +InequalityGraph::ModelValue InequalityGraph::getModelValue(TermId term) const { + Assert (d_modelValues.find(term) != d_modelValues.end()); + return (*(d_modelValues.find(term))).second; +} + +bool InequalityGraph::hasModelValue(TermId id) const { + return d_modelValues.find(id) != d_modelValues.end(); +} + +BitVector InequalityGraph::getValue(TermId id) const { + Assert (hasModelValue(id)); + return (*(d_modelValues.find(id))).second.value; +} + +bool InequalityGraph::hasReason(TermId id) const { + const ModelValue& mv = getModelValue(id); + return mv.reason != UndefinedReasonId; +} + +bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) { + Debug("bv-inequality") << "InequalityGraph::addDisequality " << reason << "\n"; + d_disequalities.push_back(reason); + + if (!isRegistered(a) || !isRegistered(b)) { + //splitDisequality(reason); + return true; + } + TermId id_a = getTermId(a); + TermId id_b = getTermId(b); + if (!hasModelValue(id_a)) { + initializeModelValue(a); + } + if (!hasModelValue(id_b)) { + initializeModelValue(b); + } + const BitVector val_a = getValue(id_a); + const BitVector val_b = getValue(id_b); + if (val_a == val_b) { + if (a.getKind() == kind::CONST_BITVECTOR) { + // then we know b cannot be smaller than the assigned value so we try to make it larger + std::vector<ReasonId> explanation_ids; + computeExplanation(UndefinedTermId, id_b, explanation_ids); + std::vector<TNode> explanation_nodes; + explanation_nodes.push_back(reason); + for (unsigned i = 0; i < explanation_ids.size(); ++i) { + explanation_nodes.push_back(getReasonNode(explanation_ids[i])); + } + Node explanation = utils::mkAnd(explanation_nodes); + d_reasonSet.insert(explanation); + return addInequality(a, b, true, explanation); + } + if (b.getKind() == kind::CONST_BITVECTOR) { + // then we know b cannot be smaller than the assigned value so we try to make it larger + std::vector<ReasonId> explanation_ids; + computeExplanation(UndefinedTermId, id_a, explanation_ids); + std::vector<TNode> explanation_nodes; + explanation_nodes.push_back(reason); + for (unsigned i = 0; i < explanation_ids.size(); ++i) { + explanation_nodes.push_back(getReasonNode(explanation_ids[i])); + } + Node explanation = utils::mkAnd(explanation_nodes); + d_reasonSet.insert(explanation); + return addInequality(b, a, true, explanation); + } + // if none of the terms are constants just add the lemma + //splitDisequality(reason); + } else { + Debug("bv-inequality-internal") << "Disequal: " << a << " => " << val_a.toString(10) << "\n" + << " " << b << " => " << val_b.toString(10) << "\n"; + } + return true; +} + +// void InequalityGraph::splitDisequality(TNode diseq) { +// Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << diseq <<"\n"; +// Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL); +// if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) { +// d_disequalitiesToSplit.push_back(diseq); +// } +// } + +void InequalityGraph::backtrack() { + Debug("bv-inequality-internal") << "InequalityGraph::backtrack()\n"; + int size = d_undoStack.size(); + for (int i = size - 1; i >= (int)d_undoStackIndex.get(); --i) { + Assert (!d_undoStack.empty()); + TermId id = d_undoStack.back().first; + InequalityEdge edge = d_undoStack.back().second; + d_undoStack.pop_back(); + + Debug("bv-inequality-internal") << " remove edge " << getTermNode(id) << " => " + << getTermNode(edge.next) <<"\n"; + Edges& edges = getEdges(id); + for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) { + Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n"; + } + Assert (!edges.empty()); + Assert (edges.back() == edge); + edges.pop_back(); + } +} + +Node InequalityGraph::makeDiseqSplitLemma(TNode diseq) { + Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL); + TNode a = diseq[0][0]; + TNode b = diseq[0][1]; + Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b); + Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); + Node eq = diseq[0]; + Node lemma = utils::mkNode(kind::OR, a_lt_b, b_lt_a, eq); + return lemma; +} + +void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) { + for (CDQueue<TNode>::const_iterator it = d_disequalities.begin(); it != d_disequalities.end(); ++it) { + if (d_disequalitiesAlreadySplit.find(*it) == d_disequalitiesAlreadySplit.end()) { + // if we haven't already split on this disequality + TNode diseq = *it; + TermId a_id = registerTerm(diseq[0][0]); + TermId b_id = registerTerm(diseq[0][1]); + if (getValue(a_id) == getValue(b_id)) { + lemmas.push_back(makeDiseqSplitLemma(diseq)); + d_disequalitiesAlreadySplit.insert(diseq); + } + } + } +} + +bool InequalityGraph::isLessThan(TNode a, TNode b) { + Assert (isRegistered(a) && isRegistered(b)); + Unimplemented(); +} + +bool InequalityGraph::hasValueInModel(TNode node) const { + if (isRegistered(node)) { + TermId id = getTermId(node); + return hasModelValue(id); + } + return false; +} + +BitVector InequalityGraph::getValueInModel(TNode node) const { + TermId id = getTermId(node); + Assert (hasModelValue(id)); + return getValue(id); +} + +void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) { + for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + TermId id = (*it).first; + BitVector value = (*it).second.value; + TNode var = getTermNode(id); + Node constant = utils::mkConst(value); + Node assignment = utils::mkNode(kind::EQUAL, var, constant); + assignments.push_back(assignment); + Debug("bitvector-model") << " " << var <<" => " << constant << "\n"; + } +} diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h new file mode 100644 index 000000000..d402b1561 --- /dev/null +++ b/src/theory/bv/bv_inequality_graph.h @@ -0,0 +1,290 @@ +/********************* */ +/*! \file bv_inequality_graph.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Algebraic solver. + ** + ** Algebraic solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H +#define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H + +#include "context/context.h" +#include "context/cdqueue.h" +#include "theory/uf/equality_engine.h" +#include "theory/theory.h" +#include <queue> +#include <list> +namespace CVC4 { +namespace theory { + + +namespace bv { + +typedef unsigned TermId; +typedef unsigned ReasonId; +extern const TermId UndefinedTermId; +extern const ReasonId UndefinedReasonId; +extern const ReasonId AxiomReasonId; + +class InequalityGraph : public context::ContextNotifyObj{ + + + context::Context* d_context; + + struct InequalityEdge { + TermId next; + ReasonId reason; + bool strict; + InequalityEdge(TermId n, bool s, ReasonId r) + : next(n), + reason(r), + strict(s) + {} + bool operator==(const InequalityEdge& other) const { + return next == other.next && reason == other.reason && strict == other.strict; + } + }; + + class InequalityNode { + TermId d_id; + unsigned d_bitwidth; + bool d_isConstant; + public: + InequalityNode(TermId id, unsigned bitwidth, bool isConst) + : d_id(id), + d_bitwidth(bitwidth), + d_isConstant(isConst) + {} + TermId getId() const { return d_id; } + unsigned getBitwidth() const { return d_bitwidth; } + bool isConstant() const { return d_isConstant; } + }; + + struct ModelValue { + TermId parent; + ReasonId reason; + BitVector value; + ModelValue() + : parent(UndefinedTermId), + reason(UndefinedReasonId), + value(0, 0u) + {} + + ModelValue(const BitVector& val, TermId p, ReasonId r) + : parent(p), + reason(r), + value(val) + {} + }; + + typedef context::CDHashMap<TermId, ModelValue> ModelValues; + + struct QueueComparator { + const ModelValues* d_model; + QueueComparator(const ModelValues* model) + : d_model(model) + {} + bool operator() (TermId left, TermId right) const { + Assert (d_model->find(left) != d_model->end() && + d_model->find(right) != d_model->end()); + + return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value; + } + }; + + typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; + typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; + + typedef std::vector<InequalityEdge> Edges; + typedef __gnu_cxx::hash_set<TermId> TermIdSet; + + typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + + std::vector<InequalityNode> d_ineqNodes; + std::vector< Edges > d_ineqEdges; + + // to keep the explanation nodes alive + NodeSet d_reasonSet; + std::vector<TNode> d_reasonNodes; + ReasonToIdMap d_reasonToIdMap; + + std::vector<Node> d_termNodes; + TermNodeToIdMap d_termNodeToIdMap; + + context::CDO<bool> d_inConflict; + std::vector<TNode> d_conflict; + bool d_signed; + + ModelValues d_modelValues; + void initializeModelValue(TNode node); + void setModelValue(TermId term, const ModelValue& mv); + ModelValue getModelValue(TermId term) const; + bool hasModelValue(TermId id) const; + bool hasReason(TermId id) const; + + /** + * Registers the term by creating its corresponding InequalityNode + * and adding the min <= term <= max default edges. + * + * @param term + * + * @return + */ + TermId registerTerm(TNode term); + TNode getTermNode(TermId id) const; + TermId getTermId(TNode node) const; + bool isRegistered(TNode term) const; + + ReasonId registerReason(TNode reason); + TNode getReasonNode(ReasonId id) const; + + + Edges& getEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; } + InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; } + const InequalityNode& getInequalityNode(TermId id) const { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; } + unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); } + bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); } + + BitVector getValue(TermId id) const; + + void addEdge(TermId a, TermId b, bool strict, TermId reason); + + void setConflict(const std::vector<ReasonId>& conflict); + /** + * If necessary update the value in the model of the current queue element. + * + * @param id current queue element we are updating + * @param start node we started with, to detect cycles + * + * @return + */ + bool updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed); + /** + * Update the current model starting with the start term. + * + * @param queue + * @param start + * + * @return + */ + bool processQueue(BFSQueue& queue, TermId start); + /** + * Return the reasons why from <= to. If from is undefined we just + * explain the current value of to. + * + * @param from + * @param to + * @param explanation + */ + void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation); + // void splitDisequality(TNode diseq); + + /** + Disequality reasoning + */ + + /*** The currently asserted disequalities */ + context::CDQueue<TNode> d_disequalities; + NodeSet d_disequalitiesAlreadySplit; + Node makeDiseqSplitLemma(TNode diseq); + /** Backtracking mechanisms **/ + std::vector<std::pair<TermId, InequalityEdge> > d_undoStack; + context::CDO<unsigned> d_undoStackIndex; + + void contextNotifyPop() { + backtrack(); + } + + void backtrack(); + +public: + + InequalityGraph(context::Context* c, bool s = false) + : ContextNotifyObj(c), + d_context(c), + d_ineqNodes(), + d_ineqEdges(), + d_inConflict(c, false), + d_conflict(), + d_signed(s), + d_modelValues(c), + d_disequalities(c), + d_disequalitiesAlreadySplit(), + d_undoStack(), + d_undoStackIndex(c) + {} + /** + * Add a new inequality to the graph + * + * @param a + * @param b + * @param strict + * @param reason + * + * @return + */ + bool addInequality(TNode a, TNode b, bool strict, TNode reason); + /** + * Add a new disequality to the graph. This may lead in a lemma. + * + * @param a + * @param b + * @param reason + * + * @return + */ + bool addDisequality(TNode a, TNode b, TNode reason); + void getConflict(std::vector<TNode>& conflict); + virtual ~InequalityGraph() throw(AssertionException) {} + /** + * Check that the currently asserted disequalities that have not been split on + * are still true in the current model. + */ + void checkDisequalities(std::vector<Node>& lemmas); + /** + * Return true if a < b is entailed by the current set of assertions. + * + * @param a + * @param b + * + * @return + */ + bool isLessThan(TNode a, TNode b); + /** + * Returns true if the term has a value in the model (i.e. if we have seen it) + * + * @param a + * + * @return + */ + bool hasValueInModel(TNode a) const; + /** + * Return the value of a in the current model. + * + * @param a + * + * @return + */ + BitVector getValueInModel(TNode a) const; + + void getAllValuesInModel(std::vector<Node>& assignments); +}; + +} +} +} + +#endif /* __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */ diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 4dbba0797..ed90e0ebe 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -32,8 +32,9 @@ class TheoryModel; namespace bv { enum SubTheory { - SUB_EQUALITY = 1, - SUB_BITBLAST = 2 + SUB_CORE = 1, + SUB_BITBLAST = 2, + SUB_INEQUALITY = 3 }; inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { @@ -41,9 +42,11 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { case SUB_BITBLAST: out << "BITBLASTER"; break; - case SUB_EQUALITY: - out << "EQUALITY"; + case SUB_CORE: + out << "BV_CORE_SUBTHEORY"; break; + case SUB_INEQUALITY: + out << "BV_INEQUALITY_SUBTHEORY"; default: Unreachable(); break; @@ -58,6 +61,7 @@ const bool d_useSatPropagation = true; // forward declaration class TheoryBV; +typedef context::CDQueue<Node> AssertionQueue; /** * Abstract base class for bit-vector subtheory solvers * @@ -71,19 +75,34 @@ protected: /** The bit-vector theory */ TheoryBV* d_bv; - + AssertionQueue d_assertionQueue; + context::CDO<uint32_t> d_assertionIndex; public: SubtheorySolver(context::Context* c, TheoryBV* bv) : d_context(c), - d_bv(bv) + d_bv(bv), + d_assertionQueue(c), + d_assertionIndex(c, 0) {} virtual ~SubtheorySolver() {} - - virtual bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) = 0; - virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0; - virtual void preRegister(TNode node) {} - virtual void collectModelInfo(TheoryModel* m) = 0; + virtual bool check(Theory::Effort e) = 0; + virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0; + virtual void preRegister(TNode node) {} + virtual void propagate(Theory::Effort e) {} + virtual void collectModelInfo(TheoryModel* m) = 0; + virtual Node getModelValue(TNode var) = 0; + virtual bool isComplete() = 0; + virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0; + virtual void addSharedTerm(TNode node) {} + bool done() { return d_assertionQueue.size() == d_assertionIndex; } + TNode get() { + Assert (!done()); + TNode res = d_assertionQueue[d_assertionIndex]; + d_assertionIndex = d_assertionIndex + 1; + return res; + } + virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } }; } diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index f48a03975..30eaaa764 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -30,13 +30,23 @@ using namespace CVC4::theory::bv::utils; BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), d_bitblaster(new Bitblaster(c, bv)), - d_bitblastQueue(c) + d_bitblastQueue(c), + d_statistics() {} BitblastSolver::~BitblastSolver() { delete d_bitblaster; } +BitblastSolver::Statistics::Statistics() + : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0) +{ + StatisticsRegistry::registerStat(&d_numCallstoCheck); +} +BitblastSolver::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_numCallstoCheck); +} + void BitblastSolver::preRegister(TNode node) { if ((node.getKind() == kind::EQUAL || node.getKind() == kind::BITVECTOR_ULT || @@ -52,22 +62,23 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) { d_bitblaster->explain(literal, assumptions); } -bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) { - Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl; +bool BitblastSolver::check(Theory::Effort e) { + Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; + ++(d_statistics.d_numCallstoCheck); //// Eager bit-blasting if (options::bitvectorEagerBitblast()) { - for (unsigned i = 0; i < assertions.size(); ++i) { - TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i]; + while (!done()) { + TNode assertion = get(); + TNode atom = assertion.getKind() == kind::NOT ? assertion[0] : assertion; if (atom.getKind() != kind::BITVECTOR_BITOF) { d_bitblaster->bbAtom(atom); } + return true; } - return true; } //// Lazy bit-blasting - // bit-blast enqueued nodes while (!d_bitblastQueue.empty()) { TNode atom = d_bitblastQueue.front(); @@ -75,10 +86,11 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory: d_bitblastQueue.pop(); } - // propagation - for (unsigned i = 0; i < assertions.size(); ++i) { - TNode fact = assertions[i]; - if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_BITBLAST)) { + // Processing assertions + while (!done()) { + TNode fact = get(); + Debug("bv-bitblast") << " fact " << fact << ")\n"; + if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) { // Some atoms have not been bit-blasted yet d_bitblaster->bbAtom(fact); // Assert to sat @@ -103,7 +115,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory: } } - // solving + // Solving if (e == Theory::EFFORT_FULL || options::bitvectorEagerFullcheck()) { Assert(!d_bv->inConflict()); Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n"; @@ -129,5 +141,7 @@ void BitblastSolver::collectModelInfo(TheoryModel* m) { } Node BitblastSolver::getModelValue(TNode node) { - return d_bitblaster->getVarValue(node); + Node val = d_bitblaster->getVarValue(node); + Assert (val != Node() || d_bv->isSharedTerm(node)); + return val; } diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 510006710..b6be84df5 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -30,23 +30,28 @@ class Bitblaster; * BitblastSolver */ class BitblastSolver : public SubtheorySolver { - + struct Statistics { + IntStat d_numCallstoCheck; + Statistics(); + ~Statistics(); + }; /** Bitblaster */ Bitblaster* d_bitblaster; /** Nodes that still need to be bit-blasted */ context::CDQueue<TNode> d_bitblastQueue; - + Statistics d_statistics; public: BitblastSolver(context::Context* c, TheoryBV* bv); ~BitblastSolver(); void preRegister(TNode node); - bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e); + bool check(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); EqualityStatus getEqualityStatus(TNode a, TNode b); - void collectModelInfo(TheoryModel* m); + void collectModelInfo(TheoryModel* m); Node getModelValue(TNode node); + bool isComplete() { return true; } }; } diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp new file mode 100644 index 000000000..f8c26c35a --- /dev/null +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -0,0 +1,401 @@ +/********************* */ +/*! \file bv_subtheory_eq.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): lianah + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Algebraic solver. + ** + ** Algebraic solver. + **/ + +#include "theory/bv/bv_subtheory_core.h" + +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/bv/slicer.h" +#include "theory/model.h" +#include "theory/bv/options.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; + +CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) + : SubtheorySolver(c, bv), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), + d_slicer(new Slicer()), + d_isCoreTheory(c, true), + d_reasons(c) +{ + if (d_useEqualityEngine) { + + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); + } +} + +CoreSolver::~CoreSolver() { + delete d_slicer; +} +void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + +void CoreSolver::preRegister(TNode node) { + if (!d_useEqualityEngine) + return; + + if (node.getKind() == kind::EQUAL) { + d_equalityEngine.addTriggerEquality(node); + if (options::bitvectorCoreSolver()) { + d_slicer->processEquality(node); + } + } else { + d_equalityEngine.addTerm(node); + } +} + + +void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) { + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + if (atom.getKind() == kind::EQUAL) { + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + } else { + d_equalityEngine.explainPredicate(atom, polarity, assumptions); + } +} + +Node CoreSolver::getBaseDecomposition(TNode a) { + std::vector<Node> a_decomp; + d_slicer->getBaseDecomposition(a, a_decomp); + Node new_a = utils::mkConcat(a_decomp); + Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n"; + return new_a; +} + +bool CoreSolver::decomposeFact(TNode fact) { + Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl; + // assert decompositions since the equality engine does not know the semantics of + // concat: + // a == a_1 concat ... concat a_k + // b == b_1 concat ... concat b_k + Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl; + // FIXME: are this the right things to assert? + // assert decompositions since the equality engine does not know the semantics of + // concat: + // a == a_1 concat ... concat a_k + // b == b_1 concat ... concat b_k + TNode eq = fact.getKind() == kind::NOT? fact[0] : fact; + + TNode a = eq[0]; + TNode b = eq[1]; + Node new_a = getBaseDecomposition(a); + Node new_b = getBaseDecomposition(b); + + Assert (utils::getSize(new_a) == utils::getSize(new_b) && + utils::getSize(new_a) == utils::getSize(a)); + + NodeManager* nm = NodeManager::currentNM(); + Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a); + Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b); + + bool ok = true; + ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue()); + if (!ok) return false; + ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue()); + if (!ok) return false; + ok = assertFactToEqualityEngine(fact, fact); + if (!ok) return false; + + if (fact.getKind() == kind::EQUAL) { + // assert the individual equalities as well + // a_i == b_i + if (new_a.getKind() == kind::BITVECTOR_CONCAT && + new_b.getKind() == kind::BITVECTOR_CONCAT) { + + Assert (new_a.getNumChildren() == new_b.getNumChildren()); + for (unsigned i = 0; i < new_a.getNumChildren(); ++i) { + Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]); + ok = assertFactToEqualityEngine(eq_i, fact); + if (!ok) return false; + } + } + } + return true; +} + +bool CoreSolver::check(Theory::Effort e) { + Trace("bitvector::core") << "CoreSolver::check \n"; + Assert (!d_bv->inConflict()); + ++(d_statistics.d_numCallstoCheck); + bool ok = true; + std::vector<Node> core_eqs; + while (! done()) { + TNode fact = get(); + + // update whether we are in the core fragment + if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) { + d_isCoreTheory = false; + } + + // only reason about equalities + if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) { + if (options::bitvectorCoreSolver()) { + ok = decomposeFact(fact); + } else { + ok = assertFactToEqualityEngine(fact, fact); + } + } else { + ok = assertFactToEqualityEngine(fact, fact); + } + if (!ok) + return false; + } + + if (Theory::fullEffort(e) && isComplete()) { + buildModel(); + } + + return true; +} + +void CoreSolver::buildModel() { + if (options::bitvectorCoreSolver()) { + // FIXME + return; + } + Debug("bv-core") << "CoreSolver::buildModel() \n"; + d_modelValues.clear(); + TNodeSet constants; + TNodeSet constants_in_eq_engine; + // collect constants in equality engine + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); + while (!eqcs_i.isFinished()) { + TNode repr = *eqcs_i; + if (repr.getKind() == kind::CONST_BITVECTOR) { + // must check if it's just the constant + eq::EqClassIterator it(repr, &d_equalityEngine); + if (!(++it).isFinished() || true) { + constants.insert(repr); + constants_in_eq_engine.insert(repr); + } + } + ++eqcs_i; + } + // build repr to value map + + eqcs_i = eq::EqClassesIterator(&d_equalityEngine); + while (!eqcs_i.isFinished()) { + TNode repr = *eqcs_i; + ++eqcs_i; + TypeNode type = repr.getType(); + if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) { + Debug("bv-core-model") << " processing " << repr <<"\n"; + // we need to assign a value for it + TypeEnumerator te(type); + Node val; + do { + val = *te; + ++te; + // Debug("bv-core-model") << " trying value " << val << "\n"; + // Debug("bv-core-model") << " is in set? " << constants.count(val) << "\n"; + // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n"; + } while (constants.count(val) != 0 && !(te.isFinished())); + + if (te.isFinished() && constants.count(val) != 0) { + // if we cannot enumerate anymore values we just return the lemma stating that + // at least two of the representatives are equal. + std::vector<TNode> representatives; + representatives.push_back(repr); + + for (TNodeSet::const_iterator it = constants_in_eq_engine.begin(); + it != constants_in_eq_engine.end(); ++it) { + TNode constant = *it; + if (utils::getSize(constant) == utils::getSize(repr)) { + representatives.push_back(constant); + } + } + for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + representatives.push_back(it->first); + } + std::vector<Node> equalities; + for (unsigned i = 0; i < representatives.size(); ++i) { + for (unsigned j = i + 1; j < representatives.size(); ++j) { + TNode a = representatives[i]; + TNode b = representatives[j]; + if (utils::getSize(a) == utils::getSize(b)) { + equalities.push_back(utils::mkNode(kind::EQUAL, a, b)); + } + } + } + Node lemma = utils::mkOr(equalities); + d_bv->lemma(lemma); + Debug("bv-core") << " lemma: " << lemma << "\n"; + return; + } + Debug("bv-core-model") << " " << repr << " => " << val <<"\n" ; + constants.insert(val); + d_modelValues[repr] = val; + } + } +} + +bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { + // Notify the equality engine + if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) { + Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl; + // Debug("bv-slicer-eq") << " reason=" << reason << endl; + bool negated = fact.getKind() == kind::NOT; + TNode predicate = negated ? fact[0] : fact; + if (predicate.getKind() == kind::EQUAL) { + if (negated) { + // dis-equality + d_equalityEngine.assertEquality(predicate, false, reason); + } else { + // equality + d_equalityEngine.assertEquality(predicate, true, reason); + } + } else { + // Adding predicate if the congruence over it is turned on + if (d_equalityEngine.isFunctionKind(predicate.getKind())) { + d_equalityEngine.assertPredicate(predicate, !negated, reason); + } + } + } + + // checking for a conflict + if (d_bv->inConflict()) { + return false; + } + return true; +} + +bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_solver.storePropagation(equality); + } else { + return d_solver.storePropagation(equality.notNode()); + } +} + +bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { + Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl; + if (value) { + return d_solver.storePropagation(predicate); + } else { + return d_solver.storePropagation(predicate.notNode()); + } +} + +bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + if (value) { + return d_solver.storePropagation(t1.eqNode(t2)); + } else { + return d_solver.storePropagation(t1.eqNode(t2).notNode()); + } +} + +void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { + d_solver.conflict(t1, t2); +} + +bool CoreSolver::storePropagation(TNode literal) { + return d_bv->storePropagation(literal, SUB_CORE); +} + +void CoreSolver::conflict(TNode a, TNode b) { + std::vector<TNode> assumptions; + d_equalityEngine.explainEquality(a, b, true, assumptions); + Node conflict = flattenAnd(assumptions); + d_bv->setConflict(conflict); +} + +void CoreSolver::collectModelInfo(TheoryModel* m) { + if (options::bitvectorCoreSolver()) { + Unreachable(); + return; + } + if (Debug.isOn("bitvector-model")) { + context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin(); + for (; it!= d_assertionQueue.end(); ++it) { + Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert " + << *it << ")\n"; + } + } + set<Node> termSet; + d_bv->computeRelevantTerms(termSet); + m->assertEqualityEngine(&d_equalityEngine, &termSet); + if (isComplete()) { + Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; + for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + Node a = it->first; + Node b = it->second; + m->assertEquality(a, b, true); + } + } +} + +Node CoreSolver::getModelValue(TNode var) { + Assert (isComplete()); + TNode repr = d_equalityEngine.getRepresentative(var); + if (repr.getKind() == kind::CONST_BITVECTOR) { + return repr; + } + if (d_modelValues.find(repr) == d_modelValues.end()) { + // it may be a shared term that never gets asserted + Assert(d_bv->isSharedTerm(var)); + return Node(); + } + return d_modelValues[repr]; +} + +CoreSolver::Statistics::Statistics() + : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0) +{ + StatisticsRegistry::registerStat(&d_numCallstoCheck); +} +CoreSolver::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_numCallstoCheck); +} diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_core.h index 2b024cfd4..d314b2fbf 100644 --- a/src/theory/bv/bv_subtheory_eq.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -18,23 +18,34 @@ #include "cvc4_private.h" #include "theory/bv/bv_subtheory.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" namespace CVC4 { namespace theory { namespace bv { +class Slicer; +class Base; /** * Bitvector equality solver */ -class EqualitySolver : public SubtheorySolver { +class CoreSolver : public SubtheorySolver { + typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + struct Statistics { + IntStat d_numCallstoCheck; + Statistics(); + ~Statistics(); + }; + // NotifyClass: handles call-back from congruence closure module - class NotifyClass : public eq::EqualityEngineNotify { - EqualitySolver& d_solver; + CoreSolver& d_solver; public: - NotifyClass(EqualitySolver& solver): d_solver(solver) {} + NotifyClass(CoreSolver& solver): d_solver(solver) {} bool eqNotifyTriggerEquality(TNode equality, bool value); bool eqNotifyTriggerPredicate(TNode predicate, bool value); bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); @@ -43,12 +54,12 @@ class EqualitySolver : public SubtheorySolver { void eqNotifyPreMerge(TNode t1, TNode t2) { } void eqNotifyPostMerge(TNode t1, TNode t2) { } void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } -}; + }; /** The notify class for d_equalityEngine */ NotifyClass d_notify; - + /** Equality engine */ eq::EqualityEngine d_equalityEngine; @@ -58,16 +69,26 @@ class EqualitySolver : public SubtheorySolver { /** Store a conflict from merging two constants */ void conflict(TNode a, TNode b); - /** FIXME: for debugging purposes only */ - context::CDList<TNode> d_assertions; -public: - - EqualitySolver(context::Context* c, TheoryBV* bv); - void setMasterEqualityEngine(eq::EqualityEngine* eq); + Slicer* d_slicer; + context::CDO<bool> d_isCoreTheory; + /** To make sure we keep the explanations */ + context::CDHashSet<Node, NodeHashFunction> d_reasons; + ModelValue d_modelValues; + void buildModel(); + bool assertFactToEqualityEngine(TNode fact, TNode reason); + bool decomposeFact(TNode fact); + Node getBaseDecomposition(TNode a); + Statistics d_statistics; +public: + CoreSolver(context::Context* c, TheoryBV* bv); + ~CoreSolver(); + bool isComplete() { return d_isCoreTheory; } + void setMasterEqualityEngine(eq::EqualityEngine* eq); void preRegister(TNode node); - bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e); + bool check(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); void collectModelInfo(TheoryModel* m); + Node getModelValue(TNode var); void addSharedTerm(TNode t) { d_equalityEngine.addTriggerTerm(t, THEORY_BV); } @@ -82,6 +103,8 @@ public: } return EQUALITY_UNKNOWN; } + bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); } + void addTermToEqualityEngine(TNode node) { d_equalityEngine.addTerm(node); } }; diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp deleted file mode 100644 index 385c2e555..000000000 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ /dev/null @@ -1,185 +0,0 @@ -/********************* */ -/*! \file bv_subtheory_eq.cpp - ** \verbatim - ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): lianah - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Algebraic solver. - ** - ** Algebraic solver. - **/ - -#include "theory/bv/bv_subtheory_eq.h" -#include "theory/bv/theory_bv.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/model.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; -using namespace CVC4::theory::bv::utils; - -EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv) - : SubtheorySolver(c, bv), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), - d_assertions(c) -{ - if (d_useEqualityEngine) { - - // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); - } -} - -void EqualitySolver::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_equalityEngine.setMasterEqualityEngine(eq); -} - -void EqualitySolver::preRegister(TNode node) { - if (!d_useEqualityEngine) - return; - - if (node.getKind() == kind::EQUAL) { - d_equalityEngine.addTriggerEquality(node); - } else { - d_equalityEngine.addTerm(node); - } -} - -void EqualitySolver::explain(TNode literal, std::vector<TNode>& assumptions) { - bool polarity = literal.getKind() != kind::NOT; - TNode atom = polarity ? literal : literal[0]; - if (atom.getKind() == kind::EQUAL) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); - } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions); - } -} - -bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) { - Trace("bitvector::equality") << "EqualitySolver::addAssertions \n"; - Assert (!d_bv->inConflict()); - - for (unsigned i = 0; i < assertions.size(); ++i) { - TNode fact = assertions[i]; - - // Notify the equality engine - if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_EQUALITY) ) { - Trace("bitvector::equality") << " (assert " << fact << ")\n"; - d_assertions.push_back(fact); - bool negated = fact.getKind() == kind::NOT; - TNode predicate = negated ? fact[0] : fact; - if (predicate.getKind() == kind::EQUAL) { - if (negated) { - // dis-equality - d_equalityEngine.assertEquality(predicate, false, fact); - } else { - // equality - d_equalityEngine.assertEquality(predicate, true, fact); - } - } else { - // Adding predicate if the congruence over it is turned on - if (d_equalityEngine.isFunctionKind(predicate.getKind())) { - d_equalityEngine.assertPredicate(predicate, !negated, fact); - } - } - } - - // checking for a conflict - if (d_bv->inConflict()) { - return false; - } - } - - return true; -} - -bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; - if (value) { - return d_solver.storePropagation(equality); - } else { - return d_solver.storePropagation(equality.notNode()); - } -} - -bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl; - if (value) { - return d_solver.storePropagation(predicate); - } else { - return d_solver.storePropagation(predicate.notNode()); - } -} - -bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl; - if (value) { - return d_solver.storePropagation(t1.eqNode(t2)); - } else { - return d_solver.storePropagation(t1.eqNode(t2).notNode()); - } -} - -void EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { - d_solver.conflict(t1, t2); -} - -bool EqualitySolver::storePropagation(TNode literal) { - return d_bv->storePropagation(literal, SUB_EQUALITY); -} - -void EqualitySolver::conflict(TNode a, TNode b) { - std::vector<TNode> assumptions; - d_equalityEngine.explainEquality(a, b, true, assumptions); - d_bv->setConflict(mkAnd(assumptions)); -} - -void EqualitySolver::collectModelInfo(TheoryModel* m) { - if (Debug.isOn("bitvector-model")) { - context::CDList<TNode>::const_iterator it = d_assertions.begin(); - for (; it!= d_assertions.end(); ++it) { - Debug("bitvector-model") << "EqualitySolver::collectModelInfo (assert " - << *it << ")\n"; - } - } - set<Node> termSet; - d_bv->computeRelevantTerms(termSet); - m->assertEqualityEngine(&d_equalityEngine, &termSet); -} diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp new file mode 100644 index 000000000..17ac8a2e5 --- /dev/null +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -0,0 +1,198 @@ +/********************* */ +/*! \file bv_subtheory_inequality.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Algebraic solver. + ** + ** Algebraic solver. + **/ + +#include "theory/bv/bv_subtheory_inequality.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; + +bool InequalitySolver::check(Theory::Effort e) { + Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; + ++(d_statistics.d_numCallstoCheck); + + bool ok = true; + while (!done() && ok) { + TNode fact = get(); + Debug("bv-subtheory-inequality") << " "<< fact <<"\n"; + if (fact.getKind() == kind::EQUAL) { + TNode a = fact[0]; + TNode b = fact[1]; + ok = d_inequalityGraph.addInequality(a, b, false, fact); + if (ok) + ok = d_inequalityGraph.addInequality(b, a, false, fact); + } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) { + TNode a = fact[0][0]; + TNode b = fact[0][1]; + ok = d_inequalityGraph.addDisequality(a, b, fact); + } + if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) { + TNode a = fact[0][1]; + TNode b = fact[0][0]; + ok = d_inequalityGraph.addInequality(a, b, true, fact); + // propagate + // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) { + // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); + // d_bv->storePropagation(neq, SUB_INEQUALITY); + // d_explanations[neq] = fact; + // } + } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) { + TNode a = fact[0][1]; + TNode b = fact[0][0]; + ok = d_inequalityGraph.addInequality(a, b, false, fact); + } else if (fact.getKind() == kind::BITVECTOR_ULT) { + TNode a = fact[0]; + TNode b = fact[1]; + ok = d_inequalityGraph.addInequality(a, b, true, fact); + // propagate + // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) { + // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); + // d_bv->storePropagation(neq, SUB_INEQUALITY); + // d_explanations[neq] = fact; + // } + } else if (fact.getKind() == kind::BITVECTOR_ULE) { + TNode a = fact[0]; + TNode b = fact[1]; + ok = d_inequalityGraph.addInequality(a, b, false, fact); + } + } + + if (!ok) { + std::vector<TNode> conflict; + d_inequalityGraph.getConflict(conflict); + d_bv->setConflict(utils::flattenAnd(conflict)); + return false; + } + + if (isComplete() && Theory::fullEffort(e)) { + // make sure all the disequalities we didn't split on are still satisifed + // and split on the ones that are not + std::vector<Node> lemmas; + d_inequalityGraph.checkDisequalities(lemmas); + for(unsigned i = 0; i < lemmas.size(); ++i) { + d_bv->lemma(lemmas[i]); + } + } + return true; +} + +EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) { + Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b); + Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); + + // if an inequality containing the terms has been asserted then we know + // the equality is false + if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a)) { + return EQUALITY_FALSE; + } + + if (!d_inequalityGraph.hasValueInModel(a) || + !d_inequalityGraph.hasValueInModel(b)) { + return EQUALITY_UNKNOWN; + } + + // TODO: check if this disequality is entailed by inequalities via transitivity + + BitVector a_val = d_inequalityGraph.getValueInModel(a); + BitVector b_val = d_inequalityGraph.getValueInModel(b); + + if (a_val == b_val) { + return EQUALITY_TRUE_IN_MODEL; + } else { + return EQUALITY_FALSE_IN_MODEL; + } +} + +void InequalitySolver::assertFact(TNode fact) { + d_assertionQueue.push_back(fact); + d_assertionSet.insert(fact); + if (!isInequalityOnly(fact)) { + d_isComplete = false; + } +} + +bool InequalitySolver::isInequalityOnly(TNode node) { + if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) { + return d_ineqTermCache[node]; + } + + if (node.getKind() == kind::NOT) { + node = node[0]; + } + + if (node.getKind() != kind::EQUAL && + node.getKind() != kind::BITVECTOR_ULT && + node.getKind() != kind::BITVECTOR_ULE && + node.getKind() != kind::CONST_BITVECTOR && + node.getKind() != kind::SELECT && + node.getKind() != kind::STORE && + node.getMetaKind() != kind::metakind::VARIABLE) { + return false; + } + bool res = true; + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + res = res && isInequalityOnly(node[i]); + } + d_ineqTermCache[node] = res; + return res; +} + +void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) { + Assert (d_explanations.find(literal) != d_explanations.end()); + TNode explanation = d_explanations[literal]; + assumptions.push_back(explanation); + Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n"; +} + +void InequalitySolver::propagate(Theory::Effort e) { + Assert (false); +} + +void InequalitySolver::collectModelInfo(TheoryModel* m) { + Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; + std::vector<Node> model; + d_inequalityGraph.getAllValuesInModel(model); + for (unsigned i = 0; i < model.size(); ++i) { + Assert (model[i].getKind() == kind::EQUAL); + m->assertEquality(model[i][0], model[i][1], true); + } +} + +Node InequalitySolver::getModelValue(TNode var) { + Assert (isComplete()); + if (!d_inequalityGraph.hasValueInModel(var)) { + Assert (d_bv->isSharedTerm(var)); + return Node(); + } + BitVector val = d_inequalityGraph.getValueInModel(var); + return utils::mkConst(val); +} + +InequalitySolver::Statistics::Statistics() + : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0) +{ + StatisticsRegistry::registerStat(&d_numCallstoCheck); +} +InequalitySolver::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_numCallstoCheck); +} + diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h new file mode 100644 index 000000000..b02233b74 --- /dev/null +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -0,0 +1,69 @@ +/********************* */ +/*! \file bv_subtheory_inequality.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Algebraic solver. + ** + ** Algebraic solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H +#define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H + +#include "theory/bv/bv_subtheory.h" +#include "theory/bv/bv_inequality_graph.h" +#include "context/cdhashset.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +class InequalitySolver: public SubtheorySolver { + struct Statistics { + IntStat d_numCallstoCheck; + Statistics(); + ~Statistics(); + }; + + context::CDHashSet<Node, NodeHashFunction> d_assertionSet; + InequalityGraph d_inequalityGraph; + context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; + context::CDO<bool> d_isComplete; + __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache; + bool isInequalityOnly(TNode node); + Statistics d_statistics; +public: + InequalitySolver(context::Context* c, TheoryBV* bv) + : SubtheorySolver(c, bv), + d_assertionSet(c), + d_inequalityGraph(c), + d_explanations(c), + d_isComplete(c, true), + d_ineqTermCache(), + d_statistics() + {} + + bool check(Theory::Effort e); + void propagate(Theory::Effort e); + void explain(TNode literal, std::vector<TNode>& assumptions); + bool isComplete() { return d_isComplete; } + void collectModelInfo(TheoryModel* m); + Node getModelValue(TNode var); + EqualityStatus getEqualityStatus(TNode a, TNode b); + void assertFact(TNode fact); +}; + +} +} +} + +#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 2faa12437..052e477ea 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -8,7 +8,7 @@ theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h" typechecker "theory/bv/theory_bv_type_rules.h" properties finite -properties check propagate +properties check propagate presolve rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" diff --git a/src/theory/bv/options b/src/theory/bv/options index 72db63c09..cdc02c9ad 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -14,4 +14,10 @@ option bitvectorShareLemmas --bitblast-share-lemmas bool option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool check the bitblasting eagerly +option bitvectorInequalitySolver --bv-inequality-solver bool + turn on the inequality solver for the bit-vector theory + +option bitvectorCoreSolver --bv-core-solver bool + turn on the core solver for the bit-vector theory + endmodule diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp new file mode 100644 index 000000000..2837b075f --- /dev/null +++ b/src/theory/bv/slicer.cpp @@ -0,0 +1,615 @@ +/********************* */ +/*! \file slicer.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitvector theory. + ** + ** Bitvector theory. + **/ + +#include "theory/bv/slicer.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" +#include "theory/bv/options.h" +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace std; + + +const TermId CVC4::theory::bv::UndefinedId = -1; + +/** + * Base + * + */ +Base::Base(uint32_t size) + : d_size(size), + d_repr(size/32 + (size % 32 == 0? 0 : 1), 0) +{ + Assert (d_size > 0); +} + + +void Base::sliceAt(Index index) { + Index vector_index = index / 32; + if (vector_index == d_repr.size()) + return; + + Index int_index = index % 32; + uint32_t bit_mask = utils::pow2(int_index); + d_repr[vector_index] = d_repr[vector_index] | bit_mask; +} + +void Base::sliceWith(const Base& other) { + Assert (d_size == other.d_size); + for (unsigned i = 0; i < d_repr.size(); ++i) { + d_repr[i] = d_repr[i] | other.d_repr[i]; + } +} + +bool Base::isCutPoint (Index index) const { + // there is an implicit cut point at the end and begining of the bv + if (index == d_size || index == 0) + return true; + + Index vector_index = index / 32; + Assert (vector_index < d_size); + Index int_index = index % 32; + uint32_t bit_mask = utils::pow2(int_index); + + return (bit_mask & d_repr[vector_index]) != 0; +} + +void Base::diffCutPoints(const Base& other, Base& res) const { + Assert (d_size == other.d_size && res.d_size == d_size); + for (unsigned i = 0; i < d_repr.size(); ++i) { + Assert (res.d_repr[i] == 0); + res.d_repr[i] = d_repr[i] ^ other.d_repr[i]; + } +} + +bool Base::isEmpty() const { + for (unsigned i = 0; i< d_repr.size(); ++i) { + if (d_repr[i] != 0) + return false; + } + return true; +} + +std::string Base::debugPrint() const { + std::ostringstream os; + os << "["; + bool first = true; + for (int i = d_size - 1; i >= 0; --i) { + if (isCutPoint(i)) { + if (first) + first = false; + else + os <<"| "; + + os << i ; + } + } + os << "]"; + return os.str(); +} + +/** + * ExtractTerm + * + */ + +std::string ExtractTerm::debugPrint() const { + ostringstream os; + os << "id" << id << "[" << high << ":" << low <<"] "; + return os.str(); +} + +/** + * NormalForm + * + */ + +std::pair<TermId, Index> NormalForm::getTerm(Index index, const UnionFind& uf) const { + Assert (index < base.getBitwidth()); + Index count = 0; + for (unsigned i = 0; i < decomp.size(); ++i) { + Index size = uf.getBitwidth(decomp[i]); + if ( count + size > index && index >= count) { + return pair<TermId, Index>(decomp[i], count); + } + count += size; + } + Unreachable(); +} + + + +std::string NormalForm::debugPrint(const UnionFind& uf) const { + ostringstream os; + os << "NF " << base.debugPrint() << endl; + os << "("; + for (int i = decomp.size() - 1; i>= 0; --i) { + os << decomp[i] << "[" << uf.getBitwidth(decomp[i]) <<"]"; + os << (i != 0? ", " : ""); + } + os << ") \n"; + return os.str(); +} +/** + * UnionFind::Node + * + */ + +std::string UnionFind::Node::debugPrint() const { + ostringstream os; + os << "Repr " << d_repr << " ["<< d_bitwidth << "] "; + os << "( " << d_ch1 <<", " << d_ch0 << ")" << endl; + return os.str(); +} + + +/** + * UnionFind + * + */ +TermId UnionFind::addTerm(Index bitwidth) { + Node node(bitwidth); + d_nodes.push_back(node); + ++(d_statistics.d_numNodes); + + TermId id = d_nodes.size() - 1; + d_representatives.insert(id); + ++(d_statistics.d_numRepresentatives); + + Debug("bv-slicer-uf") << "UnionFind::addTerm " << id << " size " << bitwidth << endl; + return id; +} +/** + * At this point we assume the slicings of the two terms are properly aligned. + * + * @param t1 + * @param t2 + */ +void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) { + Debug("bv-slicer") << "UnionFind::unionTerms " << t1.debugPrint() << " and \n" + << " " << t2.debugPrint() << endl; + Assert (t1.getBitwidth() == t2.getBitwidth()); + + NormalForm nf1(t1.getBitwidth()); + NormalForm nf2(t2.getBitwidth()); + + getNormalForm(t1, nf1); + getNormalForm(t2, nf2); + + Assert (nf1.decomp.size() == nf2.decomp.size()); + Assert (nf1.base == nf2.base); + + for (unsigned i = 0; i < nf1.decomp.size(); ++i) { + merge (nf1.decomp[i], nf2.decomp[i]); + } +} + +/** + * Merge the two terms in the union find. Both t1 and t2 + * should be root terms. + * + * @param t1 + * @param t2 + */ +void UnionFind::merge(TermId t1, TermId t2) { + Debug("bv-slicer-uf") << "UnionFind::merge (" << t1 <<", " << t2 << ")" << endl; + ++(d_statistics.d_numMerges); + t1 = find(t1); + t2 = find(t2); + + if (t1 == t2) + return; + + Assert (! hasChildren(t1) && ! hasChildren(t2)); + setRepr(t1, t2); + d_representatives.erase(t1); + d_statistics.d_numRepresentatives += -1; +} + +TermId UnionFind::find(TermId id) { + TermId repr = getRepr(id); + if (repr != UndefinedId) { + TermId find_id = find(repr); + setRepr(id, find_id); + return find_id; + } + return id; +} +/** + * Splits the representative of the term between i-1 and i + * + * @param id the id of the term + * @param i the index we are splitting at + * + * @return + */ +void UnionFind::split(TermId id, Index i) { + Debug("bv-slicer-uf") << "UnionFind::split " << id << " at " << i << endl; + id = find(id); + Debug("bv-slicer-uf") << " node: " << d_nodes[id].debugPrint() << endl; + + if (i == 0 || i == getBitwidth(id)) { + // nothing to do + return; + } + Assert (i < getBitwidth(id)); + if (!hasChildren(id)) { + // first time we split this term + TermId bottom_id = addTerm(i); + TermId top_id = addTerm(getBitwidth(id) - i); + setChildren(id, top_id, bottom_id); + + } else { + Index cut = getCutPoint(id); + if (i < cut ) + split(getChild(id, 0), i); + else + split(getChild(id, 1), i - cut); + } + ++(d_statistics.d_numSplits); +} + +void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) { + nf.clear(); + getDecomposition(term, nf.decomp); + // update nf base + Index count = 0; + for (unsigned i = 0; i < nf.decomp.size(); ++i) { + count += getBitwidth(nf.decomp[i]); + nf.base.sliceAt(count); + } + Debug("bv-slicer-uf") << "UnionFind::getNormalFrom term: " << term.debugPrint() << endl; + Debug("bv-slicer-uf") << " nf: " << nf.debugPrint(*this) << endl; +} + +void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp) { + // making sure the term is aligned + TermId id = find(term.id); + + Assert (term.high < getBitwidth(id)); + // because we split the node, this must be the whole extract + if (!hasChildren(id)) { + Assert (term.high == getBitwidth(id) - 1 && + term.low == 0); + decomp.push_back(id); + return; + } + + Index cut = getCutPoint(id); + + if (term.low < cut && term.high < cut) { + // the extract falls entirely on the low child + ExtractTerm child_ex(getChild(id, 0), term.high, term.low); + getDecomposition(child_ex, decomp); + } + else if (term.low >= cut && term.high >= cut){ + // the extract falls entirely on the high child + ExtractTerm child_ex(getChild(id, 1), term.high - cut, term.low - cut); + getDecomposition(child_ex, decomp); + } + else { + // the extract is split over the two children + ExtractTerm low_child(getChild(id, 0), cut - 1, term.low); + getDecomposition(low_child, decomp); + ExtractTerm high_child(getChild(id, 1), term.high - cut, 0); + getDecomposition(high_child, decomp); + } +} +/** + * May cause reslicings of the decompositions. Must not assume the decompositons + * are the current normal form. + * + * @param d1 + * @param d2 + * @param common + */ +void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposition& decomp2, TermId common) { + Debug("bv-slicer") << "UnionFind::handleCommonSlice common = " << common << endl; + Index common_size = getBitwidth(common); + // find starting points of common slice + Index start1 = 0; + for (unsigned j = 0; j < decomp1.size(); ++j) { + if (decomp1[j] == common) + break; + start1 += getBitwidth(decomp1[j]); + } + + Index start2 = 0; + for (unsigned j = 0; j < decomp2.size(); ++j) { + if (decomp2[j] == common) + break; + start2 += getBitwidth(decomp2[j]); + } + if (start1 > start2) { + Index temp = start1; + start1 = start2; + start2 = temp; + } + + if (start2 - start1 < common_size) { + Index overlap = start1 + common_size - start2; + Assert (overlap > 0); + Index diff = common_size - overlap; + Assert (diff >= 0); + Index granularity = utils::gcd(diff, overlap); + // split the common part + for (unsigned i = 0; i < common_size; i+= granularity) { + split(common, i); + } + } + +} + +void UnionFind::alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2) { + Debug("bv-slicer") << "UnionFind::alignSlicings " << term1.debugPrint() << endl; + Debug("bv-slicer") << " " << term2.debugPrint() << endl; + NormalForm nf1(term1.getBitwidth()); + NormalForm nf2(term2.getBitwidth()); + + getNormalForm(term1, nf1); + getNormalForm(term2, nf2); + + Assert (nf1.base.getBitwidth() == nf2.base.getBitwidth()); + + // first check if the two have any common slices + std::vector<TermId> intersection; + utils::intersect(nf1.decomp, nf2.decomp, intersection); + for (unsigned i = 0; i < intersection.size(); ++i) { + // handle common slice may change the normal form + handleCommonSlice(nf1.decomp, nf2.decomp, intersection[i]); + } + // propagate cuts to a fixpoint + bool changed; + Base cuts(term1.getBitwidth()); + do { + changed = false; + // we need to update the normal form which may have changed + getNormalForm(term1, nf1); + getNormalForm(term2, nf2); + + // align the cuts points of the two slicings + // FIXME: this can be done more efficiently + cuts.sliceWith(nf1.base); + cuts.sliceWith(nf2.base); + + for (unsigned i = 0; i < cuts.getBitwidth(); ++i) { + if (cuts.isCutPoint(i)) { + if (!nf1.base.isCutPoint(i)) { + pair<TermId, Index> pair1 = nf1.getTerm(i, *this); + split(pair1.first, i - pair1.second); + changed = true; + } + if (!nf2.base.isCutPoint(i)) { + pair<TermId, Index> pair2 = nf2.getTerm(i, *this); + split(pair2.first, i - pair2.second); + changed = true; + } + } + } + } while (changed); +} +/** + * Given an extract term a[i:j] makes sure a is sliced + * at indices i and j. + * + * @param term + */ +void UnionFind::ensureSlicing(const ExtractTerm& term) { + //Debug("bv-slicer") << "Slicer::ensureSlicing " << term.debugPrint() << endl; + TermId id = find(term.id); + split(id, term.high + 1); + split(id, term.low); +} + +/** + * Slicer + * + */ + +ExtractTerm Slicer::registerTerm(TNode node) { + Index low = 0, high = utils::getSize(node) - 1; + TNode n = node; + if (node.getKind() == kind::BITVECTOR_EXTRACT) { + n = node[0]; + high = utils::getExtractHigh(node); + low = utils::getExtractLow(node); + } + if (d_nodeToId.find(n) == d_nodeToId.end()) { + TermId id = d_unionFind.addTerm(utils::getSize(n)); + d_nodeToId[n] = id; + d_idToNode[id] = n; + } + TermId id = d_nodeToId[n]; + ExtractTerm res(id, high, low); + Debug("bv-slicer") << "Slicer::registerTerm " << node << " => " << res.debugPrint() << endl; + return res; +} + +void Slicer::processEquality(TNode eq) { + Debug("bv-slicer") << "Slicer::processEquality: " << eq << endl; + + Assert (eq.getKind() == kind::EQUAL); + TNode a = eq[0]; + TNode b = eq[1]; + ExtractTerm a_ex= registerTerm(a); + ExtractTerm b_ex= registerTerm(b); + + d_unionFind.ensureSlicing(a_ex); + d_unionFind.ensureSlicing(b_ex); + + d_unionFind.alignSlicings(a_ex, b_ex); + d_unionFind.unionTerms(a_ex, b_ex); + Debug("bv-slicer") << "Base of " << a_ex.id <<" " << d_unionFind.debugPrint(a_ex.id) << endl; + Debug("bv-slicer") << "Base of " << b_ex.id <<" " << d_unionFind.debugPrint(b_ex.id) << endl; + Debug("bv-slicer") << "Slicer::processEquality done. " << endl; +} + +void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) { + Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl; + + Index high = utils::getSize(node) - 1; + Index low = 0; + TNode top = node; + if (node.getKind() == kind::BITVECTOR_EXTRACT) { + high = utils::getExtractHigh(node); + low = utils::getExtractLow(node); + top = node[0]; + } + Assert (d_nodeToId.find(top) != d_nodeToId.end()); + TermId id = d_nodeToId[top]; + NormalForm nf(high-low+1); + d_unionFind.getNormalForm(ExtractTerm(id, high, low), nf); + + // construct actual extract nodes + unsigned size = utils::getSize(node); + Index current_low = size; + Index current_high = size; + for (int i = nf.decomp.size() - 1; i >= 0; --i) { + Index current_size = d_unionFind.getBitwidth(nf.decomp[i]); + current_low -= current_size; + Node current = Rewriter::rewrite(utils::mkExtract(node, current_high - 1, current_low)); + current_high = current_low; + decomp.push_back(current); + } + + Debug("bv-slicer") << "as ["; + for (unsigned i = 0; i < decomp.size(); ++i) { + Debug("bv-slicer") << decomp[i] <<" "; + } + Debug("bv-slicer") << "]" << endl; + +} + +bool Slicer::isCoreTerm(TNode node) { + if (d_coreTermCache.find(node) == d_coreTermCache.end()) { + Kind kind = node.getKind(); + bool not_core; + if (options::bitvectorCoreSolver()) { + not_core = (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT); + } else { + not_core = true; + } + if (not_core && + kind != kind::EQUAL && + kind != kind::NOT && + kind != kind::STORE && + kind != kind::SELECT && + node.getMetaKind() != kind::metakind::VARIABLE && + kind != kind::CONST_BITVECTOR) { + d_coreTermCache[node] = false; + return false; + } else { + // we need to recursively check whether the term is a root term or not + bool isCore = true; + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + isCore = isCore && isCoreTerm(node[i]); + } + d_coreTermCache[node] = isCore; + return isCore; + } + } + return d_coreTermCache[node]; +} +unsigned Slicer::d_numAddedEqualities = 0; + +void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) { + Assert (node.getKind() == kind::EQUAL); + TNode t1 = node[0]; + TNode t2 = node[1]; + + uint32_t width = utils::getSize(t1); + + Base base1(width); + if (t1.getKind() == kind::BITVECTOR_CONCAT) { + int size = 0; + // no need to count the last child since the end cut point is implicit + for (int i = t1.getNumChildren() - 1; i >= 1 ; --i) { + size = size + utils::getSize(t1[i]); + base1.sliceAt(size); + } + } + + Base base2(width); + if (t2.getKind() == kind::BITVECTOR_CONCAT) { + unsigned size = 0; + for (int i = t2.getNumChildren() - 1; i >= 1; --i) { + size = size + utils::getSize(t2[i]); + base2.sliceAt(size); + } + } + + base1.sliceWith(base2); + if (!base1.isEmpty()) { + // we split the equalities according to the base + int last = 0; + for (unsigned i = 1; i <= utils::getSize(t1); ++i) { + if (base1.isCutPoint(i)) { + Node extract1 = utils::mkExtract(t1, i-1, last); + Node extract2 = utils::mkExtract(t2, i-1, last); + last = i; + Assert (utils::getSize(extract1) == utils::getSize(extract2)); + equalities.push_back(utils::mkNode(kind::EQUAL, extract1, extract2)); + } + } + } else { + // just return same equality + equalities.push_back(node); + } + d_numAddedEqualities += equalities.size() - 1; +} + +std::string UnionFind::debugPrint(TermId id) { + ostringstream os; + if (hasChildren(id)) { + TermId id1 = find(getChild(id, 1)); + TermId id0 = find(getChild(id, 0)); + os << debugPrint(id1); + os << debugPrint(id0); + } else { + if (getRepr(id) == UndefinedId) { + os <<"id"<< id <<"[" << getBitwidth(id) <<"] "; + } else { + os << debugPrint(find(id)); + } + } + return os.str(); +} + +UnionFind::Statistics::Statistics(): + d_numNodes("theory::bv::slicer::NumberOfNodes", 0), + d_numRepresentatives("theory::bv::slicer::NumberOfRepresentatives", 0), + d_numSplits("theory::bv::slicer::NumberOfSplits", 0), + d_numMerges("theory::bv::slicer::NumberOfMerges", 0), + d_avgFindDepth("theory::bv::slicer::AverageFindDepth"), + d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities) +{ + StatisticsRegistry::registerStat(&d_numRepresentatives); + StatisticsRegistry::registerStat(&d_numSplits); + StatisticsRegistry::registerStat(&d_numMerges); + StatisticsRegistry::registerStat(&d_avgFindDepth); + StatisticsRegistry::registerStat(&d_numAddedEqualities); +} + +UnionFind::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_numRepresentatives); + StatisticsRegistry::unregisterStat(&d_numSplits); + StatisticsRegistry::unregisterStat(&d_numMerges); + StatisticsRegistry::unregisterStat(&d_avgFindDepth); + StatisticsRegistry::unregisterStat(&d_numAddedEqualities); +} diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h new file mode 100644 index 000000000..88254b983 --- /dev/null +++ b/src/theory/bv/slicer.h @@ -0,0 +1,255 @@ +/********************* */ +/*! \file slicer.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitvector theory. + ** + ** Bitvector theory. + **/ + +#include "cvc4_private.h" + + +#include <vector> +#include <list> +#include <ext/hash_map> +#include <math.h> + +#include "util/bitvector.h" +#include "util/statistics_registry.h" +#include "util/index.h" +#include "expr/node.h" +#include "theory/bv/theory_bv_utils.h" +#ifndef __CVC4__THEORY__BV__SLICER_BV_H +#define __CVC4__THEORY__BV__SLICER_BV_H + + +namespace CVC4 { + +namespace theory { +namespace bv { + + + +typedef Index TermId; +extern const TermId UndefinedId; + + +/** + * Base + * + */ +class Base { + Index d_size; + std::vector<uint32_t> d_repr; +public: + Base(Index size); + void sliceAt(Index index); + void sliceWith(const Base& other); + bool isCutPoint(Index index) const; + void diffCutPoints(const Base& other, Base& res) const; + bool isEmpty() const; + std::string debugPrint() const; + Index getBitwidth() const { return d_size; } + void clear() { + for (unsigned i = 0; i < d_repr.size(); ++i) { + d_repr[i] = 0; + } + } + bool operator==(const Base& other) const { + if (other.getBitwidth() != getBitwidth()) + return false; + for (unsigned i = 0; i < d_repr.size(); ++i) { + if (d_repr[i] != other.d_repr[i]) + return false; + } + return true; + } +}; + +/** + * UnionFind + * + */ +typedef __gnu_cxx::hash_set<TermId> TermSet; +typedef std::vector<TermId> Decomposition; + +struct ExtractTerm { + TermId id; + Index high; + Index low; + ExtractTerm(TermId i, Index h, Index l) + : id (i), + high(h), + low(l) + { + Assert (h >= l && id != UndefinedId); + } + Index getBitwidth() const { return high - low + 1; } + std::string debugPrint() const; +}; + +class UnionFind; + +struct NormalForm { + Base base; + Decomposition decomp; + + NormalForm(Index bitwidth) + : base(bitwidth), + decomp() + {} + /** + * Returns the term in the decomposition on which the index i + * falls in + * @param i + * + * @return + */ + std::pair<TermId, Index> getTerm(Index i, const UnionFind& uf) const; + std::string debugPrint(const UnionFind& uf) const; + void clear() { base.clear(); decomp.clear(); } +}; + + +class UnionFind { + class Node { + Index d_bitwidth; + TermId d_ch1, d_ch0; + TermId d_repr; + public: + Node(Index b) + : d_bitwidth(b), + d_ch1(UndefinedId), + d_ch0(UndefinedId), + d_repr(UndefinedId) + {} + + TermId getRepr() const { return d_repr; } + Index getBitwidth() const { return d_bitwidth; } + bool hasChildren() const { return d_ch1 != UndefinedId && d_ch0 != UndefinedId; } + + TermId getChild(Index i) const { + Assert (i < 2); + return i == 0? d_ch0 : d_ch1; + } + void setRepr(TermId id) { + Assert (! hasChildren()); + d_repr = id; + } + void setChildren(TermId ch1, TermId ch0) { + Assert (d_repr == UndefinedId && !hasChildren()); + d_ch1 = ch1; + d_ch0 = ch0; + } + std::string debugPrint() const; + }; + + /// map from TermId to the nodes that represent them + std::vector<Node> d_nodes; + /// a term is in this set if it is its own representative + TermSet d_representatives; + + void getDecomposition(const ExtractTerm& term, Decomposition& decomp); + void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common); + /// getter methods for the internal nodes + TermId getRepr(TermId id) const { + Assert (id < d_nodes.size()); + return d_nodes[id].getRepr(); + } + TermId getChild(TermId id, Index i) const { + Assert (id < d_nodes.size()); + return d_nodes[id].getChild(i); + } + Index getCutPoint(TermId id) const { + return getBitwidth(getChild(id, 0)); + } + bool hasChildren(TermId id) const { + Assert (id < d_nodes.size()); + return d_nodes[id].hasChildren(); + } + /// setter methods for the internal nodes + void setRepr(TermId id, TermId new_repr) { + Assert (id < d_nodes.size()); + d_nodes[id].setRepr(new_repr); + } + void setChildren(TermId id, TermId ch1, TermId ch0) { + Assert (id < d_nodes.size() && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch0)); + d_nodes[id].setChildren(ch1, ch0); + } + + class Statistics { + public: + IntStat d_numNodes; + IntStat d_numRepresentatives; + IntStat d_numSplits; + IntStat d_numMerges; + AverageStat d_avgFindDepth; + ReferenceStat<unsigned> d_numAddedEqualities; + //IntStat d_numAddedEqualities; + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics +; + +public: + UnionFind() + : d_nodes(), + d_representatives() + {} + + TermId addTerm(Index bitwidth); + void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2); + void merge(TermId t1, TermId t2); + TermId find(TermId t1); + void split(TermId term, Index i); + + void getNormalForm(const ExtractTerm& term, NormalForm& nf); + void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2); + void ensureSlicing(const ExtractTerm& term); + Index getBitwidth(TermId id) const { + Assert (id < d_nodes.size()); + return d_nodes[id].getBitwidth(); + } + std::string debugPrint(TermId id); + friend class Slicer; +}; + +class Slicer { + __gnu_cxx::hash_map<TermId, TNode> d_idToNode; + __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId; + __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache; + UnionFind d_unionFind; + ExtractTerm registerTerm(TNode node); +public: + Slicer() + : d_idToNode(), + d_nodeToId(), + d_coreTermCache(), + d_unionFind() + {} + + void getBaseDecomposition(TNode node, std::vector<Node>& decomp); + void processEquality(TNode eq); + bool isCoreTerm (TNode node); + static void splitEqualities(TNode node, std::vector<Node>& equalities); + static unsigned d_numAddedEqualities; +}; + + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BV__SLICER_BV_H */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index e28ef3ddf..b202b7eca 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -17,10 +17,14 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/bv/slicer.h" #include "theory/valuation.h" #include "theory/bv/bitblaster.h" #include "theory/bv/options.h" #include "theory/bv/theory_bv_rewrite_rules_normalization.h" +#include "theory/bv/bv_subtheory_core.h" +#include "theory/bv/bv_subtheory_inequality.h" +#include "theory/bv/bv_subtheory_bitblast.h" #include "theory/model.h" using namespace CVC4; @@ -31,46 +35,68 @@ using namespace CVC4::context; using namespace std; using namespace CVC4::theory::bv::utils; - - - TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : Theory(THEORY_BV, c, u, out, valuation, logicInfo, qe), d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), - d_bitblastSolver(c, this), - d_equalitySolver(c, this), + d_subtheories(), + d_subtheoryMap(), d_statistics(), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_propagatedBy(c) - {} - -TheoryBV::~TheoryBV() {} + { + SubtheorySolver* core_solver = new CoreSolver(c, this); + d_subtheories.push_back(core_solver); + d_subtheoryMap[SUB_CORE] = core_solver; + + if (options::bitvectorInequalitySolver()) { + SubtheorySolver* ineq_solver = new InequalitySolver(c, this); + d_subtheories.push_back(ineq_solver); + d_subtheoryMap[SUB_INEQUALITY] = ineq_solver; + } + + SubtheorySolver* bb_solver = new BitblastSolver(c, this); + d_subtheories.push_back(bb_solver); + d_subtheoryMap[SUB_BITBLAST] = bb_solver; + } +TheoryBV::~TheoryBV() { + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + delete d_subtheories[i]; + } +} void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_equalitySolver.setMasterEqualityEngine(eq); + dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq); } TheoryBV::Statistics::Statistics(): d_avgConflictSize("theory::bv::AvgBVConflictSize"), d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0), - d_solveTimer("theory::bv::solveTimer") + d_solveTimer("theory::bv::solveTimer"), + d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0), + d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0) { StatisticsRegistry::registerStat(&d_avgConflictSize); StatisticsRegistry::registerStat(&d_solveSubstitutions); StatisticsRegistry::registerStat(&d_solveTimer); + StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort); + StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort); } TheoryBV::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_avgConflictSize); StatisticsRegistry::unregisterStat(&d_solveSubstitutions); StatisticsRegistry::unregisterStat(&d_solveTimer); + StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort); + StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort); } + + void TheoryBV::preRegisterTerm(TNode node) { Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; @@ -78,9 +104,9 @@ void TheoryBV::preRegisterTerm(TNode node) { // don't use the equality engine in the eager bit-blasting return; } - - d_bitblastSolver.preRegister(node); - d_equalitySolver.preRegister(node); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + d_subtheories[i]->preRegister(node); + } } void TheoryBV::sendConflict() { @@ -98,51 +124,65 @@ void TheoryBV::sendConflict() { void TheoryBV::check(Effort e) { Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; - + if (Theory::fullEffort(e)) { + ++(d_statistics.d_numCallsToCheckFullEffort); + } else { + ++(d_statistics.d_numCallsToCheckStandardEffort); + } // if we are already in conflict just return the conflict if (inConflict()) { sendConflict(); return; } - // getting the new assertions - std::vector<TNode> new_assertions; while (!done()) { - Assertion assertion = get(); - TNode fact = assertion.assertion; - new_assertions.push_back(fact); - Debug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; - } - - if (!inConflict()) { - // sending assertions to the equality solver first - d_equalitySolver.addAssertions(new_assertions, e); + TNode fact = get().assertion; + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + d_subtheories[i]->assertFact(fact); + } } - if (!inConflict()) { - // sending assertions to the bitblast solver - d_bitblastSolver.addAssertions(new_assertions, e); - } + bool ok = true; + bool complete = false; + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + Assert (!inConflict()); + ok = d_subtheories[i]->check(e); + complete = d_subtheories[i]->isComplete(); - if (inConflict()) { - sendConflict(); + if (!ok) { + // if we are in a conflict no need to check with other theories + Assert (inConflict()); + sendConflict(); + return; + } + if (complete) { + // if the last subtheory was complete we stop + return; + } } } void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); // Assert (fullModel); // can only query full model - d_equalitySolver.collectModelInfo(m); - d_bitblastSolver.collectModelInfo(m); - + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + if (d_subtheories[i]->isComplete()) { + d_subtheories[i]->collectModelInfo(m); + return; + } + } } Node TheoryBV::getModelValue(TNode var) { Assert(!inConflict()); - return d_bitblastSolver.getModelValue(var); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + if (d_subtheories[i]->isComplete()) { + return d_subtheories[i]->getModelValue(var); + } + } + Unreachable(); } - void TheoryBV::propagate(Effort e) { Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; @@ -193,16 +233,25 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu return PP_ASSERT_STATUS_UNSOLVED; } - Node TheoryBV::ppRewrite(TNode t) { if (RewriteRule<BitwiseEq>::applies(t)) { Node result = RewriteRule<BitwiseEq>::run<false>(t); return Rewriter::rewrite(result); } + + if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { + std::vector<Node> equalities; + Slicer::splitEqualities(t, equalities); + return utils::mkAnd(equalities); + } + return t; } +void TheoryBV::presolve() { + Debug("bitvector") << "TheoryBV::presolve" << endl; +} bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) { @@ -226,6 +275,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) // Safe to ignore this one, subtheory should produce a conflict return true; } + d_propagatedBy[literal] = subtheory; } @@ -233,7 +283,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain // * equality engine can propagate eagerly bool ok = true; - if (subtheory == SUB_EQUALITY) { + if (subtheory == SUB_CORE) { d_out->propagate(literal); if (!ok) { setConflict(); @@ -247,15 +297,9 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { - // Ask the appropriate subtheory for the explanation - if (propagatedBy(literal, SUB_EQUALITY)) { - Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl; - d_equalitySolver.explain(literal, assumptions); - } else { - Assert(propagatedBy(literal, SUB_BITBLAST)); - Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl; - d_bitblastSolver.explain(literal, assumptions); - } + Assert (wasPropagatedBySubtheory(literal)); + SubTheory sub = getPropagatingSubtheory(literal); + d_subtheoryMap[sub]->explain(literal, assumptions); } @@ -280,7 +324,9 @@ void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) { - d_equalitySolver.addSharedTerm(t); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + d_subtheories[i]->addSharedTerm(t); + } } } @@ -290,12 +336,13 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) if (options::bitvectorEagerBitblast()) { return EQUALITY_UNKNOWN; } - - EqualityStatus status = d_equalitySolver.getEqualityStatus(a, b); - if (status == EQUALITY_UNKNOWN) { - status = d_bitblastSolver.getEqualityStatus(a, b); + + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); + if (status != EQUALITY_UNKNOWN) { + return status; + } } - - return status; + return EQUALITY_UNKNOWN; ; } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ffb043bb6..ff8b3a8b1 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -25,15 +25,16 @@ #include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" -#include "context/cdqueue.h" #include "theory/bv/bv_subtheory.h" -#include "theory/bv/bv_subtheory_eq.h" -#include "theory/bv/bv_subtheory_bitblast.h" namespace CVC4 { namespace theory { namespace bv { +class CoreSolver; +class InequalitySolver; +class BitblastSolver; + class TheoryBV : public Theory { /** The context we are using */ @@ -42,9 +43,9 @@ class TheoryBV : public Theory { /** Context dependent set of atoms we already propagated */ context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet; context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; - - BitblastSolver d_bitblastSolver; - EqualitySolver d_equalitySolver; + + std::vector<SubtheorySolver*> d_subtheories; + __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); @@ -67,6 +68,7 @@ public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); Node ppRewrite(TNode t); + void presolve(); private: class Statistics { @@ -74,6 +76,8 @@ private: AverageStat d_avgConflictSize; IntStat d_solveSubstitutions; TimerStat d_solveTimer; + IntStat d_numCallsToCheckFullEffort; + IntStat d_numCallsToCheckStandardEffort; Statistics(); ~Statistics(); }; @@ -99,10 +103,14 @@ private: typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap; PropagatedMap d_propagatedBy; - bool propagatedBy(TNode literal, SubTheory subtheory) const { + bool wasPropagatedBySubtheory(TNode literal) const { + return d_propagatedBy.find(literal) != d_propagatedBy.end(); + } + + SubTheory getPropagatingSubtheory(TNode literal) const { + Assert(wasPropagatedBySubtheory(literal)); PropagatedMap::const_iterator find = d_propagatedBy.find(literal); - if (find == d_propagatedBy.end()) return false; - else return (*find).second == subtheory; + return (*find).second; } /** Should be called to propagate the literal. */ @@ -115,6 +123,8 @@ private: void addSharedTerm(TNode t); + bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } + EqualityStatus getEqualityStatus(TNode a, TNode b); Node getModelValue(TNode var); @@ -136,10 +146,13 @@ private: void sendConflict(); + void lemma(TNode node) { d_out->lemma(node); } + friend class Bitblaster; friend class BitblastSolver; friend class EqualitySolver; - + friend class CoreSolver; + friend class InequalitySolver; };/* class TheoryBV */ }/* CVC4::theory::bv namespace */ diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 7d851d0fb..f8b9f010e 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -31,6 +31,12 @@ namespace theory { namespace bv { namespace utils { +inline uint32_t pow2(uint32_t power) { + Assert (power < 32); + uint32_t one = 1; + return one << power; +} + inline unsigned getExtractHigh(TNode node) { return node.getOperator().getConst<BitVectorExtract>().high; } @@ -63,28 +69,6 @@ inline Node mkVar(unsigned size) { return nm->mkSkolem("bv_$$", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors"); } -inline Node mkAnd(std::vector<TNode>& children) { - std::set<TNode> distinctChildren; - distinctChildren.insert(children.begin(), children.end()); - - if (children.size() == 0) { - return mkTrue(); - } - - if (children.size() == 1) { - return *children.begin(); - } - - NodeBuilder<> conjunction(kind::AND); - std::set<TNode>::const_iterator it = distinctChildren.begin(); - std::set<TNode>::const_iterator it_end = distinctChildren.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -} inline Node mkSortedNode(Kind kind, std::vector<Node>& children) { Assert (kind == kind::BITVECTOR_AND || @@ -149,14 +133,6 @@ inline Node mkXor(TNode node1, TNode node2) { } -inline Node mkAnd(std::vector<Node>& children) { - if(children.size() > 1) { - return NodeManager::currentNM()->mkNode(kind::AND, children); - } else { - return children[0]; - } -} - inline Node mkExtract(TNode node, unsigned high, unsigned low) { Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low)); std::vector<Node> children; @@ -262,7 +238,6 @@ inline Node mkConjunction(const std::set<TNode> nodes) { return conjunction; } - inline unsigned isPow2Const(TNode node) { if (node.getKind() != kind::CONST_BITVECTOR) { return false; @@ -272,6 +247,109 @@ inline unsigned isPow2Const(TNode node) { return bv.isPow2(); } +typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + +inline Node mkOr(const std::vector<Node>& nodes) { + std::set<TNode> all; + all.insert(nodes.begin(), nodes.end()); + + if (all.size() == 0) { + return mkTrue(); + } + + if (all.size() == 1) { + // All the same, or just one + return nodes[0]; + } + + + NodeBuilder<> disjunction(kind::OR); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + disjunction << *it; + ++ it; + } + + return disjunction; +}/* mkOr() */ + + +inline Node mkAnd(const std::vector<TNode>& conjunctions) { + std::set<TNode> all; + all.insert(conjunctions.begin(), conjunctions.end()); + + if (all.size() == 0) { + return mkTrue(); + } + + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + + NodeBuilder<> conjunction(kind::AND); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; +}/* mkAnd() */ + +inline Node mkAnd(const std::vector<Node>& conjunctions) { + std::set<TNode> all; + all.insert(conjunctions.begin(), conjunctions.end()); + + if (all.size() == 0) { + return mkTrue(); + } + + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + + NodeBuilder<> conjunction(kind::AND); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; +}/* mkAnd() */ + + + +inline Node flattenAnd(std::vector<TNode>& queue) { + TNodeSet nodes; + while(!queue.empty()) { + TNode current = queue.back(); + queue.pop_back(); + if (current.getKind() == kind::AND) { + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + if (nodes.count(current[i]) == 0) { + queue.push_back(current[i]); + } + } + } else { + nodes.insert(current); + } + } + std::vector<TNode> children; + for (TNodeSet::const_iterator it = nodes.begin(); it!= nodes.end(); ++it) { + children.push_back(*it); + } + return mkAnd(children); +} + + // neeed a better name, this is not technically a ground term inline bool isBVGroundTerm(TNode node) { if (node.getNumChildren() == 0) { @@ -350,27 +428,7 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) { } -inline Node mkAnd(const std::vector<TNode>& conjunctions) { - Assert(conjunctions.size() > 0); - - std::set<TNode> all; - all.insert(conjunctions.begin(), conjunctions.end()); - - if (all.size() == 1) { - // All the same, or just one - return conjunctions[0]; - } - - NodeBuilder<> conjunction(kind::AND); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - return conjunction; -}/* mkAnd() */ // Turn a set into a string @@ -406,6 +464,35 @@ inline std::string vectorToString(const std::vector<Node>& nodes) { return out.str(); } +// FIXME: dumb code +inline void intersect(const std::vector<uint32_t>& v1, + const std::vector<uint32_t>& v2, + std::vector<uint32_t>& intersection) { + for (unsigned i = 0; i < v1.size(); ++i) { + bool found = false; + for (unsigned j = 0; j < v2.size(); ++j) { + if (v2[j] == v1[i]) { + found = true; + break; + } + } + if (found) { + intersection.push_back(v1[i]); + } + } +} + +template <class T> +inline T gcd(T a, T b) { + while (b != 0) { + T t = b; + b = a % t; + a = t; + } + return a; +} + + } } } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b89ca8fa4..1c297eda6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1194,8 +1194,12 @@ Node TheoryEngine::getExplanation(TNode node) { theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable) { if(Dump.isOn("t-lemmas")) { + Node n = node; + if (negated) { + n = node.negate(); + } Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") - << QueryCommand(node.toExpr()); + << QueryCommand(n.toExpr()); } // Share with other portfolio threads diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 4cbcba50e..c9661c0c7 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -178,10 +178,23 @@ public: Integer prod = d_value * y.d_value; return BitVector(d_size, prod); } + + BitVector setBit(uint32_t i) const { + CheckArgument(i < d_size, i); + Integer res = d_value.setBit(i); + return BitVector(d_size, res); + } + + bool isBitSet(uint32_t i) const { + CheckArgument(i < d_size, i); + return d_value.isBitSet(i); + } + /** * Total division function that returns 0 when the denominator is 0. */ BitVector unsignedDivTotal (const BitVector& y) const { + CheckArgument(d_size == y.d_size, y); if (y.d_value == 0) { return BitVector(d_size, 0u); @@ -190,6 +203,7 @@ public: CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } + /** * Total division function that returns 0 when the denominator is 0. */ diff --git a/src/util/index.h b/src/util/index.h index 4c03af5b0..252f7066b 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -21,6 +21,7 @@ #include <stdint.h> #include <boost/static_assert.hpp> +#include <limits> namespace CVC4 { diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index b5452ae00..81c0428cb 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -218,6 +218,16 @@ public: return Integer( d_value << ipow); } + bool isBitSet(uint32_t i) const { + return !extractBitRange(1, i).isZero(); + } + + Integer setBit(uint32_t i) const { + cln::cl_I mask(1); + mask = mask << i; + return Integer(cln::logior(d_value, mask)); + } + Integer oneExtend(uint32_t size, uint32_t amount) const { DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); cln::cl_byte range(amount, size); diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 176604268..85d49f921 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -137,6 +137,7 @@ public: return *this; } + Integer bitwiseOr(const Integer& y) const { mpz_class result; mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); @@ -170,6 +171,24 @@ public: return Integer( result ); } + /** + * Returns the Integer obtained by setting the ith bit of the + * current Integer to 1. + * + * @param bit + * + * @return + */ + Integer setBit(uint32_t i) const { + mpz_class res = d_value; + mpz_setbit(res.get_mpz_t(), i); + return Integer(res); + } + + bool isBitSet(uint32_t i) const { + return !extractBitRange(1, i).isZero(); + } + /** * Returns the integer with the binary representation of size bits * extended with amount 1's diff --git a/src/util/record.i b/src/util/record.i index 2805d2fdf..368519f5b 100644 --- a/src/util/record.i +++ b/src/util/record.i @@ -19,6 +19,8 @@ %ignore CVC4::Record::operator!=(const Record&) const; %rename(getField) CVC4::Record::operator[](size_t) const; +#ifdef SWIGJAVA + // These Object arrays are always of two elements, the first is a String and the second a // Type. (On the C++ side, it is a std::pair<std::string, Type>.) %typemap(jni) std::pair<std::string, CVC4::Type> "jobjectArray"; @@ -33,8 +35,6 @@ jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::Type($1.second)), true)); }; -#ifdef SWIGJAVA - // Instead of Record::begin() and end(), create an // iterator() method on the Java side that returns a Java-style // Iterator. @@ -79,6 +79,15 @@ // getNext() just allows C++ iterator access from Java-side next(), make it private %javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Record>::getNext() "private"; +// map the types appropriately. for records, the "payload" of the iterator is an Object[]. +// These Object arrays are always of two elements, the first is a String and the second a +// Type. (On the C++ side, it is a std::pair<std::string, SExpr>.) +%typemap(jni) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; +%typemap(jtype) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; +%typemap(jstype) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; +%typemap(javaout) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; +%typemap(out) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; + #endif /* SWIGJAVA */ %include "util/record.h" diff --git a/src/util/utility.h b/src/util/utility.h index 5ce185b5b..089be478d 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -67,7 +67,6 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre return (match2 == last) ? match : last; } - }/* CVC4 namespace */ #endif /* __CVC4__UTILITY_H */ diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2 new file mode 100644 index 000000000..c7a5a605f --- /dev/null +++ b/test/regress/regress0/bv/core/constant_core.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x () (_ BitVec 3)) +(assert (and +(= ((_ extract 1 0) x) (concat ((_ extract 1 1) x) ((_ extract 0 0) x))) +(= ((_ extract 0 0) x) ((_ extract 1 1) x)) +(= ((_ extract 2 2) x) ((_ extract 1 1) x)) +(= (_ bv0 1) ((_ extract 0 0) x)) +(= x (concat ((_ extract 2 2) x) ((_ extract 1 0) x))) +(not (= (_ bv0 3) x)) +)) +(check-sat) +(exit)
\ No newline at end of file diff --git a/test/regress/regress0/bv/core/incremental.smt b/test/regress/regress0/bv/core/incremental.smt new file mode 100644 index 000000000..3a9ff85e0 --- /dev/null +++ b/test/regress/regress0/bv/core/incremental.smt @@ -0,0 +1,24 @@ +(benchmark ext_con_004_004_0016.smt +:logic QF_BV +:extrafuns ((v4 BitVec[16])) +:extrafuns ((dummy4 BitVec[1])) +:extrafuns ((a BitVec[16])) +:status unknown +:formula +(flet ($n1 true) +(let (?n2 (extract[15:13] a)) +(let (?n3 (extract[15:14] v4)) +(let (?n4 (concat ?n3 dummy4)) +(flet ($n5 (= ?n2 ?n4)) +(let (?n6 (extract[14:12] a)) +(let (?n7 (extract[13:12] v4)) +(let (?n8 (concat dummy4 ?n7)) +(flet ($n9 (= ?n6 ?n8)) +(flet ($n10 (and $n5 $n9)) +(let (?n11 (extract[14:14] v4)) +(let (?n12 (extract[13:13] v4)) +(flet ($n13 (= ?n11 ?n12)) +(flet ($n14 (not $n13)) +(flet ($n15 (and $n1 $n1 $n1 $n10 $n14)) +$n15 +)))))))))))))))) diff --git a/test/regress/regress0/bv/core/slice-14.smt b/test/regress/regress0/bv/core/slice-14.smt index b40f7938d..db3a3a7b3 100644 --- a/test/regress/regress0/bv/core/slice-14.smt +++ b/test/regress/regress0/bv/core/slice-14.smt @@ -1,8 +1,8 @@ (benchmark slice :status unsat :logic QF_BV - :extrafuns ((x BitVec[16])) - :assumption (= (extract[15:1] x) (extract[14:0] x)) + :extrafuns ((x BitVec[6])) + :assumption (= (extract[5:1] x) (extract[4:0] x)) :assumption (= (extract[0:0] x) bv0[1]) - :formula (not (= x bv0[16])) + :formula (not (= x bv0[6])) ) diff --git a/test/regress/regress0/bv/inequality00.smt2 b/test/regress/regress0/bv/inequality00.smt2 new file mode 100644 index 000000000..dc6285d52 --- /dev/null +++ b/test/regress/regress0/bv/inequality00.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v0 () (_ BitVec 16)) +(declare-fun v1 () (_ BitVec 16)) +(declare-fun v2 () (_ BitVec 16)) +(declare-fun v3 () (_ BitVec 16)) +(declare-fun v4 () (_ BitVec 16)) +(declare-fun v5 () (_ BitVec 16)) +(assert (and + (bvult v2 v4) + (bvult v3 v4) + (bvult v0 v1) + (bvult v1 v2) + (bvult v1 v3) + (bvult v4 v5) + (bvult v5 v1) + )) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/inequality01.smt2 b/test/regress/regress0/bv/inequality01.smt2 new file mode 100644 index 000000000..73a2515df --- /dev/null +++ b/test/regress/regress0/bv/inequality01.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v0 () (_ BitVec 16)) +(declare-fun v1 () (_ BitVec 16)) +(declare-fun v2 () (_ BitVec 16)) +(declare-fun v3 () (_ BitVec 16)) +(declare-fun v4 () (_ BitVec 16)) +(declare-fun v5 () (_ BitVec 16)) +(assert (and + (bvult v0 v1) + (bvult v1 v2) + (bvult v1 v3) + (bvult v2 v4) + (bvult v3 v4) + (bvult v4 v5) + (bvult (_ bv2 16) v2) + (bvult (_ bv5 16) v3) + )) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/inequality02.smt2 b/test/regress/regress0/bv/inequality02.smt2 new file mode 100644 index 000000000..05f11311f --- /dev/null +++ b/test/regress/regress0/bv/inequality02.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v0 () (_ BitVec 16)) +(declare-fun v1 () (_ BitVec 16)) +(declare-fun v2 () (_ BitVec 16)) +(declare-fun v3 () (_ BitVec 16)) +(declare-fun v4 () (_ BitVec 16)) +(declare-fun v5 () (_ BitVec 16)) +(assert (and + (bvult v0 v1) + (bvult (_ bv5 16) v3) + (bvult v1 v2) + (bvult v1 v3) + (bvult v5 (_ bv8 16)) + (bvult v2 v4) + (bvult v3 v4) + (bvult v4 v5) + )) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/inequality03.smt2 b/test/regress/regress0/bv/inequality03.smt2 new file mode 100644 index 000000000..a47551d14 --- /dev/null +++ b/test/regress/regress0/bv/inequality03.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v0 () (_ BitVec 16)) +(assert (and + (bvult v0 (_ bv3 16)) + (bvult (_ bv2 16) v0))) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/inequality04.smt2 b/test/regress/regress0/bv/inequality04.smt2 new file mode 100644 index 000000000..35607eaef --- /dev/null +++ b/test/regress/regress0/bv/inequality04.smt2 @@ -0,0 +1,19 @@ +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v0 () (_ BitVec 16)) +(declare-fun v1 () (_ BitVec 16)) +(declare-fun v2 () (_ BitVec 16)) +(declare-fun v3 () (_ BitVec 16)) +(declare-fun v4 () (_ BitVec 16)) +(declare-fun v5 () (_ BitVec 16)) +(assert (and + (bvule v0 v1) + (bvule v1 v2) + (bvule v2 v0) + (bvult (_ bv4 16) v0) + (bvult v2 (_ bv5 16)) + )) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/inequality05.smt2 b/test/regress/regress0/bv/inequality05.smt2 new file mode 100644 index 000000000..d8cf9cf99 --- /dev/null +++ b/test/regress/regress0/bv/inequality05.smt2 @@ -0,0 +1,28 @@ +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v0 () (_ BitVec 16)) +(declare-fun v1 () (_ BitVec 16)) +(declare-fun v2 () (_ BitVec 16)) +(declare-fun v3 () (_ BitVec 16)) +(declare-fun v4 () (_ BitVec 16)) +(declare-fun v5 () (_ BitVec 16)) +(declare-fun v6 () (_ BitVec 16)) +(declare-fun v7 () (_ BitVec 16)) +(declare-fun v8 () (_ BitVec 16)) +(declare-fun v9 () (_ BitVec 16)) +(assert (and +(bvult v6 v5) +(bvule v7 v8) +(bvugt v7 v1) +(bvuge v4 v1) +(bvuge v8 v0) +(bvugt v1 v0) +(bvuge v1 (_ bv60094 16)) +(bvule v3 v0) +(bvuge (_ bv47327 16) v6) +(bvugt v3 v6) +)) +(check-sat) +(exit)
\ No newline at end of file |