diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index e10ba0fef..dce9c088c 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -29,18 +29,18 @@ using namespace std; namespace CVC4 { -CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){ +CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){ d_refine_count = 0; - d_ceg_si = new CegConjectureSingleInv( this ); + d_ceg_si = new CegConjectureSingleInv( qe, this ); } -void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { +void CegConjecture::assign( Node q ) { Assert( d_quant.isNull() ); Assert( q.getKind()==FORALL ); d_assert_quant = q; //register with single invocation if applicable - if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){ - d_ceg_si->initialize( qe, q ); + if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){ + d_ceg_si->initialize( q ); if( q!=d_ceg_si->d_quant ){ //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant ); //may have rewritten quantified formula (for invariant synthesis) @@ -53,9 +53,9 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } Trace("cegqi") << "Base quantified fm is : " << q << std::endl; //construct base instantiation - d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) ); + d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) ); Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; - if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ + if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj ); Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; //store the inner variables for each disjunct @@ -70,7 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } } d_syntax_guided = true; - }else if( qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){ + }else if( d_qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){ d_syntax_guided = false; }else{ Assert( false ); @@ -150,7 +150,7 @@ bool CegConjecture::needsCheck() { } CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ - d_conj = new CegConjecture( qe->getSatContext() ); + d_conj = new CegConjecture( qe, qe->getSatContext() ); d_last_inst_si = false; } @@ -178,7 +178,7 @@ void CegInstantiation::registerQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==this ){ if( !d_conj->isAssigned() ){ Trace("cegqi") << "Register conjecture : " << q << std::endl; - d_conj->assign( d_quantEngine, q ); + d_conj->assign( q ); //fairness if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ |