From 60f1dd27da89be80c172e15e01c49f58e0ceb6c0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 21 Nov 2017 14:02:24 -0600
Subject: 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
---
 test/regress/regress0/sygus/Base16_1.sy | 34 +++++++++++++++++++++++++++++++++
 test/regress/regress0/sygus/Makefile.am |  3 ++-
 2 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/sygus/Base16_1.sy

(limited to 'test/regress/regress0/sygus')

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
-- 
cgit v1.2.3