From 4f8965352cacbc0cca9c88d71c1a69b7055822ef Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 4 Jan 2017 12:57:55 -0800 Subject: [PATCH] Reverting two files encoding with DOS linebreaks back into using unix linebreaks. --- proofs/signatures/th_lra.plf | 900 +++++++++--------- .../regress0/quantifiers/pure_dt_cbqi.smt2 | 12 +- 2 files changed, 455 insertions(+), 457 deletions(-) diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf index 88118e8d1..d67fdc84f 100644 --- a/proofs/signatures/th_lra.plf +++ b/proofs/signatures/th_lra.plf @@ -1,451 +1,449 @@ -; 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)))))))) - - +; 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)))))))) diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 index a11d14e4a..5c11a57f5 100644 --- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 +++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 @@ -1,6 +1,6 @@ -(set-logic ALL_SUPPORTED) -(set-info :status sat) -(declare-datatypes () ((nat (Suc (pred nat)) (zero)))) -(declare-fun y () nat) -(assert (forall ((x nat)) (not (= y (Suc x))))) -(check-sat) +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((nat (Suc (pred nat)) (zero)))) +(declare-fun y () nat) +(assert (forall ((x nat)) (not (= y (Suc x))))) +(check-sat) -- 2.30.2