From f52bee51e20b0670f9a2bd13ae2fdefd5eba1546 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Tue, 21 Feb 2012 19:43:46 +0000 Subject: [PATCH] Fix for bug303. The problem was with function applications that get normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced. Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future. --- src/theory/theory.h | 60 ++++++++++++++++++---------- src/theory/theory_engine.cpp | 27 +++++++++++++ src/theory/uf/equality_engine.h | 16 +++++++- src/theory/uf/equality_engine_impl.h | 17 ++++---- test/regress/regress0/Makefile.am | 3 +- test/regress/regress0/bug303.smt2 | 23 +++++++++++ 6 files changed, 116 insertions(+), 30 deletions(-) create mode 100644 test/regress/regress0/bug303.smt2 diff --git a/src/theory/theory.h b/src/theory/theory.h index af891e3a3..cf986a1f2 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -205,26 +205,6 @@ protected: return fact; } - /** - * Provides access to the facts queue, primarily intended for theory - * debugging purposes. - * - * @return the iterator to the beginning of the fact queue - */ - context::CDList::const_iterator facts_begin() const { - return d_facts.begin(); - } - - /** - * Provides access to the facts queue, primarily intended for theory - * debugging purposes. - * - * @return the iterator to the end of the fact queue - */ - context::CDList::const_iterator facts_end() const { - return d_facts.end(); - } - /** * The theory that owns the uninterpreted sort. */ @@ -605,6 +585,46 @@ public: return ss.str(); } + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the beginning of the fact queue + */ + context::CDList::const_iterator facts_begin() const { + return d_facts.begin(); + } + + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the end of the fact queue + */ + context::CDList::const_iterator facts_end() const { + return d_facts.end(); + } + + /** + * Provides access to the shared terms, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the beginning of the shared terms list + */ + context::CDList::const_iterator shared_terms_begin() const { + return d_sharedTerms.begin(); + } + + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the end of the shared terms list + */ + context::CDList::const_iterator shared_terms_end() const { + return d_sharedTerms.end(); + } + };/* class Theory */ std::ostream& operator<<(std::ostream& os, Theory::Effort level); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e21e83671..75c64654d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -133,6 +133,33 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl; + if (Debug.isOn("theory::assertions")) { + for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++ theoryId) { + Theory* theory = d_theoryTable[theoryId]; + if (theory && Theory::setContains((TheoryId)theoryId, d_activeTheories)) { + Debug("theory::assertions") << "--------------------------------------------" << std::endl; + Debug("theory::assertions") << "Assertions of " << theory->getId() << ": " << std::endl; + context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + if ((*it).isPreregistered) { + Debug("theory::assertions") << "[" << i << "]: "; + } else { + Debug("theory::assertions") << "(" << i << "): "; + } + Debug("theory::assertions") << (*it).assertion << endl; + } + + if (d_sharedTermsExist) { + Debug("theory::assertions") << "Shared terms of " << theory->getId() << ": " << std::endl; + context::CDList::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + Debug("theory::assertions") << "[" << i << "]: " << (*it) << endl; + } + } + } + } + } + // Do the checking CVC4_FOR_EACH_THEORY; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 29f932e04..41b39af97 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -311,8 +311,22 @@ private: /** A context-dependents count of nodes */ context::CDO d_nodesCount; + /** + * At time of addition a function application can already normalize to something, so + * we keep both the original, and the normalized version. + */ + struct FunctionApplicationPair { + FunctionApplication original; + FunctionApplication normalized; + FunctionApplicationPair() {} + FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized) + : original(original), normalized(normalized) {} + bool isNull() const { + return !original.isApplication(); + } + }; /** Map from ids to the applications */ - std::vector d_applications; + std::vector d_applications; /** Map from ids to the equality nodes */ std::vector d_equalityNodes; diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h index f30006cb9..02426c849 100644 --- a/src/theory/uf/equality_engine_impl.h +++ b/src/theory/uf/equality_engine_impl.h @@ -41,13 +41,14 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, E // Get another id for this EqualityNodeId funId = newNode(original, true); - // The function application we're creating + FunctionApplication funOriginal(t1, t2); + // The function application we're creating EqualityNodeId t1ClassId = getEqualityNode(t1).getFind(); EqualityNodeId t2ClassId = getEqualityNode(t2).getFind(); FunctionApplication funNormalized(t1ClassId, t2ClassId); - // We add the normalized version, the term needs to be re-added on each backtrack - d_applications[funId] = funNormalized; + // We add the original version + d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized); // Add the lookup data, if it's not already there typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); @@ -86,7 +87,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node, bool isApplicati // Add the node to it's position d_nodes.push_back(node); // Note if this is an application or not - d_applications.push_back(FunctionApplication()); + d_applications.push_back(FunctionApplicationPair()); // Add the trigger list for this node d_nodeTriggers.push_back(+null_trigger); // Add it to the equality graph @@ -294,7 +295,7 @@ void EqualityEngine::merge(EqualityNode& class1, EqualityNode& clas // Get the function application EqualityNodeId funId = useNode.getApplicationId(); Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl; - const FunctionApplication& fun = d_applications[useNode.getApplicationId()]; + const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; // Check if there is an application with find arguments EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); @@ -441,7 +442,7 @@ void EqualityEngine::backtrack() { Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl; d_nodeIds.erase(d_nodes[i]); - const FunctionApplication& app = d_applications[i]; + const FunctionApplication& app = d_applications[i].normalized; if (app.isApplication()) { // Remove b from use-list getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); @@ -593,8 +594,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNo if (reasonType == MERGED_THROUGH_CONGRUENCE) { // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2 Debug("equality") << "EqualityEngine::getExplanation(): due to congruence, going deeper" << std::endl; - const FunctionApplication& f1 = d_applications[currentNode]; - const FunctionApplication& f2 = d_applications[edgeNode]; + const FunctionApplication& f1 = d_applications[currentNode].original; + const FunctionApplication& f2 = d_applications[edgeNode].original; Debug("equality") << push; getExplanation(f1.a, f2.a, equalities); getExplanation(f1.b, f2.b, equalities); diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 0bc78e6c4..6947ea7c4 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -94,7 +94,8 @@ BUG_TESTS = \ bug187.smt2 \ bug220.smt2 \ bug239.smt \ - buggy-ite.smt2 + buggy-ite.smt2 \ + bug303.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug303.smt2 b/test/regress/regress0/bug303.smt2 new file mode 100644 index 000000000..bf603bc62 --- /dev/null +++ b/test/regress/regress0/bug303.smt2 @@ -0,0 +1,23 @@ +(set-logic QF_LIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(declare-fun one_cons (list) list) + +(assert (= (length (cons 1 nil)) (+ 1 (length nil)))) +(assert (= (one_cons nil) (cons 1 nil))) +(assert (not (= (length (one_cons nil)) 1))) + +(check-sat) + +(exit) -- 2.30.2