This removes sygus print callbacks, since they are no longer necessary to support the sygus v1 parser.
This involved generalizing the scope of the datatype utility sygusToBuiltin. Now, printing "as sygus" simply is accomplished by doing sygusToBuiltin conversion and then calling the printer on the builtin term.
This is required for further work towards eliminating the Expr layer.
FYI @4tXJ7f
printer/printer.h
printer/smt2/smt2_printer.cpp
printer/smt2/smt2_printer.h
- printer/sygus_print_callback.cpp
- printer/sygus_print_callback.h
printer/tptp/tptp_printer.cpp
printer/tptp/tptp_printer.h
proof/arith_proof.cpp
DESTINATION
${INCLUDE_INSTALL_DIR}/cvc4/parser)
install(FILES
- printer/sygus_print_callback.h
DESTINATION
${INCLUDE_INSTALL_DIR}/cvc4/printer)
install(FILES
#include "options/main_options.h"
#include "options/options.h"
#include "options/smt_options.h"
-#include "printer/sygus_print_callback.h"
#include "smt/model.h"
#include "smt/smt_engine.h"
#include "theory/logic_info.h"
Term op = purifySygusGTerm(term, args, cargs, ntsToUnres);
std::stringstream ssCName;
ssCName << op.getKind();
- std::shared_ptr<SygusPrintCallback> spc;
- // callback prints as the expression
- spc = std::make_shared<printer::SygusExprPrintCallback>(
- *op.d_expr, termVectorToExprs(args));
if (!args.empty())
{
Term lbvl = Term(d_solver,
{*lbvl.d_expr, *op.d_expr}));
}
dt.d_dtype->addSygusConstructor(
- *op.d_expr, ssCName.str(), sortVectorToTypes(cargs), spc);
+ *op.d_expr, ssCName.str(), sortVectorToTypes(cargs));
}
Term Grammar::purifySygusGTerm(
void Datatype::addSygusConstructor(Expr op,
const std::string& cname,
const std::vector<Type>& cargs,
- std::shared_ptr<SygusPrintCallback> spc,
int weight)
{
// avoid name clashes
std::string name = ss.str();
unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1);
DatatypeConstructor c(name, cweight);
- c.setSygus(op, spc);
+ c.setSygus(op);
for( unsigned j=0; j<cargs.size(); j++ ){
Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl;
std::stringstream sname;
void Datatype::addSygusConstructor(Kind k,
const std::string& cname,
const std::vector<Type>& cargs,
- std::shared_ptr<SygusPrintCallback> spc,
int weight)
{
ExprManagerScope ems(*d_em);
Expr op = d_em->operatorOf(k);
- addSygusConstructor(op, cname, cargs, spc, weight);
+ addSygusConstructor(op, cname, cargs, weight);
}
void Datatype::setTuple() {
d_internal = std::make_shared<DTypeConstructor>(name, weight);
}
-void DatatypeConstructor::setSygus(Expr op,
- std::shared_ptr<SygusPrintCallback> spc)
+void DatatypeConstructor::setSygus(Expr op)
{
PrettyCheckArgument(
!isResolved(), this, "cannot modify a finalized Datatype constructor");
Node opn = Node::fromExpr(op);
d_internal->setSygus(op);
- // print callback lives at the expression level currently
- d_sygus_pc = spc;
}
const std::vector<DatatypeConstructorArg>* DatatypeConstructor::getArgs()
return d_internal->getWeight();
}
-std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const
-{
- PrettyCheckArgument(
- isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_pc;
-}
-
Cardinality DatatypeConstructor::getCardinality(Type t) const
{
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() {}
- virtual ~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;
-};
-
class DTypeConstructor;
/**
* of the form (lambda (x) x).
*/
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.
- */
- std::shared_ptr<SygusPrintCallback> getSygusPrintCallback() const;
/** get weight
*
* Get the weight of this constructor. This value is used when computing the
* operator op. spc is the sygus callback of this datatype constructor,
* which is stored in a shared pointer.
*/
- void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc);
+ void setSygus(Expr op);
/**
* Get the list of arguments to this constructor.
Expr d_constructor;
/** the arguments of this constructor */
std::vector<DatatypeConstructorArg> d_args;
- /** sygus print callback */
- std::shared_ptr<SygusPrintCallback> d_sygus_pc;
};/* class DatatypeConstructor */
class DType;
* 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
void addSygusConstructor(Expr op,
const std::string& cname,
const std::vector<Type>& cargs,
- std::shared_ptr<SygusPrintCallback> spc = nullptr,
int weight = -1);
/**
* Same as above, with builtin kind k.
void addSygusConstructor(Kind k,
const std::string& cname,
const std::vector<Type>& cargs,
- std::shared_ptr<SygusPrintCallback> spc = nullptr,
int weight = -1);
/** set that this datatype is a tuple */
#include "expr/sygus_datatype.h"
-#include "printer/sygus_print_callback.h"
-
using namespace CVC4::kind;
namespace CVC4 {
void SygusDatatype::addConstructor(Node op,
const std::string& name,
const std::vector<TypeNode>& argTypes,
- std::shared_ptr<SygusPrintCallback> spc,
int weight)
{
d_cons.push_back(SygusDatatypeConstructor());
d_cons.back().d_op = op;
d_cons.back().d_name = name;
d_cons.back().d_argTypes = argTypes;
- d_cons.back().d_pc = spc;
d_cons.back().d_weight = weight;
}
std::vector<TypeNode> builtinArg;
builtinArg.push_back(tn);
addConstructor(
- av, cname, builtinArg, printer::SygusEmptyPrintCallback::getEmptyPC(), 0);
+ av, cname, builtinArg, 0);
}
void SygusDatatype::addConstructor(Kind k,
const std::vector<TypeNode>& argTypes,
- std::shared_ptr<SygusPrintCallback> spc,
int weight)
{
NodeManager* nm = NodeManager::currentNM();
- addConstructor(nm->operatorOf(k), kindToString(k), argTypes, spc, weight);
+ addConstructor(nm->operatorOf(k), kindToString(k), argTypes, weight);
}
size_t SygusDatatype::getNumConstructors() const { return d_cons.size(); }
d_dt.addSygusConstructor(d_cons[i].d_op.toExpr(),
d_cons[i].d_name,
cargs,
- d_cons[i].d_pc,
d_cons[i].d_weight);
}
Trace("sygus-type-cons") << "...built datatype " << d_dt << " ";
std::string d_name;
/** List of argument types. */
std::vector<TypeNode> d_argTypes;
- /** Print callback of the constructor. */
- std::shared_ptr<SygusPrintCallback> d_pc;
/** Weight of the constructor. */
int d_weight;
};
void addConstructor(Node op,
const std::string& name,
const std::vector<TypeNode>& argTypes,
- std::shared_ptr<SygusPrintCallback> spc = nullptr,
int weight = -1);
/**
* Add constructor that encodes an application of builtin kind k. Like above,
*/
void addConstructor(Kind k,
const std::vector<TypeNode>& argTypes,
- std::shared_ptr<SygusPrintCallback> spc = nullptr,
int weight = -1);
/**
* This adds a constructor that corresponds to the any constant constructor
return false;
}
+bool TypeNode::isSygusDatatype() const
+{
+ if (isDatatype())
+ {
+ return getDType().isSygus();
+ }
+ return false;
+}
+
std::string TypeNode::toString() const {
std::stringstream ss;
OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
/** Is this a fully instantiated datatype type */
bool isInstantiatedDatatype() const;
+ /** Is this a sygus datatype type */
+ bool isSygusDatatype() const;
+
/**
* Get instantiated datatype type. The type on which this method is called
* should be a parametric datatype whose parameter list is the same size as
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/smt2/smt2_input.h"
-#include "printer/sygus_print_callback.h"
#include "util/bitvector.h"
// ANTLR defines these, which is really bad!
Trace("parser-sygus2") << "Purified operator " << op
<< ", #args/cargs=" << args.size() << "/"
<< cargs.size() << std::endl;
- std::shared_ptr<SygusPrintCallback> spc;
- // callback prints as the expression
- spc = std::make_shared<printer::SygusExprPrintCallback>(
- op.getExpr(), api::termVectorToExprs(args));
if (!args.empty())
{
api::Term lbvl = d_solver->mkTerm(api::BOUND_VAR_LIST, args);
Trace("parser-sygus2") << "addSygusConstructor: operator " << op
<< std::endl;
dt.getDatatype().addSygusConstructor(
- op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs), spc);
+ op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs));
}
api::Term Smt2::purifySygusGTerm(api::Term term,
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
-#include "printer/sygus_print_callback.h"
#include "theory/quantifiers/candidate_rewrite_database.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
sdts[i].addConstructor(lambdaOp,
sscs.str(),
argListc,
- printer::SygusEmptyPrintCallback::getEmptyPC(),
0);
}
// recursive apply
sdttl.addConstructor(lambdaOp,
ssc.str(),
argList,
- printer::SygusEmptyPrintCallback::getEmptyPC(),
0);
Trace("srs-input-debug")
<< "Grammar for subterm " << n << " is: " << std::endl;
}
}
-void Printer::toStreamSygus(std::ostream& out, TNode n) const
-{
- // no sygus-specific printing associated with this printer,
- // just print the original term, without letification (the fifth argument is
- // set to 0).
- toStream(out, n, -1, false, 0);
-}
-
void Printer::toStream(std::ostream& out, const Model& m) const
{
for(size_t i = 0; i < m.getNumCommands(); ++i) {
/** Write an UnsatCore out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const UnsatCore& core) const;
- /**
- * 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;
-
protected:
/** Derived classes can construct, but no one else. */
Printer() {}
#include "smt_util/boolean_simplification.h"
#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/substitutions.h"
#include "theory/theory_model.h"
#include "util/smt2_quote_string.h"
}
}
-void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
-{
- 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().get();
- if (spc != nullptr && options::sygusPrintCallbacks())
- {
- spc->toStreamSygus(this, out, n.toExpr());
- }
- else
- {
- if (n.getNumChildren() > 0)
- {
- out << "(";
- }
- // print operator without letification (the fifth argument is set to 0).
- toStream(out, dt[cIndex].getSygusOp(), -1, false, 0);
- if (n.getNumChildren() > 0)
- {
- for (Node nc : n)
- {
- out << " ";
- toStreamSygus(out, nc);
- }
- out << ")";
- }
- }
- return;
- }
- }
- Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
- if (p.isNull())
- {
- p = n;
- }
- // cannot convert term to analog, print original, without letification.
- toStream(out, p, -1, false, 0);
-}
-
static void toStream(std::ostream& out, const AssertCommand* c)
{
out << "(assert " << c->getExpr() << ")";
// name
// sygus type
// constructors in order
- Printer* sygus_printer =
- Printer::getPrinter(language::output::LANG_SYGUS_V2);
do
{
Type curr = typesToPrint.front();
}
}
Node consToPrint = nm->mkNode(kind::APPLY_CONSTRUCTOR, cchildren);
- // now, print it
- sygus_printer->toStreamSygus(types_list, consToPrint);
+ // now, print it using the conversion to builtin with external
+ types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint, true);
types_list << ' ';
}
types_list << "))\n";
* with the core (UnsatCore::getSmtEngine) for printing named assertions.
*/
void toStream(std::ostream& out, const UnsatCore& core) const override;
- /**
- * Write the term that sygus datatype term node n
- * encodes to a stream with this Printer.
- */
- void toStreamSygus(std::ostream& out, TNode n) const override;
private:
void toStream(
+++ /dev/null
-/********************* */
-/*! \file sygus_print_callback.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Haniel Barbosa
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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"
-
-#include "expr/node.h"
-#include "printer/printer.h"
-
-using namespace CVC4::kind;
-using namespace std;
-
-namespace CVC4 {
-namespace printer {
-
-SygusExprPrintCallback::SygusExprPrintCallback(Expr body,
- const 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 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)
- {
- str.replace(pos, oldStr.length(), newStr);
- pos += newStr.length();
- }
-}
-
-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());
-
- // print to stream without letification
- std::stringstream body_out;
- p->toStream(body_out, sbody, -1, false, 0);
-
- // 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;
- }
-}
-
-SygusNamedPrintCallback::SygusNamedPrintCallback(std::string name)
- : d_name(name)
-{
-}
-
-void SygusNamedPrintCallback::toStreamSygus(const Printer* p,
- std::ostream& out,
- Expr e) const
-{
- if (e.getNumChildren() > 0)
- {
- out << "(";
- }
- out << d_name;
- if (e.getNumChildren() > 0)
- {
- for (Expr ec : e)
- {
- out << " ";
- p->toStreamSygus(out, ec);
- }
- out << ")";
- }
-}
-
-void SygusEmptyPrintCallback::toStreamSygus(const Printer* p,
- std::ostream& out,
- Expr e) const
-{
- if (e.getNumChildren() == 1)
- {
- p->toStreamSygus(out, e[0]);
- }
- else
- {
- Assert(false);
- }
-}
-
-std::shared_ptr<SygusEmptyPrintCallback> SygusEmptyPrintCallback::d_empty_pc = nullptr;
-
-} /* CVC4::printer namespace */
-} /* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file sygus_print_callback.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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_public.h"
-
-#ifndef CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
-#define CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
-
-#include <vector>
-
-#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, const 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 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 CVC4_PUBLIC SygusNamedPrintCallback : public SygusPrintCallback
-{
- public:
- SygusNamedPrintCallback(std::string name);
- ~SygusNamedPrintCallback() {}
- /** 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 CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback
-{
- public:
- SygusEmptyPrintCallback() {}
- ~SygusEmptyPrintCallback() {}
- /** print sygus term e on output out using printer p */
- virtual void toStreamSygus(const Printer* p,
- std::ostream& out,
- Expr e) const override;
- /* Retrieves empty callback pointer */
- static inline std::shared_ptr<SygusEmptyPrintCallback> getEmptyPC()
- {
- if (!d_empty_pc)
- {
- d_empty_pc = std::make_shared<SygusEmptyPrintCallback>();
- }
- return d_empty_pc;
- }
-
- private:
- /* empty callback object */
- static std::shared_ptr<SygusEmptyPrintCallback> d_empty_pc;
-};
-
-} /* CVC4::printer namespace */
-} /* CVC4 namespace */
-
-#endif /* CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H */
#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "expr/sygus_datatype.h"
-#include "printer/sygus_print_callback.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/evaluator.h"
typedef expr::Attribute<SygusToBuiltinTermAttributeId, Node>
SygusToBuiltinTermAttribute;
+// A variant of the above attribute for cases where we introduce a fresh
+// variable. This is to support sygusToBuiltin on non-constant sygus terms,
+// where sygus variables should be mapped to canonical builtin variables.
+// It is important to cache this so that sygusToBuiltin is deterministic.
+struct SygusToBuiltinVarAttributeId
+{
+};
+typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node>
+ SygusToBuiltinVarAttribute;
+
Node sygusToBuiltin(Node n, bool isExternal)
{
- Assert(n.isConst());
std::unordered_map<TNode, Node, TNodeHashFunction> visited;
std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
std::vector<TNode> visit;
it = visited.find(cur);
if (it == visited.end())
{
+ // Notice this condition succeeds in roughly 99% of the executions of this
+ // method (based on our coverage tests), hence the else if / else cases
+ // below do not significantly impact performance.
if (cur.getKind() == APPLY_CONSTRUCTOR)
{
if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute()))
}
}
}
+ else if (cur.getType().isSygusDatatype())
+ {
+ Assert (cur.isVar());
+ if (cur.hasAttribute(SygusToBuiltinVarAttribute()))
+ {
+ // use the previously constructed variable for it
+ visited[cur] = cur.getAttribute(SygusToBuiltinVarAttribute());
+ }
+ else
+ {
+ std::stringstream ss;
+ ss << cur;
+ const DType& dt = cur.getType().getDType();
+ // make a fresh variable
+ NodeManager * nm = NodeManager::currentNM();
+ Node var = nm->mkBoundVar(ss.str(), dt.getSygusType());
+ SygusToBuiltinVarAttribute stbv;
+ cur.setAttribute(stbv, var);
+ visited[cur] = var;
+ }
+ }
else
{
// non-datatypes are themselves
<< " Arg #" << k << ": " << argtNew << std::endl;
cargs.push_back(argtNew);
}
- // callback prints as the expression
- std::shared_ptr<SygusPrintCallback> spc;
- std::vector<Expr> args;
- if (op.getKind() == LAMBDA)
- {
- Node opBody = op[1];
- for (const Node& v : op[0])
- {
- args.push_back(v.toExpr());
- }
- spc = std::make_shared<printer::SygusExprPrintCallback>(
- opBody.toExpr(), args);
- }
- else if (cargs.empty())
- {
- spc = std::make_shared<printer::SygusExprPrintCallback>(op.toExpr(),
- args);
- }
std::stringstream ss;
ss << ops.getKind();
Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl;
- sdts.back().addConstructor(ops, ss.str(), cargs, spc);
+ sdts.back().addConstructor(ops, ss.str(), cargs);
}
Trace("dtsygus-gen-debug")
<< "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl;
const std::vector<Node>& args);
/** Sygus to builtin
*
- * This method converts a constant term of SyGuS datatype type to its builtin
+ * This method converts a term n of SyGuS datatype type to its builtin
* equivalent. For example, given input C_*( C_x(), C_y() ), this method returns
* x*y, assuming C_+, C_x, and C_y have sygus operators *, x, and y
* respectively.
* that was provided. This includes the use of defined functions. This argument
* should typically be false, unless we are e.g. exporting the value of the
* term as a final solution.
+ *
+ * If n is not constant, then its non-constant subterms that have sygus
+ * datatype types are replaced by fresh variables (of the same name, if that
+ * subterm is a variable, and having arbitrary name otherwise).
*/
-Node sygusToBuiltin(Node c, bool isExternal = false);
+Node sygusToBuiltin(Node n, bool isExternal = false);
/** Sygus to builtin eval
*
* This method returns the rewritten form of (DT_SYGUS_EVAL n args). Notice that
{
Trace("dt-sygus") << "* DT model : " << prog << " -> ";
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(ss, progv);
+ quantifiers::TermDbSygus::toStreamSygus(ss, progv);
Trace("dt-sygus") << ss.str() << std::endl;
}
// first check that the value progv for prog is what we expected
out << "(" << (verified ? "" : "candidate-") << "rewrite ";
if (d_using_sygus)
{
- Printer* p = Printer::getPrinter(options::outputLanguage());
- p->toStreamSygus(out, sol);
+ TermDbSygus::toStreamSygus(out, sol);
out << " ";
- p->toStreamSygus(out, eq_sol);
+ TermDbSygus::toStreamSygus(out, eq_sol);
}
else
{
}
if (Trace.isOn("sygus-rr-filter"))
{
- Printer* p = Printer::getPrinter(options::outputLanguage());
std::stringstream ss;
ss << "(redundant-rewrite ";
- p->toStreamSygus(ss, n);
+ TermDbSygus::toStreamSygus(ss, n);
ss << " ";
- p->toStreamSygus(ss, eq_n);
+ TermDbSygus::toStreamSygus(ss, eq_n);
ss << ")";
Trace("sygus-rr-filter") << ss.str() << std::endl;
}
{
Trace("sygus-ccore")
<< "CegisCoreConnective: Construct candidate solutions..." << std::endl;
- Printer* p = Printer::getPrinter(options::outputLanguage());
for (unsigned i = 0, size = candidates.size(); i < size; i++)
{
std::stringstream ss;
- p->toStreamSygus(ss, candidate_values[i]);
+ TermDbSygus::toStreamSygus(ss, candidate_values[i]);
Trace("sygus-ccore") << " " << candidates[i] << " -> " << ss.str()
<< std::endl;
}
for (const Node& var : p.second)
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var);
+ TermDbSygus::toStreamSygus(ss, var);
Trace("synth-stream-concrete") << " " << ss.str();
}
Trace("synth-stream-concrete") << " ]";
if (Trace.isOn("synth-stream-concrete"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value);
+ TermDbSygus::toStreamSygus(ss, d_value);
Trace("synth-stream-concrete")
<< " ....streaming next permutation for value : " << ss.str()
<< " with " << d_perm_state_class.size() << " permutation classes\n";
if (Trace.isOn("synth-stream-concrete"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(ss, perm_value);
+ TermDbSygus::toStreamSygus(ss, perm_value);
Trace("synth-stream-concrete")
<< " ....return new perm " << ss.str() << "\n";
}
if (Trace.isOn("synth-stream-concrete"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(ss, d_vars[d_last_perm[i]]);
+ TermDbSygus::toStreamSygus(ss, d_vars[d_last_perm[i]]);
Trace("synth-stream-concrete") << " " << ss.str();
}
vars.push_back(d_vars[d_last_perm[i]]);
if (Trace.isOn("synth-stream-concrete"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, value);
+ TermDbSygus::toStreamSygus(ss, value);
Trace("synth-stream-concrete")
<< " * Streaming concrete: registering value " << ss.str() << "\n";
}
for (const Node& var : p.second)
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var);
+ TermDbSygus::toStreamSygus(ss, var);
Trace("synth-stream-concrete") << " " << ss.str();
}
Trace("synth-stream-concrete") << " ]";
if (Trace.isOn("synth-stream-concrete"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value);
+ TermDbSygus::toStreamSygus(ss, d_value);
Trace("synth-stream-concrete")
<< " ..streaming next combination of " << ss.str() << "\n";
}
if (Trace.isOn("synth-stream-concrete-debug"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_last);
+ TermDbSygus::toStreamSygus(ss, d_last);
Trace("synth-stream-concrete-debug")
<< " ..using base perm " << ss.str() << "\n";
}
if (Trace.isOn("synth-stream-concrete"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(ss, comb_value);
+ TermDbSygus::toStreamSygus(ss, comb_value);
Trace("synth-stream-concrete")
<< " ....register new comb value " << ss.str()
<< " with rewritten form " << builtin_comb_value
if (!builtin_comb_value.isConst()
&& !d_comb_values.insert(builtin_comb_value).second)
{
- std::stringstream ss, ss1;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(ss, comb_value);
- Trace("synth-stream-concrete")
- << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value
- << "\n ..excluding all other concretizations (had "
- << d_comb_values.size() << " already)\n\n";
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ std::stringstream ss, ss1;
+ TermDbSygus::toStreamSygus(ss, comb_value);
+ Trace("synth-stream-concrete")
+ << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value
+ << "\n ..excluding all other concretizations (had "
+ << d_comb_values.size() << " already)\n\n";
+ }
return Node::null();
}
if (Trace.isOn("synth-stream-concrete"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(ss, comb_value);
+ TermDbSygus::toStreamSygus(ss, comb_value);
Trace("synth-stream-concrete")
<< " ..return new comb " << ss.str() << "\n\n";
}
if (Trace.isOn("synth-stream-concrete"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(ss, d_vars[d_last_comb[i]]);
+ TermDbSygus::toStreamSygus(ss, d_vars[d_last_comb[i]]);
Trace("synth-stream-concrete") << " " << ss.str();
}
vars.push_back(d_vars[d_last_comb[i]]);
#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "expr/sygus_datatype.h"
-#include "printer/sygus_print_callback.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
-#include "printer/sygus_print_callback.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
}
Node CegGrammarConstructor::createLambdaWithZeroArg(
- Kind k, TypeNode bArgType, std::shared_ptr<SygusPrintCallback> spc)
+ Kind k, TypeNode bArgType)
{
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> opLArgs;
zarg = bv::utils::mkZero(size);
}
Node body = nm->mkNode(k, zarg, opLArgs.back());
- // use a print callback since we do not want to print the lambda
- spc = std::make_shared<printer::SygusExprPrintCallback>(body.toExpr(),
- opLArgsExpr);
// create operator
Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), body);
Trace("sygus-grammar-def") << "\t...building lambda op " << op << "\n";
{
Node op =
nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), monomial);
- // use a print callback since we do not want to print the lambda
- std::shared_ptr<SygusPrintCallback> spc;
- std::vector<Expr> opLArgsExpr;
- for (unsigned j = 0, nvars = opLArgs.size(); j < nvars; j++)
- {
- opLArgsExpr.push_back(opLArgs[j].toExpr());
- }
- spc = std::make_shared<printer::SygusExprPrintCallback>(
- monomial.toExpr(), opLArgsExpr);
// add it as a constructor
std::stringstream ssop;
ssop << "monomial_" << sdc.d_name;
// a generalization of a non-Boolean variable (which has weight 0).
// This ensures that e.g. ( c1*x >= 0 ) has the same weight as
// ( x >= 0 ).
- sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, spc, 0);
+ sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, 0);
}
}
if (polynomialGrammar)
Assert(sumChildren.size() > 1);
Node ops = nm->mkNode(PLUS, sumChildren);
Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops);
- std::shared_ptr<SygusPrintCallback> spc;
- std::vector<Expr> lambdaVarsExpr;
- for (unsigned j = 0, nvars = lambdaVars.size(); j < nvars; j++)
- {
- lambdaVarsExpr.push_back(lambdaVars[j].toExpr());
- }
- spc = std::make_shared<printer::SygusExprPrintCallback>(ops.toExpr(),
- lambdaVarsExpr);
Trace("sygus-grammar-def") << "any term operator is " << op << std::endl;
// make the any term datatype, add to back
// do not consider the exclusion criteria of the generator
// a simultaneous generalization of set of non-Boolean variables.
// This ensures that ( c1*x + c2*y >= 0 ) has the same weight as
// e.g. ( x >= 0 ) or ( y >= 0 ).
- sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, spc, 0);
+ sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, 0);
// mark that predicates should be of the form (= pol 0) and (<= pol 0)
itgat->second.second = true;
}
Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
std::vector<TypeNode> cargsEmpty;
// make boolean variables weight as non-nullary constructors
- sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, nullptr, 1);
+ sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, 1);
}
}
// add constants
// predicates
if (zarg)
{
- std::shared_ptr<SygusPrintCallback> spc;
- Node op = createLambdaWithZeroArg(k, types[i], spc);
+ Node op = createLambdaWithZeroArg(k, types[i]);
ss << "eq_" << types[i];
sdtBool.addConstructor(op, ss.str(), cargs);
}
cargs.pop_back();
}
// type specific predicates
- std::shared_ptr<SygusPrintCallback> spc;
std::stringstream ssop;
if (types[i].isReal())
{
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
if (zarg)
{
- Node op = createLambdaWithZeroArg(kind, types[i], spc);
+ Node op = createLambdaWithZeroArg(kind, types[i]);
ssop << "leq_" << types[i];
sdtBool.addConstructor(op, ssop.str(), cargs);
}
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
if (zarg)
{
- Node op = createLambdaWithZeroArg(kind, types[i], spc);
+ Node op = createLambdaWithZeroArg(kind, types[i]);
ssop << "leq_" << types[i];
sdtBool.addConstructor(op, ssop.str(), cargs);
}
Node op,
const std::string& name,
const std::vector<TypeNode>& consTypes,
- std::shared_ptr<SygusPrintCallback> spc,
int weight)
{
if (shouldInclude(op))
{
- d_sdt.addConstructor(op, name, consTypes, spc, weight);
+ d_sdt.addConstructor(op, name, consTypes, weight);
}
}
void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor(
Kind k,
const std::vector<TypeNode>& consTypes,
- std::shared_ptr<SygusPrintCallback> spc,
int weight)
{
NodeManager* nm = NodeManager::currentNM();
- addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight);
+ addConstructor(nm->operatorOf(k), kindToString(k), consTypes, weight);
}
bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const
{
void addConstructor(Node op,
const std::string& name,
const std::vector<TypeNode>& consTypes,
- std::shared_ptr<SygusPrintCallback> spc = nullptr,
int weight = -1);
/**
* Possibly add a constructor to d_sdt, based on the criteria mentioned
*/
void addConstructor(Kind k,
const std::vector<TypeNode>& consTypes,
- std::shared_ptr<SygusPrintCallback> spc = nullptr,
int weight = -1);
/** Should we include constructor with operator op? */
bool shouldInclude(Node op) const;
* and an extra zero argument of that same type. For example, for k = LEQ and
* bArgType = Int, the operator will be lambda x : Int. x + 0. Currently the
* supported input types are Real (thus also Int) and BitVector.
- *
- * This method also creates a print callback for the operator, saved via the
- * argument spc, if the caller wishes to not print the lambda.
*/
static Node createLambdaWithZeroArg(Kind k,
- TypeNode bArgType,
- std::shared_ptr<SygusPrintCallback> spc);
+ TypeNode bArgType);
//---------------- end grammar construction
};
#include "expr/datatype.h"
#include "expr/node_manager_attributes.h" // for VarNameAttr
#include "options/quantifiers_options.h"
-#include "printer/sygus_print_callback.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/datatypes/theory_datatypes_utils.h"
void SygusGrammarNorm::TypeObject::addConsInfo(
SygusGrammarNorm* sygus_norm,
- const DTypeConstructor& cons,
- std::shared_ptr<SygusPrintCallback> spc)
+ const DTypeConstructor& cons)
{
Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n";
/* Recover the sygus operator to not lose reference to the original
}
d_sdt.addConstructor(
- sygus_op, cons.getName(), consTypes, spc, cons.getWeight());
+ sygus_op, cons.getName(), consTypes, cons.getWeight());
}
void SygusGrammarNorm::TypeObject::initializeDatatype(
to.d_sdt.addConstructor(iden_op,
"id",
ctypes,
- printer::SygusEmptyPrintCallback::getEmptyPC(),
0);
Trace("sygus-grammar-normalize-chain")
<< "\tAdding " << t << " to " << to.d_unres_tn << "\n";
to.d_sdt.addConstructor(iden_op,
"id_next",
ctypes,
- printer::SygusEmptyPrintCallback::getEmptyPC(),
0);
}
{
unsigned oi = op_pos[i];
Assert(oi < dt.getNumConstructors());
- to.addConsInfo(this, dt[oi], dtt[oi].getSygusPrintCallback());
+ to.addConsInfo(this, dt[oi]);
}
/* Build normalize datatype */
if (Trace.isOn("sygus-grammar-normalize"))
* The types of the arguments of "cons" are recursively normalized
*/
void addConsInfo(SygusGrammarNorm* sygus_norm,
- const DTypeConstructor& cons,
- std::shared_ptr<SygusPrintCallback> spc);
+ const DTypeConstructor& cons);
/** initializes a datatype with the information in the type object
*
#include "expr/node_algorithm.h"
#include "expr/sygus_datatype.h"
#include "options/smt_options.h"
-#include "printer/sygus_print_callback.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
if (Trace.isOn("sygus-repair-const"))
{
Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl;
- Printer* p = Printer::getPrinter(options::outputLanguage());
for (unsigned i = 0, size = candidates.size(); i < size; i++)
{
std::stringstream ss;
- p->toStreamSygus(ss, candidate_values[i]);
+ TermDbSygus::toStreamSygus(ss, candidate_values[i]);
Trace("sygus-repair-const")
<< " " << candidates[i] << " -> " << ss.str() << std::endl;
}
cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
if (Trace.isOn("sygus-repair-const"))
{
- Printer* p = Printer::getPrinter(options::outputLanguage());
std::stringstream ss;
- p->toStreamSygus(ss, cv);
+ TermDbSygus::toStreamSygus(ss, cv);
Trace("sygus-repair-const")
<< "Solution #" << i << " : " << ss.str() << std::endl;
if (skeleton == cv)
else
{
std::stringstream sss;
- p->toStreamSygus(sss, skeleton);
+ TermDbSygus::toStreamSygus(sss, skeleton);
Trace("sygus-repair-const")
<< "...inferred skeleton : " << sss.str() << std::endl;
}
if (Trace.isOn("sygus-repair-const") || Trace.isOn("sygus-engine"))
{
std::stringstream sss;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(sss, repair_cv[i]);
+ TermDbSygus::toStreamSygus(sss, repair_cv[i]);
ss << " * " << candidates[i] << " -> " << sss.str() << std::endl;
}
}
if (Trace.isOn("sygus-unif-sol"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(ss, hd_mv[e]);
+ TermDbSygus::toStreamSygus(ss, hd_mv[e]);
Trace("sygus-unif-sol")
<< " add evaluation head (" << hd_counter << "/" << d_hds.size()
<< "): " << e << " -> " << ss.str() << std::endl;
if (Trace.isOn("sygus-unif-sol"))
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, cv);
+ TermDbSygus::toStreamSygus(ss, cv);
Trace("sygus-unif-sol")
<< " add condition (" << c_counter << "/" << d_conds.size()
<< "): " << ce << " -> " << ss.str() << std::endl;
for (const Node& fc : fail_cvs)
{
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc);
+ TermDbSygus::toStreamSygus(ss, fc);
Trace("sygus-engine") << ss.str() << " ";
}
Trace("sygus-engine") << std::endl;
Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv;
TypeNode tn = onv.getType();
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
+ TermDbSygus::toStreamSygus(ss, onv);
if (printDebug)
{
sygusEnumOut << " " << ss.str();
{
Node v = candidate_values[i];
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, v);
+ TermDbSygus::toStreamSygus(ss, v);
out << "(" << d_quant[0][i] << " " << ss.str() << ")";
}
out << ")" << std::endl;
}
else
{
- Printer::getPrinter(options::outputLanguage())
- ->toStreamSygus(out, sol);
+ Node bsol = datatypes::utils::sygusToBuiltin(sol, true);
+ out << bsol;
}
out << ")" << std::endl;
}
{
if (Trace.isOn(c))
{
- if (n.isNull())
- {
- Trace(c) << n;
- }
- else
- {
- std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n);
- Trace(c) << ss.str();
- }
+ std::stringstream ss;
+ toStreamSygus(ss, n);
+ Trace(c) << ss.str();
}
}
+void TermDbSygus::toStreamSygus(std::ostream& out, Node n)
+{
+ // use external conversion
+ out << datatypes::utils::sygusToBuiltin(n, true);
+}
+
SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
{
AlwaysAssert(d_tinfo.find(tn) != d_tinfo.end());
/** print to sygus stream n on trace c */
static void toStreamSygus(const char* c, Node n);
-
+ /** print to sygus stream n on output out */
+ static void toStreamSygus(std::ostream& out, Node n);
+
private:
/** reference to the quantifiers engine */
QuantifiersEngine* d_quantEngine;
projects / cvc5.git / commitdiff