From 622865024f83cefee01f56271ba2dfae4984d0d0 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 4 Nov 2021 10:59:14 -0700
Subject: [PATCH] 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.
---
 src/smt/set_defaults.cpp                         | 15 ++++++++++++++-
 test/regress/CMakeLists.txt                      |  1 +
 .../regress/regress1/nl/nra-cad-performance.smt2 | 16 ++++++++++++++++
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress1/nl/nra-cad-performance.smt2

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)
-- 
2.30.2