diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-09 19:13:22 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-10 01:13:22 +0000 |
commit | 9348602f05094b032efb33dfd341721b270380a1 (patch) | |
tree | eff83d5e5a691c5c3d0823515c0ee9003ea44a88 | |
parent | 68d6329d38af159afa7dc9542ef8e04e4d5a3773 (diff) |
Fix parsing array constants (#7617)
This generalizes a fix for parsing array constants.
Fixes #7596.
-rw-r--r-- | src/parser/smt2/smt2.cpp | 25 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 | 5 |
3 files changed, 28 insertions, 3 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ef784746c..1fc7a637f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1011,13 +1011,32 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) // resulting rational here. This also is applied for integral real values // like 5.0 which are converted to (/ 5 1) to distinguish them from // integer constants. We must ensure numerator and denominator are - // constant and the denominator is non-zero. - if (constVal.getKind() == api::DIVISION) + // constant and the denominator is non-zero. A similar issue happens for + // negative integers and reals, with unary minus. + bool isNeg = false; + if (constVal.getKind() == api::UMINUS) + { + isNeg = true; + constVal = constVal[0]; + } + if (constVal.getKind() == api::DIVISION + && constVal[0].getKind() == api::CONST_RATIONAL + && constVal[1].getKind() == api::CONST_RATIONAL) { std::stringstream sdiv; - sdiv << constVal[0] << "/" << constVal[1]; + sdiv << (isNeg ? "-" : "") << constVal[0] << "/" << constVal[1]; constVal = d_solver->mkReal(sdiv.str()); } + else if (constVal.getKind() == api::CONST_RATIONAL && isNeg) + { + std::stringstream sneg; + sneg << "-" << constVal; + constVal = d_solver->mkInteger(sneg.str()); + } + else + { + constVal = args[0]; + } if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort())) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b08b2f6f5..9574628a8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -109,6 +109,7 @@ set(regress_0_tests regress0/arrays/issue3813-massign-assert.smt2 regress0/arrays/issue3814.smt2 regress0/arrays/issue4927-unsat-cores.smt2 + regress0/arrays/issue7596-define-array-uminus.smt2 regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2 regress0/arrays/x2.smtv1.smt2 regress0/arrays/x3.smtv1.smt2 diff --git a/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 new file mode 100644 index 000000000..da21db28e --- /dev/null +++ b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status sat) +(define-fun foo () (Array Int Int) ((as const (Array Int Int)) (- 1))) +(assert (= (select foo 0) (- 1))) +(check-sat) |