diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-22 12:09:19 -0600 |
---|---|---|
committer | Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> | 2019-11-22 10:09:19 -0800 |
commit | eff8e6a30d348e2418f805602d3dd41ac2bc795b (patch) | |
tree | 40ca7a8abdba213302399713c029f446d54ba395 /src/theory/arith | |
parent | 6080c313c0a78323934f81a47623f17ee48c17cc (diff) |
Minor refactoring of compute model value for nl (#3489)
* Refactor compute model value for nl
* Format
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/nl_model.cpp | 51 |
1 files changed, 22 insertions, 29 deletions
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index 62bdf310b..762e8b141 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -73,31 +73,22 @@ Node NlModel::computeModelValue(Node n, bool isConcrete) Trace("nl-ext-mv-debug") << "computeModelValue " << n << ", index=" << index << std::endl; Node ret; + Kind nk = n.getKind(); if (n.isConst()) { ret = n; } - else if (index == 1 - && (n.getKind() == NONLINEAR_MULT - || isTranscendentalKind(n.getKind()))) + else if (!isConcrete && hasTerm(n)) { - if (hasTerm(n)) - { - // use model value for abstraction - ret = getRepresentative(n); - } - else - { - // abstraction does not exist, use model value - ret = getValueInternal(n); - } + // use model value for abstraction + ret = getRepresentative(n); } else if (n.getNumChildren() == 0) { - if (n.getKind() == PI) + // we are interested in the exact value of PI, which cannot be computed. + // hence, we return PI itself when asked for the concrete value. + if (nk == PI) { - // we are interested in the exact value of PI, which cannot be computed. - // hence, we return PI itself when asked for the concrete value. ret = n; } else @@ -108,23 +99,25 @@ Node NlModel::computeModelValue(Node n, bool isConcrete) else { // otherwise, compute true value - std::vector<Node> children; - if (n.getMetaKind() == metakind::PARAMETERIZED) - { - children.push_back(n.getOperator()); - } - for (unsigned i = 0; i < n.getNumChildren(); i++) + TheoryId ctid = theory::kindToTheoryId(nk); + if (ctid != THEORY_ARITH && ctid != THEORY_BOOL && ctid != THEORY_BUILTIN) { - Node mc = computeModelValue(n[i], isConcrete); - children.push_back(mc); - } - ret = NodeManager::currentNM()->mkNode(n.getKind(), children); - if (n.getKind() == APPLY_UF) - { - ret = getValueInternal(ret); + // we directly look up terms not belonging to arithmetic + ret = getValueInternal(n); } else { + std::vector<Node> children; + if (n.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(n.getOperator()); + } + for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + Node mc = computeModelValue(n[i], isConcrete); + children.push_back(mc); + } + ret = NodeManager::currentNM()->mkNode(nk, children); ret = Rewriter::rewrite(ret); } } |