diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-10 15:35:07 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-10 15:35:07 +0200 |
commit | 2f2b368448c3a5e50db46b3ec2cc364ae8959ac1 (patch) | |
tree | 91576c0fd2ed7fee5da14598f15138a18c2cc27a /src/util | |
parent | 6417016a38e24b09bc062a4bd4b0a5945fbcc0ec (diff) |
Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 33 | ||||
-rw-r--r-- | src/util/datatype.h | 17 |
2 files changed, 41 insertions, 9 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 5a7a6da89..b1ab011ef 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -607,15 +607,14 @@ 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::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){ + d_sygus_op = op; + d_sygus_let_body = let_body; + d_sygus_let_args.insert( d_sygus_let_args.end(), let_args.begin(), let_args.end() ); + d_sygus_num_let_input_args = num_let_input_args; } + 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 @@ -689,6 +688,26 @@ Expr DatatypeConstructor::getSygusOp() const { return d_sygus_op; } +Expr DatatypeConstructor::getSygusLetBody() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_body; +} + +unsigned DatatypeConstructor::getNumSygusLetArgs() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_args.size(); +} + +Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_args[i]; +} + +unsigned DatatypeConstructor::getNumSygusLetInputArgs() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_num_let_input_args; +} + 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 224ac89ad..1945c4390 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -187,6 +187,9 @@ private: std::vector<DatatypeConstructorArg> d_args; /** the operator associated with this constructor (for sygus) */ Expr d_sygus_op; + Expr d_sygus_let_body; + std::vector< Expr > d_sygus_let_args; + unsigned d_sygus_num_let_input_args; void resolve(ExprManager* em, DatatypeType self, const std::map<std::string, DatatypeType>& resolutions, @@ -232,7 +235,9 @@ 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); + + /** set sygus */ + void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); /** * Add an argument (i.e., a data field) of the given name and type @@ -281,7 +286,15 @@ public: /** get sygus op */ Expr getSygusOp() const; - + /** get sygus let body */ + Expr getSygusLetBody() const; + /** get number of sygus let args */ + unsigned getNumSygusLetArgs() const; + /** get sygus let arg */ + Expr getSygusLetArg( unsigned i ) const; + /** get number of let arguments that should be printed as arguments to let */ + unsigned getNumSygusLetInputArgs() const; + /** * Get the tester name for this Datatype constructor. */ |