From 8babd81adbf77eebdb7b1a6c87e605eb9168a46d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 Jan 2025 14:25:39 -0600 Subject: [PATCH] Make constant arrays require array-exp (#11534) --- src/smt/set_defaults.cpp | 1 + src/theory/arrays/theory_arrays.cpp | 2 +- test/regress/cli/regress0/arrays/issue4414.smt2 | 1 + test/regress/cli/regress0/arrays/issue5925-2.smt2 | 1 + test/regress/cli/regress0/arrays/issue5925.smt2 | 1 + test/regress/cli/regress0/parser/fp_value.smt2 | 1 + test/regress/cli/regress1/bug681.smt2 | 1 + test/regress/cli/regress1/constarr3.cvc.smt2 | 1 + test/regress/cli/regress1/constarr3.smt2 | 1 + test/regress/cli/regress1/sygus/array-uc.sy | 2 +- test/regress/cli/regress1/sygus/node-discrete.sy | 2 +- test/regress/cli/regress1/sygus/qf_abv.smt2 | 2 +- 12 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 63b969623ac..f231dcd34c6 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -153,6 +153,7 @@ void SetDefaults::setDefaultsPre(Options& opts) // these are disabled by default but are listed here in case they are // enabled by default later SET_AND_NOTIFY_IF_NOT_USER(fp, fpExp, false, "safe options"); + SET_AND_NOTIFY_IF_NOT_USER(arrays, arraysExp, false, "safe options"); SET_AND_NOTIFY_IF_NOT_USER(sets, setsExp, false, "safe options"); // specific options that are disabled OPTION_EXCEPTION_IF_NOT(arith, nlCov, false, "safe options"); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 1ecd29d70be..bee117383b2 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -301,7 +301,7 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector& lems) Kind k = term.getKind(); if (!options().arrays.arraysExp) { - if (k == Kind::EQ_RANGE) + if (k == Kind::EQ_RANGE || k == Kind::STORE_ALL) { std::stringstream ss; ss << "Term of kind `" << k diff --git a/test/regress/cli/regress0/arrays/issue4414.smt2 b/test/regress/cli/regress0/arrays/issue4414.smt2 index 757c14b918b..c46854e49ef 100644 --- a/test/regress/cli/regress0/arrays/issue4414.smt2 +++ b/test/regress/cli/regress0/arrays/issue4414.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --arrays-exp ; EXPECT: sat (set-logic QF_AUFLIA) (declare-const a (Array Int Int)) diff --git a/test/regress/cli/regress0/arrays/issue5925-2.smt2 b/test/regress/cli/regress0/arrays/issue5925-2.smt2 index 6beb2e9ba30..13d7b74972e 100644 --- a/test/regress/cli/regress0/arrays/issue5925-2.smt2 +++ b/test/regress/cli/regress0/arrays/issue5925-2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --arrays-exp (set-logic QF_A) (set-info :status unsat) (declare-const a (Array Bool Bool)) diff --git a/test/regress/cli/regress0/arrays/issue5925.smt2 b/test/regress/cli/regress0/arrays/issue5925.smt2 index de88c037ec3..77c58f12e06 100644 --- a/test/regress/cli/regress0/arrays/issue5925.smt2 +++ b/test/regress/cli/regress0/arrays/issue5925.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --arrays-exp (set-logic QF_ABV) (set-info :status unsat) (declare-const a (Array Bool Bool)) diff --git a/test/regress/cli/regress0/parser/fp_value.smt2 b/test/regress/cli/regress0/parser/fp_value.smt2 index 955ac5e28f5..b1a682625e1 100644 --- a/test/regress/cli/regress0/parser/fp_value.smt2 +++ b/test/regress/cli/regress0/parser/fp_value.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --arrays-exp (set-logic ALL) (set-info :status unsat) (set-option :fp-exp true) diff --git a/test/regress/cli/regress1/bug681.smt2 b/test/regress/cli/regress1/bug681.smt2 index 1d77cf270db..b6bf98d8723 100644 --- a/test/regress/cli/regress1/bug681.smt2 +++ b/test/regress/cli/regress1/bug681.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --arrays-exp ; EXIT: 1 ; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays") (set-logic ALL) diff --git a/test/regress/cli/regress1/constarr3.cvc.smt2 b/test/regress/cli/regress1/constarr3.cvc.smt2 index 30a68760822..0a0e84d538c 100644 --- a/test/regress/cli/regress1/constarr3.cvc.smt2 +++ b/test/regress/cli/regress1/constarr3.cvc.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --arrays-exp ; EXIT: 1 ; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays") (set-logic ALL) diff --git a/test/regress/cli/regress1/constarr3.smt2 b/test/regress/cli/regress1/constarr3.smt2 index d514fff7033..f48e0ed75bb 100644 --- a/test/regress/cli/regress1/constarr3.smt2 +++ b/test/regress/cli/regress1/constarr3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --arrays-exp ; EXIT: 1 ; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays") (set-logic QF_ALIA) diff --git a/test/regress/cli/regress1/sygus/array-uc.sy b/test/regress/cli/regress1/sygus/array-uc.sy index 1d43efede1d..93ec23030eb 100644 --- a/test/regress/cli/regress1/sygus/array-uc.sy +++ b/test/regress/cli/regress1/sygus/array-uc.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --arrays-exp ; EXPECT: feasible (set-logic ALL) (declare-sort U 0) diff --git a/test/regress/cli/regress1/sygus/node-discrete.sy b/test/regress/cli/regress1/sygus/node-discrete.sy index 4b84657da97..21cee040eb8 100644 --- a/test/regress/cli/regress1/sygus/node-discrete.sy +++ b/test/regress/cli/regress1/sygus/node-discrete.sy @@ -1,5 +1,5 @@ ; EXPECT: feasible -; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol --arrays-exp (set-logic ALL) (declare-datatype Packet ((P1) (P2))) diff --git a/test/regress/cli/regress1/sygus/qf_abv.smt2 b/test/regress/cli/regress1/sygus/qf_abv.smt2 index 8396976aa86..d4fb8b92040 100644 --- a/test/regress/cli/regress1/sygus/qf_abv.smt2 +++ b/test/regress/cli/regress1/sygus/qf_abv.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; COMMAND-LINE: --sygus-inference=try +; COMMAND-LINE: --sygus-inference=try --arrays-exp (set-info :smt-lib-version 2.6) (set-logic QF_ABV) (set-info :status sat)