Accelerate sygus solution reconstruction for constants and id functions. Minor changes to sygus type registration. Print sygus let solutions assuming fixed variable names.

2 files changed, 7 insertions, 0 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index b1ab011ef..138fb4bb0 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -707,6 +707,11 @@ unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_sygus_num_let_input_args;
 }
+
+bool DatatypeConstructor::isSygusIdFunc() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
+}
   
 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 1945c4390..0b8b8c61f 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -294,6 +294,8 @@ public:
   Expr getSygusLetArg( unsigned i ) const;
   /** get number of let arguments that should be printed as arguments to let */
   unsigned getNumSygusLetInputArgs() const;
+  /** is this a sygus identity function */
+  bool isSygusIdFunc() const;
   
   /**
    * Get the tester name for this Datatype constructor.