From: Andrew Reynolds Date: Mon, 23 Jul 2018 18:36:53 +0000 (-0500) Subject: sygusComp2018: add regressions (#2191) X-Git-Tag: cvc5-1.0.0~4877 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=416f6d2d55fb24fea63bd13537b24a6a88509344;p=cvc5.git sygusComp2018: add regressions (#2191) --- diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index aa896258f..cef27bc72 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -814,6 +814,7 @@ REG0_TESTS = \ regress0/strings/type001.smt2 \ regress0/strings/unsound-0908.smt2 \ regress0/sygus/General_plus10.sy \ + regress0/sygus/aig-si.sy \ regress0/sygus/c100.sy \ regress0/sygus/ccp16.lus.sy \ regress0/sygus/check-generic-red.sy \ @@ -1502,6 +1503,8 @@ REG1_TESTS = \ regress1/sygus/constant.sy \ regress1/sygus/constant-ite-bv.sy \ regress1/sygus/crci-ssb-unk.sy \ + regress1/sygus/crcy-si-rcons.sy \ + regress1/sygus/crcy-si.sy \ regress1/sygus/dt-test-ns.sy \ regress1/sygus/dup-op.sy \ regress1/sygus/fg_polynomial3.sy \ @@ -1526,6 +1529,7 @@ REG1_TESTS = \ regress1/sygus/nia-max-square-ns.sy \ regress1/sygus/no-flat-simp.sy \ regress1/sygus/no-mention.sy \ + regress1/sygus/parity-si-rcons.sy \ regress1/sygus/pbe_multi.sy \ regress1/sygus/planning-unif.sy \ regress1/sygus/process-10-vars.sy \ @@ -1541,6 +1545,8 @@ REG1_TESTS = \ regress1/sygus/strings-trivial-two-type.sy \ regress1/sygus/strings-trivial.sy \ regress1/sygus/sygus-dt.sy \ + regress1/sygus/sygus-uf-ex.sy \ + regress1/sygus/t8.sy \ regress1/sygus/tl-type-0.sy \ regress1/sygus/tl-type-4x.sy \ regress1/sygus/tl-type.sy \ @@ -1549,6 +1555,7 @@ REG1_TESTS = \ regress1/sygus/twolets2-orig.sy \ regress1/sygus/unbdd_inv_gen_ex7.sy \ regress1/sygus/unbdd_inv_gen_winf1.sy \ + regress1/sygus/univ_2-long-repeat.sy \ regress1/sym/sym1.smt2 \ regress1/sym/sym2.smt2 \ regress1/sym/sym3.smt2 \ diff --git a/test/regress/regress0/sygus/aig-si.sy b/test/regress/regress0/sygus/aig-si.sy new file mode 100644 index 000000000..ef12e3c0e --- /dev/null +++ b/test/regress/regress0/sygus/aig-si.sy @@ -0,0 +1,30 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status +(set-logic BV) + +(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + (xor (not (xor a b)) (not (xor c d)))) + +(synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + ((Start Bool ((and Start Start) (not Start) a b c d)))) + +(declare-var a Bool) +(declare-var b Bool) +(declare-var c Bool) +(declare-var d Bool) + +(constraint + (= (parity a b c d) + (and (AIG a b c d) + (not (and (and (not (and a b)) (not (and (not a) (not b)))) + (and (not (and (not c) (not d))) (not (and c d)))))))) + + +(check-synth) + +; Solution: +;(define-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool +;(not +; (and +; (and (not (and (not a) b)) (not (and d (not c)))) +; (and (not (and (not b) a)) (not (and (not d) c)))))) diff --git a/test/regress/regress1/sygus/crcy-si-rcons.sy b/test/regress/regress1/sygus/crcy-si-rcons.sy new file mode 100644 index 000000000..6e2f54c31 --- /dev/null +++ b/test/regress/regress1/sygus/crcy-si-rcons.sy @@ -0,0 +1,78 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status + +(set-logic BV) + + +(define-fun origCir ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool) ) Bool + (not (not (not (xor (not (xor (not (and LN24 k3 ) ) LN129 ) ) LN141 ) ) ) ) +) + + +(synth-fun skel ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool) ) Bool + ((Start Bool ( + (and depth1 depth1) + (not depth1) + (or depth1 depth1) + (xor depth1 depth1) + )) + (depth1 Bool ( + (and depth2 depth2) + (not depth2) + (or depth2 depth2) + (xor depth2 depth2) + )) + (depth2 Bool ( + (and depth3 depth3) + (not depth3) + (or depth3 depth3) + (xor depth3 depth3) + )) + (depth3 Bool ( + (and depth4 depth4) + (not depth4) + (or depth4 depth4) + (xor depth4 depth4) + )) + (depth4 Bool ( + (and depth5 depth5) + (not depth5) + (or depth5 depth5) + (xor depth5 depth5) + LN141 + )) + (depth5 Bool ( + (and depth6 depth6) + (not depth6) + (or depth6 depth6) + (xor depth6 depth6) + )) + (depth6 Bool ( + (and depth7 depth7) + (not depth7) + (or depth7 depth7) + (xor depth7 depth7) + LN129 + )) + (depth7 Bool ( + (and depth8 depth8) + (not depth8) + (or depth8 depth8) + (xor depth8 depth8) + LN24 + )) + (depth8 Bool ( + k3 + ))) +) + + +(declare-var LN24 Bool) +(declare-var k3 Bool) +(declare-var LN129 Bool) +(declare-var LN141 Bool) + +(constraint (= (origCir LN24 k3 LN129 LN141 ) (skel LN24 k3 LN129 LN141 ))) + + +(check-synth) diff --git a/test/regress/regress1/sygus/crcy-si.sy b/test/regress/regress1/sygus/crcy-si.sy new file mode 100644 index 000000000..46500ee4d --- /dev/null +++ b/test/regress/regress1/sygus/crcy-si.sy @@ -0,0 +1,21 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic BV) + +(define-fun Spec ((k1 Bool) (k2 Bool) (k3 Bool) ) Bool + (xor k1 (and k3 (not k2))) +) + +(synth-fun Imp ((k1 Bool) (k2 Bool) (k3 Bool)) Bool + ((Start Bool ( (and d1 d1) (or d1 d1) (xor d1 d1) (not d1) ) ) + (d1 Bool ( (and d2 d2) (or d2 d2) (xor d2 d2) (not d2) ) ) + (d2 Bool ( k1 k2 k3) ) ) +) + +(declare-var k1 Bool) +(declare-var k2 Bool) +(declare-var k3 Bool) + +(constraint (= (Spec k1 k2 k3) (Imp k1 k2 k3))) +(check-synth) diff --git a/test/regress/regress1/sygus/parity-si-rcons.sy b/test/regress/regress1/sygus/parity-si-rcons.sy new file mode 100644 index 000000000..a836c9726 --- /dev/null +++ b/test/regress/regress1/sygus/parity-si-rcons.sy @@ -0,0 +1,36 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status + +(set-logic BV) + +(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + (xor (not (xor a b)) (not (xor c d)))) + +(synth-fun NAND ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + ((Start Bool ((not StartAnd) Vars Constants)) + (StartAnd Bool ((and Start Start))) + (Vars Bool (a b c d)) + (Constants Bool (true false)))) + +(declare-var a Bool) +(declare-var b Bool) +(declare-var c Bool) +(declare-var d Bool) + +(constraint + (= (parity a b c d) + (not (and (NAND a b c d) + (not + (and + (not (and (not (and d (not (and d a)))) (not (and a (not (and d a)))))) + (not (and (not (and (not (and true c)) (not (and true b)))) (not (and b c)))))))))) + + +(check-synth) + +; Solution: +;(define-fun NAND ((a Bool) (b Bool) (c Bool) (d Bool)) Bool +;(not +; (and +; (not (and (not (and (not (and c true)) b)) (not (and (not (and b c)) c)))) +; (not (and (not (and a d)) (not (and (not (and a true)) (not (and true d))))))))) diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy new file mode 100644 index 000000000..b9731de0f --- /dev/null +++ b/test/regress/regress1/sygus/sygus-uf-ex.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +(declare-fun uf ( Int ) Int) +(synth-fun f ((x Int) (y Int)) Bool +((Start Bool (true false + (<= IntExpr IntExpr ) + (= IntExpr IntExpr ) + (and Start Start ) + (or Start Start ) + (not Start ))) +(IntExpr Int (0 1 x y + (+ IntExpr IntExpr ) + (- IntExpr IntExpr ))))) +(declare-var x Int) +(constraint (f (uf x) (uf x))) +(constraint (not (f 3 4))) +(check-synth) diff --git a/test/regress/regress1/sygus/t8.sy b/test/regress/regress1/sygus/t8.sy new file mode 100644 index 000000000..4dd726875 --- /dev/null +++ b/test/regress/regress1/sygus/t8.sy @@ -0,0 +1,31 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +( +synth-fun f_143-17-143-55 ( (x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool + ((Start Bool ( +(< IntExpr IntExpr) +(and Start Start) +(= IntExpr IntExpr) +(not Start ) +(<= IntExpr IntExpr) +(or Start Start) + + + +)) +(IntExpr Int ( +x2 x1 parentNode EMPTY_PARENT +0 1 +)) + + ) +) +(declare-var x2_143-17-143-55 Int) +(declare-var x1_143-17-143-55 Int) +(declare-var parentNode_143-17-143-55 Int) +(declare-var EMPTY_PARENT_143-17-143-55 Int) + +(constraint (=> (and (= parentNode_143-17-143-55 0) (and (= EMPTY_PARENT_143-17-143-55 -1) (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)) ) ) (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55 ) true))) + +(check-synth) diff --git a/test/regress/regress1/sygus/univ_2-long-repeat.sy b/test/regress/regress1/sygus/univ_2-long-repeat.sy new file mode 100644 index 000000000..ac9493b2d --- /dev/null +++ b/test/regress/regress1/sygus/univ_2-long-repeat.sy @@ -0,0 +1,89 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-fair=direct --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((col1 String) (col2 String)) String + ((Start String (ntString)) + (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY" + (str.++ ntString ntString) + (str.replace ntString ntString ntString) + (str.at ntString ntInt) + (int.to.str ntInt) + (ite ntBool ntString ntString) + (str.substr ntString ntInt ntInt))) + (ntInt Int (0 1 2 + (+ ntInt ntInt) + (- ntInt ntInt) + (str.len ntString) + (str.to.int ntString) + (str.indexof ntString ntString ntInt))) + (ntBool Bool (true false + (str.prefixof ntString ntString) + (str.suffixof ntString ntString) + (str.contains ntString ntString))))) + + +(declare-var col1 String) +(declare-var col2 String) +(constraint (= (f "UC Berkeley" "Berkeley, CA") + "UC Berkeley, Berkeley, CA, USA")) +(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") + "University of Pennsylvania, Phialdelphia, PA, USA")) +(constraint (= (f "UCLA" "Los Angeles, CA") + "UCLA, Los Angeles, CA, USA")) +(constraint (= (f "Cornell University" "Ithaca, New York, USA") + "Cornell University, Ithaca, New York, USA")) +(constraint (= (f "Penn" "Philadelphia, PA, USA") + "Penn, Philadelphia, PA, USA")) +(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") + "University of Michigan, Ann Arbor, MI, USA")) +(constraint (= (f "UC Berkeley" "Berkeley, CA") + "UC Berkeley, Berkeley, CA, USA")) +(constraint (= (f "MIT" "Cambridge, MA") + "MIT, Cambridge, MA, USA")) +(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") + "University of Pennsylvania, Phialdelphia, PA, USA")) +(constraint (= (f "UCLA" "Los Angeles, CA") + "UCLA, Los Angeles, CA, USA")) +(constraint (= (f "University of Maryland College Park" "College Park, MD") + "University of Maryland College Park, College Park, MD, USA")) +(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") + "University of Michigan, Ann Arbor, MI, USA")) +(constraint (= (f "UC Berkeley" "Berkeley, CA") + "UC Berkeley, Berkeley, CA, USA")) +(constraint (= (f "MIT" "Cambridge, MA") + "MIT, Cambridge, MA, USA")) +(constraint (= (f "Rice University" "Houston, TX") + "Rice University, Houston, TX, USA")) +(constraint (= (f "Yale University" "New Haven, CT, USA") + "Yale University, New Haven, CT, USA")) +(constraint (= (f "Columbia University" "New York, NY, USA") + "Columbia University, New York, NY, USA")) +(constraint (= (f "NYU" "New York, New York, USA") + "NYU, New York, New York, USA")) +(constraint (= (f "Drexel University" "Philadelphia, PA") + "Drexel University, Philadelphia, PA, USA")) +(constraint (= (f "UC Berkeley" "Berkeley, CA") + "UC Berkeley, Berkeley, CA, USA")) +(constraint (= (f "UIUC" "Urbana, IL") + "UIUC, Urbana, IL, USA")) +(constraint (= (f "Temple University" "Philadelphia, PA") + "Temple University, Philadelphia, PA, USA")) +(constraint (= (f "Harvard University" "Cambridge, MA, USA") + "Harvard University, Cambridge, MA, USA")) +(constraint (= (f "University of Connecticut" "Storrs, CT, USA") + "University of Connecticut, Storrs, CT, USA")) +(constraint (= (f "Drexel University" "Philadelphia, PA") + "Drexel University, Philadelphia, PA, USA")) +(constraint (= (f "NYU" "New York, New York, USA") + "NYU, New York, New York, USA")) +(constraint (= (f "UIUC" "Urbana, IL") + "UIUC, Urbana, IL, USA")) +(constraint (= (f "New Haven University" "New Haven, CT, USA") + "New Haven University, New Haven, CT, USA")) +(constraint (= (f "University of California, Santa Barbara" "Santa Barbara, CA, USA") + "University of California, Santa Barbara, Santa Barbara, CA, USA")) +(constraint (= (f "University of Connecticut" "Storrs, CT, USA") + "University of Connecticut, Storrs, CT, USA")) + +(check-synth) diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy index 00340030f..a107fd88b 100644 --- a/test/regress/regress2/sygus/process-10-vars-2fun.sy +++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-repair-const ; EXPECT: unsat (set-logic LIA)