diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-09 18:38:12 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-02-09 18:38:12 -0800 |
commit | a70490bc79933a55041f35d5896f79004e578f05 (patch) | |
tree | 3b89ea09cf7c653b293b86dd7431132de4676fe5 /src/theory/bv/bv_inequality_graph.cpp | |
parent | 13af27ec180e73eecc846c99bd563f85577683ee (diff) |
Remove mkNode from bv::utils (#1587)
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.cpp')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.cpp | 35 |
1 files changed, 21 insertions, 14 deletions
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index d0b299d3b..12d415cad 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -2,9 +2,9 @@ /*! \file bv_inequality_graph.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Paul Meng, Morgan Deters + ** Liana Hadarean, Aina Niemetz, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -415,15 +415,17 @@ void InequalityGraph::backtrack() { } } -Node InequalityGraph::makeDiseqSplitLemma(TNode diseq) { - Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL); +Node InequalityGraph::makeDiseqSplitLemma(TNode diseq) +{ + Assert(diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL); + NodeManager* nm = NodeManager::currentNM(); 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; + Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b); + Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a); + Node eq = diseq[0]; + Node lemma = nm->mkNode(kind::OR, a_lt_b, b_lt_a, eq); + return lemma; } void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) { @@ -460,14 +462,19 @@ BitVector InequalityGraph::getValueInModel(TNode node) const { return getValue(id); } -void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) { - for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { +void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) +{ + NodeManager* nm = NodeManager::currentNM(); + for (ModelValues::const_iterator it = d_modelValues.begin(); + it != d_modelValues.end(); + ++it) + { TermId id = (*it).first; BitVector value = (*it).second.value; TNode var = getTermNode(id); Node constant = utils::mkConst(value); - Node assignment = utils::mkNode(kind::EQUAL, var, constant); - assignments.push_back(assignment); - Debug("bitvector-model") << " " << var <<" => " << constant << "\n"; + Node assignment = nm->mkNode(kind::EQUAL, var, constant); + assignments.push_back(assignment); + Debug("bitvector-model") << " " << var << " => " << constant << "\n"; } } |