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

2 files changed, 15 insertions, 3 deletions

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,