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/printer | |
parent | 047b8f69db1ab46ad68a2693565066f2a8d40b29 (diff) |
Sygus Lambda Grammars (#1390)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 14 | ||||
-rw-r--r-- | src/printer/sygus_print_callback.cpp | 118 | ||||
-rw-r--r-- | src/printer/sygus_print_callback.h | 85 |
3 files changed, 163 insertions, 54 deletions
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<Node>& let_args, unsigned ninput_args) +SygusExprPrintCallback::SygusExprPrintCallback(Expr body, + std::vector<Expr>& 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<int>(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<Node> vars; + std::vector<Node> 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<Expr>& 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<Node> subs_lvs; std::vector<Node> 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 <vector> -#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<Expr>& 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<Expr> 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<Node>& let_args, + SygusLetExprPrintCallback(Expr let_body, + std::vector<Expr>& 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<Node> 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, |