|
* [LRA proof] Refine "poly" and "term Real" distinction
Short Version:
Refined the LRA signature and used the refined version to write two new
test proofs which are close to interface compatible with the LRA proofs
that CVC4 will produce.
Love Version:
LRA proofs have the following interface:
* Given predicates between real terms
* Prove bottom
However, even though the type of the interface does not express this,
the predicates are **linear bounds**, not arbitrary real bounds. Thus
LRA proofs have the following structure:
1. Prove that the input predicates are equivalent to a set of linear
bounds.
2. Use the linear bounds to prove bottom using farkas coefficients.
Notice that the distinction between linear bounds (associated in the
signature with the string "poly") and real predicates (which relate
"term Real"s to one another) matters quite a bit. We have certain inds
of axioms for one, and other axioms for the other.
The signature used to muddy this distinction using a constructor called
"term_poly" which converted between them. I decided it was better to buy
into the distinction fully.
Now all of the axioms for step (2) use the linear bounds and axioms for
step (1) use both kinds of bounds, which makes sense because step (1) is
basically a conversion.
Also had to add an axiom or two, because some were missing.
* Update proofs/signatures/th_lra.plf
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Improved test readability, removed unused axioms
The LRA proof tests did not have appropriate documentation, and did not
specify **what** they proved. Now they each have a header comment
stating their premises and conclusion, and that conclusion is enforced
by a type annotation in the test.
The LRA signature included some unused axioms concerning `poly_term`.
Now they've been removed.
Credits to Yoni for noticing both problems.
|
