diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-27 10:32:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-27 10:32:32 -0600 |
| commit | 8795787c2ef337e73b46778b99f5bfa6c2a19f93 (patch) | |
| tree | 0989e95f24c2eeedd177d2281069d266b31d971d /src/theory/theory_engine.cpp | |
| parent | a6d3c9e7fb765704f34815900712b10e85687edc (diff) | |
(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)
This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).
Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 16d68ea5c..ba65fe69d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1175,15 +1175,6 @@ Node TheoryEngine::getPreprocessedTerm(TNode n) return d_propEngine->getPreprocessedTerm(rewritten); } -void TheoryEngine::printInstantiations( std::ostream& out ) { - if( d_quantEngine ){ - d_quantEngine->printInstantiations( out ); - }else{ - out << "Internal error : instantiations not available when quantifiers are not present." << std::endl; - Assert(false); - } -} - void TheoryEngine::printSynthSolution( std::ostream& out ) { if( d_quantEngine ){ d_quantEngine->printSynthSolution( out ); @@ -1193,30 +1184,6 @@ void TheoryEngine::printSynthSolution( std::ostream& out ) { } } -void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) { - if( d_quantEngine ){ - d_quantEngine->getInstantiatedQuantifiedFormulas( qs ); - }else{ - Assert(false); - } -} - -void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { - if( d_quantEngine ){ - d_quantEngine->getInstantiationTermVectors( q, tvecs ); - }else{ - Assert(false); - } -} - -void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) { - if( d_quantEngine ){ - d_quantEngine->getInstantiationTermVectors( insts ); - }else{ - Assert(false); - } -} - TrustNode TheoryEngine::getExplanation(TNode node) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node |