Minor clean up, fixes related to sygus.

10 files changed, 99 insertions, 83 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c28d23eac..78975bbe6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -749,7 +749,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       $cmd = new EmptyCommand();
     }
   | /* check-synth */
-    CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet();PARSER_STATE->defineSygusFuns(); }
     { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
       Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar));
       std::vector<Expr> bodyv;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 4defc7691..f874074ac 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -826,6 +826,33 @@ static string smtKindString(Kind k) throw() {
   case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv";
   case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real";
 
+  //string theory
+  case kind::STRING_CONCAT: return "str.++";
+  case kind::STRING_LENGTH: return "str.len";
+  case kind::STRING_SUBSTR: return "str.substr" ;
+  case kind::STRING_STRCTN: return "str.contains" ;
+  case kind::STRING_CHARAT: return "str.at" ;
+  case kind::STRING_STRIDOF: return "str.indexof" ;
+  case kind::STRING_STRREPL: return "str.replace" ;
+  case kind::STRING_PREFIX: return "str.prefixof" ;
+  case kind::STRING_SUFFIX: return "str.suffixof" ;
+  case kind::STRING_ITOS: return "int.to.str" ;
+  case kind::STRING_STOI: return "str.to.int" ;
+  case kind::STRING_U16TOS: return "u16.to.str" ;
+  case kind::STRING_STOU16: return "str.to.u16" ;
+  case kind::STRING_U32TOS: return "u32.to.str" ;
+  case kind::STRING_STOU32: return "str.to.u32" ;
+  case kind::STRING_IN_REGEXP: return "str.in.re";
+  case kind::STRING_TO_REGEXP: return "str.to.re";
+  case kind::REGEXP_CONCAT: return "re.++";
+  case kind::REGEXP_UNION: return "re.union";
+  case kind::REGEXP_INTER: return "re.inter";
+  case kind::REGEXP_STAR: return "re.*";
+  case kind::REGEXP_PLUS: return "re.+";
+  case kind::REGEXP_OPT: return "re.opt";
+  case kind::REGEXP_RANGE: return "re.range";
+  case kind::REGEXP_LOOP: return "re.loop";
+  
   default:
     ; /* fall through */
   }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 021798132..3a138e4b7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4420,71 +4420,72 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx
   Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
   Expr e_check = e;
   Node conj = Node::fromExpr( e );
-  Assert( conj.getKind()==kind::FORALL );
-  //possibly run quantifier elimination to make formula into single invocation
-  if( conj[1].getKind()==kind::EXISTS ){
-    Node conj_se = conj[1][1];
-    
-    Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
-    quantifiers::SingleInvocationPartition sip( kind::APPLY );
-    sip.init( conj_se );
-    Trace("smt-synth") << "...finished, got:" << std::endl;
-    sip.debugPrint("smt-synth");
-    
-    if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){
-      //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f.
-      //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), 
-      //  and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f.  We invoke synthesis solver on this result.
-    
-      //create new smt engine to do quantifier elimination
-      SmtEngine smt_qe( d_exprManager );
-      smt_qe.setLogic(getLogicInfo());
-      Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl;
-      //partition variables
-      std::vector< Node > qe_vars;
-      std::vector< Node > nqe_vars;
-      for( unsigned i=0; i<sip.d_all_vars.size(); i++ ){
-        Node v = sip.d_all_vars[i];
-        if( std::find( sip.d_si_vars.begin(), sip.d_si_vars.end(), v )==sip.d_si_vars.end() ){
-          qe_vars.push_back( v );
-        }else{
-          nqe_vars.push_back( v );
-        }
-      }
-      std::vector< Node > orig;
-      std::vector< Node > subs;
-      //skolemize non-qe variables
-      for( unsigned i=0; i<nqe_vars.size(); i++ ){
-        Node k = NodeManager::currentNM()->mkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" );
-        orig.push_back( nqe_vars[i] );
-        subs.push_back( k );
-        Trace("smt-synth") << "  subs : " << nqe_vars[i] << " -> " << k << std::endl;
-      }
-      for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){
-        orig.push_back( sip.d_func_inv[it->first] );
-        Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" );
-        subs.push_back( k );
-        Trace("smt-synth") << "  subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl;
-      }
-      Node conj_se_ngsi = sip.getFullSpecification();
-      Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() );
-      Assert( !qe_vars.empty() );
-      conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs );
+  if( conj.getKind()==kind::FORALL ){
+    //possibly run quantifier elimination to make formula into single invocation
+    if( conj[1].getKind()==kind::EXISTS ){
+      Node conj_se = conj[1][1];
+      
+      Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
+      quantifiers::SingleInvocationPartition sip( kind::APPLY );
+      sip.init( conj_se );
+      Trace("smt-synth") << "...finished, got:" << std::endl;
+      sip.debugPrint("smt-synth");
       
-      Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl;
-      Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false );
-      Trace("smt-synth") << "Result : " << qe_res << std::endl;
+      if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){
+        //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f.
+        //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), 
+        //  and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f.  We invoke synthesis solver on this result.
       
-      //create single invocation conjecture
-      Node qe_res_n = Node::fromExpr( qe_res );
-      qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() );
-      if( !nqe_vars.empty() ){
-        qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n );
+        //create new smt engine to do quantifier elimination
+        SmtEngine smt_qe( d_exprManager );
+        smt_qe.setLogic(getLogicInfo());
+        Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl;
+        //partition variables
+        std::vector< Node > qe_vars;
+        std::vector< Node > nqe_vars;
+        for( unsigned i=0; i<sip.d_all_vars.size(); i++ ){
+          Node v = sip.d_all_vars[i];
+          if( std::find( sip.d_si_vars.begin(), sip.d_si_vars.end(), v )==sip.d_si_vars.end() ){
+            qe_vars.push_back( v );
+          }else{
+            nqe_vars.push_back( v );
+          }
+        }
+        std::vector< Node > orig;
+        std::vector< Node > subs;
+        //skolemize non-qe variables
+        for( unsigned i=0; i<nqe_vars.size(); i++ ){
+          Node k = NodeManager::currentNM()->mkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" );
+          orig.push_back( nqe_vars[i] );
+          subs.push_back( k );
+          Trace("smt-synth") << "  subs : " << nqe_vars[i] << " -> " << k << std::endl;
+        }
+        for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){
+          orig.push_back( sip.d_func_inv[it->first] );
+          Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" );
+          subs.push_back( k );
+          Trace("smt-synth") << "  subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl;
+        }
+        Node conj_se_ngsi = sip.getFullSpecification();
+        Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() );
+        Assert( !qe_vars.empty() );
+        conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs );
+        
+        Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl;
+        Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false );
+        Trace("smt-synth") << "Result : " << qe_res << std::endl;
+        
+        //create single invocation conjecture
+        Node qe_res_n = Node::fromExpr( qe_res );
+        qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() );
+        if( !nqe_vars.empty() ){
+          qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n );
+        }
+        Assert( conj.getNumChildren()==3 );
+        qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] );
+        Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl;
+        e_check = qe_res_n.toExpr();
       }
-      Assert( conj.getNumChildren()==3 );
-      qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] );
-      Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl;
-      e_check = qe_res_n.toExpr();
     }
   }
   
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 955dc5d86..db597d031 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -137,11 +137,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
       doInstantiationRound( e );
       if( d_quantEngine->inConflict() ){
         Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting );
