diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy | 50 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/array_search_2.sy | 3 |
3 files changed, 53 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a1d5a35aa..97b1fb99b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -861,6 +861,7 @@ set(regress_0_tests regress0/sygus/real-si-all.sy regress0/sygus/strings-unconstrained.sy regress0/sygus/uminus_one.sy + regress0/sygus/univ_3-long-repeat-conflict.sy regress0/test11.cvc regress0/test9.cvc regress0/tptp/ARI086=1.p diff --git a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy new file mode 100644 index 000000000..c2ed642be --- /dev/null +++ b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy @@ -0,0 +1,50 @@ +; EXPECT: unknown +; COMMAND-LINE: --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") + "Berkeley, CA, USA")) +(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") + "Phialdelphia, PA, USA")) +(constraint (= (f "UCLA" "Los Angeles, CA") + "UCLA, Los Angeles, CA, USA")) +(constraint (= (f "Cornell University" "Ithaca, New York, USA") + "Ithaca, New York, USA")) +(constraint (= (f "Penn" "Philadelphia, PA, USA") + "Philadelphia, PA, USA")) +(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") + "Ann Arbor, MI, USA")) +(constraint (= (f "UC Berkeley" "Berkeley, CA") + "Berkeley, CA, USA")) +(constraint (= (f "MIT" "Cambridge, MA") + "Cambridge, MA, USA")) +(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") + "Phialdelphia, PA, USA")) +(constraint (= (f "UCLA" "Los Angeles, CA") + "Los Angeles, CA, USA")) + +; has contradictory examples +(check-synth) diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy index 41346e655..93cbf9ce9 100644 --- a/test/regress/regress1/sygus/array_search_2.sy +++ b/test/regress/regress1/sygus/array_search_2.sy @@ -1,5 +1,6 @@ +; REQUIRES: proof ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof (set-logic LIA) (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) |