diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 16:53:48 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-19 16:53:48 -0600 |
| commit | f2ed7b1aebc175b971e3cebf4c0b2fff6e4e895f (patch) | |
| tree | 9d67467344399282909475f3cf891639f8abbaf8 /src/theory/theory_engine.cpp | |
| parent | 7191e58e5561a159c0cd3b81fddbe311ba70a45b (diff) | |
Enable new implementation of CEGQI based on nested quantifier elimination (#5477)
This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation.
The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly.
Fixes #5365, fixes #5279, fixes #4849, fixes #4433.
This PR also required fixes related to how quantifier elimination is computed.
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d54538049..dc59cbbf5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1215,14 +1215,6 @@ void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) } } -void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) { - if( d_quantEngine ){ - d_quantEngine->getInstantiations( q, insts ); - }else{ - Assert(false); - } -} - void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { if( d_quantEngine ){ d_quantEngine->getInstantiationTermVectors( q, tvecs ); @@ -1231,14 +1223,6 @@ void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector } } -void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { - if( d_quantEngine ){ - d_quantEngine->getInstantiations( insts ); - }else{ - Assert(false); - } -} - void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) { if( d_quantEngine ){ d_quantEngine->getInstantiationTermVectors( insts ); @@ -1247,15 +1231,6 @@ void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std } } -Node TheoryEngine::getInstantiatedConjunction( Node q ) { - if( d_quantEngine ){ - return d_quantEngine->getInstantiatedConjunction( q ); - }else{ - Assert(false); - return Node::null(); - } -} - TrustNode TheoryEngine::getExplanation(TNode node) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node |