* Initial infrastructure for sygus printing.
* Minor
* Minor improvements
* Format
* Minor
* Empty constructor printer.
* Format
* Minor
* Format
* Address.
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");
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.
*/
* 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.
}
}/* 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) {
/** 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 */
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;
// 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:
// 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 "*";
}
}
+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<DatatypeType>(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() << ")";
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 */
--- /dev/null
+/********************* */
+/*! \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<Node>& 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<Node> subs_lvs;
+ std::vector<Node> 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 */
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+#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<Node>& 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<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;
+};
+
+/** 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 */
projects / cvc5.git / commitdiff