namespace theory {
namespace inst {
-
-InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPolicy( matchPolicy ){
+InstMatchGenerator::InstMatchGenerator( Node pat ){
d_needsReset = true;
d_active_add = false;
Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
d_pattern = pat;
d_match_pattern = pat;
d_next = NULL;
+ d_matchPolicy = MATCH_GEN_DEFAULT;
+}
+
+InstMatchGenerator::InstMatchGenerator() {
+ d_needsReset = true;
+ d_active_add = false;
+ d_next = NULL;
+ d_matchPolicy = MATCH_GEN_DEFAULT;
}
void InstMatchGenerator::setActiveAdd(bool val){
d_match_pattern_op = qe->getTermDatabase()->getOperator( d_match_pattern );
//now, collect children of d_match_pattern
- int childMatchPolicy = MATCH_GEN_DEFAULT;
+ //int childMatchPolicy = MATCH_GEN_DEFAULT;
for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){
- if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
- InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy );
+ InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( d_match_pattern[i] );
+ if( cimg ){
d_children.push_back( cimg );
d_children_index.push_back( i );
gens.push_back( cimg );
+ d_children_types.push_back( 1 );
+ }else{
+ d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
+ d_children_types.push_back( 0 );
}
+ }else{
+ d_children_types.push_back( -1 );
}
}
//create candidate generator
if( d_match_pattern.getKind()==INST_CONSTANT ){
d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
- }
- else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
- Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
+ }else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
//we will be producing candidates via literal matching heuristics
if( d_pattern.getKind()!=NOT ){
//candidates will be all equalities
Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
}
- for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
- if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
- Node vv = d_match_pattern[i];
- if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
- vv = d_match_pattern[i][0];
- }
- d_var_num[i] = vv.getAttribute(InstVarNumAttribute());
- }
- }
}
}
<< m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
Assert( !d_match_pattern.isNull() );
if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){
+ Trace("matching-fail") << "Internal error for match generator." << std::endl;
return false;
}else{
EqualityQuery* q = qe->getEqualityQuery();
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( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){
- if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
- Node tt = t[i];
- if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
- tt = NodeManager::currentNM()->mkConst(q->areEqual( tt, d_match_pattern[i][1] ));
- }
- bool addToPrev = m.get( d_var_num[i] ).isNull();
- if( !m.set( qe, d_var_num[i], tt ) ){
- //match is in conflict
- Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << tt << std::endl;
- success = false;
- break;
- }else if( addToPrev ){
- prev.push_back( d_var_num[i] );
- }
+ if( d_children_types[i]==0 ){
+ Trace("matching-debug2") << "Setting " << d_var_num[i] << " to " << t[i] << "..." << std::endl;
+ bool addToPrev = m.get( d_var_num[i] ).isNull();
+ if( !m.set( qe, d_var_num[i], t[i] ) ){
+ //match is in conflict
+ Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << t[i] << std::endl;
+ success = false;
+ break;
+ }else if( addToPrev ){
+ Trace("matching-debug2") << "Success." << std::endl;
+ prev.push_back( d_var_num[i] );
}
- }else{
+ }else if( d_children_types[i]==-1 ){
if( !q->areEqual( d_match_pattern[i], t[i] ) ){
Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
//ground arguments are not equal
Node rep = q->getRepresentative( t[ d_children_index[i] ] );
d_children[i]->reset( rep, qe );
}
- if( d_next!=NULL ){
- success = d_next->getNextMatch( f, m, qe );
- }else{
- if( d_active_add ){
- Trace("active-add") << "Active Adding instantiation " << m << std::endl;
- success = qe->addInstantiation( f, m, false );
- Trace("active-add") << "Success = " << success << std::endl;
- }
- }
+ success = continueNextMatch( f, m, qe );
}
if( !success ){
//m = InstMatch( &prev );
}
}
+bool InstMatchGenerator::continueNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
+ if( d_next!=NULL ){
+ return d_next->getNextMatch( f, m, qe );
+ }else{
+ if( d_active_add ){
+ return qe->addInstantiation( f, m, false );
+ }else{
+ return true;
+ }
+ }
+}
+
/** reset instantiation round */
void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
if( !d_match_pattern.isNull() ){
return oinit;
}
+VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) :
+ InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) {
+ d_var_num[0] = var.getAttribute(InstVarNumAttribute());
+}
+
+bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) {
+ if( !d_eq_class.isNull() ){
+ Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern ));
+ d_eq_class = Node::null();
+ d_rm_prev = m.get( d_var_num[0] ).isNull();
+ if( !m.set( qe, d_var_num[0], s ) ){
+ return false;
+ }else{
+ return continueNextMatch( f, m, qe );
+ }
+ }else{
+ if( d_rm_prev ){
+ m.d_vals[d_var_num[0]] = Node::null();
+ }
+ return false;
+ }
+}
+
+VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
+ InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){
+ d_var_num[0] = d_var.getAttribute(InstVarNumAttribute());
+}
+
+bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) {
+ if( !d_eq_class.isNull() ){
+ Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl;
+ Node s = d_subs.substitute( d_var, d_eq_class );
+ Trace("var-trigger-matching") << "...got " << s << std::endl;
+ d_eq_class = Node::null();
+ d_rm_prev = m.get( d_var_num[0] ).isNull();
+ if( !m.set( qe, d_var_num[0], s ) ){
+ return false;
+ }else{
+ return continueNextMatch( f, m, qe );
+ }
+ }else{
+ if( d_rm_prev ){
+ m.d_vals[d_var_num[0]] = Node::null();
+ }
+ return false;
+ }
+}
+
/** constructors */
InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :
d_f( f ){
/** 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;
+ virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) { return 0; }
/** set active add */
virtual void setActiveAdd( bool val ) {}
};/* class IMGenerator */
class CandidateGenerator;
class InstMatchGenerator : public IMGenerator {
-private:
+protected:
bool d_needsReset;
/** candidate generator */
CandidateGenerator* d_cg;
InstMatchGenerator* d_next;
/** eq class */
Node d_eq_class;
- /** for arithmetic matching */
- std::map< Node, Node > d_arith_coeffs;
/** variable numbers */
std::map< int, int > d_var_num;
/** initialize pattern */
void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens );
+ /** children types 0 : variable, 1 : child term, -1 : ground term */
+ std::vector< int > d_children_types;
+ /** continue */
+ bool continueNextMatch( Node f, InstMatch& m, 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_ERROR,
};
bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe );
/** constructors */
- InstMatchGenerator( Node pat, int matchOption = 0 );
+ InstMatchGenerator( Node pat );
+ InstMatchGenerator();
/** destructor */
~InstMatchGenerator(){}
/** The pattern we are producing matches for.
static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe );
};/* class InstMatchGenerator */
+//match generator for boolean term ITEs
+class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
+public:
+ VarMatchGeneratorBooleanTerm( Node var, Node comp );
+ Node d_comp;
+ bool d_rm_prev;
+ /** reset instantiation round (call this at beginning of instantiation round) */
+ void resetInstantiationRound( QuantifiersEngine* qe ){}
+ /** reset, eqc is the equivalence class to search in (any if eqc=null) */
+ void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; }
+ /** get the next match. must call reset( eqc ) before this function. */
+ bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+ /** add instantiations directly */
+ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; }
+};
+
+//match generator for purified terms (matched term is substituted into d_subs)
+class VarMatchGeneratorTermSubs : public InstMatchGenerator {
+public:
+ VarMatchGeneratorTermSubs( Node var, Node subs );
+ TNode d_var;
+ Node d_subs;
+ bool d_rm_prev;
+ /** reset instantiation round (call this at beginning of instantiation round) */
+ void resetInstantiationRound( QuantifiersEngine* qe ){}
+ /** reset, eqc is the equivalence class to search in (any if eqc=null) */
+ void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; }
+ /** get the next match. must call reset( eqc ) before this function. */
+ bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+ /** add instantiations directly */
+ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; }
+};
+
/** smart multi-trigger implementation */
class InstMatchGeneratorMulti : public IMGenerator {
private:
prefer triggers that are more relevant based on SInE style analysis
option relationalTriggers --relational-triggers bool :default false
choose relational triggers such as x = f(y), x >= f(y)
+option purifyTriggers --purify-triggers bool :default false
+ purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1
option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h"
selection mode for triggers
bool Trigger::isAtomicTrigger( Node n ){
Kind k = n.getKind();
- return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) ||
+ return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) ||
( k!=APPLY_UF && isAtomicTriggerKind( k ) );
}
bool Trigger::isAtomicTriggerKind( Kind k ) {
return false;
}
+Node Trigger::getInversionVariable( Node n ) {
+ if( n.getKind()==INST_CONSTANT ){
+ return n;
+ }else if( n.getKind()==PLUS || n.getKind()==MULT ){
+ Node ret;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){
+ if( ret.isNull() ){
+ ret = getInversionVariable( n[i] );
+ if( ret.isNull() ){
+ Trace("var-trigger-debug") << "No : multiple variables " << n << std::endl;
+ return Node::null();
+ }
+ }else{
+ return Node::null();
+ }
+ }else if( n.getKind()==MULT ){
+ if( !n[i].isConst() ){
+ Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
+ return Node::null();
+ }else if( n.getType().isInteger() ){
+ Rational r = n[i].getConst<Rational>();
+ if( r!=Rational(-1) && r!=Rational(1) ){
+ Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl;
+ return Node::null();
+ }
+ }
+ }
+ }
+ return ret;
+ }else{
+ Trace("var-trigger-debug") << "No : unsupported operator " << n << "." << std::endl;
+ }
+ return Node::null();
+}
+
+Node Trigger::getInversion( Node n, Node x ) {
+ if( n.getKind()==INST_CONSTANT ){
+ return x;
+ }else if( n.getKind()==PLUS || n.getKind()==MULT ){
+ int cindex = -1;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !quantifiers::TermDb::hasInstConstAttr(n[i]) ){
+ if( n.getKind()==PLUS ){
+ x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
+ }else if( n.getKind()==MULT ){
+ Assert( n[i].isConst() );
+ Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
+ x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
+ }
+ }else{
+ Assert( cindex==-1 );
+ cindex = i;
+ }
+ }
+ Assert( cindex!=-1 );
+ return getInversion( n[cindex], x );
+ }
+ return Node::null();
+}
+
+InstMatchGenerator* Trigger::getInstMatchGenerator( Node n ) {
+ if( n.getKind()==INST_CONSTANT ){
+ return NULL;
+ }else{
+ Trace("var-trigger-debug") << "Is " << n << " a variable trigger?" << std::endl;
+ if( isBooleanTermTrigger( n ) ){
+ VarMatchGeneratorBooleanTerm* vmg = new VarMatchGeneratorBooleanTerm( n[0], n[1] );
+ Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0] << std::endl;
+ return vmg;
+ }else{
+ Node x;
+ if( options::purifyTriggers() ){
+ x = getInversionVariable( n );
+ }
+ if( !x.isNull() ){
+ Node s = getInversion( n, x );
+ VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs( x, s );
+ Trace("var-trigger") << "Term substitution trigger : " << n << ", var = " << x << ", subs = " << s << std::endl;
+ return vmg;
+ }else{
+ return new InstMatchGenerator( n );
+ }
+ }
+ }
+}
+
Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
if( nodes.empty() ){
return d_tr;
namespace inst {
class IMGenerator;
+class InstMatchGenerator;
//a collect of nodes representing a trigger
class Trigger {
/** get pattern arithmetic */
static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs );
static bool isBooleanTermTrigger( Node n );
+ /** return data structure for producing matches for this trigger. */
+ static InstMatchGenerator* getInstMatchGenerator( Node n );
+ static Node getInversionVariable( Node n );
+ static Node getInversion( Node n, Node x );
inline void toStream(std::ostream& out) const {
/*
//add the instantiation
+ Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
//report the result
if( addedInst ){
projects / cvc5.git / commitdiff