Support get-abduct smt2 command (#3122)

2 files changed, 30 insertions, 2 deletions

diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
new file mode 100644
index 000000000..bdb680613
--- /dev/null
+++ b/test/regress/regress1/sygus-abduct-test-user.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_UFLIRA)
+(set-option :produce-abducts true)
+(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)))
+
+; Generate a predicate A that is consistent with the above axioms (i.e.
+; their conjunction is SAT), and is such that the conjunction of the above
+; axioms, A and the conjecture below are UNSAT.
+; The signature of A is below grammar.
+(get-abduct A (< x y)
+
+; the grammar for the abduct-to-synthesize
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int (n m (+ StartInt StartInt) 0 1))
+)
+
+)
diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2
index 4ac90870c..d01f5f5ff 100644
--- a/test/regress/regress1/sygus-abduct-test.smt2
+++ b/test/regress/regress1/sygus-abduct-test.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-abduct --sygus-abort-size=2 
+; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=2
 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 1
@@ -13,4 +13,4 @@
 (assert (and (<= n x)(<= x (+ n 5))))
 (assert (and (<= 1 y)(<= y m)))
 
-(check-sat-assuming ((< x y)))
+(get-abduct A (< x y))