diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-11 20:06:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-11 20:06:21 +0200 |
commit | 54f1d00d5475710ec5a4c3eab82d786ba95dfdde (patch) | |
tree | 547bd29a009a3d119a26b2ddcd509a3ef2e5d061 /src/util | |
parent | 870b29b0cce85941ed72d7e0ca75b61b0cfcf711 (diff) |
Allow sygus with no syntactic restrictions for LIA. Add regressions.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 9 | ||||
-rw-r--r-- | src/util/datatype.h | 5 |
2 files changed, 11 insertions, 3 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 18ef25e7f..948bad56c 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -134,12 +134,13 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { } -void Datatype::setSygus( Type st, Expr bvl, bool allow_const ){ +void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ CheckArgument(!d_resolved, this, "cannot set sygus type to a finalized Datatype"); d_sygus_type = st; d_sygus_bvl = bvl; - d_sygus_allow_const = allow_const; + d_sygus_allow_const = allow_const || allow_all; + d_sygus_allow_const = allow_all; } @@ -475,6 +476,10 @@ bool Datatype::getSygusAllowConst() const { return d_sygus_allow_const; } +bool Datatype::getSygusAllowAll() const { + return d_sygus_allow_const; +} + bool Datatype::involvesExternalType() const{ return d_involvesExt; } diff --git a/src/util/datatype.h b/src/util/datatype.h index 79e7bf7d7..224ac89ad 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -457,6 +457,7 @@ private: Type d_sygus_type; Expr d_sygus_bvl; bool d_sygus_allow_const; + bool d_sygus_allow_all; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache @@ -537,7 +538,7 @@ public: * bvl : the list of arguments for the synth-fun * allow_const : whether all constants are (implicitly) included in the grammar */ - void setSygus( Type st, Expr bvl, bool allow_const ); + void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ); /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -668,6 +669,8 @@ public: Expr getSygusVarList() const; /** does it allow constants */ bool getSygusAllowConst() const; + /** does it allow constants */ + bool getSygusAllowAll() const; /** * Get whether this datatype involves an external type. If so, |