diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 11:44:35 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-19 11:44:35 -0600 |
| commit | 3654512dd8b341c5725e550d438b23508493b991 (patch) | |
| tree | 367684e5521e35a452ef669a4e58bb1b5005509c /src/theory/theory_engine.h | |
| parent | b0130a1e032c201fab3c4b19f25871428b761967 (diff) | |
Fix issues related to eliminating extended arithmetic operators (#5475)
This fixes 2 issues related to eliminating arithmetic operators:
(1) counterexample lemmas in CEGQI were not being preprocessed
(2) ensureLiteral was not doing term formula removal.
This corrects these two issues. Now ensureLiteral does full theory preprocessing on the term we are ensuring literal for, meaning this may trigger lemmas if the term contains extended arithmetic operators like div.
Fixes #5469, fixes #5470, fixes #5471.
This adds --sygus-inst to 2 of these benchmarks which moreover makes them solvable.
This also improves our assertions and trace messages.
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 088e413bb..ee3611a53 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -663,7 +663,9 @@ class TheoryEngine { Node getModelValue(TNode var); /** - * Takes a literal and returns an equivalent literal that is guaranteed to be a SAT literal + * Takes a literal and returns an equivalent literal that is guaranteed to be + * a SAT literal. This rewrites and preprocesses n, which notice may involve + * sending lemmas if preprocessing n involves introducing new skolems. */ Node ensureLiteral(TNode n); @@ -746,7 +748,6 @@ private: * This function is called from the smt engine's checkModel routine. */ void checkTheoryAssertionsWithModel(bool hardFailure); - private: IntStat d_arithSubstitutionsAdded; };/* class TheoryEngine */ |