diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-22 14:25:59 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-22 14:25:59 -0600 |
commit | 20704741e4609055d61e010b6981c6916d28019a (patch) | |
tree | a8e8beec06083b91c2336e3013538e86eb177a29 /src/expr | |
parent | 047b8f69db1ab46ad68a2693565066f2a8d40b29 (diff) |
Sygus Lambda Grammars (#1390)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 71 | ||||
-rw-r--r-- | src/expr/datatype.h | 68 |
2 files changed, 41 insertions, 98 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index f654f2608..513cb2170 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -181,25 +181,18 @@ 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, std::string& cname, std::vector< CVC4::Type >& cargs, - CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) { +void Datatype::addSygusConstructor(CVC4::Expr op, + std::string& cname, + std::vector<CVC4::Type>& cargs, + std::shared_ptr<SygusPrintCallback> spc) +{ Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl; - if( !let_body.isNull() ){ - Debug("dt-sygus") << " let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl; - //TODO : remove arguments not occurring in body - //if this is a self identity function, ignore - if( let_args.size()==0 && let_args[0]==let_body ){ - Debug("dt-sygus") << " identity function " << cargs[0] << " to " << getName() << std::endl; - //TODO - } - } + Debug("dt-sygus") << " sygus op : " << op << std::endl; std::string name = getName() + "_" + cname; std::string testerId("is-"); testerId.append(name); - //checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - //checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); CVC4::DatatypeConstructor c(name, testerId ); - c.setSygus( op, let_body, let_args, let_num_input_args ); + c.setSygus(op, spc); for( unsigned j=0; j<cargs.size(); j++ ){ Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl; std::stringstream sname; @@ -208,13 +201,6 @@ void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vect } addConstructor(c); } - -void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs ) { - CVC4::Expr let_body; - std::vector< CVC4::Expr > let_args; - unsigned let_num_input_args = 0; - addSygusConstructor( op, cname, cargs, let_body, let_args, let_num_input_args ); -} void Datatype::setTuple() { PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype"); @@ -784,7 +770,8 @@ DatatypeConstructor::DatatypeConstructor(std::string name) d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO" d_tester(), d_args(), - d_sygus_num_let_input_args(0) { + d_sygus_pc(nullptr) +{ PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); } @@ -796,16 +783,19 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) d_name(name + '\0' + tester), d_tester(), d_args(), - d_sygus_num_let_input_args(0) { + d_sygus_pc(nullptr) +{ PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); PrettyCheckArgument(!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 ){ +void DatatypeConstructor::setSygus(Expr op, + std::shared_ptr<SygusPrintCallback> spc) +{ + PrettyCheckArgument( + !isResolved(), this, "cannot modify a finalized Datatype constructor"); 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; + d_sygus_pc = spc; } void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { @@ -882,37 +872,18 @@ Expr DatatypeConstructor::getSygusOp() const { return d_sygus_op; } -Expr DatatypeConstructor::getSygusLetBody() const { - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - return d_sygus_let_body; -} - -unsigned DatatypeConstructor::getNumSygusLetArgs() const { - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - return d_sygus_let_args.size(); -} - -Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const { - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - return d_sygus_let_args[i]; -} - -unsigned DatatypeConstructor::getNumSygusLetInputArgs() const { - PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - return d_sygus_num_let_input_args; -} - bool DatatypeConstructor::isSygusIdFunc() const { PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body; + return (d_sygus_op.getKind() == kind::LAMBDA + && d_sygus_op[0].getNumChildren() == 1 + && d_sygus_op[0][0] == d_sygus_op[1]); } SygusPrintCallback* DatatypeConstructor::getSygusPrintCallback() const { PrettyCheckArgument( isResolved(), this, "this datatype constructor is not yet resolved"); - // TODO (#1344) return the stored callback - return nullptr; + return d_sygus_pc.get(); } Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) { diff --git a/src/expr/datatype.h b/src/expr/datatype.h index a92a0738e..85ecfb946 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -191,7 +191,7 @@ class CVC4_PUBLIC SygusPrintCallback { public: SygusPrintCallback() {} - ~SygusPrintCallback() {} + virtual ~SygusPrintCallback() {} /** * Writes the term that sygus datatype expression e * encodes to stream out. p is the printer that @@ -232,6 +232,7 @@ class CVC4_PUBLIC DatatypeConstructor { */ DatatypeConstructor(std::string name, std::string tester); + ~DatatypeConstructor() {} /** * Add an argument (i.e., a data field) of the given name and type * to this Datatype constructor. Selector names need not be unique; @@ -287,29 +288,10 @@ class CVC4_PUBLIC DatatypeConstructor { * deep embedding. */ Expr getSygusOp() const; - /** get sygus let body - * - * The sygus official format - * (http://www.sygus.org/SyGuS-COMP2015.html) - * allows for let expressions to occur in grammars. - * - * TODO (#1344) refactor this - */ - Expr getSygusLetBody() const; - /** get number of sygus let args - * TODO (#1344) refactor this - */ - unsigned getNumSygusLetArgs() const; - /** get sygus let arg - * TODO (#1344) refactor this - */ - Expr getSygusLetArg( unsigned i ) const; - /** get number of let arguments that should be printed as arguments to let - * TODO (#1344) refactor this - */ - unsigned getNumSygusLetInputArgs() const; /** is this a sygus identity function? - * TODO (#1344) refactor this + * + * This returns true if the sygus operator of this datatype constructor is + * of the form (lambda (x) x). */ bool isSygusIdFunc() const; /** get sygus print callback @@ -431,11 +413,13 @@ class CVC4_PUBLIC DatatypeConstructor { int getSelectorIndexInternal( Expr sel ) const; /** involves external type + * * Get whether this constructor has a subfield * in any constructor that is not a datatype type. */ bool involvesExternalType() const; /** involves external type + * * Get whether this constructor has a subfield * in any constructor that is an uninterpreted type. */ @@ -443,13 +427,11 @@ class CVC4_PUBLIC DatatypeConstructor { /** set sygus * - * Set that this constructor is a sygus datatype - * constructor that encodes operator op. - * The remaining arguments are for handling - * let expressions in user-provided sygus - * grammars (see above). + * Set that this constructor is a sygus datatype constructor that encodes + * operator op. spc is the sygus callback of this datatype constructor, + * which is stored in a shared pointer. */ - void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); + void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc); private: /** the name of the constructor */ @@ -462,14 +444,11 @@ class CVC4_PUBLIC DatatypeConstructor { std::vector<DatatypeConstructorArg> d_args; /** sygus operator */ Expr d_sygus_op; - /** sygus let body */ - Expr d_sygus_let_body; - /** sygus let args */ - std::vector<Expr> d_sygus_let_args; - /** sygus num let input args */ - unsigned d_sygus_num_let_input_args; + /** sygus print callback */ + std::shared_ptr<SygusPrintCallback> d_sygus_pc; /** shared selectors for each type + * * This stores the shared (constructor-agnotic) * selectors that access the fields of this datatype. * In the terminology of "Datatypes with Shared Selectors", @@ -673,25 +652,18 @@ public: * this constructor encodes * cname : the name of the constructor (for printing only) * cargs : the arguments of the constructor + * spc : an (optional) callback that is used for custom printing. This is + * to accomodate user-provided grammars in the sygus format. * * It should be the case that cargs are sygus datatypes that * 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. */ - void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs ); - /** add sygus constructor (for let expression constructors) - * - * This adds a sygus constructor to this datatype, where - * this datatype should be currently unresolved. - * - * In contrast to the above function, the constructor we - * add corresponds to a let expression if let_body is - * non-null. For details, see documentation for - * DatatypeConstructor::getSygusLetBody above. - */ - void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, - CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ); + void addSygusConstructor(CVC4::Expr op, + std::string& cname, + std::vector<CVC4::Type>& cargs, + std::shared_ptr<SygusPrintCallback> spc = nullptr); /** set that this datatype is a tuple */ void setTuple(); |