Allow elimination of unevaluated terms by default (#8136)

Fixes #8118.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 842cf046f285dd216effc6fc469af2ff2b711ed4..71c3e8f37d985769701774b4fa95141cb14a2e27 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -72,6 +72,14 @@ name   = "SMT Layer"
   type       = "bool"
   help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions"
 
+[[option]]
+  name       = "modelVarElimUneval"
+  category   = "expert"
+  long       = "model-var-elim-uneval"
+  type       = "bool"
+  default    = "true"
+  help       = "allow variable elimination based on unevaluatable terms to variables"
+
 [[option]]
   name       = "modelCoresMode"
   category   = "regular"

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index bec5c7416d403295ec162f07fdd89ba47e5e6848..f826209b48ceddf6c7f1e965aa9197f965909425 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -339,9 +339,14 @@ bool Theory::isLegalElimination(TNode x, TNode val)
   {
     return false;
   }
-  if (!options().smt.produceModels && !logicInfo().isQuantified())
+  if (!options().smt.produceModels || options().smt.modelVarElimUneval)
   {
-    // Don't care about the model and logic is not quantified, we can eliminate.
+    // Don't care about the model, or we allow variables to be eliminated by
+    // unevaluatable terms, we can eliminate. Notice that when
+    // options().smt.modelVarElimUneval is true, val may contain unevaluatable
+    // kinds. This means that e.g. a Boolean variable may be eliminated based on
+    // an equality (= b (forall ((x)) (P x))), where its model value is (forall
+    // ((x)) (P x)).
     return true;
   }
   // If models are enabled, then it depends on whether the term contains any

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2e53419e49f33b40d05e2c9ffdc2c2d02ef5b994..4660005aacf0d8cfe0fd338e343baec0e5bdb6f1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1894,6 +1894,7 @@ set(regress_1_tests
   regress1/nl/issue7924-sqrt-partial.smt2
   regress1/nl/issue8016-iand-rewrite.smt2 
   regress1/nl/issue8052-iand-rewrite.smt2
+  regress1/nl/issue8118-elim-sin.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
   regress1/nl/metitarski_3_4_2e.smt2

diff --git a/test/regress/regress1/nl/issue8118-elim-sin.smt2 b/test/regress/regress1/nl/issue8118-elim-sin.smt2
new file mode 100644 (file)
index 0000000..47d820d
--- /dev/null
+++ b/test/regress/regress1/nl/issue8118-elim-sin.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-sort R 0)
+(declare-fun m (R R) Bool)
+(declare-fun e () R)
+(declare-fun t () R)
+(declare-fun v () Real)
+(declare-fun x () R)
+(assert (= (m x e) (distinct (m x t) (m x x))))
+(assert (= v (sin 1.0)))
+(check-sat)

diff --git a/test/regress/regress1/sets/arjun-set-univ.cvc.smt2 b/test/regress/regress1/sets/arjun-set-univ.cvc.smt2
index 8e851bb7fb56f75c15d13f043ffc9e247a0a77bb..b2051e3dd1ee3641090200e5470c7002ad26bc54 100644 (file)
--- a/test/regress/regress1/sets/arjun-set-univ.cvc.smt2
+++ b/test/regress/regress1/sets/arjun-set-univ.cvc.smt2
@@ -1,8 +1,7 @@
-; EXIT: 1
-; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
 (set-logic ALL)
 (set-option :incremental true)
 (set-option :produce-models true)
+(set-info :status sat)
 (declare-fun x () (Set Bool))
 (declare-fun y () (Set Bool))
 (declare-fun z () (Set Bool))
@@ -15,5 +14,3 @@
 (check-sat)
 
 (pop 1)
-
-(get-model)

diff --git a/test/regress/regress1/sets/univ-set-uf-elim.smt2 b/test/regress/regress1/sets/univ-set-uf-elim.smt2
index 548deca0507cdde8f53fa2417eaa6cc82f41b84f..7df8d05e484f56496f42c2296ad2086953ef721e 100644 (file)
--- a/test/regress/regress1/sets/univ-set-uf-elim.smt2
+++ b/test/regress/regress1/sets/univ-set-uf-elim.smt2
@@ -1,7 +1,6 @@
-; COMMAND-LINE: --produce-models
-; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
-; EXIT: 1
+; EXPECT: sat
 (set-logic ALL)
+(set-info :status sat)
 (declare-fun a () Int)
 (declare-fun f ((Set Bool)) Int)
 (declare-fun s () (Set Bool))