diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-21 11:15:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-21 11:15:39 -0500 |
| commit | d557a478c4643fc0bfd8c578db59803224c85b43 (patch) | |
| tree | 9e7cef12364813c561a6928756233225a4c373c9 /test/regress | |
| parent | 45a546f63d40d8ef0e0fac53854930836da2c0ea (diff) | |
Support uninterpreted constants in the evaluator (#4777)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/eval-uc.sy | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4e79b5dbe..8118d8d79 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1910,6 +1910,7 @@ set(regress_1_tests regress1/sygus/dt-test-ns.sy regress1/sygus/dup-op.sy regress1/sygus/error1-dt.sy + regress1/sygus/eval-uc.sy regress1/sygus/extract.sy regress1/sygus/fast-enum-backtrack.sy regress1/sygus/fg_polynomial3.sy diff --git a/test/regress/regress1/sygus/eval-uc.sy b/test/regress/regress1/sygus/eval-uc.sy new file mode 100644 index 000000000..e2bf9d144 --- /dev/null +++ b/test/regress/regress1/sygus/eval-uc.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho +(set-logic ALL) +(declare-sort S 0) +(declare-var f Bool) +(declare-var u (-> S Bool)) +(declare-var new_f Bool) +(declare-var new_u (-> S Bool)) +(define-fun init ((f Bool) (u (-> S Bool))) Bool (and f (forall ((x S)) (not (u x))))) +(define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and (not new_f) (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x))))))) +;(define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and new_f (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x))))))) +(synth-fun inv_matrix ((f Bool) (u (-> S Bool)) (x S)) Bool ((Start Bool)) ((Start Bool ( (or (not +(u x)) (not f)))))) +(define-fun inv ((f Bool) (u (-> S Bool))) Bool (forall ((x S)) (inv_matrix f u x))) +(constraint (=> (and (inv f u) (trans f u new_f new_u)) (inv new_f new_u))) +(check-synth) |