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 e06363883f52c4789d6fb5f43dec97e23ca104a4..867ac8a4a3306af879d7977ffc3b40939264b21c 100644 (file)
--- 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 10a1b6ba0b08f709894ed9333e354eaf31807698..0f1b090d4ec1bc79cff1c9abb2f47181646416e0 100644 (file)
--- 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 7609ad3e7deb0fa0bacb2f3c0825ba99fe692884..74ce8d32b13bdfba7af474e70eb948021a6cca64 100644 (file)
--- 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 (file)
index 0000000..abe5b09
--- /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)