diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-21 16:24:16 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-21 14:24:16 -0800 |
commit | 1e7ce9dcc5268c8e13466f63ac2c4159d71a583a (patch) | |
tree | e705a65b9957960a278382d9de70681aabae5594 /test/regress/regress0/sygus | |
parent | 3072a39f6bda5a5ce0dd538e0f1a1bd1b744d122 (diff) |
Quickly recognize when PBE conjectures are infeasible (#2718)
Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.
This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.
After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.
Diffstat (limited to 'test/regress/regress0/sygus')
-rw-r--r-- | test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy | 50 |
1 files changed, 50 insertions, 0 deletions
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) |