From: Andrew Reynolds Date: Wed, 15 Nov 2017 22:48:26 +0000 (-0600) Subject: Sygus print callbacks (#1348) X-Git-Tag: cvc5-1.0.0~5470 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9bff14c12c34fea0e6ba0649a3e8f7e8f48b5646;p=cvc5.git Sygus print callbacks (#1348) * Initial infrastructure for sygus printing. * Minor * Minor improvements * Format * Minor * Empty constructor printer. * Format * Minor * Format * Address. --- diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index a8cd83215..f654f2608 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -907,6 +907,14 @@ bool DatatypeConstructor::isSygusIdFunc() const { return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body; } +SygusPrintCallback* DatatypeConstructor::getSygusPrintCallback() const +{ + PrettyCheckArgument( + isResolved(), this, "this datatype constructor is not yet resolved"); + // TODO (#1344) return the stored callback + return nullptr; +} + Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); diff --git a/src/expr/datatype.h b/src/expr/datatype.h index da0a9813f..a92a0738e 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -178,6 +178,32 @@ public: DatatypeConstructorArg(std::string name, Expr selector); };/* class DatatypeConstructorArg */ +class Printer; + +/** sygus datatype constructor printer + * + * This is a virtual class that is used to specify + * a custom printing callback for sygus terms. This is + * useful for sygus grammars that include defined + * functions or let expressions. + */ +class CVC4_PUBLIC SygusPrintCallback +{ + public: + SygusPrintCallback() {} + ~SygusPrintCallback() {} + /** + * Writes the term that sygus datatype expression e + * encodes to stream out. p is the printer that + * requested that expression e be written on output + * stream out. Calls may be made to p to print + * subterms of e. + */ + virtual void toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const = 0; +}; + /** * A constructor for a Datatype. */ @@ -286,6 +312,13 @@ class CVC4_PUBLIC DatatypeConstructor { * TODO (#1344) refactor this */ 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. + */ + SygusPrintCallback* getSygusPrintCallback() const; /** * Get the tester name for this Datatype constructor. diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index fd7a4ee19..e50b1970f 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -70,7 +70,12 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { } }/* Printer::makePrinter() */ - +void Printer::toStreamSygus(std::ostream& out, TNode n) const throw() +{ + // no sygus-specific printing associated with this printer, + // just print the original term + toStream(out, n, -1, false, 1); +} void Printer::toStream(std::ostream& out, const Model& m) const throw() { for(size_t i = 0; i < m.getNumCommands(); ++i) { diff --git a/src/printer/printer.h b/src/printer/printer.h index ea4865fce..9baeeb8b6 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -69,14 +69,27 @@ public: /** Write a CommandStatus out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0; - - /** Write a Model out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const Model& m) const throw(); /** Write an UnsatCore out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const UnsatCore& core) const throw(); + /** + * Write the term that sygus datatype term n + * encodes to a stream with this Printer. + * For example, consider the datatype term + * (C_plus (C_minus C_x C_0) C_y) + * where C_plus, C_minus, C_x, C_0, C_y are constructors + * whose sygus operators are PLUS, MINUS, x, 0, y. + * In this case, this method is equivalent to printing + * the integer term: + * (PLUS (MINUS x 0) y) + * This method may make calls to sygus printing callback + * methods stored in sygus datatype constructors. + */ + virtual void toStreamSygus(std::ostream& out, TNode n) const throw(); + };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8a80ba59e..6ceb79001 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -364,9 +364,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::CHAIN: break; case kind::FUNCTION_TYPE: out << "->"; - for(size_t i = 0; i < n.getNumChildren(); ++i) { + for (Node nc : n) + { out << " "; - toStream(out, n[i], toDepth, types, TypeNode::null()); + toStream(out, nc, toDepth, types, TypeNode::null()); } out << ")"; return; @@ -382,11 +383,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // uf theory case kind::APPLY_UF: typeChildren = true; break; - // higher-order + // higher-order case kind::HO_APPLY: break; - case kind::LAMBDA: out << smtKindString(k) << " "; break; - - // arith theory + case kind::LAMBDA: + out << smtKindString(k) << " "; + break; + + // arith theory case kind::PLUS: case kind::MULT: case kind::NONLINEAR_MULT: @@ -819,10 +822,11 @@ static string smtKindString(Kind k) throw() { // uf theory case kind::APPLY_UF: break; - - case kind::LAMBDA: return "lambda"; - // arith theory + case kind::LAMBDA: + return "lambda"; + + // arith theory case kind::PLUS: return "+"; case kind::MULT: case kind::NONLINEAR_MULT: return "*"; @@ -1310,6 +1314,47 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) } } +void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw() +{ + if (n.getKind() == kind::APPLY_CONSTRUCTOR) + { + TypeNode tn = n.getType(); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + if (dt.isSygus()) + { + int cIndex = Datatype::indexOf(n.getOperator().toExpr()); + Assert(!dt[cIndex].getSygusOp().isNull()); + SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback(); + if (spc != nullptr) + { + spc->toStreamSygus(this, out, n.toExpr()); + } + else + { + if (n.getNumChildren() > 0) + { + out << "("; + } + out << dt[cIndex].getSygusOp(); + if (n.getNumChildren() > 0) + { + for (Node nc : n) + { + out << " "; + toStreamSygus(out, nc); + } + out << ")"; + } + } + return; + } + } + else + { + // cannot convert term to analog, print original + toStream(out, n, -1, false, 1); + } +} static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "(assert " << c->getExpr() << ")"; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index b7e9e1f40..96f55d7a2 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -48,11 +48,17 @@ public: void toStream(std::ostream& out, const CommandStatus* s) const throw(); void toStream(std::ostream& out, const SExpr& sexpr) const throw(); void toStream(std::ostream& out, const Model& m) const throw(); - /** print the unsat core to the stream out. - * We use the expression names that are stored in the SMT engine associated - * with the core (UnsatCore::getSmtEngine) for printing named assertions. - */ + /** + * Writes the unsat core to the stream out. + * We use the expression names that are stored in the SMT engine associated + * with the core (UnsatCore::getSmtEngine) for printing named assertions. + */ void toStream(std::ostream& out, const UnsatCore& core) const throw(); + /** + * Write the term that sygus datatype term node n + * encodes to a stream with this Printer. + */ + virtual void toStreamSygus(std::ostream& out, TNode n) const throw() override; };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp new file mode 100644 index 000000000..c956c32de --- /dev/null +++ b/src/printer/sygus_print_callback.cpp @@ -0,0 +1,144 @@ +/********************* */ +/*! \file sygus_print_callback.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus print callbacks + **/ + +#include "printer/sygus_print_callback.h" + +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace printer { + +SygusLetExpressionPrinter::SygusLetExpressionPrinter( + Node let_body, std::vector& let_args, unsigned ninput_args) +{ +} + +void SygusLetExpressionConstructorPrinter::doStrReplace( + std::string& str, const std::string& oldStr, const std::string& newStr) +{ + size_t pos = 0; + while ((pos = str.find(oldStr, pos)) != std::string::npos) + { + str.replace(pos, oldStr.length(), newStr); + pos += newStr.length(); + } +} + +void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p, + std::ostream& out, + Expr e) +{ + std::stringstream let_out; + // print as let term + if (d_sygus_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++) + { + Node v = d_sygus_let_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) + { + // it should be printed as a let argument + let_out << "("; + let_out << lv << " " << lv.getType() << " "; + p->toStreamSygus(let_out, e[i]); + let_out << ")"; + } + } + if (d_sygus_num_let_input_args > 0) + { + let_out << ") "; + } + // print the body + Node slet_body = d_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()); + p->toStreamSygus(let_out, slet_body); + if (d_sygus_num_let_input_args > 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 < d_sygus_let_args.size(); i++) + { + std::stringstream old_str; + old_str << new_lvs[i]; + std::stringstream new_str; + if (i >= d_sygus_num_let_input_args) + { + p->toStreamSygus(new_str, Node::fromExpr(e[i])); + } + else + { + new_str << d_sygus_let_args[i]; + } + doStrReplace(lbody, old_str.str().c_str(), new_str.str().c_str()); + } + out << lbody; +} + +SygusNamedConstructorPrinter::SygusNamedConstructorPrinter(std::string name) + : d_name(name) +{ +} + +void SygusNamedConstructorPrinter::toStreamSygus(Printer* p, + std::ostream& out, + Expr e) +{ + if (e.getNumChildren() > 0) + { + out << "("; + } + out << d_name; + if (e.getNumChildren() > 0) + { + for (Expr ec : e) + { + out << " "; + p->toStreamSygus(out, ec); + } + out << ")"; + } +} + +void SygusEmptyConstructorPrinter::toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) +{ + if (e.getNumChildren() == 1) + { + p->toStreamSygus(out, e[0]); + } + else + { + Assert(false); + } +} + +} /* CVC4::printer namespace */ +} /* CVC4 namespace */ diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h new file mode 100644 index 000000000..cdeec32f0 --- /dev/null +++ b/src/printer/sygus_print_callback.h @@ -0,0 +1,129 @@ +/********************* */ +/*! \file sygus_print_callback.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief sygus print callback functions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H +#define __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H + +#include + +#include "expr/node.h" + +namespace CVC4 { +namespace printer { + +/** sygus let expression constructor printer + * + * This class is used for printing sygus + * datatype constructor terms whose top symbol + * is a let expression. + * For example, for grammar: + * 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)) + * CVC4's support for let expressions in grammars + * is highly limited, since notice that the + * argument y : B is unused. + * + * For the above constructor, we have that + * d_let_body is (+ z 1), + * d_sygus_let_args is { y, z }, + * d_sygus_num_let_input_args is 1, since + * y is an original input argument of the + * let expression, but z is not. + */ +class SygusLetExpressionConstructorPrinter + : public SygusDatatypeConstructorPrinter +{ + public: + SygusLetExpressionPrinter(Node let_body, + std::vector& let_args, + unsigned ninput_args); + ~SygusLetExpressionPrinter() {} + /** 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; +}; + +/** sygus named constructor printer + * + * This callback is used for explicitly naming + * the builtin term that a sygus datatype constructor + * should be printed as. This is used for printing + * terms in sygus grammars that involve defined + * functions. For example, for grammar : + * A -> f( A ) | 0 + * where f is defined as: + * (define-fun ((x Int)) Int (+ x 1)) + * this class can be used as a callback for printing + * the first sygus datatype constructor f, where we use + * analog operator (lambda (x) (+ x 1)). + */ +class SygusNamedConstructorPrinter : public SygusDatatypeConstructorPrinter +{ + public: + SygusNamedConstructorPrinter(std::string name); + ~SygusNamedConstructorPrinter() {} + /** print sygus term e on output out using printer p */ + virtual void toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const override; + + private: + /** the defined function name */ + std::string d_name; +}; + +/** sygus empty printer + * + * This callback is used for printing constructors whose operators are + * implicit, such as identity functions. For example, for grammar : + * A -> B + * B -> x | 0 | 1 + * 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 +{ + public: + SygusEmptyConstructorPrinter(std::string name); + ~SygusEmptyConstructorPrinter() {} + /** print sygus term e on output out using printer p */ + virtual void toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const override; +}; + +} /* CVC4::printer namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H */