diff options
author | Ying Sheng <sqy1415@gmail.com> | 2020-09-15 09:47:15 +0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-14 20:47:15 -0500 |
commit | 51be2e14c632d45e63a40659dea2177133251dfa (patch) | |
tree | d47380a72d05dc3ede4d61f4c04f9e4034b791fc /test | |
parent | 9e2a36f53007b932412a98c8e7ff1556a53f37c5 (diff) |
Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)
Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 8 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol1.smt2 | 19 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol2.smt2 | 31 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol3.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol_arr1.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol_arr2.smt2 | 15 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol_cosa_1.smt2 | 30 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol_dt.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol_from_pono_1.smt2 | 39 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol_from_pono_2.smt2 | 41 | ||||
-rw-r--r-- | test/regress/regress1/sygus/interpol_from_pono_3.smt2 | 54 |
11 files changed, 264 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d784a1ced..ef0981372 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1943,6 +1943,14 @@ set(regress_1_tests regress1/sygus/inv-example.sy regress1/sygus/inv-missed-sol-true.sy regress1/sygus/inv-unused.sy + regress1/sygus/interpol1.smt2 + regress1/sygus/interpol2.smt2 + regress1/sygus/interpol3.smt2 + regress1/sygus/interpol_arr1.smt2 + regress1/sygus/interpol_arr2.smt2 + regress1/sygus/interpol_cosa_1.smt2 + regress1/sygus/interpol_from_pono_1.smt2 + regress1/sygus/interpol_from_pono_2.smt2 regress1/sygus/issue2914.sy regress1/sygus/issue2935.sy regress1/sygus/issue3199.smt2 diff --git a/test/regress/regress1/sygus/interpol1.smt2 b/test/regress/regress1/sygus/interpol1.smt2 new file mode 100644 index 000000000..58ef5420f --- /dev/null +++ b/test/regress/regress1/sygus/interpol1.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic NIA) +(declare-fun x ( ) Int) +(declare-fun y ( ) Int) +(declare-fun z ( ) Int) +(assert (= (* 2 x) y)) +(get-interpol A (distinct (+ (* 2 z) 1) y) + +; the grammar for the interpol-to-synthesize +((Start Bool) (StartInt Int)) +( +(Start Bool ((< StartInt StartInt))) +(StartInt Int +(y (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2)) +) + +) diff --git a/test/regress/regress1/sygus/interpol2.smt2 b/test/regress/regress1/sygus/interpol2.smt2 new file mode 100644 index 000000000..c6876ee15 --- /dev/null +++ b/test/regress/regress1/sygus/interpol2.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 + +(set-logic QF_UFLIA) + +; Let A1,...,An be formulas (called assumptions) +; Let C be a formula (called a conjecture) +; An interpolant of {A1,...,An} and G is any formula B such that: +; - A1,...,An |- B +; - B |- C +; - B has only variables that occur both in {A_1,...,A_n} and B. + +;The variables used are n,m,x,y, all integers. +(declare-fun n () Int) +(declare-fun m () Int) +(declare-fun x () Int) +(declare-fun y () Int) + +;The assumptions are: +; (*) 1 <= n <= x <= n+5 +; (*) 1 <= y <= m +(define-fun A1 () Bool (<= 1 n)) +(define-fun A2 () Bool (<= n x)) +(define-fun A3 () Bool (<= x (+ n 5))) +(define-fun A4 () Bool (<= 1 y)) +(define-fun A5 () Bool (<= y m)) +(assert (and A1 A2 A3 A4 A5)) + +;The conjuecture is: 2 <= x+y +(get-interpol A (<= 2 (+ x y))) diff --git a/test/regress/regress1/sygus/interpol3.smt2 b/test/regress/regress1/sygus/interpol3.smt2 new file mode 100644 index 000000000..8681acf3a --- /dev/null +++ b/test/regress/regress1/sygus/interpol3.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --produce-interpols=default --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic LIA) +(declare-fun a () Int) +(assert (> a 1)) +(get-interpol A (> a 0)) diff --git a/test/regress/regress1/sygus/interpol_arr1.smt2 b/test/regress/regress1/sygus/interpol_arr1.smt2 new file mode 100644 index 000000000..16190f877 --- /dev/null +++ b/test/regress/regress1/sygus/interpol_arr1.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a () (Array (_ BitVec 4) (_ BitVec 4))) +(declare-fun y () (_ BitVec 4)) +(assert (= (select a y) (_ bv0 4))) +(get-interpol A (distinct (select a y) (_ bv1 4))) diff --git a/test/regress/regress1/sygus/interpol_arr2.smt2 b/test/regress/regress1/sygus/interpol_arr2.smt2 new file mode 100644 index 000000000..18ce2b35f --- /dev/null +++ b/test/regress/regress1/sygus/interpol_arr2.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun arr () (Array Int Int)) + +(define-fun A1 () Bool (<= 1 (select arr 0))) +(define-fun A2 () Bool (<= (select arr 0) (select arr 2))) +(define-fun A3 () Bool (<= (select arr 2) (+ (select arr 0) 5))) +(define-fun A4 () Bool (<= 1 (select arr 3))) +(define-fun A5 () Bool (<= (select arr 3) (select arr 1))) +(assert (and A1 A2 A3 A4 A5)) + +;The conjuecture is: 2 <= x+y +(get-interpol A (<= 2 (+ (select arr 2) (select arr 3)))) diff --git a/test/regress/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/regress1/sygus/interpol_cosa_1.smt2 new file mode 100644 index 000000000..583f94ed4 --- /dev/null +++ b/test/regress/regress1/sygus/interpol_cosa_1.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --produce-interpols=conjecture --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(set-option :produce-interpols conjecture) +(set-option :sygus-active-gen enum) +(declare-fun cfg@1 () (_ BitVec 1)) +(declare-fun witness_0@1 () Bool) +(declare-fun op@1 () (_ BitVec 4)) +(declare-fun counter@1 () (_ BitVec 16)) +(declare-fun input14@1 () (_ BitVec 1)) +(declare-fun clk@1 () (_ BitVec 1)) +(declare-fun a@1 () (_ BitVec 16)) +(declare-fun b@1 () (_ BitVec 16)) +(reset-assertions) +(declare-fun cfg@0 () (_ BitVec 1)) +(declare-fun witness_0@0 () Bool) +(declare-fun counter@0 () (_ BitVec 16)) +(declare-fun op@0 () (_ BitVec 4)) +(declare-fun input14@0 () (_ BitVec 1)) +(declare-fun b@0 () (_ BitVec 16)) +(declare-fun a@0 () (_ BitVec 16)) +(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) +(assert (and (or (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) witness_0@0) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) +(declare-fun cfg@2 () (_ BitVec 1)) +(declare-fun counter@2 () (_ BitVec 16)) +(declare-fun op@2 () (_ BitVec 4)) +(declare-fun witness_0@2 () Bool) +(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) +(get-interpol I (not (and (and true (and (and (and (and true (= witness_0@2 (not (= (bvand (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@1 (_ bv0 4))) (bvadd a@1 b@1) (bvsub a@1 b@1)) (bvadd a@1 b@1)) input14@1))) (_ bv1 1))))) (= op@2 (ite (= cfg@1 (_ bv1 1)) (_ bv0 4) op@1))) (= counter@2 (bvadd counter@1 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@2 (_ bv0 1)))) (not witness_0@2)))) diff --git a/test/regress/regress1/sygus/interpol_dt.smt2 b/test/regress/regress1/sygus/interpol_dt.smt2 new file mode 100644 index 000000000..f64ce4a0e --- /dev/null +++ b/test/regress/regress1/sygus/interpol_dt.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --produce-interpols=default +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List))))) +(declare-fun x () List) +(declare-fun y () List) +(assert ((_ is cons) x)) +(assert ((_ is nil) (tail x))) +(assert (= (head x) 0)) +(assert (= x y)) +(get-interpol A (distinct y nil)) diff --git a/test/regress/regress1/sygus/interpol_from_pono_1.smt2 b/test/regress/regress1/sygus/interpol_from_pono_1.smt2 new file mode 100644 index 000000000..eff00e066 --- /dev/null +++ b/test/regress/regress1/sygus/interpol_from_pono_1.smt2 @@ -0,0 +1,39 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a_S_a2@1 () (_ BitVec 1)) +(declare-fun a_R_a2@1 () (_ BitVec 1)) +(declare-fun a_Q_a2@1 () (_ BitVec 1)) +(declare-fun dve_invalid@1 () (_ BitVec 1)) +(declare-fun v_x1@1 () (_ BitVec 16)) +(declare-fun a_S_a1@1 () (_ BitVec 1)) +(declare-fun v_c@1 () (_ BitVec 16)) +(declare-fun v_x2@1 () (_ BitVec 16)) +(declare-fun a_Q_a1@1 () (_ BitVec 1)) +(declare-fun a_R_a1@1 () (_ BitVec 1)) +(declare-fun f3@1 () (_ BitVec 1)) +(declare-fun f0@1 () (_ BitVec 1)) +(declare-fun f5@1 () (_ BitVec 1)) +(declare-fun f1@1 () (_ BitVec 1)) +(declare-fun f2@1 () (_ BitVec 1)) +(declare-fun f4@1 () (_ BitVec 1)) +(declare-fun dve_invalid@0 () (_ BitVec 1)) +(declare-fun a_S_a2@0 () (_ BitVec 1)) +(declare-fun a_R_a2@0 () (_ BitVec 1)) +(declare-fun a_Q_a2@0 () (_ BitVec 1)) +(declare-fun a_S_a1@0 () (_ BitVec 1)) +(declare-fun a_R_a1@0 () (_ BitVec 1)) +(declare-fun a_Q_a1@0 () (_ BitVec 1)) +(declare-fun v_x2@0 () (_ BitVec 16)) +(declare-fun v_x1@0 () (_ BitVec 16)) +(declare-fun v_c@0 () (_ BitVec 16)) +(declare-fun f5@0 () (_ BitVec 1)) +(declare-fun f3@0 () (_ BitVec 1)) +(declare-fun f4@0 () (_ BitVec 1)) +(declare-fun f2@0 () (_ BitVec 1)) +(declare-fun f0@0 () (_ BitVec 1)) +(declare-fun f1@0 () (_ BitVec 1)) +(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) + +(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) diff --git a/test/regress/regress1/sygus/interpol_from_pono_2.smt2 b/test/regress/regress1/sygus/interpol_from_pono_2.smt2 new file mode 100644 index 000000000..894e8e781 --- /dev/null +++ b/test/regress/regress1/sygus/interpol_from_pono_2.smt2 @@ -0,0 +1,41 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a_S_a2@1 () (_ BitVec 1)) +(declare-fun a_R_a2@1 () (_ BitVec 1)) +(declare-fun a_Q_a2@1 () (_ BitVec 1)) +(declare-fun dve_invalid@1 () (_ BitVec 1)) +(declare-fun v_x1@1 () (_ BitVec 16)) +(declare-fun a_S_a1@1 () (_ BitVec 1)) +(declare-fun v_c@1 () (_ BitVec 16)) +(declare-fun v_x2@1 () (_ BitVec 16)) +(declare-fun a_Q_a1@1 () (_ BitVec 1)) +(declare-fun a_R_a1@1 () (_ BitVec 1)) +(declare-fun f3@1 () (_ BitVec 1)) +(declare-fun f0@1 () (_ BitVec 1)) +(declare-fun f5@1 () (_ BitVec 1)) +(declare-fun f1@1 () (_ BitVec 1)) +(declare-fun f2@1 () (_ BitVec 1)) +(declare-fun f4@1 () (_ BitVec 1)) +(declare-fun dve_invalid@0 () (_ BitVec 1)) +(declare-fun a_S_a2@0 () (_ BitVec 1)) +(declare-fun a_R_a2@0 () (_ BitVec 1)) +(declare-fun a_Q_a2@0 () (_ BitVec 1)) +(declare-fun a_S_a1@0 () (_ BitVec 1)) +(declare-fun a_R_a1@0 () (_ BitVec 1)) +(declare-fun a_Q_a1@0 () (_ BitVec 1)) +(declare-fun v_x2@0 () (_ BitVec 16)) +(declare-fun v_x1@0 () (_ BitVec 16)) +(declare-fun v_c@0 () (_ BitVec 16)) +(declare-fun f5@0 () (_ BitVec 1)) +(declare-fun f3@0 () (_ BitVec 1)) +(declare-fun f4@0 () (_ BitVec 1)) +(declare-fun f2@0 () (_ BitVec 1)) +(declare-fun f0@0 () (_ BitVec 1)) +(declare-fun f1@0 () (_ BitVec 1)) +(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) +(assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) + +(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) + diff --git a/test/regress/regress1/sygus/interpol_from_pono_3.smt2 b/test/regress/regress1/sygus/interpol_from_pono_3.smt2 new file mode 100644 index 000000000..5de1d4ebd --- /dev/null +++ b/test/regress/regress1/sygus/interpol_from_pono_3.smt2 @@ -0,0 +1,54 @@ +; COMMAND-LINE: --produce-interpols=default +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a_S_a2@1 () (_ BitVec 1)) +(declare-fun a_R_a2@1 () (_ BitVec 1)) +(declare-fun a_Q_a2@1 () (_ BitVec 1)) +(declare-fun dve_invalid@1 () (_ BitVec 1)) +(declare-fun v_x1@1 () (_ BitVec 16)) +(declare-fun a_S_a1@1 () (_ BitVec 1)) +(declare-fun v_c@1 () (_ BitVec 16)) +(declare-fun v_x2@1 () (_ BitVec 16)) +(declare-fun a_Q_a1@1 () (_ BitVec 1)) +(declare-fun a_R_a1@1 () (_ BitVec 1)) +(declare-fun f3@1 () (_ BitVec 1)) +(declare-fun f0@1 () (_ BitVec 1)) +(declare-fun f5@1 () (_ BitVec 1)) +(declare-fun f1@1 () (_ BitVec 1)) +(declare-fun f2@1 () (_ BitVec 1)) +(declare-fun f4@1 () (_ BitVec 1)) +(declare-fun dve_invalid@0 () (_ BitVec 1)) +(declare-fun a_S_a2@0 () (_ BitVec 1)) +(declare-fun a_R_a2@0 () (_ BitVec 1)) +(declare-fun a_Q_a2@0 () (_ BitVec 1)) +(declare-fun a_S_a1@0 () (_ BitVec 1)) +(declare-fun a_R_a1@0 () (_ BitVec 1)) +(declare-fun a_Q_a1@0 () (_ BitVec 1)) +(declare-fun v_x2@0 () (_ BitVec 16)) +(declare-fun v_x1@0 () (_ BitVec 16)) +(declare-fun v_c@0 () (_ BitVec 16)) +(declare-fun f5@0 () (_ BitVec 1)) +(declare-fun f3@0 () (_ BitVec 1)) +(declare-fun f4@0 () (_ BitVec 1)) +(declare-fun f2@0 () (_ BitVec 1)) +(declare-fun f0@0 () (_ BitVec 1)) +(declare-fun f1@0 () (_ BitVec 1)) +(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) +(assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) + +(declare-fun dve_invalid@2 () (_ BitVec 1)) +(declare-fun a_S_a2@2 () (_ BitVec 1)) +(declare-fun a_R_a2@2 () (_ BitVec 1)) +(declare-fun a_Q_a2@2 () (_ BitVec 1)) +(declare-fun a_S_a1@2 () (_ BitVec 1)) +(declare-fun a_R_a1@2 () (_ BitVec 1)) +(declare-fun a_Q_a1@2 () (_ BitVec 1)) +(declare-fun v_x2@2 () (_ BitVec 16)) +(declare-fun v_x1@2 () (_ BitVec 16)) +(declare-fun v_c@2 () (_ BitVec 16)) +(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) + +(get-interpol I (not (and (and true (and (and (and (and (and (and (and (and (and (and true (= v_c@2 (bvxor (_ bv1 16) (ite (= f5@1 (_ bv1 1)) v_x2@1 (ite (= f2@1 (_ bv1 1)) v_x1@1 (bvxor (_ bv1 16) v_c@1)))))) (= v_x1@2 (ite (= f1@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x1@1)))) (= v_x2@2 (ite (= f4@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x2@1)))) (= a_Q_a1@2 (bvnot (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (= a_R_a1@2 (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)))) (= a_S_a1@2 (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)))) (= a_Q_a2@2 (bvnot (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))) (= a_R_a2@2 (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)))) (= a_S_a2@2 (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)))) (= dve_invalid@2 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@1) (bvand (bvnot a_Q_a1@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@1 (bvnot f1@1))) (bvor a_S_a1@1 (bvnot f2@1))) (bvor (bvnot f3@1) (bvand (bvnot a_Q_a2@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@1 (bvnot f4@1))) (bvor a_S_a2@1 (bvnot f5@1))) (bvor f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@1 f1@1) (bvand f2@1 (bvor f0@1 f1@1))) (bvand f3@1 (bvor f2@1 (bvor f0@1 f1@1)))) (bvand f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1))))) (bvand f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@1) a_R_a1@1) (bvand a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1)))) (bvor a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1))) (bvnot (bvor (bvand (bvnot a_Q_a2@1) a_R_a2@1) (bvand a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1))))) (bvor a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)) (bvand (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1))))) (bvor (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)) (bvand (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))))) (bvor (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1))))) (bvnot dve_invalid@1)))))) (not (not (= (bvand (bvnot dve_invalid@2) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@2) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) + + |