diff options
author | lianah <lianahady@gmail.com> | 2013-03-26 23:34:25 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-26 23:34:25 -0400 |
commit | 8ab10e0a4663e54d64c19869cf36bbaa059516ad (patch) | |
tree | 851de5c7373acdc16097a4c86cc4d572c3b0a35a | |
parent | 2bed73156740d7e93e303b02319c407a1d587109 (diff) |
inequality solver now only splits on disequalities when complete
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 13 |
2 files changed, 13 insertions, 8 deletions
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 15720885d..811e9a200 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -403,8 +403,12 @@ void CoreSolver::collectModelInfo(TheoryModel* m) { Node CoreSolver::getModelValue(TNode var) { Assert (isComplete()); - Assert (d_modelValues.find(var) != d_modelValues.end()); - return d_modelValues[d_equalityEngine.getRepresentative(var)]; + TNode repr = d_equalityEngine.getRepresentative(var); + if (repr.getKind() == kind::CONST_BITVECTOR) { + return repr; + } + Assert (d_modelValues.find(repr) != d_modelValues.end()); + return d_modelValues[repr]; } CoreSolver::Statistics::Statistics() diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 27047f6af..d6539f3ed 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -74,12 +74,13 @@ bool InequalitySolver::check(Theory::Effort e) { // make sure all the disequalities we didn't split on are still satisifed // and split on the ones that are not d_inequalityGraph.checkDisequalities(); - - // send out any lemmas - std::vector<Node> lemmas; - d_inequalityGraph.getNewLemmas(lemmas); - for(unsigned i = 0; i < lemmas.size(); ++i) { - d_bv->lemma(lemmas[i]); + if (isComplete()) { + // if we are complete we want to send out any inequality lemmas + std::vector<Node> lemmas; + d_inequalityGraph.getNewLemmas(lemmas); + for(unsigned i = 0; i < lemmas.size(); ++i) { + d_bv->lemma(lemmas[i]); + } } return true; } |