diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-29 22:25:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-29 22:25:42 -0500 |
| commit | 58985bed1bb0a812d97b3d490268023a164ba5e5 (patch) | |
| tree | f2df8f6f918d6f394e6c74e771e56cacbdb279ad /test | |
| parent | b260533f7b2c5fc217fa0f5036ab121249829bd4 (diff) | |
Allow multiple functions in sygus unif approaches (#1831)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/pbe_multi.sy | 67 |
2 files changed, 68 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 1ec6323b2..f799c20d5 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1479,6 +1479,7 @@ REG1_TESTS = \ regress1/sygus/nia-max-square-ns.sy \ regress1/sygus/no-flat-simp.sy \ regress1/sygus/no-mention.sy \ + regress1/sygus/pbe_multi.sy \ regress1/sygus/process-10-vars.sy \ regress1/sygus/qe.sy \ regress1/sygus/real-grammar.sy \ diff --git a/test/regress/regress1/sygus/pbe_multi.sy b/test/regress/regress1/sygus/pbe_multi.sy new file mode 100644 index 000000000..70cb6b2d2 --- /dev/null +++ b/test/regress/regress1/sygus/pbe_multi.sy @@ -0,0 +1,67 @@ +; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic BV)
+
+(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
+(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
+(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
+(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
+(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+
+(synth-fun f ( (x (BitVec 64))) (BitVec 64)
+(
+
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+ (shl1 Start)
+ (shr1 Start)
+ (shr4 Start)
+ (shr16 Start)
+ (bvand Start Start)
+ (bvor Start Start)
+ (bvxor Start Start)
+ (bvadd Start Start)
+ (if0 Start Start Start)
+ ))
+)
+)
+
+
+(constraint (= (f #x9db91b67d1eee4b4) #x00009db91b67d1ee))
+(constraint (= (f #x211526232b50ea1d) #xdeead9dcd4af15e2))
+(constraint (= (f #xedcec1de604e94ec) #x0000edcec1de604e))
+(constraint (= (f #xede1841179ee3684) #x0000ede1841179ee))
+(constraint (= (f #x9c623bcc40d252bd) #x639dc433bf2dad42))
+(constraint (= (f #x4601c6d84a50d01b) #xb9fe3927b5af2fe4))
+(constraint (= (f #x0c5ed1e748c4e26c) #x00000c5ed1e748c4))
+(constraint (= (f #x6bb653229e60ee94) #x00006bb653229e60))
+(constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee))
+(constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a))
+
+(synth-fun g ( (x (BitVec 64))) (BitVec 64)
+(
+
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+ (shl1 Start)
+ (shr1 Start)
+ (shr4 Start)
+ (shr16 Start)
+ (bvand Start Start)
+ (bvor Start Start)
+ (bvxor Start Start)
+ (bvadd Start Start)
+ (if0 Start Start Start)
+ ))
+)
+)
+
+(constraint (= (g #xd5a6481ee2ba1030) #xfffffffffffffffe))
+(constraint (= (g #x03e887e72dee55cd) #x03e887e72dee55cd))
+(constraint (= (g #xaced92921c8e318d) #xaced92921c8e318d))
+(constraint (= (g #x95e5e4184e40aaec) #xfffffffffffffffe))
+(constraint (= (g #x352367e34d76550b) #x352367e34d76550b))
+(constraint (= (g #x398560eeee7b1b6c) #xfffffffffffffffe))
+(constraint (= (g #x099be4899986c29a) #xfffffffffffffffe))
+(constraint (= (g #xb14b75be2e13445a) #xfffffffffffffffe))
+(constraint (= (g #xb4c680ad7e6b16ce) #xfffffffffffffffe))
+(constraint (= (g #x7e4954872868acb8) #xfffffffffffffffe))
+(check-synth)
|