Add options --partial-triggers, --elim-taut-quant, improve robustness of --purify-triggers. Enable --quant-alpha-equiv by default. Fix fairness issue when combining cbqi+E-matching. Avoid unecessary delta lemmas. Update casc scripts.

12 files changed, 82 insertions, 23 deletions

diff --git a/contrib/run-script-casc25-fof b/contrib/run-script-casc25-fof
index 7717abe47..26c544062 100755
--- a/contrib/run-script-casc25-fof
+++ b/contrib/run-script-casc25-fof
@@ -15,7 +15,7 @@ echo "------- cvc4-fof casc 25 : $bench at $2..."
 function trywith {
   limit=$1; shift;
   echo "--- Run $@ at $limit...";
-  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump --quant-alpha-equiv "$@" $bench) 2>/dev/null |
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
   (read w1 w2 w3 result w4 w5;
   case "$result" in
   Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
@@ -25,7 +25,7 @@ function trywith {
 }
 function finishwith {
   echo "--- Run $@...";
-  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump --quant-alpha-equiv "$@" $bench
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
 }
 
 # designed for 300 seconds
diff --git a/contrib/run-script-casc25-tfa b/contrib/run-script-casc25-tfa
index 463b5396e..40ed76df5 100644
--- a/contrib/run-script-casc25-tfa
+++ b/contrib/run-script-casc25-tfa
@@ -29,11 +29,12 @@ function finishwith {
 }
 
 trywith 10 --cbqi2 --decision=internal --full-saturate-quant
-trywith 10 --relevant-triggers --full-saturate-quant
+trywith 10 --relevant-triggers --full-saturate-quant --partial-triggers --purify-triggers
 trywith 10 --cbqi --full-saturate-quant
+trywith 10 --cbqi2 --e-matching  --partial-triggers --purify-triggers
 trywith 30 --qcf-tconstraint --full-saturate-quant
 trywith 60 --cbqi --cbqi-recurse --full-saturate-quant
-trywith 10 --full-saturate-quant
+trywith 10 --full-saturate-quant --partial-triggers --purify-triggers
 trywith 10 --no-e-matching --full-saturate-quant
 trywith 10 --fmf-bound-int
 finishwith --cbqi2 --cbqi-recurse --full-saturate-quant
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 54c97750a..921583ed2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -771,7 +771,7 @@ void SmtEngine::finishInit() {
     // Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
     LogicInfo everything;
     everything.lock();
-    Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, \"all-supported\" logic (below), as some internals might require the use of a logic more general than the input.")
+    Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.")
                       << SetBenchmarkLogicCommand(everything.getLogicString());
   }
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 8e7e3d69c..0a434e4ca 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -538,6 +538,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
         d_qe->getOutputChannel().lemma( delta_lem );
       }
       subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta );
+      d_used_delta = true;
     }
   }
   //check if we have already added this instantiation
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index eb99fc4f6..eb33c479e 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -71,6 +71,7 @@ public:
   std::vector< Node > d_vars;
   //delta
   Node d_n_delta;
