Output solutions for synthesis conjectures with --dump-synth. Minor refactor of previous commit.

8 files changed, 95 insertions, 50 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 9bfccc34e..bf17cf5e4 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -439,17 +439,6 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
                           if( isGenericRedundant( tnnp, g ) ){
                             rem = true;
                           }
-                          /*
-                          Node nr = NodeManager::currentNM()->mkNode( parentKind, dt[j].getSygusOp(), dto[i].getSygusOp() );
-                          Node nrr = Rewriter::rewrite( nr );
-                          Trace("sygus-split-debug") << "  Test constant args : " << nr << " rewrites to " << nrr << std::endl;
-                          //based on rewriting
-                          // if rewriting the two arguments gives an operator that is in the parent syntax, remove the redundancy
-                          if( hasOp( tnnp, nrr ) ){
-                            Trace("sygus-nf") << "* Sygus norm : simplify based on rewrite " << nr << " -> " << nrr << std::endl;
-                            rem = true;
-                          }
-                          */
                         }
                       }
                       if( rem ){
@@ -598,6 +587,8 @@ Node SygusSplit::getTypeMaxValue( TypeNode tn ) {
     return it->second;
   }
 }
+
+//this function gets all easy redundant cases, before consulting rewriters
 bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Kind k, Kind parent, int arg ) {
   Assert( hasKind( tn, k ) );
   Assert( hasKind( tnp, parent ) );
@@ -648,7 +639,6 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
     if( parent==UMINUS ){
       if( k==PLUS ){
         nk = PLUS;reqk = UMINUS;
-      }else if( k==MINUS ){
       }
     }
     if( parent==BITVECTOR_NEG ){
@@ -712,15 +702,10 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
       }
     }
   }
-
-  /*
-  if( parent==MINUS ){
-
-  }
-  */
   return true;
 }
 
+//this function gets all easy redundant cases, before consulting rewriters
 bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Node c, Kind parent, int arg ) {
   Assert( hasConst( tn, c ) );
   Assert( hasKind( tnp, parent ) );
@@ -741,16 +726,6 @@ bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pd
       return false;
     }
   }
-  //single argument rewrite
-  if( pdt[pc].getNumArgs()==1 ){
-    Node cr = NodeManager::currentNM()->mkNode( parent, c );
-    cr = Rewriter::rewrite( cr );
-    Trace("sygus-split-debug") << "  " << parent << " applied to " << c << " rewrites to " << cr << std::endl;
-    if( hasConst( tnp, cr ) ){
-      return false;
-    }
-  }
-
   return true;
 }
 
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 76ccabd4d..c638e5da6 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -24,18 +24,9 @@
 #include "context/cdchunk_list.h"
 
 namespace CVC4 {
-namespace theory {
+namespace theory { 
 namespace datatypes {
-
-//class SygusVarTrie
-//{
-//public:
-//  // datatype, constructor, argument
-//  std::map< Node, std::map< int, SygusVarTrie > > d_children;
-//  std::map< TypeNode, Node > d_var;
-//};
-
-
+  
 class SygusSplit
 {
 private:
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index bb53c9cfb..669cd8fa9 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -18,6 +18,8 @@
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "util/datatype.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -246,7 +248,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
     if( getTermDatabase()->isQAttrSygus( q ) ){
 
       std::vector< Node > model_values;
-      if( getModelValues( conj->d_candidates, model_values ) ){
+      if( getModelValues( conj, conj->d_candidates, model_values ) ){
         //check if we must apply fairness lemmas
         std::vector< Node > lems;
         if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){
@@ -300,15 +302,10 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       }
 
     }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
-      Trace("cegqi-engine") << "  * Value is : ";
       std::vector< Node > model_terms;
-      for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
-        Node t = getModelTerm( conj->d_candidates[i] );
-        model_terms.push_back( t );
-        Trace("cegqi-engine") << conj->d_candidates[i] << " -> " << t << " ";
+      if( getModelValues( conj, conj->d_candidates, model_terms ) ){
+        d_quantEngine->addInstantiation( q, model_terms, false );
       }
-      Trace("cegqi-engine") << std::endl;
-      d_quantEngine->addInstantiation( q, model_terms, false );
     }
   }else{
     Trace("cegqi-engine") << "  *** Refine candidate phase..." << std::endl;
@@ -323,7 +320,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           Assert( !conj->d_inner_vars_disj[k].empty() );
           Assert( conj->d_inner_vars_disj[k].size()==getTermDatabase()->d_skolem_constants[ce_q].size() );
           std::vector< Node > model_values;
-          if( getModelValues( getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){
+          if( getModelValues( NULL, getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){
             //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
             Node inst_ce_refine = conj->d_base_disj[k][0][1].substitute( conj->d_inner_vars_disj[k].begin(), conj->d_inner_vars_disj[k].end(),
                                                                          model_values.begin(), model_values.end() );
@@ -355,7 +352,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   }
 }
 
-bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) {
+bool CegInstantiation::getModelValues( CegConjecture * conj, std::vector< Node >& n, std::vector< Node >& v ) {
   bool success = true;
   Trace("cegqi-engine") << "  * Value is : ";
   for( unsigned i=0; i<n.size(); i++ ){
@@ -365,6 +362,9 @@ bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node
     if( nv.isNull() ){
       success = false;
     }
+    if( conj ){
+      conj->d_candidate_inst[i].push_back( nv );
+    }
   }
   Trace("cegqi-engine") << std::endl;
   return success;
@@ -449,4 +449,53 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le
   }
 }
 
+void CegInstantiation::printSynthSolution( std::ostream& out ) {
+  if( d_conj ){
+    out << "Solution:" << std::endl;
+    for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){
+      std::stringstream ss;
+      ss << d_conj->d_quant[0][i];
+      std::string f(ss.str());
+      f.erase(f.begin());
+      out << "(define-fun f ";
+      TypeNode tn = d_conj->d_quant[0][i].getType();
+      Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) );
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      Assert( dt.isSygus() );
+      out << dt.getSygusVarList() << " ";
+      out << dt.getSygusType() << " ";
+      if( d_conj->d_candidate_inst[i].empty() ){
+        out << "?";
+      }else{
+        printSygusTerm( out, d_conj->d_candidate_inst[i].back() );
+      }
+      out << ")" << std::endl;
+    }
+  }
+}
+
+void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) {
+  if( n.getKind()==APPLY_CONSTRUCTOR ){
+    TypeNode tn = n.getType();
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    if( dt.isSygus() ){
+      int cIndex = Datatype::indexOf( n.getOperator().toExpr() );
+      Assert( !dt[cIndex].getSygusOp().isNull() );
+      if( n.getNumChildren()>0 ){
+        out << "(";
+      }
+      out << dt[cIndex].getSygusOp();
+      if( n.getNumChildren()>0 ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          out << " ";
+          printSygusTerm( out, n[i] );
+        }
+        out << ")";
+      }
+      return;
+    }
+  }
+  out << n << std::endl;
+}
+
 }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 8c74b06f6..f4449117c 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -56,6 +56,8 @@ private:
     /** list of variables on inner quantification */
     std::vector< Node > d_inner_vars;    
     std::vector< std::vector< Node > > d_inner_vars_disj;
