+++ /dev/null
-; Depends on th_real.plf, smt.plf, sat.plf
-
-; LRA proofs have the following interface:
-; * Given predicates between real terms
-; * Prove bottom
-;
-; However, even though the type of the interface does not express this,
-; the predicates are **linear bounds**, not arbitrary real bounds. Thus
-; LRA proofs have the following structure:
-;
-; 1. Prove that the input predicates are equivalent to a set of linear
-; bounds.
-; 2. Use the linear bounds to prove bottom using farkas coefficients.
-;
-; Notice that the distinction between linear bounds (associated in the signature
-; with the string "poly") and real predicates (which relate "term Real"s to one
-; another) matters quite a bit. We have certain kinds of axioms for one, and
-; other axioms for the other.
-
-(program mpq_ifpos ((x mpq)) bool
- (mp_ifneg x ff (mp_ifzero x ff tt)))
-
-; a real variable
-(declare var_real type)
-; a real variable term
-(declare a_var_real (! v var_real (term Real)))
-
-;; linear polynomials in the form a_1*x_1 + a_2*x_2 .... + a_n*x_n
-
-(declare lmon type)
-(declare lmonn lmon)
-(declare lmonc (! c mpq (! v var_real (! l lmon lmon))))
-
-(program lmon_neg ((l lmon)) lmon
- (match l
- (lmonn l)
- ((lmonc c' v' l') (lmonc (mp_neg c') v' (lmon_neg l')))))
-
-(program lmon_add ((l1 lmon) (l2 lmon)) lmon
- (match l1
- (lmonn l2)
- ((lmonc c' v' l')
- (match l2
- (lmonn l1)
- ((lmonc c'' v'' l'')
- (compare v' v''
- (lmonc c' v' (lmon_add l' l2))
- (lmonc c'' v'' (lmon_add l1 l''))))))))
-
-(program lmon_mul_c ((l lmon) (c mpq)) lmon
- (match l
- (lmonn l)
- ((lmonc c' v' l') (lmonc (mp_mul c c') v' (lmon_mul_c l' c)))))
-
-;; linear polynomials in the form (a_1*x_1 + a_2*x_2 .... + a_n*x_n) + c
-
-(declare poly type)
-(declare polyc (! c mpq (! l lmon poly)))
-
-(program poly_neg ((p poly)) poly
- (match p
- ((polyc m' p') (polyc (mp_neg m') (lmon_neg p')))))
-
-(program poly_add ((p1 poly) (p2 poly)) poly
- (match p1
- ((polyc c1 l1)
- (match p2
- ((polyc c2 l2) (polyc (mp_add c1 c2) (lmon_add l1 l2)))))))
-
-(program poly_sub ((p1 poly) (p2 poly)) poly
- (poly_add p1 (poly_neg p2)))
-
-(program poly_mul_c ((p poly) (c mpq)) poly
- (match p
- ((polyc c' l') (polyc (mp_mul c' c) (lmon_mul_c l' c)))))
-
-;; code to isolate a variable from a term
-;; if (isolate v l) returns (c,l'), this means l = c*v + l', where v is not in FV(t').
-
-(declare isol type)
-(declare isolc (! r mpq (! l lmon isol)))
-
-(program isolate_h ((v var_real) (l lmon) (e bool)) isol
- (match l
- (lmonn (isolc 0/1 l))
- ((lmonc c' v' l')
- (ifmarked v'
- (match (isolate_h v l' tt)
- ((isolc ci li) (isolc (mp_add c' ci) li)))
- (match e
- (tt (isolc 0/1 l))
- (ff (match (isolate_h v l' ff)
- ((isolc ci li) (isolc ci (lmonc c' v' li))))))))))
-
-(program isolate ((v var_real) (l lmon)) isol
- (do (markvar v)
- (let i (isolate_h v l ff)
- (do (markvar v) i))))
-
-;; determine if a monomial list is constant
-
-(program is_lmon_zero ((l lmon)) bool
- (match l
- (lmonn tt)
- ((lmonc c v l')
- (match (isolate v l)
- ((isolc ci li)
- (mp_ifzero ci (is_lmon_zero li) ff))))))
-
-;; return the constant that p is equal to. If p is not constant, fail.
-
-(program is_poly_const ((p poly)) mpq
- (match p
- ((polyc c' l')
- (match (is_lmon_zero l')
- (tt c')
- (ff (fail mpq))))))
-
-;; conversion to use polynomials in term formulas
-
-
-(declare >=0_poly (! x poly formula))
-(declare =0_poly (! x poly formula))
-(declare >0_poly (! x poly formula))
-(declare distinct0_poly (! x poly formula))
-
-;; create new equality out of inequality
-
-(declare lra_>=_>=_to_=
- (! p1 poly
- (! p2 poly
- (! f1 (th_holds (>=0_poly p1))
- (! f2 (th_holds (>=0_poly p2))
- (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
- (th_holds (=0_poly p2))))))))
-
-;; axioms
-
-(declare lra_axiom_=
- (th_holds (=0_poly (polyc 0/1 lmonn))))
-
-(declare lra_axiom_>
- (! c mpq
- (! i (^ (mpq_ifpos c) tt)
- (th_holds (>0_poly (polyc c lmonn))))))
-
-(declare lra_axiom_>=
- (! c mpq
- (! i (^ (mp_ifneg c tt ff) ff)
- (th_holds (>=0_poly (polyc c lmonn))))))
-
-(declare lra_axiom_distinct
- (! c mpq
- (! i (^ (mp_ifzero c tt ff) ff)
- (th_holds (distinct0_poly (polyc c lmonn))))))
-
-;; contradiction rules
-
-(declare lra_contra_=
- (! p poly
- (! f (th_holds (=0_poly p))
- (! i (^ (mp_ifzero (is_poly_const p) tt ff) ff)
- (holds cln)))))
-
-(declare lra_contra_>
- (! p poly
- (! f (th_holds (>0_poly p))
- (! i2 (^ (mpq_ifpos (is_poly_const p)) ff)
- (holds cln)))))
-
-(declare lra_contra_>=
- (! p poly
- (! f (th_holds (>=0_poly p))
- (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)
- (holds cln)))))
-
-(declare lra_contra_distinct
- (! p poly
- (! f (th_holds (distinct0_poly p))
- (! i2 (^ (mp_ifzero (is_poly_const p) tt ff) tt)
- (holds cln)))))
-
-;; muliplication by a constant
-
-(declare lra_mul_c_=
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (=0_poly p))
- (! i (^ (poly_mul_c p c) p')
- (th_holds (=0_poly p'))))))))
-
-(declare lra_mul_c_>
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (>0_poly p))
- (! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p')
- (th_holds (>0_poly p'))))))));
-
-(declare lra_mul_c_>=
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (>=0_poly p))
- (! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p')
- (th_holds (>=0_poly p'))))))))
-
-(declare lra_mul_c_distinct
- (! p poly
- (! p' poly
- (! c mpq
- (! f (th_holds (distinct0_poly p))
- (! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p')
- (th_holds (distinct0_poly p'))))))))
-
-;; adding equations
-
-(declare lra_add_=_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_poly p1))
- (! f2 (th_holds (=0_poly p2))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (=0_poly p3)))))))))
-
-(declare lra_add_>_>
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>0_poly p1))
- (! f2 (th_holds (>0_poly p2))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_poly p3)))))))))
-
-(declare lra_add_>=_>=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>=0_poly p1))
- (! f2 (th_holds (>=0_poly p2))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>=0_poly p3)))))))))
-
-(declare lra_add_=_>
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_poly p1))
- (! f2 (th_holds (>0_poly p2))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_poly p3)))))))))
-
-(declare lra_add_=_>=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_poly p1))
- (! f2 (th_holds (>=0_poly p2))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>=0_poly p3)))))))))
-
-(declare lra_add_>_>=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>0_poly p1))
- (! f2 (th_holds (>=0_poly p2))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_poly p3)))))))))
-
-(declare lra_add_>=_>
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>=0_poly p1))
- (! f2 (th_holds (>0_poly p2))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (>0_poly p3)))))))))
-
-(declare lra_add_=_distinct
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_poly p1))
- (! f2 (th_holds (distinct0_poly p2))
- (! i (^ (poly_add p1 p2) p3)
- (th_holds (distinct0_poly p3)))))))))
-
-;; substracting equations
-
-(declare lra_sub_=_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (=0_poly p1))
- (! f2 (th_holds (=0_poly p2))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (=0_poly p3)))))))))
-
-(declare lra_sub_>_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>0_poly p1))
- (! f2 (th_holds (=0_poly p2))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (>0_poly p3)))))))))
-
-(declare lra_sub_>=_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (>=0_poly p1))
- (! f2 (th_holds (=0_poly p2))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (>=0_poly p3)))))))))
-
-(declare lra_sub_distinct_=
- (! p1 poly
- (! p2 poly
- (! p3 poly
- (! f1 (th_holds (distinct0_poly p1))
- (! f2 (th_holds (=0_poly p2))
- (! i (^ (poly_sub p1 p2) p3)
- (th_holds (distinct0_poly p3)))))))))
-
- ;; converting between terms and polynomials
-
-(declare poly_norm (! t (term Real) (! p poly type)))
-
-(declare pn_let
- (! t (term Real)
- (! p poly
- (! pn (poly_norm t p)
-
- (! u (! pnt (poly_norm t p)
- (holds cln))
- (holds cln))))))
-
-(declare pn_const
- (! x mpq
- (poly_norm (a_real x) (polyc x lmonn))))
-
-(declare pn_var
- (! v var_real
- (poly_norm (a_var_real v) (polyc 0/1 (lmonc 1/1 v lmonn)))))
-
-
-(declare pn_+
- (! x (term Real)
- (! px poly
- (! y (term Real)
- (! py poly
- (! pz poly
- (! pnx (poly_norm x px)
- (! pny (poly_norm y py)
- (! a (^ (poly_add px py) pz)
- (poly_norm (+_Real x y) pz))))))))))
-
-(declare pn_-
- (! x (term Real)
- (! px poly
- (! y (term Real)
- (! py poly
- (! pz poly
- (! pnx (poly_norm x px)
- (! pny (poly_norm y py)
- (! a (^ (poly_sub px py) pz)
- (poly_norm (-_Real x y) pz))))))))))
-
-(declare pn_mul_c_L
- (! y (term Real)
- (! py poly
- (! pz poly
- (! x mpq
- (! pny (poly_norm y py)
- (! a (^ (poly_mul_c py x) pz)
- (poly_norm (*_Real (a_real x) y) pz))))))))
-
-(declare pn_mul_c_R
- (! y (term Real)
- (! py poly
- (! pz poly
- (! x mpq
- (! pny (poly_norm y py)
- (! a (^ (poly_mul_c py x) pz)
- (poly_norm (*_Real y (a_real x)) pz))))))))
-
-(declare poly_flip_not_>=
- (! p poly
- (! p_negged poly
- (! pf_formula (th_holds (not (>=0_poly p)))
- (! sc (^ (poly_neg p) p_negged)
- (th_holds (>0_poly p_negged)))))))
-
-
-;; for polynomializing other terms, in particular ite's
-
-(declare term_atom (! v var_real (! t (term Real) type)))
-
-(declare decl_term_atom
- (! t (term Real)
- (! u (! v var_real
- (! a (term_atom v t)
- (holds cln)))
- (holds cln))))
-
-(declare pn_var_atom
- (! v var_real
- (! t (term Real)
- (! a (term_atom v t)
- (poly_norm t (polyc 0/1 (lmonc 1/1 v lmonn)))))))
-
-
-;; conversion between term formulas and polynomial formulas
-
-(declare poly_formula_norm (! ft formula (! fp formula type)))
-
-; convert between term formulas and polynomial formulas
-
-(declare poly_form
- (! ft formula
- (! fp formula
- (! p (poly_formula_norm ft fp)
- (! u (th_holds ft)
- (th_holds fp))))))
-
-(declare poly_form_not
- (! ft formula
- (! fp formula
- (! p (poly_formula_norm ft fp)
- (! u (th_holds (not ft))
- (th_holds (not fp)))))))
-
-(declare poly_formula_norm_>=
- (! x (term Real)
- (! y (term Real)
- (! p poly
- (! n (poly_norm (-_Real y x) p)
- (poly_formula_norm (>=_Real y x) (>=0_poly p)))))))
-
+++ /dev/null
-; Depends On: th_lra.plf
-;; Proof (from predicates on linear polynomials) that the following imply bottom
-;
-; -x - 1/2 y + 2 >= 0
-; x + y - 8 >= 0
-; x - y + 0 >= 0
-;
-(check
- ; Variables
- (% x var_real
- (% y var_real
- ; linear monomials (combinations)
- (@ m1 (lmonc (~ 1/1) x (lmonc (~ 1/2) y lmonn))
- (@ m2 (lmonc 1/1 x (lmonc 1/1 y lmonn))
- (@ m3 (lmonc 1/1 x (lmonc (~ 1/1) y lmonn))
- ; linear polynomials (affine)
- (@ p1 (polyc 2/1 m1)
- (@ p2 (polyc (~ 8/1) m2)
- (@ p3 (polyc 0/1 m3)
- (% pf_nonneg_1 (th_holds (>=0_poly p1))
- (% pf_nonneg_2 (th_holds (>=0_poly p2))
- (% pf_nonneg_3 (th_holds (>=0_poly p3))
- (:
- (holds cln)
- (lra_contra_>=
- _
- (lra_add_>=_>= _ _ _
- (lra_mul_c_>= _ _ 4/1 pf_nonneg_1)
- (lra_add_>=_>= _ _ _
- (lra_mul_c_>= _ _ 3/1 pf_nonneg_2)
- (lra_add_>=_>= _ _ _
- (lra_mul_c_>= _ _ 1/1 pf_nonneg_3)
- (lra_axiom_>= 0/1))))))
- )))))
- ))))
- ))
-)
-
-;; Proof (from predicates on real terms) that the following imply bottom
-;
-; -x - 1/2 y >= 2
-; x + y >= 8
-; x - y >= 0
-;
-(check
- ; Declarations
- ; Variables
- (% x var_real
- (% y var_real
- ; real predicates
- (@ f1 (>=_Real (+_Real (*_Real (a_real (~ 1/1)) (a_var_real x)) (*_Real (a_real (~ 1/2)) (a_var_real y))) (a_real (~ 2/1)))
- (@ f2 (>=_Real (+_Real (*_Real (a_real 1/1) (a_var_real x)) (*_Real (a_real 1/1) (a_var_real y))) (a_real 8/1))
- (@ f3 (>=_Real (+_Real (*_Real (a_real 1/1) (a_var_real x)) (*_Real (a_real (~ 1/1)) (a_var_real y))) (a_real 0/1))
- ; proof of real predicates
- (% pf_f1 (th_holds f1)
- (% pf_f2 (th_holds f2)
- (% pf_f3 (th_holds f3)
-
-
- ; Normalization
- ; real term -> linear polynomial normalization witnesses
- (@ n1 (poly_formula_norm_>= _ _ _
- (pn_- _ _ _ _ _
- (pn_+ _ _ _ _ _
- (pn_mul_c_L _ _ _ (~ 1/1) (pn_var x))
- (pn_mul_c_L _ _ _ (~ 1/2) (pn_var y)))
- (pn_const (~ 2/1))))
- (@ n2 (poly_formula_norm_>= _ _ _
- (pn_- _ _ _ _ _
- (pn_+ _ _ _ _ _
- (pn_mul_c_L _ _ _ 1/1 (pn_var x))
- (pn_mul_c_L _ _ _ 1/1 (pn_var y)))
- (pn_const 8/1)))
- (@ n3 (poly_formula_norm_>= _ _ _
- (pn_- _ _ _ _ _
- (pn_+ _ _ _ _ _
- (pn_mul_c_L _ _ _ 1/1 (pn_var x))
- (pn_mul_c_L _ _ _ (~ 1/1) (pn_var y)))
- (pn_const 0/1)))
- ; proof of linear polynomial predicates
- (@ pf_n1 (poly_form _ _ n1 pf_f1)
- (@ pf_n2 (poly_form _ _ n2 pf_f2)
- (@ pf_n3 (poly_form _ _ n3 pf_f3)
-
- ; derivation of a contradiction using farkas coefficients
- (:
- (holds cln)
- (lra_contra_>= _
- (lra_add_>=_>= _ _ _
- (lra_mul_c_>= _ _ 4/1 pf_n1)
- (lra_add_>=_>= _ _ _
- (lra_mul_c_>= _ _ 3/1 pf_n2)
- (lra_add_>=_>= _ _ _
- (lra_mul_c_>= _ _ 1/1 pf_n3)
- (lra_axiom_>= 0/1))))))
- )))
- )))
- )))
- )))
- ))
-)
-
-;; Term proof, 2 (>=), one (not >=)
-;; Proof (from predicates on real terms) that the following imply bottom
-;
-; -x + y >= 2
-; x + y >= 2
-; not[ y >= -2] => [y < -2] => [-y > 2]
-;
-(check
- ; Declarations
- ; Variables
- (% x var_real
- (% y var_real
- ; real predicates
- (@ f1 (>=_Real
- (+_Real (*_Real (a_real (~ 1/1)) (a_var_real x)) (a_var_real y))
- (a_real 2/1))
- (@ f2 (>=_Real
- (+_Real (a_var_real x) (a_var_real y))
- (a_real 2/1))
- (@ f3 (not (>=_Real (a_var_real y) (a_real (~ 2/1))))
-
- ; Normalization
- ; proof of real predicates
- (% pf_f1 (th_holds f1)
- (% pf_f2 (th_holds f2)
- (% pf_f3 (th_holds f3)
- ; real term -> linear polynomial normalization witnesses
- (@ n1 (poly_formula_norm_>= _ _ _
- (pn_- _ _ _ _ _
- (pn_+ _ _ _ _ _
- (pn_mul_c_L _ _ _ (~ 1/1) (pn_var x))
- (pn_var y))
- (pn_const 2/1)))
- (@ n2 (poly_formula_norm_>= _ _ _
- (pn_- _ _ _ _ _
- (pn_+ _ _ _ _ _
- (pn_var x)
- (pn_var y))
- (pn_const 2/1)))
- (@ n3 (poly_formula_norm_>= _ _ _
- (pn_- _ _ _ _ _
- (pn_var y)
- (pn_const (~ 2/1))))
- ; proof of linear polynomial predicates
- (@ pf_n1 (poly_form _ _ n1 pf_f1)
- (@ pf_n2 (poly_form _ _ n2 pf_f2)
- (@ pf_n3 (poly_flip_not_>= _ _ (poly_form_not _ _ n3 pf_f3))
-
- ; derivation of a contradiction using farkas coefficients
- (:
- (holds cln)
- (lra_contra_> _
- (lra_add_>=_> _ _ _
- (lra_mul_c_>= _ _ 1/1 pf_n1)
- (lra_add_>=_> _ _ _
- (lra_mul_c_>= _ _ 1/1 pf_n2)
- (lra_add_>_>= _ _ _
- (lra_mul_c_> _ _ 2/1 pf_n3)
- (lra_axiom_>= 0/1))))))
- )))
- )))
- )))
- )))
- ))
-)
projects / cvc5.git / commitdiff