From 20704741e4609055d61e010b6981c6916d28019a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 Nov 2017 14:25:59 -0600 Subject: [PATCH] Sygus Lambda Grammars (#1390) --- src/Makefile.am | 2 + src/expr/datatype.cpp | 71 ++---- src/expr/datatype.h | 68 ++---- src/options/smt_options | 4 +- src/parser/smt2/smt2.cpp | 221 +++++++++++------- src/parser/smt2/smt2.h | 13 ++ src/printer/smt2/smt2_printer.cpp | 14 +- src/printer/sygus_print_callback.cpp | 118 ++++++++-- src/printer/sygus_print_callback.h | 85 ++++--- .../quantifiers/ce_guided_conjecture.cpp | 8 +- .../quantifiers/ce_guided_single_inv.cpp | 25 +- .../quantifiers/quantifiers_attributes.h | 11 + .../quantifiers/term_database_sygus.cpp | 119 ++-------- src/theory/quantifiers/term_database_sygus.h | 2 - src/theory/quantifiers/term_util.h | 4 - 15 files changed, 401 insertions(+), 364 deletions(-) diff --git a/src/Makefile.am b/src/Makefile.am index dc0a2b62a..b3c4ec98c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -67,6 +67,8 @@ libcvc4_la_SOURCES = \ printer/dagification_visitor.h \ printer/printer.cpp \ printer/printer.h \ + printer/sygus_print_callback.cpp \ + printer/sygus_print_callback.h \ printer/ast/ast_printer.cpp \ printer/ast/ast_printer.h \ printer/cvc/cvc_printer.cpp \ 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& cargs, + std::shared_ptr 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 ) { - 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 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 spc); private: /** the name of the constructor */ @@ -462,14 +444,11 @@ class CVC4_PUBLIC DatatypeConstructor { std::vector d_args; /** sygus operator */ Expr d_sygus_op; - /** sygus let body */ - Expr d_sygus_let_body; - /** sygus let args */ - std::vector d_sygus_let_args; - /** sygus num let input args */ - unsigned d_sygus_num_let_input_args; + /** sygus print callback */ + std::shared_ptr 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& cargs, + std::shared_ptr spc = nullptr); /** set that this datatype is a tuple */ void setTuple(); diff --git a/src/options/smt_options b/src/options/smt_options index c701d5c20..fa6c3ae4e 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -40,7 +40,9 @@ option dumpProofs --dump-proofs bool :default false :link --proof :link-smt prod option dumpInstantiations --dump-instantiations bool :default false output instantiations of quantified formulas after every UNSAT/VALID response option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write - output mode for sygus + output mode for sygus +option sygusPrintCallbacks --sygus-print-callbacks bool :default true + use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging) option dumpSynth --dump-synth bool :read-write :default false output solution for synthesis conjectures after every UNSAT/VALID response option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a72b0ac6e..7a681f327 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -21,6 +21,7 @@ #include "parser/parser.h" #include "parser/smt1/smt1.h" #include "parser/smt2/smt2_input.h" +#include "printer/sygus_print_callback.h" #include "smt/command.h" #include "util/bitvector.h" @@ -926,23 +927,15 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) { Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; - std::vector df_name; - std::vector df_op; - std::vector< std::vector > df_let_args; - std::vector< Expr > df_let_body; - //dt.mkSygusConstructors( ops, cnames, cargs, sygus_to_builtin, - // d_sygus_let_func_to_vars, d_sygus_let_func_to_body, d_sygus_let_func_to_num_input_vars, - // df_name, df_op, df_let_args, df_let_body ); Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; - for( int i=0; i<(int)cnames.size(); i++ ){ + for (unsigned i = 0, size = cnames.size(); i < size; i++) + { bool is_dup = false; bool is_dup_op = false; - Expr let_body; - std::vector< Expr > let_args; - unsigned let_num_input_args = 0; - for( int j=0; j& ops, } } } + Debug("parser-sygus") << "SYGUS CONS " << i << " : "; if( is_dup ){ - Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << " at " << i << std::endl; + Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl; ops.erase( ops.begin() + i, ops.begin() + i + 1 ); cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 ); cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 ); i--; - }else if( is_dup_op ){ - Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] << " at " << i << std::endl; - //make into define-fun - std::vector fsorts; - for( unsigned j=0; j spc; + if (is_dup_op) + { + Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] + << std::endl; + // make into define-fun + std::vector ltypes; + for (unsigned j = 0, size = cargs[i].size(); j < size; j++) + { + ltypes.push_back(sygus_to_builtin[cargs[i][j]]); + } + std::vector largs; + Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); + + // make the let_body + std::vector children; + if (ops[i].getKind() != kind::BUILTIN) + { + children.push_back(ops[i]); + } + children.insert(children.end(), largs.begin(), largs.end()); + Kind sk = ops[i].getKind() != kind::BUILTIN + ? kind::APPLY + : getExprManager()->operatorToKind(ops[i]); + Expr body = getExprManager()->mkExpr(sk, children); + // replace by lambda + ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; + // callback prints as the expression + spc = std::make_shared(body, largs); } - //make the let_body - std::vector< Expr > children; - if( ops[i].getKind() != kind::BUILTIN ){ - children.push_back( ops[i] ); + else + { + std::map::iterator it = + d_sygus_let_func_to_body.find(ops[i]); + if (it != d_sygus_let_func_to_body.end()) + { + Debug("parser-sygus") << "--> Let expression " << ops[i] << std::endl; + Expr let_body = it->second; + std::vector let_args = d_sygus_let_func_to_vars[ops[i]]; + unsigned let_num_input_args = + d_sygus_let_func_to_num_input_vars[ops[i]]; + // the operator is just the body for the arguments + std::vector ltypes; + for (unsigned j = 0, size = let_args.size(); j < size; j++) + { + ltypes.push_back(let_args[j].getType()); + } + std::vector largs; + Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); + Expr sbody = let_body.substitute(let_args, largs); + ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, sbody); + Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; + // callback prints as a let expression + spc = std::make_shared( + let_body, let_args, let_num_input_args); + } + else if (ops[i].getType().isBitVector() && ops[i].isConst()) + { + Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " (" + << cnames[i] << ")" << std::endl; + // Since there are multiple output formats for bit-vectors and + // we are required by sygus standards to print in the exact input + // format given by the user, we use a print callback to custom print + // the given name. + spc = std::make_shared(cnames[i]); + } + else if (isDefinedFunction(ops[i])) + { + Debug("parser-sygus") << "--> Defined function " << ops[i] + << std::endl; + // turn f into (lammbda (x) (f x)) + // in a degenerate case, ops[i] may be a defined constant, + // in which case we do not replace by a lambda. + if (ops[i].getType().isFunction()) + { + std::vector ftypes = + static_cast(ops[i].getType()).getArgTypes(); + std::vector largs; + Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); + largs.insert(largs.begin(), ops[i]); + Expr body = getExprManager()->mkExpr(kind::APPLY, largs); + ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + Debug("parser-sygus") << " ...replace op : " << ops[i] + << std::endl; + } + else + { + ops[i] = getExprManager()->mkExpr(kind::APPLY, ops[i]); + Debug("parser-sygus") << " ...replace op : " << ops[i] + << std::endl; + } + // keep a callback to say it should be printed with the defined name + spc = std::make_shared(cnames[i]); + } + else + { + Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl; + } } - children.insert( children.end(), let_args.begin(), let_args.end() ); - Kind sk = ops[i].getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(ops[i]); - Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl; - let_body = getExprManager()->mkExpr( sk, children ); - Debug("parser-sygus") << ": new body of function is " << let_body << std::endl; - - Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType()); - Debug("parser-sygus") << ": function type is " << ft << std::endl; + // must rename to avoid duplication std::stringstream ss; - ss << dt.getName() << "_df_" << i; - //replace operator and name - ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + ss << dt.getName() << "_" << i << "_" << cnames[i]; cnames[i] = ss.str(); - // indicate we need a define function - df_name.push_back( ss.str() ); - df_op.push_back( ops[i] ); - df_let_args.push_back( let_args ); - df_let_body.push_back( let_body ); - - //d_sygus_defined_funs.push_back( ops[i] ); - //preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) ); - dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, 0 ); - }else{ - std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] ); - if( it!=d_sygus_let_func_to_body.end() ){ - let_body = it->second; - let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() ); - let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]]; - } - dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args ); + // add the sygus constructor + dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc); } } @@ -1030,28 +1085,25 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, //identity element Type bt = dt.getSygusType(); Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl; + std::stringstream ss; - ss << t << "_x_id"; - Expr let_body = mkBoundVar(ss.str(), bt); - std::vector< Expr > let_args; - let_args.push_back( let_body ); - //make the identity function - Type ft = getExprManager()->mkFunctionType(bt, bt); - std::stringstream ssid; - ssid << unresolved_gterm_sym[i] << "_id"; - Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); - // indicate we need a define function - df_name.push_back( ssid.str() ); - df_op.push_back( id_op ); - df_let_args.push_back( let_args ); - df_let_body.push_back( let_body ); - - //d_sygus_defined_funs.push_back( id_op ); - //preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) ); + ss << t << "_x"; + Expr var = mkBoundVar(ss.str(), bt); + std::vector lchildren; + lchildren.push_back( + getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var)); + lchildren.push_back(var); + Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren); + + // empty sygus callback (should not be printed) + std::shared_ptr sepc = + std::make_shared(); + //make the sygus argument list std::vector< Type > id_carg; id_carg.push_back( t ); - dt.addSygusConstructor( id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 ); + dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc); + //add to operators ops.push_back( id_op ); } @@ -1060,12 +1112,21 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, } } } - - - for( unsigned i=0; i& ltypes, + std::vector& lvars) +{ + for (unsigned j = 0, size = ltypes.size(); j < size; j++) + { + std::stringstream ss; + ss << dt.getName() << "_x_" << i << "_" << j; + Expr v = mkBoundVar(ss.str(), ltypes[j]); + lvars.push_back(v); } + return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars); } const void Smt2::getSygusPrimedVars( std::vector& vars, bool isPrimed ) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 9614c5524..84c049ce9 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -319,6 +319,19 @@ private: std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ); + /** make sygus bound var list + * + * This is used for converting non-builtin sygus operators to lambda + * expressions. It takes as input a datatype and constructor index (for + * naming) and a vector of type ltypes. + * It appends a bound variable to lvars for each type in ltypes, and returns + * a bound variable list whose children are lvars. + */ + Expr makeSygusBoundVarList(Datatype& dt, + unsigned i, + const std::vector& ltypes, + std::vector& lvars); + void addArithmeticOperators(); void addBitvectorOperators(); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6ceb79001..82871a1d5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1325,7 +1325,7 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw() int cIndex = Datatype::indexOf(n.getOperator().toExpr()); Assert(!dt[cIndex].getSygusOp().isNull()); SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback(); - if (spc != nullptr) + if (spc != nullptr && options::sygusPrintCallbacks()) { spc->toStreamSygus(this, out, n.toExpr()); } @@ -1351,8 +1351,16 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw() } else { - // cannot convert term to analog, print original - toStream(out, n, -1, false, 1); + Node p = n.getAttribute(theory::SygusPrintProxyAttribute()); + if (!p.isNull()) + { + out << p; + } + else + { + // cannot convert term to analog, print original + out << n; + } } } diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp index c956c32de..c5287e469 100644 --- a/src/printer/sygus_print_callback.cpp +++ b/src/printer/sygus_print_callback.cpp @@ -14,19 +14,32 @@ #include "printer/sygus_print_callback.h" +#include "expr/node.h" +#include "printer/printer.h" + using namespace CVC4::kind; using namespace std; namespace CVC4 { namespace printer { -SygusLetExpressionPrinter::SygusLetExpressionPrinter( - Node let_body, std::vector& let_args, unsigned ninput_args) +SygusExprPrintCallback::SygusExprPrintCallback(Expr body, + std::vector& args) + : d_body(body), d_body_argument(-1) { + d_args.insert(d_args.end(), args.begin(), args.end()); + for (unsigned i = 0, size = d_args.size(); i < size; i++) + { + if (d_args[i] == d_body) + { + d_body_argument = static_cast(i); + } + } } -void SygusLetExpressionConstructorPrinter::doStrReplace( - std::string& str, const std::string& oldStr, const std::string& newStr) +void SygusExprPrintCallback::doStrReplace(std::string& str, + const std::string& oldStr, + const std::string& newStr) const { size_t pos = 0; while ((pos = str.find(oldStr, pos)) != std::string::npos) @@ -36,28 +49,82 @@ void SygusLetExpressionConstructorPrinter::doStrReplace( } } -void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p, - std::ostream& out, - Expr e) +void SygusExprPrintCallback::toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const +{ + // optimization: if body is equal to an argument, then just print that one + if (d_body_argument >= 0) + { + p->toStreamSygus(out, Node::fromExpr(e[d_body_argument])); + } + else + { + // make substitution + std::vector vars; + std::vector subs; + for (unsigned i = 0, size = d_args.size(); i < size; i++) + { + vars.push_back(Node::fromExpr(d_args[i])); + std::stringstream ss; + ss << "_setpc_var_" << i; + Node lv = NodeManager::currentNM()->mkBoundVar( + ss.str(), TypeNode::fromType(d_args[i].getType())); + subs.push_back(lv); + } + + // the substituted body should be a non-sygus term + Node sbody = Node::fromExpr(d_body); + sbody = + sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + + std::stringstream body_out; + body_out << sbody; + + // do string substitution + Assert(e.getNumChildren() == d_args.size()); + std::string str_body = body_out.str(); + for (unsigned i = 0, size = d_args.size(); i < size; i++) + { + std::stringstream old_str; + old_str << subs[i]; + std::stringstream new_str; + p->toStreamSygus(new_str, Node::fromExpr(e[i])); + doStrReplace(str_body, old_str.str().c_str(), new_str.str().c_str()); + } + out << str_body; + } +} + +SygusLetExprPrintCallback::SygusLetExprPrintCallback( + Expr let_body, std::vector& let_args, unsigned ninput_args) + : SygusExprPrintCallback(let_body, let_args), + d_num_let_input_args(ninput_args) +{ +} + +void SygusLetExprPrintCallback::toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const { std::stringstream let_out; // print as let term - if (d_sygus_num_let_input_args > 0) + if (d_num_let_input_args > 0) { let_out << "(let ("; } std::vector subs_lvs; std::vector new_lvs; - for (unsigned i = 0; i < d_sygus_let_args.size(); i++) + for (unsigned i = 0, size = d_args.size(); i < size; i++) { - Node v = d_sygus_let_args[i]; + Node v = d_args[i]; subs_lvs.push_back(v); std::stringstream ss; ss << "_l_" << new_lvs.size(); Node lv = NodeManager::currentNM()->mkBoundVar(ss.str(), v.getType()); new_lvs.push_back(lv); // map free variables to proper terms - if (i < d_sygus_num_let_input_args) + if (i < d_num_let_input_args) { // it should be printed as a let argument let_out << "("; @@ -66,16 +133,17 @@ void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p, let_out << ")"; } } - if (d_sygus_num_let_input_args > 0) + if (d_num_let_input_args > 0) { let_out << ") "; } // print the body - Node slet_body = d_let_body.substitute( + Node slet_body = Node::fromExpr(d_body); + slet_body = slet_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end()); - new_lvs.insert(new_lvs.end(), lvs.begin(), lvs.end()); + // new_lvs.insert(new_lvs.end(), lvs.begin(), lvs.end()); p->toStreamSygus(let_out, slet_body); - if (d_sygus_num_let_input_args > 0) + if (d_num_let_input_args > 0) { let_out << ")"; } @@ -83,32 +151,32 @@ void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p, // ASSUMING : let_vars are interpreted literally and do not represent a class // of variables std::string lbody = let_out.str(); - for (unsigned i = 0; i < d_sygus_let_args.size(); i++) + for (unsigned i = 0, size = d_args.size(); i < size; i++) { std::stringstream old_str; old_str << new_lvs[i]; std::stringstream new_str; - if (i >= d_sygus_num_let_input_args) + if (i >= d_num_let_input_args) { p->toStreamSygus(new_str, Node::fromExpr(e[i])); } else { - new_str << d_sygus_let_args[i]; + new_str << d_args[i]; } doStrReplace(lbody, old_str.str().c_str(), new_str.str().c_str()); } out << lbody; } -SygusNamedConstructorPrinter::SygusNamedConstructorPrinter(std::string name) +SygusNamedPrintCallback::SygusNamedPrintCallback(std::string name) : d_name(name) { } -void SygusNamedConstructorPrinter::toStreamSygus(Printer* p, - std::ostream& out, - Expr e) +void SygusNamedPrintCallback::toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const { if (e.getNumChildren() > 0) { @@ -126,9 +194,9 @@ void SygusNamedConstructorPrinter::toStreamSygus(Printer* p, } } -void SygusEmptyConstructorPrinter::toStreamSygus(const Printer* p, - std::ostream& out, - Expr e) +void SygusEmptyPrintCallback::toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const { if (e.getNumChildren() == 1) { diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h index cdeec32f0..84da0f86c 100644 --- a/src/printer/sygus_print_callback.h +++ b/src/printer/sygus_print_callback.h @@ -12,18 +12,62 @@ ** \brief sygus print callback functions **/ -#include "cvc4_private.h" +#include "cvc4_public.h" #ifndef __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H #define __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H #include -#include "expr/node.h" +#include "expr/datatype.h" +#include "expr/expr.h" namespace CVC4 { namespace printer { +/** sygus expression constructor printer + * + * This class is used for printing sygus datatype constructor terms whose top + * symbol is an expression, such as a custom defined lambda. For example, for + * sygus grammar: + * A -> (+ x A B) | x | y + * B -> 0 | 1 + * The first constructor, call it C_f for A takes two arguments (A, B) and has + * sygus operator + * (lambda ((z Int) (w Int)) (+ x z w)) + * For this operator, we set a print callback that prints, e.g. the term + * C_f( t1, t2 ) + * is printed as: + * "(+ x [out1] [out2])" + * where out1 is the result of p->toStreamSygus(out,t1) and + * out2 is the result of p->toStreamSygus(out,t2). + */ +class CVC4_PUBLIC SygusExprPrintCallback : public SygusPrintCallback +{ + public: + SygusExprPrintCallback(Expr body, std::vector& args); + ~SygusExprPrintCallback() {} + /** print sygus term e on output out using printer p */ + virtual void toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const override; + + protected: + /** body of the sygus term */ + Expr d_body; + /** arguments */ + std::vector d_args; + /** body argument */ + int d_body_argument; + /** do string replace + * + * Replaces all occurrences of oldStr with newStr in str. + */ + void doStrReplace(std::string& str, + const std::string& oldStr, + const std::string& newStr) const; +}; + /** sygus let expression constructor printer * * This class is used for printing sygus @@ -33,8 +77,8 @@ namespace printer { * A -> (let ((x B)) (+ A 1)) | x | (+ A A) | 0 * B -> 0 | 1 * the first constructor for A takes as arguments - * (B,A) and has operator - * (lambda ((y B) (z A)) (+ z 1)) + * (B,A) and has sygus operator + * (lambda ((y Int) (z Int)) (+ z 1)) * CVC4's support for let expressions in grammars * is highly limited, since notice that the * argument y : B is unused. @@ -46,32 +90,21 @@ namespace printer { * y is an original input argument of the * let expression, but z is not. */ -class SygusLetExpressionConstructorPrinter - : public SygusDatatypeConstructorPrinter +class CVC4_PUBLIC SygusLetExprPrintCallback : public SygusExprPrintCallback { public: - SygusLetExpressionPrinter(Node let_body, - std::vector& let_args, + SygusLetExprPrintCallback(Expr let_body, + std::vector& let_args, unsigned ninput_args); - ~SygusLetExpressionPrinter() {} + ~SygusLetExprPrintCallback() {} /** print sygus term e on output out using printer p */ virtual void toStreamSygus(const Printer* p, std::ostream& out, Expr e) const override; private: - /** let body of the sygus term */ - Node d_sygus_let_body; - /** let arguments */ - std::vector d_sygus_let_args; /** number of arguments that are interpreted as input arguments */ - unsigned d_sygus_num_let_input_args; - /** do string replace - * Replaces all occurrences of oldStr with newStr in str. - */ - void doStrReplace(std::string& str, - const std::string& oldStr, - const std::string& newStr) const; + unsigned d_num_let_input_args; }; /** sygus named constructor printer @@ -88,11 +121,11 @@ class SygusLetExpressionConstructorPrinter * the first sygus datatype constructor f, where we use * analog operator (lambda (x) (+ x 1)). */ -class SygusNamedConstructorPrinter : public SygusDatatypeConstructorPrinter +class CVC4_PUBLIC SygusNamedPrintCallback : public SygusPrintCallback { public: - SygusNamedConstructorPrinter(std::string name); - ~SygusNamedConstructorPrinter() {} + SygusNamedPrintCallback(std::string name); + ~SygusNamedPrintCallback() {} /** print sygus term e on output out using printer p */ virtual void toStreamSygus(const Printer* p, std::ostream& out, @@ -112,11 +145,11 @@ class SygusNamedConstructorPrinter : public SygusDatatypeConstructorPrinter * The first constructor of A, call it cons, has sygus operator (lambda (x) x). * Call toStreamSygus on cons( t ) should call toStreamSygus on t directly. */ -class SygusEmptyConstructorPrinter : public SygusDatatypeConstructorPrinter +class CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback { public: - SygusEmptyConstructorPrinter(std::string name); - ~SygusEmptyConstructorPrinter() {} + SygusEmptyPrintCallback() {} + ~SygusEmptyPrintCallback() {} /** print sygus term e on output out using printer p */ virtual void toStreamSygus(const Printer* p, std::ostream& out, diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index e1bc32761..bc6817560 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -15,7 +15,9 @@ #include "theory/quantifiers/ce_guided_conjecture.h" #include "expr/datatype.h" +#include "options/base_options.h" #include "options/quantifiers_options.h" +#include "printer/printer.h" #include "prop/prop_engine.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" @@ -428,8 +430,7 @@ void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& TypeNode tn = nv.getType(); Trace("cegqi-engine") << n[i] << " -> "; std::stringstream ss; - std::vector< Node > lvs; - TermDbSygus::printSygusTerm( ss, nv, lvs ); + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv); Trace("cegqi-engine") << ss.str() << " "; } Assert( !nv.isNull() ); @@ -621,8 +622,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation if( status==0 ){ out << sol; }else{ - std::vector< Node > lvs; - TermDbSygus::printSygusTerm( out, sol, lvs ); + Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol); } out << ")" << std::endl; } diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 03026069f..b2b4fe18c 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -143,22 +143,12 @@ void CegConjectureSingleInv::initialize( Node q ) { d_sip->debugPrint( "cegqi-si" ); //map from program to bound variables - std::vector< Node > order_vars; - std::map< Node, Node > single_inv_app_map; - for( unsigned j=0; jgetFirstOrderVariableForFunction(prog); - if (!pv.isNull()) - { - Node inv = d_sip->getFunctionInvocationFor(prog); - Assert(!inv.isNull()); - single_inv_app_map[prog] = inv; - Trace("cegqi-si") << " " << pv << ", " << inv << " is associated with program " << prog << std::endl; - d_prog_to_sol_index[prog] = order_vars.size(); - order_vars.push_back( pv ); - }else{ - Trace("cegqi-si") << " " << prog << " has no fo var." << std::endl; - } + std::vector funcs; + d_sip->getFunctions(funcs); + for (unsigned j = 0, size = funcs.size(); j < size; j++) + { + Assert(std::find(progs.begin(), progs.end(), funcs[j]) != progs.end()); + d_prog_to_sol_index[funcs[j]] = j; } //check if it is single invocation @@ -180,7 +170,8 @@ void CegConjectureSingleInv::initialize( Node q ) { Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; std::vector sivars; d_sip->getSingleInvocationVariables(sivars); - Node invariant = single_inv_app_map[prog]; + Node invariant = d_sip->getFunctionInvocationFor(prog); + Assert(!invariant.isNull()); invariant = invariant.substitute(sivars.begin(), sivars.end(), prog_templ_vars.begin(), diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index b618fc5d5..9a18d13fb 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -55,6 +55,17 @@ typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute; struct SynthesisAttributeId {}; typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; +/** Attribute for setting printing information for sygus variables + * + * For variable d of sygus datatype type, if + * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t. + */ +struct SygusPrintProxyAttributeId +{ +}; +typedef expr::Attribute + SygusPrintProxyAttribute; + namespace quantifiers { /** Attribute priority for rewrite rules */ diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index e212e0dfb..8625d9089 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -21,6 +21,7 @@ #include "smt/smt_engine.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/ce_guided_conjecture.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/theory_quantifiers.h" @@ -277,13 +278,6 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int ret = children[0]; }else{ ret = NodeManager::currentNM()->mkNode( ok, children ); - /* - Node n = NodeManager::currentNM()->mkNode( APPLY, children ); - //must expand definitions - Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) ); - Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl; - return ne; - */ } } Trace("sygus-db-debug") << "...returning " << ret << std::endl; @@ -345,13 +339,12 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) { // if we are not interested in reconstructing constants, or the grammar allows them, return a proxy if( !options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst() ){ Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" ); - SygusProxyAttribute spa; + SygusPrintProxyAttribute spa; k.setAttribute(spa,c); sc = k; }else{ int carg = getOpConsNum( tn, c ); if( carg!=-1 ){ - //sc = Node::fromExpr( dt[carg].getSygusOp() ); sc = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) ); }else{ //identity functions @@ -1545,110 +1538,28 @@ void doStrReplace(std::string& str, const std::string& oldStr, const std::string Kind TermDbSygus::getOperatorKind( Node op ) { Assert( op.getKind()!=BUILTIN ); - if( smt::currentSmtEngine()->isDefinedFunction( op.toExpr() ) ){ + Assert(!smt::currentSmtEngine()->isDefinedFunction(op.toExpr())); + if (op.getKind() == LAMBDA) + { return APPLY; }else{ TypeNode tn = op.getType(); if( tn.isConstructor() ){ return APPLY_CONSTRUCTOR; - }else if( tn.isSelector() ){ + } + else if (tn.isSelector()) + { return APPLY_SELECTOR; - }else if( tn.isTester() ){ + } + else if (tn.isTester()) + { return APPLY_TESTER; - }else{ - return NodeManager::operatorToKind( op ); } - } -} - -void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ) { - if( n.getKind()==APPLY_CONSTRUCTOR ){ - TypeNode tn = n.getType(); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isSygus() ){ - int cIndex = Datatype::indexOf( n.getOperator().toExpr() ); - Assert( !dt[cIndex].getSygusOp().isNull() ); - if( dt[cIndex].getSygusLetBody().isNull() ){ - if( n.getNumChildren()>0 ){ - out << "("; - } - Node op = dt[cIndex].getSygusOp(); - if( op.getType().isBitVector() && op.isConst() ){ - //print in the style it was given - Trace("sygus-print-bvc") << "[Print " << op << " " << dt[cIndex].getName() << "]" << std::endl; - std::stringstream ss; - ss << dt[cIndex].getName(); - std::string str = ss.str(); - std::size_t found = str.find_last_of("_"); - Assert( found!=std::string::npos ); - std::string name = std::string( str.begin() + found +1, str.end() ); - out << name; - }else{ - out << op; - } - if( n.getNumChildren()>0 ){ - for( unsigned i=0; i0 ){ - let_out << "(let ("; - } - std::vector< Node > subs_lvs; - std::vector< Node > new_lvs; - for( unsigned i=0; imkBoundVar( ss.str(), v.getType() ); - new_lvs.push_back( lv ); - //map free variables to proper terms - if( i0 ){ - let_out << ") "; - } - //print the body - Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() ); - let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() ); - new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() ); - printSygusTerm( let_out, let_body, new_lvs ); - if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ - let_out << ")"; - } - //do variable substitutions since ASSUMING : let_vars are interpreted literally and do not represent a class of variables - std::string lbody = let_out.str(); - for( unsigned i=0; i=dt[cIndex].getNumSygusLetInputArgs() ){ - printSygusTerm( new_str, n[i], lvs ); - }else{ - new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) ); - } - doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() ); - } - out << lbody; - } - return; + else if (tn.isFunction()) + { + return APPLY_UF; } - }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){ - out << n.getAttribute(SygusProxyAttribute()); - }else{ - out << n; + return NodeManager::operatorToKind(op); } } diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index 5ff1612c9..45851c0c8 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -198,8 +198,6 @@ public: /** get operator kind */ static Kind getOperatorKind( Node op ); - /** print sygus term */ - static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ); /** get anchor */ static Node getAnchor( Node n ); diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index d2a8a14f0..5ac21dafb 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -62,10 +62,6 @@ typedef expr::Attribute RrPriorityAttribute; struct LtePartialInstAttributeId {}; typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute; -// attribute for sygus proxy variables -struct SygusProxyAttributeId {}; -typedef expr::Attribute SygusProxyAttribute; - // attribute for associating a synthesis function with a first order variable struct SygusSynthGrammarAttributeId {}; typedef expr::Attribute -- 2.30.2