From: Tim King <taking@google.com>
Date: Wed, 4 Jan 2017 20:57:55 +0000 (-0800)
Subject: Reverting two files encoding with DOS linebreaks back into using unix linebreaks.
X-Git-Tag: cvc5-1.0.0~5928
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f8965352cacbc0cca9c88d71c1a69b7055822ef;p=cvc5.git

Reverting two files encoding with DOS linebreaks back into using unix linebreaks.
---

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)