diff options
Diffstat (limited to 'src/theory/arith/nl_model.cpp')
-rw-r--r-- | src/theory/arith/nl_model.cpp | 43 |
1 files changed, 36 insertions, 7 deletions
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index 762e8b141..fe756e5f7 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl_model.h" #include "expr/node_algorithm.h" +#include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/rewriter.h" @@ -36,11 +37,18 @@ NlModel::NlModel(context::Context* c) : d_used_approx(false) NlModel::~NlModel() {} -void NlModel::reset(TheoryModel* m) +void NlModel::reset(TheoryModel* m, std::map<Node, Node>& arithModel) { d_model = m; d_mv[0].clear(); d_mv[1].clear(); + d_arithVal.clear(); + // process arithModel + std::map<Node, Node>::iterator it; + for (const std::pair<const Node, Node>& m : arithModel) + { + d_arithVal[m.first] = m.second; + } } void NlModel::resetCheck() @@ -127,21 +135,42 @@ Node NlModel::computeModelValue(Node n, bool isConcrete) return ret; } -Node NlModel::getValueInternal(Node n) const -{ - return d_model->getValue(n); -} - bool NlModel::hasTerm(Node n) const { - return d_model->hasTerm(n); + return d_arithVal.find(n) != d_arithVal.end(); } Node NlModel::getRepresentative(Node n) const { + if (n.isConst()) + { + return n; + } + std::map<Node, Node>::const_iterator it = d_arithVal.find(n); + if (it != d_arithVal.end()) + { + AlwaysAssert(it->second.isConst()); + return it->second; + } return d_model->getRepresentative(n); } +Node NlModel::getValueInternal(Node n) const +{ + if (n.isConst()) + { + return n; + } + std::map<Node, Node>::const_iterator it = d_arithVal.find(n); + if (it != d_arithVal.end()) + { + AlwaysAssert(it->second.isConst()); + return it->second; + } + // It is unconstrained in the model, return 0. + return d_zero; +} + int NlModel::compare(Node i, Node j, bool isConcrete, bool isAbsolute) { Node ci = computeModelValue(i, isConcrete); |