diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-21 14:02:24 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-21 14:02:24 -0600 |
| commit | 60f1dd27da89be80c172e15e01c49f58e0ceb6c0 (patch) | |
| tree | b8aef41ea8e9e37d559b6309d7337109a7fd33aa /test | |
| parent | 4a12827561bc070fb5c7fd9baf1320a6bf154bc2 (diff) | |
Cegqi bv remove extract terms preprocess pass (#1376)
* Preprocess extract -> concat pass for cegqi bv.
* Add sygus bench
* Fixes, infrastructure.
* Minor fixes.
* Try
* Minor
* Minor
* Document
* Format
* Improving debug messages.
* Address
* Format
* Overlapping extracts.
* Format
* Minor
* Address review.
* Format
* Comment
* Format
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Base16_1.sy | 34 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 |
3 files changed, 37 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 274dcaff0..c59570651 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -115,6 +115,7 @@ TESTS = \ NUM878.smt2 \ psyco-107-bv.smt2 \ ari118-bv-2occ-x.smt2 \ + extract-nproc.smt2 \ javafe.ast.StandardPrettyPrint.319.smt2 \ javafe.ast.StmtVec.009.smt2 \ javafe.ast.WhileStmt.447.smt2 \ diff --git a/test/regress/regress0/sygus/Base16_1.sy b/test/regress/regress0/sygus/Base16_1.sy new file mode 100644 index 000000000..5833751cb --- /dev/null +++ b/test/regress/regress0/sygus/Base16_1.sy @@ -0,0 +1,34 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-qe-preproc --cbqi-bv-rm-extract --sygus-out=status --cbqi-bv --cegqi-si=all +(set-logic BV) + +(define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l)))) + +(define-fun E ((x (BitVec 8))) (BitVec 8) (bvadd x #x41)) + +(define-fun f ((x (BitVec 8))) (BitVec 8) (bvsub x #x41)) + +(define-fun d ((x (BitVec 8))) Bool (bvule x #x3f)) + +(synth-fun D ((x (BitVec 8)) (y (BitVec 8)) ) (BitVec 8) + ((Start (BitVec 8) ( + (f Start) x y Const + (bvshl Start Start) (bvnot Start) + (bvand Start Start) + (bvxor Start Start) + (bvor Start Start) + (bvneg Start) + (bvadd Start Start) + (bvlshr Start Start) + (bvsub Start Start) + )) + (Const (BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00)) +)) + +(declare-var x (BitVec 8)) +(constraint (= x (D (E (B #x07 #x04 x) ) (E (B #x03 #x00 x)) )) ) + +; notice we don't have solution reconstruction for this +(check-synth) + + diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index b40ee845f..82c2c2458 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -70,7 +70,8 @@ TESTS = commutative.sy \ process-10-vars.sy \ process-10-vars-2fun.sy \ inv-unused.sy \ - ccp16.lus.sy + ccp16.lus.sy \ + Base16_1.sy # sygus tests currently taking too long for make regress |