projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 779f9cd) | patch
Add function for tightening literals (#3732)
authorAlex Ozdemir <aozdemir@hmc.edu>
Mon, 10 Feb 2020 21:53:54 +0000 (13:53 -0800)
committerGitHub <noreply@github.com>
Mon, 10 Feb 2020 21:53:54 +0000 (13:53 -0800)
commit499f1c70dbc869e2b1dd5f8a7b98d45bee2d29cc
tree7693c792269cafb3267897346ad52b18c7cc16a7tree
parent779f9cd3c0f9a3620a52c30a853bde9e7b911494commit | diff
Add function for tightening literals (#3732)

* Add function for tightening literals

The function tightens a literal if it can be tightened, and prints a
proof of the result.

* Include a #include

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
src/proof/arith_proof.cpp diff | blob | history
src/proof/arith_proof.h diff | blob | history