+  bool d_used_delta;
   //check : add instantiations based on valuation of d_vars
   bool check();
   // get delta lemmas : on-demand force minimality of d_n_delta
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 941eaf89b..f7dc709d9 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -463,13 +463,17 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE
     s = Rewriter::rewrite( s );
     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{
-      if( continueNextMatch( f, m, qe ) ){
-        return true;
+    if( s.getType().isSubtypeOf( d_var.getType() ) ){
+      d_rm_prev = m.get( d_var_num[0] ).isNull();
+      if( !m.set( qe, d_var_num[0], s ) ){
+        return false;
+      }else{
+        if( continueNextMatch( f, m, qe ) ){
+          return true;
+        }
       }
+    }else{
+      Trace("var-trigger-matching") << "Violates type requirement." << std::endl;
     }
   }
   if( d_rm_prev ){
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index de80146f9..dab32af71 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -126,9 +126,9 @@ void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<
 }
 
 int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
-  if( e<2 ){
+  if( e<1 ){
     return STATUS_UNFINISHED;
-  }else if( e==2 ){
+  }else if( e==1 ){
     if( d_quantActive.find( f )!=d_quantActive.end() ){
       //the point instantiation
       InstMatch m_point( f );
@@ -373,9 +373,9 @@ void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort )
 }
 
 int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
-  if( e<2 ){
+  if( e<1 ){
     return STATUS_UNFINISHED;
-  }else if( e==2 ){
+  }else if( e==1 ){
     CegInstantiator * cinst;
     std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
     if( it==d_cinst.end() ){
@@ -417,10 +417,11 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
     Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
     d_curr_quant = f;
     bool addedLemma = cinst->check();
+    d_used_delta = d_used_delta || cinst->d_used_delta;
     d_curr_quant = Node::null();
     return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED;
-  }else if( e==3 ){
-    if( d_check_delta_lemma_lc ){
+  }else if( e==2 ){
+    if( d_check_delta_lemma_lc && d_used_delta ){
       d_check_delta_lemma_lc = false;
       d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub );
       d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub );
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 13e8cf54b..d59690c84 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -104,6 +104,7 @@ private:
   Node d_curr_quant;
   bool d_check_delta_lemma;
   bool d_check_delta_lemma_lc;
+  bool d_used_delta;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
   int process( Node f, Theory::Effort effort, int e );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 231392a9a..ce7f01328 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -57,6 +57,9 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
 # Whether to perform quantifier macro expansion
 option macrosQuant --macros-quant bool :default false
  perform quantifiers macro expansions
+# Whether to CNF quantifier bodies
+option elimTautQuant --elim-taut-quant bool :default true
+ eliminate tautological disjuncts of quantified formulas
  
 #### E-matching options
  
@@ -83,6 +86,8 @@ option purifyDtTriggers --purify-dt-triggers bool :default false :read-write
  purify dt triggers, match all constructors of correct form instead of selectors
 option pureThTriggers --pure-th-triggers bool :default false :read-write
  use pure theory terms as single triggers
+option partialTriggers --partial-triggers bool :default false :read-write
+ use triggers that do not contain all free variables
 option multiTriggerWhenSingle --multi-trigger-when-single bool :default false
  select multi triggers when single triggers exist
 option multiTriggerPriority --multi-trigger-priority bool :default false
@@ -250,7 +255,7 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
  
 ### reduction options
 
-option quantAlphaEquiv --quant-alpha-equiv bool :default false
+option quantAlphaEquiv --quant-alpha-equiv bool :default true
   infer alpha equivalence between quantified formulas
  
 endmodule
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 07aa89ece..0198e014f 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -774,6 +774,30 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
   }
 }
 
+Node QuantifiersRewriter::computeElimTaut( Node body ) {
+  if( body.getKind()==OR ){
+    std::vector< Node > children;
+    std::map< Node, bool > lit_pol;
+    for( unsigned i=0; i<body.getNumChildren(); i++ ){
+      Node lit = body[i].getKind()==NOT ? body[i][0] : body[i];
+      bool pol = body[i].getKind()!=NOT;
+      std::map< Node, bool >::iterator it = lit_pol.find( lit );
+      if( it==lit_pol.end() ){
+        lit_pol[lit] = pol;
+        children.push_back( body[i] );
+      }else{
+        if( it->second!=pol ){
+          return NodeManager::currentNM()->mkConst( true );
+        }
+      }
+    }
+    if( children.size()!=body.getNumChildren() ){
+      return children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+    }
+  }
+  return body;
+}
+  
 Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) {
   if( body.getKind()==OR ){
     size_t var_found_count = 0;
@@ -1104,6 +1128,8 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
     return options::iteDtTesterSplitQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
+  }else if( computeOption==COMPUTE_ELIM_TAUT ){
+    return options::elimTautQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return options::varElimQuant() || options::dtVarExpandQuant();
   }else if( computeOption==COMPUTE_CNF ){
@@ -1144,6 +1170,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
       n = computeProcessIte2( n );
     }else if( computeOption==COMPUTE_PRENEX ){
       n = computePrenex( n, args, true );
+    }else if( computeOption==COMPUTE_ELIM_TAUT ){
+      n = computeElimTaut( n );
     }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
       Node prev;
       do{
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 201a03737..d01677171 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -51,6 +51,7 @@ private:
   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 );
+  static Node computeElimTaut( Node body );
   static Node computeSplit( Node f, Node body, std::vector< Node >& args );
 private:
   enum{
@@ -61,6 +62,7 @@ private:
     COMPUTE_PROCESS_ITE,
     COMPUTE_PROCESS_ITE_2,
     COMPUTE_PRENEX,
+    COMPUTE_ELIM_TAUT,
     COMPUTE_VAR_ELIMINATION,
     //COMPUTE_FLATTEN_ARGS_UF,
     COMPUTE_CNF,
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index c55ed27ea..e4d9a2730 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -145,7 +145,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
         break;
       }
     }
-    if( varCount<f[0].getNumChildren() ){
+    if( varCount<f[0].getNumChildren() && !options::partialTriggers() ){
       Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl;
       for( unsigned i=0; i<nodes.size(); i++) {
         Trace("trigger-debug") << nodes[i] << " ";
@@ -226,6 +226,12 @@ bool Trigger::isUsable( Node n, Node f ){
       if( isBooleanTermTrigger( n ) ){
         return true;
       }
+      if( options::purifyTriggers() ){
+        Node x = getInversionVariable( n );
+        if( !x.isNull() ){
+          return true;
+        }
+      }
     }
     return false;
   }else{
@@ -247,6 +253,7 @@ bool nodeContainsVar( Node n, Node v ){
 }
 
 Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
+  Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
   if( options::relationalTriggers() ){
     if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
       Node rtr;
@@ -287,7 +294,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
     }
   }
   bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
-  Trace("usable") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl;
+  Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl;
   if( usable ){
     return n;
   }else{
@@ -512,13 +519,16 @@ Node Trigger::getInversionVariable( Node n ) {
         if( !n[i].isConst() ){
           Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
           return Node::null();
-        }else if( n.getType().isInteger() ){
+        }
+        /*
+        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;
@@ -539,8 +549,13 @@ Node Trigger::getInversion( Node n, Node x ) {
           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 );
+          if( x.getType().isInteger() ){
+            Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>() );
+            x = NodeManager::currentNM()->mkNode( INTS_DIVISION, x, coeff );
+          }else{
+            Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
+            x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
+          }
         }
       }else{
         Assert( cindex==-1 );