Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizations to sygus and qcf.

6 files changed, 91 insertions, 18 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index d9059a3e6..ad900ee82 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
+#include "prop/prop_engine.h"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -291,6 +292,8 @@ void CegInstantiation::registerQuantifier( Node q ) {
     }else{
       Assert( d_conj->d_quant==q );
     }
+  }else{
+    Trace("cegqi-debug") << "Register quantifier : " << q << std::endl;
   }
 }
 
@@ -317,7 +320,7 @@ Node CegInstantiation::getNextDecisionRequest() {
         Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl;
         return req_dec[i];
       }else{
-        Trace("cegqi-debug") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl;
+        Trace("cegqi-debug2") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl;
       }
     }
 
@@ -426,6 +429,16 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         d_quantEngine->addLemma( lem );
         ++(d_statistics.d_cegqi_lemmas_ce);
         Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
+        //optimization : eagerly unfold applications of evaluation function
+        if( options::sygusEagerUnfold() ){
+          std::vector< Node > eager_lems;
+          std::map< Node, bool > visited;
+          getEagerUnfoldLemmas( eager_lems, lem, visited );        
+          for( unsigned i=0; i<eager_lems.size(); i++ ){
+            Trace("cegqi-lemma") << "Cegqi::Lemma : eager unfold : " << eager_lems[i] << std::endl;
+            d_quantEngine->addLemma( eager_lems[i] );
+          }
+        }
       }
 
     }else{
@@ -589,6 +602,53 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le
   }
 }
 
+void CegInstantiation::getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    Trace("cegqi-eager-debug") << "getEagerUnfoldLemmas " << n << std::endl;
+    visited[n] = true;
+    if( n.getKind()==APPLY_UF ){
+      TypeNode tn = n[0].getType();
+      Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
+      if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+        if( dt.isSygus() ){
+          Trace("cegqi-eager") << "Unfold eager : " << n << std::endl;
+          Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( n[0], tn );
+          Trace("cegqi-eager") << "Built-in term : " << bTerm << std::endl;
+          std::vector< Node > vars;
+          std::vector< Node > subs;
+          Node var_list = Node::fromExpr( dt.getSygusVarList() );
+          Assert( var_list.getNumChildren()+1==n.getNumChildren() );
+          for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
+            vars.push_back( var_list[j] );
+          }
+          for( unsigned j=1; j<n.getNumChildren(); j++ ){
+            if( var_list[j-1].getType().isBoolean() ){   
+              //TODO: remove this case when boolean term conversion is eliminated
+              Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+              subs.push_back( n[j].eqNode( c ) );
+            }else{
+              subs.push_back( n[j] );
+            }
+            Assert( subs[j-1].getType()==var_list[j-1].getType() );
+          }
+          bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+          Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
+          Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
+          Assert( n.getType()==bTerm.getType() );
+          Node lem = Rewriter::rewrite( NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bTerm ) ); 
+          lems.push_back( lem );
+        }
+      }
+    }
+    if( n.getKind()!=FORALL ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        getEagerUnfoldLemmas( lems, n[i], visited );
+      }
+    }
+  }
+}
+
 void CegInstantiation::printSynthSolution( std::ostream& out ) {
   if( d_conj->isAssigned() ){
     Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 57dc31850..81f70d600 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -139,6 +139,8 @@ private: //for enforcing fairness
   std::map< Node, std::map< int, Node > > d_size_term_lemma;
   /** get measure lemmas */
   void getMeasureLemmas( Node n, Node v, std::vector< Node >& lems );
+  /** get eager unfolding */
+  void getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited );
 private:
   /** check conjecture */
   void checkCegConjecture( CegConjecture * conj );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 7bc51dc50..5b5f9fc22 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -34,9 +34,10 @@ using namespace CVC4::theory::quantifiers;
 
 struct sortQuantifiersForSymbol {
   QuantifiersEngine* d_qe;
+  std::map< Node, Node > d_op_map;
   bool operator() (Node i, Node j) {
-    int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );
-    int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );
+    int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[i] );
+    int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[j] );
     if( nqfsi<nqfsj ){
       return true;
     }else if( nqfsi>nqfsj ){
@@ -325,6 +326,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       Node pat = patTermsF[i];
       if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){
         Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
+        Node mpat = pat;
         //process the pattern: if it has a required polarity, consider it
         Assert( tinfo.find( pat )!=tinfo.end() );
         int rpol = tinfo[pat].d_reqPol;
@@ -363,10 +365,10 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         }else{
           if( Trigger::isRelationalTrigger( pat ) ){
             //consider both polarities
-            addPatternToPool( f, pat.negate(), num_fv );
+            addPatternToPool( f, pat.negate(), num_fv, mpat );
           }
         }
