From 08077fa4c45c95b17eb557610a3950352f9d8a20 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 10 Oct 2014 13:32:49 +0200 Subject: [PATCH] Add owner map to better manage QuantifiersModules. Initial infrastructure for cegqi. --- src/Makefile.am | 2 + src/parser/smt2/Smt2.g | 2 +- .../quantifiers/ce_guided_instantiation.cpp | 47 +++++++++++++++++++ .../quantifiers/ce_guided_instantiation.h | 46 ++++++++++++++++++ src/theory/quantifiers/inst_strategy_cbqi.cpp | 44 ----------------- src/theory/quantifiers/inst_strategy_cbqi.h | 23 --------- .../quantifiers/instantiation_engine.cpp | 4 +- src/theory/quantifiers/model_builder.cpp | 5 +- src/theory/quantifiers/options | 4 ++ .../quantifiers/quant_conflict_find.cpp | 4 +- .../quantifiers/quantifiers_attributes.cpp | 8 ++++ .../quantifiers/quantifiers_rewriter.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 35 ++++++++++++++ src/theory/quantifiers/term_database.h | 14 ++++++ src/theory/quantifiers_engine.cpp | 38 +++++++++++++-- src/theory/quantifiers_engine.h | 28 +++++++++-- 16 files changed, 223 insertions(+), 83 deletions(-) create mode 100644 src/theory/quantifiers/ce_guided_instantiation.cpp create mode 100644 src/theory/quantifiers/ce_guided_instantiation.h diff --git a/src/Makefile.am b/src/Makefile.am index 908e3de6c..3e0831467 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -329,6 +329,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/conjecture_generator.h \ theory/quantifiers/conjecture_generator.cpp \ + theory/quantifiers/ce_guided_instantiation.h \ + theory/quantifiers/ce_guided_instantiation.cpp \ theory/quantifiers/options_handlers.h \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 366c76194..6fce26484 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1191,7 +1191,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] PARSER_STATE->warning(ss.str()); } // do nothing - } else if(attr == ":axiom" || attr == ":conjecture") { + } else if(attr==":axiom" || attr==":conjecture" || attr==":sygus" || attr==":synthesis") { if(hasValue) { std::stringstream ss; ss << "warning: Attribute " << attr << " does not take a value (ignoring)"; diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp new file mode 100644 index 000000000..fec4255b2 --- /dev/null +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -0,0 +1,47 @@ +/********************* */ +/*! \file ce_guided_instantiation.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief counterexample guided instantiation class + ** + **/ + +#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace std; + +namespace CVC4 { + +CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) { + + +} + +void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { + //TODO +} + +void CegInstantiation::registerQuantifier( Node q ) { + //TODO +} + +void CegInstantiation::assertNode( Node n ) { + +} + +} \ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h new file mode 100644 index 000000000..7861deffa --- /dev/null +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -0,0 +1,46 @@ +/********************* */ +/*! \file ce_guided_instantiation.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief counterexample guided instantiation class + **/ + +#include "cvc4_private.h" + +#ifndef CE_GUIDED_INSTANTIATION_H +#define CE_GUIDED_INSTANTIATION_H + +#include "context/cdhashmap.h" +#include "context/cdchunk_list.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class CegInstantiation : public QuantifiersModule +{ +public: + CegInstantiation( QuantifiersEngine * qe, context::Context* c ); +public: + /* Call during quantifier engine's check */ + void check( Theory::Effort e, unsigned quant_e ); + /* Called for new quantifiers */ + void registerQuantifier( Node q ); + void assertNode( Node n ); + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const { return "CegInstantiation"; } +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 25f15cd78..6a2bd5e2e 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -347,47 +347,3 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta ); return mkRationalNode(qmodel); } - - -InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) : - InstStrategy( qe ), d_th( th ){ - -} - -bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){ - //DO_THIS - return false; -} - -void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){ - -} - -int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){ - Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl; - if( e<2 ){ - return InstStrategy::STATUS_UNFINISHED; - }else if( e==2 ){ - InstMatch m( f ); - for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){ - Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); - if( i.getType().isDatatype() ){ - Node n = getValueFor( i ); - Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl; - m.setValue( j, n); - } - } - //d_quantEngine->addInstantiation( f, m ); - } - return InstStrategy::STATUS_UNKNOWN; -} - -Node InstStrategyDatatypesValue::getValueFor( Node n ){ - //simply get the ground value for n in the current model, if it exists, - // or return an arbitrary ground term otherwise - if( !TermDb::hasInstConstAttr(n) ){ - return n; - }else{ - return n; - } -} diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 9196b9703..bfc0501dc 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -81,29 +81,6 @@ public: }; -class InstStrategyDatatypesValue : public InstStrategy -{ -protected: - /** calculate if we should process this quantifier */ - bool calculateShouldProcess( Node f ); -private: - /** reference to theory datatypes */ - datatypes::TheoryDatatypes* d_th; - /** get value function */ - Node getValueFor( Node n ); -public: - //constructor - InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe ); - ~InstStrategyDatatypesValue(){} - /** reset instantiation */ - void processResetInstantiationRound( Theory::Effort effort ); - /** process method, returns a status */ - int process( Node f, Theory::Effort effort, int e ); - /** identify */ - std::string identify() const { return std::string("InstStrategyDatatypesValue"); } - -};/* class InstStrategy */ - } } } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 7207ceefb..9c3673bc2 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -215,7 +215,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine - if( TermDb::isRewriteRule( n ) ){ + if( !d_quantEngine->hasOwnership( n, this ) ){ d_quant_active[n] = false; }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){ d_quant_active[n] = false; @@ -300,7 +300,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ } void InstantiationEngine::registerQuantifier( Node f ){ - if( !TermDb::isRewriteRule( f ) ){ + if( d_quantEngine->hasOwnership( f, this ) ){ //Notice() << "do cbqi " << f << " ? " << std::endl; if( options::cbqi() ){ Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 2c9a33388..cbff2b581 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -40,7 +40,7 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe } bool QModelBuilder::isQuantifierActive( Node f ) { - return !TermDb::isRewriteRule( f ); + return d_qe->hasOwnership( f ); } @@ -382,8 +382,7 @@ QModelBuilderIG::Statistics::~Statistics(){ } bool QModelBuilderIG::isQuantifierActive( Node f ){ - return !TermDb::isRewriteRule( f ) && - ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end(); + return d_qe->hasOwnership( f ) && ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end(); } bool QModelBuilderIG::isTermActive( Node n ){ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 872f270e7..5e3c66d9a 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -173,4 +173,8 @@ option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0 number of ground terms to generate for model filtering option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false more aggressive merging for universal equality engine, introduces terms + +option ceGuidedInst --cegqi bool :default false + counterexample guided quantifier instantiation + endmodule diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index ee4464f87..060994379 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1702,7 +1702,7 @@ Node QuantConflictFind::mkEqNode( Node a, Node b ) { //-------------------------------------------------- registration void QuantConflictFind::registerQuantifier( Node q ) { - if( !TermDb::isRewriteRule( q ) ){ + if( d_quantEngine->hasOwnership( q, this ) ){ d_quants.push_back( q ); d_quant_id[q] = d_quants.size(); Trace("qcf-qregister") << "Register "; @@ -1839,7 +1839,7 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) { //-------------------------------------------------- handling assertions / eqc void QuantConflictFind::assertNode( Node q ) { - if( !TermDb::isRewriteRule( q ) ){ + if( d_quantEngine->hasOwnership( q, this ) ){ Trace("qcf-proc") << "QCF : assertQuantifier : "; debugPrintQuant("qcf-proc", q); Trace("qcf-proc") << std::endl; diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index f58e89c38..48608cb4e 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -33,6 +33,14 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, s Trace("quant-attr-debug") << "Set conjecture " << n << std::endl; ConjectureAttribute ca; n.setAttribute( ca, true ); + }else if( attr=="sygus" ){ + Trace("quant-attr-debug") << "Set sygus " << n << std::endl; + SygusAttribute ca; + n.setAttribute( ca, true ); + }else if( attr=="synthesis" ){ + Trace("quant-attr-debug") << "Set synthesis " << n << std::endl; + SynthesisAttribute ca; + n.setAttribute( ca, true ); }else if( attr=="quant-inst-max-level" ){ Assert( node_values.size()==1 ); uint64_t lvl = node_values[0].getConst().getNumerator().getLong(); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index d142007c6..fb7ff679b 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1117,7 +1117,7 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { NodeBuilder<> patternListB(kind::INST_PATTERN_LIST); //the entire rewrite rule is the first pattern if( options::quantRewriteRules() ){ - patternListB << NodeManager::currentNM()->mkNode( INST_PATTERN, r ); + patternListB << NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, r ); } patternListB << static_cast(patternB); forallB << static_cast(patternListB); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 7ec503016..405b3749d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -21,6 +21,8 @@ #include "theory/quantifiers/theory_quantifiers.h" #include "util/datatype.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/quantifiers/rewrite_engine.h" using namespace std; using namespace CVC4; @@ -991,6 +993,16 @@ void TermDb::computeAttributes( Node q ) { Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl; d_qattr_conjecture[q] = true; } + if( avar.getAttribute(SygusAttribute()) ){ + Trace("quant-attr") << "Attribute : sygus : " << q << std::endl; + d_qattr_sygus[q] = true; + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + } + if( avar.getAttribute(SynthesisAttribute()) ){ + Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl; + d_qattr_synthesis[q] = true; + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + } if( avar.hasAttribute(QuantInstLevelAttribute()) ){ d_qattr_qinstLevel[q] = avar.getAttribute(QuantInstLevelAttribute()); Trace("quant-attr") << "Attribute : quant inst level " << d_qattr_qinstLevel[q] << " : " << q << std::endl; @@ -999,6 +1011,11 @@ void TermDb::computeAttributes( Node q ) { d_qattr_rr_priority[q] = avar.getAttribute(RrPriorityAttribute()); Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl; } + if( avar.getKind()==REWRITE_RULE ){ + Assert( i==0 ); + //set rewrite engine as owner + d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() ); + } } } } @@ -1022,6 +1039,24 @@ bool TermDb::isQAttrAxiom( Node q ) { } } +bool TermDb::isQAttrSygus( Node q ) { + std::map< Node, bool >::iterator it = d_qattr_sygus.find( q ); + if( it==d_qattr_sygus.end() ){ + return false; + }else{ + return it->second; + } +} + +bool TermDb::isQAttrSynthesis( Node q ) { + std::map< Node, bool >::iterator it = d_qattr_synthesis.find( q ); + if( it==d_qattr_synthesis.end() ){ + return false; + }else{ + return it->second; + } +} + int TermDb::getQAttrQuantInstLevel( Node q ) { std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q ); if( it==d_qattr_qinstLevel.end() ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e9234bdfe..3bd0563b6 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -33,6 +33,14 @@ typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; struct ConjectureAttributeId {}; typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; +/** Attribute true for quantifiers that are SyGus conjectures */ +struct SygusAttributeId {}; +typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute; + +/** Attribute true for quantifiers that are synthesis conjectures */ +struct SynthesisAttributeId {}; +typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; + /** Attribute true for nodes that should not be used for matching */ struct NoMatchAttributeId {}; /** use the special for boolean flag */ @@ -297,6 +305,8 @@ public: //general queries concerning quantified formulas wrt modules private: std::map< Node, bool > d_qattr_conjecture; std::map< Node, bool > d_qattr_axiom; + std::map< Node, bool > d_qattr_sygus; + std::map< Node, bool > d_qattr_synthesis; std::map< Node, int > d_qattr_rr_priority; std::map< Node, int > d_qattr_qinstLevel; //record attributes @@ -306,6 +316,10 @@ public: bool isQAttrConjecture( Node q ); /** is axiom */ bool isQAttrAxiom( Node q ); + /** is sygus conjecture */ + bool isQAttrSygus( Node q ); + /** is synthesis conjecture */ + bool isQAttrSynthesis( Node q ); /** get instantiation level */ int getQAttrQuantInstLevel( Node q ); /** get rewrite rule priority */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 7ed5b2164..dfa17558d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -31,6 +31,7 @@ #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/conjecture_generator.h" +#include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/uf/options.h" #include "theory/uf/theory_uf.h" @@ -116,6 +117,12 @@ d_lemmas_produced_c(u){ }else{ d_rr_engine = NULL; } + if( options::ceGuidedInst() ){ + d_ceg_inst = new quantifiers::CegInstantiation( this, c ); + d_modules.push_back( d_ceg_inst ); + }else{ + d_ceg_inst = NULL; + } //options d_total_inst_count_debug = 0; @@ -164,6 +171,30 @@ void QuantifiersEngine::finishInit(){ } } +QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { + std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); + if( it==d_owner.end() ){ + return NULL; + }else{ + return it->second; + } +} + +void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) { + QuantifiersModule * mo = getOwner( q ); + if( mo!=m ){ + if( mo!=NULL ){ + Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << m->identify() << ", but already has owner " << mo->identify() << "!" << std::endl; + } + d_owner[q] = m; + } +} + +bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { + QuantifiersModule * mo = getOwner( q ); + return mo==m || mo==NULL; +} + void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); bool needsCheck = false; @@ -276,9 +307,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ void QuantifiersEngine::registerQuantifier( Node f ){ if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){ Trace("quant") << "QuantifiersEngine : Register quantifier "; - if( d_term_db->isRewriteRule( f ) ){ - Trace("quant") << " (rewrite rule)"; - } Trace("quant") << " : " << f << std::endl; d_quants.push_back( f ); @@ -287,6 +315,10 @@ void QuantifiersEngine::registerQuantifier( Node f ){ //make instantiation constants for f d_term_db->makeInstantiationConstantsFor( f ); d_term_db->computeAttributes( f ); + QuantifiersModule * qm = getOwner( f ); + if( qm!=NULL ){ + Trace("quant") << " Owner : " << qm->identify() << std::endl; + } //register with quantifier relevance if( d_quant_rel ){ d_quant_rel->registerQuantifier( f ); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index e84c4742e..d40277112 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -74,6 +74,7 @@ namespace quantifiers { class RewriteEngine; class RelevantDomain; class ConjectureGenerator; + class CegInstantiation; }/* CVC4::theory::quantifiers */ namespace inst { @@ -115,6 +116,8 @@ private: quantifiers::RewriteEngine * d_rr_engine; /** subgoal generator */ quantifiers::ConjectureGenerator * d_sg_gen; + /** ceg instantiation */ + quantifiers::CegInstantiation * d_ceg_inst; public: //effort levels enum { QEFFORT_CONFLICT, @@ -160,10 +163,6 @@ public: /** get equality query object for the given type. The default is the generic one */ EqualityQueryQuantifiersEngine* getEqualityQuery(); - /** get instantiation engine */ - quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } - /** get model engine */ - quantifiers::ModelEngine* getModelEngine() { return d_model_engine; } /** get default sat context for quantifiers engine */ context::Context* getSatContext(); /** get default sat context for quantifiers engine */ @@ -180,10 +179,31 @@ public: QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; } /** get phase requirement terms */ void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); +public: //modules + /** get instantiation engine */ + quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } + /** get model engine */ + quantifiers::ModelEngine* getModelEngine() { return d_model_engine; } /** get bounded integers utility */ quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; } /** Conflict find mechanism for quantifiers */ quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; } + /** rewrite rules utility */ + quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; } + /** subgoal generator */ + quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; } + /** ceg instantiation */ + quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; } +private: + /** owner of quantified formulas */ + std::map< Node, QuantifiersModule * > d_owner; +public: + /** get owner */ + QuantifiersModule * getOwner( Node q ); + /** set owner */ + void setOwner( Node q, QuantifiersModule * m ); + /** considers */ + bool hasOwnership( Node q, QuantifiersModule * m = NULL ); public: /** initialize */ void finishInit(); -- 2.30.2