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

18 files changed, 182 insertions, 54 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 242e018f6..1c7c1d171 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1187,6 +1187,44 @@ std::string GetInstantiationsCommand::getCommandName() const throw() {
   return "get-instantiations";
 }
 
+/* class GetSynthSolutionCommand */
+
+GetSynthSolutionCommand::GetSynthSolutionCommand() throw() {
+}
+
+void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_smtEngine = smtEngine;
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out, verbosity);
+  } else {
+    d_smtEngine->printSynthSolution(out);
+  }
+}
+
+Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
+  c->d_smtEngine = d_smtEngine;
+  return c;
+}
+
+Command* GetSynthSolutionCommand::clone() const {
+  GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
+  c->d_smtEngine = d_smtEngine;
+  return c;
+}
+
+std::string GetSynthSolutionCommand::getCommandName() const throw() {
+  return "get-instantiations";
+}
+
 /* class GetUnsatCoreCommand */
 
 GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index cfa00bff4..9165961fb 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -610,6 +610,19 @@ public:
   std::string getCommandName() const throw();
 };/* class GetInstantiationsCommand */
 
+class CVC4_PUBLIC GetSynthSolutionCommand : public Command {
+protected:
+  SmtEngine* d_smtEngine;
+public:
+  GetSynthSolutionCommand() throw();
+  ~GetSynthSolutionCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+  std::string getCommandName() const throw();
+};/* class GetSynthSolutionCommand */
+
 class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
 protected:
   UnsatCore d_result;
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 52522d591..460274515 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -139,6 +139,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
           res.asSatisfiabilityResult() == Result::UNSAT ) ) {
       g = new GetInstantiationsCommand();
     }
+    if( d_options[options::dumpSynth] && res.asSatisfiabilityResult() == Result::UNSAT ){
+      g = new GetSynthSolutionCommand();
+    }
     if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) {
       g = new GetUnsatCoreCommand();
     }
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 610902270..e4effd239 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -378,6 +378,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
                  d_result.asSatisfiabilityResult() == Result::UNSAT ) ) {
         Command* gi = new GetInstantiationsCommand();
         status = doCommandSingleton(gi);
+      } else if( d_options[options::dumpSynth] && d_result.asSatisfiabilityResult() == Result::UNSAT ){
+        Command* gi = new GetSynthSolutionCommand();
+        status = doCommandSingleton(gi);
       } else if( d_options[options::dumpUnsatCores] &&
                  d_result.asSatisfiabilityResult() == Result::UNSAT ) {
         Command* guc = new GetUnsatCoreCommand();
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e536ed7cc..3fa27e474 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -600,7 +600,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         std::string dname = ss.str();
         sorts.push_back(t);
         datatypes.push_back(Datatype(dname));
-        datatypes.back().setSygusType( t );
+        datatypes.back().setSygus( t, terms[0] );
         ops.push_back(std::vector<Expr>());
         cnames.push_back(std::vector<std::string>());
         cargs.push_back(std::vector<std::vector<CVC4::Type> >());
diff --git a/src/smt/options b/src/smt/options
index 20dd5b7d5..593fc4887 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -37,6 +37,8 @@ option dumpProofs --dump-proofs bool :default false :link --proof
  output proofs after every UNSAT/VALID response
 option dumpInstantiations --dump-instantiations bool :default false
  output instantiations of quantified formulas after every UNSAT/VALID response
+option dumpSynth --dump-synth bool :default false
+ output solution for synthesis conjectures after every UNSAT/VALID response
 option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on unsat core generation
 option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6732b3dc7..94efd8a75 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4155,6 +4155,13 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   }
 }
 
+void SmtEngine::printSynthSolution( std::ostream& out ) {
+  SmtScope smts(this);
+  if( d_theoryEngine ){
+    d_theoryEngine->printSynthSolution( out );
+  }
+}
+
 vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a39d2a7b5..7c5c45e42 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -521,6 +521,11 @@ public:
   void printInstantiations( std::ostream& out );
 
   /**
+   * Print solution for synthesis conjectures found by ce_guided_instantiation module
+   */
+  void printSynthSolution( std::ostream& out );
+  
+  /**
    * Get an unsatisfiable core (only if immediately preceded by an
    * UNSAT or VALID query).  Only permitted if CVC4 was built with
    * unsat-core support and produce-unsat-cores is on.
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().
    */
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index fad2719f4..06a8187f2 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -141,10 +141,11 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
 }
 
 
-void Datatype::setSygusType( Type st ){
+void Datatype::setSygus( Type st, Expr bvl ){
   CheckArgument(!d_resolved, this,
                 "cannot set sygus type to a finalized Datatype");
   d_sygus_type = st;
+  d_sygus_bvl = bvl;
 }
 
 
@@ -428,6 +429,10 @@ Type Datatype::getSygusType() const {
   return d_sygus_type;
 }
 
+Expr Datatype::getSygusVarList() const {
+  return d_sygus_bvl;
+}
+
 bool Datatype::involvesExternalType() const{
   return d_involvesExt;
 }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index b91348cdb..adb423c96 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -459,7 +459,9 @@ private:
   bool d_resolved;
   Type d_self;
   bool d_involvesExt;
+  /** information for sygus */
   Type d_sygus_type;
+  Expr d_sygus_bvl;  
 
   // "mutable" because computing the cardinality can be expensive,
   // and so it's computed just once, on demand---this is the cache
@@ -517,8 +519,11 @@ public:
    */
   void addConstructor(const DatatypeConstructor& c);
 
-  /** set the sygus type of this datatype */
-  void setSygusType( Type st );
+  /** set the sygus information of this datatype
+   *    st : the builtin type for this grammar
+   *    bvl : the list of arguments for the synth-fun
+   */
+  void setSygus( Type st, Expr bvl );
   
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
@@ -635,6 +640,8 @@ public:
   
   /** get sygus type */
   Type getSygusType() const;
+  /** get sygus var list */
+  Expr getSygusVarList() const;
 
   /**
    * Get whether this datatype involves an external type.  If so,