Make constant arrays require array-exp (cvc5#11534)

ajreynol · Jan 22, 2025 · 8babd81 · 8babd81
1 parent 77d053a
commit 8babd81
Show file tree

Hide file tree

Showing 12 changed files with 12 additions and 4 deletions.
diff --git 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
@@ -301,7 +301,7 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)