diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-23 15:44:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-23 20:44:39 +0000 |
| commit | 557e5658048b48b8908675b632fc977f78c71605 (patch) | |
| tree | 8ee9393db67c500705622bd450e16f21a5e3f53d /src/theory/sets/theory_sets.cpp | |
| parent | 86569ce68ed002aeb31d102511d3c9bd8384a7ec (diff) | |
(proof-new) Proofs for sets purification lemmas (#6416)
This adds proofs for sets purification lemmas, which are of the form (= t (skolem t)) and (member t (skolem (singleton t))). Each can be trivially justified in the internal calculus by MACRO_SR_PRED_INTRO.
Diffstat (limited to 'src/theory/sets/theory_sets.cpp')
| -rw-r--r-- | src/theory/sets/theory_sets.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 8406bd14a..4cca76057 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -37,7 +37,7 @@ TheorySets::TheorySets(context::Context* c, d_skCache(), d_state(c, u, valuation, d_skCache), d_im(*this, d_state, nullptr), - d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)), + d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, pnm)), d_notify(*d_internal.get(), d_im) { // use the official theory state and inference manager objects |