diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-26 15:16:15 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-26 15:16:23 +0100 |
| commit | 4f5c9dbbd0125294500cf5788cb131b355979fb6 (patch) | |
| tree | fd07a862b4ad35111d56bdfa84f17f8c44d45e6c /test/regress/regress0/sygus/parity-AIG-d0.sy | |
| parent | 92e4099d9d2b313a521d2a015e604645e24617f4 (diff) | |
Robust strategy for single invocation LIA synthesis conjectures. Add regressions.
Diffstat (limited to 'test/regress/regress0/sygus/parity-AIG-d0.sy')
| -rw-r--r-- | test/regress/regress0/sygus/parity-AIG-d0.sy | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy new file mode 100644 index 000000000..c4fbd1c17 --- /dev/null +++ b/test/regress/regress0/sygus/parity-AIG-d0.sy @@ -0,0 +1,30 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic BV) + +(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + (xor (not (xor a b)) (not (xor c d)))) + +(synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + ((Start Bool ((and Start Start) (not Start) a b c d)))) + +(declare-var a Bool) +(declare-var b Bool) +(declare-var c Bool) +(declare-var d Bool) + +(constraint + (= (parity a b c d) + (and (AIG a b c d) + (not (and (and (not (and a b)) (not (and (not a) (not b)))) + (and (not (and (not c) (not d))) (not (and c d)))))))) + + +(check-synth) + +; Solution: +;(define-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool +;(not +; (and +; (and (not (and (not a) b)) (not (and d (not c)))) +; (and (not (and (not b) a)) (not (and (not d) c))))))
\ No newline at end of file |