New option --purify-triggers. Refactoring of InstMatchGenerator.

6 files changed, 230 insertions, 49 deletions

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 6faa5ffca..6dbe1ec42 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -30,14 +30,21 @@ namespace CVC4 {
 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){
@@ -89,24 +96,28 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
     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
@@ -139,15 +150,6 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
       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());
-      }
-    }
   }
 }
 
@@ -157,6 +159,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
                     << 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();
@@ -171,23 +174,19 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
     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
@@ -239,15 +238,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
         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 );
@@ -259,6 +250,18 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
   }
 }
 
+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() ){
@@ -384,6 +387,54 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( std::vector< Node
   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 ){
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 56eaf2c17..aa5d37713 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -42,7 +42,7 @@ public:
   /** 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 */
@@ -50,7 +50,7 @@ public:
 class CandidateGenerator;
 
 class InstMatchGenerator : public IMGenerator {
-private:
+protected:
   bool d_needsReset;
   /** candidate generator */
   CandidateGenerator* d_cg;
@@ -63,17 +63,18 @@ private:
   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,
   };
@@ -85,7 +86,8 @@ public:
   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.
@@ -115,6 +117,39 @@ public:
   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:
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index bdd852adb..f33f1ce83 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -63,6 +63,8 @@ option relevantTriggers --relevant-triggers bool :default false
  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
 
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index c6ee48057..856ac782c 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){
 
 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 ) {
@@ -503,6 +503,93 @@ bool Trigger::isBooleanTermTrigger( Node n ) {
   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;
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 17da6f0d5..42b7598ea 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -30,6 +30,7 @@ class QuantifiersEngine;
 namespace inst {
 
 class IMGenerator;
+class InstMatchGenerator;
 
 //a collect of nodes representing a trigger
 class Trigger {
@@ -112,6 +113,10 @@ public:
   /** 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 {
     /*
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e54dfe42f..03143ab9c 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -664,6 +664,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
 
 
   //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 ){