From: lianah Date: Wed, 27 Mar 2013 19:10:57 +0000 (-0400) Subject: fixed inequality checkDisequalities inefficiency X-Git-Tag: cvc5-1.0.0~7361^2~8 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f2335d2b64dc0c7e521aea6ea29088b8de7a3ca0;p=cvc5.git fixed inequality checkDisequalities inefficiency --- diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index 6d2ed0cf6..499d362a9 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -330,7 +330,7 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) { d_disequalities.push_back(reason); if (!isRegistered(a) || !isRegistered(b)) { - splitDisequality(reason); + //splitDisequality(reason); return true; } TermId id_a = getTermId(a); @@ -371,7 +371,7 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) { return addInequality(b, a, true, explanation); } // if none of the terms are constants just add the lemma - splitDisequality(reason); + //splitDisequality(reason); } else { Debug("bv-inequality-internal") << "Disequal: " << a << " => " << val_a.toString(10) << "\n" << " " << b << " => " << val_b.toString(10) << "\n"; @@ -379,30 +379,13 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) { 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::getNewLemmas(std::vector& new_lemmas) { - for (unsigned i = d_diseqToSplitIndex; i < d_disequalitiesToSplit.size(); ++i) { - TNode diseq = d_disequalitiesToSplit[i]; - if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) { - 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); - new_lemmas.push_back(lemma); - d_disequalitiesAlreadySplit.insert(diseq); - } - d_diseqToSplitIndex = d_diseqToSplitIndex + 1; - } -} +// 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"; @@ -425,7 +408,18 @@ void InequalityGraph::backtrack() { } } -void InequalityGraph::checkDisequalities() { +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& lemmas) { for (CDQueue::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 @@ -433,8 +427,8 @@ void InequalityGraph::checkDisequalities() { TermId a_id = registerTerm(diseq[0][0]); TermId b_id = registerTerm(diseq[0][1]); if (getValue(a_id) == getValue(b_id)) { - // if the disequality is not satisified by the model - d_disequalitiesToSplit.push_back(diseq); + lemmas.push_back(makeDiseqSplitLemma(diseq)); + d_disequalitiesAlreadySplit.insert(diseq); } } } diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 860302aa4..d402b1561 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -190,7 +190,7 @@ class InequalityGraph : public context::ContextNotifyObj{ * @param explanation */ void computeExplanation(TermId from, TermId to, std::vector& explanation); - void splitDisequality(TNode diseq); + // void splitDisequality(TNode diseq); /** Disequality reasoning @@ -198,11 +198,8 @@ class InequalityGraph : public context::ContextNotifyObj{ /*** The currently asserted disequalities */ context::CDQueue d_disequalities; - context::CDQueue d_disequalitiesToSplit; - context::CDO d_diseqToSplitIndex; - TNodeSet d_lemmasAdded; - TNodeSet d_disequalitiesAlreadySplit; - + NodeSet d_disequalitiesAlreadySplit; + Node makeDiseqSplitLemma(TNode diseq); /** Backtracking mechanisms **/ std::vector > d_undoStack; context::CDO d_undoStackIndex; @@ -225,8 +222,6 @@ public: d_signed(s), d_modelValues(c), d_disequalities(c), - d_disequalitiesToSplit(c), - d_diseqToSplitIndex(c, 0), d_disequalitiesAlreadySplit(), d_undoStack(), d_undoStackIndex(c) @@ -254,18 +249,11 @@ public: bool addDisequality(TNode a, TNode b, TNode reason); void getConflict(std::vector& conflict); virtual ~InequalityGraph() throw(AssertionException) {} - /** - * Get any new lemmas (resulting from disequalities splits) that need - * to be added. - * - * @param new_lemmas - */ - void getNewLemmas(std::vector& new_lemmas); /** * Check that the currently asserted disequalities that have not been split on * are still true in the current model. */ - void checkDisequalities(); + void checkDisequalities(std::vector& lemmas); /** * Return true if a < b is entailed by the current set of assertions. * diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 5504dbc11..17ac8a2e5 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -83,13 +83,11 @@ bool InequalitySolver::check(Theory::Effort e) { return false; } - // make sure all the disequalities we didn't split on are still satisifed - // and split on the ones that are not - d_inequalityGraph.checkDisequalities(); - if (isComplete()) { - // if we are complete we want to send out any inequality lemmas + 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 lemmas; - d_inequalityGraph.getNewLemmas(lemmas); + d_inequalityGraph.checkDisequalities(lemmas); for(unsigned i = 0; i < lemmas.size(); ++i) { d_bv->lemma(lemmas[i]); }