Enable CDCAC solver for selected quantified logics (#7571)

This PR enables the CDCAC solver for quantified logics with reals, but no integers. Also, it disables SyGuS if no integers are used. The regression is a benchmark that is only solved with this new configuration.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index b701df173f395545551dbe9b7fcdfcd90e89a641..ee6aa28cfb30e265330c39e54edbbd8f7f13e675 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -186,7 +186,8 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
   }
   else if (!isSygus(opts) && logic.isQuantified()
            && (logic.isPure(THEORY_FP)
-               || (logic.isPure(THEORY_ARITH) && !logic.isLinear()))
+               || (logic.isPure(THEORY_ARITH) && !logic.isLinear()
+                   && logic.areIntegersUsed()))
            && !opts.base.incrementalSolving)
   {
     opts.quantifiers.sygusInst = true;
@@ -817,6 +818,18 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       }
     }
   }
+  else if (logic.isQuantified() && logic.isTheoryEnabled(theory::THEORY_ARITH)
+           && logic.areRealsUsed() && !logic.areIntegersUsed())
+  {
+    if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser)
+    {
+      opts.arith.nlCad = true;
+      if (!opts.arith.nlExtWasSetByUser)
+      {
+        opts.arith.nlExt = options::NlExtMode::LIGHT;
+      }
+    }
+  }
 #else
   if (opts.arith.nlCad)
   {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index da7c40bc22937504bc161622edf060d144d92b99..f97575808cfc9cd5b774028aeb6057a2be3fe11d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1790,6 +1790,7 @@ set(regress_1_tests
   regress1/nl/nl-help-unsat-quant.smt2
   regress1/nl/nl-unk-quant.smt2
   regress1/nl/nl_uf_lalt.smt2
+  regress1/nl/nra-cad-performance.smt2
   regress1/nl/ones.smt2
   regress1/nl/pinto-model-core-ni.smt2
   regress1/nl/poly-1025.smt2

diff --git a/test/regress/regress1/nl/nra-cad-performance.smt2 b/test/regress/regress1/nl/nra-cad-performance.smt2
new file mode 100644 (file)
index 0000000..5cf8357
--- /dev/null
+++ b/test/regress/regress1/nl/nra-cad-performance.smt2
@@ -0,0 +1,16 @@
+; Source: NRA/keymaera/ETCS-essentials-live-range2.proof-node1388.smt2
+; EXPECT: unsat
+; REQUIRES: poly
+(set-logic NRA)
+(set-info :status unsat)
+(declare-fun zuscore1dollarskuscore2 () Real)
+(declare-fun b () Real)
+(declare-fun Muscore0uscore0dollarmvuscore0 () Real)
+(declare-fun A () Real)
+(declare-fun puscore0dollarskuscore4 () Real)
+(declare-fun ep () Real)
+(declare-fun uscorenuscore0dollarskuscore2 () Real)
+(declare-fun vuscore1dollarskuscore2 () Real)
+(declare-fun vo () Real)
+(assert (not (exists ((Muscore0uscore0dollarmvuscore0 Real)) (=> (and (and (and (and (and (and (> uscorenuscore0dollarskuscore2 0) (>= (+ zuscore1dollarskuscore2 (* (* uscorenuscore0dollarskuscore2 ep) vo)) puscore0dollarskuscore4)) (= vuscore1dollarskuscore2 vo)) (> vo 0)) (> ep 0)) (> b 0)) (>= A 0)) (or (>= (- Muscore0uscore0dollarmvuscore0 zuscore1dollarskuscore2) (+ (/ (* vuscore1dollarskuscore2 vuscore1dollarskuscore2) (* 2 b)) (* (+ (/ A b) 1) (+ (* (/ A 2) (* ep ep)) (* ep vuscore1dollarskuscore2))))) (>= (+ (* (/ 1 2) (* 2 zuscore1dollarskuscore2)) (* (* (- uscorenuscore0dollarskuscore2 1) ep) vo)) puscore0dollarskuscore4))))))
+(check-sat)