diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-01 11:43:02 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-01 11:43:02 -0600 |
commit | ffc78cdf25327d18f7ff5b265f78480248907cab (patch) | |
tree | 157d6c3e2fc9be22e2b66462c31936b967302677 /src/expr | |
parent | f40d813048599b58327fc968344301d39f156da2 (diff) |
Minor additions for sygus (#1419)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 27 | ||||
-rw-r--r-- | src/expr/datatype.h | 28 |
2 files changed, 44 insertions, 11 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 8b6384dcc..f96066e80 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -181,17 +181,19 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ d_sygus_allow_all = allow_all; } -void Datatype::addSygusConstructor(CVC4::Expr op, +void Datatype::addSygusConstructor(Expr op, std::string& cname, - std::vector<CVC4::Type>& cargs, - std::shared_ptr<SygusPrintCallback> spc) + std::vector<Type>& cargs, + std::shared_ptr<SygusPrintCallback> spc, + int weight) { Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl; Debug("dt-sygus") << " sygus op : " << op << std::endl; std::string name = getName() + "_" + cname; std::string testerId("is-"); testerId.append(name); - CVC4::DatatypeConstructor c(name, testerId ); + unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1); + DatatypeConstructor c(name, testerId, cweight); c.setSygus(op, spc); for( unsigned j=0; j<cargs.size(); j++ ){ Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl; @@ -770,12 +772,15 @@ DatatypeConstructor::DatatypeConstructor(std::string name) d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO" d_tester(), d_args(), - d_sygus_pc(nullptr) + d_sygus_pc(nullptr), + d_weight(1) { PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); } -DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) +DatatypeConstructor::DatatypeConstructor(std::string name, + std::string tester, + unsigned weight) : // 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 // the tester name away inside the constructor name until @@ -783,7 +788,8 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) d_name(name + '\0' + tester), d_tester(), d_args(), - d_sygus_pc(nullptr) + d_sygus_pc(nullptr), + d_weight(weight) { PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); @@ -879,6 +885,13 @@ bool DatatypeConstructor::isSygusIdFunc() const { && d_sygus_op[0][0] == d_sygus_op[1]); } +unsigned DatatypeConstructor::getWeight() const +{ + PrettyCheckArgument( + isResolved(), this, "this datatype constructor is not yet resolved"); + return d_weight; +} + std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const { PrettyCheckArgument( diff --git a/src/expr/datatype.h b/src/expr/datatype.h index b899b0099..b3c81911f 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -229,8 +229,13 @@ class CVC4_PUBLIC DatatypeConstructor { * Create a new Datatype constructor with the given name for the * constructor and the given name for the tester. The actual * constructor and tester aren't created until resolution time. + * weight is the value that this constructor carries when computing size. + * For example, if A, B, C have weights 0, 1, and 3 respectively, then + * C( B( A() ), B( A() ) ) has size 5. */ - DatatypeConstructor(std::string name, std::string tester); + DatatypeConstructor(std::string name, + std::string tester, + unsigned weight = 1); ~DatatypeConstructor() {} /** @@ -295,12 +300,19 @@ class CVC4_PUBLIC DatatypeConstructor { */ bool isSygusIdFunc() const; /** get sygus print callback + * * This class stores custom ways of printing * sygus datatype constructors, for instance, * to handle defined or let expressions that * appear in user-provided grammars. */ std::shared_ptr<SygusPrintCallback> getSygusPrintCallback() const; + /** get weight + * + * Get the weight of this constructor. This value is used when computing the + * size of datatype terms that involve this constructor. + */ + unsigned getWeight() const; /** * Get the tester name for this Datatype constructor. @@ -446,6 +458,8 @@ class CVC4_PUBLIC DatatypeConstructor { Expr d_sygus_op; /** sygus print callback */ std::shared_ptr<SygusPrintCallback> d_sygus_pc; + /** weight */ + unsigned d_weight; /** shared selectors for each type * @@ -659,11 +673,17 @@ public: * encode the arguments of op. For example, a sygus constructor * with op = PLUS should be such that cargs.size()>=2 and * the sygus type of cargs[i] is Real/Int for each i. + * + * weight denotes the value added by the constructor when computing the size + * of datatype terms. Passing a value <0 denotes the default weight for the + * constructor, which is 0 for nullary constructors and 1 for non-nullary + * constructors. */ - void addSygusConstructor(CVC4::Expr op, + void addSygusConstructor(Expr op, std::string& cname, - std::vector<CVC4::Type>& cargs, - std::shared_ptr<SygusPrintCallback> spc = nullptr); + std::vector<Type>& cargs, + std::shared_ptr<SygusPrintCallback> spc = nullptr, + int weight = -1); /** set that this datatype is a tuple */ void setTuple(); |