theory/quantifiers/anti_skolem.cpp \
theory/quantifiers/equality_infer.h \
theory/quantifiers/equality_infer.cpp \
+ theory/quantifiers/inst_propagator.h \
+ theory/quantifiers/inst_propagator.cpp \
theory/arith/theory_arith_type_rules.h \
theory/arith/type_enumerator.h \
theory/arith/arithvar.h \
option instNoEntail --inst-no-entail bool :read-write :default true
do not consider instances of quantified formulas that are currently entailed
+
+option instPropagate --inst-propagate bool :read-write :default false
+ internal propagation for instantiations for selecting relevant instances
### rewrite rules options
}
Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl;
//get the representative of rhs with substitution subs
- TNode grhs = getTermDatabase()->evaluateTerm( rhs, subs, true );
+ TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true );
Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl;
if( !grhs.isNull() ){
if( glhs!=grhs ){
--- /dev/null
+/********************* */\r
+/*! \file inst_propagator.cpp\r
+ ** \verbatim\r
+ ** Top contributors (to current version):\r
+ ** Andrew Reynolds\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS\r
+ ** in the top-level source directory) and their institutional affiliations.\r
+ ** All rights reserved. See the file COPYING in the top-level source\r
+ ** directory for licensing information.\endverbatim\r
+ **\r
+ ** Propagate mechanism for instantiations\r
+ **/\r
+\r
+#include <vector>\r
+\r
+#include "theory/quantifiers/inst_propagator.h"\r
+#include "theory/rewriter.h"\r
+#include "theory/quantifiers/term_database.h"\r
+\r
+using namespace CVC4;\r
+using namespace std;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+using namespace CVC4::kind;\r
+\r
+\r
+EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){\r
+ d_true = NodeManager::currentNM()->mkConst( true );\r
+ d_false = NodeManager::currentNM()->mkConst( false );\r
+}\r
+\r
+bool EqualityQueryInstProp::reset( Theory::Effort e ) {\r
+ d_uf.clear();\r
+ d_uf_exp.clear();\r
+ d_diseq_list.clear();\r
+ return true;\r
+}\r
+\r
+/** contains term */\r
+bool EqualityQueryInstProp::hasTerm( Node a ) {\r
+ if( getEngine()->hasTerm( a ) ){\r
+ return true;\r
+ }else{\r
+ std::vector< Node > exp;\r
+ Node ar = getUfRepresentative( a, exp );\r
+ return !ar.isNull() && getEngine()->hasTerm( ar );\r
+ }\r
+}\r
+\r
+/** get the representative of the equivalence class of a */\r
+Node EqualityQueryInstProp::getRepresentative( Node a ) {\r
+ if( getEngine()->hasTerm( a ) ){\r
+ a = getEngine()->getRepresentative( a );\r
+ }\r
+ std::vector< Node > exp;\r
+ Node ar = getUfRepresentative( a, exp );\r
+ return ar.isNull() ? a : ar;\r
+}\r
+\r
+/** returns true if a and b are equal in the current context */\r
+bool EqualityQueryInstProp::areEqual( Node a, Node b ) {\r
+ if( a==b ){\r
+ return true;\r
+ }else{\r
+ eq::EqualityEngine* ee = getEngine();\r
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){\r
+ if( ee->areEqual( a, b ) ){\r
+ return true;\r
+ }\r
+ }\r
+ return false;\r
+ }\r
+}\r
+\r
+/** returns true is a and b are disequal in the current context */\r
+bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {\r
+ if( a==b ){\r
+ return true;\r
+ }else{\r
+ eq::EqualityEngine* ee = getEngine();\r
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){\r
+ if( ee->areDisequal( a, b, false ) ){\r
+ return true;\r
+ }\r
+ }\r
+ return false;\r
+ }\r
+}\r
+\r
+/** get the equality engine associated with this query */\r
+eq::EqualityEngine* EqualityQueryInstProp::getEngine() {\r
+ return d_qe->getMasterEqualityEngine();\r
+}\r
+\r
+/** get the equivalence class of a */\r
+void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {\r
+ //TODO?\r
+}\r
+\r
+TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {\r
+ TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );\r
+ if( !t.isNull() ){\r
+ return t;\r
+ }else{\r
+ //TODO?\r
+ return TNode::null();\r
+ }\r
+}\r
+\r
+Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {\r
+ bool engine_has_a = getEngine()->hasTerm( a );\r
+ if( engine_has_a ){\r
+ a = getEngine()->getRepresentative( a );\r
+ }\r
+ //get union find representative, if this occurs in the equality engine, return it\r
+ unsigned prev_size = exp.size();\r
+ Node ar = getUfRepresentative( a, exp );\r
+ if( !ar.isNull() ){\r
+ if( engine_has_a || getEngine()->hasTerm( ar ) ){\r
+ Assert( getEngine()->hasTerm( ar ) );\r
+ Assert( getEngine()->getRepresentative( ar )==ar );\r
+ return ar;\r
+ }\r
+ }else{\r
+ if( engine_has_a ){\r
+ return a;\r
+ }\r
+ }\r
+ //retract explanation\r
+ while( exp.size()>prev_size ){\r
+ exp.pop_back();\r
+ }\r
+ return Node::null();\r
+}\r
+\r
+bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {\r
+ if( areEqual( a, b ) ){\r
+ return true;\r
+ }else{\r
+ std::vector< Node > exp_a;\r
+ Node ar = getUfRepresentative( a, exp_a );\r
+ if( !ar.isNull() ){\r
+ std::vector< Node > exp_b;\r
+ if( ar==getUfRepresentative( b, exp_b ) ){\r
+ merge_exp( exp, exp_a );\r
+ merge_exp( exp, exp_b );\r
+ return true;\r
+ }\r
+ }\r
+ return false;\r
+ }\r
+}\r
+\r
+bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {\r
+ if( areDisequal( a, b ) ){\r
+ return true;\r
+ }else{\r
+ //TODO?\r
+ return false;\r
+ }\r
+}\r
+\r
+Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {\r
+ Assert( exp.empty() );\r
+ std::map< Node, Node >::iterator it = d_uf.find( a );\r
+ if( it!=d_uf.end() ){\r
+ if( it->second==a ){\r
+ Assert( d_uf_exp[ a ].empty() );\r
+ return it->second;\r
+ }else{\r
+ Node m = getUfRepresentative( it->second, exp );\r
+ Assert( !m.isNull() );\r
+ if( m!=it->second ){\r
+ //update union find\r
+ d_uf[ a ] = m;\r
+ //update explanation : merge the explanation of the parent\r
+ merge_exp( d_uf_exp[ a ], exp );\r
+ Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;\r
+ }\r
+ //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset\r
+ exp.clear();\r
+ exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );\r
+ return m;\r
+ }\r
+ }else{\r
+ return Node::null();\r
+ }\r
+}\r
+\r
+// set a == b with reason, return status, modify a and b to representatives pre-merge\r
+int EqualityQueryInstProp::setEqual( Node& a, Node& b, std::vector< Node >& reason ) {\r
+ int status = STATUS_MERGED_UNKNOWN;\r
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", reason size = " << reason.size() << std::endl;\r
+ //get the representative for a\r
+ std::vector< Node > exp_a;\r
+ Node ar = getUfRepresentative( a, exp_a );\r
+ if( ar.isNull() ){\r
+ Assert( exp_a.empty() );\r
+ ar = a;\r
+ }\r
+ if( ar==b ){\r
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;\r
+ return STATUS_NONE;\r
+ }\r
+ bool swap = false;\r
+ //get the representative for b\r
+ std::vector< Node > exp_b;\r
+ Node br = getUfRepresentative( b, exp_b );\r
+ if( br.isNull() ){\r
+ Assert( exp_b.empty() );\r
+ br = b;\r
+ if( !getEngine()->hasTerm( br ) ){\r
+ if( ar!=a ){\r
+ swap = true;\r
+ }\r
+ }else{\r
+ if( getEngine()->hasTerm( ar ) ){\r
+ status = STATUS_MERGED_KNOWN;\r
+ }\r
+ }\r
+ }else{\r
+ if( ar==br ){\r
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;\r
+ return STATUS_NONE;\r
+ }else if( getEngine()->hasTerm( ar ) ){\r
+ if( getEngine()->hasTerm( br ) ){\r
+ status = STATUS_MERGED_KNOWN;\r
+ }else{\r
+ swap = true;\r
+ }\r
+ }\r
+ }\r
+ if( swap ){\r
+ //swap\r
+ Node temp_r = ar;\r
+ ar = br;\r
+ br = temp_r;\r
+ }\r
+\r
+ Assert( ar!=br );\r
+ Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );\r
+\r
+ //update the union find\r
+ Assert( d_uf_exp[ar].empty() );\r
+ Assert( d_uf_exp[br].empty() );\r
+\r
+ d_uf[ar] = br;\r
+ merge_exp( d_uf_exp[ar], exp_a );\r
+ merge_exp( d_uf_exp[ar], exp_b );\r
+ merge_exp( d_uf_exp[ar], reason );\r
+\r
+ d_uf[br] = br;\r
+ d_uf_exp[br].clear();\r
+\r
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;\r
+ a = ar;\r
+ b = br;\r
+ return status;\r
+}\r
+\r
+\r
+void EqualityQueryInstProp::addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol ) {\r
+ if( is_prop ){\r
+ if( isLiteral( n ) ){\r
+ props.push_back( pol ? n : n.negate() );\r
+ return;\r
+ }\r
+ }\r
+ args.push_back( n );\r
+}\r
+\r
+bool EqualityQueryInstProp::isLiteral( Node n ) {\r
+ Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();\r
+ Assert( ak!=NOT );\r
+ return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;\r
+}\r
+\r
+//this is identical to TermDb::evaluateTerm2, but tracks more information\r
+Node EqualityQueryInstProp::evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,\r
+ std::map< Node, bool >& watch_list_out, std::vector< TNode >& props ) {\r
+ std::map< TNode, Node >::iterator itv = visited.find( n );\r
+ if( itv != visited.end() ){\r
+ return itv->second;\r
+ }else{\r
+ Trace("term-db-eval") << "evaluate term : " << n << std::endl;\r
+ std::vector< Node > exp_n;\r
+ Node ret = getRepresentativeExp( n, exp_n );\r
+ if( ret.isNull() ){\r
+ //term is not known to be equal to a representative in equality engine, evaluate it\r
+ Kind k = n.getKind();\r
+ if( k==FORALL ){\r
+ ret = Node::null();\r
+ }else{\r
+ std::map< Node, bool > watch_list_out_curr;\r
+ TNode f = d_qe->getTermDatabase()->getMatchOperator( n );\r
+ std::vector< TNode > args;\r
+ bool ret_set = false;\r
+ bool childChanged = false;\r
+ int abort_i = -1;\r
+ //get the child entailed polarity\r
+ Assert( n.getKind()!=IMPLIES );\r
+ bool newHasPol, newPol;\r
+ QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );\r
+ //for each child\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ TNode c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props );\r
+ if( c.isNull() ){\r
+ ret = Node::null();\r
+ ret_set = true;\r
+ break;\r
+ }else if( c==d_true || c==d_false ){\r
+ //short-circuiting\r
+ if( k==kind::AND || k==kind::OR ){\r
+ if( (k==kind::AND)==(c==d_false) ){\r
+ ret = c;\r
+ ret_set = true;\r
+ break;\r
+ }else{\r
+ //redundant\r
+ c = Node::null();\r
+ childChanged = true;\r
+ }\r
+ }else if( k==kind::ITE && i==0 ){\r
+ Assert( watch_list_out_curr.empty() );\r
+ ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props );\r
+ ret_set = true;\r
+ break;\r
+ }else if( k==kind::NOT ){\r
+ ret = c==d_true ? d_false : d_true;\r
+ ret_set = true;\r
+ break;\r
+ }\r
+ }\r
+ if( !c.isNull() ){\r
+ childChanged = childChanged || n[i]!=c;\r
+ if( !f.isNull() && !watch_list_out_curr.empty() ){\r
+ // we are done if this is an UF application and an argument is unevaluated\r
+ args.push_back( c );\r
+ abort_i = i;\r
+ break;\r
+ }else if( ( k==kind::AND || k==kind::OR ) ){\r
+ if( c.getKind()==k ){\r
+ //flatten\r
+ for( unsigned j=0; j<c.getNumChildren(); j++ ){\r
+ addArgument( args, props, c[j], newHasPol, newPol );\r
+ }\r
+ }else{\r
+ addArgument( args, props, c, newHasPol, newPol );\r
+ }\r
+ //if we are in a branching position\r
+ if( hasPol && !newHasPol && args.size()>=2 ){\r
+ //we are done if at least two args are unevaluated\r
+ abort_i = i;\r
+ break;\r
+ }\r
+ }else if( k==kind::ITE ){\r
+ //we are done if we are ITE and condition is unevaluated\r
+ Assert( i==0 );\r
+ args.push_back( c );\r
+ abort_i = i;\r
+ break;\r
+ }else{\r
+ args.push_back( c );\r
+ }\r
+ }\r
+ }\r
+ //add remaining children if we aborted\r
+ if( abort_i!=-1 ){\r
+ for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){\r
+ args.push_back( n[i] );\r
+ }\r
+ }\r
+ //copy over the watch list\r
+ for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){\r
+ watch_list_out[itc->first] = itc->second;\r
+ }\r
+\r
+ //if we have not short-circuited evaluation\r
+ if( !ret_set ){\r
+ //if it is an indexed term, return the congruent term\r
+ if( !f.isNull() && watch_list_out.empty() ){\r
+ Assert( args.size()==n.getNumChildren() );\r
+ //args contains terms known by the equality engine\r
+ TNode nn = getCongruentTerm( f, args );\r
+ Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl;\r
+ if( !nn.isNull() ){\r
+ //successfully constructed representative in EE\r
+ Assert( exp_n.empty() );\r
+ ret = getRepresentativeExp( nn, exp_n );\r
+ Trace("term-db-eval") << "return rep, exp size = " << exp_n.size() << std::endl;\r
+ merge_exp( exp, exp_n );\r
+ ret_set = true;\r
+ Assert( !ret.isNull() );\r
+ }\r
+ }\r
+ if( !ret_set ){\r
+ if( childChanged ){\r
+ Trace("term-db-eval") << "return rewrite" << std::endl;\r
+ if( ( k==kind::AND || k==kind::OR ) ){\r
+ if( args.empty() ){\r
+ ret = k==kind::AND ? d_true : d_false;\r
+ ret_set = true;\r
+ }else if( args.size()==1 ){\r
+ ret = args[0];\r
+ ret_set = true;\r
+ }\r
+ }\r
+ if( !ret_set ){\r
+ Assert( args.size()==n.getNumChildren() );\r
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){\r
+ args.insert( args.begin(), n.getOperator() );\r
+ }\r
+ ret = NodeManager::currentNM()->mkNode( k, args );\r
+ ret = Rewriter::rewrite( ret );\r
+ watch_list_out[ret] = true;\r
+ }\r
+ }else{\r
+ ret = n;\r
+ watch_list_out[ret] = true;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }else{\r
+ Trace("term-db-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;\r
+ merge_exp( exp, exp_n );\r
+ }\r
+ Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl;\r
+ visited[n] = ret;\r
+ return ret;\r
+ }\r
+}\r
+\r
+void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {\r
+ //TODO : optimize\r
+ if( v.empty() ){\r
+ Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() );\r
+ v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );\r
+ }else{\r
+ //std::vector< Node >::iterator v_end = v.end();\r
+ up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;\r
+ for( int j=0; j<up_to_size; j++ ){\r
+ if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){\r
+ v.push_back( v_to_merge[j] );\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+\r
+void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {\r
+ d_active = true;\r
+ //information about the instance\r
+ d_q = q;\r
+ d_lem = lem;\r
+ Assert( d_terms.empty() );\r
+ d_terms.insert( d_terms.end(), terms.begin(), terms.end() );\r
+ //the current lemma\r
+ d_curr = body;\r
+ d_curr_exp.push_back( body );\r
+}\r
+\r
+InstPropagator::InstPropagator( QuantifiersEngine* qe ) :\r
+d_qe( qe ), d_notify(*this), d_qy( qe ){\r
+}\r
+\r
+bool InstPropagator::reset( Theory::Effort e ) {\r
+ d_icount = 0;\r
+ d_ii.clear();\r
+ for( unsigned i=0; i<2; i++ ){\r
+ d_conc_to_id[i].clear();\r
+ }\r
+ d_conflict = false;\r
+ d_watch_list.clear();\r
+ d_relevant_inst.clear();\r
+ return d_qy.reset( e );\r
+}\r
+\r
+void InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {\r
+ if( !d_conflict ){\r
+ if( Trace.isOn("qip-prop") ){\r
+ Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;\r
+ for( unsigned i=0; i<terms.size(); i++ ){\r
+ Trace("qip-prop") << " " << terms[i] << std::endl;\r
+ }\r
+ }\r
+ unsigned id = d_icount;\r
+ d_icount++;\r
+ Trace("qip-prop") << "...assign id=" << id << std::endl;\r
+ d_ii[id].init( q, lem, terms, body );\r
+ //initialize the information\r
+ if( cacheConclusion( id, body ) ){\r
+ Assert( d_update_list.empty() );\r
+ d_update_list.push_back( id );\r
+ bool firstTime = true;\r
+ //update infos in the update list until empty \r
+ do {\r
+ unsigned uid = d_update_list.back();\r
+ d_update_list.pop_back();\r
+ if( d_ii[uid].d_active ){\r
+ update( uid, d_ii[uid], firstTime );\r
+ }\r
+ firstTime = false;\r
+ }while( !d_update_list.empty() );\r
+ }else{\r
+ d_ii[id].d_active = false;\r
+ Trace("qip-prop") << "...duplicate." << std::endl;\r
+ }\r
+ }\r
+}\r
+\r
+bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {\r
+ Assert( !d_conflict );\r
+ Assert( ii.d_active );\r
+ Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;\r
+ //update the evaluation of the current lemma\r
+ std::map< TNode, Node > visited;\r
+ std::map< Node, bool > watch_list;\r
+ std::vector< TNode > props;\r
+ Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props );\r
+ if( eval.isNull() ){\r
+ ii.d_active = false;\r
+ }else if( firstTime || eval!=ii.d_curr ){\r
+ if( EqualityQueryInstProp::isLiteral( eval ) ){\r
+ props.push_back( eval );\r
+ eval = d_qy.d_true;\r
+ watch_list.clear();\r
+ }\r
+ if( Trace.isOn("qip-prop") ){\r
+ Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;\r
+ Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = ";\r
+ debugPrintExplanation( ii.d_curr_exp, "qip-prop" );\r
+ Trace("qip-prop") << std::endl;\r
+ Trace("qip-prop") << "...watch list: " << std::endl;\r
+ for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){\r
+ Trace("qip-prop") << " " << itw->first << std::endl;\r
+ }\r
+ Trace("qip-prop") << "...new propagations: " << std::endl;\r
+ for( unsigned i=0; i<props.size(); i++ ){\r
+ Trace("qip-prop") << " " << props[i] << std::endl;\r
+ }\r
+ Trace("qip-prop") << std::endl;\r
+ }\r
+ //determine the status of eval\r
+ if( eval==d_qy.d_false ){\r
+ Assert( props.empty() );\r
+ //we have inferred a conflict\r
+ conflict( ii.d_curr_exp );\r
+ return false;\r
+ }else{\r
+ for( unsigned i=0; i<props.size(); i++ ){\r
+ //if we haven't propagated this literal yet\r
+ if( cacheConclusion( id, props[i], 1 ) ){\r
+ Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];\r
+ bool pol = props[i].getKind()!=NOT;\r
+ if( lit.getKind()==EQUAL ){\r
+ propagate( lit[0], lit[1], pol, ii.d_curr_exp );\r
+ }else{\r
+ propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );\r
+ }\r
+ if( d_conflict ){\r
+ return false;\r
+ }\r
+ }\r
+ }\r
+ //if we have not inferred this conclusion yet\r
+ if( cacheConclusion( id, eval ) ){\r
+ ii.d_curr = eval;\r
+ //update the watch list\r
+ Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;\r
+ //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations.\r
+ // Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms.\r
+ for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){\r
+ d_watch_list[ itw->first ][ id ] = true;\r
+ }\r
+ }else{\r
+ Trace("qip-prop-debug") << "...conclusion is duplicate." << std::endl;\r
+ ii.d_active = false;\r
+ }\r
+ }\r
+ }else{\r
+ Trace("qip-prop-debug") << "...did not update." << std::endl;\r
+ }\r
+ Assert( !d_conflict );\r
+ return true;\r
+}\r
+\r
+void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {\r
+ if( Trace.isOn("qip-propagate") ){\r
+ Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";\r
+ debugPrintExplanation( exp, "qip-propagate" );\r
+ Trace("qip-propagate") << "..." << std::endl;\r
+ }\r
+ if( pol ){\r
+ std::vector< Node > exp_d;\r
+ if( d_qy.areDisequalExp( a, b, exp_d ) ){\r
+ Trace("qip-prop-debug") << "...conflict." << std::endl;\r
+ EqualityQueryInstProp::merge_exp( exp, exp_d );\r
+ conflict( exp );\r
+ }else{\r
+ //set equal\r
+ int status = d_qy.setEqual( a, b, exp );\r
+ if( status==EqualityQueryInstProp::STATUS_NONE ){\r
+ Trace("qip-prop-debug") << "...already equal." << std::endl;\r
+ return;\r
+ }else if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){\r
+ Assert( d_qy.getEngine()->hasTerm( a ) );\r
+ Assert( d_qy.getEngine()->hasTerm( b ) );\r
+ Trace("qip-prop-debug") << "...equality between known terms." << std::endl;\r
+ addRelevantInstances( exp, "qip-propagate" );\r
+ }\r
+ Trace("qip-prop-debug") << "...merging " << a << " and " << b << std::endl;\r
+ for( unsigned i=0; i<2; i++ ){\r
+ //update terms from watched lists\r
+ Node c = i==0 ? a : b;\r
+ std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );\r
+ if( it!=d_watch_list.end() ){\r
+ Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;\r
+ for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){\r
+ unsigned idw = itw->first;\r
+ if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){\r
+ Trace("qip-prop-debug") << "...will update " << idw << std::endl;\r
+ d_update_list.push_back( idw );\r
+ }\r
+ }\r
+ d_watch_list.erase( c );\r
+ }\r
+ }\r
+ }\r
+ }else{\r
+ std::vector< Node > exp_e;\r
+ if( d_qy.areEqualExp( a, b, exp_e ) ){\r
+ EqualityQueryInstProp::merge_exp( exp, exp_e );\r
+ conflict( exp );\r
+ }else{\r
+ //TODO?\r
+ }\r
+ }\r
+}\r
+\r
+void InstPropagator::conflict( std::vector< Node >& exp ) {\r
+ Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;\r
+ d_conflict = true;\r
+ d_relevant_inst.clear();\r
+ addRelevantInstances( exp, "qip-propagate" );\r
+}\r
+\r
+bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {\r
+ Assert( prop_index==0 || prop_index==1 );\r
+ //check if the conclusion is non-redundant\r
+ if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){\r
+ d_conc_to_id[prop_index][body] = id;\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {\r
+ for( unsigned i=0; i<exp.size(); i++ ){\r
+ Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );\r
+ Trace(c) << " relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;\r
+ d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;\r
+ }\r
+}\r
+\r
+void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {\r
+ for( unsigned i=0; i<exp.size(); i++ ){\r
+ Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );\r
+ Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";\r
+ }\r
+}\r
+\r
--- /dev/null
+/********************* */\r
+/*! \file inst_propagator.h\r
+ ** \verbatim\r
+ ** Top contributors (to current version):\r
+ ** Andrew Reynolds\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS\r
+ ** in the top-level source directory) and their institutional affiliations.\r
+ ** All rights reserved. See the file COPYING in the top-level source\r
+ ** directory for licensing information.\endverbatim\r
+ **\r
+ ** \brief Propagate mechanism for instantiations\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H\r
+#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H\r
+\r
+#include <iostream>\r
+#include <string>\r
+#include <vector>\r
+#include <map>\r
+#include "expr/node.h"\r
+#include "expr/type_node.h"\r
+#include "theory/quantifiers_engine.h"\r
+#include "theory/quantifiers/term_database.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace quantifiers {\r
+\r
+class EqualityQueryInstProp : public EqualityQuery {\r
+private:\r
+ /** pointer to quantifiers engine */\r
+ QuantifiersEngine* d_qe;\r
+public:\r
+ EqualityQueryInstProp( QuantifiersEngine* qe );\r
+ ~EqualityQueryInstProp(){};\r
+ /** reset */\r
+ bool reset( Theory::Effort e );\r
+ /** identify */\r
+ std::string identify() const { return "EqualityQueryInstProp"; }\r
+ /** extends engine */\r
+ bool extendsEngine() { return true; }\r
+ /** contains term */\r
+ bool hasTerm( Node a );\r
+ /** get the representative of the equivalence class of a */\r
+ Node getRepresentative( Node a );\r
+ /** returns true if a and b are equal in the current context */\r
+ bool areEqual( Node a, Node b );\r
+ /** returns true is a and b are disequal in the current context */\r
+ bool areDisequal( Node a, Node b );\r
+ /** get the equality engine associated with this query */\r
+ eq::EqualityEngine* getEngine();\r
+ /** get the equivalence class of a */\r
+ void getEquivalenceClass( Node a, std::vector< Node >& eqc );\r
+ /** get congruent term */\r
+ TNode getCongruentTerm( Node f, std::vector< TNode >& args );\r
+public:\r
+ /** get the representative of the equivalence class of a, with explanation */\r
+ Node getRepresentativeExp( Node a, std::vector< Node >& exp );\r
+ /** returns true if a and b are equal in the current context */\r
+ bool areEqualExp( Node a, Node b, std::vector< Node >& exp );\r
+ /** returns true is a and b are disequal in the current context */\r
+ bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );\r
+private:\r
+ /** term index */\r
+ std::map< Node, TermArgTrie > d_func_map_trie;\r
+ /** union find for terms beyond what is stored in equality engine */\r
+ std::map< Node, Node > d_uf;\r
+ std::map< Node, std::vector< Node > > d_uf_exp;\r
+ Node getUfRepresentative( Node a, std::vector< Node >& exp );\r
+ /** disequality list, stores explanations */\r
+ std::map< Node, std::map< Node, Node > > d_diseq_list;\r
+ /** add arg */\r
+ void addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol );\r
+public:\r
+ enum {\r
+ STATUS_MERGED_KNOWN,\r
+ STATUS_MERGED_UNKNOWN,\r
+ STATUS_NONE,\r
+ };\r
+ /** set equal */\r
+ int setEqual( Node& a, Node& b, std::vector< Node >& reason );\r
+ Node d_true;\r
+ Node d_false;\r
+public:\r
+ //for explanations\r
+ static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );\r
+\r
+ Node evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,\r
+ std::map< Node, bool >& watch_list_out, std::vector< TNode >& props );\r
+ static bool isLiteral( Node n );\r
+};\r
+\r
+class InstPropagator : public QuantifiersUtil {\r
+private:\r
+ /** pointer to quantifiers engine */\r
+ QuantifiersEngine* d_qe;\r
+ /** notify class */\r
+ class InstantiationNotifyInstPropagator : public InstantiationNotify {\r
+ InstPropagator& d_ip;\r
+ public:\r
+ InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}\r
+ virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); }\r
+ };\r
+ InstantiationNotifyInstPropagator d_notify;\r
+ /** notify instantiation method */\r
+ void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );\r
+ /** equality query */\r
+ EqualityQueryInstProp d_qy;\r
+ class InstInfo {\r
+ public:\r
+ bool d_active;\r
+ Node d_q;\r
+ Node d_lem;\r
+ std::vector< Node > d_terms;\r
+ // the current entailed body\r
+ Node d_curr;\r
+ //explanation for current entailed body\r
+ std::vector< Node > d_curr_exp;\r
+ void init( Node q, Node lem, std::vector< Node >& terms, Node body );\r
+ };\r
+ /** instantiation count/info */\r
+ unsigned d_icount;\r
+ std::map< unsigned, InstInfo > d_ii;\r
+ std::map< TNode, unsigned > d_conc_to_id[2];\r
+ /** are we in conflict */\r
+ bool d_conflict;\r
+ /** watch list */\r
+ std::map< Node, std::map< unsigned, bool > > d_watch_list;\r
+ /** update list */\r
+ std::vector< unsigned > d_update_list;\r
+ /** relevant instances */\r
+ std::map< unsigned, bool > d_relevant_inst;\r
+private:\r
+ bool update( unsigned id, InstInfo& i, bool firstTime = false );\r
+ void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );\r
+ void conflict( std::vector< Node >& exp );\r
+ bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );\r
+ void addRelevantInstances( std::vector< Node >& exp, const char * c );\r
+\r
+ void debugPrintExplanation( std::vector< Node >& exp, const char * c );\r
+public:\r
+ InstPropagator( QuantifiersEngine* qe );\r
+ ~InstPropagator(){}\r
+ /** reset */\r
+ bool reset( Theory::Effort e );\r
+ /** identify */\r
+ std::string identify() const { return "InstPropagator"; }\r
+ /** get the notify mechanism */\r
+ InstantiationNotify* getInstantiationNotify() { return &d_notify; }\r
+};\r
+\r
+}\r
+}\r
+}\r
+\r
+#endif\r
d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
}
if( d_type==typ_ground ){
- int e = p->evaluate( d_n );
- if( e==1 ){
- d_ground_eval[0] = p->d_true;
- }else if( e==-1 ){
- d_ground_eval[0] = p->d_false;
+ //int e = p->evaluate( d_n );
+ //if( e==1 ){
+ // d_ground_eval[0] = p->d_true;
+ //}else if( e==-1 ){
+ // d_ground_eval[0] = p->d_false;
+ //}
+ //modified
+ for( unsigned i=0; i<2; i++ ){
+ if( p->getTermDatabase()->isEntailed( d_n, i==0 ) ){
+ d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
+ }
}
}else if( d_type==typ_eq ){
for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
if( !d_n[i].hasBoundVar() ){
- d_ground_eval[i] = p->evaluateTerm( d_n[i] );
+ TNode t = p->getTermDatabase()->getEntailedTerm( d_n[i] );
+ if( t.isNull() ){
+ d_ground_eval[i] = d_n[i];
+ }else{
+ d_ground_eval[i] = t;
+ }
}
}
}
int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );
if( vn==-1 ){
//evaluate the value, see if it is compatible
- int e = p->evaluate( n );
- if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
+ //int e = p->evaluate( n );
+ //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
+ // d_child_counter = 0;
+ //}
+ //modified
+ if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){
d_child_counter = 0;
}
}else{
}
}
-int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
- int ret = 0;
- if( n.getKind()==EQUAL ){
- Node n1 = evaluateTerm( n[0] );
- Node n2 = evaluateTerm( n[1] );
- Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;
- if( areEqual( n1, n2 ) ){
- ret = 1;
- }else if( areDisequal( n1, n2 ) ){
- ret = -1;
- }
- //else if( d_effort>QuantConflictFind::effort_conflict ){
- // ret = -1;
- //}
- }else if( MatchGen::isHandledUfTerm( n ) ){ //predicate
- Node nn = evaluateTerm( n );
- Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;
- if( areEqual( nn, d_true ) ){
- ret = 1;
- }else if( areEqual( nn, d_false ) ){
- ret = -1;
- }
- //else if( d_effort>QuantConflictFind::effort_conflict ){
- // ret = -1;
- //}
- }else if( n.getKind()==NOT ){
- return -evaluate( n[0] );
- }else if( n.getKind()==ITE ){
- int cev1 = evaluate( n[0] );
- int cevc[2] = { 0, 0 };
- for( unsigned i=0; i<2; i++ ){
- if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){
- cevc[i] = evaluate( n[i+1] );
- if( cev1!=0 ){
- ret = cevc[i];
- break;
- }else if( cevc[i]==0 ){
- break;
- }
- }
- }
- if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){
- ret = cevc[0];
- }
- }else if( n.getKind()==IFF ){
- int cev1 = evaluate( n[0] );
- if( cev1!=0 ){
- int cev2 = evaluate( n[1] );
- if( cev2!=0 ){
- ret = cev1==cev2 ? 1 : -1;
- }
- }
-
- }else{
- int ssval = 0;
- if( n.getKind()==OR ){
- ssval = 1;
- }else if( n.getKind()==AND ){
- ssval = -1;
- }
- bool isUnk = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- int cev = evaluate( n[i] );
- if( cev==ssval ){
- ret = ssval;
- break;
- }else if( cev==0 ){
- isUnk = true;
- }
- }
- if( ret==0 && !isUnk ){
- ret = -ssval;
- }
- }
- Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;
- return ret;
-}
-
short QuantConflictFind::getMaxQcfEffort() {
if( options::qcfMode()==QCF_CONFLICT_ONLY ){
return effort_conflict;
}
}
-Node QuantConflictFind::evaluateTerm( Node n ) {
- if( MatchGen::isHandledUfTerm( n ) ){
- Node f = MatchGen::getMatchOperator( this, n );
- Node nn;
- if( getEqualityEngine()->hasTerm( n ) ){
- nn = getTermDatabase()->existsTerm( f, n );
- }else{
- std::vector< TNode > args;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node c = evaluateTerm( n[i] );
- args.push_back( c );
- }
- nn = getTermDatabase()->d_func_map_trie[f].existsTerm( args );
- }
- if( !nn.isNull() ){
- Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;
- return getRepresentative( nn );
- }else{
- Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;
- return n;
- }
- }else if( n.getKind()==ITE ){
- int v = evaluate( n[0], false, false );
- if( v==1 ){
- return evaluateTerm( n[1] );
- }else if( v==-1 ){
- return evaluateTerm( n[2] );
- }
- }
- return getRepresentative( n );
-}
-
/** new node */
void QuantConflictFind::newEqClass( Node n ) {
std::vector< Node > terms;
qi->getMatch( terms );
if( !qi->isTConstraintSpurious( this, terms ) ){
+ //for debugging
if( Debug.isOn("qcf-check-inst") ){
- //if( e==effort_conflict ){
Node inst = d_quantEngine->getInstantiation( q, terms );
Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
- Assert( evaluate( inst )!=1 );
- Assert( evaluate( inst )==-1 || e>effort_conflict );
- //}
+ Assert( !getTermDatabase()->isEntailed( inst, true ) );
+ Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
}
if( d_quantEngine->addInstantiation( q, terms, false ) ){
Trace("qcf-check") << " ... Added instantiation" << std::endl;
Node d_true;
Node d_false;
TNode getZero( Kind k );
-private:
- Node evaluateTerm( Node n );
- int evaluate( Node n, bool pref = false, bool hasPref = false );
private:
//currently asserted quantifiers
NodeList d_qassert;
using namespace CVC4::context;
using namespace CVC4::theory;
+
+unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
+ return QuantifiersEngine::QEFFORT_NONE;
+}
+
+eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
+ return d_quantEngine->getMasterEqualityEngine();
+}
+
+bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
+ eq::EqualityEngine * ee = getEqualityEngine();
+ return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );
+}
+
+bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
+ eq::EqualityEngine * ee = getEqualityEngine();
+ return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );
+}
+
+TNode QuantifiersModule::getRepresentative( TNode n ) {
+ eq::EqualityEngine * ee = getEqualityEngine();
+ if( ee->hasTerm( n ) ){
+ return ee->getRepresentative( n );
+ }else{
+ return n;
+ }
+}
+
+quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
+ return d_quantEngine->getTermDatabase();
+}
+
bool QuantArith::getMonomial( Node n, Node& c, Node& v ){
if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
c = n[0];
class QuantifiersEngine;
+namespace quantifiers {
+ class TermDb;
+}
+
+class QuantifiersModule {
+protected:
+ QuantifiersEngine* d_quantEngine;
+public:
+ QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+ virtual ~QuantifiersModule(){}
+ //get quantifiers engine
+ QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
+ /** presolve */
+ virtual void presolve() {}
+ /* whether this module needs to check this round */
+ virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
+ /* whether this module needs a model built */
+ virtual unsigned needsModel( Theory::Effort e );
+ /* reset at a round */
+ virtual void reset_round( Theory::Effort e ){}
+ /* Call during quantifier engine's check */
+ virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
+ /* check was complete (e.g. no lemmas implies a model) */
+ virtual bool checkComplete() { return true; }
+ /* Called for new quantified formulas */
+ virtual void preRegisterQuantifier( Node q ) { }
+ /* Called for new quantifiers after owners are finalized */
+ virtual void registerQuantifier( Node q ) = 0;
+ virtual void assertNode( Node n ) {}
+ virtual void propagate( Theory::Effort level ){}
+ virtual Node getNextDecisionRequest() { return TNode::null(); }
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ virtual std::string identify() const = 0;
+public:
+ eq::EqualityEngine * getEqualityEngine();
+ bool areDisequal( TNode n1, TNode n2 );
+ bool areEqual( TNode n1, TNode n2 );
+ TNode getRepresentative( TNode n );
+ quantifiers::TermDb * getTermDatabase();
+};/* class QuantifiersModule */
+
+class QuantifiersUtil {
+public:
+ QuantifiersUtil(){}
+ virtual ~QuantifiersUtil(){}
+ /* reset at a round */
+ virtual bool reset( Theory::Effort e ) = 0;
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ virtual std::string identify() const = 0;
+};
+
+
class QuantArith
{
public:
};
-class EqualityQuery {
+class EqualityQuery : public QuantifiersUtil{
public:
EqualityQuery(){}
virtual ~EqualityQuery(){};
virtual eq::EqualityEngine* getEngine() = 0;
/** get the equivalence class of a */
virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
+ /** get the term that exists in EE that is congruent to f with args (f is returned by TermDb::getMatchOperator(...) */
+ virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
};/* class EqualityQuery */
return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i];
}
-void RelevantDomain::reset(){
+bool RelevantDomain::reset( Theory::Effort e ) {
d_is_computed = false;
+ return true;
}
void RelevantDomain::compute(){
namespace theory {
namespace quantifiers {
-class RelevantDomain
+class RelevantDomain : public QuantifiersUtil
{
private:
class RDomain
public:
RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
virtual ~RelevantDomain(){}
- void reset();
+ /* reset */
+ bool reset( Theory::Effort e );
+ /** identify */
+ std::string identify() const { return "RelevantDomain"; }
//compute the relevant domain
void compute();
}
}
-//returns a term n' equivalent to n
-// - if hasSubs = true, then n is consider under substitution subs
-// - if mkNewTerms = true, then n' is either null, or a term in the master equality engine
-Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ) {
+//return a term n' equivalent to n
+// maximal subterms of n' are representatives in the equality engine qy
+Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ) {
std::map< TNode, Node >::iterator itv = visited.find( n );
if( itv != visited.end() ){
return itv->second;
}
- Node ret;
+ Assert( n.getKind()!=BOUND_VARIABLE );
Trace("term-db-eval") << "evaluate term : " << n << std::endl;
- if( qy->hasTerm( n ) ){
- Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
- ret = qy->getRepresentative( n );
- }else if( n.getKind()==BOUND_VARIABLE ){
- if( hasSubs ){
- Assert( subs.find( n )!=subs.end() );
- Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
- if( subsRep ){
- Assert( qy->hasTerm( subs[n] ) );
- Assert( qy->getRepresentative( subs[n] )==subs[n] );
- ret = subs[n];
- }else{
- ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited, qy );
- }
- }
- }else if( n.getKind()==FORALL ){
- ret = n;
- }else{
- if( n.hasOperator() ){
+ Node ret;
+ if( !qy->hasTerm( n ) ){
+ //term is not known to be equal to a representative in equality engine, evaluate it
+ if( n.getKind()==FORALL ){
+ ret = Node::null();
+ }else if( n.hasOperator() ){
TNode f = getMatchOperator( n );
std::vector< TNode > args;
bool ret_set = false;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited, qy );
+ TNode c = evaluateTerm2( n[i], visited, qy );
if( c.isNull() ){
- ret = TNode::null();
+ ret = Node::null();
ret_set = true;
break;
+ }else if( c==d_true || c==d_false ){
+ //short-circuiting
+ if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){
+ ret = c;
+ ret_set = true;
+ break;
+ }else if( n.getKind()==kind::ITE && i==0 ){
+ ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy );
+ ret_set = true;
+ break;
+ }
}
- Trace("term-db-eval") << "Child " << i << " : " << c << std::endl;
- //short-circuit and/or
- if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){
- ret = c;
- ret_set = true;
- break;
- }else{
- args.push_back( c );
- }
+ Trace("term-db-eval") << " child " << i << " : " << c << std::endl;
+ args.push_back( c );
}
if( !ret_set ){
+ //if it is an indexed term, return the congruent term
if( !f.isNull() ){
- Trace("term-db-eval") << "Get term from DB" << std::endl;
- TNode nn = d_func_map_trie[f].existsTerm( args );
- Trace("term-db-eval") << "Got term " << nn << std::endl;
- if( !nn.isNull() && qy->hasTerm( nn ) ){
- Trace("term-db-eval") << "return rep " << std::endl;
+ TNode nn = qy->getCongruentTerm( f, args );
+ Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl;
+ if( !nn.isNull() ){
ret = qy->getRepresentative( nn );
+ Trace("term-db-eval") << "return rep" << std::endl;
ret_set = true;
+ Assert( !ret.isNull() );
}
}
if( !ret_set ){
+ Trace("term-db-eval") << "return rewrite" << std::endl;
//a theory symbol or a new UF term
if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
args.insert( args.begin(), n.getOperator() );
}
}
}
+ }else{
+ Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
+ ret = qy->getRepresentative( n );
}
Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << std::endl;
visited[n] = ret;
}
-TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
+TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
Assert( !qy->extendsEngine() );
- Trace("term-db-eval") << "evaluate term : " << n << std::endl;
+ Trace("term-db-entail") << "get entailed term : " << n << std::endl;
if( qy->getEngine()->hasTerm( n ) ){
- Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
+ Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
return n;
}else if( n.getKind()==BOUND_VARIABLE ){
if( hasSubs ){
Assert( subs.find( n )!=subs.end() );
- Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
+ Trace("term-db-entail") << "...substitution is : " << subs[n] << std::endl;
if( subsRep ){
Assert( qy->getEngine()->hasTerm( subs[n] ) );
Assert( qy->getEngine()->getRepresentative( subs[n] )==subs[n] );
return subs[n];
}else{
- return evaluateTerm2( subs[n], subs, subsRep, hasSubs, qy );
+ return getEntailedTerm2( subs[n], subs, subsRep, hasSubs, qy );
+ }
+ }
+ }else if( n.getKind()==ITE ){
+ for( unsigned i=0; i<2; i++ ){
+ if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
+ return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy );
}
}
}else{
if( !f.isNull() ){
std::vector< TNode > args;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, qy );
+ TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy );
if( c.isNull() ){
return TNode::null();
}
c = qy->getEngine()->getRepresentative( c );
- Trace("term-db-eval") << "Got child : " << c << std::endl;
+ Trace("term-db-entail") << " child " << i << " : " << c << std::endl;
args.push_back( c );
}
- Trace("term-db-eval") << "Get term from DB" << std::endl;
- TNode nn = d_func_map_trie[f].existsTerm( args );
- Trace("term-db-eval") << "Got term " << nn << std::endl;
+ TNode nn = qy->getCongruentTerm( f, args );
+ Trace("term-db-entail") << " got congruent term " << nn << " for " << n << std::endl;
return nn;
}
}
return TNode::null();
}
-Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms, EqualityQuery * qy ) {
+Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy ) {
if( qy==NULL ){
qy = d_quantEngine->getEqualityQuery();
}
- if( mkNewTerms ){
- std::map< TNode, Node > visited;
- return evaluateTerm2( n, subs, subsRep, true, visited, qy );
- }else{
- return evaluateTerm2( n, subs, subsRep, true, qy );
+ std::map< TNode, Node > visited;
+ return evaluateTerm2( n, visited, qy );
+}
+
+TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) {
+ if( qy==NULL ){
+ qy = d_quantEngine->getEqualityQuery();
}
+ return getEntailedTerm2( n, subs, subsRep, true, qy );
}
-Node TermDb::evaluateTerm( TNode n, bool mkNewTerms, EqualityQuery * qy ) {
+TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) {
if( qy==NULL ){
qy = d_quantEngine->getEqualityQuery();
}
std::map< TNode, TNode > subs;
- if( mkNewTerms ){
- std::map< TNode, Node > visited;
- return evaluateTerm2( n, subs, false, false, visited, qy );
- }else{
- return evaluateTerm2( n, subs, false, false, qy );
- }
+ return getEntailedTerm2( n, subs, false, false, qy );
}
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
+bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
Assert( !qy->extendsEngine() );
- Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl;
+ Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
Assert( n.getType().isBoolean() );
if( n.getKind()==EQUAL ){
- TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs, qy );
+ TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
if( !n1.isNull() ){
- TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs, qy );
+ TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy );
if( !n2.isNull() ){
if( n1==n2 ){
return pol;
}
}
}else if( n.getKind()==NOT ){
- return isEntailed( n[0], subs, subsRep, hasSubs, !pol, qy );
+ return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy );
}else if( n.getKind()==OR || n.getKind()==AND ){
bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( isEntailed( n[i], subs, subsRep, hasSubs, pol, qy ) ){
+ if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){
if( simPol ){
return true;
}
return !simPol;
}else if( n.getKind()==IFF || n.getKind()==ITE ){
for( unsigned i=0; i<2; i++ ){
- if( isEntailed( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
+ if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
- return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol, qy );
+ return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy );
}
}
}else if( n.getKind()==APPLY_UF ){
- TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs, qy );
+ TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy );
if( !n1.isNull() ){
Assert( qy->hasTerm( n1 ) );
if( n1==d_true ){
return false;
}
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
+bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
if( qy==NULL ){
+ Assert( d_consistent_ee );
qy = d_quantEngine->getEqualityQuery();
}
- if( d_consistent_ee ){
- return isEntailed( n, subs, subsRep, true, pol, qy );
- }else{
- //don't check entailment wrt an inconsistent ee
- return false;
+ std::map< TNode, TNode > subs;
+ return isEntailed2( n, subs, false, false, pol, qy );
+}
+
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
+ if( qy==NULL ){
+ Assert( d_consistent_ee );
+ qy = d_quantEngine->getEqualityQuery();
}
+ return isEntailed2( n, subs, subsRep, true, pol, qy );
}
bool TermDb::hasTermCurrent( Node n, bool useMode ) {
}
}
}
-
+ //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
+ for( std::hash_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){
+ Node n = *it;
+ if( !ee->hasTerm( n ) ){
+ ee->addTerm( n );
+ }
+ }
//rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl;
for( unsigned i=0; i<it->second.size(); i++ ){
Node n = it->second[i];
- //to be added to term index, term must be relevant, and either exist in EE or be an inst closure term
- if( hasTermCurrent( n ) && ( ee->hasTerm( n ) || d_iclosure_processed.find( n )!=d_iclosure_processed.end() ) ){
+ //to be added to term index, term must be relevant, and exist in EE
+ if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
if( !n.getAttribute(NoMatchAttribute()) ){
if( options::finiteModelFind() ){
computeModelBasisArgAttribute( n );
}
}
-TNode TermDb::existsTerm( Node f, Node n ) {
+TNode TermDb::getCongruentTerm( Node f, Node n ) {
computeArgReps( n );
return d_func_map_trie[f].existsTerm( d_arg_reps[n] );
}
+TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+ return d_func_map_trie[f].existsTerm( args );
+}
+
Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
Node mbt;
class TermDbSygus;
-class TermDb {
+class TermDb : public QuantifiersUtil {
friend class ::CVC4::theory::QuantifiersEngine;
friend class ::CVC4::theory::inst::Trigger;
friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
/** set has term */
void setHasTerm( Node n );
/** evaluate term */
- TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
- Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy );
- bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
+ Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy );
+ TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+ bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
public:
TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
~TermDb(){}
void presolve();
/** reset (calculate which terms are active) */
bool reset( Theory::Effort effort );
+ /** identify */
+ std::string identify() const { return "TermDb"; }
/** get match operator */
Node getMatchOperator( Node n );
/** get term arg index */
TermArgTrie * getTermArgTrie( Node f );
TermArgTrie * getTermArgTrie( Node eqc, Node f );
/** exists term */
- TNode existsTerm( Node f, Node n );
+ TNode getCongruentTerm( Node f, Node n );
+ TNode getCongruentTerm( Node f, std::vector< TNode >& args );
/** compute arg reps */
void computeArgReps( TNode n );
/** compute uf eqc terms */
/** evaluate a term under a substitution. Return representative in EE if possible.
* subsRep is whether subs contains only representatives
*/
- Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false, EqualityQuery * qy = NULL );
- /** same as above, but without substitution */
- Node evaluateTerm( TNode n, bool mkNewTerms = false, EqualityQuery * qy = NULL );
+ Node evaluateTerm( TNode n, EqualityQuery * qy = NULL );
+ /** get entailed term, does not construct new terms, less aggressive */
+ TNode getEntailedTerm( TNode n, EqualityQuery * qy = NULL );
+ TNode getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy = NULL );
/** is entailed (incomplete check) */
+ bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL );
bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL );
/** has term */
bool hasTermCurrent( Node n, bool useMode = true );
#include "theory/quantifiers/quant_split.h"
#include "theory/quantifiers/anti_skolem.h"
#include "theory/quantifiers/equality_infer.h"
+#include "theory/quantifiers/inst_propagator.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
using namespace CVC4::theory;
using namespace CVC4::theory::inst;
-unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
- return QuantifiersEngine::QEFFORT_NONE;
-}
-
-eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
- return d_quantEngine->getMasterEqualityEngine();
-}
-
-bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
- eq::EqualityEngine * ee = getEqualityEngine();
- return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );
-}
-
-bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
- eq::EqualityEngine * ee = getEqualityEngine();
- return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );
-}
-
-TNode QuantifiersModule::getRepresentative( TNode n ) {
- eq::EqualityEngine * ee = getEqualityEngine();
- if( ee->hasTerm( n ) ){
- return ee->getRepresentative( n );
- }else{
- return n;
- }
-}
-
-quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
- return d_quantEngine->getTermDatabase();
-}
-
QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
d_te( te ),
d_lemmas_produced_c(u),
d_presolve_cache(u),
d_presolve_cache_wq(u),
d_presolve_cache_wic(u){
+ //utilities
d_eq_query = new EqualityQueryQuantifiersEngine( c, this );
+ d_util.push_back( d_eq_query );
+
d_term_db = new quantifiers::TermDb( c, u, this );
+ d_util.push_back( d_term_db );
+
+ if( options::instPropagate() ){
+ d_inst_prop = new quantifiers::InstPropagator( this );
+ d_util.push_back( d_inst_prop );
+ d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() );
+ }else{
+ d_inst_prop = NULL;
+ }
+
d_tr_trie = new inst::TriggerTrie;
d_hasAddedLemma = false;
//don't add true lemma
delete d_i_cbqi;
delete d_qsplit;
delete d_anti_skolem;
+ delete d_inst_prop;
}
EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
if( needsRelDom ){
d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
+ d_util.push_back( d_rel_dom );
}
if( needsBuilder ){
Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
if( needsCheck ){
+ //flush previous lemmas (for instance, if was interupted), or other lemmas to process
+ flushLemmas();
+ if( d_hasAddedLemma ){
+ return;
+ }
+
if( Trace.isOn("quant-engine-debug") ){
Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
Trace("quant-engine-debug") << " depth : " << d_ierCounter_c << std::endl;
Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl;
Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
}
-
- //reset relevant information
-
- //flush previous lemmas (for instance, if was interupted), or other lemmas to process
- flushLemmas();
- if( d_hasAddedLemma ){
- return;
- }
-
if( Trace.isOn("quant-engine-ee-pre") ){
Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
debugPrintEqualityEngine( "quant-engine-ee-pre" );
}
- Trace("quant-engine-debug2") << "Reset equality engine..." << std::endl;
- if( !d_eq_query->reset( e ) ){
- flushLemmas();
- return;
- }
-
if( Trace.isOn("quant-engine-assert") ){
Trace("quant-engine-assert") << "Assertions : " << std::endl;
getTheoryEngine()->printAssertions("quant-engine-assert");
}
+
+ //reset utilities
+ for( unsigned i=0; i<d_util.size(); i++ ){
+ Trace("quant-engine-debug2") << "Reset " << d_util[i]->identify().c_str() << "..." << std::endl;
+ if( !d_util[i]->reset( e ) ){
+ flushLemmas();
+ if( d_hasAddedLemma ){
+ return;
+ }else{
+ //should only fail reset if added a lemma
+ Assert( false );
+ }
+ }
+ }
+
if( Trace.isOn("quant-engine-ee") ){
Trace("quant-engine-ee") << "Equality engine : " << std::endl;
debugPrintEqualityEngine( "quant-engine-ee" );
}
-
- Trace("quant-engine-debug2") << "Reset term database..." << std::endl;
- if( !d_term_db->reset( e ) ){
- flushLemmas();
- return;
- }
- if( d_rel_dom ){
- d_rel_dom->reset();
- }
+
+ //reset the model
d_model->reset_round();
+ //reset the modules
for( unsigned i=0; i<d_modules.size(); i++ ){
Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
d_modules[i]->reset_round( e );
//check for positive entailment
if( options::instNoEntail() ){
+ //TODO: check consistency of equality engine (if not aborting on utility's reset)
std::map< TNode, TNode > subs;
for( unsigned i=0; i<terms.size(); i++ ){
subs[q[0][i]] = terms[i];
}
setInstantiationLevelAttr( body, q[1], maxInstLevel+1 );
}
- //notify listeners
- for( unsigned j=0; j<d_inst_notify.size(); j++ ){
- d_inst_notify[j]->notifyInstantiation( q, lem, terms, body );
+ if( d_curr_effort_level>QEFFORT_CONFLICT ){
+ //notify listeners
+ for( unsigned j=0; j<d_inst_notify.size(); j++ ){
+ d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body );
+ }
}
Trace("inst-add-debug") << " -> Success." << std::endl;
++(d_statistics.d_instantiations);
Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
}
+TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+ return d_qe->getTermDatabase()->getCongruentTerm( f, args );
+}
+
//helper functions
Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){
class TermDbSygus;
}
-class QuantifiersModule {
-protected:
- QuantifiersEngine* d_quantEngine;
-public:
- QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
- virtual ~QuantifiersModule(){}
- //get quantifiers engine
- QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
- /** presolve */
- virtual void presolve() {}
- /* whether this module needs to check this round */
- virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
- /* whether this module needs a model built */
- virtual unsigned needsModel( Theory::Effort e );
- /* reset at a round */
- virtual void reset_round( Theory::Effort e ){}
- /* Call during quantifier engine's check */
- virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
- /* check was complete (e.g. no lemmas implies a model) */
- virtual bool checkComplete() { return true; }
- /* Called for new quantified formulas */
- virtual void preRegisterQuantifier( Node q ) { }
- /* Called for new quantifiers after owners are finalized */
- virtual void registerQuantifier( Node q ) = 0;
- virtual void assertNode( Node n ) {}
- virtual void propagate( Theory::Effort level ){}
- virtual Node getNextDecisionRequest() { return TNode::null(); }
- /** Identify this module (for debugging, dynamic configuration, etc..) */
- virtual std::string identify() const = 0;
-public:
- eq::EqualityEngine * getEqualityEngine();
- bool areDisequal( TNode n1, TNode n2 );
- bool areEqual( TNode n1, TNode n2 );
- TNode getRepresentative( TNode n );
- quantifiers::TermDb * getTermDatabase();
-};/* class QuantifiersModule */
-
class InstantiationNotify {
public:
InstantiationNotify(){}
- virtual void notifyInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+ virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
};
namespace quantifiers {
class QuantDSplit;
class QuantAntiSkolem;
class EqualityInference;
+ class InstPropagator;
}/* CVC4::theory::quantifiers */
namespace inst {
private:
/** reference to theory engine object */
TheoryEngine* d_te;
+ /** vector of utilities for quantifiers */
+ std::vector< QuantifiersUtil* > d_util;
/** vector of modules for quantifiers */
std::vector< QuantifiersModule* > d_modules;
/** instantiation notify */
quantifiers::QuantDSplit * d_qsplit;
/** quantifiers anti-skolemization */
quantifiers::QuantAntiSkolem * d_anti_skolem;
+ /** quantifiers instantiation propagtor */
+ quantifiers::InstPropagator * d_inst_prop;
public: //effort levels
enum {
QEFFORT_CONFLICT,
Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
/** get score */
int getRepScore( Node n, Node f, int index, TypeNode v_tn );
+ /** flatten representatives */
+ void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
public:
EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
virtual ~EqualityQueryQuantifiersEngine();
/** reset */
bool reset( Theory::Effort e );
+ /** identify */
+ std::string identify() const { return "EqualityQueryQE"; }
/** general queries about equality */
bool hasTerm( Node a );
Node getRepresentative( Node a );
bool areDisequal( Node a, Node b );
eq::EqualityEngine* getEngine();
void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+ TNode getCongruentTerm( Node f, std::vector< TNode >& args );
/** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
If cbqi is active, this will return a term in the equivalence class of "a" that does
not contain instantiation constants, if such a term exists.
*/
Node getInternalRepresentative( Node a, Node f, int index );
- /** flatten representatives */
- void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
/** get quantifiers equality inference */
quantifiers::EqualityInference * getEqualityInference() { return d_eq_inference; }
}; /* EqualityQueryQuantifiersEngine */
projects / cvc5.git / commitdiff