From d26ee67911fedfef966a0e4d64ffda02007d65a0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Mar 2020 14:38:16 -0600 Subject: 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. --- src/preprocessing/passes/real_to_int.cpp | 30 ++++++++++---------- test/regress/CMakeLists.txt | 2 ++ .../regress0/push-pop/issue3915-real-as-int.smt2 | 33 ++++++++++++++++++++++ .../regress1/quantifiers/real-to-int-quant.smt2 | 6 ++++ 4 files changed, 56 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress0/push-pop/issue3915-real-as-int.smt2 create mode 100644 test/regress/regress1/quantifiers/real-to-int-quant.smt2 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& 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& 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& 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); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 34f7a8713..a7d931246 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -682,6 +682,7 @@ set(regress_0_tests regress0/push-pop/incremental-subst-bug.cvc regress0/push-pop/issue1986.smt2 regress0/push-pop/issue2137.min.smt2 + regress0/push-pop/issue3915-real-as-int.smt2 regress0/push-pop/quant-fun-proc-unfd.smt2 regress0/push-pop/simple_unsat_cores.smt2 regress0/push-pop/test.00.cvc @@ -1508,6 +1509,7 @@ set(regress_1_tests regress1/quantifiers/qe.smt2 regress1/quantifiers/quant-wf-int-ind.smt2 regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 + regress1/quantifiers/real-to-int-quant.smt2 regress1/quantifiers/recfact.cvc regress1/quantifiers/rel-trigger-unusable.smt2 regress1/quantifiers/repair-const-nterm.smt2 diff --git a/test/regress/regress0/push-pop/issue3915-real-as-int.smt2 b/test/regress/regress0/push-pop/issue3915-real-as-int.smt2 new file mode 100644 index 000000000..ad6ba3b33 --- /dev/null +++ b/test/regress/regress0/push-pop/issue3915-real-as-int.smt2 @@ -0,0 +1,33 @@ +; COMMAND-LINE: --incremental --check-models --solve-real-as-int +; EXPECT: sat +(set-logic UFNIA) +(set-option :incremental true) +(set-option :check-models true) +(set-option :solve-real-as-int true) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const v4 Bool) +(declare-const v5 Bool) +(declare-const v6 Bool) +(declare-const v7 Bool) +(declare-const v8 Bool) +(declare-const v9 Bool) +(declare-const v10 Bool) +(declare-const v11 Bool) +(declare-const v12 Bool) +(declare-const v13 Bool) +(declare-const v14 Bool) +(declare-const i1 Int) +(assert (forall ((q0 Int) (q1 Int) (q2 Int) (q3 Bool)) (=> (= v7 q3 v7 q3 v0 q3 q3 q3 q3 v3) (> q0 59)))) +(push 1) +(declare-const v15 Bool) +(declare-sort S0 0) +(declare-sort S1 0) +(declare-const i2 Int) +(assert v13) +(push 1) +(declare-const S1-0 S1) +(assert (forall ((q4 Int)) (not (distinct q4 q4)))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/real-to-int-quant.smt2 b/test/regress/regress1/quantifiers/real-to-int-quant.smt2 new file mode 100644 index 000000000..5d7b8d44e --- /dev/null +++ b/test/regress/regress1/quantifiers/real-to-int-quant.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --solve-real-as-int +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(assert (forall ((x Real) (y Real)) (=> (< x y) (exists ((z Real)) (and (< x z) (< z (+ y 2)))))) ) +(check-sat) -- cgit v1.2.3