diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-27 09:57:52 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-27 09:57:52 -0600 |
| commit | 10d0e5a5d4d59d3dc6d85330374ac3787c6ed8b4 (patch) | |
| tree | 1870aa917134196557f43cdc03d8dd36b667a2e3 | |
| parent | cb7dd2ebdd96e6791cb60e7d995244511f56819f (diff) | |
| parent | 72f1d72852213f46d77c85216c9250bb0f0e3eae (diff) | |
Merge branch 'master' into fixStrLitParserfixStrLitParser
| -rw-r--r-- | proofs/signatures/th_lra.plf | 9 | ||||
| -rw-r--r-- | proofs/signatures/th_lra_test.plf | 32 | ||||
| -rw-r--r-- | proofs/signatures/th_real.plf | 6 |
3 files changed, 42 insertions, 5 deletions
diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf index d67fdc84f..67b17c9af 100644 --- a/proofs/signatures/th_lra.plf +++ b/proofs/signatures/th_lra.plf @@ -1,5 +1,4 @@ -; 59 loc in side conditions - +; Depends on th_real.plf, th_smt.plf (program mpq_ifpos ((x mpq)) bool (mp_ifneg x ff (mp_ifzero x ff tt))) @@ -111,7 +110,7 @@ (! 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)))))))))) + (th_holds (=0_Real (poly_term p2))))))))) ;; axioms @@ -202,7 +201,7 @@ (! 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))))))))))) + (th_holds (=0_Real (poly_term p3)))))))))) (declare lra_add_>_> (! p1 poly @@ -256,7 +255,7 @@ (! 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))))))))))) + (th_holds (distinct0_Real (poly_term p3)))))))))) ;; substracting equations diff --git a/proofs/signatures/th_lra_test.plf b/proofs/signatures/th_lra_test.plf new file mode 100644 index 000000000..687ff988b --- /dev/null +++ b/proofs/signatures/th_lra_test.plf @@ -0,0 +1,32 @@ +; Depends On: th_lra.plf +(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_Real (poly_term p1))) + (% pf_nonneg_2 (th_holds (>=0_Real (poly_term p2))) + (% pf_nonneg_3 (th_holds (>=0_Real (poly_term p3))) + (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))))) + ))))) + )))) + )) +) + + + diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf index 3478e23ef..3529779f3 100644 --- a/proofs/signatures/th_real.plf +++ b/proofs/signatures/th_real.plf @@ -1,3 +1,4 @@ +; Depends On: th_smt.plf (declare Real sort) (define arithpred_Real (! x (term Real) @@ -21,5 +22,10 @@ ; a constant term (declare a_real (! x mpq (term Real))) +(declare >=0_Real (! x (term Real) formula)) +(declare =0_Real (! x (term Real) formula)) +(declare >0_Real (! x (term Real) formula)) +(declare distinct0_Real (! x (term Real) formula)) + ; unary negation (declare u-_Real (! t (term Real) (term Real))) |