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.

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)