-        Trace("inst-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound();
-        if( lastWaiting>0 ){
-          Trace("inst-engine") << " (prev " << lastWaiting << ")";
-        }
-        Trace("inst-engine") << std::endl;
+        Trace("inst-engine") << "Conflict, added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
       }else if( d_quantEngine->hasAddedLemma() ){
         Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting)  << std::endl;
       }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 0bbca88eb..3063e7a2f 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -221,11 +221,12 @@ int ModelEngine::checkModel(){
 
   //print debug information
   if( d_quantEngine->inConflict() ){
-    Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl;
+    Trace("model-engine") << "Conflict, added lemmas = ";
   }else{
-    Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
-    Trace("model-engine") << d_totalLemmas << std::endl;
-  }
+    Trace("model-engine") << "Added Lemmas = ";
+  } 
+  Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / ";
+  Trace("model-engine") << d_totalLemmas << std::endl;
   return d_addedLemmas;
 }
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 6963f7e62..e41dfc67a 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -230,7 +230,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
     ret = ret.negate();
     status = REWRITE_AGAIN_FULL;
   }else if( in.getKind()==FORALL ){
-    if( in[1].isConst() ){
+    if( in[1].isConst() && in.getNumChildren()==2 ){
       return RewriteResponse( status, in[1] );
     }else{
       //compute attributes
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 61c02d3ac..ae9426172 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -3111,6 +3111,7 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           std::string name = std::string( str.begin() + found +1, str.end() );
           out << name;
         }else{
+          Trace("ajr-temp") << "[[print operator " << op << "]]" << std::endl;
           out << op;
         }
         if( n.getNumChildren()>0 ){
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 12edb5277..afb7aeb92 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -89,7 +89,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_tr_trie = new inst::TriggerTrie;
   d_curr_effort_level = QEFFORT_NONE;
   d_conflict = false;
-  d_num_added_lemmas_round = 0;
   d_hasAddedLemma = false;
   //don't add true lemma
   d_lemmas_produced_c[d_term_db->d_true] = true;
@@ -367,7 +366,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
 
   d_conflict = false;
-  d_num_added_lemmas_round = 0;
   d_hasAddedLemma = false;
   bool setIncomplete = false;
   if( e==Theory::EFFORT_LAST_CALL ){
@@ -969,7 +967,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
       d_lemmas_produced_c[ lem ] = true;
       d_lemmas_waiting.push_back( lem );
       Trace("inst-add-debug") << "Added lemma" << std::endl;
-      d_num_added_lemmas_round++;
       return true;
     }else{
       Trace("inst-add-debug") << "Duplicate." << std::endl;
@@ -978,7 +975,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
   }else{
     //do not need to rewrite, will be rewritten after sending
     d_lemmas_waiting.push_back( lem );
-    d_num_added_lemmas_round++;
     return true;
   }
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 60666c4a9..7522c633b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -158,8 +158,6 @@ private:  //this information is reset during check
   /** are we in conflict */
   bool d_conflict;
   context::CDO< bool > d_conflict_c;
-  /** number of lemmas we actually added this round (for debugging) */
-  unsigned d_num_added_lemmas_round;
   /** has added lemma this round */
   bool d_hasAddedLemma;
 private:
@@ -332,8 +330,6 @@ public:
   bool inConflict() { return d_conflict; }
   /** get number of waiting lemmas */
   unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
-  /** get number of waiting lemmas */
-  unsigned getNumLemmasAddedThisRound() { return d_num_added_lemmas_round; }
   /** get needs check */
   bool getInstWhenNeedsCheck( Theory::Effort e );
   /** get user pat mode */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b3e1925ae..93aedd17b 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3275,11 +3275,9 @@ void TheoryStrings::separateByLength(std::vector< Node >& n,
     Assert( d_equalityEngine.getRepresentative(eqc)==eqc );
     EqcInfo* ei = getOrMakeEqcInfo( eqc, false );
     Node lt = ei ? ei->d_length_term : Node::null();
-    Trace("ajr-temp") << "Length term for " << eqc << " is " << lt << std::endl;
     if( !lt.isNull() ){
       lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
       Node r = d_equalityEngine.getRepresentative( lt );
-      Trace("ajr-temp") << "Length term rep for " << eqc << " is " << lt << std::endl;
       if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){
         eqc_to_leqc[r] = leqc_counter;
         leqc_to_eqc[leqc_counter] = r;