projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 77eb7c8) | patch
LIRA sig: int, real terms, and conversions (#3610)
authorAlex Ozdemir <aozdemir@hmc.edu>
Fri, 17 Jan 2020 23:21:03 +0000 (15:21 -0800)
committerGitHub <noreply@github.com>
Fri, 17 Jan 2020 23:21:03 +0000 (15:21 -0800)
commitf9712e22adc1f422f113df4dbc90623f632890a6
treea9fc59c9b3966f17c3c8ee4e802bfdf759676f04tree
parent77eb7c81060ae590a5ae1bbab88c7e21d57b39b9commit | diff
LIRA sig: int, real terms, and conversions (#3610)

* LIRA sig: int, real terms, and conversions

* Address Yoni's comments.

* Better description of "reify" functions
* explicit (rather than implicit) `fail` when reifying integer division

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
proofs/signatures/th_lira.plf [new file with mode: 0644] blob