From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 4 Nov 2021 17:59:14 +0000 (-0700)
Subject: Enable CDCAC solver for selected quantified logics (#7571)
X-Git-Tag: cvc5-1.0.0~893
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=622865024f83cefee01f56271ba2dfae4984d0d0;p=cvc5.git

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 b701df173..ee6aa28cf 100644
--- 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 da7c40bc2..f97575808 100644
--- 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
index 000000000..5cf835705
--- /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)