diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-11-27 00:59:22 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-27 00:59:22 -0800 |
commit | 72f1d72852213f46d77c85216c9250bb0f0e3eae (patch) | |
tree | be37eea42008589c825680033a0a14776fef69d8 /proofs/signatures/th_lra_test.plf | |
parent | 391ab9df6c3fd9a3771864900c1718534c1e4666 (diff) |
LRA proof signature fixes and a first proof for linear polynomials (#2713)
* LRA proof signature fixes and a first proof
The existing LRA signature had a few problems (e.g. referencing symbols
that didn't exist, extra parentheses, etc). I patched it up and wrote an
first example LRA proof. load `th_lra_test.plf` last to run that test.
* Add dependency info to signatures
I chose to indicate shallow dependencies only.
Diffstat (limited to 'proofs/signatures/th_lra_test.plf')
-rw-r--r-- | proofs/signatures/th_lra_test.plf | 32 |
1 files changed, 32 insertions, 0 deletions
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))))) + ))))) + )))) + )) +) + + + |