Add term db mode. Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches. Minor cleanup.

10 files changed, 189 insertions, 80 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index a05c7010b..453f8eb7f 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1110,6 +1110,7 @@ void TheoryDatatypes::computeCareGraph(){
                 TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
                 Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
                 EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
+                Trace("dt-cg") << "...eq status is " << eqStatus << std::endl;
                 if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
                   somePairIsDisequal = true;
                   break;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 02536eb99..8a0ec3c09 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -173,7 +173,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       if( gen ){
         generateTriggers( f, effort, e, status );
         if( d_auto_gen_trigger[f].empty() && f.getNumChildren()==2 ){
-          Trace("no-trigger") << "Could not find trigger for " << f << std::endl;
+          Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
         }
       }
 
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 80dbb783e..5e692ace1 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -132,6 +132,13 @@ typedef enum {
   CEGQI_FAIR_NONE,
 } CegqiFairMode;
 
+typedef enum {
+  /** consider all terms in master equality engine */
+  TERM_DB_ALL,
+  /** consider only relevant terms */
+  TERM_DB_RELEVANT,
+} TermDbMode;
+
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 97a43a96d..f4f1bcd86 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -29,6 +29,8 @@ option varElimQuant /--disable-var-elim-quant bool :default true
 option dtVarExpandQuant --dt-var-exp-quant bool :default true
  expand datatype variables bound to one constructor in quantifiers
 
+option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
+ split variables occurring as conditions of ITE in quantifiers
 option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
  disable simple ite lifting for quantified formulas
 
@@ -57,6 +59,8 @@ option macrosQuant --macros-quant bool :default false
 option foPropQuant --fo-prop-quant bool :default false
  perform first-order propagation on quantifiers
 
+option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler  CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h"
+ which ground terms to consider for instantiation
 # Whether to use smart triggers
 option smartTriggers /--disable-smart-triggers bool :default true
  disable smart triggers
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index e00879303..08fcf319d 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -188,6 +188,16 @@ none \n\
 + Do not enforce fairness. \n\
 \n\
 ";
+static const std::string termDbModeHelp = "\
+Modes for term database, supported by --term-db-mode:\n\
+\n\
+all  \n\
++ Consider all terms in the system.\n\
+\n\
+relevant \n\
++ Consider only terms connected to current assertions. \n\
+\n\
+";
 
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
@@ -380,6 +390,20 @@ inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optar
   }
 }
 
+inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "all" ) {
+    return TERM_DB_ALL;
+  } else if(optarg == "relevant") {
+    return TERM_DB_RELEVANT;
+  } else if(optarg ==  "help") {
+    puts(termDbModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --term-db-mode: `") +
+                          optarg + "'.  Try --term-db-mode help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index b39d7fff6..62a87bb99 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -241,6 +241,7 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int
 }
 
 void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
+  Assert( n.getKind()!=IMPLIES && n.getKind()!=XOR );
   newHasPol = hasPol;
   newPol = pol;
   if( n.getKind()==NOT ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0d338f283..0ed175393 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -131,7 +131,7 @@ bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
   if( std::find( args.begin(), args.end(), n )!=args.end() ){
     return true;
   }else{
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( hasArg( args, n[i] ) ){
         return true;
       }
@@ -140,6 +140,19 @@ bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
   }
 }
 
+bool QuantifiersRewriter::hasArg1( Node a, Node n ) {
+  if( n==a ){
+    return true;
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( hasArg1( a, n[i] ) ){
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
 void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){
   std::vector< Node > processed;
   setNestedQuantifiers2( n, q, processed );
@@ -335,43 +348,88 @@ Node QuantifiersRewriter::computeNNF( Node body ){
   }
 }
 
-Node QuantifiersRewriter::computeSimpleIteLift( Node body ) {
-  if( body.getKind()==EQUAL ){
-    for( size_t i=0; i<2; i++ ){
-      if( body[i].getKind()==ITE ){
-        Node no = i==0 ? body[1] : body[0];
-        bool doRewrite = false;
-        std::vector< Node > children;
-        children.push_back( body[i][0] );
-        for( size_t j=1; j<=2; j++ ){
-          //check if it rewrites to a constant
-          Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
-          nn = Rewriter::rewrite( nn );
-          children.push_back( nn );
-          if( nn.isConst() ){
-            doRewrite = true;
+Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) {
+  if( body.getType().isBoolean() ){
+    if( body.getKind()==EQUAL && options::simpleIteLiftQuant() ){
+      for( size_t i=0; i<2; i++ ){
+        if( body[i].getKind()==ITE ){
+          Node no = i==0 ? body[1] : body[0];
+          bool doRewrite = false;
+          std::vector< Node > children;
+          children.push_back( body[i][0] );
+          for( size_t j=1; j<=2; j++ ){
+            //check if it rewrites to a constant
+            Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
+            nn = Rewriter::rewrite( nn );
+            children.push_back( nn );
+            if( nn.isConst() ){
+              doRewrite = true;
+            }
+          }
+          if( doRewrite ){
+            return NodeManager::currentNM()->mkNode( ITE, children );
           }
         }
-        if( doRewrite ){
-          return NodeManager::currentNM()->mkNode( ITE, children );
+      }
+    }else if( body.getKind()==ITE && hasPol && options::iteCondVarSplitQuant() ){
+      for( unsigned r=0; r<2; r++ ){
+        //check if there is a variable elimination
+        Node b = r==0 ? body[0] : body[0].negate();
+        QuantPhaseReq qpr( b );
+        std::vector< Node > vars;
+        std::vector< Node > subs;
+        Trace("ite-var-split-quant") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
+        for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
+          Trace("ite-var-split-quant") << "phase req " << it->first << " -> " << it->second << std::endl;
+          if( it->second ){
+            if( it->first.getKind()==EQUAL ){
+              for( unsigned i=0; i<2; i++ ){
+                if( it->first[i].getKind()==BOUND_VARIABLE ){
+                  unsigned j = i==0 ? 1 : 0;
+                  if( !hasArg1( it->first[i], it->first[j] ) ){
+                    vars.push_back( it->first[i] );
+                    subs.push_back( it->first[j] );
+                    break;
+                  }
+                }
+              }
+            }
+          }
+        }
+        if( !vars.empty() ){
+          //bool cpol = (r==1);
+          Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+          //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+          //pos = Rewriter::rewrite( pos );
+          Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
+          //Trace("ite-var-split-quant") << "Split ITE " << body << " into : " << std::endl;
+          //Trace("ite-var-split-quant") << "   " << pos << std::endl;
+          //Trace("ite-var-split-quant") << "   " << neg << std::endl;
+          return NodeManager::currentNM()->mkNode( AND, pos, neg );
         }
       }
     }
-  }else if( body.getKind()!=APPLY_UF && body.getType()==NodeManager::currentNM()->booleanType() ){
-    bool changed = false;
-    std::vector< Node > children;
-    for( size_t i=0; i<body.getNumChildren(); i++ ){
-      Node nn = computeSimpleIteLift( body[i] );
-      children.push_back( nn );
-      changed = changed || nn!=body[i];
-    }
-    if( changed ){
-      return NodeManager::currentNM()->mkNode( body.getKind(), children );
+    if( body.getKind()!=EQUAL && body.getKind()!=APPLY_UF ){
+      bool changed = false;
+      std::vector< Node > children;
+      for( size_t i=0; i<body.getNumChildren(); i++ ){
+        bool newHasPol;
+        bool newPol;
+        QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+        Node nn = computeProcessIte( body[i], newHasPol, newPol );
+        children.push_back( nn );
+        changed = changed || nn!=body[i];
+      }
+      if( changed ){
+        return NodeManager::currentNM()->mkNode( body.getKind(), children );
+      }
     }
   }
   return body;
 }
 
+
+
 Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
   Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
   QuantPhaseReq qpr( body );
@@ -385,9 +443,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
           int j = i==0 ? 1 : 0;
           std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
           if( ita!=args.end() ){
-            std::vector< Node > temp;
-            temp.push_back( it->first[i] );
-            if( !hasArg( temp, it->first[j] ) ){
+            if( !hasArg1( it->first[i], it->first[j] ) ){
               vars.push_back( it->first[i] );
               subs.push_back( it->first[j] );
               args.erase( ita );
@@ -607,18 +663,22 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
     }else{
       return body;
     }
-  }else if( body.getKind()==ITE || body.getKind()==XOR || body.getKind()==IFF ){
-    return body;
   }else{
     Assert( body.getKind()!=EXISTS );
     bool childrenChanged = false;
     std::vector< Node > newChildren;
     for( int i=0; i<(int)body.getNumChildren(); i++ ){
-      bool newPol = body.getKind()==NOT  ? !pol : pol;
-      Node n = computePrenex( body[i], args, newPol );
-      newChildren.push_back( n );
-      if( n!=body[i] ){
-        childrenChanged = true;
+      bool newHasPol;
+      bool newPol;
+      QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
+      if( newHasPol ){
+        Node n = computePrenex( body[i], args, newPol );
+        newChildren.push_back( n );
+        if( n!=body[i] ){
+          childrenChanged = true;
+        }
+      }else{
+        newChildren.push_back( body[i] );
       }
     }
     if( childrenChanged ){
@@ -959,8 +1019,8 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
     return options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_NNF ){
     return options::nnfQuant();
-  }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
-    return options::simpleIteLiftQuant();
+  }else if( computeOption==COMPUTE_PROCESS_ITE ){
+    return options::iteCondVarSplitQuant() || options::simpleIteLiftQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
@@ -997,8 +1057,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
       return computeAggressiveMiniscoping( args, n, isNested );
     }else if( computeOption==COMPUTE_NNF ){
       n = computeNNF( n );
-    }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
-      n = computeSimpleIteLift( n );
+    }else if( computeOption==COMPUTE_PROCESS_ITE ){
+      n = computeProcessIte( n, true, true );
     }else if( computeOption==COMPUTE_PRENEX ){
       n = computePrenex( n, args, true );
     }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 901a47f79..badf97c46 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -42,6 +42,7 @@ private:
   static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
   static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
   static bool hasArg( std::vector< Node >& args, Node n );
+  static bool hasArg1( Node a, Node n );
   static void setNestedQuantifiers( Node n, Node q );
   static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed );
   static Node computeClause( Node n );
@@ -51,7 +52,7 @@ private:
   static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested = false );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false );
   static Node computeNNF( Node body );
-  static Node computeSimpleIteLift( Node body );
+  static Node computeProcessIte( Node body, bool hasPol, bool pol );
   static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
@@ -62,7 +63,7 @@ private:
     COMPUTE_MINISCOPING,
     COMPUTE_AGGRESSIVE_MINISCOPING,
     COMPUTE_NNF,
-    COMPUTE_SIMPLE_ITE_LIFT,
+    COMPUTE_PROCESS_ITE,
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
     //COMPUTE_FLATTEN_ARGS_UF,
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 4979a3dfd..9e7d14b9a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -316,10 +316,16 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   return false;
 }
 
-bool TermDb::hasTermCurrent( Node n ) { 
+bool TermDb::hasTermCurrent( Node n ) {
   //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n );
-  //return d_has_map.find( n )!=d_has_map.end(); 
-  return true;
+  if( options::termDbMode()==TERM_DB_ALL ){
+    return true;
+  }else if( options::termDbMode()==TERM_DB_RELEVANT ){
+    return d_has_map.find( n )!=d_has_map.end();
+  }else{
+    Assert( false );
+    return false;
+  }
 }
 
 void TermDb::setHasTerm( Node n ) {
@@ -348,44 +354,44 @@ void TermDb::reset( Theory::Effort effort ){
   d_func_map_eqc_trie.clear();
 
   //compute has map
-  /*
-  d_has_map.clear();
-  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
-  while( !eqcs_i.isFinished() ){
-    TNode r = (*eqcs_i);
-    bool addedFirst = false;
-    Node first;
-    //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-    while( !eqc_i.isFinished() ){
-      TNode n = (*eqc_i);
-      if( first.isNull() ){
-        first = n;
-      }else{
-        if( !addedFirst ){
-          addedFirst = true;
-          setHasTerm( first );
+  if( options::termDbMode()==TERM_DB_RELEVANT ){
+    d_has_map.clear();
+    eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+    while( !eqcs_i.isFinished() ){
+      TNode r = (*eqcs_i);
+      bool addedFirst = false;
+      Node first;
+      //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+      while( !eqc_i.isFinished() ){
+        TNode n = (*eqc_i);
+        if( first.isNull() ){
+          first = n;
+        }else{
+          if( !addedFirst ){
+            addedFirst = true;
+            setHasTerm( first );
+          }
+          setHasTerm( n );
         }
-        setHasTerm( n );
+        ++eqc_i;
       }
-      ++eqc_i;
+      ++eqcs_i;
     }
-    ++eqcs_i;
-  }
-  for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
-    Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId];
-    if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
-      context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
-      for (unsigned i = 0; it != it_end; ++ it, ++i) {
-        Trace("ajr-temp") << "Set has term " << (*it).assertion << std::endl;
-        setHasTerm( (*it).assertion );
+    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
+      Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId];
+      if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
+        context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+        for (unsigned i = 0; it != it_end; ++ it, ++i) {
+          Trace("ajr-temp") << "Set has term " << (*it).assertion << std::endl;
+          setHasTerm( (*it).assertion );
+        }
       }
     }
   }
-  */
-  
-  
+
+
   //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_nonred_count[ it->first ] = 0;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e589e8f87..136c0409f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -83,6 +83,10 @@ namespace theory {
     class EqualityEngine;
   }/* CVC4::theory::eq namespace */
 
+  namespace quantifiers {
+    class TermDb;
+  }
+
   class EntailmentCheckParameters;
   class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
@@ -101,6 +105,7 @@ class TheoryEngine {
 
   /** Shared terms database can use the internals notify the theories */
   friend class SharedTermsDatabase;
+  friend class theory::quantifiers::TermDb;
 
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;