+    /** list of terms we have instantiated candidates with */
+    std::map< int, std::vector< Node > > d_candidate_inst;
     /** initialize guard */
     void initializeGuard( QuantifiersEngine * qe );
     /** measure term */
@@ -99,11 +101,14 @@ private:
   /** check conjecture */
   void checkCegConjecture( CegConjecture * conj );
   /** get model values */
-  bool getModelValues( std::vector< Node >& n, std::vector< Node >& v );
+  bool getModelValues( CegConjecture * conj, std::vector< Node >& n, std::vector< Node >& v );
   /** get model value */
   Node getModelValue( Node n );
   /** get model term */
   Node getModelTerm( Node n );
+private:
+  /** print sygus term */
+  void printSygusTerm( std::ostream& out, Node n );
 public:
   CegInstantiation( QuantifiersEngine * qe, context::Context* c );
 public:
@@ -118,6 +123,8 @@ public:
   Node getNextDecisionRequest();
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const { return "CegInstantiation"; }
+  /** print solution for synthesis conjectures */
+  void printSynthSolution( std::ostream& out );  
 };
 
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2cf6002cd..7fb6c0bb7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -924,6 +924,14 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) {
   }
 }
 
+void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
+  if( d_ceg_inst ){
+    d_ceg_inst->printSynthSolution( out );
+  }else{
+    out << "Internal error : module for synth solution not found." << std::endl;
+  }
+}
+  
 QuantifiersEngine::Statistics::Statistics():
   d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
   d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index c533f4cbb..eb4470eec 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -303,6 +303,8 @@ public:
 public:
   /** print instantiations */
   void printInstantiations( std::ostream& out );
+  /** print solution for synthesis conjectures */
+  void printSynthSolution( std::ostream& out );
   /** statistics class */
   class Statistics {
   public:
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 22bf37470..74a8fab73 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1224,6 +1224,14 @@ void TheoryEngine::printInstantiations( std::ostream& out ) {
   }
 }
 
+void TheoryEngine::printSynthSolution( std::ostream& out ) {
+  if( d_quantEngine ){
+    d_quantEngine->printSynthSolution( out );
+  }else{
+    out << "Internal error : synth solution not available when quantifiers are not present." << std::endl;
+  }
+}
+
 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
   std::set<TNode> all;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 6360ea5fb..4f1a5163e 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -776,6 +776,11 @@ public:
   void printInstantiations( std::ostream& out );
 
   /**
+   * Print solution for synthesis conjectures found by ce_guided_instantiation module
+   */
+  void printSynthSolution( std::ostream& out );
+  
+  /**
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */