diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-12 10:33:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-12 10:33:32 -0600 |
| commit | 4f367612a386d21315cee7d377176bc83a1402c5 (patch) | |
| tree | 6b572e49d2cddecf11ce8fedf74084df5c449420 /src/theory/quantifiers_engine.cpp | |
| parent | b9eee8d69e9de4641514c35d49c495bd5adead5f (diff) | |
(proof-new) Proofs for skolemization (#5339)
This adds support for proofs in the quantifiers module that performs skolemization.
Also fixes a bug in the proof checker for skolemization.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index cceb04d9f..7f0b46c99 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,7 +30,8 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, +QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, + DecisionManager& dm, ProofNodeManager* pnm) : d_te(te), d_context(te->getSatContext()), @@ -49,7 +50,7 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), d_instantiate(new quantifiers::Instantiate(this, d_userContext, pnm)), - d_skolemize(new quantifiers::Skolemize(this, d_userContext)), + d_skolemize(new quantifiers::Skolemize(this, d_userContext, pnm)), d_term_enum(new quantifiers::TermEnumeration), d_conflict_c(d_context, false), d_quants_prereg(d_userContext), @@ -809,16 +810,16 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ } if( !pol ){ // do skolemization - Node lem = d_skolemize->process(f); + TrustNode lem = d_skolemize->process(f); if (!lem.isNull()) { if (Trace.isOn("quantifiers-sk-debug")) { - Node slem = Rewriter::rewrite(lem); + Node slem = Rewriter::rewrite(lem.getNode()); Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } - getOutputChannel().lemma( + getOutputChannel().trustedLemma( lem, LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY); } return; |