diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-12 16:13:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-12 16:13:27 -0500 |
commit | dd84f87edba9b0cde271fe7000208c5f8f97b890 (patch) | |
tree | 4cb6f0c00a45250fa575d13f49c502ec01026b89 | |
parent | 920343a4a5586297dd98305b83785207025083b8 (diff) |
Do not allow quantifiers over real variables in real to int pass. (#4049)
With quantifiers over real variables, --solve-real-as-int is neither sound nor complete. Thus we should abort in this case.
-rw-r--r-- | src/preprocessing/passes/real_to_int.cpp | 10 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/issue3915-real-as-int.smt2 | 33 |
3 files changed, 7 insertions, 37 deletions
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index f50cecd1b..1c77f6f54 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -115,7 +115,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va { throw TypeCheckingException( v.toExpr(), - string("Cannot translate to Int: ") + v.toString()); + std::string("Cannot translate to Int: ") + v.toString()); } } } @@ -166,8 +166,12 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va { if (n.getKind() == kind::BOUND_VARIABLE) { - // special case for bound variables (must call mkBoundVar) - ret = nm->mkBoundVar(nm->integerType()); + // cannot change the type of quantified variables, since this leads + // to incompleteness. + throw TypeCheckingException( + n.toExpr(), + std::string("Cannot translate bound variable to Int: ") + + n.toString()); } else if (n.isVar()) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index de2091ef6..c23ed07ee 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -690,7 +690,6 @@ 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/real-as-int-incremental.smt2 regress0/push-pop/simple_unsat_cores.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 deleted file mode 100644 index ad6ba3b33..000000000 --- a/test/regress/regress0/push-pop/issue3915-real-as-int.smt2 +++ /dev/null @@ -1,33 +0,0 @@ -; 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)
|