diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-17 14:09:46 -0500 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-17 14:09:46 -0500 |
commit | 19cf50fcb832b01bb119dc1cfc31884e4e864f06 (patch) | |
tree | 2c9c0f41307ab5d62df39102571935bd2ea5fff1 /test | |
parent | 19ab3936ef46e93a98a142e0c454659ecc1d1e27 (diff) |
Cegis-specific infrastructure (#1933)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/VC22_a.sy | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/find_sc_bvult_bvnot.sy | 74 |
3 files changed, 76 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c0f1cf315..f8fdd4a18 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1480,6 +1480,7 @@ REG1_TESTS = \ regress1/sygus/dt-test-ns.sy \ regress1/sygus/dup-op.sy \ regress1/sygus/fg_polynomial3.sy \ + regress1/sygus/find_sc_bvult_bvnot.sy \ regress1/sygus/hd-01-d1-prog.sy \ regress1/sygus/hd-19-d1-prog-dup-op.sy \ regress1/sygus/hd-sdiv.sy \ diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy index 32e4723aa..ce437bc34 100644 --- a/test/regress/regress1/sygus/VC22_a.sy +++ b/test/regress/regress1/sygus/VC22_a.sy @@ -1,5 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --cegis-sample=use (set-logic LIA) (synth-fun f ((x1 Int) (x2 Int)) Int diff --git a/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy new file mode 100644 index 000000000..e994c2a5b --- /dev/null +++ b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy @@ -0,0 +1,74 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --cegis-sample=trust +(set-logic BV) + +; we test --cegis-sample=trust since we can exhaustively sample BV4 + +(synth-fun SC ((s (BitVec 4)) (t (BitVec 4))) Bool + ((Start Bool ( + true + false + (not Start) + (and Start Start) + (or Start Start) +; (=> Start Start) + (= StartBv StartBv) + (bvult StartBv StartBv) + (bvslt StartBv StartBv) + (bvuge StartBv StartBv) + (bvsge StartBv StartBv) + )) + (StartBv (BitVec 4) ( + s + t + #x0 + #x8 ; min_val + #x7 ; max_val + (bvneg StartBv) + (bvnot StartBv) + (bvadd StartBv StartBv) + (bvsub StartBv StartBv) + (bvand StartBv StartBv) + (bvlshr StartBv StartBv) + (bvor StartBv StartBv) + (bvshl StartBv StartBv) + )) +)) + +(declare-var s (BitVec 4)) +(declare-var t (BitVec 4)) +(define-fun udivtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4) + (ite (= b #x0) #xF (bvudiv a b)) +) +(define-fun uremtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4) + (ite (= b #x0) a (bvurem a b)) +) +(define-fun case ((x (BitVec 4)) (s (BitVec 4)) (t (BitVec 4))) Bool +(bvult (bvnot x) t) +) +(constraint + (= + (or + (case #x0 s t) + (case #x1 s t) + (case #x2 s t) + (case #x3 s t) + (case #x4 s t) + (case #x5 s t) + (case #x6 s t) + (case #x7 s t) + (case #x8 s t) + (case #x9 s t) + (case #xA s t) + (case #xB s t) + (case #xC s t) + (case #xD s t) + (case #xE s t) + (case #xF s t) + ) + (SC s t) + ) +) + +(check-synth) |