From 7f85896a9f1c9d3c8f65c53c16fea2156bc4dfab Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 29 May 2015 11:47:28 +0200 Subject: [PATCH] Do not enforce dt fairness when single invocation sygus. --- contrib/run-script-smtcomp2015 | 2 +- .../quantifiers/ce_guided_instantiation.cpp | 34 ++++++++++++------- .../quantifiers/ce_guided_instantiation.h | 15 +++++--- src/theory/quantifiers/ce_guided_single_inv.h | 2 ++ src/theory/quantifiers_engine.cpp | 2 ++ 5 files changed, 36 insertions(+), 19 deletions(-) diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015 index c66ee11c6..4cfe5acd9 100644 --- a/contrib/run-script-smtcomp2015 +++ b/contrib/run-script-smtcomp2015 @@ -55,7 +55,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality trywith 30 --inst-when=full --full-saturate-quant trywith 30 --fmf-bound-int --macros-quant - trywith 30 --no-inst-no-entail --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant + trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 30 --decision=justification-stoponly --full-saturate-quant # large runs 3min trywith 60 --term-db-mode=relevant --full-saturate-quant diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 5e6bcf0b4..aaab8f3f9 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -112,7 +112,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { qe->getOutputChannel().lemma( lem ); qe->getOutputChannel().requirePhase( lit, true ); - if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_HEIGHT_PRED ){ + if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){ //implies height bounds on each candidate variable std::vector< Node > lem_c; for( unsigned j=0; jisSingleInvocation(); +} + CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ d_conj = new CegConjecture( qe->getSatContext() ); d_last_inst_si = false; @@ -139,7 +147,7 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) { } unsigned CegInstantiation::needsModel( Theory::Effort e ) { - return QuantifiersEngine::QEFFORT_MODEL; + return QuantifiersEngine::QEFFORT_MODEL; } void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { @@ -161,21 +169,21 @@ void CegInstantiation::registerQuantifier( Node q ) { d_conj->assign( d_quantEngine, q ); //fairness - if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){ + if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ std::vector< Node > mc; for( unsigned j=0; jd_candidates.size(); j++ ){ TypeNode tn = d_conj->d_candidates[j].getType(); - if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_SIZE ){ + if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE ){ if( tn.isDatatype() ){ mc.push_back( NodeManager::currentNM()->mkNode( DT_SIZE, d_conj->d_candidates[j] ) ); } - }else if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){ + }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){ registerMeasuredType( tn ); std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn ); if( it!=d_uf_measure.end() ){ mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) ); } - }else if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_HEIGHT_PRED ){ + }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){ //measure term is a fresh constant mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) ); } @@ -208,15 +216,15 @@ Node CegInstantiation::getNextDecisionRequest() { d_conj->initializeGuard( d_quantEngine ); bool value; if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { - if( d_conj->d_guard_split.isNull() ){ - Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); - d_quantEngine->getOutputChannel().lemma( lem ); - } + //if( d_conj->d_guard_split.isNull() ){ + // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); + // d_quantEngine->getOutputChannel().lemma( lem ); + //} Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; return d_conj->d_guard; } //enforce fairness - if( d_conj->isAssigned() && options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){ + if( d_conj->isAssigned() && d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { if( !value ){ @@ -242,7 +250,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-engine-debug") << conj->d_candidates[i] << " "; } Trace("cegqi-engine-debug") << std::endl; - if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){ + if( conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ Trace("cegqi-engine") << " * Current term size : " << conj->d_curr_lit.get() << std::endl; } @@ -266,7 +274,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { std::vector< Node > model_values; if( getModelValues( conj, conj->d_candidates, model_values ) ){ //check if we must apply fairness lemmas - if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){ + if( conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){ std::vector< Node > lems; for( unsigned j=0; jd_candidates.size(); j++ ){ getMeasureLemmas( conj->d_candidates[j], model_values[j], lems ); diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 52e110720..09e449b35 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -21,6 +21,7 @@ #include "context/cdchunk_list.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/ce_guided_single_inv.h" +#include "theory/quantifiers/modes.h" namespace CVC4 { namespace theory { @@ -49,7 +50,7 @@ public: /** list of constants for quantified formula */ std::vector< Node > d_candidates; /** list of variables on inner quantification */ - std::vector< Node > d_inner_vars; + std::vector< Node > d_inner_vars; std::vector< std::vector< Node > > d_inner_vars_disj; /** list of terms we have instantiated candidates with */ std::map< int, std::vector< Node > > d_candidate_inst; @@ -78,9 +79,13 @@ public: //for fairness Node getLiteral( QuantifiersEngine * qe, int i ); /** is ground */ bool isGround() { return d_inner_vars.empty(); } + /** fairness */ + CegqiFairMode getCegqiFairMode(); + /** is single invocation */ + bool isSingleInvocation(); }; - - + + class CegInstantiation : public QuantifiersModule { typedef context::CDHashMap NodeBoolMap; @@ -128,7 +133,7 @@ public: /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "CegInstantiation"; } /** print solution for synthesis conjectures */ - void printSynthSolution( std::ostream& out ); + void printSynthSolution( std::ostream& out ); /** collect disjuncts */ static void collectDisjuncts( Node n, std::vector< Node >& ex ); public: @@ -139,7 +144,7 @@ public: IntStat d_cegqi_si_lemmas; Statistics(); ~Statistics(); - };/* class CegInstantiation::Statistics */ + };/* class CegInstantiation::Statistics */ Statistics d_statistics; }; diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index fc7481739..54f762720 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -158,6 +158,8 @@ public: void check( std::vector< Node >& lems ); //get solution Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ); + // is single invocation + bool isSingleInvocation() { return !d_single_inv.isNull(); } }; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2177ebc32..6a4998016 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -888,12 +888,14 @@ void QuantifiersEngine::flushLemmas(){ //take default output channel if none is provided d_hasAddedLemma = true; for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){ + Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl; getOutputChannel().lemma( d_lemmas_waiting[i], false, true ); } d_lemmas_waiting.clear(); } if( !d_phase_req_waiting.empty() ){ for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){ + Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl; getOutputChannel().requirePhase( it->first, it->second ); } d_phase_req_waiting.clear(); -- 2.30.2