From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 1 Jun 2020 17:14:56 +0000 (-0700)
Subject: Set theoryof-mode after theory widening (#4545)
X-Git-Tag: cvc5-1.0.0~3276
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a6c8c9a293eca7cd753368d7f23f9978deb2b2d5;p=cvc5.git

Set theoryof-mode after theory widening (#4545)

Fixes #4367. We set the theoryof-mode depending on whether sharing is
enabled or not. However, we were checking whether sharing was enabled
before theory widening, leading to unexpected results. This commit moves
the check after widening the theories.

For the benchmark in the issue, setting the theoryof-mode before theory
widening lead to problems because of the following:

The main solver checks the condition for enabling term-based
theoryof-mode, decides not to do it because sharing is not enabled
Main solver adds UF to the logic
Main solver does a check-sat all
Unsat core check runs, sees both UF and NRA enabled, and switches
to term-based mode
Main solver gets to second check-sat call, now the theoryof-mode is
suddenly changed, which leads to problems in the equality engine
This commit fixes the issue in this particular instance but it is important
to note that it does not address the issue of the subsolver changing
settings in general. This can only really be solved by separating the
options from the ExprManager/NodeManager and having separate
options for each SmtEngine/Solver instance.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index e06363883..867ac8a4a 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -538,18 +538,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     smte.setOption("produce-models", SExpr("true"));
   }
 
-  // Set the options for the theoryOf
-  if (!options::theoryOfMode.wasSetByUser())
-  {
-    if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
-        && !logic.isTheoryEnabled(THEORY_STRINGS)
-        && !logic.isTheoryEnabled(THEORY_SETS))
-    {
-      Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
-      options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
-    }
-  }
-
   /////////////////////////////////////////////////////////////////////////////
   // Theory widening
   //
@@ -609,6 +597,18 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   }
   /////////////////////////////////////////////////////////////////////////////
 
+  // Set the options for the theoryOf
+  if (!options::theoryOfMode.wasSetByUser())
+  {
+    if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
+        && !logic.isTheoryEnabled(THEORY_STRINGS)
+        && !logic.isTheoryEnabled(THEORY_SETS))
+    {
+      Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
+      options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
+    }
+  }
+
   // by default, symmetry breaker is on only for non-incremental QF_UF
   if (!options::ufSymmetryBreaker.wasSetByUser())
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 10a1b6ba0..0f1b090d4 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -37,6 +37,7 @@ set(regress_0_tests
   regress0/arith/issue3413.smt2
   regress0/arith/issue3480.smt2
   regress0/arith/issue3683.smt2
+  regress0/arith/issue4367.smt2
   regress0/arith/issue4525.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
diff --git a/test/regress/regress0/arith/issue3480.smt2 b/test/regress/regress0/arith/issue3480.smt2
index 7609ad3e7..74ce8d32b 100644
--- a/test/regress/regress0/arith/issue3480.smt2
+++ b/test/regress/regress0/arith/issue3480.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --quiet
+; COMMAND-LINE: --theoryof-mode=type --quiet
 (set-logic QF_NIA)
 (declare-fun a () Int)
 (declare-fun b () Int)
diff --git a/test/regress/regress0/arith/issue4367.smt2 b/test/regress/regress0/arith/issue4367.smt2
new file mode 100644
index 000000000..abe5b09fd
--- /dev/null
+++ b/test/regress/regress0/arith/issue4367.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --incremental --check-unsat-cores
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic NRA)
+(declare-const r0 Real)
+(assert (! (forall ((q0 Bool) (q1 Real)) (= (* r0 r0) r0 r0)) :named IP_2))
+(assert (! (not (forall ((q2 Real)) (not (<= 55.033442 r0 55.033442 q2)))) :named IP_5))
+(push 1)
+(check-sat)
+(pop 1)
+(check-sat)