diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-25 16:39:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-25 21:39:02 +0000 |
| commit | cb748679157eb658ce5d1173d8f26957daf8f3df (patch) | |
| tree | 024859338fd336e43bba8b1775db5c0a9caeeca3 /test | |
| parent | 2aaa6ec1dfc3d7a41f120ef5361272b63363347b (diff) | |
Add new method for enumerating unsat queries with SyGuS (#7459)
This adds a new option for --sygus-query-gen=unsat to generate unsat queries (previously, only satisfiable queries were supported).
The algorithm can be seen as a variant of abduction where we conjoin predicates that both (1) refine the current model and (2) avoid repeated unsat cores.
It does some minor refactoring of ExprMinerManager to support the new module.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress2/sygus/qgu-bools.sy | 21 |
2 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 215f75e97..2cf9554e2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2638,6 +2638,7 @@ set(regress_2_tests regress2/sygus/pbe_bvurem.sy regress2/sygus/process-10-vars-2fun.sy regress2/sygus/process-arg-invariance.sy + regress2/sygus/qgu-bools.sy regress2/sygus/real-grammar-neg.sy regress2/sygus/sets-fun-test.sy regress2/sygus/sumn_recur_synth.sy diff --git a/test/regress/regress2/sygus/qgu-bools.sy b/test/regress/regress2/sygus/qgu-bools.sy new file mode 100644 index 000000000..35445e927 --- /dev/null +++ b/test/regress/regress2/sygus/qgu-bools.sy @@ -0,0 +1,21 @@ +; COMMAND-LINE: --sygus-query-gen=unsat --sygus-abort-size=2 +; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") +; SCRUBBER: grep -v -E '(\(define-fun|\(query)' +; EXIT: 1 +(set-logic ALL) +(synth-fun P ((a Bool) (b Bool) (c Bool)) Bool +((Start Bool)) +( +(Start Bool ( +a +b +c +(not Start) +(= Start Start) +(or Start Start) +(ite Start Start Start) +)) +)) + + +(check-synth) |