diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-29 13:58:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-29 13:58:09 -0500 |
commit | 90eddb069c3c9abf96719ac20aff45b44af86207 (patch) | |
tree | 5e9b48565fdcc33ecbc094ae5e14101e6e4ccb3c /test/regress/regress1/sygus-abduct-test-user.smt2 | |
parent | 3aba99657b39ccc0ab400c7ed9778673a3acddd7 (diff) |
Support get-abduct smt2 command (#3122)
Diffstat (limited to 'test/regress/regress1/sygus-abduct-test-user.smt2')
-rw-r--r-- | test/regress/regress1/sygus-abduct-test-user.smt2 | 28 |
1 files changed, 28 insertions, 0 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)) +) + +) |