diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-12 12:26:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-12 17:26:44 +0000 |
| commit | 7361b587e9a1b717dfa906d02f66feb6896e80dd (patch) | |
| tree | 4bd9bf83d0e39458e000ed907d194f602b979306 /src/theory/fp/theory_fp.cpp | |
| parent | eead4c73cf785250f45585c2ee786c273df59542 (diff) | |
Consolidate interface to prop engine (#6189)
This consolidates the interface for asserting input formulas to the PropEngine from SmtSolver.
As a consequence of this PR, this corrects one issue with the justification heuristic where skolem definitions were considered "assertions" by the justification heuristic (e.g. formulas that must be satisfied) instead of just being required for skolems in relevant literals. This was asymmetric from skolem definitions from lemmas, which were not being considered assertions. Now, skolem definitions are never assertions.
I tested this on QF_LIA SMT-LIB with decision=justification with 300 second timeout, essentially no difference in results (+6-5 all close to timeout). Also no difference on QF_S + QF_SLIA.
Diffstat (limited to 'src/theory/fp/theory_fp.cpp')
0 files changed, 0 insertions, 0 deletions