From 55be526dfb5bafa3d27cc1dc5de9ee6d668eba94 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 23 Feb 2022 16:35:15 -0600
Subject: [PATCH] Allow elimination of unevaluated terms by default (#8136)

Fixes #8118.
---
 src/options/smt_options.toml                       |  8 ++++++++
 src/theory/theory.cpp                              |  9 +++++++--
 test/regress/CMakeLists.txt                        |  1 +
 test/regress/regress1/nl/issue8118-elim-sin.smt2   | 11 +++++++++++
 test/regress/regress1/sets/arjun-set-univ.cvc.smt2 |  5 +----
 test/regress/regress1/sets/univ-set-uf-elim.smt2   |  5 ++---
 6 files changed, 30 insertions(+), 9 deletions(-)
 create mode 100644 test/regress/regress1/nl/issue8118-elim-sin.smt2

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 842cf046f..71c3e8f37 100644
--- 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 bec5c7416..f826209b4 100644
--- 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 2e53419e4..4660005aa 100644
--- 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
index 000000000..47d820de8
--- /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 8e851bb7f..b2051e3dd 100644
--- 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 548deca05..7df8d05e4 100644
--- 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))
-- 
2.30.2