(! u1 (! k (term s1)
(! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))
(holds cln)))
- (holds cln)))))))
+ (holds cln)))))))
\ No newline at end of file
(program mp_ispos ((x mpz)) formula
(mp_ifneg x false true))
-
+
(program mpz_eq ((x mpz) (y mpz)) formula
(mp_ifzero (mpz_sub x y) true false))
(program mpz_ ((x mpz) (y mpz)) formula
(mp_ifzero (mpz_sub x y) true false))
-
+
; "bitvec" is a term of type "sort"
; (declare BitVec sort)
(declare BitVec (!n mpz sort))
(declare bvc (! b bit (! v bv bv)))
; calculate the length of a bitvector
-;; (program bv_len ((v bv)) mpz
+;; (program bv_len ((v bv)) mpz
;; (match v
;; (bvn 0)
;; ((bvc b v') (mp_add (bv_len v') 1))))
(! n mpz
(! v bv
(term (BitVec n)))))
-
+
; a bv variable
(declare var_bv type)
; bit vector binary operators
(define bvop2
(! n mpz
- (! x (term (BitVec n))
+ (! x (term (BitVec n))
(! y (term (BitVec n))
(term (BitVec n))))))
; bit vector unary operators
(define bvop1
(! n mpz
- (! x (term (BitVec n))
+ (! x (term (BitVec n))
(term (BitVec n)))))
(! t1 (term (BitVec m))
(! t2 (term (BitVec m'))
(term (BitVec n))))))))
-
-;; side-condition fails in signature only??
+
+;; side-condition fails in signature only??
;; (! s (^ (mp_add m m') n)
;; (declare repeat bvopp)
(term (BitVec n)))))))
-
-;; TODO: add checks for valid typing for these operators
+
+;; TODO: add checks for valid typing for these operators
;; (! c1 (^ (mpz_lte i j)
;; (! c2 (^ (mpz_lt i n) true)
;; (! c3 (^ (mp_ifneg i false true) true)
-;; (! c4 (^ (mp_ifneg j false true) true)
+;; (! c4 (^ (mp_ifneg j false true) true)
;; (! s (^ (mp_add (mpz_sub i j) 1) m)
-
+
; bit vector predicates
(define bvpred
(! n mpz
(! x (term (BitVec n))
(! y (term (BitVec n))
formula))))
-
+
(declare bvult bvpred)
(declare bvule bvpred)
(declare bvugt bvpred)
(declare bvsle bvpred)
(declare bvsgt bvpred)
(declare bvsge bvpred)
-
(declare bbltc (! f formula (! v bblt bblt)))
; calculate the length of a bit-blasted term
-(program bblt_len ((v bblt)) mpz
+(program bblt_len ((v bblt)) mpz
(match v
(bbltn 0)
((bbltc b v') (mp_add (bblt_len v') 1))))
(bblast_term n x y)))))
+; Binds a symbol to the bblast_term to be used later on.
(declare decl_bblast
(! n mpz
(! b bblt
;; BITBLASTING RULES
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST CONSTANT
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(program bblast_const ((v bv) (n mpz)) bblt
- (mp_ifneg n (match v (bvn bbltn)
+ (mp_ifneg n (match v (bvn bbltn)
(default (fail bblt)))
(match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1)))))
(default (fail bblt)))))
-
+
(declare bv_bbl_const (! n mpz
(! f bblt
(! v bv
(! c (^ (bblast_const v (mp_add n (~ 1))) f)
(bblast_term n (a_bv n v) f))))))
-
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST VARIABLE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(program bblast_var ((x var_bv) (n mpz)) bblt
- (mp_ifneg n bbltn
+ (mp_ifneg n bbltn
(bbltc (bitof x n) (bblast_var x (mp_add n (~ 1))))))
(declare bv_bbl_var (! n mpz
(! c (^ (bblast_var x (mp_add n (~ 1))) f)
(bblast_term n (a_var_bv n x) f))))))
-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST CONCAT
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(program bblast_concat ((x bblt) (y bblt)) bblt
- (match x
+ (match x
(bbltn (match y ((bbltc by y') (bbltc by (bblast_concat x y')))
(bbltn bbltn)))
((bbltc bx x') (bbltc bx (bblast_concat x' y)))))
-
-
+
(declare bv_bbl_concat (! n mpz
(! m mpz
(! m1 mpz
(! c (^ (bblast_concat xb yb ) rb)
(bblast_term n (concat n m m1 x y) rb)))))))))))))
-
+(declare bv_bbl_concat_alias_1 (! n mpz
+ (! m mpz
+ (! m1 mpz
+ (! x (term (BitVec m))
+ (! y (term (BitVec m1))
+ (! xb bblt
+ (! yb bblt
+ (! rb bblt
+ (! a (term (BitVec m))
+ (! e (th_holds (= _ x a))
+ (! xbb (bblast_term m x xb)
+ (! ybb (bblast_term m1 y yb)
+ (! c (^ (bblast_concat xb yb) rb)
+ (bblast_term n (concat n m m1 a y) rb)))))))))))))))
+
+(declare bv_bbl_concat_alias_2 (! n mpz
+ (! m mpz
+ (! m1 mpz
+ (! x (term (BitVec m))
+ (! y (term (BitVec m1))
+ (! xb bblt
+ (! yb bblt
+ (! rb bblt
+ (! xbb (bblast_term m x xb)
+ (! a (term (BitVec m1))
+ (! e (th_holds (= _ y a))
+ (! ybb (bblast_term m1 y yb)
+ (! c (^ (bblast_concat xb yb) rb)
+ (bblast_term n (concat n m m1 x a) rb)))))))))))))))
+
+(declare bv_bbl_concat_alias_1_2 (! n mpz
+ (! m mpz
+ (! m1 mpz
+ (! x (term (BitVec m))
+ (! y (term (BitVec m1))
+ (! xb bblt
+ (! yb bblt
+ (! rb bblt
+ (! a1 (term (BitVec m))
+ (! e (th_holds (= _ x a1))
+ (! xbb (bblast_term m x xb)
+ (! a2 (term (BitVec m1))
+ (! e (th_holds (= _ y a2))
+ (! ybb (bblast_term m1 y yb)
+ (! c (^ (bblast_concat xb yb) rb)
+ (bblast_term n (concat n m m1 a1 a2) rb)))))))))))))))))
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST EXTRACT
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(program bblast_extract_rec ((x bblt) (i mpz) (j mpz) (n mpz)) bblt
- (match x
+ (match x
((bbltc bx x') (mp_ifneg (mpz_sub (mpz_sub j n) 1)
(mp_ifneg (mpz_sub (mpz_sub n i) 1)
(bbltc bx (bblast_extract_rec x' i j (mpz_sub n 1)))
(bblast_extract_rec x' i j (mpz_sub n 1)))
-
+
bbltn))
(bbltn bbltn)))
(program bblast_extract ((x bblt) (i mpz) (j mpz) (n mpz)) bblt
- (bblast_extract_rec x i j (mpz_sub n 1)))
+ (bblast_extract_rec x i j (mpz_sub n 1)))
(declare bv_bbl_extract (! n mpz
(! i mpz
(! j mpz
(! m mpz
- (! x (term (BitVec m))
+ (! x (term (BitVec m))
(! xb bblt
(! rb bblt
(! xbb (bblast_term m x xb)
(! c ( ^ (bblast_extract xb i j m) rb)
(bblast_term n (extract n i j m x) rb)))))))))))
+(declare bv_bbl_extract_alias (! n mpz
+ (! i mpz
+ (! j mpz
+ (! m mpz
+ (! x (term (BitVec m))
+ (! xb bblt
+ (! rb bblt
+ (! a (term (BitVec m))
+ (! e (th_holds (= _ x a))
+ (! xbb (bblast_term m x xb)
+ (! c ( ^ (bblast_extract xb i j m) rb)
+ (bblast_term n (extract n i j m a) rb)))))))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST ZERO/SIGN EXTEND
(declare bv_bbl_zero_extend (! n mpz
(! k mpz
(! m mpz
- (! x (term (BitVec m))
+ (! x (term (BitVec m))
(! xb bblt
(! rb bblt
(! xbb (bblast_term m x xb)
(! c ( ^ (bblast_zextend xb k m) rb)
(bblast_term n (zero_extend n k m x) rb))))))))))
-
(program bblast_sextend ((x bblt) (i mpz)) bblt
(match x (bbltn (fail bblt))
- ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb))))
+ ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb))))
(declare bv_bbl_sign_extend (! n mpz
(! k mpz
(! m mpz
- (! x (term (BitVec m))
+ (! x (term (BitVec m))
(! xb bblt
(! rb bblt
(! xbb (bblast_term m x xb)
(! c ( ^ (bblast_sextend xb k m) rb)
(bblast_term n (sign_extend n k m x) rb))))))))))
-
-
-
+
+(declare bv_bbl_sign_extend_alias (! n mpz
+ (! k mpz
+ (! m mpz
+ (! x (term (BitVec m))
+ (! xb bblt
+ (! rb bblt
+ (! a (term (BitVec m))
+ (! e (th_holds (= _ x a))
+ (! xbb (bblast_term m x xb)
+ (! c ( ^ (bblast_sextend xb k m) rb)
+ (bblast_term n (sign_extend n k m a) rb))))))))))))
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST BVAND
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
+
(program bblast_bvand ((x bblt) (y bblt)) bblt
- (match x
+ (match x
(bbltn (match y (bbltn bbltn) (default (fail bblt))))
- ((bbltc bx x') (match y
+ ((bbltc bx x') (match y
(bbltn (fail bblt))
((bbltc by y') (bbltc (and bx by) (bblast_bvand x' y')))))))
-
-
+
(declare bv_bbl_bvand (! n mpz
(! x (term (BitVec n))
(! y (term (BitVec n))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(program bblast_bvnot ((x bblt)) bblt
- (match x
- (bbltn bbltn)
+ (match x
+ (bbltn bbltn)
((bbltc bx x') (bbltc (not bx) (bblast_bvnot x')))))
-
-
+
(declare bv_bbl_bvnot (! n mpz
(! x (term (BitVec n))
(! xb bblt
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST BVOR
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
+
(program bblast_bvor ((x bblt) (y bblt)) bblt
- (match x
+ (match x
(bbltn (match y (bbltn bbltn) (default (fail bblt))))
- ((bbltc bx x') (match y
+ ((bbltc bx x') (match y
(bbltn (fail bblt))
((bbltc by y') (bbltc (or bx by) (bblast_bvor x' y')))))))
-
-
+
(declare bv_bbl_bvor (! n mpz
(! x (term (BitVec n))
(! y (term (BitVec n))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST BVXOR
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
+
(program bblast_bvxor ((x bblt) (y bblt)) bblt
- (match x
+ (match x
(bbltn (match y (bbltn bbltn) (default (fail bblt))))
- ((bbltc bx x') (match y
+ ((bbltc bx x') (match y
(bbltn (fail bblt))
((bbltc by y') (bbltc (xor bx by) (bblast_bvxor x' y')))))))
-
-
+
(declare bv_bbl_bvxor (! n mpz
(! x (term (BitVec n))
(! y (term (BitVec n))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST BVADD
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; return the carry bit after adding x y
+
+;; return the carry bit after adding x y
;; FIXME: not the most efficient thing in the world
(program bblast_bvadd_carry ((a bblt) (b bblt) (carry formula)) formula
(match a
(bbltn (fail formula))
((bbltc bi b') (or (and ai bi) (and (xor ai bi) (bblast_bvadd_carry a' b' carry))))))))
-;; ripple carry adder where carry is the initial carry bit
+;; ripple carry adder where carry is the initial carry bit
(program bblast_bvadd ((a bblt) (b bblt) (carry formula)) bblt
(match a
( bbltn (match b (bbltn bbltn) (default (fail bblt))))
;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt
;(match a
; ( bbltn (match b (bbltn bbltn) (default (fail bblt))))
-; ((bbltc ai a') (match b
+; ((bbltc ai a') (match b
; (bbltn (fail bblt))
-; ((bbltc bi b')
+; ((bbltc bi b')
; (let carry' (or (and ai bi) (and (xor ai bi) carry))
; (bbltc (xor (xor ai bi) carry)
; (bblast_bvadd_2h a' b' carry'))))))))
;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt
-;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit
+;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit
;(let br (reverseb b) ;; from the least significant bit up
;(let ret (bblast_bvadd_2h ar br carry)
; (reverseb ret)))))
-
+
(declare bv_bbl_bvadd (! n mpz
(! x (term (BitVec n))
(! y (term (BitVec n))
(! c (^ (bblast_bvadd xb yb false) rb)
(bblast_term n (bvadd n x y) rb)))))))))))
+(declare bv_bbl_bvadd_alias_1 (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! xb bblt
+ (! yb bblt
+ (! rb bblt
+ (! a (term (BitVec n))
+ (! e (th_holds (= _ x a))
+ (! xbb (bblast_term n x xb)
+ (! ybb (bblast_term n y yb)
+ (! c (^ (bblast_bvadd xb yb false) rb)
+ (bblast_term n (bvadd n a y) rb)))))))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST BVNEG
(program bblast_bvneg ((x bblt) (n mpz)) bblt
(bblast_bvadd (bblast_bvnot x) (bblast_zero n) true))
-
-
+
+
(declare bv_bbl_bvneg (! n mpz
(! x (term (BitVec n))
(! xb bblt
;; BITBLAST BVMUL
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
+
;; shift add multiplier
;; (program concat ((a bblt) (b bblt)) bblt
;; (match a (bbltn b)
;; ((bbltc ai a') (bbltc ai (concat a' b)))))
-
+
(program top_k_bits ((a bblt) (k mpz)) bblt
(mp_ifzero k bbltn
(match a (bbltn (fail bblt))
(program bottom_k_bits ((a bblt) (k mpz)) bblt
(reverseb (top_k_bits (reverseb a) k)))
-;; assumes the least signigicant bit is at the beginning of the list
+;; assumes the least signigicant bit is at the beginning of the list
(program k_bit ((a bblt) (k mpz)) formula
(mp_ifneg k (fail formula)
(match a (bbltn (fail formula))
(program and_with_bit ((a bblt) (bt formula)) bblt
(match a (bbltn bbltn)
((bbltc ai a') (bbltc (and bt ai) (and_with_bit a' bt)))))
-
+
;; a is going to be the current result
;; carry is going to be false initially
;; b is the and of a and b[k]
(let ak (top_k_bits a k')
(let b' (and_with_bit ak (k_bit b k))
(mp_ifzero (mpz_sub k' 1)
- (mult_step_k_h res b' bbltn false k)
+ (mult_step_k_h res b' bbltn false k)
(let res' (mult_step_k_h res b' bbltn false k)
(mult_step a b (reverseb res') n (mp_add k 1))))))))
(program bblast_bvmul ((a bblt) (b bblt) (n mpz)) bblt
-(let ar (reverseb a) ;; reverse a and b so that we can build the circuit
+(let ar (reverseb a) ;; reverse a and b so that we can build the circuit
(let br (reverseb b) ;; from the least significant bit up
(let res (and_with_bit ar (k_bit br 0))
- (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step
+ (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step
res
(mult_step ar br res n 1))))))
-
+
(declare bv_bbl_bvmul (! n mpz
(! x (term (BitVec n))
(! y (term (BitVec n))
(bblast_term n (bvmul n x y) rb)))))))))))
-
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST EQUALS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
+
; bit blast x = y
; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))
; f is the accumulator formula that builds the equality in the right order
(program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula
- (match x
+ (match x
(bbltn (match y (bbltn f) (default (fail formula))))
- ((bbltc fx x') (match y
+ ((bbltc fx x') (match y
(bbltn (fail formula))
((bbltc fy y') (bblast_eq_rec x' y' (and (iff fx fy) f)))))
(default (fail formula))))
((bbltc bx x') (match y ((bbltc by y') (bblast_eq_rec x' y' (iff bx by)))
(default (fail formula))))
(default (fail formula))))
-
+
+
+;; TODO: a temporary bypass for rewrites that we don't support yet. As soon
+;; as we do, remove this rule.
+
+(declare bv_bbl_=_false
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! bbx (bblast_term n x bx)
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_eq bx by) f)
+ (th_holds (iff (= (BitVec n) x y) false))))))))))))
+
(declare bv_bbl_=
(! n mpz
(! x (term (BitVec n))
(! c (^ (bblast_eq bx by) f)
(th_holds (iff (= (BitVec n) x y) f))))))))))))
-
+(declare bv_bbl_=_swap
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! bbx (bblast_term n x bx)
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_eq by bx) f)
+ (th_holds (iff (= (BitVec n) x y) f))))))))))))
+
+(declare bv_bbl_=_alias_1
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! a (term (BitVec n))
+ (! e (th_holds (= _ x a))
+ (! bbx (bblast_term n x bx)
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_eq bx by) f)
+ (th_holds (iff (= (BitVec n) a y) f))))))))))))))
+
+(declare bv_bbl_=_alias_1_swap
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! a (term (BitVec n))
+ (! e (th_holds (= _ x a))
+ (! bbx (bblast_term n x bx)
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_eq by bx) f)
+ (th_holds (iff (= (BitVec n) a y) f))))))))))))))
+
+(declare bv_bbl_=_alias_2
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! bbx (bblast_term n x bx)
+ (! a (term (BitVec n))
+ (! e (th_holds (= _ y a))
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_eq bx by) f)
+ (th_holds (iff (= (BitVec n) x a) f))))))))))))))
+
+(declare bv_bbl_=_alias_2_swap
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! bbx (bblast_term n x bx)
+ (! a (term (BitVec n))
+ (! e (th_holds (= _ y a))
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_eq by bx) f)
+ (th_holds (iff (= (BitVec n) x a) f))))))))))))))
+
+(declare bv_bbl_=_alias_1_2
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! a1 (term (BitVec n))
+ (! e1 (th_holds (= _ x a1))
+ (! bbx (bblast_term n x bx)
+ (! a2 (term (BitVec n))
+ (! e2 (th_holds (= _ y a2))
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_eq bx by) f)
+ (th_holds (iff (= (BitVec n) a1 a2) f))))))))))))))))
+
+(declare bv_bbl_=_alias_1_2_swap
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! a1 (term (BitVec n))
+ (! e1 (th_holds (= _ x a1))
+ (! bbx (bblast_term n x bx)
+ (! a2 (term (BitVec n))
+ (! e2 (th_holds (= _ y a2))
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_eq by bx) f)
+ (th_holds (iff (= (BitVec n) a1 a2) f))))))))))))))))
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST BVULT
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
+
(program bblast_bvult ((x bblt) (y bblt) (n mpz)) formula
(match x
( bbltn (fail formula))
(! c (^ (bblast_bvult bx by (mp_add n (~1))) f)
(th_holds (iff (bvult n x y) f))))))))))))
+(declare bv_bbl_bvult_alias_1
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! a1 (term (BitVec n))
+ (! e1 (th_holds (= _ x a1))
+ (! bbx (bblast_term n x bx)
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_bvult bx by (mp_add n (~1))) f)
+ (th_holds (iff (bvult n a1 y) f))))))))))))))
+
+(declare bv_bbl_bvult_alias_2
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! bbx (bblast_term n x bx)
+ (! a2 (term (BitVec n))
+ (! e2 (th_holds (= _ y a2))
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_bvult bx by (mp_add n (~1))) f)
+ (th_holds (iff (bvult n x a2) f))))))))))))))
+
+(declare bv_bbl_bvult_alias_1_2
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! a1 (term (BitVec n))
+ (! e1 (th_holds (= _ x a1))
+ (! bbx (bblast_term n x bx)
+ (! a2 (term (BitVec n))
+ (! e2 (th_holds (= _ y a2))
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_bvult bx by (mp_add n (~1))) f)
+ (th_holds (iff (bvult n a1 a2) f))))))))))))))))
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; BITBLAST BVSLT
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
+
(program bblast_bvslt ((x bblt) (y bblt) (n mpz)) formula
(match x
( bbltn (fail formula))
(! bby (bblast_term n y by)
(! c (^ (bblast_bvslt bx by n) f)
(th_holds (iff (bvslt n x y) f))))))))))))
-
+
+(declare bv_bbl_bvslt_alias_1
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! a (term (BitVec n))
+ (! e (th_holds (= _ x a))
+ (! bbx (bblast_term n x bx)
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_bvslt bx by n) f)
+ (th_holds (iff (bvslt n a y) f))))))))))))))
+
+(declare bv_bbl_bvslt_alias_2
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! bx bblt
+ (! by bblt
+ (! f formula
+ (! bbx (bblast_term n x bx)
+ (! a (term (BitVec n))
+ (! e (th_holds (= _ y a))
+ (! bby (bblast_term n y by)
+ (! c (^ (bblast_bvslt bx by n) f)
+ (th_holds (iff (bvslt n x a) f))))))))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; REWRITE RULES
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-
+
+
; rewrite rule :
; x + y = y + x
(declare bvadd_symm
(! x (term (BitVec n))
(! y (term (BitVec n))
(th_holds (= (BitVec n) (bvadd _ x y) (bvadd _ y x)))))))
-
+
;; (declare bvcrazy_rewrite
;; (! n mpz
;; (! x (term (BitVec n))
;; (! s (^ (rewrite_scc xn yn) true)
;; (! u (! x (term (BitVec n)) (holds cln))
;; (holds cln)))))))))))
-
+
;; (th_holds (= (BitVec n) (bvadd x y) (bvadd y x)))))))
-
-
-; necessary?
+
+
+; necessary?
;; (program calc_bvand ((a bv) (b bv)) bv
;; (match a
;; (bvn (match b (bvn bvn) (default (fail bv))))
;; (default (fail bv))))))
;; ; rewrite rule (w constants) :
-;; ; a & b = c
+;; ; a & b = c
;; (declare bvand_const (! c bv
;; (! a bv
;; (! b bv
;; (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c))))))))
-;; making constant bit-vectors
+;; making constant bit-vectors
(program mk_ones ((n mpz)) bv
(mp_ifzero n bvn (bvc b1 (mk_ones (mpz_sub n 1)))))
(mp_ifzero n bvn (bvc b0 (mk_ones (mpz_sub n 1)))))
-
+
;; (bvxnor a b) => (bvnot (bvxor a b))
;; (declare bvxnor_elim
;; (! n mpz
;; (! rwb (rw_term _ b (a_bv _ zero_bits))
;; (rw_term _ (bvxor _ a b)
;; a'))))))))))
-
+
;; ;; (bvxor a 11) => (bvnot a)
;; (declare bvxor_one
;; (! n mpz
;; (rw_term _ (bvxor _ a b)
;; (bvnot _ a')))))))))))
-
+
;; ;; (bvnot (bvnot a)) => a
;; (declare bvnot_idemp
;; (! n mpz
;; (! rwa (rw_term _ a a')
;; (rw_term _ (bvnot _ (bvnot _ a))
;; a'))))))
-
proof/skolemization_manager.h \
proof/theory_proof.cpp \
proof/theory_proof.h \
+ proof/lemma_proof.cpp \
+ proof/lemma_proof.h \
proof/uf_proof.cpp \
proof/uf_proof.h \
proof/unsat_core.cpp \
proof/unsat_core.h \
+ proof/proof_output_channel.cpp \
+ proof/proof_output_channel.h \
prop/cnf_stream.cpp \
prop/cnf_stream.h \
prop/prop_engine.cpp \
# Step 4: Generate X_options.h from X_options.sed
# Step 5: Generate X_options.cpp from X_options.sed.
# This stage also waits for X_options.h as otherwise it cannot compile.
-#
+#
OPTIONS_SRC_FILES = \
arith_options \
# directories that are cleaned first. Without this rule, "distclean"
# fails.
%.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@"
-
// Nothing to do here at this point.
}
+void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ // Nothing to do here at this point.
+}
+
} /* CVC4 namespace */
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
};
void ProofArray::setRowMergeTag(unsigned tag) {
d_reasonRow = tag;
+ d_proofPrinter.d_row = tag;
}
void ProofArray::setRow1MergeTag(unsigned tag) {
d_reasonRow1 = tag;
+ d_proofPrinter.d_row1 = tag;
}
void ProofArray::setExtMergeTag(unsigned tag) {
d_reasonExt = tag;
+ d_proofPrinter.d_ext = tag;
+}
+
+unsigned ProofArray::getRowMergeTag() const {
+ return d_reasonRow;
+}
+
+unsigned ProofArray::getRow1MergeTag() const {
+ return d_reasonRow1;
+}
+
+unsigned ProofArray::getExtMergeTag() const {
+ return d_reasonExt;
}
void ProofArray::toStream(std::ostream& out) {
void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map) {
Debug("pf::array") << "Printing array proof in LFSC : " << std::endl;
- pf->debug_print("pf::array");
+ pf->debug_print("pf::array", 0, &d_proofPrinter);
Debug("pf::array") << std::endl;
toStreamRecLFSC( out, tp, pf, 0, map );
Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl;
const LetMap& map) {
Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
- pf->debug_print("pf::array");
+ pf->debug_print("pf::array", 0, &d_proofPrinter);
Debug("pf::array") << std::endl;
if(tb == 0) {
pf->d_children[i + count]->d_node.isNull();
++count) {
Debug("pf::array") << "Found a congruence: " << std::endl;
- pf->d_children[i+count]->debug_print("pf::array");
+ pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter);
congruenceClosures.push_back(pf->d_children[i+count]);
}
++i;
}
}
- Assert(neg >= 0);
+
+ bool disequalityFound = (neg >= 0);
+ if (!disequalityFound) {
+ Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
+ Debug("pf::array") << "Proof for: " << pf->d_node << std::endl;
+ Assert(pf->d_node.getKind() == kind::EQUAL);
+ Assert(pf->d_node.getNumChildren() == 2);
+ Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst());
+ }
Node n1;
std::stringstream ss, ss2;
//Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
- if(pf->d_children.size() > 2) {
+ if(!disequalityFound || pf->d_children.size() > 2) {
n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
} else {
n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
}
- Node n2 = pf->d_children[neg]->d_node;
- Assert(n2.getKind() == kind::NOT);
- Debug("mgdx") << "\nhave proven: " << n1 << std::endl;
- Debug("mgdx") << "n2 is " << n2 << std::endl;
- Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl;
- Debug("mgdx") << "n2[0] is " << n2[0] << std::endl;
-
- if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
- if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
-
- if (pf->d_children[neg]->d_id == d_reasonExt) {
- // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
-
- // (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6
-
- out << "(clausify_false (contra _ ";
- out << ss.str();
-
- toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map);
+ out << "(clausify_false (contra _ ";
- out << " ";
- out << ss2.str();
- out << "))";
+ if (disequalityFound) {
+ Node n2 = pf->d_children[neg]->d_node;
+ Assert(n2.getKind() == kind::NOT);
+ Debug("mgdx") << "\nhave proven: " << n1 << std::endl;
+ Debug("mgdx") << "n2 is " << n2 << std::endl;
+ Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl;
+ Debug("mgdx") << "n2[0] is " << n2[0] << std::endl;
- } else {
- // The negative node is, e.g., a pure equality
- out << "(clausify_false (contra _ ";
+ if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
+ if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
- if(n2[0].getKind() == kind::APPLY_UF) {
+ if ((pf->d_children[neg]->d_id == d_reasonExt) ||
+ (pf->d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) {
+ // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
+ out << ss.str();
+ out << " ";
+ toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map);
+ out << ss2.str();
+ } else if (n2[0].getKind() == kind::APPLY_UF) {
out << "(trans _ _ _ _ ";
out << "(symm _ _ _ ";
out << ss.str();
Debug("pf::array") << "ArrayProof::toStream: getLitName( " << n2[0] << " ) = " <<
ProofManager::getLitName(n2[0]) << std::endl;
- out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
+ out << " " << ProofManager::getLitName(n2[0]);
}
+ } else {
+ Node n2 = pf->d_node;
+ Assert(n2.getKind() == kind::EQUAL);
+ Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
+
+ out << ss.str();
+ out << " ";
+ ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out,
+ n1[0].toExpr(),
+ n1[1].toExpr());
}
+ out << "))" << std::endl;
return Node();
}
if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) {
Debug("mgd") << "\nok, looking at congruence:\n";
- pf->debug_print("mgd");
+ pf->debug_print("mgd", 0, &d_proofPrinter);
std::stack<const theory::eq::EqProof*> stk;
for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) {
Assert(!pf2->d_node.isNull());
Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
- pf2->debug_print("mgd");
+ pf2->debug_print("mgd", 0, &d_proofPrinter);
// Temp
Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl;
Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl;
Debug("mgd") << "SIDE IS 1\n";
if(!match(pf2->d_node, n1[1])) {
Debug("mgd") << "IN BAD CASE, our first subproof is\n";
- pf2->d_children[0]->debug_print("mgd");
+ pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter);
}
Assert(match(pf2->d_node, n1[1]));
side = 1;
return pf->d_node;
}
+ else if (pf->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
+ Debug("pf::array") << "Proof for: " << pf->d_node << std::endl;
+ Assert(pf->d_node.getKind() == kind::NOT);
+ Node n = pf->d_node[0];
+ Assert(n.getKind() == kind::EQUAL);
+ Assert(n.getNumChildren() == 2);
+ Assert(n[0].isConst() && n[1].isConst());
+
+ ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out,
+ n[0].toExpr(),
+ n[1].toExpr());
+ return pf->d_node;
+ }
+
else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) {
bool firstNeg = false;
bool secondNeg = false;
Assert(pf->d_children.size() >= 2);
std::stringstream ss;
Debug("mgd") << "\ndoing trans proof[[\n";
- pf->debug_print("mgd");
+ pf->debug_print("mgd", 0, &d_proofPrinter);
Debug("mgd") << "\n";
Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n";
Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
Warning() << "0 proves " << n1 << "\n";
Warning() << "1 proves " << n2 << "\n\n";
- pf->debug_print("mgdx",0);
+ pf->debug_print("mgdx", 0, &d_proofPrinter);
//toStreamRec(Warning.getStream(), pf, 0);
Warning() << "\n\n";
Unreachable();
t4 = pf->d_children[0]->d_node[0][side][0][2];
ret = pf->d_node;
+ // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry.
+ bool swap = (t2 == pf->d_children[0]->d_node[0][side][0][1]);
+
Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
Assert(pf->d_children.size() == 1);
Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
+ if (swap) {
+ out << "(symm _ _ _ ";
+ }
+
out << "(negativerow _ _ ";
- tp->printTerm(t1.toExpr(), out, map);
+ tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map);
out << " ";
- tp->printTerm(t2.toExpr(), out, map);
+ tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map);
out << " ";
tp->printTerm(t3.toExpr(), out, map);
out << " ";
tp->printTerm(t4.toExpr(), out, map);
out << " ";
-
- // if (subproof[0][1] == t3) {
- Debug("pf::array") << "Dont need symmetry!" << std::endl;
- out << ss.str();
- // } else {
- // Debug("pf::array") << "Need symmetry!" << std::endl;
- // out << "(negsymm _ _ _ " << ss.str() << ")";
- // }
+ if (side != 0) {
+ out << "(negsymm _ _ _ " << ss.str() << ")";
+ } else {
+ out << ss.str();
+ }
out << ")";
- // Unreachable();
+ if (swap) {
+ out << ") ";
+ }
return ret;
}
}
std::string ArrayProof::skolemToLiteral(Expr skolem) {
+ Debug("pf::array") << "ArrayProof::skolemToLiteral( " << skolem << ")" << std::endl;
Assert(d_skolemToLiteral.find(skolem) != d_skolemToLiteral.end());
return d_skolemToLiteral[skolem];
}
void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
- Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedTerm: term = " << term << std::endl;
-
Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY);
if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) {
void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) {
Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl;
Assert (type.isArray() || type.isSort());
- os << type <<" ";
+ if (type.isArray()){
+ ArrayType array_type(type);
+
+ Debug("pf::array") << "LFSCArrayProof::printOwnedSort: type is an array. Index type: "
+ << array_type.getIndexType()
+ << ", element type: " << array_type.getConstituentType() << std::endl;
+
+ os << "(Array ";
+ printSort(array_type.getIndexType(), os);
+ os << " ";
+ printSort(array_type.getConstituentType(), os);
+ os << ")";
+ } else {
+ os << type <<" ";
+ }
}
void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
void LFSCArrayProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
// declaring the sorts
- Debug("pf::array") << "Arrays declaring sorts..." << std::endl;
-
for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) {
if (!ProofManager::currentPM()->wasPrinted(*it)) {
os << "(% " << *it << " sort\n";
void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
Debug("pf::array") << "Array: print deferred declarations called" << std::endl;
+ unsigned count = 1;
for (ExprSet::const_iterator it = d_skolemDeclarations.begin(); it != d_skolemDeclarations.end(); ++it) {
Expr term = *it;
Node equality = ProofManager::getSkolemizationManager()->getDisequality(*it);
<< "It is a witness for: " << equality << std::endl;
std::ostringstream newSkolemLiteral;
- newSkolemLiteral << ".sl" << d_skolemToLiteral.size();
+ newSkolemLiteral << ".sl" << count++;
std::string skolemLiteral = newSkolemLiteral.str();
d_skolemToLiteral[*it] = skolemLiteral;
Node array_two = equality[0][1];
LetMap map;
-
os << "(ext _ _ ";
printTerm(array_one.toExpr(), os, map);
os << " ";
printTerm(array_two.toExpr(), os, map);
os << " (\\ ";
- printTerm(*it, os, map);
+ os << ProofManager::sanitize(*it);
os << " (\\ ";
os << skolemLiteral.c_str();
os << "\n";
}
}
+void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ // Nothing to do here at this point.
+}
+
} /* CVC4 namespace */
//proof object outputted by TheoryARRAY
class ProofArray : public Proof {
private:
+ class ArrayProofPrinter : public theory::eq::EqProof::PrettyPrinter {
+ public:
+ ArrayProofPrinter() : d_row(0), d_row1(0), d_ext(0) {
+ }
+
+ std::string printTag(unsigned tag) {
+ if (tag == theory::eq::MERGED_THROUGH_CONGRUENCE) return "Congruence";
+ if (tag == theory::eq::MERGED_THROUGH_EQUALITY) return "Pure Equality";
+ if (tag == theory::eq::MERGED_THROUGH_REFLEXIVITY) return "Reflexivity";
+ if (tag == theory::eq::MERGED_THROUGH_CONSTANTS) return "Constants";
+ if (tag == theory::eq::MERGED_THROUGH_TRANS) return "Transitivity";
+
+ if (tag == d_row) return "Read Over Write";
+ if (tag == d_row1) return "Read Over Write (1)";
+ if (tag == d_ext) return "Extensionality";
+
+ std::ostringstream result;
+ result << tag;
+ return result.str();
+ }
+
+ unsigned d_row;
+ unsigned d_row1;
+ unsigned d_ext;
+ };
+
Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
theory::eq::EqProof* pf,
unsigned tb,
unsigned d_reasonRow1;
/** Merge tag for EXT applications */
unsigned d_reasonExt;
+
+ ArrayProofPrinter d_proofPrinter;
public:
ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {}
//it is simply an equality engine proof
void setRowMergeTag(unsigned tag);
void setRow1MergeTag(unsigned tag);
void setExtMergeTag(unsigned tag);
+
+ unsigned getRowMergeTag() const;
+ unsigned getRow1MergeTag() const;
+ unsigned getExtMergeTag() const;
};
namespace theory {
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
};
**/
-#include "proof/bitvector_proof.h"
#include "options/bv_options.h"
+#include "proof/array_proof.h"
+#include "proof/bitvector_proof.h"
#include "proof/clause_id.h"
+#include "proof/proof_output_channel.h"
#include "proof/proof_utils.h"
#include "proof/sat_proof_implementation.h"
#include "prop/bvminisat/bvminisat.h"
}
void BitVectorProof::registerTermBB(Expr term) {
+ Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term << " )" << std::endl;
+
if (d_seenBBTerms.find(term) != d_seenBBTerms.end())
return;
d_seenBBTerms.insert(term);
d_bbTerms.push_back(term);
+
+ // If this term gets used in the final proof, we will want to register it. However,
+ // we don't know this at this point; and when the theory proof engine sees it, if it belongs
+ // to another theory, it won't register it with this proof. So, we need to tell the
+ // engine to inform us.
+
+ if (theory::Theory::theoryOf(term) != theory::THEORY_BV) {
+ Debug("pf::bv") << "\tMarking term " << term << " for future BV registration" << std::endl;
+ d_proofEngine->markTermForFutureRegistration(term, theory::THEORY_BV);
+ }
}
void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) {
+ Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom << ", " << atom_bb << " )" << std::endl;
+
Expr def = atom.iffExpr(atom_bb);
- d_bbAtoms.insert(std::make_pair(atom, def));
+ d_bbAtoms.insert(std::make_pair(atom, def));
registerTerm(atom);
+
+ // Register the atom's terms for bitblasting
+ registerTermBB(atom[0]);
+ registerTermBB(atom[1]);
}
void BitVectorProof::registerTerm(Expr term) {
+ Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl;
+
d_usedBB.insert(term);
if (Theory::isLeafOf(term, theory::THEORY_BV) &&
d_declarations.insert(term);
}
+ Debug("pf::bv") << "Going to register children: " << std::endl;
+ for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+ Debug("pf::bv") << "\t" << term[i] << std::endl;
+ }
+
// don't care about parametric operators for bv?
for (unsigned i = 0; i < term.getNumChildren(); ++i) {
d_proofEngine->registerTerm(term[i]);
}
std::string BitVectorProof::getBBTermName(Expr expr) {
+ Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" << expr.getId() << std::endl;
std::ostringstream os;
os << "bt"<< expr.getId();
return os.str();
}
void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl) {
+ Debug("pf::bv") << "BitVectorProof::endBVConflict called" << std::endl;
+
std::vector<Expr> expr_confl;
for (int i = 0; i < confl.size(); ++i) {
prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]);
Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
expr_confl.push_back(expr_lit);
}
+
Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl);
Debug("pf::bv") << "Make conflict for " << conflict << std::endl;
ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl);
d_bbConflictMap[conflict] = clause_id;
d_resolutionProof->endResChain(clause_id);
- Debug("pf::bv") << "BitVectorProof::endBVConflict id"<<clause_id<< " => " << conflict << "\n";
+ Debug("pf::bv") << "BitVectorProof::endBVConflict id" <<clause_id<< " => " << conflict << "\n";
d_isAssumptionConflict = false;
}
void BitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) {
+
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
Debug("pf::bv") << "Construct full proof." << std::endl;
d_resolutionProof->constructProof();
return;
}
- for(unsigned i = 0; i < conflicts.size(); ++i) {
+
+ for (unsigned i = 0; i < conflicts.size(); ++i) {
Expr confl = conflicts[i];
- Debug("pf::bv") << "Finalize conflict " << confl << std::endl;
- //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end());
- if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){
+ Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl;
+
+ // Special case: if the conflict has a (true) or a (not false) in it, it is trivial...
+ bool ignoreConflict = false;
+ if ((confl.isConst() && confl.getConst<bool>()) ||
+ (confl.getKind() == kind::NOT && confl[0].isConst() && !confl[0].getConst<bool>())) {
+ ignoreConflict = true;
+ } else if (confl.getKind() == kind::OR) {
+ for (unsigned k = 0; k < confl.getNumChildren(); ++k) {
+ if ((confl[k].isConst() && confl[k].getConst<bool>()) ||
+ (confl[k].getKind() == kind::NOT && confl[k][0].isConst() && !confl[k][0].getConst<bool>())) {
+ ignoreConflict = true;
+ }
+ }
+ }
+ if (ignoreConflict) {
+ Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)" << std::endl;
+ continue;
+ }
+
+ if (d_bbConflictMap.find(confl) != d_bbConflictMap.end()) {
ClauseId id = d_bbConflictMap[confl];
d_resolutionProof->collectClauses(id);
- }else{
- Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl;
+ } else {
+ // There is no exact match for our conflict, but maybe it is a subset of another conflict
+ ExprToClauseId::const_iterator it;
+ bool matchFound = false;
+ for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
+ Expr possibleMatch = it->first;
+ if (possibleMatch.getKind() != kind::OR) {
+ // This is a single-node conflict. If this node is in the conflict we're trying to prove,
+ // we have a match.
+ for (unsigned k = 0; k < confl.getNumChildren(); ++k) {
+ if (confl[k] == possibleMatch) {
+ matchFound = true;
+ d_resolutionProof->collectClauses(it->second);
+ break;
+ }
+ }
+ } else {
+ if (possibleMatch.getNumChildren() > confl.getNumChildren())
+ continue;
+
+ unsigned k = 0;
+ bool matching = true;
+ for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) {
+ // j is the index in possibleMatch
+ // k is the index in confl
+ while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) {
+ ++k;
+ }
+ if (k == confl.getNumChildren()) {
+ // We couldn't find a match for possibleMatch[j], so not a match
+ matching = false;
+ break;
+ }
+ }
+
+ if (matching) {
+ Debug("pf::bv") << "Collecting info from a sub-conflict" << std::endl;
+ d_resolutionProof->collectClauses(it->second);
+ matchFound = true;
+ break;
+ }
+ }
+ }
+
+ if (!matchFound) {
+ Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl
+ << "Dumping existing conflicts:" << std::endl;
+
+ i = 0;
+ for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
+ ++i;
+ Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl;
+ }
+
+ Unreachable();
+ }
}
}
}
printBitOf(term, os, map);
return;
}
- case kind::VARIABLE:
+
+ case kind::VARIABLE: {
+ os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")";
+ return;
+ }
+
case kind::SKOLEM: {
- os << "(a_var_bv " << utils::getSize(term)<<" " << ProofManager::sanitize(term) <<")";
+
+ // TODO: we need to distinguish between "real" skolems (e.g. from array) and "fake" skolems,
+ // like ITE terms. Is there a more elegant way?
+
+ if (ProofManager::getSkolemizationManager()->isSkolem(term)) {
+ os << ProofManager::sanitize(term);
+ } else {
+ os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")";
+ }
return;
}
+
default:
Unreachable();
}
<< ", var = " << var << std::endl;
os << "(bitof ";
- if (var.getKind() == kind::VARIABLE || var.getKind() == kind::SKOLEM) {
- // If var is "simple", we can just sanitize and print
- os << ProofManager::sanitize(var);
- } else {
- // If var is "complex", it can belong to another theory. Therefore, dispatch again.
- d_proofEngine->printBoundTerm(var, os, map);
- }
-
+ os << d_exprToVariableName[var];
os << " " << bit << ")";
}
void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) {
Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl;
-
Assert (type.isBitVector());
unsigned width = utils::getSize(type);
os << "(BitVec "<<width<<")";
}
void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+ Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" << std::endl;
Expr conflict = utils::mkSortedExpr(kind::OR, lemma);
+ Debug("pf::bv") << "\tconflict = " << conflict << std::endl;
+
if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) {
std::ostringstream lemma_paren;
for (unsigned i = 0; i < lemma.size(); ++i) {
// print corresponding literal in bv sat solver
prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
os << pm->getAtomName(bb_var, "bb");
- os <<"(\\unit"<<bb_var<<"\n";
+ os <<"(\\ unit"<<bb_var<<"\n";
lemma_paren <<")";
}
Expr lem = utils::mkOr(lemma);
d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren);
os <<lemma_paren.str();
} else {
- Unreachable(); // If we were to reach here, we would crash because BV replay is currently not supported
- // in TheoryProof::printTheoryLemmaProof()
- Debug("pf::bv") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl;
- BitVectorProof::printTheoryLemmaProof( lemma, os, paren );
+ Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching sub-conflict..."
+ << std::endl;
+
+ bool matching;
+
+ ExprToClauseId::const_iterator it;
+ unsigned i = 0;
+ for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
+ // Our conflict is sorted, and the records are also sorted.
+ ++i;
+ Expr possibleMatch = it->first;
+
+ if (possibleMatch.getKind() != kind::OR) {
+ // This is a single-node conflict. If this node is in the conflict we're trying to prove,
+ // we have a match.
+ matching = false;
+
+ for (unsigned k = 0; k < conflict.getNumChildren(); ++k) {
+ if (conflict[k] == possibleMatch) {
+ matching = true;
+ break;
+ }
+ }
+ } else {
+ if (possibleMatch.getNumChildren() > conflict.getNumChildren())
+ continue;
+
+ unsigned k = 0;
+
+ matching = true;
+ for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) {
+ // j is the index in possibleMatch
+ // k is the index in conflict
+ while (k < conflict.getNumChildren() && conflict[k] != possibleMatch[j]) {
+ ++k;
+ }
+ if (k == conflict.getNumChildren()) {
+ // We couldn't find a match for possibleMatch[j], so not a match
+ matching = false;
+ break;
+ }
+ }
+ }
+
+ if (matching) {
+ Debug("pf::bv") << "Found a match with conflict #" << i << ": " << std::endl << possibleMatch << std::endl;
+ // The rest is just a copy of the usual handling, if a precise match is found.
+ // We only use the literals that appear in the matching conflict, though, and not in the
+ // original lemma - as these may not have even been bit blasted!
+ std::ostringstream lemma_paren;
+
+ if (possibleMatch.getKind() == kind::OR) {
+ for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) {
+ Expr lit = possibleMatch[i];
+
+ if (lit.getKind() == kind::NOT) {
+ os << "(intro_assump_t _ _ _ ";
+ } else {
+ os << "(intro_assump_f _ _ _ ";
+ }
+ lemma_paren <<")";
+ // print corresponding literal in main sat solver
+ ProofManager* pm = ProofManager::currentPM();
+ CnfProof* cnf = pm->getCnfProof();
+ prop::SatLiteral main_lit = cnf->getLiteral(lit);
+ os << pm->getLitName(main_lit);
+ os <<" ";
+ // print corresponding literal in bv sat solver
+ prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
+ os << pm->getAtomName(bb_var, "bb");
+ os <<"(\\ unit"<<bb_var<<"\n";
+ lemma_paren <<")";
+ }
+ } else {
+ // The conflict only consists of one node, either positive or negative.
+ Expr lit = possibleMatch;
+ if (lit.getKind() == kind::NOT) {
+ os << "(intro_assump_t _ _ _ ";
+ } else {
+ os << "(intro_assump_f _ _ _ ";
+ }
+ lemma_paren <<")";
+ // print corresponding literal in main sat solver
+ ProofManager* pm = ProofManager::currentPM();
+ CnfProof* cnf = pm->getCnfProof();
+ prop::SatLiteral main_lit = cnf->getLiteral(lit);
+ os << pm->getLitName(main_lit);
+ os <<" ";
+ // print corresponding literal in bv sat solver
+ prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
+ os << pm->getAtomName(bb_var, "bb");
+ os <<"(\\ unit"<<bb_var<<"\n";
+ lemma_paren <<")";
+ }
+
+ ClauseId lemma_id = it->second;
+ d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren);
+ os <<lemma_paren.str();
+
+ return;
+ }
+ }
+
+ Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl
+ << "Dumping existing conflicts:" << std::endl;
+
+ i = 0;
+ for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
+ ++i;
+ Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl;
+ }
+
+ Unreachable();
}
}
ExprSet::const_iterator it = d_declarations.begin();
ExprSet::const_iterator end = d_declarations.end();
for (; it != end; ++it) {
- os << "(% " << ProofManager::sanitize(*it) <<" var_bv\n";
+ if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)) {
+ d_exprToVariableName[*it] = ProofManager::sanitize(*it);
+ } else {
+ d_exprToVariableName[*it] = assignAlias(*it);
+ }
+
+ os << "(% " << d_exprToVariableName[*it] <<" var_bv" << "\n";
paren <<")";
}
}
// Nothing to do here at this point.
}
+void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ // Print "trust" statements to bind complex bv variables to their associated terms
+
+ ExprToString::const_iterator it = d_assignedAliases.begin();
+ ExprToString::const_iterator end = d_assignedAliases.end();
+
+ for (; it != end; ++it) {
+ Debug("pf::bv") << "Printing aliasing declaration for: " << *it << std::endl;
+ std::stringstream declaration;
+ declaration << ".fbvd" << d_aliasToBindDeclaration.size();
+ d_aliasToBindDeclaration[it->second] = declaration.str();
+
+ os << "(th_let_pf _ ";
+
+ os << "(trust_f ";
+ os << "(= (BitVec " << utils::getSize(it->first) << ") ";
+ os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") ";
+ LetMap emptyMap;
+ d_proofEngine->printBoundTerm(it->first, os, emptyMap);
+ os << ")) ";
+ os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n";
+ paren << "))";
+ }
+
+ os << "\n";
+}
+
void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
// TODO: once we have the operator elimination rules remove those that we
// eliminated
Assert (term.getType().isBitVector());
Kind kind = term.getKind();
- if (Theory::isLeafOf(term, theory::THEORY_BV) &&
- !term.isConst()) {
- os << "(bv_bbl_var "<<utils::getSize(term) << " " << ProofManager::sanitize(term) <<" _ )";
+ if (Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) {
+ // A term is a leaf if it has no children, or if it belongs to another theory
+ os << "(bv_bbl_var " << utils::getSize(term) << " " << d_exprToVariableName[term];
+ os << " _ )";
return;
}
case kind::BITVECTOR_PLUS :
case kind::BITVECTOR_SUB :
case kind::BITVECTOR_CONCAT : {
- for (unsigned i =0; i < term.getNumChildren() - 1; ++i) {
+ Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl;
+
+ for (int i = term.getNumChildren() - 1; i > 0; --i) {
os <<"(bv_bbl_"<< utils::toLFSCKind(kind);
+
+ if (i > 1) {
+ // This is not the inner-most operation; only child i+1 can be aliased
+ if (hasAlias(term[i])) {os << "_alias_2";}
+ } else {
+ // This is the inner-most operation; both children can be aliased
+ if (hasAlias(term[i-1]) || hasAlias(term[i])) {os << "_alias";}
+ if (hasAlias(term[i-1])) {os << "_1";}
+ if (hasAlias(term[i])) {os << "_2";}
+ }
+
if (kind == kind::BITVECTOR_CONCAT) {
- os << " " << utils::getSize(term) <<" _ ";
+ os << " " << utils::getSize(term) << " _";
}
- os <<" _ _ _ _ _ _ ";
+ os << " _ _ _ _ _ _ ";
}
- os << getBBTermName(term[0]) <<" ";
+
+ if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
+ os << getBBTermName(term[0]) << " ";
for (unsigned i = 1; i < term.getNumChildren(); ++i) {
+ if (hasAlias(term[i])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[i]]] << " ";}
os << getBBTermName(term[i]);
os << ") ";
}
return;
}
+
case kind::BITVECTOR_NEG :
case kind::BITVECTOR_NOT :
case kind::BITVECTOR_ROTATE_LEFT :
case kind::BITVECTOR_ROTATE_RIGHT : {
- os <<"(bv_bbl_"<<utils::toLFSCKind(kind);
- os <<" _ _ _ _ ";
+ os << "(bv_bbl_"<<utils::toLFSCKind(kind);
+ os << " _ _ _ _ ";
os << getBBTermName(term[0]);
- os <<")";
+ os << ")";
return;
}
case kind::BITVECTOR_EXTRACT : {
- os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" ";
- os << utils::getSize(term) << " ";
+ os <<"(bv_bbl_"<<utils::toLFSCKind(kind);
+
+ if (hasAlias(term[0])) {os << "_alias";};
+
+ os << " " << utils::getSize(term) << " ";
os << utils::getExtractHigh(term) << " ";
os << utils::getExtractLow(term) << " ";
os << " _ _ _ _ ";
+
+ if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
+
os << getBBTermName(term[0]);
os <<")";
return;
case kind::BITVECTOR_REPEAT :
case kind::BITVECTOR_ZERO_EXTEND :
case kind::BITVECTOR_SIGN_EXTEND : {
- os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" ";
+ os <<"(bv_bbl_" <<utils::toLFSCKind(kind) << (hasAlias(term[0]) ? "_alias " : " ");
os << utils::getSize(term) <<" ";
if (term.getKind() == kind::BITVECTOR_REPEAT) {
unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
os << amount;
}
+
os <<" _ _ _ _ ";
+ if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
os << getBBTermName(term[0]);
os <<")";
return;
}
}
-void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) {
+void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) {
Kind kind = atom.getKind();
switch(kind) {
case kind::BITVECTOR_ULT :
case kind::BITVECTOR_SLE :
case kind::BITVECTOR_SGT :
case kind::BITVECTOR_SGE :
- case kind::EQUAL:
- {
- os <<"(bv_bbl_" << utils::toLFSCKind(atom.getKind());
+ case kind::EQUAL: {
+ Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl;
+
+ os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind());
+
+ if (hasAlias(atom[0]) || hasAlias(atom[1])) {os << "_alias";}
+ if (hasAlias(atom[0])) {os << "_1";}
+ if (hasAlias(atom[1])) {os << "_2";}
+
+ if (swap) {os << "_swap";}
+
os << " _ _ _ _ _ _ ";
- os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")";
+
+ if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";}
+ os << getBBTermName(atom[0]);
+
+ os << " ";
+
+ if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";}
+ os << getBBTermName(atom[1]);
+
+ os << ")";
return;
}
default:
}
}
+void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) {
+ Assert(atom.getKind() == kind::EQUAL);
+
+ os << "(bv_bbl_=_false";
+ os << " _ _ _ _ _ _ ";
+ if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";}
+ os << getBBTermName(atom[0]);
+
+ os << " ";
+
+ if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";}
+ os << getBBTermName(atom[1]);
+
+ os << ")";
+}
void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) {
// bit-blast terms
+ {
+ Debug("pf::bv") << "LFSCBitVectorProof::printBitblasting: the bitblasted terms are: " << std::endl;
+ std::vector<Expr>::const_iterator it = d_bbTerms.begin();
+ std::vector<Expr>::const_iterator end = d_bbTerms.end();
+
+ Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
+
+ for (; it != end; ++it) {
+ if (d_usedBB.find(*it) == d_usedBB.end()) {
+ Debug("pf::bv") << "\t" << *it << "\t(UNUSED)" << std::endl;
+ } else {
+ Debug("pf::bv") << "\t" << *it << std::endl;
+ }
+ }
+
+ Debug("pf::bv") << std::endl;
+ }
+
std::vector<Expr>::const_iterator it = d_bbTerms.begin();
std::vector<Expr>::const_iterator end = d_bbTerms.end();
for (; it != end; ++it) {
if (d_usedBB.find(*it) == d_usedBB.end() &&
options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER)
continue;
- os <<"(decl_bblast _ _ _ ";
+
+ os << "(decl_bblast _ _ _ ";
printTermBitblasting(*it, os);
- os << "(\\ "<< getBBTermName(*it);
- paren <<"\n))";
+ os << "(\\ "<< getBBTermName(*it) << "\n";
+ paren << "))";
}
// bit-blast atoms
ExprToExpr::const_iterator ait = d_bbAtoms.begin();
bool val = ait->first.getConst<bool>();
os << "(iff_symm " << (val ? "true" : "false" ) << ")";
} else {
- printAtomBitblasting(ait->first, os);
+ Assert(ait->first == ait->second[0]);
+
+ bool swap = false;
+ if (ait->first.getKind() == kind::EQUAL) {
+ Expr bitwiseEquivalence = ait->second[1];
+ if ((bitwiseEquivalence.getKind() == kind::CONST_BOOLEAN) && !bitwiseEquivalence.getConst<bool>()) {
+ printAtomBitblastingToFalse(ait->first, os);
+ } else {
+ if (bitwiseEquivalence.getKind() != kind::AND) {
+ // Just one bit
+ if (bitwiseEquivalence.getNumChildren() > 0 && bitwiseEquivalence[0].getKind() == kind::BITVECTOR_BITOF) {
+ swap = (ait->first[1] == bitwiseEquivalence[0][0]);
+ }
+ } else {
+ // Multiple bits
+ if (bitwiseEquivalence[0].getNumChildren() > 0 &&
+ bitwiseEquivalence[0][0].getKind() == kind::BITVECTOR_BITOF) {
+ swap = (ait->first[1] == bitwiseEquivalence[0][0][0]);
+ } else if (bitwiseEquivalence[0].getNumChildren() > 0 &&
+ bitwiseEquivalence[0][1].getKind() == kind::BITVECTOR_BITOF) {
+ swap = (ait->first[0] == bitwiseEquivalence[0][1][0]);
+ }
+ }
+
+ printAtomBitblasting(ait->first, os, swap);
+ }
+ } else {
+ printAtomBitblasting(ait->first, os, swap);
+ }
}
os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n";
used_lemmas);
Assert (used_lemmas.empty());
+ IdToSatClause::iterator it2;
+ Debug("pf::bv") << std::endl << "BV Used inputs: " << std::endl;
+ for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) {
+ Debug("pf::bv") << "\t input = " << *(it2->second) << std::endl;
+ }
+ Debug("pf::bv") << std::endl;
+
// print mapping between theory atoms and internal SAT variables
- os << ";; BB atom mapping\n";
+ os << std::endl << ";; BB atom mapping\n" << std::endl;
+
+ std::set<Node> atoms;
+ d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
- NodeSet atoms;
- d_cnfProof->collectAtomsForClauses(used_inputs,atoms);
+ std::set<Node>::iterator atomIt;
+ Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl;
+ for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
+ Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl;
+ }
+ Debug("pf::bv") << std::endl;
// first print bit-blasting
printBitblasting(os, paren);
// print CNF conversion proof for bit-blasted facts
d_cnfProof->printAtomMapping(atoms, os, paren);
- os << ";; Bit-blasting definitional clauses \n";
+ os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl;
for (IdToSatClause::iterator it = used_inputs.begin();
it != used_inputs.end(); ++it) {
d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren);
}
- os << ";; Bit-blasting learned clauses \n";
+ os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl;
d_resolutionProof->printResolutions(os, paren);
}
+std::string LFSCBitVectorProof::assignAlias(Expr expr) {
+ static unsigned counter = 0;
+ Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end());
+ std::stringstream ss;
+ ss << "fbv" << counter++;
+ Debug("pf::bv") << "assignAlias( " << expr << ") = " << ss.str() << std::endl;
+ d_assignedAliases[expr] = ss.str();
+ return ss.str();
+}
+
+bool LFSCBitVectorProof::hasAlias(Expr expr) {
+ return d_assignedAliases.find(expr) != d_assignedAliases.end();
+}
+
} /* namespace CVC4 */
typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId;
typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr;
+typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString;
class BitVectorProof : public TheoryProof {
protected:
virtual void registerTerm(Expr term);
virtual void printTermBitblasting(Expr term, std::ostream& os) = 0;
- virtual void printAtomBitblasting(Expr term, std::ostream& os) = 0;
+ virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0;
+ virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0;
virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0;
virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0;
void printPredicate(Expr term, std::ostream& os, const LetMap& map);
void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map);
void printBitOf(Expr term, std::ostream& os, const LetMap& map);
+
+ ExprToString d_exprToVariableName;
+ ExprToString d_assignedAliases;
+ std::map<std::string, std::string> d_aliasToBindDeclaration;
+ std::string assignAlias(Expr expr);
+ bool hasAlias(Expr expr);
public:
LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
:BitVectorProof(bv, proofEngine)
virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
virtual void printTermBitblasting(Expr term, std::ostream& os);
- virtual void printAtomBitblasting(Expr term, std::ostream& os);
+ virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
+ virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
virtual void printBitblasting(std::ostream& os, std::ostream& paren);
virtual void printResolutionProof(std::ostream& os, std::ostream& paren);
};
#include "proof/clause_id.h"
#include "proof/proof_manager.h"
+#include "proof/proof_utils.h"
#include "proof/theory_proof.h"
#include "prop/cnf_stream.h"
#include "prop/minisat/minisat.h"
: d_cnfStream(stream)
, d_clauseToAssertion(ctx)
, d_assertionToProofRule(ctx)
- , d_clauseIdToOwnerTheory(ctx)
, d_currentAssertionStack()
, d_currentDefinitionStack()
, d_clauseToDefinition(ctx)
setClauseAssertion(clause, current_assertion);
setClauseDefinition(clause, current_expr);
- registerExplanationLemma(clause);
}
void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
d_assertionToProofRule.insert(assertion, reason);
}
-void CnfProof::registerExplanationLemma(ClauseId clauseId) {
- d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory());
+LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) {
+ Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end());
+ return d_lemmaToProofRecipe[lemma];
}
-theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) {
- Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end());
- return d_clauseIdToOwnerTheory[clause];
+bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) {
+ return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end();
}
-
void CnfProof::setCnfDependence(Node from, Node to) {
Debug("proof:cnf") << "CnfProof::setCnfDependence "
<< "from " << from << std::endl
return d_currentAssertionStack.back();
}
-void CnfProof::setExplainerTheory(theory::TheoryId theory) {
- d_explainerTheory = theory;
-}
-
-theory::TheoryId CnfProof::getExplainerTheory() {
- return d_explainerTheory;
+void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) {
+ Assert(proofRecipe);
+ Assert(proofRecipe->getNumSteps() > 0);
+ d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe;
}
void CnfProof::pushCurrentDefinition(Node definition) {
return d_currentDefinitionStack.back();
}
-
Node CnfProof::getAtom(prop::SatVariable var) {
prop::SatLiteral lit (var);
Node node = d_cnfStream->getNode(lit);
return node;
}
-
void CnfProof::collectAtoms(const prop::SatClause* clause,
- NodeSet& atoms) {
+ std::set<Node>& atoms) {
for (unsigned i = 0; i < clause->size(); ++i) {
prop::SatLiteral lit = clause->operator[](i);
prop::SatVariable var = lit.getSatVariable();
TNode atom = getAtom(var);
if (atoms.find(atom) == atoms.end()) {
- Assert (atoms.find(atom) == atoms.end());
atoms.insert(atom);
}
}
return d_cnfStream->getLiteral(atom);
}
+bool CnfProof::hasLiteral(TNode atom) {
+ return d_cnfStream->hasLiteral(atom);
+}
+
+void CnfProof::ensureLiteral(TNode atom, bool noPreregistration) {
+ d_cnfStream->ensureLiteral(atom, noPreregistration);
+}
+
void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses,
- NodeSet& atom_map) {
+ std::set<Node>& atoms) {
IdToSatClause::const_iterator it = clauses.begin();
for (; it != clauses.end(); ++it) {
const prop::SatClause* clause = it->second;
- collectAtoms(clause, atom_map);
+ collectAtoms(clause, atoms);
}
+}
+
+void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
+ std::set<Node>& atoms,
+ NodePairSet& rewrites) {
+ IdToSatClause::const_iterator it = lemmaClauses.begin();
+ for (; it != lemmaClauses.end(); ++it) {
+ const prop::SatClause* clause = it->second;
+
+ // TODO: just calculate the map from ID to recipe once,
+ // instead of redoing this over and over again
+ std::vector<Expr> clause_expr;
+ std::set<Node> clause_expr_nodes;
+ for(unsigned i = 0; i < clause->size(); ++i) {
+ prop::SatLiteral lit = (*clause)[i];
+ Node node = getAtom(lit.getSatVariable());
+ Expr atom = node.toExpr();
+ if (atom.isConst()) {
+ Assert (atom == utils::mkTrue());
+ continue;
+ }
+ clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
+ }
+
+ LemmaProofRecipe recipe = getProofRecipe(clause_expr_nodes);
+ for (unsigned i = 0; i < recipe.getNumSteps(); ++i) {
+ const LemmaProofRecipe::ProofStep* proofStep = recipe.getStep(i);
+ Node atom = proofStep->getLiteral();
+
+ if (atom == Node()) {
+ // The last proof step always has the empty node as its target...
+ continue;
+ }
+
+ if (atom.getKind() == kind::NOT) {
+ atom = atom[0];
+ }
+
+ atoms.insert(atom);
+ }
+
+ LemmaProofRecipe::RewriteIterator rewriteIt;
+ for (rewriteIt = recipe.rewriteBegin(); rewriteIt != recipe.rewriteEnd(); ++rewriteIt) {
+ rewrites.insert(NodePair(rewriteIt->first, rewriteIt->second));
+
+ // The unrewritten terms also need to have literals, so insert them into atoms
+ Node rewritten = rewriteIt->first;
+ if (rewritten.getKind() == kind::NOT) {
+ rewritten = rewritten[0];
+ }
+ atoms.insert(rewritten);
+ }
+ }
}
void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
}
}
-void LFSCCnfProof::printAtomMapping(const NodeSet& atoms,
+void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren) {
- NodeSet::const_iterator it = atoms.begin();
- NodeSet::const_iterator end = atoms.end();
+ std::set<Node>::const_iterator it = atoms.begin();
+ std::set<Node>::const_iterator end = atoms.end();
- for (;it != end; ++it) {
+ for (;it != end; ++it) {
os << "(decl_atom ";
Node atom = *it;
prop::SatVariable var = getLiteral(atom).getSatVariable();
LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
pe->printLetTerm(atom.toExpr(), os);
- os << " (\\ " << ProofManager::getVarName(var, d_name)
- << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
+ os << " (\\ " << ProofManager::getVarName(var, d_name);
+ os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
paren << ")))";
}
}
const prop::SatClause* clause,
std::ostream& os,
std::ostream& paren) {
+ Debug("cnf-pf") << std::endl << std::endl << "LFSCCnfProof::printCnfProofForClause( " << id << " ) starting "
+ << std::endl;
+
os << "(satlem _ _ ";
std::ostringstream clause_paren;
printClause(*clause, os, clause_paren);
// and prints the proof of the top-level formula
bool is_input = printProofTopLevel(base_assertion, os_base);
+ if (is_input) {
+ Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl;
+ }
+
//get base assertion with polarity
bool base_pol = base_assertion.getKind()!=kind::NOT;
base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion;
if( !pols[0] || num_nots_1==1 ){
os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") ";
}else{
+ Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl;
os_base_n << ProofManager::getLitName(lit1, d_name) << " ";
}
Assert( elimNum!=0 );
os << ")" << clause_paren.str()
<< " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
+
paren << "))";
}
#include "context/cdhashmap.h"
#include "proof/clause_id.h"
+#include "proof/lemma_proof.h"
#include "proof/sat_proof.h"
#include "util/proof.h"
typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule;
-typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory;
+typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe;
+typedef std::pair<Node, Node> NodePair;
+typedef std::set<NodePair> NodePairSet;
class CnfProof {
protected:
/** Map from assertion to reason for adding assertion **/
NodeToProofRule d_assertionToProofRule;
- /** Map from assertion to the theory that added this assertion **/
- ClauseIdToTheory d_clauseIdToOwnerTheory;
-
- /** The last theory to explain a lemma **/
- theory::TheoryId d_explainerTheory;
+ /** Map from lemma to the recipe for proving it **/
+ LemmaToRecipe d_lemmaToProofRecipe;
/** Top of stack is assertion currently being converted to CNF **/
std::vector<Node> d_currentAssertionStack;
Node getAtom(prop::SatVariable var);
prop::SatLiteral getLiteral(TNode node);
+ bool hasLiteral(TNode node);
+ void ensureLiteral(TNode node, bool noPreregistration = false);
+
void collectAtoms(const prop::SatClause* clause,
- NodeSet& atoms);
+ std::set<Node>& atoms);
void collectAtomsForClauses(const IdToSatClause& clauses,
- NodeSet& atoms);
+ std::set<Node>& atoms);
+ void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
+ std::set<Node>& atoms,
+ NodePairSet& rewrites);
void collectAssertionsForClauses(const IdToSatClause& clauses,
NodeSet& assertions);
void popCurrentDefinition();
Node getCurrentDefinition();
- void setExplainerTheory(theory::TheoryId theory);
- theory::TheoryId getExplainerTheory();
- theory::TheoryId getOwnerTheory(ClauseId clause);
-
- void registerExplanationLemma(ClauseId clauseId);
+ void setProofRecipe(LemmaProofRecipe* proofRecipe);
+ LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma);
+ bool haveProofRecipe(const std::set<Node> &lemma);
// accessors for the leaf assertions that are being converted to CNF
bool isAssertion(Node node);
Node getAssertionForClause(ClauseId clause);
/** Virtual methods for printing things **/
- virtual void printAtomMapping(const NodeSet& atoms,
+ virtual void printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren) = 0;
{}
~LFSCCnfProof() {}
- void printAtomMapping(const NodeSet& atoms,
+ void printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren);
--- /dev/null
+/********************* */
+/*! \file lemma_proof.h
+** \verbatim
+**
+** \brief A class for recoding the steps required in order to prove a theory lemma.
+**
+** A class for recoding the steps required in order to prove a theory lemma.
+**
+**/
+
+#include "proof/lemma_proof.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+
+LemmaProofRecipe::ProofStep::ProofStep(theory::TheoryId theory, Node literalToProve) :
+ d_theory(theory), d_literalToProve(literalToProve) {
+}
+
+theory::TheoryId LemmaProofRecipe::ProofStep::getTheory() const {
+ return d_theory;
+}
+
+Node LemmaProofRecipe::ProofStep::getLiteral() const {
+ return d_literalToProve;
+}
+
+void LemmaProofRecipe::ProofStep::addAssertion(const Node& assertion) {
+ d_assertions.insert(assertion);
+}
+
+std::set<Node> LemmaProofRecipe::ProofStep::getAssertions() const {
+ return d_assertions;
+}
+
+void LemmaProofRecipe::addStep(ProofStep& proofStep) {
+ std::list<ProofStep>::iterator existingFirstStep = d_proofSteps.begin();
+ d_proofSteps.push_front(proofStep);
+}
+
+std::set<Node> LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const {
+ Assert(index < d_proofSteps.size());
+
+ std::set<Node> existingAssertions = getBaseAssertions();
+
+ std::list<ProofStep>::const_iterator step = d_proofSteps.begin();
+ while (index != 0) {
+ existingAssertions.insert(step->getLiteral().negate());
+ ++step;
+ --index;
+ }
+
+ std::set<Node> neededAssertions = step->getAssertions();
+
+ std::set<Node> result;
+ std::set_difference(neededAssertions.begin(), neededAssertions.end(),
+ existingAssertions.begin(), existingAssertions.end(),
+ std::inserter(result, result.begin()));
+ return result;
+}
+
+void LemmaProofRecipe::dump(const char *tag) const {
+
+ if (d_proofSteps.size() == 1) {
+ Debug(tag) << std::endl << "[Simple lemma]" << std::endl << std::endl;
+ }
+
+ unsigned count = 1;
+ Debug(tag) << "Base assertions:" << std::endl;
+ for (std::set<Node>::iterator baseIt = d_baseAssertions.begin();
+ baseIt != d_baseAssertions.end();
+ ++baseIt) {
+ Debug(tag) << "\t#" << count << ": " << "\t" << *baseIt << std::endl;
+ ++count;
+ }
+
+ Debug(tag) << std::endl << std::endl << "Proof steps:" << std::endl;
+
+ count = 1;
+ for (std::list<ProofStep>::const_iterator step = d_proofSteps.begin(); step != d_proofSteps.end(); ++step) {
+ Debug(tag) << "\tStep #" << count << ": " << "\t[" << step->getTheory() << "] ";
+ if (step->getLiteral() == Node()) {
+ Debug(tag) << "Contradiction";
+ } else {
+ Debug(tag) << step->getLiteral();
+ }
+
+ Debug(tag) << std::endl;
+
+ std::set<Node> missingAssertions = getMissingAssertionsForStep(count - 1);
+ for (std::set<Node>::const_iterator it = missingAssertions.begin(); it != missingAssertions.end(); ++it) {
+ Debug(tag) << "\t\t\tMissing assertion for step: " << *it << std::endl;
+ }
+
+ Debug(tag) << std::endl;
+ ++count;
+ }
+
+ if (!d_assertionToExplanation.empty()) {
+ Debug(tag) << std::endl << "Rewrites used:" << std::endl;
+ count = 1;
+ for (std::map<Node, Node>::const_iterator rewrite = d_assertionToExplanation.begin();
+ rewrite != d_assertionToExplanation.end();
+ ++rewrite) {
+ Debug(tag) << "\tRewrite #" << count << ":" << std::endl
+ << "\t\t" << rewrite->first
+ << std::endl << "\t\trewritten into" << std::endl
+ << "\t\t" << rewrite->second
+ << std::endl << std::endl;
+ ++count;
+ }
+ }
+}
+
+void LemmaProofRecipe::addBaseAssertion(Node baseAssertion) {
+ d_baseAssertions.insert(baseAssertion);
+}
+
+std::set<Node> LemmaProofRecipe::getBaseAssertions() const {
+ return d_baseAssertions;
+}
+
+theory::TheoryId LemmaProofRecipe::getTheory() const {
+ Assert(d_proofSteps.size() > 0);
+ return d_proofSteps.back().getTheory();
+}
+
+void LemmaProofRecipe::addRewriteRule(Node assertion, Node explanation) {
+ if (d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()) {
+ Assert(d_assertionToExplanation[assertion] == explanation);
+ }
+
+ d_assertionToExplanation[assertion] = explanation;
+}
+
+bool LemmaProofRecipe::wasRewritten(Node assertion) const {
+ return d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end();
+}
+
+Node LemmaProofRecipe::getExplanation(Node assertion) const {
+ Assert(d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end());
+ return d_assertionToExplanation.find(assertion)->second;
+}
+
+LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteBegin() const {
+ return d_assertionToExplanation.begin();
+}
+
+LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteEnd() const {
+ return d_assertionToExplanation.end();
+}
+
+bool LemmaProofRecipe::operator<(const LemmaProofRecipe& other) const {
+ return d_baseAssertions < other.d_baseAssertions;
+ }
+
+bool LemmaProofRecipe::simpleLemma() const {
+ return d_proofSteps.size() == 1;
+}
+
+bool LemmaProofRecipe::compositeLemma() const {
+ return !simpleLemma();
+}
+
+const LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) const {
+ Assert(index < d_proofSteps.size());
+
+ std::list<ProofStep>::const_iterator it = d_proofSteps.begin();
+ while (index != 0) {
+ ++it;
+ --index;
+ }
+
+ return &(*it);
+}
+
+LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) {
+ Assert(index < d_proofSteps.size());
+
+ std::list<ProofStep>::iterator it = d_proofSteps.begin();
+ while (index != 0) {
+ ++it;
+ --index;
+ }
+
+ return &(*it);
+}
+
+unsigned LemmaProofRecipe::getNumSteps() const {
+ return d_proofSteps.size();
+}
+
+} /* namespace CVC4 */
--- /dev/null
+/********************* */
+/*! \file lemma_proof.h
+** \verbatim
+**
+** \brief A class for recoding the steps required in order to prove a theory lemma.
+**
+** A class for recoding the steps required in order to prove a theory lemma.
+**
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__LEMMA_PROOF_H
+#define __CVC4__LEMMA_PROOF_H
+
+#include "expr/expr.h"
+#include "proof/clause_id.h"
+#include "prop/sat_solver_types.h"
+#include "util/proof.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class LemmaProofRecipe {
+public:
+ class ProofStep {
+ public:
+ ProofStep(theory::TheoryId theory, Node literalToProve);
+ theory::TheoryId getTheory() const;
+ Node getLiteral() const;
+ void addAssertion(const Node& assertion);
+ std::set<Node> getAssertions() const;
+
+ private:
+ theory::TheoryId d_theory;
+ Node d_literalToProve;
+ std::set<Node> d_assertions;
+ };
+
+ //* The lemma assertions and owner */
+ void addBaseAssertion(Node baseAssertion);
+ std::set<Node> getBaseAssertions() const;
+ theory::TheoryId getTheory() const;
+
+ //* Rewrite rules */
+ typedef std::map<Node, Node>::const_iterator RewriteIterator;
+ RewriteIterator rewriteBegin() const;
+ RewriteIterator rewriteEnd() const;
+
+ void addRewriteRule(Node assertion, Node explanation);
+ bool wasRewritten(Node assertion) const;
+ Node getExplanation(Node assertion) const;
+
+ //* Proof Steps */
+ void addStep(ProofStep& proofStep);
+ const ProofStep* getStep(unsigned index) const;
+ ProofStep* getStep(unsigned index);
+ unsigned getNumSteps() const;
+ std::set<Node> getMissingAssertionsForStep(unsigned index) const;
+ bool simpleLemma() const;
+ bool compositeLemma() const;
+
+ void dump(const char *tag) const;
+ bool operator<(const LemmaProofRecipe& other) const;
+
+private:
+ //* The list of assertions for this lemma */
+ std::set<Node> d_baseAssertions;
+
+ //* The various steps needed to derive the empty clause */
+ std::list<ProofStep> d_proofSteps;
+
+ //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */
+ std::map<Node, Node> d_assertionToExplanation;
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__LEMMA_PROOF_H */
return append(prefix+".l", lit.toInt());
}
-
std::string ProofManager::getPreprocessedAssertionName(Node node,
const std::string& prefix) {
node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node;
Assert(!lit.isNegated());
return getAtomName(lit.getSatVariable(), prefix);
}
+
std::string ProofManager::getLitName(TNode lit,
const std::string& prefix) {
- return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
+ std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
+ if (currentPM()->d_rewriteFilters.find(litName) != currentPM()->d_rewriteFilters.end()) {
+ return currentPM()->d_rewriteFilters[litName];
+ }
+
+ return litName;
}
std::string ProofManager::sanitize(TNode node) {
{}
void LFSCProof::toStream(std::ostream& out) {
+
+ Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
+
d_satProof->constructProof();
// collecting leaf clauses in resolution proof
for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
- NodeSet atoms;
+ std::set<Node> atoms;
+ NodePairSet rewrites;
// collects the atoms in the clauses
+ d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
+
+ if (!rewrites.empty()) {
+ Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
+ NodePairSet::const_iterator rewriteIt;
+ for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) {
+ Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl;
+ }
+ Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
+ } else {
+ Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
+ }
+
+ // The derived/unrewritten atoms may not have CNF literals required later on.
+ // If they don't, add them.
+ std::set<Node>::const_iterator it;
+ for (it = atoms.begin(); it != atoms.end(); ++it) {
+ Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
+ if (!d_cnfProof->hasLiteral(*it)) {
+ // For arithmetic: these literals are not normalized, causing an error in Arith.
+ if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) {
+ d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver.
+ } else {
+ d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration.
+ }
+ }
+ }
+
d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
for (NodeSet::const_iterator it = used_assertions.begin();
it != used_assertions.end(); ++it) {
utils::collectAtoms(*it, atoms);
+ // utils::collectAtoms(*it, newAtoms);
}
- NodeSet::iterator atomIt;
- Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " << std::endl << std::endl;
+ std::set<Node>::iterator atomIt;
+ Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: "
+ << std::endl << std::endl;
for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
-
- if (Debug.isOn("proof:pm")) {
- // std::cout << NodeManager::currentNM();
- Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl;
- for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) {
- Debug("proof:pm") << " " << *it << std::endl;
- }
-
- Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl;
- for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) {
- Debug("proof:pm") << " " << *it << std::endl;
- }
- }
}
-
smt::SmtScope scope(d_smtEngine);
std::ostringstream paren;
out << "(check\n";
out << " ;; Declarations\n";
// declare the theory atoms
- NodeSet::const_iterator it = atoms.begin();
- NodeSet::const_iterator end = atoms.end();
-
Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
- for(; it != end; ++it) {
+ for(it = atoms.begin(); it != atoms.end(); ++it) {
Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
d_theoryProof->registerTerm((*it).toExpr());
}
out << "(: (holds cln)\n\n";
// Have the theory proofs print deferred declarations, e.g. for skolem variables.
- out << " ;; Printing deferred declarations \n";
+ out << " ;; Printing deferred declarations \n\n";
d_theoryProof->printDeferredDeclarations(out, paren);
+ out << " ;; Printing aliasing declarations \n\n";
+ d_theoryProof->printAliasingDeclarations(out, paren);
+
+ out << " ;; Rewrites for Lemmas \n";
+ d_theoryProof->printLemmaRewrites(rewrites, out, paren);
+
// print trust that input assertions are their preprocessed form
printPreprocessedAssertions(used_assertions, out, paren);
Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
- // FIXME: for now assume all theory lemmas are in CNF form so
- // distinguish between them and inputs
- // print theory lemmas for resolution proof
-
Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
d_theoryProof->printTheoryLemmas(used_lemmas, out, paren);
Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
NodeSet::const_iterator it = assertions.begin();
NodeSet::const_iterator end = assertions.end();
+ Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl;
+
for (; it != end; ++it) {
os << "(th_let_pf _ ";
os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
paren << "))";
-
}
os << "\n";
d_printedTypes.insert(type);
}
+void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) {
+ d_rewriteFilters[original] = substitute;
+}
+
+void ProofManager::clearRewriteFilters() {
+ d_rewriteFilters.clear();
+}
+
std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) {
switch(k) {
case RULE_GIVEN:
namespace CVC4 {
+class SmtGlobals;
+
// forward declarations
namespace Minisat {
class Solver;
std::set<Type> d_printedTypes;
+ std::map<std::string, std::string> d_rewriteFilters;
+
protected:
LogicInfo d_logic;
void markPrinted(const Type& type);
bool wasPrinted(const Type& type) const;
+ void addRewriteFilter(const std::string &original, const std::string &substitute);
+ void clearRewriteFilters();
+
};/* class ProofManager */
class LFSCProof : public Proof {
--- /dev/null
+/********************* */
+/*! \file proof_output_channel.cpp
+** \verbatim
+** \brief [[ Add one-line brief description here ]]
+**
+** [[ Add lengthier description here ]]
+** \todo document this file
+**/
+
+#include "base/cvc4_assert.h"
+#include "proof_output_channel.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/valuation.h"
+
+namespace CVC4 {
+
+ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
+
+void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() {
+ Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl;
+ Assert(d_conflict.isNull());
+ Assert(!n.isNull());
+ d_conflict = n;
+ Assert(pf != NULL);
+ d_proof = pf;
+}
+
+bool ProofOutputChannel::propagate(TNode x) throw() {
+ Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x << std::endl;
+ d_propagations.insert(x);
+ return true;
+}
+
+theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, bool, bool) throw() {
+ Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl;
+ d_lemma = n;
+ return theory::LemmaStatus(TNode::null(), 0);
+}
+
+theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) throw() {
+ AlwaysAssert(false);
+ return theory::LemmaStatus(TNode::null(), 0);
+}
+
+void ProofOutputChannel::requirePhase(TNode n, bool b) throw() {
+ Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl;
+ Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl;
+}
+
+bool ProofOutputChannel::flipDecision() throw() {
+ Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl;
+ AlwaysAssert(false);
+ return false;
+}
+
+void ProofOutputChannel::setIncomplete() throw() {
+ Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl;
+ AlwaysAssert(false);
+}
+
+
+MyPreRegisterVisitor::MyPreRegisterVisitor(theory::Theory* theory)
+ : d_theory(theory)
+ , d_visited() {
+}
+
+bool MyPreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
+ return d_visited.find(current) != d_visited.end();
+}
+
+void MyPreRegisterVisitor::visit(TNode current, TNode parent) {
+ d_theory->preRegisterTerm(current);
+ d_visited.insert(current);
+}
+
+void MyPreRegisterVisitor::start(TNode node) {
+}
+
+void MyPreRegisterVisitor::done(TNode node) {
+}
+
+} /* namespace CVC4 */
--- /dev/null
+/********************* */
+/*! \file proof_output_channel.h
+ ** \verbatim
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
+#define __CVC4__PROOF_OUTPUT_CHANNEL_H
+
+#include "theory/output_channel.h"
+
+namespace CVC4 {
+
+class ProofOutputChannel : public theory::OutputChannel {
+public:
+ Node d_conflict;
+ Proof* d_proof;
+ Node d_lemma;
+ std::set<Node> d_propagations;
+
+ ProofOutputChannel();
+
+ virtual ~ProofOutputChannel() throw() {}
+
+ void conflict(TNode n, Proof* pf) throw();
+ bool propagate(TNode x) throw();
+ theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw();
+ theory::LemmaStatus splitLemma(TNode, bool) throw();
+ void requirePhase(TNode n, bool b) throw();
+ bool flipDecision() throw();
+ void setIncomplete() throw();
+};/* class ProofOutputChannel */
+
+class MyPreRegisterVisitor {
+ theory::Theory* d_theory;
+ __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
+public:
+ typedef void return_type;
+ MyPreRegisterVisitor(theory::Theory* theory);
+ bool alreadyVisited(TNode current, TNode parent);
+ void visit(TNode current, TNode parent);
+ void start(TNode node);
+ void done(TNode node);
+}; /* class MyPreRegisterVisitor */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */
namespace CVC4 {
namespace utils {
-void collectAtoms(TNode node, CVC4::NodeSet& seen) {
+void collectAtoms(TNode node, std::set<Node>& seen) {
if (seen.find(node) != seen.end())
return;
if (theory::Theory::theoryOf(node) != theory::THEORY_BOOL || node.isVar()) {
seen.insert(node);
return;
}
-
+
for (unsigned i = 0; i < node.getNumChildren(); ++i) {
collectAtoms(node[i], seen);
}
// bit-vector kinds
case kind::BITVECTOR_AND :
- return "bvand";
+ return "bvand";
case kind::BITVECTOR_OR :
- return "bvor";
+ return "bvor";
case kind::BITVECTOR_XOR :
- return "bvxor";
+ return "bvxor";
case kind::BITVECTOR_NAND :
- return "bvnand";
+ return "bvnand";
case kind::BITVECTOR_NOR :
- return "bvnor";
+ return "bvnor";
case kind::BITVECTOR_XNOR :
- return "bvxnor";
+ return "bvxnor";
case kind::BITVECTOR_COMP :
- return "bvcomp";
+ return "bvcomp";
case kind::BITVECTOR_MULT :
return "bvmul";
case kind::BITVECTOR_PLUS :
- return "bvadd";
+ return "bvadd";
case kind::BITVECTOR_SUB :
return "bvsub";
case kind::BITVECTOR_UDIV :
return "bvudiv";
case kind::BITVECTOR_UREM :
case kind::BITVECTOR_UREM_TOTAL :
- return "bvurem";
+ return "bvurem";
case kind::BITVECTOR_SDIV :
- return "bvsdiv";
+ return "bvsdiv";
case kind::BITVECTOR_SREM :
return "bvsrem";
case kind::BITVECTOR_SMOD :
- return "bvsmod";
+ return "bvsmod";
case kind::BITVECTOR_SHL :
- return "bvshl";
+ return "bvshl";
case kind::BITVECTOR_LSHR :
return "bvlshr";
case kind::BITVECTOR_ASHR :
return "bvashr";
case kind::BITVECTOR_CONCAT :
- return "concat";
+ return "concat";
case kind::BITVECTOR_NEG :
- return "bvneg";
+ return "bvneg";
case kind::BITVECTOR_NOT :
- return "bvnot";
+ return "bvnot";
case kind::BITVECTOR_ROTATE_LEFT :
- return "rotate_left";
+ return "rotate_left";
case kind::BITVECTOR_ROTATE_RIGHT :
return "rotate_right";
case kind::BITVECTOR_ULT :
- return "bvult";
+ return "bvult";
case kind::BITVECTOR_ULE :
- return "bvule";
+ return "bvule";
case kind::BITVECTOR_UGT :
return "bvugt";
case kind::BITVECTOR_UGE :
return "bvuge";
case kind::BITVECTOR_SLT :
- return "bvslt";
+ return "bvslt";
case kind::BITVECTOR_SLE :
- return "bvsle";
+ return "bvsle";
case kind::BITVECTOR_SGT :
- return "bvsgt";
+ return "bvsgt";
case kind::BITVECTOR_SGE :
- return "bvsge";
+ return "bvsge";
case kind::BITVECTOR_EXTRACT :
- return "extract";
+ return "extract";
case kind::BITVECTOR_REPEAT :
- return "repeat";
+ return "repeat";
case kind::BITVECTOR_ZERO_EXTEND :
return "zero_extend";
case kind::BITVECTOR_SIGN_EXTEND :
#include "cvc4_private.h"
-#pragma once
+#pragma once
#include <set>
#include <vector>
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::pair<Node, Node> NodePair;
+typedef std::set<NodePair> NodePairSet;
+
namespace utils {
std::string toLFSCKind(Kind kind);
}
inline unsigned getSize(Type type) {
- BitVectorType bv(type);
+ BitVectorType bv(type);
return bv.getSize();
}
return NodeManager::currentNM()->toExprManager()->mkConst<bool>(false);
}
inline BitVector mkBitVectorOnes(unsigned size) {
- Assert(size > 0);
- return BitVector(1, Integer(1)).signExtend(size - 1);
+ Assert(size > 0);
+ return BitVector(1, Integer(1)).signExtend(size - 1);
}
inline Expr mkExpr(Kind k , Expr expr) {
inline Expr mkExpr(Kind k , std::vector<Expr>& children) {
return NodeManager::currentNM()->toExprManager()->mkExpr(k, children);
}
-
-
+
+
inline Expr mkOnes(unsigned size) {
- BitVector val = mkBitVectorOnes(size);
- return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
+ BitVector val = mkBitVectorOnes(size);
+ return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
}
inline Expr mkConst(unsigned size, unsigned int value) {
BitVector val(size, value);
- return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
+ return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
}
inline Expr mkConst(const BitVector& value) {
inline Expr mkOr(const std::vector<Expr>& nodes) {
std::set<Expr> all;
all.insert(nodes.begin(), nodes.end());
- Assert(all.size() != 0 );
+ Assert(all.size() != 0 );
if (all.size() == 1) {
// All the same, or just one
return nodes[0];
}
-
-
+
+
NodeBuilder<> disjunction(kind::OR);
std::set<Expr>::const_iterator it = all.begin();
std::set<Expr>::const_iterator it_end = all.end();
}
Node res = disjunction;
- return res.toExpr();
+ return res.toExpr();
}/* mkOr() */
-
+
inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
std::set<Expr> all;
all.insert(conjunctions.begin(), conjunctions.end());
if (all.size() == 0) {
- return mkTrue();
+ return mkTrue();
}
-
+
if (all.size() == 1) {
// All the same, or just one
return conjunctions[0];
}
-
+
NodeBuilder<> conjunction(kind::AND);
std::set<Expr>::const_iterator it = all.begin();
++ it;
}
- Node res = conjunction;
+ Node res = conjunction;
return res.toExpr();
}/* mkAnd() */
all.insert(children.begin(), children.end());
if (all.size() == 0) {
- return mkTrue();
+ return mkTrue();
}
-
+
if (all.size() == 1) {
// All the same, or just one
return children[0];
}
-
+
NodeBuilder<> res(kind);
std::set<Expr>::const_iterator it = all.begin();
}/* mkSortedNode() */
inline const bool getBit(Expr expr, unsigned i) {
- Assert (i < utils::getSize(expr) &&
- expr.isConst());
+ Assert (i < utils::getSize(expr) &&
+ expr.isConst());
Integer bit = expr.getConst<BitVector>().extract(i, i).getValue();
- return (bit == 1u);
+ return (bit == 1u);
}
-void collectAtoms(TNode node, NodeSet& seen);
+void collectAtoms(TNode node, std::set<Node>& seen);
}
if (kind == THEORY_LEMMA) {
Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
d_lemmaClauses.insert(newId);
- Debug("pf::sat")
- << "TSatProof::registerClause registering a new lemma clause: "
- << newId << " = " << *buildClause(newId)
- << ". Explainer theory: " << d_cnfProof->getExplainerTheory()
- << std::endl;
- d_cnfProof->registerExplanationLemma(newId);
+ Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: "
+ << newId << " = " << *buildClause(newId)
+ << std::endl;
}
}
}
if (kind == THEORY_LEMMA) {
Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
- Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new "
- "lemma (UNIT CLAUSE): "
- << lit << ". Explainer theory: "
- << d_cnfProof->getExplainerTheory() << std::endl;
+ Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): "
+ << lit
+ << std::endl;
d_lemmaClauses.insert(newId);
- d_cnfProof->registerExplanationLemma(newId);
}
}
ClauseId id = d_unitId[toInt(lit)];
// clause allocator. So reload reason ptr each time.
const typename Solver::TClause& initial_reason = getClause(reason_ref);
size_t current_reason_size = initial_reason.size();
- for (int i = 0; i < current_reason_size; i++) {
+ for (size_t i = 0; i < current_reason_size; i++) {
const typename Solver::TClause& current_reason = getClause(reason_ref);
current_reason_size = current_reason.size();
typename Solver::TLit l = current_reason[i];
// Here, the call to resolveUnit() can reallocate memory in the
// clause allocator. So reload conflict ptr each time.
size_t conflict_size = getClause(conflict_ref).size();
- for (int i = 0; i < conflict_size; ++i) {
+ for (size_t i = 0; i < conflict_size; ++i) {
const typename Solver::TClause& conflict = getClause(conflict_ref);
typename Solver::TLit lit = conflict[i];
ClauseId res_id = resolveUnit(~lit);
}
if (id == this->d_emptyClauseId) {
- out << "(\\empty empty)";
+ out <<"(\\ empty empty)";
return;
}
- out << "(\\" << this->clauseName(id) << "\n"; // bind to lemma name
- paren << "))"; // closing parethesis for lemma binding and satlem
+ out << "(\\ " << this->clauseName(id) << "\n"; // bind to lemma name
+ paren << "))"; // closing parethesis for lemma binding and satlem
}
/// LFSCSatProof class
Node getSkolem(Node disequality);
Node getDisequality(Node skolem);
bool isSkolem(Node skolem);
-
void clear();
std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin();
#include "proof/clause_id.h"
#include "proof/cnf_proof.h"
#include "proof/proof_manager.h"
+#include "proof/proof_output_channel.h"
#include "proof/proof_utils.h"
#include "proof/sat_proof.h"
#include "proof/uf_proof.h"
unsigned CVC4::LetCount::counter = 0;
static unsigned LET_COUNT = 1;
-//for proof replay
-class ProofOutputChannel : public theory::OutputChannel {
-public:
- Node d_conflict;
- Proof* d_proof;
- Node d_lemma;
-
- ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
- virtual ~ProofOutputChannel() throw() {}
-
- void conflict(TNode n, Proof* pf) throw() {
- Trace("theory-proof-debug") << "; CONFLICT: " << n << std::endl;
- Assert(d_conflict.isNull());
- Assert(!n.isNull());
- d_conflict = n;
- Assert(pf != NULL);
- d_proof = pf;
- }
- bool propagate(TNode x) throw() {
- Trace("theory-proof-debug") << "got a propagation: " << x << std::endl;
- return true;
- }
- theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw() {
- Trace("theory-proof-debug") << "new lemma: " << n << std::endl;
- d_lemma = n;
- return theory::LemmaStatus(TNode::null(), 0);
- }
- theory::LemmaStatus splitLemma(TNode, bool) throw() {
- AlwaysAssert(false);
- return theory::LemmaStatus(TNode::null(), 0);
- }
- void requirePhase(TNode n, bool b) throw() {
- Debug("theory-proof-debug") << "ProofOutputChannel::requirePhase called" << std::endl;
- Trace("theory-proof-debug") << "requirePhase " << n << " " << b << std::endl;
- }
- bool flipDecision() throw() {
- Debug("theory-proof-debug") << "ProofOutputChannel::flipDecision called" << std::endl;
- AlwaysAssert(false);
- return false;
- }
- void setIncomplete() throw() {
- Debug("theory-proof-debug") << "ProofOutputChannel::setIncomplete called" << std::endl;
- AlwaysAssert(false);
- }
-};/* class ProofOutputChannel */
-
-//for proof replay
-class MyPreRegisterVisitor {
- theory::Theory* d_theory;
- __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
-public:
- typedef void return_type;
- MyPreRegisterVisitor(theory::Theory* theory)
- : d_theory(theory)
- , d_visited()
- {}
- bool alreadyVisited(TNode current, TNode parent) { return d_visited.find(current) != d_visited.end(); }
- void visit(TNode current, TNode parent) {
- if(theory::Theory::theoryOf(current) == d_theory->getId()) {
- //Trace("theory-proof-debug") << "preregister " << current << std::endl;
- d_theory->preRegisterTerm(current);
- d_visited.insert(current);
- }
- }
- void start(TNode node) { }
- void done(TNode node) { }
-}; /* class MyPreRegisterVisitor */
-
TheoryProofEngine::TheoryProofEngine()
: d_registrationCache()
, d_theoryProofTable()
}
}
-
void TheoryProofEngine::registerTheory(theory::Theory* th) {
- if( th ){
+ if (th) {
theory::TheoryId id = th->getId();
if(d_theoryProofTable.find(id) == d_theoryProofTable.end()) {
- Trace("theory-proof-debug") << "; register theory " << id << std::endl;
+ Trace("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl;
if (id == theory::THEORY_UF) {
d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this);
}
TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) {
+ // The UF theory handles queries for the Builtin theory.
+ if (id == theory::THEORY_BUILTIN) {
+ Debug("pf::tp") << "TheoryProofEngine::getTheoryProof: BUILTIN --> UF" << std::endl;
+ id = theory::THEORY_UF;
+ }
+
Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end());
return d_theoryProofTable[id];
}
+void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryId id) {
+ d_exprToTheoryIds[term].insert(id);
+}
+
+void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+ LetMap emptyMap;
+
+ os << "(trust_f (not (= _ ";
+ printBoundTerm(c1, os, emptyMap);
+ os << " ";
+ printBoundTerm(c2, os, emptyMap);
+ os << ")))";
+}
+
void TheoryProofEngine::registerTerm(Expr term) {
+ Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl;
+
if (d_registrationCache.count(term)) {
return;
}
- Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering new term: " << term << std::endl;
+
+ Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl;
theory::TheoryId theory_id = theory::Theory::theoryOf(term);
- Debug("pf::tp") << "Term's theory: " << theory_id << std::endl;
+ Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl;
// don't need to register boolean terms
if (theory_id == theory::THEORY_BUILTIN ||
if (!supportedTheory(theory_id)) return;
+ // Register the term with its owner theory
getTheoryProof(theory_id)->registerTerm(term);
+
+ // A special case: the array theory needs to know of every skolem, even if
+ // it belongs to another theory (e.g., a BV skolem)
+ if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) {
+ Debug("pf::tp") << "TheoryProofEngine::registerTerm: Special case: registering a non-array skolem: " << term << std::endl;
+ getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term);
+ }
+
d_registrationCache.insert(term);
}
-theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) {
+theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* clause) {
ProofManager* pm = ProofManager::currentPM();
- Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )"
- << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
+ std::set<Node> nodes;
+ for(unsigned i = 0; i < clause->size(); ++i) {
+ prop::SatLiteral lit = (*clause)[i];
+ Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+ Expr atom = node.toExpr();
+ if (atom.isConst()) {
+ Assert (atom == utils::mkTrue());
+ continue;
+ }
- if ((pm->getLogic() == "QF_UFLIA") || (pm->getLogic() == "QF_UFLRA")) {
- Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma: special hack for Arithmetic-with-holes support. "
- << "Returning THEORY_ARITH" << std::endl;
- return theory::THEORY_ARITH;
+ nodes.insert(lit.isNegated() ? node.notNode() : node);
}
- return pm->getCnfProof()->getOwnerTheory(id);
-
- // if (pm->getLogic() == "QF_UF") return theory::THEORY_UF;
- // if (pm->getLogic() == "QF_BV") return theory::THEORY_BV;
- // if (pm->getLogic() == "QF_AX") return theory::THEORY_ARRAY;
- // if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV;
-
- // Debug("pf::tp") << "Unsupported logic (" << pm->getLogic() << ")" << std::endl;
-
- // Unreachable();
+ // Ensure that the lemma is in the database.
+ Assert (pm->getCnfProof()->haveProofRecipe(nodes));
+ return pm->getCnfProof()->getProofRecipe(nodes).getTheory();
}
void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) {
void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) {
theory::TheoryId theory_id = theory::Theory::theoryOf(term);
- Debug("pf::tp") << std::endl << "LFSCTheoryProofEngine::printTheoryTerm: term = " << term
- << ", theory_id = " << theory_id << std::endl;
// boolean terms and ITEs are special because they
// are common to all theories
Unreachable();
}
+void LFSCTheoryProofEngine::performExtraRegistrations() {
+ ExprToTheoryIds::const_iterator it;
+ for (it = d_exprToTheoryIds.begin(); it != d_exprToTheoryIds.end(); ++it) {
+ if (d_registrationCache.count(it->first)) { // Only register if the term appeared
+ TheoryIdSet::const_iterator theoryIt;
+ for (theoryIt = it->second.begin(); theoryIt != it->second.end(); ++theoryIt) {
+ Debug("pf::tp") << "\tExtra registration of term " << it->first
+ << " with theory: " << *theoryIt << std::endl;
+ Assert(supportedTheory(*theoryIt));
+ getTheoryProof(*theoryIt)->registerTerm(it->first);
+ }
+ }
+ }
+}
+
+void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) {
+ TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
+ TheoryProofTable::const_iterator end = d_theoryProofTable.end();
+ for (; it != end; ++it) {
+ it->second->treatBoolsAsFormulas(value);
+ }
+}
+
void LFSCTheoryProofEngine::registerTermsFromAssertions() {
ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
for(; it != end; ++it) {
registerTerm(*it);
}
+
+ performExtraRegistrations();
}
void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) {
for (; it != end; ++it) {
Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl;
- // FIXME: merge this with counter
- os << "(% A" << counter++ << " (th_holds ";
+ std::ostringstream name;
+ name << "A" << counter++;
+ os << "(% " << name.str() << " (th_holds ";
printLetTerm(*it, os);
os << ")\n";
paren << ")";
}
- //store map between assertion and counter
- // ProofManager::currentPM()->setAssertion( *it );
+
Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl;
}
+void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren) {
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites called" << std::endl << std::endl;
+
+ NodePairSet::const_iterator it;
+
+ for (it = rewrites.begin(); it != rewrites.end(); ++it) {
+ Debug("pf::tp") << "printLemmaRewrites: " << it->first << " --> " << it->second << std::endl;
+
+ std::ostringstream rewriteRule;
+ rewriteRule << ".lrr" << d_assertionToRewrite.size();
+
+ LetMap emptyMap;
+ os << "(th_let_pf _ (trust_f (iff ";
+ printBoundTerm(it->second.toExpr(), os, emptyMap);
+ os << " ";
+ printBoundTerm(it->first.toExpr(), os, emptyMap);
+ os << ")) (\\ " << rewriteRule.str() << "\n";
+
+ d_assertionToRewrite[it->first] = rewriteRule.str();
+ Debug("pf::tp") << "d_assertionToRewrite[" << it->first << "] = " << rewriteRule.str() << std::endl;
+ paren << "))";
+ }
+
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites done" << std::endl << std::endl;
+}
+
void LFSCTheoryProofEngine::printSortDeclarations(std::ostream& os, std::ostream& paren) {
Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations called" << std::endl << std::endl;
}
}
-void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
- std::ostream& os,
- std::ostream& paren) {
- os << " ;; Theory Lemmas \n";
- ProofManager* pm = ProofManager::currentPM();
- IdToSatClause::const_iterator it = lemmas.begin();
- IdToSatClause::const_iterator end = lemmas.end();
-
- Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl;
+void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl;
+ TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
+ TheoryProofTable::const_iterator end = d_theoryProofTable.end();
for (; it != end; ++it) {
- Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl;
- ClauseId id = it->first;
- Debug("pf::tp") << "\tLemma = " << id
- << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
+ it->second->printAliasingDeclarations(os, paren);
}
- it = lemmas.begin();
+}
- // BitVector theory is special case: must know all
- // conflicts needed ahead of time for resolution
- // proof lemmas
- std::vector<Expr> bv_lemmas;
- for (; it != end; ++it) {
+void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) {
+ Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl;
+
+ ProofManager* pm = ProofManager::currentPM();
+ for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
ClauseId id = it->first;
+ Debug("pf::dumpLemmas") << "**** \tLemma ID = " << id << std::endl;
const prop::SatClause* clause = it->second;
+ std::set<Node> nodes;
+ for(unsigned i = 0; i < clause->size(); ++i) {
+ prop::SatLiteral lit = (*clause)[i];
+ Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+ if (node.isConst()) {
+ Assert (node.toExpr() == utils::mkTrue());
+ continue;
+ }
+ nodes.insert(lit.isNegated() ? node.notNode() : node);
+ }
+
+ LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes);
+ recipe.dump("pf::dumpLemmas");
+ }
- theory::TheoryId theory_id = getTheoryForLemma(id);
- if (theory_id != theory::THEORY_BV) continue;
+ Debug("pf::dumpLemmas") << "Theory lemma printing DONE" << std::endl << std::endl;
+}
+
+// TODO: this function should be moved into the BV prover.
+void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) {
+ // BitVector theory is special case: must know all conflicts needed
+ // ahead of time for resolution proof lemmas
+ std::vector<Expr> bv_lemmas;
+
+ for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
+ const prop::SatClause* clause = it->second;
std::vector<Expr> conflict;
+ std::set<Node> conflictNodes;
for(unsigned i = 0; i < clause->size(); ++i) {
prop::SatLiteral lit = (*clause)[i];
- Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
+ Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable());
+ Expr atom = node.toExpr();
+
+ // The literals (true) and (not false) are omitted from conflicts
if (atom.isConst()) {
Assert (atom == utils::mkTrue() ||
(atom == utils::mkFalse() && lit.isNegated()));
continue;
}
+
Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
conflict.push_back(expr_lit);
+ conflictNodes.insert(lit.isNegated() ? node.notNode() : node);
+ }
+
+ LemmaProofRecipe recipe = ProofManager::currentPM()->getCnfProof()->getProofRecipe(conflictNodes);
+
+ unsigned numberOfSteps = recipe.getNumSteps();
+
+ prop::SatClause currentClause = *clause;
+ std::vector<Expr> currentClauseExpr = conflict;
+
+ for (unsigned i = 0; i < numberOfSteps; ++i) {
+ const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i);
+
+ if (currentStep->getTheory() != theory::THEORY_BV) {
+ continue;
+ }
+
+ // If any rewrites took place, we need to update the conflict clause accordingly
+ std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i);
+ std::map<Node, Node> explanationToMissingAssertion;
+ std::set<Node>::iterator assertionIt;
+ for (assertionIt = missingAssertions.begin();
+ assertionIt != missingAssertions.end();
+ ++assertionIt) {
+ Node negated = (*assertionIt).negate();
+ explanationToMissingAssertion[recipe.getExplanation(negated)] = negated;
+ }
+
+ currentClause = *clause;
+ currentClauseExpr = conflict;
+
+ for (unsigned j = 0; j < i; ++j) {
+ // Literals already used in previous steps need to be negated
+ Node previousLiteralNode = recipe.getStep(j)->getLiteral();
+
+ // If this literal is the result of a rewrite, we need to translate it
+ if (explanationToMissingAssertion.find(previousLiteralNode) !=
+ explanationToMissingAssertion.end()) {
+ previousLiteralNode = explanationToMissingAssertion[previousLiteralNode];
+ }
+
+ Node previousLiteralNodeNegated = previousLiteralNode.negate();
+ prop::SatLiteral previousLiteralNegated =
+ ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated);
+
+ currentClause.push_back(previousLiteralNegated);
+ currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr());
+ }
+
+ // If we're in the final step, the last literal is Null and should not be added.
+ // Otherwise, the current literal does NOT need to be negated
+ Node currentLiteralNode = currentStep->getLiteral();
+
+ if (currentLiteralNode != Node()) {
+ prop::SatLiteral currentLiteral =
+ ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode);
+
+ currentClause.push_back(currentLiteral);
+ currentClauseExpr.push_back(currentLiteralNode.toExpr());
+ }
+
+ bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, currentClauseExpr));
}
- bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, conflict));
}
- // FIXME: ugly, move into bit-vector proof by adding lemma
- // queue inside each theory_proof
+
BitVectorProof* bv = ProofManager::getBitVectorProof();
bv->finalizeConflicts(bv_lemmas);
-
bv->printResolutionProof(os, paren);
+}
+
+void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
+ std::ostream& os,
+ std::ostream& paren) {
+ os << " ;; Theory Lemmas \n";
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl;
+
+ if (Debug.isOn("pf::dumpLemmas")) {
+ dumpTheoryLemmas(lemmas);
+ }
+
+ finalizeBvConflicts(lemmas, os, paren);
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
Assert (lemmas.size() == 1);
return;
}
- it = lemmas.begin();
-
+ ProofManager* pm = ProofManager::currentPM();
Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl;
- for (; it != end; ++it) {
- Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing a new lemma!" << std::endl;
-
- // Debug("pf::tp") << "\tLemma = " << it->first << ", " << *(it->second) << std::endl;
+ for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
ClauseId id = it->first;
- Debug("pf::tp") << "Owner theory:" << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
const prop::SatClause* clause = it->second;
- // printing clause as it appears in resolution proof
- os << "(satlem _ _ ";
- std::ostringstream clause_paren;
- Debug("pf::tp") << "CnfProof printing clause..." << std::endl;
- pm->getCnfProof()->printClause(*clause, os, clause_paren);
- Debug("pf::tp") << "CnfProof printing clause - Done!" << std::endl;
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = "
+ << id << std::endl;
std::vector<Expr> clause_expr;
+ std::set<Node> clause_expr_nodes;
for(unsigned i = 0; i < clause->size(); ++i) {
prop::SatLiteral lit = (*clause)[i];
- Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
+ Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+ Expr atom = node.toExpr();
if (atom.isConst()) {
Assert (atom == utils::mkTrue());
continue;
}
Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom;
clause_expr.push_back(expr_lit);
+ clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
}
- Debug("pf::tp") << "Expression printing done!" << std::endl;
-
- // query appropriate theory for proof of clause
- theory::TheoryId theory_id = getTheoryForLemma(id);
- Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
- Debug("theory-proof-debug") << ";; Get theory lemma from " << theory_id << "..." << std::endl;
- getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren);
- Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
- // os << " (clausify_false trust)";
- os << clause_paren.str();
- os << "( \\ " << pm->getLemmaClauseName(id) <<"\n";
- paren << "))";
+ LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(clause_expr_nodes);
+
+ if (recipe.simpleLemma()) {
+ // In a simple lemma, there will be no propositional resolution in the end
+
+ Debug("pf::tp") << "Simple lemma" << std::endl;
+ // Printing the clause as it appears in resolution proof
+ os << "(satlem _ _ ";
+ std::ostringstream clause_paren;
+ pm->getCnfProof()->printClause(*clause, os, clause_paren);
+
+ // Find and handle missing assertions, due to rewrites
+ std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(0);
+ if (!missingAssertions.empty()) {
+ Debug("pf::tp") << "Have missing assertions for this simple lemma!" << std::endl;
+ }
+
+ std::set<Node>::const_iterator missingAssertion;
+ for (missingAssertion = missingAssertions.begin();
+ missingAssertion != missingAssertions.end();
+ ++missingAssertion) {
+
+ Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl;
+ Assert(recipe.wasRewritten(missingAssertion->negate()));
+ Node explanation = recipe.getExplanation(missingAssertion->negate()).negate();
+ Debug("pf::tp") << "Found explanation: " << explanation << std::endl;
+
+ // We have a missing assertion.
+ // rewriteIt->first is the assertion after the rewrite (the explanation),
+ // rewriteIt->second is the original assertion that needs to be fed into the theory.
+
+ bool found = false;
+ unsigned k;
+ for (k = 0; k < clause_expr.size(); ++k) {
+ if (clause_expr[k] == explanation.toExpr()) {
+ found = true;
+ break;
+ }
+ }
+
+ Assert(found);
+ Debug("pf::tp") << "Replacing theory assertion "
+ << clause_expr[k]
+ << " with "
+ << *missingAssertion
+ << std::endl;
+
+ clause_expr[k] = missingAssertion->toExpr();
+
+ std::ostringstream rewritten;
+ rewritten << "(or_elim_1 _ _ ";
+ rewritten << "(not_not_intro _ ";
+ rewritten << pm->getLitName(explanation);
+ rewritten << ") (iff_elim_1 _ _ ";
+ rewritten << d_assertionToRewrite[missingAssertion->negate()];
+ rewritten << "))";
+
+ Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
+ << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+ << std::endl << std::endl;
+
+ pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
+ }
+
+ // Query the appropriate theory for a proof of this clause
+ theory::TheoryId theory_id = getTheoryForLemma(clause);
+ Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
+ getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren);
+
+ // Turn rewrite filter OFF
+ pm->clearRewriteFilters();
+
+ Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
+ os << clause_paren.str();
+ os << "( \\ " << pm->getLemmaClauseName(id) <<"\n";
+ paren << "))";
+ } else { // This is a composite lemma
+
+ unsigned numberOfSteps = recipe.getNumSteps();
+ prop::SatClause currentClause = *clause;
+ std::vector<Expr> currentClauseExpr = clause_expr;
+
+ for (unsigned i = 0; i < numberOfSteps; ++i) {
+ const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i);
+
+ currentClause = *clause;
+ currentClauseExpr = clause_expr;
+
+ for (unsigned j = 0; j < i; ++j) {
+ // Literals already used in previous steps need to be negated
+ Node previousLiteralNode = recipe.getStep(j)->getLiteral();
+ Node previousLiteralNodeNegated = previousLiteralNode.negate();
+ prop::SatLiteral previousLiteralNegated =
+ ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated);
+ currentClause.push_back(previousLiteralNegated);
+ currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr());
+ }
+
+ // If the current literal is NULL, can ignore (final step)
+ // Otherwise, the current literal does NOT need to be negated
+ Node currentLiteralNode = currentStep->getLiteral();
+ if (currentLiteralNode != Node()) {
+ prop::SatLiteral currentLiteral =
+ ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode);
+
+ currentClause.push_back(currentLiteral);
+ currentClauseExpr.push_back(currentLiteralNode.toExpr());
+ }
+
+ os << "(satlem _ _ ";
+ std::ostringstream clause_paren;
+
+ pm->getCnfProof()->printClause(currentClause, os, clause_paren);
+
+ // query appropriate theory for proof of clause
+ theory::TheoryId theory_id = currentStep->getTheory();
+ Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
+
+ std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i);
+ if (!missingAssertions.empty()) {
+ Debug("pf::tp") << "Have missing assertions for this step!" << std::endl;
+ }
+
+ // Turn rewrite filter ON
+ std::set<Node>::const_iterator missingAssertion;
+ for (missingAssertion = missingAssertions.begin();
+ missingAssertion != missingAssertions.end();
+ ++missingAssertion) {
+
+ Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl;
+
+ Assert(recipe.wasRewritten(missingAssertion->negate()));
+ Node explanation = recipe.getExplanation(missingAssertion->negate()).negate();
+
+ Debug("pf::tp") << "Found explanation: " << explanation << std::endl;
+
+ // We have a missing assertion.
+ // rewriteIt->first is the assertion after the rewrite (the explanation),
+ // rewriteIt->second is the original assertion that needs to be fed into the theory.
+
+ bool found = false;
+ unsigned k;
+ for (k = 0; k < currentClauseExpr.size(); ++k) {
+ if (currentClauseExpr[k] == explanation.toExpr()) {
+ found = true;
+ break;
+ }
+ }
+
+ Assert(found);
+
+ Debug("pf::tp") << "Replacing theory assertion "
+ << currentClauseExpr[k]
+ << " with "
+ << *missingAssertion
+ << std::endl;
+
+ currentClauseExpr[k] = missingAssertion->toExpr();
+
+ std::ostringstream rewritten;
+ rewritten << "(or_elim_1 _ _ ";
+ rewritten << "(not_not_intro _ ";
+ rewritten << pm->getLitName(explanation);
+ rewritten << ") (iff_elim_1 _ _ ";
+ rewritten << d_assertionToRewrite[missingAssertion->negate()];
+ rewritten << "))";
+
+ Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
+ << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+ << std::endl << std::endl;
+
+ pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
+ }
+
+ getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren);
+
+ // Turn rewrite filter OFF
+ pm->clearRewriteFilters();
+
+ Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
+ os << clause_paren.str();
+ os << "( \\ " << pm->getLemmaClauseName(id) << "s" << i <<"\n";
+ paren << "))";
+ }
+
+ Assert(numberOfSteps >= 2);
+
+ os << "(satlem_simplify _ _ _ ";
+ for (unsigned i = 0; i < numberOfSteps - 1; ++i) {
+ // Resolve step i with step i + 1
+ if (recipe.getStep(i)->getLiteral().getKind() == kind::NOT) {
+ os << "(Q _ _ ";
+ } else {
+ os << "(R _ _ ";
+ }
+
+ os << pm->getLemmaClauseName(id) << "s" << i;
+ os << " ";
+ }
+
+ os << pm->getLemmaClauseName(id) << "s" << numberOfSteps - 1 << " ";
+
+ prop::SatLiteral v;
+ for (int i = numberOfSteps - 2; i >= 0; --i) {
+ v = ProofManager::currentPM()->getCnfProof()->getLiteral(recipe.getStep(i)->getLiteral());
+ os << ProofManager::getVarName(v.getSatVariable(), "") << ") ";
+ }
+
+ os << "( \\ " << pm->getLemmaClauseName(id) << "\n";
+ paren << "))";
+ }
}
}
void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) {
- // Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
+ Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
LetMap::const_iterator it = map.find(term);
if (it != map.end()) {
}
void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
- //default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
- Assert( d_theory!=NULL );
+ // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
+ Assert(d_theory!=NULL);
+
context::UserContext fakeContext;
ProofOutputChannel oc;
theory::Valuation v(NULL);
//make new copy of theory
theory::Theory* th;
- Trace("theory-proof-debug") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
- if(d_theory->getId()==theory::THEORY_UF) {
+ Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
+
+ if (d_theory->getId()==theory::THEORY_UF) {
th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v,
ProofManager::currentPM()->getLogicInfo(),
"replay::");
- } else if(d_theory->getId()==theory::THEORY_ARRAY) {
+ } else if (d_theory->getId()==theory::THEORY_ARRAY) {
th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v,
ProofManager::currentPM()->getLogicInfo(),
"replay::");
void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
Assert (term.getType().isBoolean());
if (term.isVariable()) {
- os << "(p_app " << ProofManager::sanitize(term) <<")";
+ if (d_treatBoolsAsFormulas)
+ os << "(p_app " << ProofManager::sanitize(term) <<")";
+ else
+ os << ProofManager::sanitize(term);
return;
}
return;
case kind::CONST_BOOLEAN:
- os << (term.getConst<bool>() ? "true" : "false");
+ if (d_treatBoolsAsFormulas)
+ os << (term.getConst<bool>() ? "true" : "false");
+ else
+ os << (term.getConst<bool>() ? "t_true" : "t_false");
return;
default:
// Nothing to do here at this point.
}
+void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ // Nothing to do here at this point.
+}
+
void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
std::ostream& os,
std::ostream& paren) {
#include "proof/clause_id.h"
#include "prop/sat_solver_types.h"
#include "util/proof.h"
+#include "proof/proof_utils.h"
namespace CVC4 {
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;
+typedef std::set<theory::TheoryId> TheoryIdSet;
+typedef std::map<Expr, TheoryIdSet> ExprToTheoryIds;
+
class TheoryProofEngine {
protected:
ExprSet d_registrationCache;
TheoryProofTable d_theoryProofTable;
+ ExprToTheoryIds d_exprToTheoryIds;
/**
* Returns whether the theory is currently supported in proof
*/
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
+ /**
+ * Print aliasing declarations.
+ *
+ * @param os
+ * @param paren closing parenthesis
+ */
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
+
/**
* Print proofs of all the theory lemmas (must prove
* actual clause used in resolution proof).
*/
void registerTheory(theory::Theory* theory);
- theory::TheoryId getTheoryForLemma(ClauseId id);
+ theory::TheoryId getTheoryForLemma(const prop::SatClause* clause);
TheoryProof* getTheoryProof(theory::TheoryId id);
+
+ void markTermForFutureRegistration(Expr term, theory::TheoryId id);
+
+ void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+
+ virtual void treatBoolsAsFormulas(bool value) {};
};
class LFSCTheoryProofEngine : public TheoryProofEngine {
virtual void printLetTerm(Expr term, std::ostream& os);
virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map);
virtual void printAssertions(std::ostream& os, std::ostream& paren);
+ virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTheoryLemmas(const IdToSatClause& lemmas,
std::ostream& os,
std::ostream& paren);
virtual void printSort(Type type, std::ostream& os);
+
+ void performExtraRegistrations();
+
+ void treatBoolsAsFormulas(bool value);
+
+private:
+ static void dumpTheoryLemmas(const IdToSatClause& lemmas);
+
+ // TODO: this function should be moved into the BV prover.
+ void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren);
+
+ std::map<Node, std::string> d_assertionToRewrite;
};
class TheoryProof {
* @param paren
*/
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
+ /**
+ * Print any aliasing declarations.
+ *
+ * @param os
+ * @param paren
+ */
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
/**
* Register a term of this theory that appears in the proof.
*
* @param term
*/
virtual void registerTerm(Expr term) = 0;
+
+ virtual void treatBoolsAsFormulas(bool value) {}
};
class BooleanProof : public TheoryProof {
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
};
class LFSCBooleanProof : public BooleanProof {
public:
LFSCBooleanProof(TheoryProofEngine* proofEngine)
- : BooleanProof(proofEngine)
+ : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
{}
virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
+
+ void treatBoolsAsFormulas(bool value) {
+ d_treatBoolsAsFormulas = value;
+ }
+
+private:
+ bool d_treatBoolsAsFormulas;
};
} /* CVC4 namespace */
pf->debug_print("pf::uf");
Debug("pf::uf") << std::endl;
- if(tb == 0) {
+ if (tb == 0) {
+ // Special case: false was an input, so the proof is just "false".
+ if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY &&
+ pf->d_node == NodeManager::currentNM()->mkConst(false)) {
+ out << "(clausify_false ";
+ out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode());
+ out << ")" << std::endl;
+ return Node();
+ }
+
Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS);
Assert(!pf->d_node.isNull());
Assert(pf->d_children.size() >= 2);
++i;
}
}
- Assert(neg >= 0);
+
+ bool disequalityFound = (neg >= 0);
+ if (!disequalityFound) {
+ Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
+ Debug("pf::uf") << "Proof for: " << pf->d_node << std::endl;
+ Assert(pf->d_node.getKind() == kind::EQUAL);
+ Assert(pf->d_node.getNumChildren() == 2);
+ Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst());
+ }
Node n1;
std::stringstream ss;
- //Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
- if(pf->d_children.size() > 2) {
+
+ if(!disequalityFound || subTrans.d_children.size() >= 2) {
n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
} else {
n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
Debug("pf::uf") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
}
- Node n2 = pf->d_children[neg]->d_node;
- Assert(n2.getKind() == kind::NOT);
- out << "(clausify_false (contra _ ";
Debug("pf::uf") << "\nhave proven: " << n1 << std::endl;
- Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
- if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; }
- if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; }
+ out << "(clausify_false (contra _ ";
+
+ if (disequalityFound) {
+ Node n2 = pf->d_children[neg]->d_node;
+ Assert(n2.getKind() == kind::NOT);
+ Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
- if(n2[0].getKind() == kind::APPLY_UF) {
- out << "(trans _ _ _ _ ";
- out << "(symm _ _ _ ";
- out << ss.str();
- out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
- } else {
- Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
- if(n1[1] == n2[0][0]) {
- out << "(symm _ _ _ " << ss.str() << ")";
+ if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; }
+ if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; }
+
+ if(n2[0].getKind() == kind::APPLY_UF) {
+ out << "(trans _ _ _ _ ";
+
+ if (n1[0] == n2[0]) {
+ out << "(symm _ _ _ ";
+ out << ss.str();
+ out << ") ";
+ } else {
+ Assert(n1[1] == n2[0]);
+ out << ss.str();
+ }
+ out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
} else {
- out << ss.str();
+ Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
+ if(n1[1] == n2[0][0]) {
+ out << "(symm _ _ _ " << ss.str() << ")";
+ } else {
+ out << ss.str();
+ }
+ out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
}
- out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
+ } else {
+ Node n2 = pf->d_node;
+ Assert(n2.getKind() == kind::EQUAL);
+ Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
+
+ out << ss.str();
+ out << " ";
+ ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr());
+ out << "))" << std::endl;
}
+
return Node();
}
} else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) {
// n1 is an equality/iff, but n2 is a predicate
if(n1[0] == n2) {
- n1 = n1[1];
+ n1 = n1[1].iffNode(NodeManager::currentNM()->mkConst(true));
ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")";
} else if(n1[1] == n2) {
- n1 = n1[0];
+ n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true));
ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")";
} else {
Unreachable();
} else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
// n2 is an equality/iff, but n1 is a predicate
if(n2[0] == n1) {
- n1 = n2[1];
+ n1 = n2[1].iffNode(NodeManager::currentNM()->mkConst(true));
ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")";
} else if(n2[1] == n1) {
- n1 = n2[0];
+ n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true));
ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")";
} else {
Unreachable();
}
} else {
- // Both n1 and n2 are prediacates. Don't know what to do...
+ // Both n1 and n2 are predicates. Don't know what to do...
Unreachable();
}
}
Assert (term.getKind() == kind::APPLY_UF);
+ d_proofEngine->treatBoolsAsFormulas(false);
if(term.getType().isBoolean()) {
os << "(p_app ";
if(term.getType().isBoolean()) {
os << ")";
}
+ d_proofEngine->treatBoolsAsFormulas(true);
}
void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
// declaring the terms
+ Debug("pf::uf") << "LFSCUFProof::printTermDeclarations called" << std::endl;
+
for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
Expr term = *it;
os << "(arrow";
for (unsigned i = 0; i < args.size(); i++) {
Type arg_type = args[i];
- os << " " << arg_type;
+ os << " ";
+ d_proofEngine->printSort(arg_type, os);
if (i < args.size() - 2) {
os << " (arrow";
fparen << ")";
}
paren << ")";
}
+
+ Debug("pf::uf") << "LFSCUFProof::printTermDeclarations done" << std::endl;
}
void LFSCUFProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
// Nothing to do here at this point.
}
+void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+ // Nothing to do here at this point.
+}
+
} /* namespace CVC4 */
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+ virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
};
return find != d_nodeToLiteralMap.end();
}
-void TseitinCnfStream::ensureLiteral(TNode n) {
+void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
// These are not removable and have no proof ID
d_removable = false;
d_literalToNodeMap.insert_safe(~lit, n.notNode());
} else {
// We have a theory atom or variable.
- lit = convertAtom(n);
+ lit = convertAtom(n, noPreregistration);
}
Assert(hasLiteral(n) && getNode(lit) == n);
d_cnfProof = proof;
}
-SatLiteral CnfStream::convertAtom(TNode node) {
+SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
Debug("cnf") << "convertAtom(" << node << ")" << endl;
Assert(!hasLiteral(node), "atom already mapped!");
} else {
theoryLiteral = true;
canEliminate = false;
- preRegister = true;
+ preRegister = !noPreregistration;
}
// Make a new literal (variables are not considered theory literals)
SatLiteral CnfStream::getLiteral(TNode node) {
Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node");
- Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str());
+
+ Assert(d_nodeToLiteralMap.contains(node),
+ "Literal not in the CNF Cache: %s\n",
+ node.toString().c_str());
+
SatLiteral literal = d_nodeToLiteralMap[node];
Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
return literal;
bool negated,
ProofRule proof_id,
TNode from,
- theory::TheoryId ownerTheory) {
+ LemmaProofRecipe* proofRecipe) {
Debug("cnf") << "convertAndAssert(" << node
<< ", removable = " << (removable ? "true" : "false")
<< ", negated = " << (negated ? "true" : "false") << ")" << endl;
Node assertion = negated ? node.notNode() : (Node)node;
Node from_assertion = negated? from.notNode() : (Node) from;
- d_cnfProof->setExplainerTheory(ownerTheory);
+ if (proofRecipe) {
+ Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl;
+ proofRecipe->dump("pf::sat");
+ d_cnfProof->setProofRecipe(proofRecipe);
+ }
+
if (proof_id != RULE_INVALID) {
d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
#include "smt_util/lemma_channels.h"
namespace CVC4 {
+
+class LemmaProofRecipe;
+
namespace prop {
class PropEngine;
* structure in this expression. Assumed to not be in the
* translation cache.
*/
- SatLiteral convertAtom(TNode node);
+ SatLiteral convertAtom(TNode node, bool noPreprocessing = false);
public:
* @param node node to convert and assert
* @param removable whether the sat solver can choose to remove the clauses
* @param negated whether we are asserting the node negated
- * @param ownerTheory indicates the theory that should invoked to prove the formula.
+ * @param proofRecipe contains the proof recipe for proving this node
*/
- virtual void convertAndAssert(TNode node,
- bool removable,
- bool negated,
- ProofRule proof_id,
- TNode from = TNode::null(),
- theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0;
+ virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0;
+
/**
* Get the node that is represented by the given SatLiteral.
* @param literal the literal from the sat solver
* this is like a "convert-but-don't-assert" version of
* convertAndAssert().
*/
- virtual void ensureLiteral(TNode n) = 0;
+ virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0;
/**
* Returns the literal that represents the given node in the SAT CNF
*/
void convertAndAssert(TNode node, bool removable,
bool negated, ProofRule rule, TNode from = TNode::null(),
- theory::TheoryId ownerTheory = theory::THEORY_LAST);
+ LemmaProofRecipe* proofRecipe = NULL);
/**
* Constructs the stream to use the given sat solver.
*/
SatLiteral toCNF(TNode node, bool negated = false);
- void ensureLiteral(TNode n);
+ void ensureLiteral(TNode n, bool noPreregistration = false);
};/* class TseitinCnfStream */
vec<Lit> explanation;
MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
+ Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl;
+
// Sort the literals by trail index level
lemma_lt lt(*this);
sort(explanation, lt);
}
explanation.shrink(i - j);
+ Debug("pf::sat") << "Solver::reason: explanation = " ;
+ for (int i = 0; i < explanation.size(); ++i) {
+ Debug("pf::sat") << explanation[i] << " ";
+ }
+ Debug("pf::sat") << std::endl;
+
// We need an explanation clause so we add a fake literal
if (j == 1) {
// Add not TRUE to the clause
CRef real_reason = ca.alloc(explLevel, explanation, true);
// FIXME: at some point will need more information about where this explanation
// came from (ie. the theory/sharing)
+ Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA);
ProofManager::getCnfProof()->registerConvertedClause(id, true);
// no need to pop current assertion as this is not converted to cnf
// If we are in solve or decision level > 0
if (minisat_busy || decisionLevel() > 0) {
+ Debug("pf::sat") << "Add clause adding a new lemma: ";
+ for (int k = 0; k < ps.size(); ++k) {
+ Debug("pf::sat") << ps[k] << " ";
+ }
+ Debug("pf::sat") << std::endl;
+
lemmas.push();
ps.copyTo(lemmas.last());
lemmas_removable.push(removable);
{
// The current lemma
vec<Lit>& lemma = lemmas[i];
+
+ Debug("pf::sat") << "Solver::updateLemmas: working on lemma: ";
+ for (int k = 0; k < lemma.size(); ++k) {
+ Debug("pf::sat") << lemma[k] << " ";
+ }
+ Debug("pf::sat") << std::endl;
+
// If it's an empty lemma, we have a conflict at zero level
if (lemma.size() == 0) {
Assert (! PROOF_ON());
TNode cnf_assertion = lemmas_cnf_assertion[i].first;
TNode cnf_def = lemmas_cnf_assertion[i].second;
+ Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA);
ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
Node cnf_assertion = lemmas_cnf_assertion[i].first;
Node cnf_def = lemmas_cnf_assertion[i].second;
+ Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl;
ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
// FIXME: This relies on the invariant that when ok() is false
// the SAT solver does not add the clause (which is what Minisat currently does)
if (!ok()) {
- return ClauseIdUndef;
+ return ClauseIdUndef;
}
d_minisat->addClause(minisat_clause, removable, clause_id);
PROOF( Assert (clause_id != ClauseIdError););
}
bool MinisatSatSolver::ok() const {
- return d_minisat->okay();
+ return d_minisat->okay();
}
void MinisatSatSolver::interrupt() {
return true;
}
-void MinisatSatSolver::requirePhase(SatLiteral lit) {
+void MinisatSatSolver::requirePhase(SatLiteral lit) {
Assert(!d_minisat->rnd_pol);
Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl;
SatVariable v = lit.getSatVariable();
d_minisat->freezePolarity(v, lit.isNegated());
}
-bool MinisatSatSolver::flipDecision() {
+bool MinisatSatSolver::flipDecision() {
Debug("minisat") << "flipDecision()" << std::endl;
return d_minisat->flipDecision();
}
-bool MinisatSatSolver::isDecision(SatVariable decn) const {
- return d_minisat->isDecision( decn );
+bool MinisatSatSolver::isDecision(SatVariable decn) const {
+ return d_minisat->isDecision( decn );
}
/** Incremental interface */
template<>
prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
return prop::MinisatSatSolver::toSatLiteral(lit);
-}
+}
template<>
void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
}
} /* namespace CVC4 */
-
-
void PropEngine::assertLemma(TNode node, bool negated,
bool removable,
ProofRule rule,
- theory::TheoryId ownerTheory,
+ LemmaProofRecipe* proofRecipe,
TNode from) {
//Assert(d_inCheckSat, "Sat solver should be in solve()!");
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
// Assert as (possibly) removable
- d_cnfStream->convertAndAssert(node, removable, negated, rule, from, ownerTheory);
+ d_cnfStream->convertAndAssert(node, removable, negated, rule, from, proofRecipe);
}
void PropEngine::requirePhase(TNode n, bool phase) {
class ResourceManager;
class DecisionEngine;
class TheoryEngine;
+class LemmaProofRecipe;
namespace theory {
class TheoryRegistrar;
* @param removable whether this lemma can be quietly removed based
* on an activity heuristic (or not)
*/
- void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, theory::TheoryId ownerTheory, TNode from = TNode::null());
+ void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, LemmaProofRecipe* proofRecipe, TNode from = TNode::null());
/**
* If ever n is decided upon, it must be in the given phase. This
TNode lNode = d_cnfStream->getNode(l);
Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
- NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode);
- Node explanationNode = theoryExplanation.node;
- theory::TheoryId explainerTheory = theoryExplanation.theory;
+ LemmaProofRecipe* proofRecipe = NULL;
+ PROOF(proofRecipe = new LemmaProofRecipe;);
+
+ Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
PROOF({
- ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode);
- ProofManager::getCnfProof()->setExplainerTheory(explainerTheory);
+ ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
+ ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
+
+ Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: "
+ << std::endl;
+ proofRecipe->dump("pf::sat");
- Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: "
- << explainerTheory << std::endl;
+ delete proofRecipe;
+ proofRecipe = NULL;
});
- Debug("prop-explain") << "explainPropagation() => " << explanationNode << std::endl;
- if (explanationNode.getKind() == kind::AND) {
- Node::const_iterator it = explanationNode.begin();
- Node::const_iterator it_end = explanationNode.end();
+ Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
+ if (theoryExplanation.getKind() == kind::AND) {
+ Node::const_iterator it = theoryExplanation.begin();
+ Node::const_iterator it_end = theoryExplanation.end();
explanation.push_back(l);
for (; it != it_end; ++ it) {
explanation.push_back(~d_cnfStream->getLiteral(*it));
}
} else {
explanation.push_back(l);
- explanation.push_back(~d_cnfStream->getLiteral(explanationNode));
+ explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
}
}
if(lemmaCount % 1 == 0) {
Debug("shared") << "=) " << asNode << std::endl;
}
- d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST);
+
+ LemmaProofRecipe* noProofRecipe = NULL;
+ d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe);
} else {
Debug("shared") << "=(" << asNode << std::endl;
}
Trace("smt-qe-debug") << " return : " << ret << std::endl;
//recursive (for nested quantification)
ret = replaceQuantifiersWithInstantiations( reti, insts, visited );
- }
+ }
}else if( n.getNumChildren()>0 ){
bool childChanged = false;
std::vector< Node > children;
//must have finite model finding on
options::finiteModelFind.set( true );
}
-
+
//if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){
if( !options::instWhenStrictInterleave.wasSetByUser() ){
options::instWhenStrictInterleave.set( false );
}
}
-
+
//local theory extensions
if( options::localTheoryExt() ){
if( !options::instMaxLevel.wasSetByUser() ){
//apply counterexample guided instantiation options
if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){
if( !options::ceGuidedInst.wasSetByUser() ){
- options::ceGuidedInst.set( true );
- }
+ options::ceGuidedInst.set( true );
+ }
}
if( options::ceGuidedInst() ){
//counterexample-guided instantiation for sygus
}
//counterexample-guided instantiation for non-sygus
// enable if any quantifiers with arithmetic or datatypes
- if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) ||
+ if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) ||
options::cbqiAll() ){
if( !options::cbqi.wasSetByUser() ){
options::cbqi.set( true );
ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr());
}
);
-
+
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
if( options::ceGuidedInst() ){
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
dumpAssertions("post-everything", d_assertions);
-
+
//set instantiation level of everything to zero
if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
//possibly run quantifier elimination to make formula into single invocation
if( conj[1].getKind()==kind::EXISTS ){
Node conj_se = conj[1][1];
-
+
Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
quantifiers::SingleInvocationPartition sip( kind::APPLY );
sip.init( conj_se );
Trace("smt-synth") << "...finished, got:" << std::endl;
sip.debugPrint("smt-synth");
-
+
if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){
//We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f.
- //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ),
+ //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ),
// and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f. We invoke synthesis solver on this result.
-
+
//create new smt engine to do quantifier elimination
SmtEngine smt_qe( d_exprManager );
smt_qe.setLogic(getLogicInfo());
Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() );
Assert( !qe_vars.empty() );
conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs );
-
+
Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl;
Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false );
Trace("smt-synth") << "Result : " << qe_res << std::endl;
-
+
//create single invocation conjecture
Node qe_res_n = Node::fromExpr( qe_res );
qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() );
}
}
}
-
+
return checkSatisfiability( e_check, true, false );
}
Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
}
Trace("smt-qe") << "Do quantifier elimination " << e << std::endl;
- Node n_e = Node::fromExpr( e );
+ Node n_e = Node::fromExpr( e );
if( n_e.getKind()!=kind::EXISTS ){
throw ModalException("Expecting an existentially quantified formula as argument to get-qe.");
}
InternalError(ss.str().c_str());
}
//get the instantiations for all quantified formulas
- std::map< Node, std::vector< Node > > insts;
+ std::map< Node, std::vector< Node > > insts;
d_theoryEngine->getInstantiations( insts );
//find the quantified formula that corresponds to the input
Node top_q;
Chat() << "checking proof..." << endl;
- if ( !(d_logic.isPure(theory::THEORY_BOOL) ||
- d_logic.isPure(theory::THEORY_BV) ||
- d_logic.isPure(theory::THEORY_ARRAY) ||
- (d_logic.isPure(theory::THEORY_UF) &&
- ! d_logic.hasCardinalityConstraints())) ||
- d_logic.isQuantified()) {
- // no checking for these yet
- Notice() << "Notice: no proof-checking for non-UF/Bool/BV proofs yet" << endl;
+ std::string logicString = d_logic.getLogicString();
+
+ if (!(
+ // Pure logics
+ logicString == "QF_UF" ||
+ logicString == "QF_AX" ||
+ logicString == "QF_BV" ||
+ // Non-pure logics
+ logicString == "QF_AUF" ||
+ logicString == "QF_UFBV" ||
+ logicString == "QF_ABV" ||
+ logicString == "QF_AUFBV"
+ )) {
+ // This logic is not yet supported
+ Notice() << "Notice: no proof-checking for " << logicString << " proofs yet" << endl;
return;
}
Debug("pf::ee") << "Getting explanation for ROW guard: "
<< indexOne << " != " << indexTwo << std::endl;
+
eq::EqProof* childProof = new eq::EqProof;
d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof);
+
+ // It could be that the guard condition is a constant disequality. In this case,
+ // we need to change it to a different format.
+ if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
+ // The proof has two children, explaining why each index is a (different) constant.
+ Assert(childProof->d_children.size() == 2);
+
+ Node constantOne, constantTwo;
+ // Each subproof explains why one of the indices is constant.
+
+ if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
+ constantOne = childProof->d_children[0]->d_node;
+ } else {
+ Assert(childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
+ if ((childProof->d_children[0]->d_node[0] == indexOne) ||
+ (childProof->d_children[0]->d_node[0] == indexTwo)) {
+ constantOne = childProof->d_children[0]->d_node[1];
+ } else {
+ constantOne = childProof->d_children[0]->d_node[0];
+ }
+ }
+
+ if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
+ constantTwo = childProof->d_children[1]->d_node;
+ } else {
+ Assert(childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
+ if ((childProof->d_children[1]->d_node[0] == indexOne) ||
+ (childProof->d_children[1]->d_node[0] == indexTwo)) {
+ constantTwo = childProof->d_children[1]->d_node[1];
+ } else {
+ constantTwo = childProof->d_children[1]->d_node[0];
+ }
+ }
+
+ eq::EqProof* constantDisequalityProof = new eq::EqProof;
+ constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS;
+ constantDisequalityProof->d_node =
+ NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate();
+
+ // Middle is where we need to insert the new disequality
+ std::vector<eq::EqProof *>::iterator middle = childProof->d_children.begin();
+ ++middle;
+
+ childProof->d_children.insert(middle, constantDisequalityProof);
+
+ childProof->d_id = theory::eq::MERGED_THROUGH_TRANS;
+ childProof->d_node =
+ NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate();
+ }
+
proof->d_children.push_back(childProof);
} else {
// This is the case of (i == k) because ((a[i]:=t)[k] != a[k]),
Node TheoryArrays::explain(TNode literal) {
- return explain(literal, NULL);
+ Node explanation = explain(literal, NULL);
+ return explanation;
}
Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
break;
default:
Unreachable();
+ break;
}
}
void TheoryArrays::conflict(TNode a, TNode b) {
Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
+
if (a.getKind() == kind::CONST_BOOLEAN) {
d_conflictNode = explain(a.iffNode(b), proof);
} else {
continue;
}
Node signature = computeSignature(assertions[i][j]);
- storeSignature(signature, assertions[i][j]);
+ storeSignature(signature, assertions[i][j]);
Debug("bv-abstraction") << " assertion: " << assertions[i][j] <<"\n";
Debug("bv-abstraction") << " signature: " << signature <<"\n";
}
for (unsigned i = 0; i < assertions.size(); ++i) {
if (assertions[i].getKind() == kind::OR &&
assertions[i][0].getKind() == kind::AND) {
- std::vector<Node> new_children;
+ std::vector<Node> new_children;
for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) {
if (hasSignature(assertions[i][j])) {
new_children.push_back(abstractSignatures(assertions[i][j]));
new_children.push_back(assertions[i][j]);
}
}
- new_assertions.push_back(utils::mkNode(kind::OR, new_children));
+ new_assertions.push_back(utils::mkNode(kind::OR, new_children));
} else {
// assertions that are not changed
- new_assertions.push_back(assertions[i]);
+ new_assertions.push_back(assertions[i]);
}
}
skolemizeArguments(new_assertions);
}
-
+
// if we are using the eager solver reverse the abstraction
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
if (d_funcToSignature.size() == 0) {
// we did not change anything
return false;
}
- NodeNodeMap seen;
+ NodeNodeMap seen;
for (unsigned i = 0; i < new_assertions.size(); ++i) {
- new_assertions[i] = reverseAbstraction(new_assertions[i], seen);
+ new_assertions[i] = reverseAbstraction(new_assertions[i], seen);
}
// we undo the abstraction functions so the logic is QF_BV still
- return true;
+ return true;
}
-
+
// return true if we have created new function symbols for the problem
return d_funcToSignature.size() != 0;
}
bool AbstractionModule::isConjunctionOfAtomsRec(TNode node, TNodeSet& seen) {
if (seen.find(node)!= seen.end())
return true;
-
+
if (!node.getType().isBitVector()) {
return (node.getKind() == kind::AND || utils::isBVPredicate(node));
}
if (seen.find(assertion) != seen.end())
return seen[assertion];
-
+
if (isAbstraction(assertion)) {
Node interp = getInterpretation(assertion);
seen[assertion] = interp;
- Assert (interp.getType() == assertion.getType());
+ Assert (interp.getType() == assertion.getType());
return interp;
}
if (assertion.getNumChildren() == 0) {
seen[assertion] = assertion;
- return assertion;
+ return assertion;
}
-
+
NodeBuilder<> result(assertion.getKind());
if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) {
- result << assertion.getOperator();
+ result << assertion.getOperator();
}
for (unsigned i = 0; i < assertion.getNumChildren(); ++i) {
- result << reverseAbstraction(assertion[i], seen);
+ result << reverseAbstraction(assertion[i], seen);
}
Node res = result;
seen[assertion] = res;
- return res;
+ return res;
}
void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
TNode assertion = assertions[i];
if (assertion.getKind() != kind::OR)
continue;
-
+
bool is_skolemizable = true;
for (unsigned k = 0; k < assertion.getNumChildren(); ++k) {
if (assertion[k].getKind() != kind::EQUAL ||
NodeBuilder<> skolem_func (kind::APPLY_UF);
skolem_func << func;
std::vector<Node> skolem_args;
-
+
for (unsigned j = 0; j < args.getArity(); ++j) {
bool all_same = true;
for (unsigned k = 1; k < args.getNumEntries(); ++k) {
if ( args.getEntry(k)[j] != args.getEntry(0)[j])
- all_same = false;
+ all_same = false;
}
- Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j]));
+ Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j]));
skolem_args.push_back(new_arg);
- skolem_func << new_arg;
+ skolem_func << new_arg;
}
-
- Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u));
-
+
+ Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u));
+
// enumerate arguments assignments
- std::vector<Node> or_assignments;
+ std::vector<Node> or_assignments;
for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) {
NodeBuilder<> arg_assignment(kind::AND);
ArgsVec& args = *it;
for (unsigned k = 0; k < args.size(); ++k) {
Node eq = utils::mkNode(kind::EQUAL, args[k], skolem_args[k]);
- arg_assignment << eq;
+ arg_assignment << eq;
}
or_assignments.push_back(arg_assignment);
}
-
+
Node new_func_def = utils::mkNode(kind::AND, skolem_func_eq1, utils::mkNode(kind::OR, or_assignments));
- assertion_builder << new_func_def;
+ assertion_builder << new_func_def;
}
Node new_assertion = assertion_builder;
Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " << assertions[i] << " => \n";
- Debug("bv-abstraction-dbg") << " " << new_assertion;
+ Debug("bv-abstraction-dbg") << " " << new_assertion;
assertions[i] = new_assertion;
}
}
void AbstractionModule::storeSignature(Node signature, TNode assertion) {
if(d_signatures.find(signature) == d_signatures.end()) {
- d_signatures[signature] = 0;
+ d_signatures[signature] = 0;
}
- d_signatures[signature] = d_signatures[signature] + 1;
- d_assertionToSignature[assertion] = signature;
+ d_signatures[signature] = d_signatures[signature] + 1;
+ d_assertionToSignature[assertion] = signature;
}
Node AbstractionModule::computeSignature(TNode node) {
- resetSignatureIndex();
- NodeNodeMap cache;
+ resetSignatureIndex();
+ NodeNodeMap cache;
Node sig = computeSignatureRec(node, cache);
return sig;
}
Assert (node.getKind() == kind::VARIABLE);
unsigned bitwidth = utils::getSize(node);
if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) {
- d_signatureSkolems[bitwidth] = vector<Node>();
+ d_signatureSkolems[bitwidth] = vector<Node>();
}
-
+
vector<Node>& skolems = d_signatureSkolems[bitwidth];
// get the index of bv variables of this size
- unsigned index = getBitwidthIndex(bitwidth);
+ unsigned index = getBitwidthIndex(bitwidth);
Assert (skolems.size() + 1 >= index );
if (skolems.size() == index) {
ostringstream os;
os << "sig_" <<bitwidth <<"_" << index;
- NodeManager* nm = NodeManager::currentNM();
+ NodeManager* nm = NodeManager::currentNM();
skolems.push_back(nm->mkSkolem(os.str(), nm->mkBitVectorType(bitwidth), "skolem for computing signatures"));
}
++(d_signatureIndices[bitwidth]);
if (d_signatureIndices.find(bitwidth) == d_signatureIndices.end()) {
d_signatureIndices[bitwidth] = 0;
}
- return d_signatureIndices[bitwidth];
+ return d_signatureIndices[bitwidth];
}
void AbstractionModule::resetSignatureIndex() {
for (IndexMap::iterator it = d_signatureIndices.begin(); it != d_signatureIndices.end(); ++it) {
- it->second = 0;
+ it->second = 0;
}
}
}
Node AbstractionModule::getGeneralizedSignature(Node node) {
- NodeNodeMap::const_iterator it = d_assertionToSignature.find(node);
+ NodeNodeMap::const_iterator it = d_assertionToSignature.find(node);
Assert (it != d_assertionToSignature.end());
- Node generalized_signature = getGeneralization(it->second);
- return generalized_signature;
+ Node generalized_signature = getGeneralization(it->second);
+ return generalized_signature;
}
Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
if (cache.find(node) != cache.end()) {
- return cache.find(node)->second;
+ return cache.find(node)->second;
}
-
+
if (node.getNumChildren() == 0) {
if (node.getKind() == kind::CONST_BITVECTOR)
return node;
Node sig = getSignatureSkolem(node);
- cache[node] = sig;
- return sig;
+ cache[node] = sig;
+ return sig;
}
NodeBuilder<> builder(node.getKind());
}
for (unsigned i = 0; i < node.getNumChildren(); ++i) {
Node converted = computeSignatureRec(node[i], cache);
- builder << converted;
+ builder << converted;
}
Node result = builder;
cache[node] = result;
- return result;
+ return result;
}
-/**
+/**
* Returns 0, if the two are equal,
* 1 if s is a generalization of t
* 2 if t is a generalization of s
* -1 if the two cannot be unified
*
- * @param s
- * @param t
- *
- * @return
+ * @param s
+ * @param t
+ *
+ * @return
*/
int AbstractionModule::comparePatterns(TNode s, TNode t) {
if (s.getKind() == kind::SKOLEM &&
t.getKind() == kind::SKOLEM) {
return 0;
}
-
+
if (s.getKind() == kind::CONST_BITVECTOR &&
t.getKind() == kind::CONST_BITVECTOR) {
if (s == t) {
t.getKind() == kind::SKOLEM) {
return 2;
}
-
+
if (s.getNumChildren() != t.getNumChildren() ||
s.getKind() != t.getKind())
return -1;
}
TNode AbstractionModule::getGeneralization(TNode term) {
- NodeNodeMap::iterator it = d_sigToGeneralization.find(term);
+ NodeNodeMap::iterator it = d_sigToGeneralization.find(term);
// if not in the map we add it
if (it == d_sigToGeneralization.end()) {
d_sigToGeneralization[term] = term;
- return term;
+ return term;
}
- // doesn't have a generalization
+ // doesn't have a generalization
if (it->second == term)
return term;
-
+
TNode generalization = getGeneralization(it->second);
Assert (generalization != term);
d_sigToGeneralization[term] = generalization;
- return generalization;
+ return generalization;
}
void AbstractionModule::storeGeneralization(TNode s, TNode t) {
Assert (s == getGeneralization(s));
Assert (t == getGeneralization(t));
- d_sigToGeneralization[s] = t;
+ d_sigToGeneralization[s] = t;
}
void AbstractionModule::finalizeSignatures() {
for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) {
TNode t = getGeneralization(tt->first);
TNode s = getGeneralization(ss->first);
-
+
if (t != s) {
int status = comparePatterns(s, t);
- Assert (status);
+ Assert (status);
if (status < 0)
continue;
if (status == 1) {
- storeGeneralization(t, s);
+ storeGeneralization(t, s);
} else {
- storeGeneralization(s, t);
+ storeGeneralization(s, t);
}
}
}
}
// keep only most general signatures
for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) {
- TNode sig = it->first;
+ TNode sig = it->first;
TNode gen = getGeneralization(sig);
if (sig != gen) {
- Assert (d_signatures.find(gen) != d_signatures.end());
+ Assert (d_signatures.find(gen) != d_signatures.end());
// update the count
d_signatures[gen]+= d_signatures[sig];
- d_signatures.erase(it++);
+ d_signatures.erase(it++);
} else {
++it;
}
// remove signatures that are not frequent enough
for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) {
if (it->second <= 7) {
- d_signatures.erase(it++);
+ d_signatures.erase(it++);
} else {
++it;
}
}
-
+
for (SignatureMap::const_iterator it = d_signatures.begin(); it != d_signatures.end(); ++it) {
TNode signature = it->first;
// we already processed this signature
collectArgumentTypes(signature, arg_types, seen);
Assert (signature.getType().isBoolean());
// make function return a bitvector of size 1
- //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u));
+ //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u));
TypeNode range = NodeManager::currentNM()->mkBitVectorType(1);
-
+
TypeNode abs_type = nm->mkFunctionType(arg_types, range);
Node abs_func = nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory");
Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n";
// NOTE: signature expression type is BOOLEAN
d_signatureToFunc[signature] = abs_func;
- d_funcToSignature[abs_func] = signature;
+ d_funcToSignature[abs_func] = signature;
}
d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size());
-
+
Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " << d_signatureToFunc.size() << " signatures. \n";
}
void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen) {
if (seen.find(sig) != seen.end())
return;
-
+
if (sig.getKind() == kind::SKOLEM) {
types.push_back(sig.getType());
- seen.insert(sig);
- return;
+ seen.insert(sig);
+ return;
}
for (unsigned i = 0; i < sig.getNumChildren(); ++i) {
void AbstractionModule::collectArguments(TNode node, TNode signature, std::vector<Node>& args, TNodeSet& seen) {
if (seen.find(node)!= seen.end())
return;
-
+
if (node.getKind() == kind::VARIABLE ||
node.getKind() == kind::CONST_BITVECTOR) {
// a constant in the node can either map to an argument of the abstraction
- // or can be hard-coded and part of the abstraction
+ // or can be hard-coded and part of the abstraction
if (signature.getKind() == kind::SKOLEM) {
args.push_back(node);
seen.insert(node);
} else {
- Assert (signature.getKind() == kind::CONST_BITVECTOR);
+ Assert (signature.getKind() == kind::CONST_BITVECTOR);
}
- //
- return;
+ //
+ return;
}
Assert (node.getKind() == signature.getKind() &&
- node.getNumChildren() == signature.getNumChildren());
+ node.getNumChildren() == signature.getNumChildren());
for (unsigned i = 0; i < node.getNumChildren(); ++i) {
- collectArguments(node[i], signature[i], args, seen);
- seen.insert(node);
+ collectArguments(node[i], signature[i], args, seen);
+ seen.insert(node);
}
}
Node AbstractionModule::abstractSignatures(TNode assertion) {
- Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n";
+ Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n";
// assume the assertion has been fully abstracted
Node signature = getGeneralizedSignature(assertion);
-
- Debug("bv-abstraction") << " with sig "<< signature <<"\n";
+
+ Debug("bv-abstraction") << " with sig "<< signature <<"\n";
NodeNodeMap::iterator it = d_signatureToFunc.find(signature);
if (it!= d_signatureToFunc.end()) {
std::vector<Node> args;
collectArguments(assertion, signature, args, seen);
std::vector<TNode> real_args;
for (unsigned i = 1; i < args.size(); ++i) {
- real_args.push_back(args[i]);
+ real_args.push_back(args[i]);
}
- d_argsTable.addEntry(func, real_args);
- Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args),
+ d_argsTable.addEntry(func, real_args);
+ Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args),
utils::mkConst(1, 1u));
- Debug("bv-abstraction") << "=> "<< result << "\n";
- Assert (result.getType() == assertion.getType());
- return result;
+ Debug("bv-abstraction") << "=> "<< result << "\n";
+ Assert (result.getType() == assertion.getType());
+ return result;
}
- return assertion;
+ return assertion;
}
bool AbstractionModule::isAbstraction(TNode node) {
if (constant != utils::mkConst(1, 1u))
return false;
- TNode func_symbol = func.getOperator();
+ TNode func_symbol = func.getOperator();
if (d_funcToSignature.find(func_symbol) == d_funcToSignature.end())
return false;
- return true;
+ return true;
}
Node AbstractionModule::getInterpretation(TNode node) {
Assert (constant.getKind() == kind::CONST_BITVECTOR &&
apply.getKind() == kind::APPLY_UF);
- Node func = apply.getOperator();
+ Node func = apply.getOperator();
Assert (d_funcToSignature.find(func) != d_funcToSignature.end());
-
+
Node sig = d_funcToSignature[func];
-
+
// substitute arguments in signature
TNodeTNodeMap seen;
unsigned index = 0;
Node result = substituteArguments(sig, apply, index, seen);
- Assert (result.getType().isBoolean());
+ Assert (result.getType().isBoolean());
Assert (index == apply.getNumChildren());
// Debug("bv-abstraction") << "AbstractionModule::getInterpretation " << node << "\n";
// Debug("bv-abstraction") << " => " << result << "\n";
- return result;
+ return result;
}
Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsigned& index, TNodeTNodeMap& seen) {
if (seen.find(signature) != seen.end()) {
- return seen[signature];
+ return seen[signature];
}
-
+
if (signature.getKind() == kind::SKOLEM) {
// return corresponding argument and increment counter
seen[signature] = apply[index];
- return apply[index++];
+ return apply[index++];
}
if (signature.getNumChildren() == 0) {
Assert (signature.getKind() != kind::VARIABLE &&
- signature.getKind() != kind::SKOLEM);
+ signature.getKind() != kind::SKOLEM);
seen[signature] = signature;
- return signature;
+ return signature;
}
-
+
NodeBuilder<> builder(signature.getKind());
if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) {
builder << signature.getOperator();
}
-
+
for (unsigned i = 0; i < signature.getNumChildren(); ++i) {
Node child = substituteArguments(signature[i], apply, index, seen);
- builder << child;
+ builder << child;
}
- Node result = builder;
+ Node result = builder;
seen[signature]= result;
return result;
if (Dump.isOn("bv-abstraction")) {
NodeNodeMap seen;
Node c = reverseAbstraction(conflict, seen);
- Dump("bv-abstraction") << PushCommand();
+ Dump("bv-abstraction") << PushCommand();
Dump("bv-abstraction") << AssertCommand(c.toExpr());
Dump("bv-abstraction") << CheckSatCommand();
- Dump("bv-abstraction") << PopCommand();
+ Dump("bv-abstraction") << PopCommand();
}
- Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
+ Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
if (conflict.getKind() != kind::AND)
- return conflict;
+ return conflict;
std::vector<Node> conjuncts;
for (unsigned i = 0; i < conflict.getNumChildren(); ++i)
conjuncts.push_back(conflict[i]);
-
+
theory::SubstitutionMap subst(new context::Context());
for (unsigned i = 0; i < conjuncts.size(); ++i) {
TNode conjunct = conjuncts[i];
} else {
continue;
}
-
+
Assert (!subst.hasSubstitution(s));
Assert (!t.isNull() &&
!s.isNull() &&
s!= t);
- subst.addSubstitution(s, t);
+ subst.addSubstitution(s, t);
for (unsigned k = 0; k < conjuncts.size(); k++) {
conjuncts[k] = subst.apply(conjuncts[k]);
}
}
Node new_conflict = Rewriter::rewrite(utils::mkAnd(conjuncts));
-
+
Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n";
Debug("bv-abstraction") << " => " << new_conflict <<"\n";
if (Dump.isOn("bv-abstraction")) {
-
+
NodeNodeMap seen;
Node nc = reverseAbstraction(new_conflict, seen);
- Dump("bv-abstraction") << PushCommand();
+ Dump("bv-abstraction") << PushCommand();
Dump("bv-abstraction") << AssertCommand(nc.toExpr());
Dump("bv-abstraction") << CheckSatCommand();
- Dump("bv-abstraction") << PopCommand();
+ Dump("bv-abstraction") << PopCommand();
}
-
- return new_conflict;
+
+ return new_conflict;
}
void DebugPrintInstantiations(const std::vector< std::vector<ArgsVec> >& instantiations,
const std::vector<TNode> functions) {
// print header
- Debug("bv-abstraction-dbg") <<"[ ";
+ Debug("bv-abstraction-dbg") <<"[ ";
for (unsigned i = 0; i < functions.size(); ++i) {
for (unsigned j = 1; j < functions[i].getNumChildren(); ++j) {
Debug("bv-abstraction-dgb") << functions[i][j] <<" ";
const std::vector<ArgsVec>& inst = instantiations[i];
for (unsigned j = 0; j < inst.size(); ++j) {
for (unsigned k = 0; k < inst[j].size(); ++k) {
- Debug("bv-abstraction-dbg") << inst[j][k] << " ";
+ Debug("bv-abstraction-dbg") << inst[j][k] << " ";
}
- Debug("bv-abstraction-dbg") << " || ";
+ Debug("bv-abstraction-dbg") << " || ";
}
Debug("bv-abstraction-dbg") <<"]\n";
}
}
void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& lemmas) {
- Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n";
+ Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n";
std::vector<TNode> functions;
// collect abstract functions
// if (functions.size() >= 3) {
// // dump conflict
// NodeNodeMap seen;
- // Node reversed = reverseAbstraction(conflict, seen);
- // std::cout << "CONFLICT " << reversed << "\n";
+ // Node reversed = reverseAbstraction(conflict, seen);
+ // std::cout << "CONFLICT " << reversed << "\n";
// }
-
+
if (functions.size() == 0 || functions.size() > options::bvNumFunc()) {
return;
}
SubstitutionMap skolem_subst(new context::Context());
SubstitutionMap reverse_skolem(new context::Context());
makeFreshSkolems(conflict, skolem_subst, reverse_skolem);
-
+
Node skolemized_conflict = skolem_subst.apply(conflict);
for (unsigned i = 0; i < functions.size(); ++i) {
functions[i] = skolem_subst.apply(functions[i]);
}
- conflict = skolem_subst.apply(conflict);
+ conflict = skolem_subst.apply(conflict);
LemmaInstantiatior inst(functions, d_argsTable, conflict);
std::vector<Node> new_lemmas;
- inst.generateInstantiations(new_lemmas);
+ inst.generateInstantiations(new_lemmas);
for (unsigned i = 0; i < new_lemmas.size(); ++i) {
TNode lemma = reverse_skolem.apply(new_lemmas[i]);
if (d_addedLemmas.find(lemma) == d_addedLemmas.end()) {
lemmas.push_back(lemma);
- Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
+ Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
storeLemma(lemma);
if (Dump.isOn("bv-abstraction")) {
NodeNodeMap seen;
Node l = reverseAbstraction(lemma, seen);
- Dump("bv-abstraction") << PushCommand();
+ Dump("bv-abstraction") << PushCommand();
Dump("bv-abstraction") << AssertCommand(l.toExpr());
Dump("bv-abstraction") << CheckSatCommand();
- Dump("bv-abstraction") << PopCommand();
+ Dump("bv-abstraction") << PopCommand();
}
}
}
return -1;
}
-/**
+/**
* Assumes the stack without top is consistent, and checks that the
* full stack is consistent
- *
- * @param stack
- *
- * @return
+ *
+ * @param stack
+ *
+ * @return
*/
bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stack) {
if (stack.empty())
return true;
-
+
unsigned current = stack.size() - 1;
TNode func = d_functions[current];
ArgsTableEntry& matches = d_argsTable.getEntry(func.getOperator());
for (unsigned k = 0; k < args.size(); ++k) {
TNode s = func[k];
TNode t = args[k];
-
+
TNode s0 = s;
while (d_subst.hasSubstitution(s0)) {
s0 = d_subst.getSubstitution(s0);
}
-
+
TNode t0 = t;
while (d_subst.hasSubstitution(t0)) {
t0 = d_subst.getSubstitution(t0);
else
continue;
}
-
+
if(s0.getMetaKind() == kind::metakind::VARIABLE &&
t0.isConst()) {
d_subst.addSubstitution(s0, t0);
Assert (s0.getMetaKind() == kind::metakind::VARIABLE &&
t0.getMetaKind() == kind::metakind::VARIABLE);
-
+
if (s0 != t0) {
d_subst.addSubstitution(s0, t0);
}
}
- return true;
+ return true;
}
bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) {
void AbstractionModule::LemmaInstantiatior::mkLemma() {
Node lemma = d_subst.apply(d_conflict);
// Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::mkLemma " << lemma <<"\n";
- d_lemmas.push_back(lemma);
+ d_lemmas.push_back(lemma);
}
void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
if (!isConsistent(stack))
return;
-
+
if (accept(stack)) {
mkLemma();
return;
d_ctx->push();
stack.push_back(x);
backtrack(stack);
-
+
d_ctx->pop();
stack.pop_back();
x = next(x, stack.size());
void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector<Node>& lemmas) {
- Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations ";
+ Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations ";
std::vector<int> stack;
backtrack(stack);
- Assert (d_ctx->getLevel() == 0);
- Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n";
- lemmas.swap(d_lemmas);
+ Assert (d_ctx->getLevel() == 0);
+ Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n";
+ lemmas.swap(d_lemmas);
}
void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map) {
void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args) {
Assert (fresh_args.size() == 0);
Assert (func.getKind() == kind::APPLY_UF);
- TNodeNodeMap d_map;
+ TNodeNodeMap d_map;
for (unsigned i = 0; i < func.getNumChildren(); ++i) {
TNode arg = func[i];
if (arg.isConst()) {
continue;
}
Assert (arg.getMetaKind() == kind::metakind::VARIABLE);
- TNodeNodeMap::iterator it = d_map.find(arg);
+ TNodeNodeMap::iterator it = d_map.find(arg);
if (it != d_map.end()) {
- fresh_args.push_back(it->second);
+ fresh_args.push_back(it->second);
} else {
Node skolem = utils::mkVar(utils::getSize(arg));
d_map[arg] = skolem;
Debug("bv-abstraction-dbg") <<"\n";
}
-
+
SubstitutionMap subst(new context::Context());
for (unsigned i = 0; i < ss.size(); ++i) {
Assert (s0 != t0);
subst.addSubstitution(s0, t0);
}
-
+
Node res = subst.apply(conflict);
- Debug("bv-abstraction-dbg") << " Lemma: " << res <<"\n";
- return res;
+ Debug("bv-abstraction-dbg") << " Lemma: " << res <<"\n";
+ return res;
}
void AbstractionModule::storeLemma(TNode lemma) {
atom = atom.getKind() == kind::NOT ? atom[0] : atom;
Assert (atom.getKind() != kind::NOT);
Assert (utils::isBVPredicate(atom));
- d_lemmaAtoms.insert(atom);
+ d_lemmaAtoms.insert(atom);
}
} else {
lemma = lemma.getKind() == kind::NOT? lemma[0] : lemma;
bool AbstractionModule::isLemmaAtom(TNode node) const {
Assert (node.getType().isBoolean());
node = node.getKind() == kind::NOT? node[0] : node;
-
+
return d_inputAtoms.find(node) == d_inputAtoms.end() &&
- d_lemmaAtoms.find(node) != d_lemmaAtoms.end();
+ d_lemmaAtoms.find(node) != d_lemmaAtoms.end();
}
void AbstractionModule::addInputAtom(TNode atom) {
void AbstractionModule::ArgsTableEntry::addArguments(const ArgsVec& args) {
Assert (args.size() == d_arity);
- d_data.push_back(args);
+ d_data.push_back(args);
}
void AbstractionModule::ArgsTable::addEntry(TNode signature, const ArgsVec& args) {
if (d_data.find(signature) == d_data.end()) {
- d_data[signature] = ArgsTableEntry(args.size());
+ d_data[signature] = ArgsTableEntry(args.size());
}
ArgsTableEntry& entry = d_data[signature];
- entry.addArguments(args);
+ entry.addArguments(args);
}
bool AbstractionModule::ArgsTable::hasEntry(TNode signature) const {
- return d_data.find(signature) != d_data.end();
+ return d_data.find(signature) != d_data.end();
}
AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode signature) {
Assert (hasEntry(signature));
- return d_data.find(signature)->second;
+ return d_data.find(signature)->second;
}
-AbstractionModule::Statistics::Statistics()
- : d_numFunctionsAbstracted("theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
- , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0)
- , d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime")
+AbstractionModule::Statistics::Statistics(const std::string& name)
+ : d_numFunctionsAbstracted(name + "theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
+ , d_numArgsSkolemized(name + "theory::bv::AbstractioModule::NumArgsSkolemized", 0)
+ , d_abstractionTime(name + "theory::bv::AbstractioModule::AbstractionTime")
{
smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
IntStat d_numFunctionsAbstracted;
IntStat d_numArgsSkolemized;
TimerStat d_abstractionTime;
- Statistics();
+ Statistics(const std::string& name);
~Statistics();
};
-
+
class ArgsTableEntry {
std::vector<ArgsVec> d_data;
unsigned d_arity;
unsigned getArity() { return d_arity; }
unsigned getNumEntries() { return d_data.size(); }
ArgsVec& getEntry(unsigned i ) { Assert (i < d_data.size()); return d_data[i]; }
- };
+ };
class ArgsTable {
__gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
- bool hasEntry(TNode signature) const;
+ bool hasEntry(TNode signature) const;
public:
typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
ArgsTable() {}
iterator end() { return d_data.end(); }
};
- /**
+ /**
* Checks if one pattern is a generalization of the other
- *
- * @param s
- * @param t
- *
+ *
+ * @param s
+ * @param t
+ *
* @return 1 if s :> t, 2 if s <: t, 0 if they equivalent and -1 if they are incomparable
*/
static int comparePatterns(TNode s, TNode t);
theory::SubstitutionMap d_subst;
TNode d_conflict;
std::vector<Node> d_lemmas;
-
+
void backtrack(std::vector<int>& stack);
int next(int val, int index);
bool isConsistent(const std::vector<int>& stack);
, d_conflict(conflict)
, d_lemmas()
{
- Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n";
+ Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n";
// initializing the search space
for (unsigned i = 0; i < functions.size(); ++i) {
TNode func_op = functions[i].getOperator();
}
}
- void generateInstantiations(std::vector<Node>& lemmas);
-
+ void generateInstantiations(std::vector<Node>& lemmas);
+
};
-
+
typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
- typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap;
+ typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap;
typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap;
typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap;
typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
-
- ArgsTable d_argsTable;
+
+ ArgsTable d_argsTable;
// mapping between signature and uninterpreted function symbol used to
// abstract the signature
NodeNodeMap d_signatureToFunc;
- NodeNodeMap d_funcToSignature;
+ NodeNodeMap d_funcToSignature;
- NodeNodeMap d_assertionToSignature;
+ NodeNodeMap d_assertionToSignature;
SignatureMap d_signatures;
- NodeNodeMap d_sigToGeneralization;
+ NodeNodeMap d_sigToGeneralization;
TNodeSet d_skolems;
// skolems maps
Node getGeneralizedSignature(Node node);
Node getSignatureSkolem(TNode node);
- unsigned getBitwidthIndex(unsigned bitwidth);
+ unsigned getBitwidthIndex(unsigned bitwidth);
void resetSignatureIndex();
Node computeSignatureRec(TNode, NodeNodeMap&);
void storeSignature(Node signature, TNode assertion);
// crazy instantiation methods
void generateInstantiations(unsigned current,
- std::vector<ArgsTableEntry>& matches,
+ std::vector<ArgsTableEntry>& matches,
std::vector<std::vector<ArgsVec> >& instantiations,
std::vector<std::vector<ArgsVec> >& new_instantiations);
Node tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict);
void makeFreshArgs(TNode func, std::vector<Node>& fresh_args);
void makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map);
-
+
void skolemizeArguments(std::vector<Node>& assertions);
Node reverseAbstraction(Node assertion, NodeNodeMap& seen);
void storeLemma(TNode lemma);
Statistics d_statistics;
-
+
public:
- AbstractionModule()
+ AbstractionModule(const std::string& name)
: d_argsTable()
, d_signatureToFunc()
, d_funcToSignature()
, d_addedLemmas()
, d_lemmaAtoms()
, d_inputAtoms()
- , d_statistics()
+ , d_statistics(name)
{}
- /**
+ /**
* returns true if there are new uninterepreted functions symbols in the output
- *
- * @param assertions
- * @param new_assertions
- *
- * @return
+ *
+ * @param assertions
+ * @param new_assertions
+ *
+ * @return
*/
bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
- /**
- * Returns true if the node represents an abstraction predicate.
- *
- * @param node
- *
- * @return
+ /**
+ * Returns true if the node represents an abstraction predicate.
+ *
+ * @param node
+ *
+ * @return
*/
bool isAbstraction(TNode node);
- /**
- * Returns the interpretation of the abstraction predicate.
- *
- * @param node
- *
- * @return
+ /**
+ * Returns the interpretation of the abstraction predicate.
+ *
+ * @param node
+ *
+ * @return
*/
Node getInterpretation(TNode node);
- Node simplifyConflict(TNode conflict);
+ Node simplifyConflict(TNode conflict);
void generalizeConflict(TNode conflict, std::vector<Node>& lemmas);
void addInputAtom(TNode atom);
bool isLemmaAtom(TNode node) const;
BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
: SubtheorySolver(c, bv),
- d_bitblaster(new TLazyBitblaster(c, bv, "lazy")),
+ d_bitblaster(new TLazyBitblaster(c, bv, bv->getFullInstanceName() + "lazy")),
d_bitblastQueue(c),
- d_statistics(),
+ d_statistics(bv->getFullInstanceName()),
d_validModelCache(c, true),
d_lemmaAtomsQueue(c),
d_useSatPropagation(options::bitvectorPropagate()),
delete d_bitblaster;
}
-BitblastSolver::Statistics::Statistics()
- : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
- , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
+BitblastSolver::Statistics::Statistics(const std::string &instanceName)
+ : d_numCallstoCheck(instanceName + "theory::bv::BitblastSolver::NumCallsToCheck", 0)
+ , d_numBBLemmas(instanceName + "theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
{
smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
}
void BitblastSolver::setAbstraction(AbstractionModule* abs) {
- d_abstractionModule = abs;
- d_bitblaster->setAbstraction(abs);
+ d_abstractionModule = abs;
+ d_bitblaster->setAbstraction(abs);
}
void BitblastSolver::preRegister(TNode node) {
bool BitblastSolver::check(Theory::Effort e) {
Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
- Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+ Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
++(d_statistics.d_numCallstoCheck);
// skip atoms that are the result of abstraction lemmas
if (d_abstractionModule->isLemmaAtom(fact)) {
d_lemmaAtomsQueue.push_back(fact);
- continue;
+ continue;
}
}
-
+
if (!d_bv->inConflict() &&
(!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
// Some atoms have not been bit-blasted yet
if (options::bvAbstraction() &&
e == Theory::EFFORT_FULL &&
d_lemmaAtomsQueue.size()) {
-
+
// bit-blast lemma atoms
while(!d_lemmaAtomsQueue.empty()) {
TNode lemma_atom = d_lemmaAtomsQueue.front();
return false;
}
}
-
+
Assert(!d_bv->inConflict());
bool ok = d_bitblaster->solve();
if (!ok) {
++(d_statistics.d_numBBLemmas);
return false;
}
-
+
}
-
+
return true;
}
Node BitblastSolver::getModelValue(TNode node)
{
if (d_bv->d_invalidateModelCache.get()) {
- d_bitblaster->invalidateModelCache();
+ d_bitblaster->invalidateModelCache();
}
- d_bv->d_invalidateModelCache.set(false);
+ d_bv->d_invalidateModelCache.set(false);
Node val = d_bitblaster->getTermModel(node, true);
return val;
}
Node final_conflict = conflict;
if (options::bitvectorQuickXplain() &&
conflict.getKind() == kind::AND) {
- // std::cout << "Original conflict " << conflict.getNumChildren() << "\n";
+ // std::cout << "Original conflict " << conflict.getNumChildren() << "\n";
final_conflict = d_quickXplain->minimizeConflict(conflict);
- //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n";
+ //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n";
}
d_bv->setConflict(final_conflict);
}
}/* namespace CVC4::theory::bv */
}/* namespace CVC4::theory */
}/* namespace CVC4 */
-
struct Statistics {
IntStat d_numCallstoCheck;
IntStat d_numBBLemmas;
- Statistics();
+ Statistics(const std::string &instanceName);
~Statistics();
};
/** Bitblaster */
Node getModelValue(TNode node);
bool isComplete() { return true; }
void bitblastQueue();
- void setAbstraction(AbstractionModule* module);
- uint64_t computeAtomWeight(TNode atom);
+ void setAbstraction(AbstractionModule* module);
+ uint64_t computeAtomWeight(TNode atom);
void setProofLog( BitVectorProof * bvp );
};
namespace theory {
namespace bv {
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
- : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, std::string name)
+ : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
d_context(c),
d_alreadyPropagatedSet(c),
d_sharedTermsSet(c),
d_subtheories(),
d_subtheoryMap(),
- d_statistics(),
+ d_statistics(getFullInstanceName()),
d_staticLearnCache(),
d_BVDivByZero(),
d_BVRemByZero(),
d_literalsToPropagateIndex(c, 0),
d_propagatedBy(c),
d_eagerSolver(NULL),
- d_abstractionModule(new AbstractionModule()),
+ d_abstractionModule(new AbstractionModule(getFullInstanceName())),
d_isCoreTheory(false),
d_calledPreregister(false)
{
getOutputChannel().spendResource(ammount);
}
-TheoryBV::Statistics::Statistics():
- d_avgConflictSize("theory::bv::AvgBVConflictSize"),
- d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
- d_solveTimer("theory::bv::solveTimer"),
- d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
- d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0),
- d_weightComputationTimer("theory::bv::weightComputationTimer"),
- d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
+TheoryBV::Statistics::Statistics(const std::string &name):
+ d_avgConflictSize(name + "theory::bv::AvgBVConflictSize"),
+ d_solveSubstitutions(name + "theory::bv::NumberOfSolveSubstitutions", 0),
+ d_solveTimer(name + "theory::bv::solveTimer"),
+ d_numCallsToCheckFullEffort(name + "theory::bv::NumberOfFullCheckCalls", 0),
+ d_numCallsToCheckStandardEffort(name + "theory::bv::NumberOfStandardCheckCalls", 0),
+ d_weightComputationTimer(name + "theory::bv::weightComputationTimer"),
+ d_numMultSlice(name + "theory::bv::NumMultSliceApplied", 0)
{
smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
for (unsigned i = 0; i < args1.getNumChildren(); ++i) {
eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
}
-
+
Node args_eq = eqs.size() == 1 ? eqs[0] : nm->mkNode(kind::AND, eqs);
Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
// if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
// // Ackermanize UF if using eager bit-blasting
- // Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
+ // Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
// node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
- // return node;
+ // return node;
// } else {
Node divByZero = getBVDivByZero(node.getKind(), width);
Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
if (d_conflictNode.isNull()) {
return;
} else {
- Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
+ Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
d_out->conflict(d_conflictNode);
d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
d_conflictNode = Node::null();
// return the explanation
Node explanation = utils::mkAnd(assumptions);
Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
- Debug("bitvector::explain") << "TheoryBV::explain done. \n";
+ Debug("bitvector::explain") << "TheoryBV::explain done. \n";
return explanation;
}
{
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
return EQUALITY_UNKNOWN;
- Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+ Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
if (status != EQUALITY_UNKNOWN) {
public:
TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo);
+ Valuation valuation, const LogicInfo& logicInfo,
+ std::string name = "");
~TheoryBV();
void presolve();
- bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-
+ bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+
void setProofLog( BitVectorProof * bvp );
private:
IntStat d_solveSubstitutions;
TimerStat d_solveTimer;
IntStat d_numCallsToCheckFullEffort;
- IntStat d_numCallsToCheckStandardEffort;
+ IntStat d_numCallsToCheckStandardEffort;
TimerStat d_weightComputationTimer;
IntStat d_numMultSlice;
- Statistics();
+ Statistics(const std::string &name);
~Statistics();
};
*/
Node getBVDivByZero(Kind k, unsigned width);
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
void collectFunctionSymbols(TNode term, TNodeSet& seen);
void storeFunction(TNode func, TNode term);
typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
NodeSet d_staticLearnCache;
-
+
/**
* Maps from bit-vector width to division-by-zero uninterpreted
* function symbols.
CVC4::theory::SubstitutionMap d_funcToSkolem;
context::CDO<bool> d_lemmasAdded;
-
+
// Are we in conflict?
context::CDO<bool> d_conflict;
typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
PropagatedMap d_propagatedBy;
- EagerBitblastSolver* d_eagerSolver;
+ EagerBitblastSolver* d_eagerSolver;
AbstractionModule* d_abstractionModule;
bool d_isCoreTheory;
bool d_calledPreregister;
-
+
bool wasPropagatedBySubtheory(TNode literal) const {
- return d_propagatedBy.find(literal) != d_propagatedBy.end();
+ return d_propagatedBy.find(literal) != d_propagatedBy.end();
}
-
+
SubTheory getPropagatingSubtheory(TNode literal) const {
- Assert(wasPropagatedBySubtheory(literal));
+ Assert(wasPropagatedBySubtheory(literal));
PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
return (*find).second;
}
void addSharedTerm(TNode t);
bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
-
+
EqualityStatus getEqualityStatus(TNode a, TNode b);
Node getModelValue(TNode var);
void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; }
- void checkForLemma(TNode node);
+ void checkForLemma(TNode node);
friend class LazyBitblaster;
friend class TLazyBitblaster;
#include "options/bv_options.h"
#include "options/options.h"
#include "options/quantifiers_options.h"
+#include "proof/cnf_proof.h"
+#include "proof/lemma_proof.h"
#include "proof/proof_manager.h"
#include "proof/theory_proof.h"
#include "smt/ite_removal.h"
namespace CVC4 {
+inline void flattenAnd(Node n, std::vector<TNode>& out){
+ Assert(n.getKind() == kind::AND);
+ for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
+ Node curr = *i;
+ if(curr.getKind() == kind::AND){
+ flattenAnd(curr, out);
+ }else{
+ out.push_back(curr);
+ }
+ }
+}
+
+inline Node flattenAnd(Node n){
+ std::vector<TNode> out;
+ flattenAnd(n, out);
+ return NodeManager::currentNM()->mkNode(kind::AND, out);
+}
+
+theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
+ ProofRule rule,
+ bool removable,
+ bool preprocess,
+ bool sendAtoms)
+ throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+ Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << ", preprocess = " << preprocess << std::endl;
+ ++ d_statistics.lemmas;
+ d_engine->d_outputChannelUsed = true;
+
+ LemmaProofRecipe* proofRecipe = NULL;
+ PROOF({
+ // Theory lemmas have one step that proves the empty clause
+ proofRecipe = new LemmaProofRecipe;
+
+ Node emptyNode;
+ LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode);
+
+ Node rewritten;
+ if (lemma.getKind() == kind::OR) {
+ for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
+ rewritten = theory::Rewriter::rewrite(lemma[i]);
+ if (rewritten != lemma[i]) {
+ proofRecipe->addRewriteRule(lemma[i].negate(), rewritten.negate());
+ }
+ proofStep.addAssertion(lemma[i]);
+ proofRecipe->addBaseAssertion(rewritten);
+ }
+ } else {
+ rewritten = theory::Rewriter::rewrite(lemma);
+ if (rewritten != lemma) {
+ proofRecipe->addRewriteRule(lemma.negate(), rewritten.negate());
+ }
+ proofStep.addAssertion(lemma);
+ proofRecipe->addBaseAssertion(rewritten);
+ }
+ proofRecipe->addStep(proofStep);
+ });
+
+ theory::LemmaStatus result = d_engine->lemma(lemma,
+ rule,
+ false,
+ removable,
+ preprocess,
+ sendAtoms ? d_theory : theory::THEORY_LAST,
+ proofRecipe);
+ PROOF(delete proofRecipe;);
+ return result;
+}
+
+theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable)
+ throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+ Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
+ ++ d_statistics.lemmas;
+ d_engine->d_outputChannelUsed = true;
+
+
+ LemmaProofRecipe* proofRecipe = NULL;
+ Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl;
+ theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, proofRecipe);
+ return result;
+}
+
+bool TheoryEngine::EngineOutputChannel::propagate(TNode literal)
+ throw(AssertionException, UnsafeInterruptException) {
+ Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
+ ++ d_statistics.propagations;
+ d_engine->d_outputChannelUsed = true;
+ return d_engine->propagate(literal, d_theory);
+}
+
+void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf)
+ throw(AssertionException, UnsafeInterruptException) {
+ Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
+ Assert (pf == NULL); // Theory shouldn't be producing proofs yet
+ ++ d_statistics.conflicts;
+ d_engine->d_outputChannelUsed = true;
+ d_engine->conflict(conflictNode, d_theory);
+}
+
void TheoryEngine::finishInit() {
// initialize the quantifiers engine
d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
// We need to split on it
Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
- lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, carePair.theory);
+
+ LemmaProofRecipe* proofRecipe = NULL;
+ lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe);
+
// This code is supposed to force preference to follow what the theory models already have
// but it doesn't seem to make a big difference - need to explore more -Clark
// if (true) {
void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
- Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl;
+ Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
Assert(toTheoryId != fromTheoryId);
if(toTheoryId != THEORY_SAT_SOLVER &&
assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
}
} else {
+ // We could be propagating a unit-clause lemma. In this case, we need to provide a
+ // recipe.
+ // TODO: Consider putting this someplace else? This is the only refence to the proof
+ // manager in this class.
+
+ PROOF({
+ LemmaProofRecipe proofRecipe;
+ proofRecipe.addBaseAssertion(literal);
+
+ Node emptyNode;
+ LemmaProofRecipe::ProofStep proofStep(theory, emptyNode);
+ proofStep.addAssertion(literal);
+ proofRecipe.addStep(proofStep);
+
+ ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
+ });
+
// Just send off to the SAT solver
Assert(d_propEngine->isSatLiteral(literal));
assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
return conjunction;
}
-NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) {
+Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) {
Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
bool polarity = node.getKind() != kind::NOT;
// If we're not in shared mode, explanations are simple
if (!d_logicInfo.isSharingEnabled()) {
+ Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. "
+ << " Responsible theory is: "
+ << theoryOf(atom)->getId() << std::endl;
+
Node explanation = theoryOf(atom)->explain(node);
Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
- return NodeTheoryPair(explanation, theoryOf(atom)->getId());
+ PROOF({
+ if(proofRecipe) {
+ Node emptyNode;
+ LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode);
+ proofStep.addAssertion(node);
+ proofRecipe->addBaseAssertion(node);
+
+ if (explanation.getKind() == kind::AND) {
+ // If the explanation is a conjunction, the recipe for the corresponding lemma is
+ // the negation of its conjuncts.
+ Node flat = flattenAnd(explanation);
+ for (unsigned i = 0; i < flat.getNumChildren(); ++i) {
+ if (flat[i].isConst() && flat[i].getConst<bool>()) {
+ ++ i;
+ continue;
+ }
+ if (flat[i].getKind() == kind::NOT &&
+ flat[i][0].isConst() && !flat[i][0].getConst<bool>()) {
+ ++ i;
+ continue;
+ }
+ Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: "
+ << flat[i].negate() << std::endl;
+ proofStep.addAssertion(flat[i].negate());
+ proofRecipe->addBaseAssertion(flat[i].negate());
+ }
+ } else {
+ // The recipe for proving it is by negating it. "True" is not an acceptable reason.
+ if (!((explanation.isConst() && explanation.getConst<bool>()) ||
+ (explanation.getKind() == kind::NOT &&
+ explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
+ proofStep.addAssertion(explanation.negate());
+ proofRecipe->addBaseAssertion(explanation.negate());
+ }
+ }
+
+ proofRecipe->addStep(proofStep);
+ }
+ });
+
+ return explanation;
}
+ Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl;
+
// Initial thing to explain
NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
+ Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node "
+ << nodeExplainerPair.node
+ << " is theory: " << nodeExplainerPair.theory << std::endl;
TheoryId explainer = nodeExplainerPair.theory;
// Create the workplace for explanations
std::vector<NodeTheoryPair> explanationVector;
explanationVector.push_back(d_propagationMap[toExplain]);
// Process the explanation
- getExplanation(explanationVector);
+ if (proofRecipe) {
+ Node emptyNode;
+ LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode);
+ proofStep.addAssertion(node);
+ proofRecipe->addStep(proofStep);
+ proofRecipe->addBaseAssertion(node);
+ }
+
+ getExplanation(explanationVector, proofRecipe);
Node explanation = mkExplanation(explanationVector);
Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
- return NodeTheoryPair(explanation, explainer);
+ return explanation;
}
Node TheoryEngine::getExplanation(TNode node) {
- return getExplanationAndExplainer(node).node;
+ LemmaProofRecipe *dontCareRecipe = NULL;
+ return getExplanationAndRecipe(node, dontCareRecipe);
}
struct AtomsCollect {
bool removable,
bool preprocess,
theory::TheoryId atomsTo,
- theory::TheoryId ownerTheory) {
+ LemmaProofRecipe* proofRecipe) {
// For resource-limiting (also does a time check).
// spendResource();
}
// assert to prop engine
- d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, ownerTheory, node);
+ d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node);
for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
- d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, ownerTheory, node);
+ d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node);
}
// WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
<< CheckSatCommand(conflict.toExpr());
}
+ LemmaProofRecipe* proofRecipe = NULL;
+ PROOF({
+ proofRecipe = new LemmaProofRecipe;
+ Node emptyNode;
+ LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
+
+ if (conflict.getKind() == kind::AND) {
+ for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
+ proofStep.addAssertion(conflict[i].negate());
+ }
+ } else {
+ proofStep.addAssertion(conflict.negate());
+ }
+
+ proofRecipe->addStep(proofStep);
+ });
+
// In the multiple-theories case, we need to reconstruct the conflict
if (d_logicInfo.isSharingEnabled()) {
// Create the workplace for explanations
std::vector<NodeTheoryPair> explanationVector;
explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
+
// Process the explanation
- getExplanation(explanationVector);
+ getExplanation(explanationVector, proofRecipe);
Node fullConflict = mkExplanation(explanationVector);
Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
Assert(properConflict(fullConflict));
- lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId);
+ lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
+
} else {
// When only one theory, the conflict should need no processing
Assert(properConflict(conflict));
- lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId);
+ PROOF({
+ if (conflict.getKind() == kind::AND) {
+ // If the conflict is a conjunction, the corresponding lemma is derived by negating
+ // its conjuncts.
+ for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
+ if (conflict[i].isConst() && conflict[i].getConst<bool>()) {
+ ++ i;
+ continue;
+ }
+ if (conflict[i].getKind() == kind::NOT &&
+ conflict[i][0].isConst() && !conflict[i][0].getConst<bool>()) {
+ ++ i;
+ continue;
+ }
+ proofRecipe->getStep(0)->addAssertion(conflict[i].negate());
+ proofRecipe->addBaseAssertion(conflict[i].negate());
+ }
+ } else {
+ proofRecipe->getStep(0)->addAssertion(conflict.negate());
+ proofRecipe->addBaseAssertion(conflict.negate());
+ }
+ });
+
+ lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
}
+
+ PROOF({
+ delete proofRecipe;
+ proofRecipe = NULL;
+ });
}
void TheoryEngine::staticInitializeBVOptions(const std::vector<Node>& assertions) {
return result;
}
-void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector)
-{
+void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
Assert(explanationVector.size() > 0);
unsigned i = 0; // Index of the current literal we are processing
unsigned j = 0; // Index of the last literal we are keeping
- while (i < explanationVector.size()) {
+ std::set<Node> inputAssertions;
+ PROOF(inputAssertions = proofRecipe->getStep(0)->getAssertions(););
+ while (i < explanationVector.size()) {
// Get the current literal to explain
NodeTheoryPair toExplain = explanationVector[i];
- Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
+ Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
+
// If a true constant or a negation of a false constant we can ignore it
if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
// If from the SAT solver, keep it
if (toExplain.theory == THEORY_SAT_SOLVER) {
+ Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
explanationVector[j++] = explanationVector[i++];
continue;
}
// See if it was sent to the theory by another theory
PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
if (find != d_propagationMap.end()) {
+ Debug("theory::explain") << "\tTerm was propagated by another theory (theory = "
+ << theoryOf((*find).second.theory)->getId() << ")" << std::endl;
// There is some propagation, check if its a timely one
if ((*find).second.timestamp < toExplain.timestamp) {
+ Debug("theory::explain") << "\tRelevant timetsamp, pushing "
+ << (*find).second.node << "to index = " << explanationVector.size() << std::endl;
explanationVector.push_back((*find).second);
- ++ i;
+ ++i;
+
+ PROOF({
+ if (toExplain.node != (*find).second.node) {
+ Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node
+ << ", toExplain = " << (*find).second.node << std::endl;
+
+ if (proofRecipe) {
+ proofRecipe->addRewriteRule(toExplain.node, (*find).second.node);
+ }
+ }
+ })
+
continue;
}
}
Node explanation;
if (toExplain.theory == THEORY_BUILTIN) {
explanation = d_sharedTerms.explain(toExplain.node);
+ Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
} else {
explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
+ Debug("theory::explain") << "\tTerm was propagated by owner theory: "
+ << theoryOf(toExplain.theory)->getId()
+ << ". Explanation: " << explanation << std::endl;
}
+
Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl;
Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
// Mark the explanation
NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
explanationVector.push_back(newExplain);
+
++ i;
+
+ PROOF({
+ if (proofRecipe) {
+ // If we're expanding the target node of the explanation (this is the first expansion...),
+ // we don't want to add it as a separate proof step. It is already part of the assertions.
+ if (inputAssertions.find(toExplain.node) == inputAssertions.end()) {
+ LemmaProofRecipe::ProofStep proofStep(toExplain.theory, toExplain.node);
+ if (explanation.getKind() == kind::AND) {
+ Node flat = flattenAnd(explanation);
+ for (unsigned k = 0; k < flat.getNumChildren(); ++ k) {
+ // If a true constant or a negation of a false constant we can ignore it
+ if (! ((flat[k].isConst() && flat[k].getConst<bool>()) ||
+ (flat[k].getKind() == kind::NOT && flat[k][0].isConst() && !flat[k][0].getConst<bool>()))) {
+ proofStep.addAssertion(flat[k].negate());
+ }
+ }
+ } else {
+ if (! ((explanation.isConst() && explanation.getConst<bool>()) ||
+ (explanation.getKind() == kind::NOT && explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
+ proofStep.addAssertion(explanation.negate());
+ }
+ }
+ proofRecipe->addStep(proofStep);
+ }
+ }
+ });
}
// Keep only the relevant literals
explanationVector.resize(j);
-}
+ PROOF({
+ if (proofRecipe) {
+ // The remaining literals are the base of the proof
+ for (unsigned k = 0; k < explanationVector.size(); ++k) {
+ proofRecipe->addBaseAssertion(explanationVector[k].node.negate());
+ }
+ }
+ });
+}
void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
{
namespace CVC4 {
class ResourceManager;
+class LemmaProofRecipe;
/**
* A pair of a theory and a node. This is used to mark the flow of
}
}
- void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) {
- Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
- Assert(pf == NULL); // theory shouldn't be producing proofs yet
- ++ d_statistics.conflicts;
- d_engine->d_outputChannelUsed = true;
- d_engine->conflict(conflictNode, d_theory);
- }
+ void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException);
- bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) {
- Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
- ++ d_statistics.propagations;
- d_engine->d_outputChannelUsed = true;
- return d_engine->propagate(literal, d_theory);
- }
+ bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException);
theory::LemmaStatus lemma(TNode lemma,
ProofRule rule,
bool removable = false,
bool preprocess = false,
bool sendAtoms = false)
- throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
- Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
- ++ d_statistics.lemmas;
- d_engine->d_outputChannelUsed = true;
- return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST, d_theory);
- }
+ throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException);
- /*theory::LemmaStatus preservedLemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) {
- Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::preservedLemma(" << lemma << ")" << std::endl;
- ++ d_statistics.lemmas;
- d_engine->d_outputChannelUsed = true;
- return d_engine->lemma(lemma, false, removable, preprocess, d_theory);
- }*/
-
- theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
- Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::splitLemma(" << lemma << ")" << std::endl;
- ++ d_statistics.lemmas;
- d_engine->d_outputChannelUsed = true;
- return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, d_theory);
- }
+ theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException);
void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
NodeManager* curr = NodeManager::currentNM();
bool removable,
bool preprocess,
theory::TheoryId atomsTo,
- theory::TheoryId ownerTheory);
+ LemmaProofRecipe* proofRecipe);
/** Enusre that the given atoms are send to the given theory */
void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
* asking relevant theories to explain the propagations. Initially
* the explanation vector should contain only the element (node, theory)
* where the node is the one to be explained, and the theory is the
- * theory that sent the literal.
+ * theory that sent the literal. The lemmaProofRecipe will contain a list
+ * of the explanation steps required to produce the original node.
*/
- void getExplanation(std::vector<NodeTheoryPair>& explanationVector);
+ void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe);
public:
* Returns an explanation of the node propagated to the SAT solver and the theory
* that propagated it.
*/
- NodeTheoryPair getExplanationAndExplainer(TNode node);
+ Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);
/**
* collect model info
std::vector<EqProof *> orderedChildren;
bool nullCongruenceFound = false;
for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
- if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) {
-
- // For now, assume there can only be one null congruence child
- Assert(!nullCongruenceFound);
+ if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE &&
+ eqpc->d_children[i]->d_node.isNull()) {
nullCongruenceFound = true;
-
Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl;
orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]);
orderedChildren.push_back(eqpc->d_children[i]->d_children[1]);
getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc);
if( eqpc ) {
eqpc->d_children.push_back( eqpcc );
+
+ Debug("pf::ee") << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" << std::endl;
+ eqpc->debug_print("pf::ee", 1);
}
}
}
void EqualityEngine::debugPrintGraph() const {
+ Debug("equality::graph") << std::endl << "Dumping graph" << std::endl;
for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) {
Debug("equality::graph") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):";
Debug("equality::graph") << std::endl;
}
+ Debug("equality::graph") << std::endl;
}
bool EqualityEngine::areEqual(TNode t1, TNode t2) const {
return d_current == null_id;
}
-void EqProof::debug_print( const char * c, unsigned tb ) const{
- for( unsigned i=0; i<tb; i++ ) { Debug( c ) << " "; }
- Debug( c ) << d_id << "(";
+void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const {
+ for(unsigned i=0; i<tb; i++) { Debug( c ) << " "; }
+
+ if (prettyPrinter)
+ Debug( c ) << prettyPrinter->printTag(d_id);
+ else
+ Debug( c ) << d_id;
+
+ Debug( c ) << "(";
if( !d_children.empty() || !d_node.isNull() ){
if( !d_node.isNull() ){
Debug( c ) << std::endl;
for( unsigned i=0; i<d_children.size(); i++ ){
if( i>0 || !d_node.isNull() ) Debug( c ) << ",";
Debug( c ) << std::endl;
- d_children[i]->debug_print( c, tb+1 );
+ d_children[i]->debug_print( c, tb+1, prettyPrinter );
}
}
Debug( c ) << ")" << std::endl;
class EqProof
{
public:
+ class PrettyPrinter {
+ public:
+ virtual ~PrettyPrinter() {}
+ virtual std::string printTag(unsigned tag) = 0;
+ };
+
EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
unsigned d_id;
Node d_node;
std::vector< EqProof * > d_children;
- void debug_print( const char * c, unsigned tb = 0 ) const;
+ void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const;
};/* class EqProof */
} // Namespace eq
void TheoryUF::computeCareGraph() {
if (d_sharedTerms.size() > 0) {
- //use term indexing
+ //use term indexing
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
std::map< Node, quantifiers::TermArgTrie > index;
std::map< Node, unsigned > arity;
void TheoryUF::conflict(TNode a, TNode b) {
eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
+
if (a.getKind() == kind::CONST_BOOLEAN) {
d_conflictNode = explain(a.iffNode(b),pf);
} else {
bug00.smt \
bug338.smt2 \
bug347.smt \
- bug348.smt \
bug451.smt \
bug509.smt \
bug580.smt2 \
projects / cvc5.git / commitdiff