diff options
-rw-r--r-- | src/theory/arrays/array_info.cpp | 38 | ||||
-rw-r--r-- | src/theory/arrays/array_info.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 137 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 28 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 4 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 4 | ||||
-rw-r--r-- | src/theory/rewriter_attributes.h | 4 | ||||
-rw-r--r-- | src/theory/theory.h | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 18 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 18 | ||||
-rw-r--r-- | test/regress/regress0/arrays/bug272.minimized.smt (renamed from test/regress/regress0/arrays/unsound1.minimized.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress0/arrays/bug272.smt (renamed from test/regress/regress0/arrays/unsound1.smt) | 0 |
12 files changed, 139 insertions, 122 deletions
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index c795de0b9..5a836fdc2 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -34,20 +34,20 @@ bool inList(const CTNodeList* l, const TNode el) { void printList (CTNodeList* list) { CTNodeList::const_iterator it = list->begin(); - Debug("arrays-info")<<" [ "; + Trace("arrays-info")<<" [ "; for(; it != list->end(); it++ ) { - Debug("arrays-info")<<(*it)<<" "; + Trace("arrays-info")<<(*it)<<" "; } - Debug("arrays-info")<<"] \n"; + Trace("arrays-info")<<"] \n"; } void printList (List<TNode>* list) { List<TNode>::const_iterator it = list->begin(); - Debug("arrays-info")<<" [ "; + Trace("arrays-info")<<" [ "; for(; it != list->end(); it++ ) { - Debug("arrays-info")<<(*it)<<" "; + Trace("arrays-info")<<(*it)<<" "; } - Debug("arrays-info")<<"] \n"; + Trace("arrays-info")<<"] \n"; } void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{ @@ -67,7 +67,7 @@ void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{ void ArrayInfo::addIndex(const Node a, const TNode i) { Assert(a.getType().isArray()); Assert(!i.getType().isArray()); // temporary for flat arrays - Debug("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n"; + Trace("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n"; List<TNode>* temp_indices; Info* temp_info; @@ -84,7 +84,7 @@ void ArrayInfo::addIndex(const Node a, const TNode i) { temp_indices = (*it).second->indices; temp_indices->append(i); } - if(Debug.isOn("arrays-ind")) { + if(Trace.isOn("arrays-ind")) { printList((*(info_map.find(a))).second->indices); } @@ -115,7 +115,7 @@ void ArrayInfo::addStore(const Node a, const TNode st){ void ArrayInfo::addInStore(const TNode a, const TNode b){ - Debug("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n"; + Trace("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n"; Assert(a.getType().isArray()); Assert(b.getType().isArray()); @@ -182,20 +182,20 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){ TimerStat::CodeTimer codeTimer(d_mergeInfoTimer); ++d_callsMergeInfo; - Debug("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n"; - Debug("arrays-mergei")<<" and "<<b<<"\n"; + Trace("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n"; + Trace("arrays-mergei")<<" and "<<b<<"\n"; CNodeInfoMap::iterator ita = info_map.find(a); CNodeInfoMap::iterator itb = info_map.find(b); if(ita != info_map.end()) { - Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n"; - if(Debug.isOn("arrays-mergei")) + Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n"; + if(Trace.isOn("arrays-mergei")) (*ita).second->print(); if(itb != info_map.end()) { - Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n"; - if(Debug.isOn("arrays-mergei")) + Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n"; + if(Trace.isOn("arrays-mergei")) (*itb).second->print(); List<TNode>* lista_i = (*ita).second->indices; @@ -241,9 +241,9 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){ } } else { - Debug("arrays-mergei")<<" First element has no info \n"; + Trace("arrays-mergei")<<" First element has no info \n"; if(itb != info_map.end()) { - Debug("arrays-mergei")<<" adding second element's info \n"; + Trace("arrays-mergei")<<" adding second element's info \n"; (*itb).second->print(); List<TNode>* listb_i = (*itb).second->indices; @@ -258,11 +258,11 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){ info_map[a] = temp_info; } else { - Debug("arrays-mergei")<<" Second element has no info \n"; + Trace("arrays-mergei")<<" Second element has no info \n"; } } - Debug("arrays-mergei")<<"Arrays::mergeInfo done \n"; + Trace("arrays-mergei")<<"Arrays::mergeInfo done \n"; } diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 6eb20e30a..ce3f015b5 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -85,11 +85,11 @@ public: */ void print() const { Assert(indices != NULL && stores!= NULL); // && equals != NULL); - Debug("arrays-info")<<" indices "; + Trace("arrays-info")<<" indices "; printList(indices); - Debug("arrays-info")<<" stores "; + Trace("arrays-info")<<" stores "; printList(stores); - Debug("arrays-info")<<" in_stores "; + Trace("arrays-info")<<" in_stores "; printList(in_stores); } }; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index dab78c17a..888a98a45 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -76,7 +76,7 @@ TheoryArrays::~TheoryArrays() { void TheoryArrays::addSharedTerm(TNode t) { - Debug("arrays") << "Arrays::addSharedTerm(): " + Trace("arrays") << "Arrays::addSharedTerm(): " << t << endl; } @@ -85,7 +85,7 @@ void TheoryArrays::notifyEq(TNode lhs, TNode rhs) { } void TheoryArrays::notifyCongruent(TNode a, TNode b) { - Debug("arrays") << "Arrays::notifyCongruent(): " + Trace("arrays") << "Arrays::notifyCongruent(): " << a << " = " << b << endl; if(!d_conflict.isNull()) { return; @@ -103,10 +103,10 @@ void TheoryArrays::check(Effort e) { return; } - Debug("arrays") <<"Arrays::start check "; + Trace("arrays") <<"Arrays::start check "; while(!done()) { Node assertion = get(); - Debug("arrays") << "Arrays::check(): " << assertion << endl; + Trace("arrays") << "Arrays::check(): " << assertion << endl; switch(assertion.getKind()) { case kind::EQUAL: @@ -143,6 +143,7 @@ void TheoryArrays::check(Effort e) { } else if(find(a) == find(b)) { Node conflict = constructConflict(assertion[0]); + d_conflict = Node::null(); d_out->conflict(conflict, false); return; } @@ -162,10 +163,10 @@ void TheoryArrays::check(Effort e) { // generate the lemmas on the worklist //while(!d_RowQueue.empty() || ! d_extQueue.empty()) { dischargeLemmas(); - Debug("arrays-lem")<<"Arrays::discharged lemmas "<<d_RowQueue.size()<<"\n"; + Trace("arrays-lem")<<"Arrays::discharged lemmas "<<d_RowQueue.size()<<"\n"; //} } - Debug("arrays") << "Arrays::check(): done" << endl; + Trace("arrays") << "Arrays::check(): done" << endl; } Node TheoryArrays::getValue(TNode n) { @@ -390,7 +391,7 @@ Node TheoryArrays::preprocess(TNode atom) { void TheoryArrays::merge(TNode a, TNode b) { Assert(d_conflict.isNull()); - Debug("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl; + Trace("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl; /* * take care of the congruence closure part @@ -546,7 +547,7 @@ bool TheoryArrays::isNonLinear(TNode a) { } bool TheoryArrays::isAxiom(TNode t1, TNode t2) { - Debug("arrays-axiom")<<"Arrays::isAxiom start "<<t1<<" = "<<t2<<"\n"; + Trace("arrays-axiom")<<"Arrays::isAxiom start "<<t1<<" = "<<t2<<"\n"; if(t1.getKind() == kind::SELECT) { TNode a = t1[0]; TNode i = t1[1]; @@ -556,7 +557,7 @@ bool TheoryArrays::isAxiom(TNode t1, TNode t2) { TNode j = a[1]; TNode v = a[2]; if(i == j && v == t2) { - Debug("arrays-axiom")<<"Arrays::isAxiom true\n"; + Trace("arrays-axiom")<<"Arrays::isAxiom true\n"; return true; } } @@ -566,8 +567,8 @@ bool TheoryArrays::isAxiom(TNode t1, TNode t2) { Node TheoryArrays::constructConflict(TNode diseq) { - Debug("arrays") << "arrays: begin constructConflict()" << endl; - Debug("arrays") << "arrays: using diseq == " << diseq << endl; + Trace("arrays") << "arrays: begin constructConflict()" << endl; + Trace("arrays") << "arrays: using diseq == " << diseq << endl; // returns the reason the two terms are equal Node explanation = d_cc.explain(diseq[0], diseq[1]); @@ -594,7 +595,7 @@ Node TheoryArrays::constructConflict(TNode diseq) { nb<<diseq.notNode(); Node conflict = nb; - Debug("arrays") << "conflict constructed : " << conflict << endl; + Trace("arrays") << "conflict constructed : " << conflict << endl; return conflict; } @@ -665,7 +666,7 @@ void TheoryArrays::addDiseq(TNode diseq) { } void TheoryArrays::appendToDiseqList(TNode of, TNode eq) { - Debug("arrays") << "appending " << eq << endl + Trace("arrays") << "appending " << eq << endl << " to diseq list of " << of << endl; Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF); @@ -688,7 +689,6 @@ void TheoryArrays::appendToDiseqList(TNode of, TNode eq) { * Iterates through the indices of a and stores of b and checks if any new * Row lemmas need to be instantiated. */ - bool TheoryArrays::isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j) { Assert(a.getType().isArray()); Assert(b.getType().isArray()); @@ -707,61 +707,78 @@ bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) { Node bj = nm->mkNode(kind::SELECT, b, j); if(find(i) == find(j) || find(aj) == find(bj)) { - //Debug("arrays-lem")<<"isRedundantInContext valid "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n"; - checkRowForIndex(j,b); // why am i doing this? - checkRowForIndex(i,a); + Trace("arrays") << "isRedundantInContext valid " + << a << " " << b << " " << i << " " << j << endl; + checkRowForIndex(j, b); // why am i doing this? + checkRowForIndex(i, a); return true; } - Node literal1 = Rewriter::rewrite(i.eqNode(j)); + Trace("arrays") << "isRedundantInContext " << a << endl + << "isRedundantInContext " << b << endl + << "isRedundantInContext " << i << endl + << "isRedundantInContext " << j << endl; + Node ieqj = i.eqNode(j); + Node literal1 = Rewriter::rewrite(ieqj); bool hasValue1, satValue1; Node ff = nm->mkConst<bool>(false); Node tt = nm->mkConst<bool>(true); if (literal1 == ff) { hasValue1 = true; satValue1 = false; - } - else if (literal1 == tt) { + } else if (literal1 == tt) { hasValue1 = true; satValue1 = true; + } else { + hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1)); } - else hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1)); if (hasValue1) { - if (satValue1) return true; - Node literal2 = Rewriter::rewrite(aj.eqNode(bj)); + if (satValue1) { + Trace("arrays") << "isRedundantInContext returning, hasValue1 && satValue1" << endl; + return true; + } + Node ajeqbj = aj.eqNode(bj); + Node literal2 = Rewriter::rewrite(ajeqbj); bool hasValue2, satValue2; if (literal2 == ff) { hasValue2 = true; satValue2 = false; - } - else if (literal2 == tt) { + } else if (literal2 == tt) { hasValue2 = true; satValue2 = true; + } else { + hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2)); } - else hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2)); if (hasValue2) { - if (satValue2) return true; + if (satValue2) { + Trace("arrays") << "isRedundantInContext returning, hasValue2 && satValue2" << endl; + return true; + } // conflict Assert(!satValue1 && !satValue2); Assert(literal1.getKind() == kind::EQUAL && literal2.getKind() == kind::EQUAL); NodeBuilder<2> nb(kind::AND); - literal1 = areDisequal(literal1[0],literal1[1]); - literal2 = areDisequal(literal2[0],literal2[1]); + //literal1 = areDisequal(literal1[0], literal1[1]); + //literal2 = areDisequal(literal2[0], literal2[1]); Assert(!literal1.isNull() && !literal2.isNull()); nb << literal1.notNode() << literal2.notNode(); literal1 = nb; + d_conflict = Node::null(); d_out->conflict(literal1, false); + Trace("arrays") << "TheoryArrays::isRedundantInContext() " + << "conflict via lemma: " << literal1 << endl; return true; } } - if(alreadyAddedRow(a,b,i,j)) { - // Debug("arrays-lem")<<"isRedundantInContext already added "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n"; + if(alreadyAddedRow(a, b, i, j)) { + Trace("arrays") << "isRedundantInContext already added " + << a << " " << b << " " << i << " " << j << endl; return true; } return false; } TNode TheoryArrays::areDisequal(TNode a, TNode b) { - Debug("arrays-prop")<<"Arrays::areDisequal "<<a<<" "<<b<<"\n"; + Trace("arrays-prop") << "Arrays::areDisequal " << a << " " << b << "\n"; a = find(a); b = find(b); @@ -770,7 +787,7 @@ TNode TheoryArrays::areDisequal(TNode a, TNode b) { if(it!= d_disequalities.end()) { CTNodeListAlloc::const_iterator i = (*it).second->begin(); for( ; i!= (*it).second->end(); i++) { - Debug("arrays-prop")<<" "<<*i<<"\n"; + Trace("arrays-prop") << " " << *i << "\n"; TNode s = (*i)[0]; TNode t = (*i)[1]; @@ -791,12 +808,12 @@ TNode TheoryArrays::areDisequal(TNode a, TNode b) { } } - Debug("arrays-prop")<<" not disequal \n"; + Trace("arrays-prop") << " not disequal \n"; return TNode::null(); } bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { - Debug("arrays-prop")<<"Arrays::propagateFromRow "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n"; + Trace("arrays-prop")<<"Arrays::propagateFromRow "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n"; NodeManager* nm = NodeManager::currentNM(); Node aj = nm->mkNode(kind::SELECT, a, j); @@ -816,7 +833,7 @@ bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { // check if the current context implies that (NOT i = j) if(diseq != TNode::null()) { // if it's unassigned - Debug("arrays-prop")<<"satValue "<<d_valuation.getSatValue(eq_aj_bj).isNull(); + Trace("arrays-prop")<<"satValue "<<d_valuation.getSatValue(eq_aj_bj).isNull(); if(d_valuation.getSatValue(eq_aj_bj).isNull()) { d_out->propagate(eq_aj_bj); ++d_numProp; @@ -848,14 +865,14 @@ bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { } } - Debug("arrays-prop")<<"Arrays::propagateFromRow no prop \n"; + Trace("arrays-prop")<<"Arrays::propagateFromRow no prop \n"; return false; } void TheoryArrays::explain(TNode n) { - Debug("arrays")<<"Arrays::explain start for "<<n<<"\n"; + Trace("arrays")<<"Arrays::explain start for "<<n<<"\n"; ++d_numExplain; Assert(n.getKind()==kind::EQUAL); @@ -938,17 +955,17 @@ void TheoryArrays::explain(TNode n) { nb << diseq; Node reason = nb; d_out->explanation(reason); - Debug("arrays")<<"explanation "<< reason<<" done \n"; + Trace("arrays")<<"explanation "<< reason<<" done \n"; */ } void TheoryArrays::checkRowLemmas(TNode a, TNode b) { - Debug("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n"; - if(Debug.isOn("arrays-crl")) + Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n"; + if(Trace.isOn("arrays-crl")) d_infoMap.getInfo(a)->print(); - Debug("arrays-crl")<<" ------------ and "<<b<<"\n"; - if(Debug.isOn("arrays-crl")) + Trace("arrays-crl")<<" ------------ and "<<b<<"\n"; + if(Trace.isOn("arrays-crl")) d_infoMap.getInfo(b)->print(); List<TNode>* i_a = d_infoMap.getIndices(a); @@ -995,7 +1012,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) { } } - Debug("arrays-crl")<<"Arrays::checkLemmas done.\n"; + Trace("arrays-crl")<<"Arrays::checkLemmas done.\n"; } /** @@ -1018,7 +1035,7 @@ inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) { - Debug("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n"; + Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n"; d_RowAlreadyAdded.insert(make_quad(a,b,i,j)); d_out->lemma(lem); ++d_numRow; @@ -1032,10 +1049,10 @@ inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) { * store(a _ _ ) */ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { - Debug("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n"; - Debug("arrays-cri")<<" index "<<i<<"\n"; + Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n"; + Trace("arrays-cri")<<" index "<<i<<"\n"; - if(Debug.isOn("arrays-cri")) { + if(Trace.isOn("arrays-cri")) { d_infoMap.getInfo(a)->print(); } Assert(a.getType().isArray()); @@ -1048,9 +1065,9 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { TNode store = *it; Assert(store.getKind()==kind::STORE); TNode j = store[1]; - //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; + //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; if(!isRedundandRowLemma(store, store[0], j, i)) { - //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; + //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; queueRowLemma(store, store[0], j, i); } } @@ -1060,9 +1077,9 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { TNode instore = *it; Assert(instore.getKind()==kind::STORE); TNode j = instore[1]; - //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; + //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; if(!isRedundandRowLemma(instore, instore[0], j, i)) { - //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; + //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; queueRowLemma(instore, instore[0], j, i); } } @@ -1071,9 +1088,9 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { void TheoryArrays::checkStore(TNode a) { - Debug("arrays-cri")<<"Arrays::checkStore "<<a<<"\n"; + Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n"; - if(Debug.isOn("arrays-cri")) { + if(Trace.isOn("arrays-cri")) { d_infoMap.getInfo(a)->print(); } Assert(a.getType().isArray()); @@ -1088,7 +1105,7 @@ void TheoryArrays::checkStore(TNode a) { TNode j = *it; if(!isRedundandRowLemma(a, b, i, j)) { - //Debug("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; + //Trace("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; queueRowLemma(a,b,i,j); } } @@ -1116,8 +1133,8 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) { Assert(a.getType().isArray()); Assert(b.getType().isArray()); - Debug("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n"; - Debug("arrays-cle")<<" and "<<b<<" \n"; + Trace("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n"; + Trace("arrays-cle")<<" and "<<b<<" \n"; if( d_extAlreadyAdded.count(make_pair(a, b)) == 0 @@ -1131,13 +1148,13 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) { Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, ak, bk)); Node lem = nm->mkNode(kind::OR, eq, neq); - Debug("arrays-lem")<<"Arrays::addExtLemma "<<lem<<"\n"; + Trace("arrays-lem")<<"Arrays::addExtLemma "<<lem<<"\n"; d_extAlreadyAdded.insert(make_pair(a,b)); d_out->lemma(lem); ++d_numExt; return; } - Debug("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; + Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index f4cccfec5..cf822cb65 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -260,7 +260,7 @@ private: bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) { - //Debug("arrays-lem")<<"alreadyAddedRow check for "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n"; + //Trace("arrays-lem")<<"alreadyAddedRow check for "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n"; std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin(); a = find(a); b = find(b); @@ -274,7 +274,7 @@ private: TNode i_ = find((*it).third); TNode j_ = find((*it).fourth); if( a == a_ && b == b_ && i==i_ && j==j_) { - //Debug("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n"; + //Trace("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n"; return true; } } @@ -384,25 +384,25 @@ public: */ void preRegisterTerm(TNode n) { //TimerStat::CodeTimer codeTimer(d_preregisterTimer); - Debug("arrays-preregister")<<"Arrays::preRegisterTerm "<<n<<"\n"; + Trace("arrays-preregister")<<"Arrays::preRegisterTerm "<<n<<"\n"; //TODO: check non-linear arrays with an AlwaysAssert!!! //if(n.getType().isArray()) switch(n.getKind()) { case kind::EQUAL: // stores the seen atoms for propagation - Debug("arrays-preregister")<<"atom "<<n<<"\n"; + Trace("arrays-preregister")<<"atom "<<n<<"\n"; d_atoms.insert(n); // add to proper equality lists addEq(n); break; case kind::SELECT: - //Debug("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n"; + //Trace("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n"; d_infoMap.addIndex(n[0], n[1]); checkRowForIndex(n[1], find(n[0])); - //Debug("arrays-preregister")<<"n[0] \n"; + //Trace("arrays-preregister")<<"n[0] \n"; //d_infoMap.getInfo(n[0])->print(); - //Debug("arrays-preregister")<<"find(n[0]) \n"; + //Trace("arrays-preregister")<<"find(n[0]) \n"; //d_infoMap.getInfo(find(n[0]))->print(); break; @@ -428,16 +428,16 @@ public: break; } default: - Debug("darrays")<<"Arrays::preRegisterTerm non-array term. \n"; + Trace("darrays")<<"Arrays::preRegisterTerm non-array term. \n"; } } //void registerTerm(TNode n) { - // Debug("arrays-register")<<"Arrays::registerTerm "<<n<<"\n"; + // Trace("arrays-register")<<"Arrays::registerTerm "<<n<<"\n"; //} void presolve() { - Debug("arrays")<<"Presolving \n"; + Trace("arrays")<<"Presolving \n"; d_donePreregister = true; } @@ -447,7 +447,7 @@ public: void propagate(Effort e) { - Debug("arrays-prop")<<"Propagating \n"; + Trace("arrays-prop")<<"Propagating \n"; context::CDList<TNode>::const_iterator it = d_prop_queue.begin(); /* @@ -466,10 +466,10 @@ public: for(; it!= d_atoms.end(); it++) { TNode eq = *it; Assert(eq.getKind()==kind::EQUAL); - Debug("arrays-prop")<<"value of "<<eq<<" "; - Debug("arrays-prop")<<d_valuation.getSatValue(eq); + Trace("arrays-prop")<<"value of "<<eq<<" "; + Trace("arrays-prop")<<d_valuation.getSatValue(eq); if(find(eq[0]) == find(eq[1])) { - Debug("arrays-prop")<<" eq \n"; + Trace("arrays-prop")<<" eq \n"; ++d_numProp; } } diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 059b7ce8b..d7b37d8ba 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -33,7 +33,7 @@ class TheoryArraysRewriter { public: static RewriteResponse postRewrite(TNode node) { - Debug("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl; + Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl; switch (node.getKind()) { case kind::SELECT: { // select(store(a,i,v),i) = v @@ -85,7 +85,7 @@ public: } static inline RewriteResponse preRewrite(TNode node) { - Debug("arrays-prerewrite") << "Arrays::preRewrite " << node << std::endl; + Trace("arrays-prerewrite") << "Arrays::preRewrite " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); } diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index e896f9058..bb42a5ec7 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -64,7 +64,7 @@ Node Rewriter::rewrite(Node node) { Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { - Debug("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl; + Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl; // Put the node on the stack in order to start the "recursive" rewrite vector<RewriteStackElement> rewriteStack; @@ -76,7 +76,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Get the top of the recursion stack RewriteStackElement& rewriteStackTop = rewriteStack.back(); - Debug("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl; + Trace("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl; // Before rewriting children we need to do a pre-rewrite of the node if (rewriteStackTop.nextChild == 0) { diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index 86c2585b1..a2b2d06b7 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -51,7 +51,7 @@ struct RewriteAttibute { * Set the value of the pre-rewrite cache. */ static void setPreRewriteCache(TNode node, TNode cache) throw() { - Debug("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl; + Trace("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl; Assert(!cache.isNull()); if (node == cache) { node.setAttribute(pre_rewrite(), Node::null()); @@ -83,7 +83,7 @@ struct RewriteAttibute { */ static void setPostRewriteCache(TNode node, TNode cache) throw() { Assert(!cache.isNull()); - Debug("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl; + Trace("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl; if (node == cache) { node.setAttribute(post_rewrite(), Node::null()); } else { diff --git a/src/theory/theory.h b/src/theory/theory.h index 56a5f2f76..93d78f57c 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -140,7 +140,7 @@ protected: TNode fact = d_facts[d_factsHead]; d_wasSharedTermFact = false; d_factsHead = d_factsHead + 1; - Debug("theory") << "Theory::get() => " << fact + Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl; d_out->newFact(fact); return fact; @@ -312,7 +312,7 @@ public: * Assert a fact in the current context. */ void assertFact(TNode node) { - Debug("theory") << "Theory::assertFact(" << node << ")" << std::endl; + Trace("theory") << "Theory::assertFact(" << node << ")" << std::endl; d_facts.push_back(node); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3571171f8..28d7ab2c0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -73,7 +73,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { list<TNode> toReg; toReg.push_back(fact); - Debug("theory") << "Theory::get(): registering new atom" << endl; + Trace("theory") << "Theory::get(): registering new atom" << endl; /* Essentially this is doing a breadth-first numbering of * non-registered subterms with children. Any non-registered @@ -195,20 +195,20 @@ void TheoryEngine::preRegister(TNode preprocessed) { } else { Theory* theory = theoryOf(current); TheoryId theoryLHS = theory->getId(); - Debug("register") << "preregistering " << current + Trace("register") << "preregistering " << current << " with " << theoryLHS << std::endl; markActive(theoryLHS); theory->preRegisterTerm(current); } } else { TheoryId theory = theoryIdOf(current); - Debug("register") << "preregistering " << current + Trace("register") << "preregistering " << current << " with " << theory << std::endl; markActive(theory); d_theoryTable[theory]->preRegisterTerm(current); TheoryId typeTheory = theoryIdOf(current.getType()); if (theory != typeTheory) { - Debug("register") << "preregistering " << current + Trace("register") << "preregistering " << current << " with " << typeTheory << std::endl; markActive(typeTheory); d_theoryTable[typeTheory]->preRegisterTerm(current); @@ -254,7 +254,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) { try { CVC4_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { - Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; + Trace("theory") << "TheoryEngine::check() => conflict" << std::endl; } return true; @@ -315,7 +315,7 @@ bool TheoryEngine::presolve() { // Presolve for each theory using the statement above CVC4_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { - Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl; + Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl; } // return whether we have a conflict return !d_theoryOut.d_conflictNode.get().isNull(); @@ -374,9 +374,9 @@ bool TheoryEngine::hasRegisterTerm(TheoryId th) const { theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) { TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; - Debug("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl; + Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl; Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut); - Debug("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl; + Trace("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl; return solveStatus; } @@ -390,7 +390,7 @@ struct preprocess_stack_element { Node TheoryEngine::preprocess(TNode assertion) { - Debug("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl; + Trace("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl; // Do a topological sort of the subexpressions and substitute them vector<preprocess_stack_element> toVisit; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d4138f807..3507723f9 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -126,7 +126,7 @@ class TheoryEngine { void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::conflict(" + Trace("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; d_conflictNode = conflictNode; ++(d_engine->d_statistics.d_statConflicts); @@ -137,7 +137,7 @@ class TheoryEngine { void propagate(TNode lit, bool) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::propagate(" + Trace("theory") << "EngineOutputChannel::propagate(" << lit << ")" << std::endl; d_propagatedLiterals.push_back(lit); ++(d_engine->d_statistics.d_statPropagate); @@ -145,7 +145,7 @@ class TheoryEngine { void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::lemma(" + Trace("theory") << "EngineOutputChannel::lemma(" << node << ")" << std::endl; ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node); @@ -153,7 +153,7 @@ class TheoryEngine { void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::explanation(" + Trace("theory") << "EngineOutputChannel::explanation(" << explanationNode << ")" << std::endl; d_explanationNode = explanationNode; ++(d_engine->d_statistics.d_statExplanation); @@ -355,7 +355,7 @@ public: * @param node the assertion */ inline void assertFact(TNode node) { - Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; // Mark it as asserted in this context // @@ -369,16 +369,16 @@ public: // Again, equality is a special case if (atom.getKind() == kind::EQUAL) { if(d_logic == "QF_AX") { - Debug("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl; + Trace("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl; d_theoryTable[theory::THEORY_ARRAY]->assertFact(node); } else { theory::Theory* theory = theoryOf(atom); - Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl; + Trace("theory") << "asserting " << node << " to " << theory->getId() << std::endl; theory->assertFact(node); } } else { theory::Theory* theory = theoryOf(atom); - Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl; + Trace("theory") << "asserting " << node << " to " << theory->getId() << std::endl; theory->assertFact(node); } } @@ -443,7 +443,7 @@ public: TNode atom = node.getKind() == kind::NOT ? node[0] : node; if (atom.getKind() == kind::EQUAL) { if(d_logic == "QF_AX") { - Debug("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl; + Trace("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl; d_theoryTable[theory::THEORY_ARRAY]->explain(node); } else { theoryOf(atom[0])->explain(node); diff --git a/test/regress/regress0/arrays/unsound1.minimized.smt b/test/regress/regress0/arrays/bug272.minimized.smt index 360740310..360740310 100644 --- a/test/regress/regress0/arrays/unsound1.minimized.smt +++ b/test/regress/regress0/arrays/bug272.minimized.smt diff --git a/test/regress/regress0/arrays/unsound1.smt b/test/regress/regress0/arrays/bug272.smt index c7e779acd..c7e779acd 100644 --- a/test/regress/regress0/arrays/unsound1.smt +++ b/test/regress/regress0/arrays/bug272.smt |