From: ajreynol Date: Wed, 4 Nov 2015 09:41:49 +0000 (+0100) Subject: Better combination of UF with cbqi, refactor quantifiers intialization. X-Git-Tag: cvc5-1.0.0~6177 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f9e109b0ac12ffbfd167a19dcd60f16241a0542c;p=cvc5.git Better combination of UF with cbqi, refactor quantifiers intialization. --- diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 5ae8905d1..3e69a616a 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -292,9 +292,9 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve std::vector< Node > mbp_vts_coeff[2][2]; std::vector< Node > mbp_lit[2]; //std::vector< MbpBounds > mbp_bounds[2]; - unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; - for( unsigned r=0; r >::iterator ita = d_curr_asserts.find( tid ); if( ita!=d_curr_asserts.end() ){ @@ -303,7 +303,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; Node atom = lit.getKind()==NOT ? lit[0] : lit; bool pol = lit.getKind()!=NOT; - if( tid==THEORY_ARITH ){ + if( pvtn.isReal() ){ //arithmetic inequalities and disequalities if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ Assert( atom[0].getType().isInteger() || atom[0].getType().isReal() ); @@ -614,7 +614,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //[4] resort to using value in model // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype - if( effort>0 || pvtn.isBoolean() || !curr_var.empty() ){ + if( ( effort>0 || pvtn.isBoolean() || !curr_var.empty() ) && !pvtn.isSort() ){ Node mv = getModelValue( pv ); Node pv_coeff_m; Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; @@ -976,14 +976,10 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node } Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { - /* - if( e.getType().isInteger() && !t.getType().isInteger() ){ - //TODO : round up/down this bound? - return Node::null(); - } - */ Node val = t; Trace("cbqi-bound2") << "Value : " << val << std::endl; + Assert( !e.getType().isInteger() || t.getType().isInteger() ); + Assert( !e.getType().isInteger() || mt.getType().isInteger() ); //add rho value //get the value of c*e Node ceValue = me; @@ -1005,7 +1001,7 @@ Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower Node rho; //if( !mt.getType().isInteger() ){ //round up/down - //mt = NodeManager::currentNM()->mkNode( + //mt = NodeManager::currentNM()->mkNode( //} if( isLower ){ rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); @@ -1157,6 +1153,7 @@ void CegInstantiator::processAssertions() { //for each variable std::vector< TheoryId > tids; + tids.push_back(THEORY_UF); for( unsigned i=0; i& lems, st d_var_order_index.clear(); } } - - //remove ITEs + + //remove ITEs IteSkolemMap iteSkolemMap; d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); Assert( d_aux_vars.empty() ); @@ -1466,7 +1463,7 @@ int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node } } } - + ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); if( ires!=0 ){ Node realPart; @@ -1510,7 +1507,7 @@ int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl; if( ires!=0 ){ - val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS, + val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS, NodeManager::currentNM()->mkNode( ires==-1 ? MINUS : PLUS, val, realPart ), NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); Trace("cbqi-inst-debug") << "result : " << val << std::endl; @@ -1521,6 +1518,6 @@ int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node vts_coeff_inf = vts_coeff[0]; vts_coeff_delta = vts_coeff[1]; } - + return ires; } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 07de0a3d1..56d5022c4 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -34,7 +34,7 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ){ - + } bool InstStrategyCbqi::needsCheck( Theory::Effort e ) { @@ -44,7 +44,7 @@ bool InstStrategyCbqi::needsCheck( Theory::Effort e ) { unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) { for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( d_quantEngine->getOwner( q )==this && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ return QuantifiersEngine::QEFFORT_STANDARD; } } @@ -57,7 +57,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine - if( d_quantEngine->getOwner( q )==this ){ + if( doCbqi( q ) ){ if( !hasAddedCbqiLemma( q ) ){ d_added_cbqi_lemma.insert( q ); Trace("cbqi") << "Do cbqi for " << q << std::endl; @@ -76,7 +76,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; registerCounterexampleLemma( q, lem ); } - //set inactive the quantified formulas whose CE literals are asserted false + //set inactive the quantified formulas whose CE literals are asserted false }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); @@ -106,7 +106,7 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( d_quantEngine->getOwner( q )==this && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ process( q, e, ee ); } } @@ -127,13 +127,15 @@ bool InstStrategyCbqi::checkComplete() { void InstStrategyCbqi::preRegisterQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ - //take ownership of the quantified formula - d_quantEngine->setOwner( q, this ); + if( !options::cbqiAll() && !options::cbqiSplx() ){ + //take full ownership of the quantified formula + d_quantEngine->setOwner( q, this ); + } } } void InstStrategyCbqi::registerQuantifier( Node q ) { - + } void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 2785ad128..49f561234 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -30,16 +30,7 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL){ - -} - -InstantiationEngine::~InstantiationEngine() { - delete d_i_ag; - delete d_isup; -} - -void InstantiationEngine::finishInit(){ +QuantifiersModule( qe ){ if( options::eMatching() ){ //these are the instantiation strategies for E-matching //user-provided patterns @@ -51,9 +42,18 @@ void InstantiationEngine::finishInit(){ //auto-generated patterns d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine ); d_instStrategies.push_back( d_i_ag ); + }else{ + d_isup = NULL; + d_i_ag = NULL; } } +InstantiationEngine::~InstantiationEngine() { + delete d_i_ag; + delete d_isup; +} + + void InstantiationEngine::presolve() { for( unsigned i=0; ipresolve(); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index bc1199588..4a990ff6b 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -74,8 +74,6 @@ private: public: InstantiationEngine( QuantifiersEngine* qe ); ~InstantiationEngine(); - /** initialize */ - void finishInit(); void presolve(); bool needsCheck( Theory::Effort e ); void reset_round( Theory::Effort e ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index a60f5af78..2578d0b7f 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -31,8 +31,10 @@ option dtVarExpandQuant --dt-var-exp-quant bool :default true #ite lift mode for quantified formulas option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h" ite lifting mode for quantified formulas -option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true - split variables occurring as conditions of ITE in quantifiers +option condVarSplitQuant --cond-var-split-quant bool :default true + split quantified formulas that lead to variable eliminations +option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false + aggressive split quantified formulas that lead to variable eliminations option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false split ites with dt testers as conditions # Whether to CNF quantifier bodies diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index a1af1313d..26b598413 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -624,7 +624,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign } if( !d_unassigned.empty() && ( success || doContinue ) ){ - Trace("qcf-check") << "Assign to unassigned..." << std::endl; + Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size() << ")..." << std::endl; do { if( doFail ){ Trace("qcf-check-unassign") << "Failure, try again..." << std::endl; @@ -702,6 +702,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign } } }while( success && isMatchSpurious( p ) ); + Trace("qcf-check") << "done assigning." << std::endl; } if( success ){ for( unsigned i=0; isecond.push_back( r ); } }else{ - d_eqcs[rtn].push_back( r ); + if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){ + d_eqcs[rtn].push_back( r ); + } } } ++eqcs_i; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index e911b0dc4..895408269 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -648,62 +648,111 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, bool hasPol, bool pol, } } -Node QuantifiersRewriter::computeProcessIte( Node body ){ - if( body.getKind()==ITE ){ - if( options::iteDtTesterSplitQuant() ){ - Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl; - std::map< Node, Node > pcons; - std::map< Node, std::map< int, Node > > ncons; - std::vector< Node > conj; - computeDtTesterIteSplit( body, pcons, ncons, conj ); - Assert( !conj.empty() ); - if( conj.size()>1 ){ - Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl; - for( unsigned i=0; i=0 ) || ( n.getKind()==OR && pol<=0 ) ){ + pol = n.getKind()==AND ? 1 : -1; + for( unsigned i=0; imkNode( AND, conj ); } } - if( options::iteCondVarSplitQuant() ){ - Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl; + }else if( n.getKind()==BOUND_VARIABLE ){ + return true; + } + return false; +} + +Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){ + if( options::iteDtTesterSplitQuant() && body.getKind()==ITE ){ + Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl; + std::map< Node, Node > pcons; + std::map< Node, std::map< int, Node > > ncons; + std::vector< Node > conj; + computeDtTesterIteSplit( body, pcons, ncons, conj ); + Assert( !conj.empty() ); + if( conj.size()>1 ){ + Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl; + for( unsigned i=0; imkNode( AND, conj ); + } + } + if( options::condVarSplitQuant() ){ + if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() && !TermDb::isFunDefAnnotation( ipl ) ) ){ + Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl; bool do_split = false; - for( unsigned r=0; r<2; r++ ){ - //check if there is a variable elimination - Node b = r==0 ? body[0] : body[0].negate(); - QuantPhaseReq qpr( b ); - Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; - for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ - Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl; - if( it->second ){ - if( it->first.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - if( it->first[i].getKind()==BOUND_VARIABLE ){ - unsigned j = i==0 ? 1 : 0; - if( !TermDb::containsTerm( it->first[j], it->first[i] ) ){ - do_split = true; - break; - } - } + unsigned index_max = body.getKind()==ITE ? 0 : 1; + for( unsigned index=0; index<=index_max; index++ ){ + if( isConditionalVariableElim( body[index] ) ){ + do_split = true; + break; + } + } + if( do_split ){ + Node pos; + Node neg; + if( body.getKind()==ITE ){ + pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); + neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); + }else{ + pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); + neg = NodeManager::currentNM()->mkNode( OR, body[0], body[1].negate() ); + } + Trace("quantifiers-rewrite-debug") << "*** Split (conditional variable eq) " << body << " into : " << std::endl; + Trace("quantifiers-rewrite-debug") << " " << pos << std::endl; + Trace("quantifiers-rewrite-debug") << " " << neg << std::endl; + return NodeManager::currentNM()->mkNode( AND, pos, neg ); + } + }else if( body.getKind()==OR && options::condVarSplitQuantAgg() ){ + std::vector< Node > bchildren; + std::vector< Node > nchildren; + for( unsigned i=0; i children; + for( unsigned j=0; jmkNode( AND, children ) ); + } + split = true; + } } } - if( do_split ){ - //bool cpol = (r==1); - Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); - //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - //pos = Rewriter::rewrite( pos ); - Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); - Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl; - Trace("quantifiers-rewrite-ite") << " " << pos << std::endl; - Trace("quantifiers-rewrite-ite") << " " << neg << std::endl; - return NodeManager::currentNM()->mkNode( AND, pos, neg ); + if( !split ){ + bchildren.push_back( body[i] ); } } + if( !nchildren.empty() ){ + Trace("quantifiers-rewrite-debug") << "*** Split (conditional variable eq) " << body << " into : " << std::endl; + for( unsigned i=0; imkNode( OR, bchildren ); + Trace("quantifiers-rewrite-debug") << " " << nchildren[i] << std::endl; + bchildren.pop_back(); + } + return NodeManager::currentNM()->mkNode( AND, nchildren ); + } } } return body; @@ -738,10 +787,9 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& break; } } - } - else if( it->first.getKind()==APPLY_TESTER ){ + }else if( it->first.getKind()==APPLY_TESTER ){ if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){ - Trace("dt-var-expand") << "Expand datatype variable based on : " << it->first << std::endl; + Trace("var-elim-dt") << "Expand datatype variable based on : " << it->first << std::endl; std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] ); if( ita!=args.end() ){ vars.push_back( it->first[0] ); @@ -760,11 +808,21 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& newVars.push_back( v ); } subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) ); - Trace("dt-var-expand") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl; + Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl; args.erase( ita ); args.insert( args.end(), newVars.begin(), newVars.end() ); } } + }else if( it->first.getKind()==BOUND_VARIABLE ){ + if( options::varElimQuant() ){ + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first ); + if( ita!=args.end() ){ + Trace("var-elim-bool") << "Variable eliminate : " << it->first << " in " << body << std::endl; + vars.push_back( it->first ); + subs.push_back( NodeManager::currentNM()->mkConst( it->second ) ); + args.erase( ita ); + } + } } } if( !vars.empty() ){ @@ -1286,7 +1344,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption return true; //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); }else if( computeOption==COMPUTE_PROCESS_ITE ){ - return options::iteDtTesterSplitQuant() || options::iteCondVarSplitQuant(); + return options::iteDtTesterSplitQuant() || options::condVarSplitQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ @@ -1332,7 +1390,7 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp n = NodeManager::currentNM()->mkNode( OR, new_conds ); } }else if( computeOption==COMPUTE_PROCESS_ITE ){ - n = computeProcessIte( n ); + n = computeProcessIte( n, ipl ); }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 98a83b7de..0ad79587a 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -39,6 +39,7 @@ private: static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); static Node computeClause( Node n ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); + static bool isConditionalVariableElim( Node n, int pol=0 ); private: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ); @@ -48,7 +49,7 @@ private: static Node computeProcessTerms( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds ); - static Node computeProcessIte( Node body ); + static Node computeProcessIte( Node body, Node ipl ); static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); @@ -60,9 +61,9 @@ private: COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, COMPUTE_PROCESS_TERMS, - COMPUTE_PROCESS_ITE, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, + COMPUTE_PROCESS_ITE, //COMPUTE_FLATTEN_ARGS_UF, //COMPUTE_CNF, COMPUTE_LAST diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index bfeacf044..e513666a4 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1599,9 +1599,23 @@ bool TermDb::isFunDef( Node q ) { return !getFunDefHead( q ).isNull(); } +bool TermDb::isFunDefAnnotation( Node ipl ) { + if( !ipl.isNull() ){ + for( unsigned i=0; i > d_op_map; /** map from type nodes to terms of that type */ std::map< TypeNode, std::vector< Node > > d_type_map; - - + + /** count number of non-redundant ground terms per operator */ std::map< Node, int > d_op_nonred_count; /**mapping from UF terms to representatives of their arguments */ @@ -165,7 +165,7 @@ public: std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ std::map< Node, Node > d_term_elig_eqc; - + public: /** ground terms for operator */ unsigned getNumGroundTerms( Node f ); @@ -204,7 +204,7 @@ public: Node getEligibleTermInEqc( TNode r ); /** is inst closure */ bool isInstClosure( Node r ); - + //for model basis private: //map from types to model basis terms @@ -301,7 +301,7 @@ public: bool isClosedEnumerableType( TypeNode tn ); // may complete bool mayComplete( TypeNode tn ); - + //for triggers private: /** helper function for compute var contains */ @@ -414,6 +414,8 @@ public: //general queries concerning quantified formulas wrt modules static Node getRewriteRule( Node q ); /** is fun def */ static bool isFunDef( Node q ); + /** is fun def */ + static bool isFunDefAnnotation( Node ipl ); /** is sygus conjecture */ static bool isSygusConjecture( Node q ); /** is sygus conjecture */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 41e560557..ba3dc9fb0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -94,8 +94,6 @@ d_presolve_cache_wic(u){ d_tr_trie = new inst::TriggerTrie; d_hasAddedLemma = false; - bool needsBuilder = false; - bool needsRelDom = false; Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; @@ -115,95 +113,145 @@ d_presolve_cache_wic(u){ d_quant_rel = NULL; } + d_qcf = NULL; + d_sg_gen = NULL; + d_inst_engine = NULL; + d_i_cbqi = NULL; + d_model_engine = NULL; + d_bint = NULL; + d_rr_engine = NULL; + d_ceg_inst = NULL; + d_lte_part_inst = NULL; + d_alpha_equiv = NULL; + d_fun_def_engine = NULL; + d_uee = NULL; + d_fs = NULL; + d_rel_dom = NULL; + d_builder = NULL; + + d_total_inst_count_debug = 0; + d_ierCounter = 0; + d_ierCounter_lc = 0; + //if any strategy called only on last call, use phase 3 + d_inst_when_phase = options::cbqi() ? 3 : 2; +} + +QuantifiersEngine::~QuantifiersEngine(){ + delete d_builder; + delete d_rr_engine; + delete d_bint; + delete d_model_engine; + delete d_inst_engine; + delete d_qcf; + delete d_quant_rel; + delete d_rel_dom; + delete d_model; + delete d_tr_trie; + delete d_term_db; + delete d_eq_query; + delete d_sg_gen; + delete d_ceg_inst; + delete d_lte_part_inst; + delete d_fun_def_engine; + delete d_uee; + delete d_fs; + delete d_i_cbqi; +} + +EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { + return d_eq_query; +} + +context::Context* QuantifiersEngine::getSatContext(){ + return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext(); +} + +context::UserContext* QuantifiersEngine::getUserContext(){ + return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext(); +} + +OutputChannel& QuantifiersEngine::getOutputChannel(){ + return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel(); +} +/** get default valuation for the quantifiers engine */ +Valuation& QuantifiersEngine::getValuation(){ + return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation(); +} + +void QuantifiersEngine::finishInit(){ + context::Context * c = getSatContext(); + Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl; + bool needsBuilder = false; + bool needsRelDom = false; //add quantifiers modules if( options::quantConflictFind() || options::quantRewriteRules() ){ d_qcf = new quantifiers::QuantConflictFind( this, c); d_modules.push_back( d_qcf ); - }else{ - d_qcf = NULL; } if( options::conjectureGen() ){ d_sg_gen = new quantifiers::ConjectureGenerator( this, c ); d_modules.push_back( d_sg_gen ); - }else{ - d_sg_gen = NULL; } //maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules if( !options::finiteModelFind() || options::fmfInstEngine() ){ d_inst_engine = new quantifiers::InstantiationEngine( this ); d_modules.push_back( d_inst_engine ); - }else{ - d_inst_engine = NULL; } - //counterexample-based instantiation (initialized during finishInit) - d_i_cbqi = NULL; - if( options::cbqi() && options::cbqiModel() ){ - needsBuilder = true; + if( options::cbqi() ){ + if( options::cbqiSplx() ){ + d_i_cbqi = new quantifiers::InstStrategySimplex( (arith::TheoryArith*)getTheoryEngine()->theoryOf( THEORY_ARITH ), this ); + d_modules.push_back( d_i_cbqi ); + }else{ + d_i_cbqi = new quantifiers::InstStrategyCegqi( this ); + d_modules.push_back( d_i_cbqi ); + if( options::cbqiModel() ){ + needsBuilder = true; + } + } } //finite model finding if( options::finiteModelFind() ){ if( options::fmfBoundInt() ){ d_bint = new quantifiers::BoundedIntegers( c, this ); d_modules.push_back( d_bint ); - }else{ - d_bint = NULL; } d_model_engine = new quantifiers::ModelEngine( c, this ); d_modules.push_back( d_model_engine ); needsBuilder = true; - }else{ - d_model_engine = NULL; - d_bint = NULL; } if( options::quantRewriteRules() ){ d_rr_engine = new quantifiers::RewriteEngine( c, this ); d_modules.push_back(d_rr_engine); - }else{ - d_rr_engine = NULL; } if( options::ceGuidedInst() ){ d_ceg_inst = new quantifiers::CegInstantiation( this, c ); d_modules.push_back( d_ceg_inst ); needsBuilder = true; - }else{ - d_ceg_inst = NULL; } if( options::ltePartialInst() ){ d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); d_modules.push_back( d_lte_part_inst ); - }else{ - d_lte_part_inst = NULL; } if( options::quantAlphaEquiv() ){ d_alpha_equiv = new quantifiers::AlphaEquivalence( this ); - }else{ - d_alpha_equiv = NULL; } //if( options::funDefs() ){ // d_fun_def_engine = new quantifiers::FunDefEngine( this, c ); // d_modules.push_back( d_fun_def_engine ); - //}else{ - d_fun_def_engine = NULL; //} if( options::quantEqualityEngine() ){ d_uee = new quantifiers::QuantEqualityEngine( this, c ); d_modules.push_back( d_uee ); - }else{ - d_uee = NULL; } //full saturation : instantiate from relevant domain, then arbitrary terms if( options::fullSaturateQuant() || options::fullSaturateInst() ){ d_fs = new quantifiers::FullSaturation( this ); d_modules.push_back( d_fs ); needsRelDom = true; - }else{ - d_fs = NULL; } if( needsRelDom ){ d_rel_dom = new quantifiers::RelevantDomain( this, d_model ); - }else{ - d_rel_dom = NULL; } if( needsBuilder ){ @@ -219,74 +267,8 @@ d_presolve_cache_wic(u){ Trace("quant-engine-debug") << "...make default model builder." << std::endl; d_builder = new quantifiers::QModelBuilderDefault( c, this ); } - }else{ - d_builder = NULL; } - d_total_inst_count_debug = 0; - d_ierCounter = 0; - d_ierCounter_lc = 0; -} - -QuantifiersEngine::~QuantifiersEngine(){ - delete d_builder; - delete d_rr_engine; - delete d_bint; - delete d_model_engine; - delete d_inst_engine; - delete d_qcf; - delete d_quant_rel; - delete d_rel_dom; - delete d_model; - delete d_tr_trie; - delete d_term_db; - delete d_eq_query; - delete d_sg_gen; - delete d_ceg_inst; - delete d_lte_part_inst; - delete d_fun_def_engine; - delete d_uee; - delete d_fs; - delete d_i_cbqi; -} - -EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { - return d_eq_query; -} - -context::Context* QuantifiersEngine::getSatContext(){ - return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext(); -} - -context::Context* QuantifiersEngine::getUserContext(){ - return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext(); -} - -OutputChannel& QuantifiersEngine::getOutputChannel(){ - return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel(); -} -/** get default valuation for the quantifiers engine */ -Valuation& QuantifiersEngine::getValuation(){ - return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation(); -} - -void QuantifiersEngine::finishInit(){ - Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl; - //counterexample-based quantifier instantiation - if( options::cbqi() ){ - if( options::cbqiSplx() ){ - d_i_cbqi = new quantifiers::InstStrategySimplex( (arith::TheoryArith*)getTheoryEngine()->theoryOf( THEORY_ARITH ), this ); - d_modules.push_back( d_i_cbqi ); - }else{ - d_i_cbqi = new quantifiers::InstStrategyCegqi( this ); - d_modules.push_back( d_i_cbqi ); - } - }else{ - d_i_cbqi = NULL; - } - for( int i=0; i<(int)d_modules.size(); i++ ){ - d_modules[i]->finishInit(); - } } QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { @@ -717,7 +699,7 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v d_temp_inst_debug[f]++; d_total_inst_count_debug++; Trace("inst") << "*** Instantiate " << f << " with " << std::endl; - for( int i=0; i<(int)terms.size(); i++ ){ + for( unsigned i=0; i& v } Trace("inst") << std::endl; } - Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) ); - } - if( options::cbqiSplx() ){ - for( int i=0; i<(int)terms.size(); i++ ){ - if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ + if( options::cbqi() ){ + if( quantifiers::TermDb::getInstConstAttr(terms[i])==f ){ Trace("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; - for( int i=0; i<(int)terms.size(); i++ ){ + for( unsigned i=0; imaxInstLevel ){ maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); @@ -1017,9 +997,9 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){ performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck(); }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase==0 ) || e==Theory::EFFORT_LAST_CALL ); }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase==0 ) || e==Theory::EFFORT_LAST_CALL ); }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){ performCheck = ( e >= Theory::EFFORT_LAST_CALL ); }else{ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 572149885..bbf3fad61 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -53,8 +53,6 @@ public: virtual ~QuantifiersModule(){} //get quantifiers engine QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } - /** initialize */ - virtual void finishInit() {} /** presolve */ virtual void presolve() {} /* whether this module needs to check this round */ @@ -201,6 +199,7 @@ private: /** inst round counters */ int d_ierCounter; int d_ierCounter_lc; + int d_inst_when_phase; /** has presolve been called */ context::CDO< bool > d_presolve; /** presolve cache */ @@ -220,7 +219,7 @@ public: /** get default sat context for quantifiers engine */ context::Context* getSatContext(); /** get default sat context for quantifiers engine */ - context::Context* getUserContext(); + context::UserContext* getUserContext(); /** get default output channel for the quantifiers engine */ OutputChannel& getOutputChannel(); /** get default valuation for the quantifiers engine */ diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 9d6df2796..bb85e62b3 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -40,7 +40,8 @@ TESTS = \ fib-core.smt2 \ fore19-exp2-core.smt2 \ with-ind-104-core.smt2 \ - syn002-si-real-int.smt2 + syn002-si-real-int.smt2 \ + krs-sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/krs-sat.smt2 b/test/regress/regress0/fmf/krs-sat.smt2 new file mode 100644 index 000000000..22d9e4474 --- /dev/null +++ b/test/regress/regress0/fmf/krs-sat.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort $$unsorted 0) +(declare-fun cowlNothing ($$unsorted) Bool) +(declare-fun cowlThing ($$unsorted) Bool) +(declare-fun xsd_integer ($$unsorted) Bool) +(declare-fun xsd_string ($$unsorted) Bool) +(declare-fun is () $$unsorted) +(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) ))) +(assert (forall ((X $$unsorted)) (= (xsd_string X) (not (xsd_integer X))) )) +(assert (and (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X is)) ) (cowlThing is))) +(assert (cowlThing is)) +(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) ) (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X is)) ))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 89dcc0a26..e6b0a59fc 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -59,8 +59,9 @@ TESTS = \ floor.smt2 \ array-unsat-simp3.smt2 \ mix-simp.smt2 \ - mix-coeff.smt2 \ - mix-match.smt2 + mix-coeff.smt2 \ + mix-match.smt2 \ + ari056.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/ari056.smt2 b/test/regress/regress0/quantifiers/ari056.smt2 new file mode 100644 index 000000000..ed4d2bf4a --- /dev/null +++ b/test/regress/regress0/quantifiers/ari056.smt2 @@ -0,0 +1,4 @@ +(set-logic UFNIRA) +(set-info :status unsat) +(assert (forall ((X Int)) (= X 12) )) +(check-sat)