diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-12 15:37:00 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-12 15:37:00 -0500 |
commit | ad18e6d4bab518a29648823eca9ba5ee1ebc8400 (patch) | |
tree | a377d00e07e5af4cd669252c1ebb1b11cc5c3506 /src/theory/quantifiers_engine.cpp | |
parent | d44ef0e9af9230e1949b0d3d4b03f1fcd497ad6d (diff) |
Encapsulate synth engine (#3271)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 47 |
1 files changed, 25 insertions, 22 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a03596060..a6ec1c077 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -385,11 +385,6 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const return d_tr_trie.get(); } -quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const -{ - return d_private->d_synth_e.get(); -} - QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); if( it==d_owner.end() ){ @@ -527,24 +522,32 @@ void QuantifiersEngine::ppNotifyAssertions( Trace("quant-engine-proc") << "ppNotifyAssertions in QE, #assertions = " << assertions.size() << " check epr = " << (d_qepr != NULL) << std::endl; - if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) || - d_qepr != NULL) { - for (unsigned i = 0; i < assertions.size(); i++) { - if (options::instLevelInputOnly() && options::instMaxLevel() != -1) { - quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions[i], - 0); - } - if (d_qepr != NULL) { - d_qepr->registerAssertion(assertions[i]); - } + if (options::instLevelInputOnly() && options::instMaxLevel() != -1) + { + for (const Node& a : assertions) + { + quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0); } - if (d_qepr != NULL) { - // must handle sources of other new constants e.g. separation logic - // FIXME: cleanup - sep::TheorySep* theory_sep = - static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP)); - theory_sep->initializeBounds(); - d_qepr->finishInit(); + } + if (d_qepr != NULL) + { + for (const Node& a : assertions) + { + d_qepr->registerAssertion(a); + } + // must handle sources of other new constants e.g. separation logic + // FIXME (as part of project 3) : cleanup + sep::TheorySep* theory_sep = + static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP)); + theory_sep->initializeBounds(); + d_qepr->finishInit(); + } + if (options::ceGuidedInst()) + { + quantifiers::SynthEngine* sye = d_private->d_synth_e.get(); + for (const Node& a : assertions) + { + sye->preregisterAssertion(a); } } } |