Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.

10 files changed, 92 insertions, 65 deletions

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 4e73fa6cf..dcee52337 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -353,7 +353,7 @@ definedFun[CVC4::Expr& expr]
                                       MK_EXPR(CVC4::kind::TO_INTEGER, expr),
                                       MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
       if(remainder) {
-        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+        expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)));
       }
       expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
     }
@@ -368,7 +368,7 @@ definedFun[CVC4::Expr& expr]
                                       MK_EXPR(CVC4::kind::TO_INTEGER, expr),
                                       MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
       if(remainder) {
-        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+        expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)));
       }
       expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
     }
@@ -381,7 +381,7 @@ definedFun[CVC4::Expr& expr]
       expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
       expr = MK_EXPR(CVC4::kind::TO_INTEGER, expr);
       if(remainder) {
-        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+        expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)));
       }
       expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
     }
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index d817fb179..082fa2580 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -37,6 +37,7 @@ struct ArraySelectTypeRule {
       }
       TypeNode indexType = n[1].getType(check);
       if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
+      //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){  //FIXME:typing
         throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
       }
     }
@@ -56,9 +57,11 @@ struct ArrayStoreTypeRule {
         TypeNode indexType = n[1].getType(check);
         TypeNode valueType = n[2].getType(check);
         if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
+        //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){  //FIXME:typing
           throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
         }
-        if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){
+        if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){  
+        //if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){  //FIXME:typing
           Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl;
           Debug("array-types") << "value types: " << valueType << std::endl;
           throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 412b3d7ec..0540044b5 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -80,9 +80,12 @@ struct DatatypeConstructorTypeRule {
                                  << (*tchild_it) << std::endl;
           TypeNode argumentType = *tchild_it;
           if (!childType.isComparableTo(argumentType)) {
+          //if (!childType.isSubtypeOf(argumentType)) {   //FIXME:typing
             std::stringstream ss;
-            ss << "bad type for constructor argument:\nexpected: "
-               << argumentType << "\ngot     : " << childType;
+            ss << "bad type for constructor argument:\n"
+               << "child type:  " << childType << "\n"
+               << "not subtype: " << argumentType << "\n"
+               << "in term : " << n;
             throw TypeCheckingExceptionPrivate(n, ss.str());
           }
         }
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 1543b2ebd..521f1c978 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -502,6 +502,14 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
       }
     }
   }
+  if( Trace.isOn("cegqi-si-apply-subs-debug") ){
+    Trace("cegqi-si-apply-subs-debug") << "req_coeff = " << req_coeff << "  " << tn << std::endl;
+    for( unsigned i=0; i<subs.size(); i++ ){
+      Trace("cegqi-si-apply-subs-debug") << "  " << vars[i] << " -> " << subs[i] << "   types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
+      Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) );
+    }
+  }
+  
   if( !req_coeff ){
     Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
     if( n!=nret ){
@@ -515,8 +523,12 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
       std::vector< Node > nsubs;
       for( unsigned i=0; i<vars.size(); i++ ){
         if( !coeff[i].isNull() ){
+          Assert( vars[i].getType().isInteger() );
           Assert( coeff[i].isConst() );
-          nsubs.push_back( Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) ) ));
+          Node nn =NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) );
+          nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
+          nn =  Rewriter::rewrite( nn );
+          nsubs.push_back( nn );
         }else{
           nsubs.push_back( subs[i] );
         }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 2cef4f6a1..2a7b589d0 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -659,6 +659,10 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
 }
 
 bool FullSaturation::process( Node f, bool fullEffort ){
+  // ignore if constant true (rare case of non-standard quantifier whose body is rewritten to true)
+  if( f[1].isConst() && f[1].getConst<bool>() ){
+    return false;
+  }
   //first, try from relevant domain
   RelevantDomain * rd = d_quantEngine->getRelevantDomain();
   unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
@@ -770,7 +774,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
       }
     }
   }
-  //term enumerator?
+  //TODO : term enumerator?
   return false;
 }
 
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 636bfdb59..99dbb7ab9 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -44,7 +44,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
     Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
     //first, collect macro definitions
     std::vector< Node > macro_assertions;
