diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-26 12:43:50 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-26 12:43:50 -0600 |
commit | ca648afb2a7574991b1dc9817c1b8e2546548073 (patch) | |
tree | 30bcc19878be364e9e2c61bc10e9974acf198f30 /src/theory/quantifiers/anti_skolem.cpp | |
parent | 022dbeb9e2dc925cf0dcffb75ea57aedf09395de (diff) |
Refactor quantifiers engine initialization (#5813)
This is a step towards breaking up the quantifiers engine.
The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.
This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.
Diffstat (limited to 'src/theory/quantifiers/anti_skolem.cpp')
-rw-r--r-- | src/theory/quantifiers/anti_skolem.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index 531dd8d21..c91ba419b 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -84,9 +84,10 @@ QuantAntiSkolem::CDSkQuantCache::~CDSkQuantCache() { } } -QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe) - : QuantifiersModule(qe) { - d_sqc = new CDSkQuantCache(qe->getUserContext()); +QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs) + : QuantifiersModule(qs, qe) +{ + d_sqc = new CDSkQuantCache(qs.getUserContext()); } QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; } @@ -160,7 +161,8 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e) bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) { Assert(!quants.empty()); std::sort( quants.begin(), quants.end() ); - if( d_sqc->add( d_quantEngine->getUserContext(), quants ) ){ + if (d_sqc->add(d_qstate.getUserContext(), quants)) + { //partition into connected components if( pconnected && quants.size()>1 ){ Trace("anti-sk-debug") << "Partition into connected components..." << std::endl; |