diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-05 14:38:16 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-05 14:38:16 -0600 |
commit | d26ee67911fedfef966a0e4d64ffda02007d65a0 (patch) | |
tree | d8d5511eeb12ecace73845785546df95e8f67f1f /src/preprocessing | |
parent | 04039407e6308070c148de0d5e93640ec1b0a341 (diff) |
Fix issues with real to int (#3918)
This fixes a few issues in the real to int preprocessing pass. Previously it was not robust to cases where the input had constraints that were not over the reals.
Fixes #3915 and fixes #3913 and fixes #3916.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/real_to_int.cpp | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index ca47e3ea0..dba7ccbe3 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -38,13 +38,13 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va } else { + NodeManager* nm = NodeManager::currentNM(); Node ret = n; if (n.getNumChildren() > 0) { - if (n.getKind() == kind::EQUAL || n.getKind() == kind::GEQ - || n.getKind() == kind::LT - || n.getKind() == kind::GT - || n.getKind() == kind::LEQ) + if ((n.getKind() == kind::EQUAL && n[0].getType().isReal()) + || n.getKind() == kind::GEQ || n.getKind() == kind::LT + || n.getKind() == kind::GT || n.getKind() == kind::LEQ) { ret = Rewriter::rewrite(n); Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl; @@ -137,11 +137,6 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va Trace("real-as-int") << " " << n << std::endl; Trace("real-as-int") << " " << ret << std::endl; } - else - { - throw TypeCheckingException( - n.toExpr(), string("Cannot translate to Int: ") + n.toString()); - } } } else @@ -162,14 +157,19 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va } else { - if (n.isVar()) + TypeNode tn = n.getType(); + if (tn.isReal() && !tn.isInteger()) { - if (!n.getType().isInteger()) + if (n.getKind() == kind::BOUND_VARIABLE) + { + // special case for bound variables (must call mkBoundVar) + ret = nm->mkBoundVar(nm->integerType()); + } + else if (n.isVar()) { - ret = NodeManager::currentNM()->mkSkolem( - "__realToIntInternal_var", - NodeManager::currentNM()->integerType(), - "Variable introduced in realToIntInternal pass"); + ret = nm->mkSkolem("__realToIntInternal_var", + nm->integerType(), + "Variable introduced in realToIntInternal pass"); var_eq.push_back(n.eqNode(ret)); TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel(); m->addSubstitution(n, ret); |