diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-26 13:11:01 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-26 13:11:01 +0100 |
commit | edd8886e56c8bb84f3fd85fc6f697d870bc0a3b7 (patch) | |
tree | 1fe3e8699f3c4831a302a369b377396ae5a347a4 /src/util | |
parent | f3045ccce9d30114f6e90cfa72de176da344cb1f (diff) |
Output solutions for synthesis conjectures with --dump-synth. Minor refactor of previous commit.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 7 | ||||
-rw-r--r-- | src/util/datatype.h | 11 |
2 files changed, 15 insertions, 3 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index fad2719f4..06a8187f2 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -141,10 +141,11 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { } -void Datatype::setSygusType( Type st ){ +void Datatype::setSygus( Type st, Expr bvl ){ CheckArgument(!d_resolved, this, "cannot set sygus type to a finalized Datatype"); d_sygus_type = st; + d_sygus_bvl = bvl; } @@ -428,6 +429,10 @@ Type Datatype::getSygusType() const { return d_sygus_type; } +Expr Datatype::getSygusVarList() const { + return d_sygus_bvl; +} + bool Datatype::involvesExternalType() const{ return d_involvesExt; } diff --git a/src/util/datatype.h b/src/util/datatype.h index b91348cdb..adb423c96 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -459,7 +459,9 @@ private: bool d_resolved; Type d_self; bool d_involvesExt; + /** information for sygus */ Type d_sygus_type; + Expr d_sygus_bvl; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache @@ -517,8 +519,11 @@ public: */ void addConstructor(const DatatypeConstructor& c); - /** set the sygus type of this datatype */ - void setSygusType( Type st ); + /** set the sygus information of this datatype + * st : the builtin type for this grammar + * bvl : the list of arguments for the synth-fun + */ + void setSygus( Type st, Expr bvl ); /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -635,6 +640,8 @@ public: /** get sygus type */ Type getSygusType() const; + /** get sygus var list */ + Expr getSygusVarList() const; /** * Get whether this datatype involves an external type. If so, |