diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-29 18:24:30 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-29 18:24:30 -0600 |
commit | 9f66cbe823294a5f64d07b512622c9590a286d9b (patch) | |
tree | c7f7f6585770130dd80a47e09d770a30b00ff29f /test | |
parent | 043de624d75615ae0f5b163e2effb44cac0885a3 (diff) |
Fix fast SyGuS enumeration for interpreted constants (#3501)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/once_2.sy | 44 |
2 files changed, 45 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e7252834e..e4b5b8057 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1736,6 +1736,7 @@ set(regress_1_tests regress1/sygus/nia-max-square-ns.sy regress1/sygus/no-flat-simp.sy regress1/sygus/no-mention.sy + regress1/sygus/once_2.sy regress1/sygus/only-const-grammar.sy regress1/sygus/parity-si-rcons.sy regress1/sygus/pbe_multi.sy diff --git a/test/regress/regress1/sygus/once_2.sy b/test/regress/regress1/sygus/once_2.sy new file mode 100644 index 000000000..af6d56aaf --- /dev/null +++ b/test/regress/regress1/sygus/once_2.sy @@ -0,0 +1,44 @@ +; EXPECT: unsat +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic BV) + +(define-sort Stream () (_ BitVec 2)) + +(define-fun BV_ONE () Stream (_ bv1 2)) + +(define-fun + O ( (X Stream) ) Stream + (bvneg (bvand X (bvnot (bvsub X BV_ONE)))) +) + +(synth-fun op ((x Stream)) Stream + (( y_term Stream)) + (( y_term Stream ( + ( Constant Stream) + ( Variable Stream) + ( bvnot y_term ) + ( bvand y_term y_term ) + ( bvor y_term y_term ) + ( bvneg y_term ) + ( bvadd y_term y_term ) + ( bvsub y_term y_term ) + ( bvmul y_term y_term ) + ( bvudiv y_term y_term ) + ( bvurem y_term y_term ) + ( bvshl y_term y_term ) + ( bvlshr y_term y_term ) + )) +)) + +(define-fun C ((x Stream)) Bool + (= (op x) (O x)) +) + +(constraint (and +(C (_ bv0 2)) +(C (_ bv1 2)) +(C (_ bv2 2)) +(C (_ bv3 2)) +)) + +(check-synth) |