Fix option --quant-fun-wd. Add mk_starexec script to contrib.

3 files changed, 26 insertions, 14 deletions

diff --git a/contrib/mk_starexec b/contrib/mk_starexec
new file mode 100644
index 000000000..aafe1f0c2
--- /dev/null
+++ b/contrib/mk_starexec
@@ -0,0 +1,9 @@
+#!/bin/bash
+# Run : mk_starexec [TEXT] 
+# Run from directory containing cvc4 binary and subdirectory starexec/ containing the starexec space, i.e. subdirectory bin/ with configuration files.
+# Generates file cvc4-[TEXT].tgz that can be uploaded to starexec.
+strip cvc4
+cp cvc4 ./starexec/bin/cvc4
+cd starexec
+tar -czf ../cvc4-$1.tgz .
+rm bin/cvc4
\ No newline at end of file
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 249b71130..414df2882 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -240,20 +240,24 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
     d_patTerms[1][f].clear();
     std::vector< Node > patTermsF;
     //well-defined function: can assume LHS is only trigger
-    Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
-    if( d_quantEngine->getTermDatabase()->isQAttrFunDef( f ) && options::quantFunWellDefined() ){
-      Assert( bd.getKind()==EQUAL || bd.getKind()==IFF );
-      Assert( bd[0].getKind()==APPLY_UF );
-      patTermsF.push_back( bd[0] );
-    }else{
-      Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true );
+    if( options::quantFunWellDefined() ){
+      Node hd = TermDb::getFunDefHead( f );
+      if( !hd.isNull() ){
+        hd = d_quantEngine->getTermDatabase()->getInstConstantNode( hd, f );
+        patTermsF.push_back( hd );
+      }
     }
-    Trace("auto-gen-trigger") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
-    Trace("auto-gen-trigger") << "   ";
-    for( int i=0; i<(int)patTermsF.size(); i++ ){
-      Trace("auto-gen-trigger") << patTermsF[i] << " ";
+    //otherwise, use algorithm for collecting pattern terms
+    if( patTermsF.empty() ){
+      Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
+      Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true );
+      Trace("auto-gen-trigger") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
+      Trace("auto-gen-trigger") << "   ";
+      for( int i=0; i<(int)patTermsF.size(); i++ ){
+        Trace("auto-gen-trigger") << patTermsF[i] << " ";
+      }
+      Trace("auto-gen-trigger") << std::endl;
     }
-    Trace("auto-gen-trigger") << std::endl;
     //extend to literal matching (if applicable)
     d_quantEngine->getPhaseReqTerms( f, patTermsF );
     //sort into single/multi triggers
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 090d127f1..e6f1ceee0 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1241,8 +1241,7 @@ void TermDb::computeAttributes( Node q ) {
         if( avar.getAttribute(FunDefAttribute()) ){
           Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
           d_qattr_fundef[q] = true;
-          //Assert( q[1].getKind()==EQUAL || q[1].getKind()==IFF );
-          //Assert( q[2][i][0]==q[1][0] || q[2][i][0]==q[1][1] );
+          //get operator directly from pattern
           Node f = q[2][i][0].getOperator();
           if( d_fun_defs.find( f )!=d_fun_defs.end() ){
             Message() << "Cannot define function " << f << " more than once." << std::endl;