From ec4a985f9b27740d0e84202bb7bcd5f5bdc8fb83 Mon Sep 17 00:00:00 2001 From: lianah Date: Wed, 27 Mar 2013 00:29:18 -0400 Subject: [PATCH] fixed model generation bug; commented out attempt at inequality propagation --- src/theory/bv/bv_subtheory_core.cpp | 2 +- src/theory/bv/bv_subtheory_inequality.cpp | 17 ++++++++++++++++- src/theory/bv/bv_subtheory_inequality.h | 2 ++ src/theory/bv/theory_bv.cpp | 1 + src/theory/bv/theory_bv.h | 2 ++ 5 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 811e9a200..c4f1b1b86 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -243,7 +243,7 @@ void CoreSolver::buildModel() { if (repr.getKind() == kind::CONST_BITVECTOR) { // must check if it's just the constant eq::EqClassIterator it(repr, &d_equalityEngine); - if (!(++it).isFinished()) { + if (!(++it).isFinished() || true) { constants.insert(repr); constants_in_eq_engine.insert(repr); } diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index d6539f3ed..9f7760608 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -49,6 +49,12 @@ bool InequalitySolver::check(Theory::Effort e) { 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]; @@ -57,6 +63,12 @@ bool InequalitySolver::check(Theory::Effort e) { 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]; @@ -147,7 +159,10 @@ bool InequalitySolver::isInequalityOnly(TNode node) { } void InequalitySolver::explain(TNode literal, std::vector& assumptions) { - Assert (false); + 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) { diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index b19ebb381..b02233b74 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -36,6 +36,7 @@ class InequalitySolver: public SubtheorySolver { context::CDHashSet d_assertionSet; InequalityGraph d_inequalityGraph; + context::CDHashMap d_explanations; context::CDO d_isComplete; __gnu_cxx::hash_map d_ineqTermCache; bool isInequalityOnly(TNode node); @@ -45,6 +46,7 @@ public: : SubtheorySolver(c, bv), d_assertionSet(c), d_inequalityGraph(c), + d_explanations(c), d_isComplete(c, true), d_ineqTermCache(), d_statistics() diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 8245fdbdc..502d49f58 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -275,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; } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 6bc4bdaf6..ff8b3a8b1 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -123,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); -- 2.30.2