diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-11-04 10:59:14 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-04 17:59:14 +0000 |
| commit | 622865024f83cefee01f56271ba2dfae4984d0d0 (patch) | |
| tree | 22cb7434de40d4251b369fe4ea7ae015971f3392 /test/regress | |
| parent | aaf0877baf437395f915b8a12457a72b77fc39ce (diff) | |
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.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/nl/nra-cad-performance.smt2 | 16 |
2 files changed, 17 insertions, 0 deletions
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) |