inst_gen.h \
inst_gen.cpp \
quant_util.h \
- quant_util.cpp
+ quant_util.cpp \
+ inst_match_generator.h \
+ inst_match_generator.cpp
EXTRA_DIST = \
kinds \
namespace CVC4 {
namespace theory {
-struct ModelBasisAttributeId {};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-// 0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId {};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
-
class QuantifiersEngine;
namespace quantifiers{
**/
#include "theory/quantifiers/inst_match.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/candidate_generator.h"
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers_engine.h"
using namespace std;
using namespace CVC4;
}
}
-InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
- initializePattern( pat, qe );
-}
-
-InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
- if( pats.size()==1 ){
- initializePattern( pats[0], qe );
- }else{
- initializePatterns( pats, qe );
- }
-}
-
-void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){
- int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;
- for( int i=0; i<(int)pats.size(); i++ ){
- d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) );
- }
- d_pattern = Node::null();
- d_match_pattern = Node::null();
- d_cg = NULL;
-}
-
-void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
- Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
- Assert( pat.hasAttribute(InstConstantAttribute()) );
- d_pattern = pat;
- d_match_pattern = pat;
- if( d_match_pattern.getKind()==NOT ){
- //we want to add the children of the NOT
- d_match_pattern = d_pattern[0];
- }
- if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){
- if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){
- Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );
- //swap sides
- d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
- d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;
- if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching
- d_match_pattern = d_match_pattern[1];
- }else{
- d_match_pattern = d_pattern[0][0];
- }
- }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){
- Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );
- if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching
- d_match_pattern = d_match_pattern[0];
- }
- }
- }
- int childMatchPolicy = MATCH_GEN_DEFAULT;
- for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
- if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
- if( d_match_pattern[i].getKind()!=INST_CONSTANT ){
- d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) );
- d_children_index.push_back( i );
- }
- }
- }
-
- Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
-
- //create candidate generator
- if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
- Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
- //we will be producing candidates via literal matching heuristics
- if( d_pattern.getKind()!=NOT ){
- //candidates will be all equalities
- d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );
- }else{
- //candidates will be all disequalities
- d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
- }
- }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){
- Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
- if( d_pattern.getKind()==NOT ){
- Unimplemented("Disequal generator unimplemented");
- }else{
- Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
- //we are matching only in a particular equivalence class
- d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
- //store the equivalence class that we will call d_cg->reset( ... ) on
- d_eq_class = d_pattern[1];
- }
- }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
- //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){
- //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;
- //}
- //we will be scanning lists trying to find d_match_pattern.getOperator()
- d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
- }else{
- d_cg = new CandidateGeneratorQueue;
- if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
- Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
- Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
- d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
- }else{
- Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;
- for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
- Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl;
- }
- //we will treat this as match gen internal arithmetic
- d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC;
- }
- }
-}
-
-/** get match (not modulo equality) */
-bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){
- Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
- << m.size() << ")" << ", " << d_children.size() << std::endl;
- Assert( !d_match_pattern.isNull() );
- if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){
- return true;
- }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){
- return getMatchArithmetic( t, m, qe );
- }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){
- return false;
- }else{
- EqualityQuery* q = qe->getEqualityQuery();
- //add m to partial match vector
- std::vector< InstMatch > partial;
- partial.push_back( InstMatch( &m ) );
- //if t is null
- Assert( !t.isNull() );
- Assert( !t.hasAttribute(InstConstantAttribute()) );
- Assert( t.getKind()==d_match_pattern.getKind() );
- Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
- //first, check if ground arguments are not equal, or a match is in conflict
- for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
- if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
- if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){
- //match is in conflict
- Debug("matching-debug") << "Match in conflict " << t[i] << " and "
- << d_match_pattern[i] << " because "
- << partial[0].get(d_match_pattern[i])
- << std::endl;
- Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl;
- return false;
- }
- }
- }else{
- if( !q->areEqual( d_match_pattern[i], t[i] ) ){
- Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
- //ground arguments are not equal
- return false;
- }
- }
- }
- //now, fit children into match
- //we will be requesting candidates for matching terms for each child
- std::vector< Node > reps;
- for( int i=0; i<(int)d_children.size(); i++ ){
- Node rep = q->getRepresentative( t[ d_children_index[i] ] );
- reps.push_back( rep );
- d_children[i]->d_cg->reset( rep );
- }
-
- //combine child matches
- int index = 0;
- while( index>=0 && index<(int)d_children.size() ){
- partial.push_back( InstMatch( &partial[index] ) );
- if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){
- index++;
- }else{
- d_children[index]->d_cg->reset( reps[index] );
- partial.pop_back();
- if( !partial.empty() ){
- partial.pop_back();
- }
- index--;
- }
- }
- if( index>=0 ){
- m = partial.back();
- return true;
- }else{
- return false;
- }
- }
-}
-
-bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){
- bool success = false;
- Node t;
- do{
- //get the next candidate term t
- t = d_cg->getNextCandidate();
- //if t not null, try to fit it into match m
- if( !t.isNull() && t.getType()==d_match_pattern.getType() ){
- success = getMatch( t, m, qe );
- }
- }while( !success && !t.isNull() );
- if (saveMatched) m.d_matched = t;
- return success;
-}
-
-bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){
- Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl;
- if( !d_arith_coeffs.empty() ){
- NodeBuilder<> tb(kind::PLUS);
- Node ic = Node::null();
- for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
- Debug("matching-arith") << it->first << " -> " << it->second << std::endl;
- if( !it->first.isNull() ){
- if( m.find( it->first )==m.end() ){
- //see if we can choose this to set
- if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){
- ic = it->first;
- }
- }else{
- Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl;
- Node tm = m.get( it->first );
- if( !it->second.isNull() ){
- tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm );
- }
- tb << tm;
- }
- }else{
- tb << it->second;
- }
- }
- if( !ic.isNull() ){
- Node tm;
- if( tb.getNumChildren()==0 ){
- tm = t;
- }else{
- tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
- tm = NodeManager::currentNM()->mkNode( MINUS, t, tm );
- }
- if( !d_arith_coeffs[ ic ].isNull() ){
- Assert( !ic.getType().isInteger() );
- Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() );
- tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm );
- }
- m.set( ic, Rewriter::rewrite( tm ));
- //set the rest to zeros
- for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
- if( !it->first.isNull() ){
- if( m.find( it->first )==m.end() ){
- m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) );
- }
- }
- }
- Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;
- return true;
- }else{
- return false;
- }
- }else{
- return false;
- }
-}
-
-
-/** reset instantiation round */
-void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
- if( d_match_pattern.isNull() ){
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->resetInstantiationRound( qe );
- }
- }else{
- if( d_cg ){
- d_cg->resetInstantiationRound();
- }
- }
-}
-
-void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
- if( d_match_pattern.isNull() ){
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->reset( eqc, qe );
- }
- d_partial.clear();
- }else{
- if( !d_eq_class.isNull() ){
- //we have a specific equivalence class in mind
- //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
- //just look in equivalence class of the RHS
- d_cg->reset( d_eq_class );
- }else{
- d_cg->reset( eqc );
- }
- }
-}
-
-bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
- m.d_matched = Node::null();
- if( d_match_pattern.isNull() ){
- int index = (int)d_partial.size();
- while( index>=0 && index<(int)d_children.size() ){
- if( index>0 ){
- d_partial.push_back( InstMatch( &d_partial[index-1] ) );
- }else{
- d_partial.push_back( InstMatch() );
- }
- if( d_children[index]->getNextMatch( d_partial[index], qe ) ){
- index++;
- }else{
- d_children[index]->reset( Node::null(), qe );
- d_partial.pop_back();
- if( !d_partial.empty() ){
- d_partial.pop_back();
- }
- index--;
- }
- }
- if( index>=0 ){
- m = d_partial.back();
- d_partial.pop_back();
- return true;
- }else{
- return false;
- }
- }else{
- bool res = getNextMatch2( m, qe, true );
- Assert(!res || !m.d_matched.isNull());
- return res;
- }
-}
-
-
-
-// Currently the implementation doesn't take into account that
-// variable should have the same value given.
-// TODO use the d_children way perhaps
-// TODO replace by a real dictionnary
-// We should create a real substitution? slower more precise
-// We don't do that often
-bool InstMatchGenerator::nonunifiable( TNode t0, const std::vector<Node> & vars){
- if(d_match_pattern.isNull()) return true;
-
- typedef std::vector<std::pair<TNode,TNode> > tstack;
- tstack stack(1,std::make_pair(t0,d_match_pattern)); // t * pat
-
- while(!stack.empty()){
- const std::pair<TNode,TNode> p = stack.back(); stack.pop_back();
- const TNode & t = p.first;
- const TNode & pat = p.second;
-
- // t or pat is a variable currently we consider that can match anything
- if( find(vars.begin(),vars.end(),t) != vars.end() ) continue;
- if( pat.getKind() == INST_CONSTANT ) continue;
-
- // t and pat are nonunifiable
- if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) {
- if(t == pat) continue;
- else return true;
- };
- if( t.getOperator() != pat.getOperator() ) return true;
-
- //put the children on the stack
- for( size_t i=0; i < pat.getNumChildren(); i++ ){
- stack.push_back(std::make_pair(t[i],pat[i]));
- };
- }
- // The heuristic can't find non-unifiability
- return false;
-}
-
-int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
- //now, try to add instantiation for each match produced
- int addedLemmas = 0;
- InstMatch m;
- while( getNextMatch( m, qe ) ){
- //m.makeInternal( d_quantEngine->getEqualityQuery() );
- m.add( baseMatch );
- if( qe->addInstantiation( f, m ) ){
- addedLemmas++;
- if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){
- return addedLemmas;
- }
- }
- m.clear();
- }
- //return number of lemmas added
- return addedLemmas;
-}
-
-int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
- Assert( options::eagerInstQuant() );
- if( !d_match_pattern.isNull() ){
- InstMatch m;
- if( getMatch( t, m, qe ) ){
- if( qe->addInstantiation( f, m ) ){
- return 1;
- }
- }
- }else{
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->addTerm( f, t, qe );
- }
- }
- return 0;
-}
-
-/** constructors */
-InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :
-d_f( f ){
- Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;
- std::map< Node, std::vector< Node > > var_contains;
- qe->getTermDatabase()->getVarContains( f, pats, var_contains );
- //convert to indicies
- for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
- Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
- for( int i=0; i<(int)it->second.size(); i++ ){
- Debug("smart-multi-trigger") << it->second[i] << " ";
- int index = it->second[i].getAttribute(InstVarNumAttribute());
- d_var_contains[ it->first ].push_back( index );
- d_var_to_node[ index ].push_back( it->first );
- }
- Debug("smart-multi-trigger") << std::endl;
- }
- for( int i=0; i<(int)pats.size(); i++ ){
- Node n = pats[i];
- //make the match generator
- d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) );
- //compute unique/shared variables
- std::vector< int > unique_vars;
- std::map< int, bool > shared_vars;
- int numSharedVars = 0;
- for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
- if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
- Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
- unique_vars.push_back( d_var_contains[n][j] );
- }else{
- shared_vars[ d_var_contains[n][j] ] = true;
- numSharedVars++;
- }
- }
- //we use the latest shared variables, then unique variables
- std::vector< int > vars;
- int index = i==0 ? (int)(pats.size()-1) : (i-1);
- while( numSharedVars>0 && index!=i ){
- for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
- if( it->second ){
- if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=
- d_var_contains[ pats[index] ].end() ){
- vars.push_back( it->first );
- shared_vars[ it->first ] = false;
- numSharedVars--;
- }
- }
- }
- index = index==0 ? (int)(pats.size()-1) : (index-1);
- }
- vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
- Debug("smart-multi-trigger") << " Index[" << i << "]: ";
- for( int i=0; i<(int)vars.size(); i++ ){
- Debug("smart-multi-trigger") << vars[i] << " ";
- }
- Debug("smart-multi-trigger") << std::endl;
- //make ordered inst match trie
- InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;
- imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );
- d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );
- }
-
-}
-
-/** reset instantiation round (call this whenever equivalence classes have changed) */
-void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->resetInstantiationRound( qe );
- }
-}
-
-/** reset, eqc is the equivalence class to search in (any if eqc=null) */
-void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->reset( eqc, qe );
- }
-}
-
-int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
- int addedLemmas = 0;
- Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
- for( int i=0; i<(int)d_children.size(); i++ ){
- Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
- std::vector< InstMatch > newMatches;
- InstMatch m;
- while( d_children[i]->getNextMatch( m, qe ) ){
- m.makeRepresentative( qe );
- newMatches.push_back( InstMatch( &m ) );
- m.clear();
- }
- for( int j=0; j<(int)newMatches.size(); j++ ){
- processNewMatch( qe, newMatches[j], i, addedLemmas );
- }
- }
- return addedLemmas;
-}
-
-void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){
- //see if these produce new matches
- d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true );
- //possibly only do the following if we know that new matches will be produced?
- //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
- // we can safely skip the following lines, even when we have already produced this match.
- Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;
- //process new instantiations
- int childIndex = (fromChildIndex+1)%(int)d_children.size();
- std::vector< IndexedTrie > unique_var_tries;
- processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),
- unique_var_tries, 0, childIndex, fromChildIndex, true );
-}
-
-void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
- std::vector< IndexedTrie >& unique_var_tries,
- int trieIndex, int childIndex, int endChildIndex, bool modEq ){
- if( childIndex==endChildIndex ){
- //now, process unique variables
- processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
- }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
- int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
- if( m.find( curr_ic )==m.end() ){
- //if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME
- // //unique variable(s), defer calculation
- // unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );
- // int newChildIndex = (childIndex+1)%(int)d_children.size();
- // processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
- // 0, newChildIndex, endChildIndex, modEq );
- //}else{
- //shared and non-set variable, add to InstMatch
- for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
- InstMatch mn( &m );
- mn.set( curr_ic, it->first);
- processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
- }
- //}
- }else{
- //shared and set variable, try to merge
- Node n = m.get( curr_ic );
- std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n );
- if( it!=tr->d_data.end() ){
- processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
- }
- if( modEq ){
- //check modulo equality for other possible instantiations
- if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
- qe->getEqualityQuery()->getEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( en!=n ){
- std::map< Node, InstMatchTrie >::iterator itc = tr->d_data.find( en );
- if( itc!=tr->d_data.end() ){
- processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
- }
- }
- ++eqc;
- }
- }
- }
- }
- }else{
- int newChildIndex = (childIndex+1)%(int)d_children.size();
- processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
- 0, newChildIndex, endChildIndex, modEq );
- }
-}
-
-void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
- std::vector< IndexedTrie >& unique_var_tries,
- int uvtIndex, InstMatchTrie* tr, int trieIndex ){
- if( uvtIndex<(int)unique_var_tries.size() ){
- int childIndex = unique_var_tries[uvtIndex].first.first;
- if( !tr ){
- tr = unique_var_tries[uvtIndex].second;
- trieIndex = unique_var_tries[uvtIndex].first.second;
- }
- if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
- int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
- //unique non-set variable, add to InstMatch
- for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
- InstMatch mn( &m );
- mn.set( curr_ic, it->first);
- processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
- }
- }else{
- processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
- }
- }else{
- //m is an instantiation
- if( qe->addInstantiation( d_f, m ) ){
- addedLemmas++;
- Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
- }
- }
-}
-
-int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
- Assert( options::eagerInstQuant() );
- int addedLemmas = 0;
- for( int i=0; i<(int)d_children.size(); i++ ){
- if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){
- InstMatch m;
- //if it produces a match, then process it with the rest
- if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){
- processNewMatch( qe, m, i, addedLemmas );
- }
- }
- }
- return addedLemmas;
-}
-
-int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
- InstMatch m;
- m.add( baseMatch );
- int addedLemmas = 0;
- if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){
- for( int i=0; i<2; i++ ){
- addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) );
- }
- }else{
- addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );
- }
- return addedLemmas;
-}
-
-void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
- if( argIndex==(int)d_match_pattern.getNumChildren() ){
- //m is an instantiation
- if( qe->addInstantiation( d_f, m ) ){
- addedLemmas++;
- Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;
- }
- }else{
- if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
- Node ic = d_match_pattern[argIndex];
- for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
- Node t = it->first;
- if( m.get( ic ).isNull() || m.get( ic )==t ){
- Node prev = m.get( ic );
- m.set( ic, t);
- addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
- m.set( ic, prev);
- }
- }
- }else{
- Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
- std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
- if( it!=tat->d_data.end() ){
- addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
- }
- }
- }
-}
-
-int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
- Assert( options::eagerInstQuant() );
- InstMatch m;
- for( int i=0; i<(int)t.getNumChildren(); i++ ){
- if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- m.set(d_match_pattern[i], t[i]);
- }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){
- return 0;
- }
- }
- return qe->addInstantiation( f, m ) ? 1 : 0;
-}
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
#include "util/hash.h"
#include <ext/hash_set>
-#include <iostream>
#include <map>
#include "context/cdlist.h"
-#include "theory/quantifiers/candidate_generator.h"
-
-//#define USE_EFFICIENT_E_MATCHING
+#include "expr/node.h"
namespace CVC4 {
namespace theory {
-/** Attribute true for nodes that should not be used for matching */
-struct NoMatchAttributeId {};
-/** use the special for boolean flag */
-typedef expr::Attribute< NoMatchAttributeId,
- bool,
- expr::attr::NullCleanupStrategy,
- true // context dependent
- > NoMatchAttribute;
-
-// attribute for "contains instantiation constants from"
-struct InstConstantAttributeId {};
-typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
-
-struct InstLevelAttributeId {};
-typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
-
-struct InstVarNumAttributeId {};
-typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
-
-// Attribute that tell if a node have been asserted in this branch
-struct AvailableInTermDbId {};
-/** use the special for boolean flag */
-typedef expr::Attribute<AvailableInTermDbId,
- bool,
- expr::attr::NullCleanupStrategy,
- true // context dependent
- > AvailableInTermDb;
-
-
class QuantifiersEngine;
-namespace quantifiers{
- class TermArgTrie;
-}
-
-namespace uf{
- class InstantiatorTheoryUf;
- class TheoryUF;
-}/* CVC4::theory::uf namespace */
+class EqualityQuery;
namespace inst {
-class EqualityQuery {
-public:
- EqualityQuery(){}
- virtual ~EqualityQuery(){};
- /** contains term */
- virtual bool hasTerm( Node a ) = 0;
- /** get the representative of the equivalence class of a */
- virtual Node getRepresentative( Node a ) = 0;
- /** returns true if a and b are equal in the current context */
- virtual bool areEqual( Node a, Node b ) = 0;
- /** returns true is a and b are disequal in the current context */
- virtual bool areDisequal( Node a, Node b ) = 0;
- /** 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.
- */
- virtual Node getInternalRepresentative( Node a ) = 0;
- /** get the equality engine associated with this query */
- virtual eq::EqualityEngine* getEngine() = 0;
- /** get the equivalence class of a */
- virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
-};/* class EqualityQuery */
-
/** basic class defining an instantiation */
class InstMatch {
/* map from variable to ground terms */
}
};/* class InstMatchTrieOrdered */
-/** base class for producing InstMatch objects */
-class IMGenerator {
-public:
- /** reset instantiation round (call this at beginning of instantiation round) */
- virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
- /** get the next match. must call reset( eqc ) before this function. */
- virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
- /** return true if whatever Node is substituted for the variables the
- given Node can't match the pattern */
- virtual bool nonunifiable( TNode t, const std::vector<Node> & vars) = 0;
- /** add instantiations directly */
- virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
- /** add ground term t, called when t is added to term db */
- virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;
-};/* class IMGenerator */
-
-
-class InstMatchGenerator : public IMGenerator {
-private:
- /** candidate generator */
- CandidateGenerator* d_cg;
- /** policy to use for matching */
- int d_matchPolicy;
- /** children generators */
- std::vector< InstMatchGenerator* > d_children;
- std::vector< int > d_children_index;
- /** partial vector */
- std::vector< InstMatch > d_partial;
- /** eq class */
- Node d_eq_class;
- /** for arithmetic matching */
- std::map< Node, Node > d_arith_coeffs;
- /** initialize pattern */
- void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe );
- void initializePattern( Node pat, QuantifiersEngine* qe );
-public:
- enum {
- //options for producing matches
- MATCH_GEN_DEFAULT = 0,
- MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers
- //others (internally used)
- MATCH_GEN_INTERNAL_ARITHMETIC,
- MATCH_GEN_INTERNAL_ERROR,
- };
-private:
- /** get the next match. must call d_cg->reset( ... ) before using.
- only valid for use where !d_match_pattern.isNull().
- */
- bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );
- /** for arithmetic */
- bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
-public:
- /** get the match against ground term or formula t.
- d_match_pattern and t should have the same shape.
- only valid for use where !d_match_pattern.isNull().
- */
- bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );
-
- /** constructors */
- InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );
- InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
- /** destructor */
- ~InstMatchGenerator(){}
- /** The pattern we are producing matches for.
- If null, this is a multi trigger that is merging matches from d_children.
- */
- Node d_pattern;
- /** match pattern */
- Node d_match_pattern;
-public:
- /** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe );
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- void reset( Node eqc, QuantifiersEngine* qe );
- /** get the next match. must call reset( eqc ) before this function. */
- bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
- /** return true if whatever Node is substituted for the variables the
- given Node can't match the pattern */
- bool nonunifiable( TNode t, const std::vector<Node> & vars);
- /** add instantiations */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** add ground term t */
- int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGenerator */
-
-/** smart multi-trigger implementation */
-class InstMatchGeneratorMulti : public IMGenerator {
-private:
- /** indexed trie */
- typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
- /** process new match */
- void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
- /** process new instantiations */
- void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
- std::vector< IndexedTrie >& unique_var_tries,
- int trieIndex, int childIndex, int endChildIndex, bool modEq );
- /** process new instantiations 2 */
- void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
- std::vector< IndexedTrie >& unique_var_tries,
- int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
-private:
- /** var contains (variable indices) for each pattern node */
- std::map< Node, std::vector< int > > d_var_contains;
- /** variable indices contained to pattern nodes */
- std::map< int, std::vector< Node > > d_var_to_node;
- /** quantifier to use */
- Node d_f;
- /** policy to use for matching */
- int d_matchPolicy;
- /** children generators */
- std::vector< InstMatchGenerator* > d_children;
- /** inst match tries for each child */
- std::vector< InstMatchTrieOrdered > d_children_trie;
- /** calculate matches */
- void calculateMatches( QuantifiersEngine* qe );
-public:
- /** constructors */
- InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
- /** destructor */
- ~InstMatchGeneratorMulti(){}
- /** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe );
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- void reset( Node eqc, QuantifiersEngine* qe );
- /** get the next match. must call reset( eqc ) before this function. (not implemented) */
- bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
- /** return true if whatever Node is substituted for the variables the
- given Node can't match the pattern */
- bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
- /** add instantiations */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** add ground term t */
- int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorMulti */
-
-/** smart (single)-trigger implementation */
-class InstMatchGeneratorSimple : public IMGenerator {
-private:
- /** quantifier for match term */
- Node d_f;
- /** match term */
- Node d_match_pattern;
- /** add instantiations */
- void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
-public:
- /** constructors */
- InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}
- /** destructor */
- ~InstMatchGeneratorSimple(){}
- /** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe ) {}
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- void reset( Node eqc, QuantifiersEngine* qe ) {}
- /** get the next match. must call reset( eqc ) before this function. (not implemented) */
- bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
- /** return true if whatever Node is substituted for the variables the
- given Node can't match the pattern */
- bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
- /** add instantiations */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** add ground term t, possibly add instantiations */
- int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorSimple */
-
}/* CVC4::theory::inst namespace */
typedef CVC4::theory::inst::InstMatch InstMatch;
-typedef CVC4::theory::inst::EqualityQuery EqualityQuery;
}/* CVC4::theory namespace */
}/* CVC4 namespace */
--- /dev/null
+/********************* */\r
+/*! \file inst_match_generator.cpp\r
+** \verbatim\r
+** Original author: ajreynol\r
+** Major contributors: bobot\r
+** Minor contributors (to current version): barrett, mdeters\r
+** This file is part of the CVC4 prototype.\r
+** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+** See the file COPYING in the top-level source directory for licensing\r
+** information.\endverbatim\r
+**\r
+** \brief Implementation of inst match generator class\r
+**/\r
+\r
+#include "theory/quantifiers/inst_match_generator.h"\r
+#include "theory/quantifiers/trigger.h"\r
+#include "theory/quantifiers/term_database.h"\r
+#include "theory/quantifiers/candidate_generator.h"\r
+#include "theory/quantifiers_engine.h"\r
+\r
+using namespace std;\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::context;\r
+using namespace CVC4::theory;\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace inst {\r
+\r
+\r
+InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){\r
+ initializePattern( pat, qe );\r
+}\r
+\r
+InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){\r
+ if( pats.size()==1 ){\r
+ initializePattern( pats[0], qe );\r
+ }else{\r
+ initializePatterns( pats, qe );\r
+ }\r
+}\r
+\r
+void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){\r
+ int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;\r
+ for( int i=0; i<(int)pats.size(); i++ ){\r
+ d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) );\r
+ }\r
+ d_pattern = Node::null();\r
+ d_match_pattern = Node::null();\r
+ d_cg = NULL;\r
+}\r
+\r
+void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){\r
+ Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;\r
+ Assert( pat.hasAttribute(InstConstantAttribute()) );\r
+ d_pattern = pat;\r
+ d_match_pattern = pat;\r
+ if( d_match_pattern.getKind()==NOT ){\r
+ //we want to add the children of the NOT\r
+ d_match_pattern = d_pattern[0];\r
+ }\r
+ if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){\r
+ if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){\r
+ Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );\r
+ //swap sides\r
+ d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );\r
+ d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;\r
+ if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching\r
+ d_match_pattern = d_match_pattern[1];\r
+ }else{\r
+ d_match_pattern = d_pattern[0][0];\r
+ }\r
+ }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){\r
+ Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );\r
+ if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching\r
+ d_match_pattern = d_match_pattern[0];\r
+ }\r
+ }\r
+ }\r
+ int childMatchPolicy = MATCH_GEN_DEFAULT;\r
+ for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){\r
+ if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){\r
+ if( d_match_pattern[i].getKind()!=INST_CONSTANT ){\r
+ d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) );\r
+ d_children_index.push_back( i );\r
+ }\r
+ }\r
+ }\r
+\r
+ Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;\r
+\r
+ //create candidate generator\r
+ if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){\r
+ Assert( d_matchPolicy==MATCH_GEN_DEFAULT );\r
+ //we will be producing candidates via literal matching heuristics\r
+ if( d_pattern.getKind()!=NOT ){\r
+ //candidates will be all equalities\r
+ d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );\r
+ }else{\r
+ //candidates will be all disequalities\r
+ d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );\r
+ }\r
+ }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){\r
+ Assert( d_matchPolicy==MATCH_GEN_DEFAULT );\r
+ if( d_pattern.getKind()==NOT ){\r
+ Unimplemented("Disequal generator unimplemented");\r
+ }else{\r
+ Assert( Trigger::isAtomicTrigger( d_match_pattern ) );\r
+ //we are matching only in a particular equivalence class\r
+ d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );\r
+ //store the equivalence class that we will call d_cg->reset( ... ) on\r
+ d_eq_class = d_pattern[1];\r
+ }\r
+ }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){\r
+ //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){\r
+ //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;\r
+ //}\r
+ //we will be scanning lists trying to find d_match_pattern.getOperator()\r
+ d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );\r
+ }else{\r
+ d_cg = new CandidateGeneratorQueue;\r
+ if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){\r
+ Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;\r
+ Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;\r
+ d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;\r
+ }else{\r
+ Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;\r
+ for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){\r
+ Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl;\r
+ }\r
+ //we will treat this as match gen internal arithmetic\r
+ d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC;\r
+ }\r
+ }\r
+}\r
+\r
+/** get match (not modulo equality) */\r
+bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){\r
+ Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("\r
+ << m.size() << ")" << ", " << d_children.size() << std::endl;\r
+ Assert( !d_match_pattern.isNull() );\r
+ if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){\r
+ return true;\r
+ }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){\r
+ return getMatchArithmetic( t, m, qe );\r
+ }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){\r
+ return false;\r
+ }else{\r
+ EqualityQuery* q = qe->getEqualityQuery();\r
+ //add m to partial match vector\r
+ std::vector< InstMatch > partial;\r
+ partial.push_back( InstMatch( &m ) );\r
+ //if t is null\r
+ Assert( !t.isNull() );\r
+ Assert( !t.hasAttribute(InstConstantAttribute()) );\r
+ Assert( t.getKind()==d_match_pattern.getKind() );\r
+ Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );\r
+ //first, check if ground arguments are not equal, or a match is in conflict\r
+ for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){\r
+ if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){\r
+ if( d_match_pattern[i].getKind()==INST_CONSTANT ){\r
+ if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){\r
+ //match is in conflict\r
+ Debug("matching-debug") << "Match in conflict " << t[i] << " and "\r
+ << d_match_pattern[i] << " because "\r
+ << partial[0].get(d_match_pattern[i])\r
+ << std::endl;\r
+ Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl;\r
+ return false;\r
+ }\r
+ }\r
+ }else{\r
+ if( !q->areEqual( d_match_pattern[i], t[i] ) ){\r
+ Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;\r
+ //ground arguments are not equal\r
+ return false;\r
+ }\r
+ }\r
+ }\r
+ //now, fit children into match\r
+ //we will be requesting candidates for matching terms for each child\r
+ std::vector< Node > reps;\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ Node rep = q->getRepresentative( t[ d_children_index[i] ] );\r
+ reps.push_back( rep );\r
+ d_children[i]->d_cg->reset( rep );\r
+ }\r
+\r
+ //combine child matches\r
+ int index = 0;\r
+ while( index>=0 && index<(int)d_children.size() ){\r
+ partial.push_back( InstMatch( &partial[index] ) );\r
+ if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){\r
+ index++;\r
+ }else{\r
+ d_children[index]->d_cg->reset( reps[index] );\r
+ partial.pop_back();\r
+ if( !partial.empty() ){\r
+ partial.pop_back();\r
+ }\r
+ index--;\r
+ }\r
+ }\r
+ if( index>=0 ){\r
+ m = partial.back();\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+ }\r
+}\r
+\r
+bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){\r
+ bool success = false;\r
+ Node t;\r
+ do{\r
+ //get the next candidate term t\r
+ t = d_cg->getNextCandidate();\r
+ //if t not null, try to fit it into match m\r
+ if( !t.isNull() && t.getType()==d_match_pattern.getType() ){\r
+ success = getMatch( t, m, qe );\r
+ }\r
+ }while( !success && !t.isNull() );\r
+ if (saveMatched) m.d_matched = t;\r
+ return success;\r
+}\r
+\r
+bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){\r
+ Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl;\r
+ if( !d_arith_coeffs.empty() ){\r
+ NodeBuilder<> tb(kind::PLUS);\r
+ Node ic = Node::null();\r
+ for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){\r
+ Debug("matching-arith") << it->first << " -> " << it->second << std::endl;\r
+ if( !it->first.isNull() ){\r
+ if( m.find( it->first )==m.end() ){\r
+ //see if we can choose this to set\r
+ if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){\r
+ ic = it->first;\r
+ }\r
+ }else{\r
+ Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl;\r
+ Node tm = m.get( it->first );\r
+ if( !it->second.isNull() ){\r
+ tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm );\r
+ }\r
+ tb << tm;\r
+ }\r
+ }else{\r
+ tb << it->second;\r
+ }\r
+ }\r
+ if( !ic.isNull() ){\r
+ Node tm;\r
+ if( tb.getNumChildren()==0 ){\r
+ tm = t;\r
+ }else{\r
+ tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;\r
+ tm = NodeManager::currentNM()->mkNode( MINUS, t, tm );\r
+ }\r
+ if( !d_arith_coeffs[ ic ].isNull() ){\r
+ Assert( !ic.getType().isInteger() );\r
+ Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() );\r
+ tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm );\r
+ }\r
+ m.set( ic, Rewriter::rewrite( tm ));\r
+ //set the rest to zeros\r
+ for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){\r
+ if( !it->first.isNull() ){\r
+ if( m.find( it->first )==m.end() ){\r
+ m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) );\r
+ }\r
+ }\r
+ }\r
+ Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+\r
+/** reset instantiation round */\r
+void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){\r
+ if( d_match_pattern.isNull() ){\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ d_children[i]->resetInstantiationRound( qe );\r
+ }\r
+ }else{\r
+ if( d_cg ){\r
+ d_cg->resetInstantiationRound();\r
+ }\r
+ }\r
+}\r
+\r
+void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){\r
+ if( d_match_pattern.isNull() ){\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ d_children[i]->reset( eqc, qe );\r
+ }\r
+ d_partial.clear();\r
+ }else{\r
+ if( !d_eq_class.isNull() ){\r
+ //we have a specific equivalence class in mind\r
+ //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term\r
+ //just look in equivalence class of the RHS\r
+ d_cg->reset( d_eq_class );\r
+ }else{\r
+ d_cg->reset( eqc );\r
+ }\r
+ }\r
+}\r
+\r
+bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){\r
+ m.d_matched = Node::null();\r
+ if( d_match_pattern.isNull() ){\r
+ int index = (int)d_partial.size();\r
+ while( index>=0 && index<(int)d_children.size() ){\r
+ if( index>0 ){\r
+ d_partial.push_back( InstMatch( &d_partial[index-1] ) );\r
+ }else{\r
+ d_partial.push_back( InstMatch() );\r
+ }\r
+ if( d_children[index]->getNextMatch( d_partial[index], qe ) ){\r
+ index++;\r
+ }else{\r
+ d_children[index]->reset( Node::null(), qe );\r
+ d_partial.pop_back();\r
+ if( !d_partial.empty() ){\r
+ d_partial.pop_back();\r
+ }\r
+ index--;\r
+ }\r
+ }\r
+ if( index>=0 ){\r
+ m = d_partial.back();\r
+ d_partial.pop_back();\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+ }else{\r
+ bool res = getNextMatch2( m, qe, true );\r
+ Assert(!res || !m.d_matched.isNull());\r
+ return res;\r
+ }\r
+}\r
+\r
+\r
+\r
+int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){\r
+ //now, try to add instantiation for each match produced\r
+ int addedLemmas = 0;\r
+ InstMatch m;\r
+ while( getNextMatch( m, qe ) ){\r
+ //m.makeInternal( d_quantEngine->getEqualityQuery() );\r
+ m.add( baseMatch );\r
+ if( qe->addInstantiation( f, m ) ){\r
+ addedLemmas++;\r
+ if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){\r
+ return addedLemmas;\r
+ }\r
+ }\r
+ m.clear();\r
+ }\r
+ //return number of lemmas added\r
+ return addedLemmas;\r
+}\r
+\r
+int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){\r
+ Assert( options::eagerInstQuant() );\r
+ if( !d_match_pattern.isNull() ){\r
+ InstMatch m;\r
+ if( getMatch( t, m, qe ) ){\r
+ if( qe->addInstantiation( f, m ) ){\r
+ return 1;\r
+ }\r
+ }\r
+ }else{\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ d_children[i]->addTerm( f, t, qe );\r
+ }\r
+ }\r
+ return 0;\r
+}\r
+\r
+/** constructors */\r
+InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :\r
+d_f( f ){\r
+ Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;\r
+ std::map< Node, std::vector< Node > > var_contains;\r
+ qe->getTermDatabase()->getVarContains( f, pats, var_contains );\r
+ //convert to indicies\r
+ for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){\r
+ Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";\r
+ for( int i=0; i<(int)it->second.size(); i++ ){\r
+ Debug("smart-multi-trigger") << it->second[i] << " ";\r
+ int index = it->second[i].getAttribute(InstVarNumAttribute());\r
+ d_var_contains[ it->first ].push_back( index );\r
+ d_var_to_node[ index ].push_back( it->first );\r
+ }\r
+ Debug("smart-multi-trigger") << std::endl;\r
+ }\r
+ for( int i=0; i<(int)pats.size(); i++ ){\r
+ Node n = pats[i];\r
+ //make the match generator\r
+ d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) );\r
+ //compute unique/shared variables\r
+ std::vector< int > unique_vars;\r
+ std::map< int, bool > shared_vars;\r
+ int numSharedVars = 0;\r
+ for( int j=0; j<(int)d_var_contains[n].size(); j++ ){\r
+ if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){\r
+ Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;\r
+ unique_vars.push_back( d_var_contains[n][j] );\r
+ }else{\r
+ shared_vars[ d_var_contains[n][j] ] = true;\r
+ numSharedVars++;\r
+ }\r
+ }\r
+ //we use the latest shared variables, then unique variables\r
+ std::vector< int > vars;\r
+ int index = i==0 ? (int)(pats.size()-1) : (i-1);\r
+ while( numSharedVars>0 && index!=i ){\r
+ for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){\r
+ if( it->second ){\r
+ if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=\r
+ d_var_contains[ pats[index] ].end() ){\r
+ vars.push_back( it->first );\r
+ shared_vars[ it->first ] = false;\r
+ numSharedVars--;\r
+ }\r
+ }\r
+ }\r
+ index = index==0 ? (int)(pats.size()-1) : (index-1);\r
+ }\r
+ vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );\r
+ Debug("smart-multi-trigger") << " Index[" << i << "]: ";\r
+ for( int i=0; i<(int)vars.size(); i++ ){\r
+ Debug("smart-multi-trigger") << vars[i] << " ";\r
+ }\r
+ Debug("smart-multi-trigger") << std::endl;\r
+ //make ordered inst match trie\r
+ InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;\r
+ imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );\r
+ d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );\r
+ }\r
+\r
+}\r
+\r
+/** reset instantiation round (call this whenever equivalence classes have changed) */\r
+void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ d_children[i]->resetInstantiationRound( qe );\r
+ }\r
+}\r
+\r
+/** reset, eqc is the equivalence class to search in (any if eqc=null) */\r
+void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ d_children[i]->reset( eqc, qe );\r
+ }\r
+}\r
+\r
+int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){\r
+ int addedLemmas = 0;\r
+ Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;\r
+ std::vector< InstMatch > newMatches;\r
+ InstMatch m;\r
+ while( d_children[i]->getNextMatch( m, qe ) ){\r
+ m.makeRepresentative( qe );\r
+ newMatches.push_back( InstMatch( &m ) );\r
+ m.clear();\r
+ }\r
+ for( int j=0; j<(int)newMatches.size(); j++ ){\r
+ processNewMatch( qe, newMatches[j], i, addedLemmas );\r
+ }\r
+ }\r
+ return addedLemmas;\r
+}\r
+\r
+void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){\r
+ //see if these produce new matches\r
+ d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true );\r
+ //possibly only do the following if we know that new matches will be produced?\r
+ //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that\r
+ // we can safely skip the following lines, even when we have already produced this match.\r
+ Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;\r
+ //process new instantiations\r
+ int childIndex = (fromChildIndex+1)%(int)d_children.size();\r
+ std::vector< IndexedTrie > unique_var_tries;\r
+ processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),\r
+ unique_var_tries, 0, childIndex, fromChildIndex, true );\r
+}\r
+\r
+void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,\r
+ std::vector< IndexedTrie >& unique_var_tries,\r
+ int trieIndex, int childIndex, int endChildIndex, bool modEq ){\r
+ if( childIndex==endChildIndex ){\r
+ //now, process unique variables\r
+ processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );\r
+ }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){\r
+ int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];\r
+ Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );\r
+ if( m.find( curr_ic )==m.end() ){\r
+ //if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME\r
+ // //unique variable(s), defer calculation\r
+ // unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );\r
+ // int newChildIndex = (childIndex+1)%(int)d_children.size();\r
+ // processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,\r
+ // 0, newChildIndex, endChildIndex, modEq );\r
+ //}else{\r
+ //shared and non-set variable, add to InstMatch\r
+ for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){\r
+ InstMatch mn( &m );\r
+ mn.set( curr_ic, it->first);\r
+ processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,\r
+ trieIndex+1, childIndex, endChildIndex, modEq );\r
+ }\r
+ //}\r
+ }else{\r
+ //shared and set variable, try to merge\r
+ Node n = m.get( curr_ic );\r
+ std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n );\r
+ if( it!=tr->d_data.end() ){\r
+ processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,\r
+ trieIndex+1, childIndex, endChildIndex, modEq );\r
+ }\r
+ if( modEq ){\r
+ //check modulo equality for other possible instantiations\r
+ if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){\r
+ eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),\r
+ qe->getEqualityQuery()->getEngine() );\r
+ while( !eqc.isFinished() ){\r
+ Node en = (*eqc);\r
+ if( en!=n ){\r
+ std::map< Node, InstMatchTrie >::iterator itc = tr->d_data.find( en );\r
+ if( itc!=tr->d_data.end() ){\r
+ processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,\r
+ trieIndex+1, childIndex, endChildIndex, modEq );\r
+ }\r
+ }\r
+ ++eqc;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }else{\r
+ int newChildIndex = (childIndex+1)%(int)d_children.size();\r
+ processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,\r
+ 0, newChildIndex, endChildIndex, modEq );\r
+ }\r
+}\r
+\r
+void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,\r
+ std::vector< IndexedTrie >& unique_var_tries,\r
+ int uvtIndex, InstMatchTrie* tr, int trieIndex ){\r
+ if( uvtIndex<(int)unique_var_tries.size() ){\r
+ int childIndex = unique_var_tries[uvtIndex].first.first;\r
+ if( !tr ){\r
+ tr = unique_var_tries[uvtIndex].second;\r
+ trieIndex = unique_var_tries[uvtIndex].first.second;\r
+ }\r
+ if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){\r
+ int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];\r
+ Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );\r
+ //unique non-set variable, add to InstMatch\r
+ for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){\r
+ InstMatch mn( &m );\r
+ mn.set( curr_ic, it->first);\r
+ processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );\r
+ }\r
+ }else{\r
+ processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );\r
+ }\r
+ }else{\r
+ //m is an instantiation\r
+ if( qe->addInstantiation( d_f, m ) ){\r
+ addedLemmas++;\r
+ Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;\r
+ }\r
+ }\r
+}\r
+\r
+int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){\r
+ Assert( options::eagerInstQuant() );\r
+ int addedLemmas = 0;\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){\r
+ InstMatch m;\r
+ //if it produces a match, then process it with the rest\r
+ if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){\r
+ processNewMatch( qe, m, i, addedLemmas );\r
+ }\r
+ }\r
+ }\r
+ return addedLemmas;\r
+}\r
+\r
+int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){\r
+ InstMatch m;\r
+ m.add( baseMatch );\r
+ int addedLemmas = 0;\r
+ if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){\r
+ for( int i=0; i<2; i++ ){\r
+ addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) );\r
+ }\r
+ }else{\r
+ addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );\r
+ }\r
+ return addedLemmas;\r
+}\r
+\r
+void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){\r
+ if( argIndex==(int)d_match_pattern.getNumChildren() ){\r
+ //m is an instantiation\r
+ if( qe->addInstantiation( d_f, m ) ){\r
+ addedLemmas++;\r
+ Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;\r
+ }\r
+ }else{\r
+ if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){\r
+ Node ic = d_match_pattern[argIndex];\r
+ for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){\r
+ Node t = it->first;\r
+ if( m.get( ic ).isNull() || m.get( ic )==t ){\r
+ Node prev = m.get( ic );\r
+ m.set( ic, t);\r
+ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );\r
+ m.set( ic, prev);\r
+ }\r
+ }\r
+ }else{\r
+ Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );\r
+ std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );\r
+ if( it!=tat->d_data.end() ){\r
+ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){\r
+ Assert( options::eagerInstQuant() );\r
+ InstMatch m;\r
+ for( int i=0; i<(int)t.getNumChildren(); i++ ){\r
+ if( d_match_pattern[i].getKind()==INST_CONSTANT ){\r
+ m.set(d_match_pattern[i], t[i]);\r
+ }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){\r
+ return 0;\r
+ }\r
+ }\r
+ return qe->addInstantiation( f, m ) ? 1 : 0;\r
+}\r
+\r
+}/* CVC4::theory::inst namespace */\r
+}/* CVC4::theory namespace */\r
+}/* CVC4 namespace */\r
--- /dev/null
+/********************* */\r
+/*! \file inst_match_generator.h\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: bobot\r
+ ** Minor contributors (to current version): mdeters\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief inst match generator class\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H\r
+#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H\r
+\r
+#include "theory/quantifiers/inst_match.h"\r
+#include <map>\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+\r
+class QuantifiersEngine;\r
+namespace quantifiers{\r
+ class TermArgTrie;\r
+}\r
+\r
+namespace inst {\r
+\r
+/** base class for producing InstMatch objects */\r
+class IMGenerator {\r
+public:\r
+ /** reset instantiation round (call this at beginning of instantiation round) */\r
+ virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;\r
+ /** reset, eqc is the equivalence class to search in (any if eqc=null) */\r
+ virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;\r
+ /** get the next match. must call reset( eqc ) before this function. */\r
+ virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;\r
+ /** add instantiations directly */\r
+ virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;\r
+ /** add ground term t, called when t is added to term db */\r
+ virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;\r
+};/* class IMGenerator */\r
+\r
+class CandidateGenerator;\r
+\r
+class InstMatchGenerator : public IMGenerator {\r
+private:\r
+ /** candidate generator */\r
+ CandidateGenerator* d_cg;\r
+ /** policy to use for matching */\r
+ int d_matchPolicy;\r
+ /** children generators */\r
+ std::vector< InstMatchGenerator* > d_children;\r
+ std::vector< int > d_children_index;\r
+ /** partial vector */\r
+ std::vector< InstMatch > d_partial;\r
+ /** eq class */\r
+ Node d_eq_class;\r
+ /** for arithmetic matching */\r
+ std::map< Node, Node > d_arith_coeffs;\r
+ /** initialize pattern */\r
+ void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe );\r
+ void initializePattern( Node pat, QuantifiersEngine* qe );\r
+public:\r
+ enum {\r
+ //options for producing matches\r
+ MATCH_GEN_DEFAULT = 0,\r
+ MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers\r
+ //others (internally used)\r
+ MATCH_GEN_INTERNAL_ARITHMETIC,\r
+ MATCH_GEN_INTERNAL_ERROR,\r
+ };\r
+private:\r
+ /** get the next match. must call d_cg->reset( ... ) before using.\r
+ only valid for use where !d_match_pattern.isNull().\r
+ */\r
+ bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );\r
+ /** for arithmetic */\r
+ bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );\r
+public:\r
+ /** get the match against ground term or formula t.\r
+ d_match_pattern and t should have the same shape.\r
+ only valid for use where !d_match_pattern.isNull().\r
+ */\r
+ bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );\r
+\r
+ /** constructors */\r
+ InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );\r
+ InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );\r
+ /** destructor */\r
+ ~InstMatchGenerator(){}\r
+ /** The pattern we are producing matches for.\r
+ If null, this is a multi trigger that is merging matches from d_children.\r
+ */\r
+ Node d_pattern;\r
+ /** match pattern */\r
+ Node d_match_pattern;\r
+public:\r
+ /** reset instantiation round (call this whenever equivalence classes have changed) */\r
+ void resetInstantiationRound( QuantifiersEngine* qe );\r
+ /** reset, eqc is the equivalence class to search in (any if eqc=null) */\r
+ void reset( Node eqc, QuantifiersEngine* qe );\r
+ /** get the next match. must call reset( eqc ) before this function. */\r
+ bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );\r
+ /** add instantiations */\r
+ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );\r
+ /** add ground term t */\r
+ int addTerm( Node f, Node t, QuantifiersEngine* qe );\r
+};/* class InstMatchGenerator */\r
+\r
+/** smart multi-trigger implementation */\r
+class InstMatchGeneratorMulti : public IMGenerator {\r
+private:\r
+ /** indexed trie */\r
+ typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;\r
+ /** process new match */\r
+ void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );\r
+ /** process new instantiations */\r
+ void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,\r
+ std::vector< IndexedTrie >& unique_var_tries,\r
+ int trieIndex, int childIndex, int endChildIndex, bool modEq );\r
+ /** process new instantiations 2 */\r
+ void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,\r
+ std::vector< IndexedTrie >& unique_var_tries,\r
+ int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );\r
+private:\r
+ /** var contains (variable indices) for each pattern node */\r
+ std::map< Node, std::vector< int > > d_var_contains;\r
+ /** variable indices contained to pattern nodes */\r
+ std::map< int, std::vector< Node > > d_var_to_node;\r
+ /** quantifier to use */\r
+ Node d_f;\r
+ /** policy to use for matching */\r
+ int d_matchPolicy;\r
+ /** children generators */\r
+ std::vector< InstMatchGenerator* > d_children;\r
+ /** inst match tries for each child */\r
+ std::vector< InstMatchTrieOrdered > d_children_trie;\r
+ /** calculate matches */\r
+ void calculateMatches( QuantifiersEngine* qe );\r
+public:\r
+ /** constructors */\r
+ InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );\r
+ /** destructor */\r
+ ~InstMatchGeneratorMulti(){}\r
+ /** reset instantiation round (call this whenever equivalence classes have changed) */\r
+ void resetInstantiationRound( QuantifiersEngine* qe );\r
+ /** reset, eqc is the equivalence class to search in (any if eqc=null) */\r
+ void reset( Node eqc, QuantifiersEngine* qe );\r
+ /** get the next match. must call reset( eqc ) before this function. (not implemented) */\r
+ bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }\r
+ /** add instantiations */\r
+ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );\r
+ /** add ground term t */\r
+ int addTerm( Node f, Node t, QuantifiersEngine* qe );\r
+};/* class InstMatchGeneratorMulti */\r
+\r
+/** smart (single)-trigger implementation */\r
+class InstMatchGeneratorSimple : public IMGenerator {\r
+private:\r
+ /** quantifier for match term */\r
+ Node d_f;\r
+ /** match term */\r
+ Node d_match_pattern;\r
+ /** add instantiations */\r
+ void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );\r
+public:\r
+ /** constructors */\r
+ InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}\r
+ /** destructor */\r
+ ~InstMatchGeneratorSimple(){}\r
+ /** reset instantiation round (call this whenever equivalence classes have changed) */\r
+ void resetInstantiationRound( QuantifiersEngine* qe ) {}\r
+ /** reset, eqc is the equivalence class to search in (any if eqc=null) */\r
+ void reset( Node eqc, QuantifiersEngine* qe ) {}\r
+ /** get the next match. must call reset( eqc ) before this function. (not implemented) */\r
+ bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }\r
+ /** add instantiations */\r
+ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );\r
+ /** add ground term t, possibly add instantiations */\r
+ int addTerm( Node f, Node t, QuantifiersEngine* qe );\r
+};/* class InstMatchGeneratorSimple */\r
+\r
+}\r
+}\r
+}\r
+\r
+#endif\r
}
//for calculating terms that we don't need to consider
if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
- //need to consider if it is not congruent modulo model basis
- if( !tabt.addTerm( d_qe, n ) ){
- BasisNoMatchAttribute bnma;
- n.setAttribute(bnma,true);
+ if( !n.getAttribute(BasisNoMatchAttribute()) ){
+ //need to consider if it is not congruent modulo model basis
+ if( !tabt.addTerm( d_qe, n ) ){
+ BasisNoMatchAttribute bnma;
+ n.setAttribute(bnma,true);
+ }
}
}
}
}
}
+bool ModelEngineBuilder::hasConstantDefinition( Node n ){
+ Node lit = n.getKind()==NOT ? n[0] : n;
+ if( lit.getKind()==APPLY_UF ){
+ Node op = lit.getOperator();
+ if( !d_uf_prefs[op].d_const_val.isNull() ){
+ return true;
+ }
+ }
+ return false;
+}
+
bool ModelEngineBuilder::optUseModel() {
return options::fmfModelBasedInst();
}
bool ModelEngineBuilder::isTermActive( Node n ){
return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term
( n.getAttribute(ModelBasisArgAttribute())==1 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
- //and is not congruent to another
- //active term
+ //and is not congruent modulo model basis
+ //to another active term
}
isConst = false;
if( gn.getKind()==APPLY_UF ){
uf_terms.push_back( gn );
- isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull();
+ isConst = hasConstantDefinition( gn );
}else if( gn.getKind()==EQUAL ){
isConst = true;
for( int j=0; j<2; j++ ){
if( n[j].getKind()==APPLY_UF &&
fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){
uf_terms.push_back( gn[j] );
- isConst = isConst && !d_uf_prefs[ gn[j].getOperator() ].d_const_val.isNull();
+ isConst = isConst && hasConstantDefinition( gn[j] );
}else{
isConst = false;
}
std::vector< Node > tr_terms;
if( lit.getKind()==APPLY_UF ){
//only match predicates that are contrary to this one, use literal matching
- std::vector< Node > children;
- children.push_back( lit );
- children.push_back( !phase ? fm->d_true : fm->d_false );
- Node eq = d_qe->getTermDatabase()->mkNodeInstConstant( IFF, children, f );
+ Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
+ d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f );
tr_terms.push_back( eq );
}else if( lit.getKind()==EQUAL ){
//collect trigger terms
d_quant_selection_formula[f] = s;
Node gs = d_qe->getTermDatabase()->getModelBasis( f, s );
setSelectedTerms( gs );
+ //quick check if it is constant sat
+ if( hasConstantDefinition( s ) ){
+ d_quant_sat[f] = true;
+ }
}
//analyze sub quantifiers
- for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
- analyzeQuantifier( fm, d_sub_quants[f][i] );
+ if( d_quant_sat.find( f )==d_quant_sat.end() ){
+ for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
+ analyzeQuantifier( fm, d_sub_quants[f][i] );
+ }
}
}
if( fp!=f ) Trace("inst-gen") << " ";
Trace("inst-gen") << "Sel Form : " << d_quant_selection_formula[f] << std::endl;
int addedLemmas = 0;
- //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
- //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
- // effectively acting as partial instantiations instead of pointwise instantiations.
- if( !d_quant_selection_formula[f].isNull() ){
- //first, try on sub quantifiers
- for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
- addedLemmas += doInstGen( fm, d_sub_quants[f][i] );
- }
- if( addedLemmas>0 ){
- Trace("inst-gen") << " -> children added lemmas" << std::endl;
- return addedLemmas;
- }else{
- Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl;
- //get all possible values of selection formula
- InstGenProcess igp( d_quant_selection_formula[f] );
- igp.calculateMatches( d_qe, f );
- Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl;
- for( int i=0; i<igp.getNumMatches(); i++ ){
- //if the match is not already true in the model
- if( igp.getMatchValue( i )!=fm->d_true ){
- InstMatch m;
- igp.getMatch( d_qe->getEqualityQuery(), i, m );
- //we only consider matches that are non-empty
- // matches that are empty should trigger other instances that are non-empty
- if( !m.empty() ){
- Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl;
- //translate to be in terms match in terms of fp
- InstMatch mp;
- getParentQuantifierMatch( mp, fp, m, f );
-
- //if this is a partial instantion
- if( !m.isComplete( f ) ){
- //if the instantiation does not yet exist
- if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){
- //get the partial instantiation pf
- Node pf = d_qe->getInstantiation( fp, mp );
- Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl;
- Trace("inst-gen-pi") << " " << pf << std::endl;
- d_sub_quants[ f ].push_back( pf );
- d_sub_quant_inst[ pf ] = InstMatch( &mp );
- d_sub_quant_parent[ pf ] = fp;
- mp.add( d_quant_basis_match[ fp ] );
- d_quant_basis_match[ pf ] = InstMatch( &mp );
- addedLemmas += initializeQuantifier( pf, fp );
- Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl;
- }
- }else{
- if( d_qe->addInstantiation( fp, mp ) ){
- addedLemmas++;
+ if( d_quant_sat.find( f )==d_quant_sat.end() ){
+ //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
+ //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
+ // effectively acting as partial instantiations instead of pointwise instantiations.
+ if( !d_quant_selection_formula[f].isNull() ){
+ //first, try on sub quantifiers
+ for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
+ addedLemmas += doInstGen( fm, d_sub_quants[f][i] );
+ }
+ if( addedLemmas>0 ){
+ Trace("inst-gen") << " -> children added lemmas" << std::endl;
+ return addedLemmas;
+ }else{
+ Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl;
+ //get all possible values of selection formula
+ InstGenProcess igp( d_quant_selection_formula[f] );
+ igp.calculateMatches( d_qe, f );
+ Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl;
+ for( int i=0; i<igp.getNumMatches(); i++ ){
+ //if the match is not already true in the model
+ if( igp.getMatchValue( i )!=fm->d_true ){
+ InstMatch m;
+ igp.getMatch( d_qe->getEqualityQuery(), i, m );
+ //we only consider matches that are non-empty
+ // matches that are empty should trigger other instances that are non-empty
+ if( !m.empty() ){
+ Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl;
+ //translate to be in terms match in terms of fp
+ InstMatch mp;
+ getParentQuantifierMatch( mp, fp, m, f );
+
+ //if this is a partial instantion
+ if( !m.isComplete( f ) ){
+ //if the instantiation does not yet exist
+ if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){
+ //get the partial instantiation pf
+ Node pf = d_qe->getInstantiation( fp, mp );
+ Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl;
+ Trace("inst-gen-pi") << " " << pf << std::endl;
+ d_sub_quants[ f ].push_back( pf );
+ d_sub_quant_inst[ pf ] = InstMatch( &mp );
+ d_sub_quant_parent[ pf ] = fp;
+ mp.add( d_quant_basis_match[ fp ] );
+ d_quant_basis_match[ pf ] = InstMatch( &mp );
+ addedLemmas += initializeQuantifier( pf, fp );
+ Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl;
+ }
+ }else{
+ if( d_qe->addInstantiation( fp, mp ) ){
+ addedLemmas++;
+ }
}
}
}
}
- }
- if( addedLemmas==0 ){
- //all sub quantifiers must be satisfied as well
- bool subQuantSat = true;
- for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
- if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){
- subQuantSat = false;
- break;
+ if( addedLemmas==0 ){
+ //all sub quantifiers must be satisfied as well
+ bool subQuantSat = true;
+ for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
+ if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){
+ subQuantSat = false;
+ break;
+ }
+ }
+ if( subQuantSat ){
+ d_quant_sat[ f ] = true;
}
}
- if( subQuantSat ){
- d_quant_sat[ f ] = true;
- }
- }
- if( fp!=f ) Trace("inst-gen") << " ";
- Trace("inst-gen") << " -> added lemmas = " << addedLemmas << std::endl;
- if( d_quant_sat.find( f )!=d_quant_sat.end() ){
if( fp!=f ) Trace("inst-gen") << " ";
- Trace("inst-gen") << " -> *** it is satisfied" << std::endl;
+ Trace("inst-gen") << " -> added lemmas = " << addedLemmas << std::endl;
+ if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+ if( fp!=f ) Trace("inst-gen") << " ";
+ Trace("inst-gen") << " -> *** it is satisfied" << std::endl;
+ }
}
}
}
ret = getSelectionFormula( fn[0], n[0], !polarity, useOption );
}else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){
//whether we only need to find one or all
- bool posPol = (( n.getKind()==OR || n.getKind()==IMPLIES ) && polarity ) || ( n.getKind()==AND && !polarity );
+ bool favorPol = ( n.getKind()!=AND && polarity ) || ( n.getKind()==AND && !polarity );
std::vector< Node > children;
- bool retSet = false;
for( int i=0; i<(int)n.getNumChildren(); i++ ){
Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i];
Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i];
Node nn = getSelectionFormula( fnc, nc, polarity, useOption );
- if( nn.isNull()!=posPol ){ //TODO: may want to weaken selection formula
- ret = nn;
- retSet = true;
+ if( nn.isNull() && !favorPol ){
+ //cannot make selection formula
+ children.clear();
break;
}
- if( std::find( children.begin(), children.end(), nn )==children.end() ){
- children.push_back( nn );
+ if( !nn.isNull() ){
+ if( favorPol ){ //temporary
+ return nn; //
+ } //
+ if( std::find( children.begin(), children.end(), nn )==children.end() ){
+ children.push_back( nn );
+ }
}
}
- if( !retSet && !posPol ){
- ret = NodeManager::currentNM()->mkNode( AND, children );
+ if( !children.empty() ){
+ if( favorPol ){
+ //filter which formulas we wish to keep, make disjunction
+ Node min_lit;
+ int min_score = -1;
+ for( size_t i=0; i<children.size(); i++ ){
+ //if it is constant apply uf application, return it for sure
+ if( hasConstantDefinition( children[i] ) ){
+ min_lit = children[i];
+ break;
+ }else{
+ int score = getSelectionFormulaScore( children[i] );
+ if( min_score<0 || score<min_score ){
+ min_score = score;
+ min_lit = children[i];
+ }
+ }
+ }
+ //currently just return the best single literal
+ ret = min_lit;
+ }else{
+ //selection formula must be conjunction of children
+ ret = NodeManager::currentNM()->mkNode( AND, children );
+ }
+ }else{
+ ret = Node::null();
}
}else if( n.getKind()==ITE ){
Node nn;
return ret;
}
+int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){
+ if( fn.getType().isBoolean() ){
+ if( fn.getKind()==APPLY_UF ){
+ Node op = fn.getOperator();
+ //return total number of terms
+ return d_qe->getTermDatabase()->d_op_count[op];
+ }else{
+ int score = 0;
+ for( size_t i=0; i<fn.getNumChildren(); i++ ){
+ score += getSelectionFormulaScore( fn[i] );
+ }
+ return score;
+ }
+ }else{
+ return 0;
+ }
+}
+
void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){
//if it is apply uf and has model basis arguments, then mark term as being "selected"
bool d_considerAxioms;
// set effort
void setEffort( int effort );
+protected: //helper functions
+ /** term has constant definition */
+ bool hasConstantDefinition( Node n );
public:
//options
virtual bool optUseModel();
private:
//get selection formula for quantifier body
Node getSelectionFormula( Node fn, Node n, bool polarity, int useOption );
+ //get a heuristic score for a selection formula
+ int getSelectionFormulaScore( Node fn );
//set selected terms in term
void setSelectedTerms( Node s );
//is usable selection literal
\r
#include "theory/quantifiers/quant_util.h"\r
#include "theory/quantifiers/inst_match.h"\r
+#include "theory/quantifiers/term_database.h"\r
\r
using namespace std;\r
using namespace CVC4;\r
#define __CVC4__THEORY__QUANT_UTIL_H\r
\r
#include "theory/theory.h"\r
+#include "theory/uf/equality_engine.h"\r
\r
#include <ext/hash_set>\r
#include <iostream>\r
std::map< Node, Node > d_phase_reqs_equality_term;\r
};\r
\r
+\r
+class EqualityQuery {\r
+public:\r
+ EqualityQuery(){}\r
+ virtual ~EqualityQuery(){};\r
+ /** contains term */\r
+ virtual bool hasTerm( Node a ) = 0;\r
+ /** get the representative of the equivalence class of a */\r
+ virtual Node getRepresentative( Node a ) = 0;\r
+ /** returns true if a and b are equal in the current context */\r
+ virtual bool areEqual( Node a, Node b ) = 0;\r
+ /** returns true is a and b are disequal in the current context */\r
+ virtual bool areDisequal( Node a, Node b ) = 0;\r
+ /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.\r
+ If cbqi is active, this will return a term in the equivalence class of "a" that does\r
+ not contain instantiation constants, if such a term exists.\r
+ */\r
+ virtual Node getInternalRepresentative( Node a ) = 0;\r
+ /** get the equality engine associated with this query */\r
+ virtual eq::EqualityEngine* getEngine() = 0;\r
+ /** get the equivalence class of a */\r
+ virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;\r
+};/* class EqualityQuery */\r
+\r
}\r
}\r
\r
}
}
-Trigger* TrTrie::getTrigger2( std::vector< Node >& nodes ){
- if( nodes.empty() ){
- return d_tr;
- }else{
- Node n = nodes.back();
- nodes.pop_back();
- if( d_children.find( n )!=d_children.end() ){
- return d_children[n]->getTrigger2( nodes );
- }else{
- return NULL;
- }
- }
-}
-
-void TrTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
- if( nodes.empty() ){
- d_tr = t;
- }else{
- Node n = nodes.back();
- nodes.pop_back();
- if( d_children.find( n )==d_children.end() ){
- d_children[n] = new TrTrie;
- }
- d_children[n]->addTrigger2( nodes, t );
- }
-}
-
void TermDb::addTermEfficient( Node n, std::set< Node >& added){
static AvailableInTermDb aitdi;
if (inst::Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){
d_op_map[op].push_back( n );
added.insert( n );
- uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
for( int i=0; i<(int)n.getNumChildren(); i++ ){
addTerm( n[i], added, withinQuant );
if( options::efficientEMatching() ){
+ uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
if( d_parents[n[i]][op].empty() ){
//must add parent to equivalence class info
- Node nir = d_ith->getRepresentative( n[i] );
- uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir );
+ Node nir = ith->getRepresentative( n[i] );
+ uf::EqClassInfo* eci_nir = ith->getEquivalenceClassInfo( nir );
if( eci_nir ){
eci_nir->d_pfuns[ op ] = true;
}
}
if( options::eagerInstQuant() ){
if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
+ uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
int addedLemmas = 0;
- for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
- addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n );
+ for( int i=0; i<(int)ith->d_op_triggers[op].size(); i++ ){
+ addedLemmas += ith->d_op_triggers[op][i]->addTerm( n );
}
//Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() );
int alreadyCongruentCount = 0;
//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 ){
+ d_op_count[ it->first ] = 0;
if( !it->second.empty() ){
if( it->second[0].getType().isBoolean() ){
d_pred_map_trie[ 0 ][ it->first ].d_data.clear();
congruentCount++;
}else{
nonCongruentCount++;
+ d_op_count[ it->first ]++;
}
}else{
congruentCount++;
congruentCount++;
}else{
nonCongruentCount++;
+ d_op_count[ op ]++;
}
}else{
alreadyCongruentCount++;
return n2;
}
-Node TermDb::mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ){
- Node n = NodeManager::currentNM()->mkNode( k, children );
- setInstantiationConstantAttr( n, f );
- return n;
-}
-
Node TermDb::getSkolemizedBody( Node f ){
}
d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(),
d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() );
- if( f.hasAttribute(InstLevelAttribute()) ){
- setInstantiationLevelAttr( d_skolem_body[ f ], f.getAttribute(InstLevelAttribute()) );
- }
}
return d_skolem_body[ f ];
}
-
-void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){
- if( !n.hasAttribute(InstLevelAttribute()) ){
- InstLevelAttribute ila;
- n.setAttribute(ila,level);
- }
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- setInstantiationLevelAttr( n[i], level );
- }
-}
-
Node TermDb::getFreeVariableForInstConstant( Node n ){
TypeNode tn = n.getType();
if( d_free_vars.find( tn )==d_free_vars.end() ){
namespace CVC4 {
namespace theory {
+/** Attribute true for nodes that should not be used for matching */
+struct NoMatchAttributeId {};
+/** use the special for boolean flag */
+typedef expr::Attribute< NoMatchAttributeId,
+ bool,
+ expr::attr::NullCleanupStrategy,
+ true // context dependent
+ > NoMatchAttribute;
+
+// attribute for "contains instantiation constants from"
+struct InstConstantAttributeId {};
+typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
+
+struct InstLevelAttributeId {};
+typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
+
+struct InstVarNumAttributeId {};
+typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
+
+// Attribute that tell if a node have been asserted in this branch
+struct AvailableInTermDbId {};
+/** use the special for boolean flag */
+typedef expr::Attribute<AvailableInTermDbId,
+ bool,
+ expr::attr::NullCleanupStrategy,
+ true // context dependent
+ > AvailableInTermDb;
+
+struct ModelBasisAttributeId {};
+typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
+//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+// 0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId {};
+typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
+
+
class QuantifiersEngine;
namespace inst{
};/* class TermArgTrie */
-/** a trie of triggers */
-class TrTrie {
-private:
- inst::Trigger* getTrigger2( std::vector< Node >& nodes );
- void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
-public:
- TrTrie() : d_tr( NULL ){}
- inst::Trigger* d_tr;
- std::map< TNode, TrTrie* > d_children;
- inst::Trigger* getTrigger( std::vector< Node >& nodes ){
- std::vector< Node > temp;
- temp.insert( temp.begin(), nodes.begin(), nodes.end() );
- std::sort( temp.begin(), temp.end() );
- return getTrigger2( temp );
- }
- void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){
- std::vector< Node > temp;
- temp.insert( temp.begin(), nodes.begin(), nodes.end() );
- std::sort( temp.begin(), temp.end() );
- return addTrigger2( temp, t );
- }
-};/* class inst::Trigger::TrTrie */
-
-
class TermDb {
friend class ::CVC4::theory::QuantifiersEngine;
friend class ::CVC4::theory::inst::Trigger;
private:
/** reference to the quantifiers engine */
QuantifiersEngine* d_quantEngine;
- /** calculated no match terms */
- bool d_matching_active;
/** terms processed */
std::hash_set< Node, NodeHashFunction > d_processed;
public:
- TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}
+ TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
~TermDb(){}
/** map from APPLY_UF operators to ground terms for that operator */
std::map< Node, std::vector< Node > > d_op_map;
+ /** count number of APPLY_UF terms per operator */
+ std::map< Node, int > d_op_count;
/** map from APPLY_UF functions to trie */
std::map< Node, TermArgTrie > d_func_map_trie;
/** map from APPLY_UF predicates to trie */
void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
/** reset (calculate which terms are active) */
void reset( Theory::Effort effort );
- /** set active */
- void setMatchingActive( bool a ) { d_matching_active = a; }
- /** get active */
- bool getMatchingActive() { return d_matching_active; }
private:
/** for efficient e-matching */
void addTermEfficient( Node n, std::set< Node >& added);
Node convertNodeToPattern( Node n, Node f,
const std::vector<Node> & vars,
const std::vector<Node> & nvars);
- /** get iff term */
- Node getInstConstantIffTerm( Node n, bool pol );
- /** make node, validating the inst constant attribute */
- Node mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f );
/** set instantiation constant attr */
void setInstantiationConstantAttr( Node n, Node f );
public:
/** get free variable for instantiation constant */
Node getFreeVariableForInstConstant( Node n );
- /** set instantiation level attr */
- void setInstantiationLevelAttr( Node n, uint64_t level );
//for triggers
private:
void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
/** get var contains for node n */
void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
-private:
- /** all triggers will be stored in this trie */
- TrTrie d_tr_trie;
-public:
- /** get trigger */
- inst::Trigger* getTrigger( std::vector< Node >& nodes ){ return d_tr_trie.getTrigger( nodes ); }
- /** add trigger */
- void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){ d_tr_trie.addTrigger( nodes, t ); }
};/* class TermDb */
}/* CVC4::theory::quantifiers namespace */
#include "theory/uf/equality_engine.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/inst_match_generator.h"
using namespace std;
using namespace CVC4;
return d_mg->addTerm( d_f, t, d_quantEngine );
}
+//bool Trigger::nonunifiable( TNode t, const std::vector<Node> & vars){
+// return d_mg->nonunifiable(t,vars);
+//}
+
int Trigger::addInstantiations( InstMatch& baseMatch ){
int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine );
if( addedLemmas>0 ){
// Notice() << "Trigger new old = " << trNew << " " << trOld << std::endl;
//}
}else{
- Trigger* t = qe->getTermDatabase()->getTrigger( trNodes );
+ Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
if( t ){
if( trOption==TR_GET_OLD ){
//just return old trigger
}
}
Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );
- qe->getTermDatabase()->addTrigger( trNodes, t );
+ qe->getTriggerDatabase()->addTrigger( trNodes, t );
return t;
}
Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
}
return false;
}
+
+Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
+ if( nodes.empty() ){
+ return d_tr;
+ }else{
+ Node n = nodes.back();
+ nodes.pop_back();
+ if( d_children.find( n )!=d_children.end() ){
+ return d_children[n]->getTrigger2( nodes );
+ }else{
+ return NULL;
+ }
+ }
+}
+
+void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
+ if( nodes.empty() ){
+ d_tr = t;
+ }else{
+ Node n = nodes.back();
+ nodes.pop_back();
+ if( d_children.find( n )==d_children.end() ){
+ d_children[n] = new TriggerTrie;
+ }
+ d_children[n]->addTrigger2( nodes, t );
+ }
+}
#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
#include "theory/quantifiers/inst_match.h"
+#include "expr/node.h"
+#include "util/hash.h"
+#include <map>
namespace CVC4 {
namespace theory {
+
+class QuantifiersEngine;
+
namespace inst {
+class IMGenerator;
+
//a collect of nodes representing a trigger
class Trigger {
private:
bool getMatch( Node t, InstMatch& m);
/** add ground term t, called when t is added to the TermDb */
int addTerm( Node t );
- /** return true if whatever Node is subsituted for the variables the
- given Node can't match the pattern */
- bool nonunifiable( TNode t, const std::vector<Node> & vars){
- return d_mg->nonunifiable(t,vars);
- }
/** return whether this is a multi-trigger */
bool isMultiTrigger() { return d_nodes.size()>1; }
public:
return out;
}
+
+/** a trie of triggers */
+class TriggerTrie {
+private:
+ inst::Trigger* getTrigger2( std::vector< Node >& nodes );
+ void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
+public:
+ TriggerTrie() : d_tr( NULL ){}
+ inst::Trigger* d_tr;
+ std::map< TNode, TriggerTrie* > d_children;
+ inst::Trigger* getTrigger( std::vector< Node >& nodes ){
+ std::vector< Node > temp;
+ temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+ std::sort( temp.begin(), temp.end() );
+ return getTrigger2( temp );
+ }
+ void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){
+ std::vector< Node > temp;
+ temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+ std::sort( temp.begin(), temp.end() );
+ return addTrigger2( temp, t );
+ }
+};/* class inst::Trigger::Trigger */
+
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
using namespace std;
using namespace CVC4;
d_quant_rel( false ){ //currently do not care about relevance
d_eq_query = new EqualityQueryQuantifiersEngine( this );
d_term_db = new quantifiers::TermDb( this );
+ d_tr_trie = new inst::TriggerTrie;
d_hasAddedLemma = false;
//the model object
}
}
-std::vector<Node> QuantifiersEngine::createInstVariable( std::vector<Node> & vars ){
- std::vector<Node> inst_constant;
- inst_constant.reserve(vars.size());
- for( std::vector<Node>::const_iterator v = vars.begin();
- v != vars.end(); ++v ){
- //make instantiation constants
- Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() );
- inst_constant.push_back( ic );
- };
- return inst_constant;
-}
-
void QuantifiersEngine::registerQuantifier( Node f ){
if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
d_quants.push_back( f );
}
}
+bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
+ Assert( f.getKind()==FORALL );
+ Assert( !f.hasAttribute(InstConstantAttribute()) );
+ Assert( vars.size()==terms.size() );
+ Node body = getInstantiation( f, vars, terms );
+ //make the lemma
+ NodeBuilder<> nb(kind::OR);
+ nb << f.notNode() << body;
+ Node lem = nb;
+ //check for duplication
+ if( addLemma( lem ) ){
+ Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
+ uint64_t maxInstLevel = 0;
+ for( int i=0; i<(int)terms.size(); i++ ){
+ if( terms[i].hasAttribute(InstConstantAttribute()) ){
+ Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
+ for( int i=0; i<(int)terms.size(); i++ ){
+ Debug("inst") << " " << terms[i] << std::endl;
+ }
+ Unreachable("Bad instantiation");
+ }else{
+ Trace("inst") << " " << terms[i];
+ //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute());
+ Trace("inst") << std::endl;
+ if( terms[i].hasAttribute(InstLevelAttribute()) ){
+ if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
+ maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+ }
+ }else{
+ setInstantiationLevelAttr( terms[i], 0 );
+ }
+ }
+ }
+ Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
+ setInstantiationLevelAttr( body, maxInstLevel+1 );
+ ++(d_statistics.d_instantiations);
+ d_statistics.d_total_inst_var += (int)terms.size();
+ d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 );
+ return true;
+ }else{
+ ++(d_statistics.d_inst_duplicate);
+ return false;
+ }
+}
+
+void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
+ if( !n.hasAttribute(InstLevelAttribute()) ){
+ InstLevelAttribute ila;
+ n.setAttribute(ila,level);
+ }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ setInstantiationLevelAttr( n[i], level );
+ }
+}
+
Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
//process partial instantiation if necessary
}
}
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
- Assert( f.getKind()==FORALL );
- Assert( !f.hasAttribute(InstConstantAttribute()) );
- Assert( vars.size()==terms.size() );
- Node body = getInstantiation( f, vars, terms );
- //make the lemma
- NodeBuilder<> nb(kind::OR);
- nb << f.notNode() << body;
- Node lem = nb;
- //check for duplication
- if( addLemma( lem ) ){
- Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
- uint64_t maxInstLevel = 0;
- for( int i=0; i<(int)terms.size(); i++ ){
- if( terms[i].hasAttribute(InstConstantAttribute()) ){
- Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
- for( int i=0; i<(int)terms.size(); i++ ){
- Debug("inst") << " " << terms[i] << std::endl;
- }
- Unreachable("Bad instantiation");
- }else{
- Trace("inst") << " " << terms[i];
- //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute());
- Trace("inst") << std::endl;
- if( terms[i].hasAttribute(InstLevelAttribute()) ){
- if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
- maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
- }
- }else{
- d_term_db->setInstantiationLevelAttr( terms[i], 0 );
- }
- }
- }
- Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
- d_term_db->setInstantiationLevelAttr( body, maxInstLevel+1 );
- ++(d_statistics.d_instantiations);
- d_statistics.d_total_inst_var += (int)terms.size();
- d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 );
- return true;
- }else{
- ++(d_statistics.d_inst_duplicate);
- return false;
- }
-}
-
bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){
//make sure there are values for each variable we are instantiating
m.makeComplete( f, this );
bool nodeChanged = false;
if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
- std::vector< Node > children;
- children.push_back( nodes[i] );
- children.push_back( NodeManager::currentNM()->mkConst<bool>(preq) );
- nodes[i] = d_term_db->mkNodeInstConstant( IFF, children, f );
+ nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
+ d_term_db->setInstantiationConstantAttr( nodes[i], f );
nodeChanged = true;
}
//else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
d_statistics.d_lit_phase_nreq += (int)nodes.size();
}
}
+/*
+EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) {
+ // Should use skeleton (in order to have the type and the kind
+ // or any needed other information) instead of only the type
+
+ // TheoryId id = Theory::theoryOf(t);
+ // inst::EqualityQuery* eq = d_eq_query_arr[id];
+ // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
+ // else return eq;
+
+ // hack because the generic one is too slow
+ // TheoryId id = Theory::theoryOf(t);
+ // if( true || id == theory::THEORY_UF){
+ // uf::InstantiatorTheoryUf* ith = static_cast<uf::InstantiatorTheoryUf*>( getInstantiator( theory::THEORY_UF ));
+ // return new uf::EqualityQueryInstantiatorTheoryUf(ith);
+ // }
+ // inst::EqualityQuery* eq = d_eq_query_arr[id];
+ // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
+ // else return eq;
+
+
+ //Currently we use the generic EqualityQuery
+ return getEqualityQuery();
+}
+
+
+rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() {
+ return new GenericCandidateGeneratorClasses(this);
+}
+
+rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() {
+ return new GenericCandidateGeneratorClass(this);
+}
+
+rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) {
+ // TheoryId id = Theory::theoryOf(t);
+ // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses();
+ // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses();
+ // else return eq;
+ return getRRCanGenClasses();
+}
+
+rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) {
+ // TheoryId id = Theory::theoryOf(t);
+ // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass();
+ // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass();
+ // else return eq;
+ return getRRCanGenClass();
+}
+*/
QuantifiersEngine::Statistics::Statistics():
d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
eqc.push_back( a );
}
}
-
-inst::EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) {
- /** Should use skeleton (in order to have the type and the kind
- or any needed other information) instead of only the type */
-
- // TheoryId id = Theory::theoryOf(t);
- // inst::EqualityQuery* eq = d_eq_query_arr[id];
- // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
- // else return eq;
-
- /** hack because the generic one is too slow */
- // TheoryId id = Theory::theoryOf(t);
- // if( true || id == theory::THEORY_UF){
- // uf::InstantiatorTheoryUf* ith = static_cast<uf::InstantiatorTheoryUf*>( getInstantiator( theory::THEORY_UF ));
- // return new uf::EqualityQueryInstantiatorTheoryUf(ith);
- // }
- // inst::EqualityQuery* eq = d_eq_query_arr[id];
- // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
- // else return eq;
-
-
- //Currently we use the generic EqualityQuery
- return getEqualityQuery();
-}
-
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() {
- return new GenericCandidateGeneratorClasses(this);
-}
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() {
- return new GenericCandidateGeneratorClass(this);
-}
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) {
- // TheoryId id = Theory::theoryOf(t);
- // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses();
- // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses();
- // else return eq;
- return getRRCanGenClasses();
-}
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) {
- // TheoryId id = Theory::theoryOf(t);
- // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass();
- // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass();
- // else return eq;
- return getRRCanGenClass();
-}
class FirstOrderModel;
}/* CVC4::theory::quantifiers */
+namespace inst {
+ class TriggerTrie;
+}/* CVC4::theory::inst */
class QuantifiersEngine {
friend class quantifiers::InstantiationEngine;
/** phase requirements for each quantifier for each instantiation literal */
std::map< Node, QuantPhaseReq* > d_phase_reqs;
private:
- /** list of all quantifiers (pre-rewrite) */
+ /** list of all quantifiers seen */
std::vector< Node > d_quants;
- /** lemmas produced */
+ /** list of all lemmas produced */
std::map< Node, bool > d_lemmas_produced;
/** lemmas waiting */
std::vector< Node > d_lemmas_waiting;
/** has added lemma this round */
bool d_hasAddedLemma;
- /** inst matches produced for each quantifier */
+ /** list of all instantiations produced for each quantifier */
std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
- /** owner of quantifiers */
- std::map< Node, Theory* > d_owner;
/** term database */
quantifiers::TermDb* d_term_db;
+ /** all triggers will be stored in this trie */
+ inst::TriggerTrie* d_tr_trie;
/** extended model object */
quantifiers::FirstOrderModel* d_model;
private:
TheoryEngine* getTheoryEngine() { return d_te; }
/** get equality query object for the given type. The default is the
generic one */
- inst::EqualityQuery* getEqualityQuery(TypeNode t);
- inst::EqualityQuery* getEqualityQuery() { return d_eq_query; }
- /** get equality query object for the given type. The default is the
- one of UF */
- rrinst::CandidateGenerator* getRRCanGenClasses(TypeNode t);
- rrinst::CandidateGenerator* getRRCanGenClass(TypeNode t);
- /* generic candidate generator */
- rrinst::CandidateGenerator* getRRCanGenClasses();
- rrinst::CandidateGenerator* getRRCanGenClass();
+ EqualityQuery* getEqualityQuery() { return d_eq_query; }
/** get instantiation engine */
quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
/** get model engine */
Node getNextDecisionRequest();
/** reset instantiation round */
void resetInstantiationRound( Theory::Effort level );
-
- //create inst variable
- std::vector<Node> createInstVariable( std::vector<Node> & vars );
private:
/** compute term vector */
void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
/** instantiate f with arguments terms */
bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
+ /** set instantiation level attr */
+ void setInstantiationLevelAttr( Node n, uint64_t level );
public:
/** get instantiation */
Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
quantifiers::FirstOrderModel* getModel() { return d_model; }
/** get term database */
quantifiers::TermDb* getTermDatabase() { return d_term_db; }
+ /** get trigger database */
+ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
void addTermToDatabase( Node n, bool withinQuant = false );
public:
#include "theory/rewriterules/rr_trigger.h"
#include "theory/rewriterules/rr_inst_match_impl.h"
#include "theory/rewriterules/rr_candidate_generator.h"
+#include "theory/quantifiers/candidate_generator.h"
using namespace CVC4;
using namespace CVC4::kind;
//set-up d_variables, d_constants, d_childrens
for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){
- EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType());
+ //EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType());
+ EqualityQuery* q = qe->getEqualityQuery();
Assert( q != NULL );
if( d_pattern[i].hasAttribute(InstConstantAttribute()) ){
if( d_pattern[i].getKind()==INST_CONSTANT ){
EqualityQuery* d_q;
public:
VarMatcher(Node var, QuantifiersEngine* qe): d_var(var), d_binded(false){
- d_q = qe->getEqualityQuery(var.getType());
+ //d_q = qe->getEqualityQuery(var.getType());
+ d_q = qe->getEqualityQuery();
}
void resetInstantiationRound( QuantifiersEngine* qe ){};
bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){
public:
void mkCandidateGenerator(){
if(classes)
- d_cg = d_qe->getRRCanGenClasses();
+ d_cg = new GenericCandidateGeneratorClasses(d_qe);
else
- d_cg = d_qe->getRRCanGenClass();
+ d_cg = new GenericCandidateGeneratorClass(d_qe);
}
GenericCandidateGeneratorClasses(QuantifiersEngine* qe):
#include "context/cdlist.h"
#include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/term_database.h"
#include "expr/node_manager.h"
#include "expr/node_builder.h"
Node cand = cg->getNextCandidate();
//.......
}while( !cand.isNull() );
-
+
eqc is the equivalence class you are searching in
*/
virtual void reset( TNode eqc ) = 0;
InstMatchTrie2Gen<modEq>::InstMatchTrie2Gen(context::Context* c, QuantifiersEngine* qe):
d_context(c), d_mods(c) {
d_eQ = qe->getEqualityQuery();
- d_cG = qe->getRRCanGenClass();
+ d_cG = new GenericCandidateGeneratorClass(qe);
};
/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
rewriter::Subst & pvars,
rewriter::Subst & vars);
+ //create inst variable
+ std::vector<Node> createInstVariable( std::vector<Node> & vars );
+
/** statistics class */
class Statistics {
public:
vars.push_back(*v);
};
/* Instantiation version */
- std::vector<Node> inst_constants =
- getQuantifiersEngine()->createInstVariable(vars);
+ std::vector<Node> inst_constants = createInstVariable(vars);
/* Body/Remove_term/Guards/Triggers */
Node body = r[2][1];
TNode new_terms = r[2][1];
}
+std::vector<Node> TheoryRewriteRules::createInstVariable( std::vector<Node> & vars ){
+ std::vector<Node> inst_constant;
+ inst_constant.reserve(vars.size());
+ for( std::vector<Node>::const_iterator v = vars.begin();
+ v != vars.end(); ++v ){
+ //make instantiation constants
+ Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() );
+ inst_constant.push_back( ic );
+ };
+ return inst_constant;
+}
+
}/* CVC4::theory::rewriterules namespace */
}/* CVC4::theory namespace */
#include "theory/quantifiers/options.h"
#include "theory/rewriterules/options.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/candidate_generator.h"
using namespace std;
using namespace CVC4;
//take all terms from the uf term db and add to candidate generator
if( pats[0].getKind() == kind::INST_CONSTANT ){
TypeNode ty = pats[0].getType();
- rrinst::CandidateGenerator* cg = d_quantEngine->getRRCanGenClasses(ty);
+ rrinst::CandidateGenerator* cg = new GenericCandidateGeneratorClasses(d_quantEngine);
cg->reset(Node::null());
TNode c;
SetNode ele;
#include "util/statistics_registry.h"
#include "theory/uf/theory_uf.h"
#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/inst_match_generator.h"
#include "util/ntuple.h"
#include "context/cdqueue.h"
projects / cvc5.git / commitdiff