-        addPatternToPool( f, pat, num_fv );
+        addPatternToPool( f, pat, num_fv, mpat );
       }
     }
     //tinfo not used below this point
@@ -398,12 +400,17 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       if( options::relevantTriggers() ){
         sortQuantifiersForSymbol sqfs;
         sqfs.d_qe = d_quantEngine;
+        for( unsigned i=0; i<patTerms.size(); i++ ){
+          Assert( d_pat_to_mpat.find( patTerms[i] )!=d_pat_to_mpat.end() );
+          Assert( d_pat_to_mpat[patTerms[i]].hasOperator() );
+          sqfs.d_op_map[ patTerms[i] ] = d_pat_to_mpat[patTerms[i]].getOperator();
+        }        
         //sort based on # occurrences (this will cause Trigger to select rarer symbols)
         std::sort( patTerms.begin(), patTerms.end(), sqfs );
         Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
         for( unsigned i=0; i<patTerms.size(); i++ ){
-          Debug("relevant-trigger") << "   " << patTerms[i] << " (";
-          Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
+          Debug("relevant-trigger") << "   " << patTerms[i] << " from " << d_pat_to_mpat[patTerms[i]] << " (";
+          Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_pat_to_mpat[patTerms[i]].getOperator() ) << ")" << std::endl;
         }
       }
       //now, generate the trigger...
@@ -462,7 +469,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
   }
 }
 
-void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv ) {
+void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ) {
+  d_pat_to_mpat[pat] = mpat;
   unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren();
   if( num_fv==num_vars && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
     d_patTerms[0][q].push_back( pat );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 97d97b10a..e6d993294 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -86,13 +86,14 @@ private:
   // number of trigger variables per quantifier
   std::map< Node, unsigned > d_num_trigger_vars;
   std::map< Node, Node > d_vc_partition[2];
+  std::map< Node, Node > d_pat_to_mpat;
 private:
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
   int process( Node q, Theory::Effort effort, int e );
   /** generate triggers */
   void generateTriggers( Node q );
-  void addPatternToPool( Node q, Node pat, unsigned num_fv );
+  void addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat );
   void addTrigger( inst::Trigger * tr, Node f );
   /** has user patterns */
   bool hasUserPatterns( Node q );
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 1365feda9..346807a0e 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -112,14 +112,15 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
     //optimization : record variable argument positions for terms that must be matched
     std::vector< TNode > vars;
     //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
-    //if( options::qcfSkipRd() ){
-    //  for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
-    //    vars.push_back( d_vars[j] );
-    //  }
-    //}
-    //get all variables that are always relevant
-    std::map< TNode, bool > visited;
-    getPropagateVars( p, vars, q[1], false, visited );
+    if( options::qcfSkipRd() ){
+      for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
+        vars.push_back( d_vars[j] );
+      }
+    }else{
+      //get all variables that are always relevant
+      std::map< TNode, bool > visited;
+      getPropagateVars( p, vars, q[1], false, visited );
+    }
     for( unsigned j=0; j<vars.size(); j++ ){
       Node v = vars[j];
       TNode f = p->getTermDatabase()->getMatchOperator( v );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ae9426172..e3cf15c53 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1944,7 +1944,8 @@ Node TermDb::simpleNegate( Node n ){
 
 bool TermDb::isAssoc( Kind k ) {
   return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
-         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
+         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT ||
+         k==STRING_CONCAT;
 }
 
 bool TermDb::isComm( Kind k ) {