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_real.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_real.plf')
| -rw-r--r-- | proofs/signatures/th_real.plf | 6 |
1 files changed, 6 insertions, 0 deletions
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))) |