diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-05 14:59:20 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-05 15:59:17 -0800 |
| commit | e1845f92742854a35c294541bd931b898b0211d2 (patch) | |
| tree | 39bbe132003a16610d7dbe2a576e0d70873ff856 /src/prop/bvminisat | |
| parent | 1caa321893805c826a18e68aa5a3c86ce5304a9f (diff) | |
Add a new arith constraint proof rule: IntTightenAP (#3818)
This rule is used when a bound on an integer expression is tightened
because of integer reasoning.
Before this rule was subsumed by IntHoleAP, a catch-all rule for integer
reasoning. We are now articulating IntTightenAP separately, because we
can produce proofs for it.
For IntHoleAP, we will have to omit a hole.
Diffstat (limited to 'src/prop/bvminisat')
0 files changed, 0 insertions, 0 deletions