ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms, improvement for pre skolemization

9 files changed, 71 insertions, 23 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 85a96f90a..5a80512cd 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -140,7 +140,7 @@ void InstMatch::set(TNode var, TNode n){
   	//var.getType() == n.getType()
   	!n.getType().isSubtypeOf( var.getType() ) ){
     Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
-    Trace("inst-match-warn") << var << " " << var.getType() << n << " " << n.getType() << std::endl ;
+    Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
     Assert(false);
   }
   d_map[var] = n;
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 5484e25e9..dd8588b52 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -74,7 +74,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
     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 ){
+        if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
           InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy );
           d_children.push_back( cimg );
           d_children_index.push_back( i );
@@ -115,7 +115,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
       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 ) ){
+      if( !Trigger::isArithmeticTrigger( 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;
@@ -155,14 +155,20 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
     //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( !m.setMatch( q, d_match_pattern[i], t[i] ) ){
+        if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
+          Node vv = d_match_pattern[i];
+          Node tt = t[i];
+          if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
+            vv = d_match_pattern[i][0];
+            tt = NodeManager::currentNM()->mkConst(q->areEqual( tt, d_match_pattern[i][1] ));
+          }
+          if( !m.setMatch( q, vv, tt ) ){
             //match is in conflict
-            Debug("matching-debug") << "Match in conflict " << t[i] << " and "
-                                    << d_match_pattern[i] << " because "
-                                    << m.get(d_match_pattern[i])
+            Debug("matching-debug") << "Match in conflict " << tt << " and "
+                                    << vv << " because "
+                                    << m.get(vv)
                                     << std::endl;
-            Debug("matching-fail") << "Match fail: " << m.get(d_match_pattern[i]) << " and " << t[i] << std::endl;
+            Debug("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl;
             success = false;
             break;
           }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 3f5cc7666..0915f59a5 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -145,6 +145,10 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
     if( gen ){
       generateTriggers( f, effort, e, status );
     }
+    //if( e==4 ){
+    //  d_processed_trigger.clear();
+    //  d_quantEngine->getEqualityQuery()->setLiberal( true );
+    //}
     Debug("quant-uf-strategy")  << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
     //Notice() << "Try auto-generated triggers..." << std::endl;
     for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){
@@ -171,6 +175,9 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
         }
       }
     }
+    //if( e==4 ){
+    //  d_quantEngine->getEqualityQuery()->setLiberal( false );
+    //}
     Debug("quant-uf-strategy") << "done." << std::endl;
     //Notice() << "done" << std::endl;
     return status;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 7a3687dd5..222fc4425 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -36,7 +36,8 @@ option cnfQuant --cnf-quant bool :default false
 #   forall x. P( x ) => f( S( x ) ) = x
 option preSkolemQuant --pre-skolem-quant bool :default false
  apply skolemization eagerly to bodies of quantified formulas
-
+option iteRemoveQuant --ite-remove-quant bool :default false
+ apply ite removal to bodies of quantifiers
 # Whether to perform agressive miniscoping
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
@@ -48,7 +49,7 @@ option macrosQuant --macros-quant bool :default false
 option smartTriggers /--disable-smart-triggers bool :default true
  disable smart triggers
 # Whether to use relevent triggers
-option relevantTriggers --relevant-triggers bool :default true
+option relevantTriggers /--disable-relevant-triggers bool :default true
  prefer triggers that are more relevant based on SInE style analysis
 
 # Whether to consider terms in the bodies of quantifiers for matching
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 85602dbab..0b4f2654b 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -91,6 +91,8 @@ public:
   virtual eq::EqualityEngine* getEngine() = 0;
   /** get the equivalence class of a */
   virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
+
+  virtual void setLiberal( bool l ) = 0;
 };/* class EqualityQuery */
 
 }
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index cff28f243..125829e06 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -226,17 +226,24 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
 
 bool Trigger::isUsable( Node n, Node f ){
   if( n.getAttribute(InstConstantAttribute())==f ){
-    if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
-      std::map< Node, Node > coeffs;
-      return getPatternArithmetic( f, n, coeffs );
-    }else{
+    if( isAtomicTrigger( n ) ){
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
         if( !isUsable( n[i], f ) ){
           return false;
         }
       }
       return true;
+    }else if( n.getKind()==INST_CONSTANT ){
+      return true;
+    }else{
+      std::map< Node, Node > coeffs;
+      if( isArithmeticTrigger( f, n, coeffs ) ){
+        return true;
+      }else if( isBooleanTermTrigger( n ) ){
+        return true;
+      }
     }
+    return false;
   }else{
     return true;
   }
@@ -368,7 +375,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
   }
 }
 
-bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){
+bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ){
   if( n.getKind()==PLUS ){
     Assert( coeffs.empty() );
     NodeBuilder<> t(kind::PLUS);
@@ -381,7 +388,7 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
             coeffs.clear();
             return false;
           }
-        }else if( !getPatternArithmetic( f, n[i], coeffs ) ){
+        }else if( !isArithmeticTrigger( f, n[i], coeffs ) ){
           coeffs.clear();
           return false;
         }
@@ -413,6 +420,22 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
   return false;
 }
 
+bool Trigger::isBooleanTermTrigger( Node n ) {
+  if( n.getKind()==ITE ){
+    //check for boolean term converted to ITE
+    if( n[0].getKind()==INST_CONSTANT &&
+        n[1].getKind()==CONST_BITVECTOR &&
+        n[2].getKind()==CONST_BITVECTOR ){
+      if( ((BitVectorType)n[1].getType().toType()).getSize()==1 &&
+          n[1].getConst<BitVector>().toInteger()==1 &&
+          n[2].getConst<BitVector>().toInteger()==0 ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
 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 93731283b..9ecac0120 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -109,7 +109,8 @@ public:
   static bool isAtomicTrigger( Node n );
   static bool isSimpleTrigger( Node n );
   /** get pattern arithmetic */
-  static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs );
+  static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs );
+  static bool isBooleanTermTrigger( Node n );
 
   inline void toStream(std::ostream& out) const {
     out << "TRIGGER( ";
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a11cc85c0..f12143bbe 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -583,12 +583,16 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
     return true;
   }else{
     eq::EqualityEngine* ee = getEngine();
-    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-      if( ee->areEqual( a, b ) ){
-        return true;
+    if( d_liberal ){
+      return true;//!areDisequal( a, b );
+    }else{
+      if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+        if( ee->areEqual( a, b ) ){
+          return true;
+        }
       }
+      return false;
     }
-    return false;
   }
 }
 
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 9f520f420..5f288a186 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -272,6 +272,8 @@ private:
   std::map< Node, int > d_rep_score;
   /** reset count */
   int d_reset_count;
+
+  bool d_liberal;
 private:
   /** node contains */
   Node getInstance( Node n, std::vector< Node >& eqc );
@@ -280,7 +282,7 @@ private:
   /** choose rep based on sort inference */
   bool optInternalRepSortInference();
 public:
-  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
+  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
   ~EqualityQueryQuantifiersEngine(){}
   /** reset */
   void reset();
@@ -296,6 +298,8 @@ public:
       not contain instantiation constants, if such a term exists.
    */
   Node getInternalRepresentative( Node a, Node f, int index );
+
+  void setLiberal( bool l ) { d_liberal = l; }
 }; /* EqualityQueryQuantifiersEngine */
 
 }/* CVC4::theory namespace */