summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/logiccell_help.sy
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/sygus/logiccell_help.sy')
-rw-r--r--test/regress/regress1/sygus/logiccell_help.sy135
1 files changed, 67 insertions, 68 deletions
diff --git a/test/regress/regress1/sygus/logiccell_help.sy b/test/regress/regress1/sygus/logiccell_help.sy
index 1ba05e648..d6e8a75a4 100644
--- a/test/regress/regress1/sygus/logiccell_help.sy
+++ b/test/regress/regress1/sygus/logiccell_help.sy
@@ -1,119 +1,118 @@
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-repair-const
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-repair-const
(set-logic BV)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Utils
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(define-sort Bit () (BitVec 1))
+(define-sort Bit () (_ BitVec 1))
-(define-fun bit2bool ((b Bit)) Bool
+(define-fun bit2bool ((b Bit)) Bool
(= b #b1)
)
-(define-fun extend ((i (BitVec 4))) (BitVec 16)
+(define-fun extend ((i (_ BitVec 4))) (_ BitVec 16)
(concat #b000000000000 i)
)
-(define-fun extractBit ((i (BitVec 4)) (x (BitVec 16))) Bit
- ((_ extract 0 0) (bvlshr x (extend i)))
+(define-fun extractBit ((i (_ BitVec 4)) (x (_ BitVec 16))) Bit
+ ((_ extract 0 0) (bvlshr x (extend i)))
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Arch
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(define-fun lut4 ((i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (lut_val (BitVec 16))) Bit
+(define-fun lut4 ((i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (lut_val (_ BitVec 16))) Bit
(extractBit (concat i0 i1 i2 i3) lut_val)
)
(define-fun carry ((i0 Bit) (i1 Bit) (ci Bit)) Bit
- (bvor (bvand i0 i1) (bvand i0 ci) (bvand i1 ci))
+ (bvor (bvand i0 i1) (bvand i0 ci) (bvand i1 ci))
)
(define-fun mux2 ((s Bit) (i0 Bit) (i1 Bit)) Bit
;(ite (bit2bool s) i0 i1)
- (bvor (bvand s i0) (bvand (bvnot s) i1))
+ (bvor (bvand s i0) (bvand (bvnot s) i1))
)
(define-fun logic-cell (
- (i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (c_in Bit) ; inputs
- (s Bit) (lut_val (BitVec 16)) ;configs
- ) (BitVec 2) ; Cout O
- (let (
- (c_out Bit (carry i1 i2 c_in))
- (l_out Bit (lut4 i0 i1 i2 (mux2 s i3 c_in) lut_val))
- )
- (concat c_out l_out)
+ (i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (c_in Bit) ; inputs
+ (s Bit) (lut_val (_ BitVec 16)) ;configs
+ ) (_ BitVec 2) ; Cout O
+ (let (
+ (c_out (carry i1 i2 c_in))
+ (l_out (lut4 i0 i1 i2 (mux2 s i3 c_in) lut_val))
+ )
+ (concat c_out l_out)
))
(define-fun plb2 (
- (i_0_0 Bit) (i_0_1 Bit) (i_0_2 Bit) (i_0_3 Bit)
- (i_1_0 Bit) (i_1_1 Bit) (i_1_2 Bit) (i_1_3 Bit)
- (c_in Bit)
- (s_0 Bit) (lut_val_0 (BitVec 16)) ;configs
- (s_1 Bit) (lut_val_1 (BitVec 16)) ;configs
- ) (BitVec 3)
- (let ((lc0 (BitVec 2) (logic-cell i_0_0 i_0_1 i_0_2 i_0_3 c_in s_0 lut_val_0)))
- (let ((lc1 (BitVec 2) (logic-cell i_1_0 i_1_1 i_1_2 i_1_3 ((_ extract 1 1) lc0) s_1 lut_val_1)))
- (concat lc1 ((_ extract 0 0) lc0))
- ))
+ (i_0_0 Bit) (i_0_1 Bit) (i_0_2 Bit) (i_0_3 Bit)
+ (i_1_0 Bit) (i_1_1 Bit) (i_1_2 Bit) (i_1_3 Bit)
+ (c_in Bit)
+ (s_0 Bit) (lut_val_0 (_ BitVec 16)) ;configs
+ (s_1 Bit) (lut_val_1 (_ BitVec 16)) ;configs
+ ) (_ BitVec 3)
+ (let ((lc0 (logic-cell i_0_0 i_0_1 i_0_2 i_0_3 c_in s_0 lut_val_0)))
+ (let ((lc1 (logic-cell i_1_0 i_1_1 i_1_2 i_1_3 ((_ extract 1 1) lc0) s_1 lut_val_1)))
+ (concat lc1 ((_ extract 0 0) lc0))
+ ))
)
-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; synth
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(define-fun extract2 ((i (BitVec 1)) (x (BitVec 2))) Bit
- ((_ extract 0 0) (bvlshr x (concat #b0 i)))
+(define-fun extract2 ((i (_ BitVec 1)) (x (_ BitVec 2))) Bit
+ ((_ extract 0 0) (bvlshr x (concat #b0 i)))
)
-(synth-fun f ((x (BitVec 2)) (y (BitVec 2)) (c_in Bit)) (BitVec 3) (
- (Start (BitVec 3) (
- (plb2 #b0 (extract2 #b0 x) (extract2 #b0 y) #b0
- #b0 (extract2 #b1 x) (extract2 #b1 y) #b0
- Cin
- S LUT_VAL
- S LUT_VAL)
- ))
- (Cin Bit (
- c_in
- (Constant Bit)
- ))
- (S Bit (
- (Constant Bit)
- ))
- (LUT_VAL (BitVec 16) (
- (Constant (BitVec 16))
- ))
+(synth-fun f ((x (_ BitVec 2)) (y (_ BitVec 2)) (c_in Bit)) (_ BitVec 3)
+ ((Start (_ BitVec 3)) (Cin Bit) (S Bit) (LUT_VAL (_ BitVec 16))) (
+ (Start (_ BitVec 3) (
+ (plb2 #b0 (extract2 #b0 x) (extract2 #b0 y) #b0
+ #b0 (extract2 #b1 x) (extract2 #b1 y) #b0
+ Cin
+ S LUT_VAL
+ S LUT_VAL)
+ ))
+ (Cin Bit (
+ c_in
+ (Constant Bit)
+ ))
+ (S Bit (
+ (Constant Bit)
+ ))
+ (LUT_VAL (_ BitVec 16) (
+ (Constant (_ BitVec 16))
+ ))
))
-(declare-var x (BitVec 2))
-(declare-var y (BitVec 2))
+(declare-var x (_ BitVec 2))
+(declare-var y (_ BitVec 2))
-(constraint (=
- (bvadd (concat #b0 x) (concat #b0 y))
- (f x y #b0)
+(constraint (=
+ (bvadd (concat #b0 x) (concat #b0 y))
+ (f x y #b0)
))
-(constraint (=
- (bvadd (bvadd (concat #b0 x) (concat #b0 y)) #b001)
- (f x y #b1)
+(constraint (=
+ (bvadd (bvadd (concat #b0 x) (concat #b0 y)) #b001)
+ (f x y #b1)
))
-
(check-synth)
-
-;(define-fun lut4_ite ((I0 Bit) (I1 Bit) (I2 Bit) (I3 Bit) (LUT_VAL (BitVec 16))) Bit
-; (let ((s3 (BitVec 8) (ite (bit2bool I3) ((_ extract 15 8) LUT_VAL) ((_ extract 7 0) LUT_VAL))))
-; (let ((s2 (BitVec 4) (ite (bit2bool I2) ((_ extract 7 4) s3) ((_ extract 3 0) s3))))
-; (let ((s1 (BitVec 2) (ite (bit2bool I1) ((_ extract 3 2) s2) ((_ extract 1 0) s2))))
-; (let ((s0 (BitVec 1) (ite (bit2bool I0) ((_ extract 1 1) s1) ((_ extract 0 0) s1))))
-; s0
-; )
-; )
-; )
-; )
+
+;(define-fun lut4_ite ((I0 Bit) (I1 Bit) (I2 Bit) (I3 Bit) (LUT_VAL (_ BitVec 16))) Bit
+; (let ((s3 (_ BitVec 8) (ite (bit2bool I3) ((_ extract 15 8) LUT_VAL) ((_ extract 7 0) LUT_VAL))))
+; (let ((s2 (ite (bit2bool I2) ((_ extract 7 4) s3) ((_ extract 3 0) s3))))
+; (let ((s1 (ite (bit2bool I1) ((_ extract 3 2) s2) ((_ extract 1 0) s2))))
+; (let ((s0 (ite (bit2bool I0) ((_ extract 1 1) s1) ((_ extract 0 0) s1))))
+; s0
+; )
+; )
+; )
+; )
;)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback