diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-01 09:07:42 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-01 09:07:42 -0600 |
commit | f40d813048599b58327fc968344301d39f156da2 (patch) | |
tree | 6441035d51eccca0156ed15d142ced27eb7187d4 /test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy | |
parent | 9f3ea3328213e08bf39b8ceeea272205255fd7ed (diff) |
Refactor and generalize PBE strategies (#1410)
Diffstat (limited to 'test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy')
-rw-r--r-- | test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy new file mode 100644 index 000000000..abcfc2217 --- /dev/null +++ b/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy @@ -0,0 +1,32 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status + +(set-logic BV) + +(define-fun hd19 ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) + (bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m)))) + +; bvand is a duplicate +(synth-fun f ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) + ((Start (BitVec 32) ((bvand Start Start) + (bvsub Start Start) + (bvxor Start Start) + (bvor Start Start) + (bvand Start Start) + (bvshl Start Start) + (bvlshr Start Start) + (bvashr Start Start) + (bvnot Start) + (bvneg Start) + x + m + k)))) + + +(declare-var x (BitVec 32)) +(declare-var m (BitVec 32)) +(declare-var k (BitVec 32)) + +(constraint (= (hd19 x m k) (f x m k))) +(check-synth) + |