-    for( unsigned i=0; i<assertions.size(); i++ ){
+    for( int i=0; i<(int)assertions.size(); i++ ){
       Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
       if( processAssertion( assertions[i] ) ){
         PROOF( 
@@ -167,6 +167,7 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
   Assert( n.getKind()==APPLY_UF );
   TypeNode tno = n.getOperator().getType();
   std::map< Node, bool > vars;
+  // allow if a vector of unique variables of the same type as UF arguments
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
     if( n[i].getKind()!=BOUND_VARIABLE ){
       return false;
@@ -174,11 +175,6 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
     if( n[i].getType()!=tno[i] ){
       return false;
     }
-    if( !tno[i].isSort() && !tno[i].isReal() && ( !tno[i].isDatatype() || tno[i].isParametricDatatype() ) && 
-        !tno[i].isBitVector() && !tno[i].isString() && !tno[i].isFloatingPoint() ){
-      //only non-parametric types are supported
-      return false;
-    }
     if( vars.find( n[i] )==vars.end() ){
       vars[n[i]] = true;
     }else{
@@ -331,6 +327,7 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
   }else{
     //literal case
     if( isMacroLiteral( n, pol ) ){
+      Trace("macros-debug") << "Check macro literal : " << n << std::endl;
       std::map< Node, bool > visited;
       std::vector< Node > candidates;
       for( size_t i=0; i<n.getNumChildren(); i++ ){
@@ -339,6 +336,7 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
       for( size_t i=0; i<candidates.size(); i++ ){
         Node m = candidates[i];
         Node op = m.getOperator();
+        Trace("macros-debug") << "Check macro candidate : " << m << std::endl;
         if( d_macro_defs.find( op )==d_macro_defs.end() ){
           std::vector< Node > fvs;
           visited.clear();
@@ -416,6 +414,7 @@ Node QuantifierMacros::simplify( Node n ){
         if( it!=d_macro_defs.end() && !it->second.isNull() ){
           //only apply if children are subtypes of arguments
           bool success = true;
+          // FIXME : this can be eliminated when we have proper typing rules
           std::vector< Node > cond;
           TypeNode tno = op.getType();
           for( unsigned i=0; i<children.size(); i++ ){
@@ -423,13 +422,13 @@ Node QuantifierMacros::simplify( Node n ){
             if( etc.isNull() ){
               //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op, 
               //  and not ensuring it applies to n when its types are correct.
-              //however, this should never fail: we never process types for which we cannot constuct conditions that ensure correct types, e.g. (is-int t).
-              Assert( false );
+              //Assert( false );
               success = false;
               break;
             }else if( !etc.isConst() ){
               cond.push_back( etc );
             }
+            Assert( children[i].getType().isSubtypeOf( tno[i] ) );
           }
           if( success ){
             //do substitution if necessary
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index f2a4e6d17..5b02a877a 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -398,49 +398,46 @@ bool Trigger::isSimpleTrigger( Node n ){
 }
 
 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
-void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
+void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
                                 quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
-                                bool pol, bool hasPol, bool epol, bool hasEPol ){
-  std::map< Node, Node >::iterator itv = visited.find( n );
+                                bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable ){
+  std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
   if( itv==visited.end() ){
-    visited[ n ] = Node::null();
+    visited[ n ].clear();
     Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
     if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
       Node nu;
       bool nu_single = false;
-      if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
+      if( knowIsUsable ){
+        nu = n;
+      }else if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
         nu = getIsUsableTrigger( n, q );
-        if( !nu.isNull() ){
-          Assert( nu.getKind()!=NOT );
-          Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
-          Node reqEq;
-          if( nu.getKind()==EQUAL ){
-            if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){
-              if( hasPol ){
-                reqEq = nu[1];
-              }
-              nu = nu[0];
-            }
-          }
-          Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) );
-          Assert( isUsableTrigger( nu, q ) );
-          //do not add if already visited
-          bool add = true;
-          if( n!=nu ){
-            std::map< Node, Node >::iterator itvu = visited.find( nu );
-            if( itvu!=visited.end() ){
-              add = false;
+        if( !nu.isNull() && nu!=n ){
+          collectPatTerms2( q, nu, visited, tinfo, tstrt, exclude, added, pol, hasPol, epol, hasEPol, true );
+          // copy to n
+          visited[n].insert( visited[n].end(), added.begin(), added.end() );
+          return;
+        }
+      }
+      if( !nu.isNull() ){
+        Assert( nu==n );
+        Assert( nu.getKind()!=NOT );
+        Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
+        Node reqEq;
+        if( nu.getKind()==EQUAL ){
+          if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){
+            if( hasPol ){
+              reqEq = nu[1];
             }
-          }
-          if( add ){
-            Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
-            visited[ nu ] = nu;
-            tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
-            nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
-          }else{
-            nu = Node::null();
+            nu = nu[0];
           }
         }
+        Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) );
+        Assert( isUsableTrigger( nu, q ) );
+        //tinfo.find( nu )==tinfo.end()
+        Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
+        tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
+        nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
       }
       Node nrec = nu.isNull() ? n : nu;
       std::vector< Node > added2;
@@ -451,6 +448,7 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited,
         QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
         collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol );
       }
+      // if this is not a usable trigger, don't worry about caching the results, since triggers do not contain non-usable subterms
       if( !nu.isNull() ){
         bool rm_nu = false;
         for( unsigned i=0; i<added2.size(); i++ ){
@@ -461,7 +459,7 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited,
             if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
               //discard all subterms
               Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
-              visited[added2[i]] = Node::null();
+              visited[ added2[i] ].clear();
               tinfo.erase( added2[i] );
             }else{
               if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
@@ -476,18 +474,20 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited,
           }
         }
         if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
-          visited[nu] = Node::null();
           tinfo.erase( nu );
         }else{
-          Assert( std::find( added.begin(), added.end(), nu )==added.end() );
-          added.push_back( nu );
+          if( std::find( added.begin(), added.end(), nu )==added.end() ){
+            added.push_back( nu );
+          }
         }
+        visited[n].insert( visited[n].end(), added.begin(), added.end() );
       }
     }
   }else{
-    if( !itv->second.isNull() ){
-      if( std::find( added.begin(), added.end(), itv->second )==added.end() ){
-        added.push_back( itv->second );
+    for( unsigned i=0; i<itv->second.size(); ++i ){
+      Node t = itv->second[i];
+      if( std::find( added.begin(), added.end(), t )==added.end() ){
+        added.push_back( t );
       }
     }
   }
@@ -573,7 +573,7 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector<
 
 void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
                                std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){
-  std::map< Node, Node > visited;
+  std::map< Node, std::vector< Node > > visited;
   if( filterInst ){
     //immediately do not consider any term t for which another term is an instance of t
     std::vector< Node > patTerms2;
@@ -607,7 +607,7 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
       //do not consider terms that have instances
       for( unsigned i=0; i<patTerms2.size(); i++ ){
         if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
-          visited[ patTerms2[i] ] = Node::null();
+          visited[ patTerms2[i] ].clear();
         }
       }
     }
@@ -615,9 +615,7 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
   std::vector< Node > added;
   collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true );
   for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){
-    if( !visited[it->first].isNull() ){
-      patTerms.push_back( it->first );
-    }
+    patTerms.push_back( it->first );
   }
 }
 
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 234025e7b..8d8f01926 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -137,9 +137,9 @@ private:
   static Node getIsUsableEq( Node q, Node eq );
   static bool isUsableEqTerms( Node q, Node n1, Node n2 );
   /** collect all APPLY_UF pattern terms for f in n */
-  static void collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
+  static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
                                 quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
-                                bool pol, bool hasPol, bool epol, bool hasEPol );
+                                bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false );
 
   std::vector< Node > d_nodes;
 
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index a5a78e691..e2830b57e 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -116,7 +116,13 @@ struct MemberTypeRule {
       }
       TypeNode elementType = n[0].getType(check);
       if(!elementType.isComparableTo(setType.getSetElementType())) {
-        throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types");
+      //if(!elementType.isSubtypeOf(setType.getSetElementType())) {     //FIXME:typing
+        std::stringstream ss;
+        ss << "member operating on sets of different types:\n"
+           << "child type:  " << elementType << "\n"
+           << "not subtype: " << setType.getSetElementType() << "\n"
+           << "in term : " << n;
+        throw TypeCheckingExceptionPrivate(n, ss.str());
       }
     }
     return nodeManager->booleanType();
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 5d97dda38..6f97a9662 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -46,12 +46,14 @@ class UfTypeRule {
         TypeNode currentArgument = (*argument_it).getType();
         TypeNode currentArgumentType = *argument_type_it;
         if (!currentArgument.isComparableTo(currentArgumentType)) {
+        //if (!currentArgument.isSubtypeOf(currentArgumentType)) {   //FIXME:typing
           std::stringstream ss;
           ss << "argument type is not a subtype of the function's argument "
              << "type:\n"
              << "argument:  " << *argument_it << "\n"
              << "has type:  " << (*argument_it).getType() << "\n"
-             << "not subtype: " << *argument_type_it;
+             << "not subtype: " << *argument_type_it << "\n"
+             << "in term : " << n;
           throw TypeCheckingExceptionPrivate(n, ss.str());
         }
       }