-; 59 loc in side conditions\r
-\r
-(program mpq_ifpos ((x mpq)) bool\r
- (mp_ifneg x ff (mp_ifzero x ff tt)))\r
-\r
-; a real variable\r
-(declare var_real type)\r
-; a real variable term\r
-(declare a_var_real (! v var_real (term Real)))\r
-\r
-;; linear polynomials in the form a_1*x_1 + a_2*x_2 .... + a_n*x_n\r
-\r
-(declare lmon type)\r
-(declare lmonn lmon)\r
-(declare lmonc (! c mpq (! v var_real (! l lmon lmon))))\r
-\r
-(program lmon_neg ((l lmon)) lmon \r
- (match l\r
- (lmonn l)\r
- ((lmonc c' v' l') (lmonc (mp_neg c') v' (lmon_neg l')))))\r
-\r
-(program lmon_add ((l1 lmon) (l2 lmon)) lmon\r
- (match l1\r
- (lmonn l2)\r
- ((lmonc c' v' l') \r
- (match l2\r
- (lmonn l1)\r
- ((lmonc c'' v'' l'')\r
- (compare v' v'' \r
- (lmonc c' v' (lmon_add l' l2))\r
- (lmonc c'' v'' (lmon_add l1 l''))))))))\r
-\r
-(program lmon_mul_c ((l lmon) (c mpq)) lmon\r
- (match l\r
- (lmonn l)\r
- ((lmonc c' v' l') (lmonc (mp_mul c c') v' (lmon_mul_c l' c)))))\r
-\r
-;; linear polynomials in the form (a_1*x_1 + a_2*x_2 .... + a_n*x_n) + c \r
-\r
-(declare poly type)\r
-(declare polyc (! c mpq (! l lmon poly)))\r
-\r
-(program poly_neg ((p poly)) poly\r
- (match p\r
- ((polyc m' p') (polyc (mp_neg m') (lmon_neg p')))))\r
-\r
-(program poly_add ((p1 poly) (p2 poly)) poly\r
- (match p1\r
- ((polyc c1 l1)\r
- (match p2\r
- ((polyc c2 l2) (polyc (mp_add c1 c2) (lmon_add l1 l2)))))))\r
-\r
-(program poly_sub ((p1 poly) (p2 poly)) poly\r
- (poly_add p1 (poly_neg p2)))\r
- \r
-(program poly_mul_c ((p poly) (c mpq)) poly\r
- (match p\r
- ((polyc c' l') (polyc (mp_mul c' c) (lmon_mul_c l' c)))))\r
- \r
-;; code to isolate a variable from a term\r
-;; if (isolate v l) returns (c,l'), this means l = c*v + l', where v is not in FV(t').\r
-\r
-(declare isol type)\r
-(declare isolc (! r mpq (! l lmon isol)))\r
-\r
-(program isolate_h ((v var_real) (l lmon) (e bool)) isol\r
- (match l\r
- (lmonn (isolc 0/1 l))\r
- ((lmonc c' v' l') \r
- (ifmarked v'\r
- (match (isolate_h v l' tt) \r
- ((isolc ci li) (isolc (mp_add c' ci) li)))\r
- (match e \r
- (tt (isolc 0/1 l))\r
- (ff (match (isolate_h v l' ff) \r
- ((isolc ci li) (isolc ci (lmonc c' v' li))))))))))\r
-\r
-(program isolate ((v var_real) (l lmon)) isol\r
- (do (markvar v)\r
- (let i (isolate_h v l ff)\r
- (do (markvar v) i))))\r
-\r
-;; determine if a monomial list is constant\r
-\r
-(program is_lmon_zero ((l lmon)) bool\r
- (match l\r
- (lmonn tt)\r
- ((lmonc c v l')\r
- (match (isolate v l)\r
- ((isolc ci li) \r
- (mp_ifzero ci (is_lmon_zero li) ff))))))\r
- \r
-;; return the constant that p is equal to. If p is not constant, fail.\r
- \r
-(program is_poly_const ((p poly)) mpq\r
- (match p\r
- ((polyc c' l')\r
- (match (is_lmon_zero l')\r
- (tt c')\r
- (ff (fail mpq))))))\r
-\r
-;; conversion to use polynomials in term formulas\r
-\r
-(declare poly_term (! p poly (term Real)))\r
- \r
-;; create new equality out of inequality\r
-\r
-(declare lra_>=_>=_to_=\r
- (! p1 poly\r
- (! p2 poly\r
- (! f1 (th_holds (>=0_Real (poly_term p1)))\r
- (! f2 (th_holds (>=0_Real (poly_term p2)))\r
- (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)\r
- (th_holds (=0_Real (poly_term p2))))))))))\r
- \r
-;; axioms\r
-\r
-(declare lra_axiom_=\r
- (th_holds (=0_Real (poly_term (polyc 0/1 lmonn)))))\r
- \r
-(declare lra_axiom_>\r
- (! c mpq \r
- (! i (^ (mpq_ifpos c) tt)\r
- (th_holds (>0_Real (poly_term (polyc c lmonn)))))))\r
- \r
-(declare lra_axiom_>=\r
- (! c mpq \r
- (! i (^ (mp_ifneg c tt ff) ff)\r
- (th_holds (>=0_Real (poly_term (polyc c lmonn)))))))\r
- \r
-(declare lra_axiom_distinct\r
- (! c mpq \r
- (! i (^ (mp_ifzero c tt ff) ff)\r
- (th_holds (distinct0_Real (poly_term (polyc c lmonn)))))))\r
-\r
-;; contradiction rules\r
-\r
-(declare lra_contra_=\r
- (! p poly\r
- (! f (th_holds (=0_Real (poly_term p)))\r
- (! i (^ (mp_ifzero (is_poly_const p) tt ff) ff)\r
- (holds cln)))))\r
- \r
-(declare lra_contra_>\r
- (! p poly\r
- (! f (th_holds (>0_Real (poly_term p)))\r
- (! i2 (^ (mpq_ifpos (is_poly_const p)) ff)\r
- (holds cln)))))\r
- \r
-(declare lra_contra_>=\r
- (! p poly\r
- (! f (th_holds (>=0_Real (poly_term p)))\r
- (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)\r
- (holds cln)))))\r
- \r
-(declare lra_contra_distinct\r
- (! p poly\r
- (! f (th_holds (distinct0_Real (poly_term p)))\r
- (! i2 (^ (mp_ifzero (is_poly_const p) tt ff) tt)\r
- (holds cln)))))\r
-\r
-;; muliplication by a constant\r
-\r
-(declare lra_mul_c_=\r
- (! p poly\r
- (! p' poly\r
- (! c mpq\r
- (! f (th_holds (=0_Real (poly_term p)))\r
- (! i (^ (poly_mul_c p c) p')\r
- (th_holds (=0_Real (poly_term p')))))))))\r
-\r
-(declare lra_mul_c_>\r
- (! p poly\r
- (! p' poly\r
- (! c mpq\r
- (! f (th_holds (>0_Real (poly_term p)))\r
- (! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p')\r
- (th_holds (>0_Real (poly_term p')))))))));)\r
- \r
-(declare lra_mul_c_>=\r
- (! p poly\r
- (! p' poly\r
- (! c mpq\r
- (! f (th_holds (>=0_Real (poly_term p)))\r
- (! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p')\r
- (th_holds (>=0_Real (poly_term p')))))))));)\r
- \r
-(declare lra_mul_c_distinct\r
- (! p poly\r
- (! p' poly\r
- (! c mpq\r
- (! f (th_holds (distinct0_Real (poly_term p)))\r
- (! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p')\r
- (th_holds (distinct0_Real (poly_term p')))))))));)\r
-\r
-;; adding equations\r
-\r
-(declare lra_add_=_=\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (=0_Real (poly_term p1)))\r
- (! f2 (th_holds (=0_Real (poly_term p2)))\r
- (! i (^ (poly_add p1 p2) p3)\r
- (th_holds (=0_Real (poly_term p3)))))))))))\r
- \r
-(declare lra_add_>_>\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (>0_Real (poly_term p1)))\r
- (! f2 (th_holds (>0_Real (poly_term p2)))\r
- (! i (^ (poly_add p1 p2) p3)\r
- (th_holds (>0_Real (poly_term p3))))))))))\r
- \r
-(declare lra_add_>=_>=\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (>=0_Real (poly_term p1)))\r
- (! f2 (th_holds (>=0_Real (poly_term p2)))\r
- (! i (^ (poly_add p1 p2) p3)\r
- (th_holds (>=0_Real (poly_term p3))))))))))\r
-\r
-(declare lra_add_=_>\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (=0_Real (poly_term p1)))\r
- (! f2 (th_holds (>0_Real (poly_term p2)))\r
- (! i (^ (poly_add p1 p2) p3)\r
- (th_holds (>0_Real (poly_term p3))))))))))\r
- \r
-(declare lra_add_=_>=\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (=0_Real (poly_term p1)))\r
- (! f2 (th_holds (>=0_Real (poly_term p2)))\r
- (! i (^ (poly_add p1 p2) p3)\r
- (th_holds (>=0_Real (poly_term p3))))))))))\r
-\r
-(declare lra_add_>_>=\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (>0_Real (poly_term p1)))\r
- (! f2 (th_holds (>=0_Real (poly_term p2)))\r
- (! i (^ (poly_add p1 p2) p3)\r
- (th_holds (>0_Real (poly_term p3))))))))))\r
- \r
-(declare lra_add_=_distinct\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (=0_Real (poly_term p1)))\r
- (! f2 (th_holds (distinct0_Real (poly_term p2)))\r
- (! i (^ (poly_add p1 p2) p3)\r
- (th_holds (distinct0_Real (poly_term p3)))))))))))\r
- \r
-;; substracting equations\r
-\r
-(declare lra_sub_=_=\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (=0_Real (poly_term p1)))\r
- (! f2 (th_holds (=0_Real (poly_term p2)))\r
- (! i (^ (poly_sub p1 p2) p3)\r
- (th_holds (=0_Real (poly_term p3)))))))))))\r
- \r
-(declare lra_sub_>_=\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (>0_Real (poly_term p1)))\r
- (! f2 (th_holds (=0_Real (poly_term p2)))\r
- (! i (^ (poly_sub p1 p2) p3)\r
- (th_holds (>0_Real (poly_term p3))))))))))\r
- \r
-(declare lra_sub_>=_=\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (>=0_Real (poly_term p1)))\r
- (! f2 (th_holds (=0_Real (poly_term p2)))\r
- (! i (^ (poly_sub p1 p2) p3)\r
- (th_holds (>=0_Real (poly_term p3))))))))))\r
- \r
-(declare lra_sub_distinct_=\r
- (! p1 poly\r
- (! p2 poly\r
- (! p3 poly\r
- (! f1 (th_holds (distinct0_Real (poly_term p1)))\r
- (! f2 (th_holds (=0_Real (poly_term p2)))\r
- (! i (^ (poly_sub p1 p2) p3)\r
- (th_holds (distinct0_Real (poly_term p3)))))))))))\r
-\r
- ;; converting between terms and polynomials\r
-\r
-(declare poly_norm (! t (term Real) (! p poly type))) \r
-\r
-(declare pn_let \r
- (! t (term Real)\r
- (! p poly\r
- (! pn (poly_norm t p)\r
-\r
- (! u (! pnt (poly_norm t p)\r
- (holds cln))\r
- (holds cln))))))\r
-\r
-(declare pn_const\r
- (! x mpq\r
- (poly_norm (a_real x) (polyc x lmonn))))\r
- \r
-(declare pn_var\r
- (! v var_real\r
- (poly_norm (a_var_real v) (polyc 0/1 (lmonc 1/1 v lmonn)))))\r
-\r
-\r
-(declare pn_+\r
- (! x (term Real)\r
- (! px poly\r
- (! y (term Real)\r
- (! py poly\r
- (! pz poly\r
- (! pnx (poly_norm x px)\r
- (! pny (poly_norm y py)\r
- (! a (^ (poly_add px py) pz)\r
- (poly_norm (+_Real x y) pz))))))))))\r
- \r
-(declare pn_-\r
- (! x (term Real)\r
- (! px poly\r
- (! y (term Real)\r
- (! py poly\r
- (! pz poly\r
- (! pnx (poly_norm x px)\r
- (! pny (poly_norm y py)\r
- (! a (^ (poly_sub px py) pz)\r
- (poly_norm (-_Real x y) pz))))))))))\r
- \r
-(declare pn_mul_c_L\r
- (! y (term Real)\r
- (! py poly\r
- (! pz poly\r
- (! x mpq\r
- (! pny (poly_norm y py)\r
- (! a (^ (poly_mul_c py x) pz)\r
- (poly_norm (*_Real (a_real x) y) pz))))))))\r
- \r
-(declare pn_mul_c_R\r
- (! y (term Real)\r
- (! py poly\r
- (! pz poly\r
- (! x mpq\r
- (! pny (poly_norm y py)\r
- (! a (^ (poly_mul_c py x) pz)\r
- (poly_norm (*_Real y (a_real x)) pz))))))))\r
-\r
-;; for polynomializing other terms, in particular ite's\r
-\r
-(declare term_atom (! v var_real (! t (term Real) type)))\r
-\r
-(declare decl_term_atom\r
- (! t (term Real)\r
- (! u (! v var_real\r
- (! a (term_atom v t)\r
- (holds cln)))\r
- (holds cln))))\r
- \r
-(declare pn_var_atom\r
- (! v var_real\r
- (! t (term Real)\r
- (! a (term_atom v t)\r
- (poly_norm t (polyc 0/1 (lmonc 1/1 v lmonn)))))))\r
-\r
-\r
-;; conversion between term formulas and polynomial formulas\r
-\r
-(declare poly_formula_norm (! ft formula (! fp formula type))) \r
-\r
-; convert between term formulas and polynomial formulas\r
-\r
-(declare poly_form\r
- (! ft formula\r
- (! fp formula\r
- (! p (poly_formula_norm ft fp)\r
- (! u (th_holds ft)\r
- (th_holds fp))))))\r
- \r
-(declare poly_form_not\r
- (! ft formula\r
- (! fp formula\r
- (! p (poly_formula_norm ft fp)\r
- (! u (th_holds (not ft))\r
- (th_holds (not fp)))))))\r
- \r
-; form equivalence between term formula and polynomial formula \r
- \r
-(declare poly_norm_=\r
- (! x (term Real)\r
- (! y (term Real)\r
- (! p poly\r
- (! h (th_holds (= Real x y))\r
- (! n (poly_norm (-_Real x y) p)\r
- (! u (! pn (th_holds (=0_Real (poly_term p)))\r
- (holds cln))\r
- (holds cln))))))))\r
- \r
-(declare poly_norm_>\r
- (! x (term Real)\r
- (! y (term Real)\r
- (! p poly\r
- (! h (th_holds (>_Real x y))\r
- (! n (poly_norm (-_Real x y) p)\r
- (! u (! pn (th_holds (>0_Real (poly_term p)))\r
- (holds cln))\r
- (holds cln))))))))\r
- \r
-(declare poly_norm_<\r
- (! x (term Real)\r
- (! y (term Real)\r
- (! p poly\r
- (! h (th_holds (<_Real x y))\r
- (! n (poly_norm (-_Real y x) p)\r
- (! u (! pn (th_holds (>0_Real (poly_term p)))\r
- (holds cln))\r
- (holds cln))))))))\r
- \r
-(declare poly_norm_>=\r
- (! x (term Real)\r
- (! y (term Real)\r
- (! p poly\r
- (! h (th_holds (>=_Real x y))\r
- (! n (poly_norm (-_Real x y) p)\r
- (! u (! pn (th_holds (>=0_Real (poly_term p)))\r
- (holds cln))\r
- (holds cln))))))))\r
- \r
-(declare poly_norm_<=\r
- (! x (term Real)\r
- (! y (term Real)\r
- (! p poly\r
- (! h (th_holds (<=_Real x y))\r
- (! n (poly_norm (-_Real y x) p)\r
- (! u (! pn (th_holds (>=0_Real (poly_term p)))\r
- (holds cln))\r
- (holds cln))))))))\r
- \r
- \r
+; 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)
+ (holds cln)))))
+
+(declare lra_contra_>
+ (! p poly
+ (! f (th_holds (>0_Real (poly_term p)))
+ (! i2 (^ (mpq_ifpos (is_poly_const p)) ff)
+ (holds cln)))))
+
+(declare lra_contra_>=
+ (! p poly
+ (! f (th_holds (>=0_Real (poly_term p)))
+ (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)
+ (holds cln)))))
+
+(declare lra_contra_distinct
+ (! p poly
+ (! f (th_holds (distinct0_Real (poly_term 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_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)
+ (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))))))))
+
+;; 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)))))))
+
+; form equivalence between term formula and polynomial formula
+
+(declare poly_norm_=
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (= Real x y))
+ (! n (poly_norm (-_Real x y) p)
+ (! u (! pn (th_holds (=0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
+
+(declare poly_norm_>
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (>_Real x y))
+ (! n (poly_norm (-_Real x y) p)
+ (! u (! pn (th_holds (>0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
+
+(declare poly_norm_<
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (<_Real x y))
+ (! n (poly_norm (-_Real y x) p)
+ (! u (! pn (th_holds (>0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
+
+(declare poly_norm_>=
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (>=_Real x y))
+ (! n (poly_norm (-_Real x y) p)
+ (! u (! pn (th_holds (>=0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
+
+(declare poly_norm_<=
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (<=_Real x y))
+ (! n (poly_norm (-_Real y x) p)
+ (! u (! pn (th_holds (>=0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
projects / cvc5.git / commitdiff