diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 5 | ||||
-rw-r--r-- | src/util/datatype.h | 2 |
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. |