projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 391ab9d) | patch
LRA proof signature fixes and a first proof for linear polynomials (#2713)
authorAlex Ozdemir <aozdemir@hmc.edu>
Tue, 27 Nov 2018 08:59:22 +0000 (00:59 -0800)
committerGitHub <noreply@github.com>
Tue, 27 Nov 2018 08:59:22 +0000 (00:59 -0800)
commit72f1d72852213f46d77c85216c9250bb0f0e3eae
treebe37eea42008589c825680033a0a14776fef69d8tree
parent391ab9df6c3fd9a3771864900c1718534c1e4666commit | 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.
proofs/signatures/th_lra.plf diff | blob | history
proofs/signatures/th_lra_test.plf [new file with mode: 0644] blob
proofs/signatures/th_real.plf diff | blob | history