New algorithm for interpolation and abduction based on unsat cores (#3255)

4 files changed, 33 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0bcaa049a..787633178 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1682,8 +1682,10 @@ set(regress_1_tests
   regress1/strings/username_checker_min.smt2
   regress1/sygus-abduct-ex1-grammar.smt2
   regress1/sygus-abduct-test.smt2
+  regress1/sygus-abduct-test-ccore.smt2
   regress1/sygus-abduct-test-user.smt2
   regress1/sygus/VC22_a.sy
+  regress1/sygus/abd-simple-conj-4.smt2
   regress1/sygus/abv.sy
   regress1/sygus/array_search_5-Q-easy.sy
   regress1/sygus/bvudiv-by-2.sy
diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/sygus-abduct-test-ccore.smt2
new file mode 100644
index 000000000..86f5fe133
--- /dev/null
+++ b/test/regress/regress1/sygus-abduct-test-ccore.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-logic QF_UFLIRA)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+(get-abduct A (not (< x y)))
diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
index 4b7870c78..bb02ebce2 100644
--- a/test/regress/regress1/sygus-abduct-test-user.smt2
+++ b/test/regress/regress1/sygus-abduct-test-user.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --produce-abducts
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic QF_UFLIRA)
@@ -19,6 +20,8 @@
 (get-abduct A (not (< x y))
 
 ; the grammar for the abduct-to-synthesize
+; notice it does not permit the sygus-core-connective algorithm; this regression
+; tests that we ignore this option properly.
 ((Start Bool) (StartInt Int))
 (
 (Start Bool ((< StartInt StartInt)))
diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
new file mode 100644
index 000000000..98bf70fd7
--- /dev/null
+++ b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(declare-fun w () Int)
+(declare-fun u () Int)
+(declare-fun v () Int)
+(assert (>= x 0))
+(get-abduct A (>= (+ x y z w u v) 2))