diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 19:47:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-02 19:47:52 -0500 |
| commit | 5f3d21a7402538af837eaf943b5252b1db90080b (patch) | |
| tree | 0f8a791a8b9fcd03545f720df1110516ada7689e /src/theory/theory_engine.cpp | |
| parent | 4e6eb0a191ec78cbebd842f9c732ef9bd76bd724 (diff) | |
(proof-new) Support proofs of quantifier instantiation (#5001)
This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions.
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6837d4be5..6a548e5b6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -165,7 +165,8 @@ void TheoryEngine::finishInit() { if (d_logicInfo.isQuantified()) { // initialize the quantifiers engine - d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); + d_quantEngine = + new QuantifiersEngine(d_context, d_userContext, this, d_pnm); } // initialize the theory combination manager, which decides and allocates the // equality engines to use for all theories. |