diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 14:23:04 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 14:23:04 +0100 |
commit | a50f977b02c5653e03d4f3d9d8c7df1f9e2be48e (patch) | |
tree | 9e8c569a9250c6c8c7eb7826539e63ae414133d9 /src/util | |
parent | 9e5b1fd1083c1c82d5bbc61a4a316211db629c43 (diff) |
Mark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus regressions.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 22 | ||||
-rw-r--r-- | src/util/datatype.h | 17 |
2 files changed, 39 insertions, 0 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 7813626a7..c15e103f9 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -140,6 +140,14 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { d_constructors.push_back(c); } + +void Datatype::setSygusType( Type st ){ + CheckArgument(!d_resolved, this, + "cannot set sygus type to a finalized Datatype"); + d_sygus_type = st; +} + + Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); @@ -543,6 +551,15 @@ 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::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 @@ -611,6 +628,11 @@ Expr DatatypeConstructor::getTester() const { return d_tester; } +Expr DatatypeConstructor::getSygusOp() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_op; +} + 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 32fae8235..084202956 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -185,6 +185,8 @@ private: Expr d_constructor; Expr d_tester; std::vector<DatatypeConstructorArg> d_args; + /** the operator associated with this constructor (for sygus) */ + Expr d_sygus_op; void resolve(ExprManager* em, DatatypeType self, const std::map<std::string, DatatypeType>& resolutions, @@ -223,6 +225,7 @@ 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); /** * Add an argument (i.e., a data field) of the given name and type @@ -268,6 +271,9 @@ public: * Datatype must be resolved. */ Expr getTester() const; + + /** get sygus op */ + Expr getSygusOp() const; /** * Get the tester name for this Datatype constructor. @@ -453,6 +459,7 @@ private: bool d_resolved; Type d_self; bool d_involvesExt; + Type d_sygus_type; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache @@ -510,6 +517,9 @@ public: */ void addConstructor(const DatatypeConstructor& c); + /** set the sygus type of this datatype */ + void setSygusType( Type st ); + /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -530,6 +540,9 @@ public: /** is this a co-datatype? */ inline bool isCodatatype() const; + + /** is this a sygus datatype? */ + inline bool isSygus() const; /** * Return the cardinality of this datatype (the sum of the @@ -720,6 +733,10 @@ inline bool Datatype::isCodatatype() const { return d_isCo; } +inline bool Datatype::isSygus() const { + return !d_sygus_type.isNull(); +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } |