; 59 loc in side conditions
(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 poly_term (! p poly (term Real)))
;; create new equality out of inequality
(declare lra_>=_>=_to_=
(! p1 poly
(! p2 poly
(! f1 (th_holds (>=0_Real (poly_term p1)))
(! f2 (th_holds (>=0_Real (poly_term p2)))
(! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
(th_holds (=0_Real (poly_term p2))))))))))
;; axioms
(declare lra_axiom_=
(th_holds (=0_Real (poly_term (polyc 0/1 lmonn)))))
(declare lra_axiom_>
(! c mpq
(! i (^ (mpq_ifpos c) tt)
(th_holds (>0_Real (poly_term (polyc c lmonn)))))))
(declare lra_axiom_>=
(! c mpq
(! i (^ (mp_ifneg c tt ff) ff)
(th_holds (>=0_Real (poly_term (polyc c lmonn)))))))
(declare lra_axiom_distinct
(! c mpq
(! i (^ (mp_ifzero c tt ff) ff)
(th_holds (distinct0_Real (poly_term (polyc c lmonn)))))))
;; contradiction rules
(declare lra_contra_=
(! p poly
(! f (th_holds (=0_Real (poly_term p)))
(! i (^ (mp_ifzero (is_poly_const p) tt ff) ff)
bottom))))
(declare lra_contra_>
(! p poly
(! f (th_holds (>0_Real (poly_term p)))
(! i2 (^ (mpq_ifpos (is_poly_const p)) ff)
bottom))))
(declare lra_contra_>=
(! p poly
(! f (th_holds (>=0_Real (poly_term p)))
(! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)
bottom))))
(declare lra_contra_distinct
(! p poly
(! f (th_holds (distinct0_Real (poly_term p)))
(! i2 (^ (mp_ifzero (is_poly_const p) tt ff) tt)
bottom))))
;; muliplication by a constant
(declare lra_mul_c_=
(! p poly
(! p' poly
(! c mpq
(! f (th_holds (=0_Real (poly_term p)))
(! i (^ (poly_mul_c p c) p')
(th_holds (=0_Real (poly_term p')))))))))
(declare lra_mul_c_>
(! p poly
(! p' poly
(! c mpq
(! f (th_holds (>0_Real (poly_term p)))
(! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p')
(th_holds (>0_Real (poly_term p')))))))));)
(declare lra_mul_c_>=
(! p poly
(! p' poly
(! c mpq
(! f (th_holds (>=0_Real (poly_term p)))
(! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p')
(th_holds (>=0_Real (poly_term p')))))))));)
(declare lra_mul_c_distinct
(! p poly
(! p' poly
(! c mpq
(! f (th_holds (distinct0_Real (poly_term p)))
(! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p')
(th_holds (distinct0_Real (poly_term p')))))))));)
;; adding equations
(declare lra_add_=_=
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (=0_Real (poly_term p1)))
(! f2 (th_holds (=0_Real (poly_term p2)))
(! i (^ (poly_add p1 p2) p3)
(th_holds (=0_Real (poly_term p3)))))))))))
(declare lra_add_>_>
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (>0_Real (poly_term p1)))
(! f2 (th_holds (>0_Real (poly_term p2)))
(! i (^ (poly_add p1 p2) p3)
(th_holds (>0_Real (poly_term p3))))))))))
(declare lra_add_>=_>=
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (>=0_Real (poly_term p1)))
(! f2 (th_holds (>=0_Real (poly_term p2)))
(! i (^ (poly_add p1 p2) p3)
(th_holds (>=0_Real (poly_term p3))))))))))
(declare lra_add_=_>
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (=0_Real (poly_term p1)))
(! f2 (th_holds (>0_Real (poly_term p2)))
(! i (^ (poly_add p1 p2) p3)
(th_holds (>0_Real (poly_term p3))))))))))
(declare lra_add_=_>=
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (=0_Real (poly_term p1)))
(! f2 (th_holds (>=0_Real (poly_term p2)))
(! i (^ (poly_add p1 p2) p3)
(th_holds (>=0_Real (poly_term p3))))))))))
(declare lra_add_>_>=
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (>0_Real (poly_term p1)))
(! f2 (th_holds (>=0_Real (poly_term p2)))
(! i (^ (poly_add p1 p2) p3)
(th_holds (>0_Real (poly_term p3))))))))))
(declare lra_add_=_distinct
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (=0_Real (poly_term p1)))
(! f2 (th_holds (distinct0_Real (poly_term p2)))
(! i (^ (poly_add p1 p2) p3)
(th_holds (distinct0_Real (poly_term p3)))))))))))
;; substracting equations
(declare lra_sub_=_=
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (=0_Real (poly_term p1)))
(! f2 (th_holds (=0_Real (poly_term p2)))
(! i (^ (poly_sub p1 p2) p3)
(th_holds (=0_Real (poly_term p3)))))))))))
(declare lra_sub_>_=
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (>0_Real (poly_term p1)))
(! f2 (th_holds (=0_Real (poly_term p2)))
(! i (^ (poly_sub p1 p2) p3)
(th_holds (>0_Real (poly_term p3))))))))))
(declare lra_sub_>=_=
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (>=0_Real (poly_term p1)))
(! f2 (th_holds (=0_Real (poly_term p2)))
(! i (^ (poly_sub p1 p2) p3)
(th_holds (>=0_Real (poly_term p3))))))))))
(declare lra_sub_distinct_=
(! p1 poly
(! p2 poly
(! p3 poly
(! f1 (th_holds (distinct0_Real (poly_term p1)))
(! f2 (th_holds (=0_Real (poly_term p2)))
(! i (^ (poly_sub p1 p2) p3)
(th_holds (distinct0_Real (poly_term 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)
bottom)
bottom)))))
(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))))))))
;; 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)
bottom))
bottom)))
(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)))))))
; form equivalence between term formula and polynomial formula
(declare poly_norm_=
(! x (term Real)
(! y (term Real)
(! p poly
(! n (poly_norm (-_Real x y) p)
(! u (! pn (poly_formula_norm (= Real x y) (=0_Real (poly_term p)))
bottom)
bottom))))))
(declare poly_norm_>
(! x (term Real)
(! y (term Real)
(! p poly
(! n (poly_norm (-_Real x y) p)
(! u (! pn (poly_formula_norm (>_Real x y) (>0_Real (poly_term p)))
bottom)
bottom))))))
(declare poly_norm_<
(! x (term Real)
(! y (term Real)
(! p poly
(! n (poly_norm (-_Real y x) p)
(! u (! pn (poly_formula_norm (<_Real x y) (>0_Real (poly_term p)))
bottom)
bottom))))))
(declare poly_norm_>=
(! x (term Real)
(! y (term Real)
(! p poly
(! n (poly_norm (-_Real x y) p)
(! u (! pn (poly_formula_norm (>=_Real x y) (>=0_Real (poly_term p)))
bottom)
bottom))))))
(declare poly_norm_<=
(! x (term Real)
(! y (term Real)
(! p poly
(! n (poly_norm (-_Real y x) p)
(! u (! pn (poly_formula_norm (<=_Real x y) (>=0_Real (poly_term p)))
bottom)
bottom))))))
(declare poly_norm_distinct
(! x (term Real)
(! y (term Real)
(! p poly
(! n (poly_norm (-_Real y x) p) ; note the sign change
(! u (! pn (poly_formula_norm (distinct Real x y) (distinct0_Real (poly_term p)))
bottom)
bottom))))))
;; negated polynomial formula conversion
(declare lra_not_=_to_distinct
(! p poly
(! p' poly
(! f (th_holds (not (=0_Real (poly_term p))))
(! u (^ (poly_neg p) p')
(th_holds (distinct0_Real (poly_term p'))))))))
(declare lra_not_>_to_>=
(! p poly
(! p' poly
(! f (th_holds (not (>0_Real (poly_term p))))
(! u (^ (poly_neg p) p')
(th_holds (>=0_Real (poly_term p'))))))))
(declare lra_not_>=_to_>
(! p poly
(! p' poly
(! f (th_holds (not (>=0_Real (poly_term p))))
(! u (^ (poly_neg p) p')
(th_holds (>0_Real (poly_term p'))))))))
(declare lra_not_distinct_to_=
(! p poly
(! p' poly
(! f (th_holds (not (distinct0_Real (poly_term p))))
(! u (^ (poly_neg p) p')
(th_holds (=0_Real (poly_term p'))))))))