Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.

2 files changed, 41 insertions, 9 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 5a7a6da89..b1ab011ef 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -607,15 +607,14 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
   CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 }
 
-DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester, Expr sygus_op) :
-  d_name(name + '\0' + tester),
-  d_tester(),
-  d_args(),
-  d_sygus_op(sygus_op) {
-  CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
-  CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){
+  d_sygus_op = op;
+  d_sygus_let_body = let_body;
+  d_sygus_let_args.insert( d_sygus_let_args.end(), let_args.begin(), let_args.end() );
+  d_sygus_num_let_input_args = num_let_input_args;
 }
 
+
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow
@@ -689,6 +688,26 @@ Expr DatatypeConstructor::getSygusOp() const {
   return d_sygus_op;
 }
 
+Expr DatatypeConstructor::getSygusLetBody() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_let_body;
+}
+
+unsigned DatatypeConstructor::getNumSygusLetArgs() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_let_args.size();
+}
+
+Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_let_args[i];
+} 
+
+unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_num_let_input_args;
+}
+  
 Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 224ac89ad..1945c4390 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -187,6 +187,9 @@ private:
   std::vector<DatatypeConstructorArg> d_args;
   /** the operator associated with this constructor (for sygus) */
   Expr d_sygus_op;
+  Expr d_sygus_let_body;
+  std::vector< Expr > d_sygus_let_args;
+  unsigned d_sygus_num_let_input_args;
 
   void resolve(ExprManager* em, DatatypeType self,
                const std::map<std::string, DatatypeType>& resolutions,
@@ -232,7 +235,9 @@ public:
    * constructor and tester aren't created until resolution time.
    */
   DatatypeConstructor(std::string name, std::string tester);
-  DatatypeConstructor(std::string name, std::string tester, Expr sygus_op);
+  
+  /** set sygus */
+  void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
 
   /**
    * Add an argument (i.e., a data field) of the given name and type
@@ -281,7 +286,15 @@ public:
   
   /** get sygus op */
   Expr getSygusOp() const;
-
+  /** get sygus let body */
+  Expr getSygusLetBody() const;
+  /** get number of sygus let args */
+  unsigned getNumSygusLetArgs() const;
+  /** get sygus let arg */
+  Expr getSygusLetArg( unsigned i ) const;
+  /** get number of let arguments that should be printed as arguments to let */
+  unsigned getNumSygusLetInputArgs() const;
+  
   /**
    * Get the tester name for this Datatype constructor.
    */