From 8ab10e0a4663e54d64c19869cf36bbaa059516ad Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 26 Mar 2013 23:34:25 -0400 Subject: [PATCH] inequality solver now only splits on disequalities when complete --- src/theory/bv/bv_subtheory_core.cpp | 8 ++++++-- 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 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 lemmas; + d_inequalityGraph.getNewLemmas(lemmas); + for(unsigned i = 0; i < lemmas.size(); ++i) { + d_bv->lemma(lemmas[i]); + } } return true; } -- 2.30.2