diff options
author | lianah <lianahady@gmail.com> | 2013-03-26 15:36:47 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-26 15:36:47 -0400 |
commit | a15bf2140e45d76f98f0887be6461618c884589d (patch) | |
tree | 98bf9421e6b8cac0c14b5f61ee9eb2c7b23d65a1 /src/theory/bv/bv_inequality_graph.cpp | |
parent | e69531ce6cefe15dcc7afe9b79d2b36c778148fa (diff) |
fixed inequality bugs due to improper explanation
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.cpp')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.cpp | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index a1d2efbb5..3dfeba140 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -358,7 +358,17 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) { return addInequality(a, b, true, explanation); } if (b.getKind() == kind::CONST_BITVECTOR) { - return addInequality(b, a, true, reason); + // then we know b cannot be smaller than the assigned value so we try to make it larger + std::vector<ReasonId> explanation_ids; + computeExplanation(UndefinedTermId, id_a, explanation_ids); + std::vector<TNode> explanation_nodes; + explanation_nodes.push_back(reason); + for (unsigned i = 0; i < explanation_ids.size(); ++i) { + explanation_nodes.push_back(getReasonNode(explanation_ids[i])); + } + Node explanation = utils::mkAnd(explanation_nodes); + d_reasonSet.insert(explanation); + return addInequality(b, a, true, explanation); } // if none of the terms are constants just add the lemma splitDisequality(reason); @@ -410,8 +420,7 @@ void InequalityGraph::backtrack() { Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n"; } Assert (!edges.empty()); - InequalityEdge back = edges.back(); - Assert (back == edge); + Assert (edges.back() == edge); edges.pop_back(); } } |