datatype.cpp
record.cpp
record.h
+ sygus_datatype.cpp
+ sygus_datatype.h
uninterpreted_constant.cpp
uninterpreted_constant.h
)
--- /dev/null
+/********************* */
+/*! \file sygus_datatype.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 class for constructing SyGuS datatypes.
+ **/
+
+#include "expr/sygus_datatype.h"
+
+#include "printer/sygus_print_callback.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+SygusDatatype::SygusDatatype(const std::string& name) : d_dt(Datatype(name)) {}
+
+std::string SygusDatatype::getName() const { return d_dt.getName(); }
+
+void SygusDatatype::addConstructor(Node op,
+ const std::string& name,
+ std::shared_ptr<SygusPrintCallback> spc,
+ int weight,
+ const std::vector<TypeNode>& consTypes)
+{
+ d_ops.push_back(op);
+ d_cons_names.push_back(std::string(name));
+ d_pc.push_back(spc);
+ d_weight.push_back(weight);
+ d_consArgs.push_back(consTypes);
+}
+
+void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
+{
+ // add an "any constant" proxy variable
+ Node av = NodeManager::currentNM()->mkSkolem("_any_constant", tn);
+ // mark that it represents any constant
+ SygusAnyConstAttribute saca;
+ av.setAttribute(saca, true);
+ std::stringstream ss;
+ ss << getName() << "_any_constant";
+ std::string cname(ss.str());
+ std::vector<TypeNode> builtinArg;
+ builtinArg.push_back(tn);
+ addConstructor(
+ av, cname, printer::SygusEmptyPrintCallback::getEmptyPC(), 0, builtinArg);
+}
+
+void SygusDatatype::initializeDatatype(TypeNode sygusType,
+ Node sygusVars,
+ bool allowConst,
+ bool allowAll)
+{
+ /* Use the sygus type to not lose reference to the original types (Bool,
+ * Int, etc) */
+ d_dt.setSygus(sygusType.toType(), sygusVars.toExpr(), allowConst, allowAll);
+ for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
+ {
+ // must convert to type now
+ std::vector<Type> cargs;
+ for (TypeNode& ct : d_consArgs[i])
+ {
+ cargs.push_back(ct.toType());
+ }
+ // add (sygus) constructor
+ d_dt.addSygusConstructor(
+ d_ops[i].toExpr(), d_cons_names[i], cargs, d_pc[i], d_weight[i]);
+ }
+ Trace("sygus-type-cons") << "...built datatype " << d_dt << " ";
+}
+
+const Datatype& SygusDatatype::getDatatype() const { return d_dt; }
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file sygus_datatype.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 A class for constructing SyGuS datatypes.
+ **/
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__SYGUS_DATATYPE_H
+#define CVC4__EXPR__SYGUS_DATATYPE_H
+
+#include <string>
+#include <vector>
+
+#include "expr/attribute.h"
+#include "expr/datatype.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+/** Attribute true for variables that represent any constant */
+struct SygusAnyConstAttributeId
+{
+};
+typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
+
+/**
+ * Keeps the necessary information for initializing a sygus datatype, which
+ * includes the operators, names, print callbacks and list of argument types
+ * for each constructor.
+ *
+ * It also maintains a datatype to represent the structure of the type node.
+ *
+ * Notice that this class is only responsible for setting SyGuS-related
+ * information regarding the datatype. It is still required that the user
+ * of this class construct the datatype type corresponding to the datatype
+ * e.g. via a call to ExprManager::mkMutualDatatypeTypes().
+ */
+class SygusDatatype
+{
+ public:
+ /** constructor */
+ SygusDatatype(const std::string& name);
+ ~SygusDatatype() {}
+ /** get the name of this datatype */
+ std::string getName() const;
+ /**
+ * Add constructor that encodes an application of builtin operator op.
+ *
+ * op: the builtin operator,
+ * name: the name of the constructor,
+ * spc: the print callback (for custom printing of this node),
+ * weight: the weight of this constructor,
+ * consTypes: the argument types of the constructor (typically other sygus
+ * datatype types).
+ */
+ void addConstructor(Node op,
+ const std::string& name,
+ std::shared_ptr<SygusPrintCallback> spc,
+ int weight,
+ const std::vector<TypeNode>& consTypes);
+ /**
+ * This adds a constructor that corresponds to the any constant constructor
+ * for the given (builtin) type tn.
+ */
+ void addAnyConstantConstructor(TypeNode tn);
+
+ /** builds a datatype with the information in the type object
+ *
+ * sygusType: the builtin type that this datatype encodes,
+ * sygusVars: the formal argument list of the function-to-synthesize,
+ * allowConst: whether the grammar corresponding to this datatype allows
+ * any constant,
+ * allowAll: whether the grammar corresponding to this datatype allows
+ * any term.
+ */
+ void initializeDatatype(TypeNode sygusType,
+ Node sygusVars,
+ bool allowConst,
+ bool allowAll);
+ /** Get the sygus datatype initialized by this class */
+ const Datatype& getDatatype() const;
+
+ private:
+ //---------- information to build normalized type node
+ /** Operators for each constructor. */
+ std::vector<Node> d_ops;
+ /** Names for each constructor. */
+ std::vector<std::string> d_cons_names;
+ /** Print callbacks for each constructor */
+ std::vector<std::shared_ptr<SygusPrintCallback>> d_pc;
+ /** Weights for each constructor */
+ std::vector<int> d_weight;
+ /** List of argument types for each constructor */
+ std::vector<std::vector<TypeNode>> d_consArgs;
+ /** Datatype to represent type's structure */
+ Datatype d_dt;
+};
+
+} // namespace CVC4
+
+#endif
#include "theory/datatypes/datatypes_rewriter.h"
#include "expr/node_algorithm.h"
+#include "expr/sygus_datatype.h"
#include "options/datatypes_options.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/datatypes/sygus_extension.h"
#include "expr/node_manager.h"
+#include "expr/sygus_datatype.h"
#include "options/base_options.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "expr/node_algorithm.h"
+#include "expr/sygus_datatype.h"
using namespace CVC4;
using namespace CVC4::kind;
};
typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
-/** Attribute true for variables that represent any constant */
-struct SygusAnyConstAttributeId
-{
-};
-typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
-
/**
* Attribute true for enumerators whose current model values were registered by
* the datatypes sygus solver, and were not excluded by sygus symmetry breaking.
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#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"
{
}
+SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn)
+ : d_tn(src_tn),
+ d_unres_tn(unres_tn),
+ d_sdt(unres_tn.getAttribute(expr::VarNameAttr()))
+{
+}
Kind SygusGrammarNorm::TypeObject::getEliminateKind(Kind ok)
{
Kind nk = ok;
exp_sop_n = Rewriter::rewrite(exp_sop_n);
}
- d_ops.push_back(exp_sop_n);
- Trace("sygus-grammar-normalize-defs")
- << "\tOriginal op: " << cons.getSygusOp()
- << "\n\tExpanded one: " << exp_sop_n
- << "\n\tRewritten one: " << d_ops.back() << "\n\n";
- d_cons_names.push_back(cons.getName());
- d_pc.push_back(cons.getSygusPrintCallback());
- d_weight.push_back(cons.getWeight());
- d_cons_args_t.push_back(std::vector<Type>());
+ std::vector<TypeNode> consTypes;
for (const DatatypeConstructorArg& arg : cons)
{
- /* Collect unresolved type nodes corresponding to the typenode of the
- * arguments */
- d_cons_args_t.back().push_back(
- sygus_norm
- ->normalizeSygusRec(TypeNode::fromType(
- static_cast<SelectorType>(arg.getType()).getRangeType()))
- .toType());
+ // Collect unresolved type nodes corresponding to the typenode of the
+ // arguments.
+ TypeNode atype = TypeNode::fromType(arg.getRangeType());
+ // normalize it recursively
+ atype = sygus_norm->normalizeSygusRec(atype);
+ consTypes.push_back(atype);
}
+
+ Trace("sygus-type-cons-defs") << "\tOriginal op: " << cons.getSygusOp()
+ << "\n\tExpanded one: " << exp_sop_n << "\n\n";
+ d_sdt.addConstructor(exp_sop_n,
+ cons.getName(),
+ cons.getSygusPrintCallback(),
+ cons.getWeight(),
+ consTypes);
}
-void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
- const Datatype& dt)
+void SygusGrammarNorm::TypeObject::initializeDatatype(
+ SygusGrammarNorm* sygus_norm, const Datatype& dt)
{
/* Use the sygus type to not lose reference to the original types (Bool,
* Int, etc) */
- d_dt.setSygus(dt.getSygusType(),
- sygus_norm->d_sygus_vars.toExpr(),
- dt.getSygusAllowConst(),
- dt.getSygusAllowAll());
- for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
- {
- d_dt.addSygusConstructor(d_ops[i].toExpr(),
- d_cons_names[i],
- d_cons_args_t[i],
- d_pc[i],
- d_weight[i]);
- }
- Trace("sygus-grammar-normalize") << "...built datatype " << d_dt << " ";
+ TypeNode sygusType = TypeNode::fromType(dt.getSygusType());
+ d_sdt.initializeDatatype(sygusType,
+ sygus_norm->d_sygus_vars.toExpr(),
+ dt.getSygusAllowConst(),
+ dt.getSygusAllowAll());
+ Trace("sygus-grammar-normalize")
+ << "...built datatype " << d_sdt.getDatatype() << " ";
/* Add to global accumulators */
- sygus_norm->d_dt_all.push_back(d_dt);
+ sygus_norm->d_dt_all.push_back(d_sdt.getDatatype());
sygus_norm->d_unres_t_all.insert(d_unres_tn.toType());
Trace("sygus-grammar-normalize") << "---------------------------------\n";
}
/* creates type for element */
std::vector<unsigned> tmp;
tmp.push_back(d_elem_pos.back());
- Type t = sygus_norm->normalizeSygusRec(to.d_tn, dt, tmp).toType();
+ TypeNode t = sygus_norm->normalizeSygusRec(to.d_tn, dt, tmp);
/* consumes element */
d_elem_pos.pop_back();
/* adds to Root: "type" */
- to.d_ops.push_back(iden_op);
- to.d_cons_names.push_back("id");
- to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
- /* Identity operators should not increase the size of terms */
- to.d_weight.push_back(0);
- to.d_cons_args_t.push_back(std::vector<Type>());
- to.d_cons_args_t.back().push_back(t);
+ std::vector<TypeNode> ctypes;
+ ctypes.push_back(t);
+ to.d_sdt.addConstructor(iden_op,
+ "id",
+ printer::SygusEmptyPrintCallback::getEmptyPC(),
+ 0,
+ ctypes);
Trace("sygus-grammar-normalize-chain")
<< "\tAdding " << t << " to " << to.d_unres_tn << "\n";
/* adds to Root: "type + Root" */
- to.d_ops.push_back(nm->operatorOf(PLUS));
- to.d_cons_names.push_back(kindToString(PLUS));
- to.d_pc.push_back(nullptr);
- to.d_weight.push_back(-1);
- to.d_cons_args_t.push_back(std::vector<Type>());
- to.d_cons_args_t.back().push_back(t);
- to.d_cons_args_t.back().push_back(to.d_unres_tn.toType());
+ std::vector<TypeNode> ctypesp;
+ ctypesp.push_back(t);
+ ctypesp.push_back(to.d_unres_tn);
+ to.d_sdt.addConstructor(
+ nm->operatorOf(PLUS), kindToString(PLUS), nullptr, -1, ctypesp);
Trace("sygus-grammar-normalize-chain")
<< "\tAdding PLUS to " << to.d_unres_tn << " with arg types "
<< to.d_unres_tn << " and " << t << "\n";
Trace("sygus-grammar-normalize-chain") << "\n";
}
/* adds to Root: (\lambda x. x ) Next */
- to.d_ops.push_back(iden_op);
- to.d_cons_names.push_back("id_next");
- to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
- to.d_weight.push_back(0);
- to.d_cons_args_t.push_back(std::vector<Type>());
- to.d_cons_args_t.back().push_back(
- sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos).toType());
+ std::vector<TypeNode> ctypes;
+ ctypes.push_back(sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos));
+ to.d_sdt.addConstructor(iden_op,
+ "id_next",
+ printer::SygusEmptyPrintCallback::getEmptyPC(),
+ 0,
+ ctypes);
}
std::map<TypeNode, Node> SygusGrammarNorm::d_tn_to_id = {};
/* Creates type object for normalization */
TypeObject to(tn, unres_tn);
- /* Determine normalization transformation based on sygus type and given
- * operators */
- std::unique_ptr<Transf> transformation = inferTransf(tn, dt, op_pos);
- /* If a transformation was selected, apply it */
- if (transformation != nullptr)
- {
- transformation->buildType(this, to, dt, op_pos);
- }
-
- /* Remaining operators are rebuilt as they are */
- for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
- {
- Assert(op_pos[i] < dt.getNumConstructors());
- to.addConsInfo(this, dt[op_pos[i]]);
- }
if (dt.getSygusAllowConst())
{
TypeNode sygus_type = TypeNode::fromType(dt.getSygusType());
&& !sygus_type.isBoolean())
{
Trace("sygus-grammar-normalize") << "...add any constant constructor.\n";
- // add an "any constant" proxy variable
- Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type);
- // mark that it represents any constant
- SygusAnyConstAttribute saca;
- av.setAttribute(saca, true);
- std::stringstream ss;
- ss << to.d_unres_tn << "_any_constant";
- std::string cname(ss.str());
- std::vector<Type> builtin_arg;
- builtin_arg.push_back(dt.getSygusType());
+ TypeNode dtn = TypeNode::fromType(dt.getSygusType());
// we add this constructor first since we use left associative chains
// and our symmetry breaking should group any constants together
// beneath the same application
// we set its weight to zero since it should be considered at the
// same level as constants.
- to.d_ops.insert(to.d_ops.begin(), av.toExpr());
- to.d_cons_names.insert(to.d_cons_names.begin(), cname);
- to.d_cons_args_t.insert(to.d_cons_args_t.begin(), builtin_arg);
- to.d_pc.insert(to.d_pc.begin(),
- printer::SygusEmptyPrintCallback::getEmptyPC());
- to.d_weight.insert(to.d_weight.begin(), 0);
+ to.d_sdt.addAnyConstantConstructor(dtn);
}
}
+
+ /* Determine normalization transformation based on sygus type and given
+ * operators */
+ std::unique_ptr<Transf> transformation = inferTransf(tn, dt, op_pos);
+ /* If a transformation was selected, apply it */
+ if (transformation != nullptr)
+ {
+ transformation->buildType(this, to, dt, op_pos);
+ }
+
+ /* Remaining operators are rebuilt as they are */
+ for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+ {
+ Assert(op_pos[i] < dt.getNumConstructors());
+ to.addConsInfo(this, dt[op_pos[i]]);
+ }
/* Build normalize datatype */
if (Trace.isOn("sygus-grammar-normalize"))
{
}
Trace("sygus-grammar-normalize") << " and datatype " << dt << " \n";
}
- to.buildDatatype(this, dt);
- return to.d_unres_tn;
+ to.initializeDatatype(this, dt);
+ return unres_tn;
}
TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
#include "expr/datatype.h"
#include "expr/node.h"
-#include "expr/node_manager_attributes.h" // for VarNameAttr
+#include "expr/sygus_datatype.h"
#include "expr/type.h"
#include "expr/type_node.h"
#include "theory/quantifiers/term_util.h"
* the unresolved type node used as placeholder for references of the yet to
* be built normalized type
*
- * a datatype to represent the structure of the type node for the normalized
- * type
+ * A (SyGuS) datatype to represent the structure of the type node for the
+ * normalized type.
*/
class TypeObject
{
public:
/* Stores the original type node and the unresolved placeholder. The
* datatype for the latter is created with the respective name. */
- TypeObject(TypeNode src_tn, TypeNode unres_tn)
- : d_tn(src_tn),
- d_unres_tn(unres_tn),
- d_dt(Datatype(unres_tn.getAttribute(expr::VarNameAttr())))
- {
- }
+ TypeObject(TypeNode src_tn, TypeNode unres_tn);
~TypeObject() {}
/** adds information in "cons" (operator, name, print callback, argument
*/
static Node eliminatePartialOperators(Node n);
- /** builds a datatype with the information in the type object
+ /** initializes a datatype with the information in the type object
*
* "dt" is the datatype of the original typenode. It is necessary for
* retrieving ancillary information during the datatype building, such as
* its sygus type (e.g. Int)
*
- * The built datatype and its unresolved type are saved in the global
+ * The initialized datatype and its unresolved type are saved in the global
* accumulators of "sygus_norm"
*/
- void buildDatatype(SygusGrammarNorm* sygus_norm, const Datatype& dt);
+ void initializeDatatype(SygusGrammarNorm* sygus_norm, const Datatype& dt);
//---------- information stored from original type node
//---------- information to build normalized type node
- /* Operators for each constructor. */
- std::vector<Node> d_ops;
- /* Names for each constructor. */
- std::vector<std::string> d_cons_names;
- /* Print callbacks for each constructor */
- std::vector<std::shared_ptr<SygusPrintCallback>> d_pc;
- /* Weights for each constructor */
- std::vector<int> d_weight;
- /* List of argument types for each constructor */
- std::vector<std::vector<Type>> d_cons_args_t;
/* Unresolved type node placeholder */
TypeNode d_unres_tn;
- /* Datatype to represent type's structure */
- Datatype d_dt;
+ /** A sygus datatype */
+ SygusDatatype d_sdt;
}; /* class TypeObject */
/** Transformation abstract class
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "base/check.h"
+#include "expr/sygus_datatype.h"
#include "options/base_options.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/sygus/type_info.h"
#include "base/check.h"
+#include "expr/sygus_datatype.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
projects / cvc5.git / commitdiff