From 5482ab60880e4611354354d863367411a99d540c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 15 Nov 2019 16:11:34 -0600 Subject: [PATCH] Introduce SyGuS datatype API (#3465) --- src/expr/CMakeLists.txt | 2 + src/expr/sygus_datatype.cpp | 81 +++++++++ src/expr/sygus_datatype.h | 110 ++++++++++++ src/theory/datatypes/datatypes_rewriter.cpp | 1 + src/theory/datatypes/sygus_extension.cpp | 1 + .../datatypes/theory_datatypes_utils.cpp | 1 + src/theory/datatypes/theory_datatypes_utils.h | 6 - .../quantifiers/sygus/sygus_grammar_norm.cpp | 159 ++++++++---------- .../quantifiers/sygus/sygus_grammar_norm.h | 33 +--- .../quantifiers/sygus/term_database_sygus.cpp | 1 + src/theory/quantifiers/sygus/type_info.cpp | 1 + 11 files changed, 279 insertions(+), 117 deletions(-) create mode 100644 src/expr/sygus_datatype.cpp create mode 100644 src/expr/sygus_datatype.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 479b28cfb..0c1044e74 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -48,6 +48,8 @@ libcvc4_add_sources( datatype.cpp record.cpp record.h + sygus_datatype.cpp + sygus_datatype.h uninterpreted_constant.cpp uninterpreted_constant.h ) diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp new file mode 100644 index 000000000..be2b04402 --- /dev/null +++ b/src/expr/sygus_datatype.cpp @@ -0,0 +1,81 @@ +/********************* */ +/*! \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 spc, + int weight, + const std::vector& 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 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 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 diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h new file mode 100644 index 000000000..d7b18644a --- /dev/null +++ b/src/expr/sygus_datatype.h @@ -0,0 +1,110 @@ +/********************* */ +/*! \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 +#include + +#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 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 spc, + int weight, + const std::vector& 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 d_ops; + /** Names for each constructor. */ + std::vector d_cons_names; + /** Print callbacks for each constructor */ + std::vector> d_pc; + /** Weights for each constructor */ + std::vector d_weight; + /** List of argument types for each constructor */ + std::vector> d_consArgs; + /** Datatype to represent type's structure */ + Datatype d_dt; +}; + +} // namespace CVC4 + +#endif diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 572ddbac2..be4226f69 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -17,6 +17,7 @@ #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" diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 7e5a3ae98..ceb5d2dab 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -15,6 +15,7 @@ #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" diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index bb62ab8ae..5bf0ca036 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -17,6 +17,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" #include "expr/node_algorithm.h" +#include "expr/sygus_datatype.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index 92783c2f7..2ac288c4c 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -34,12 +34,6 @@ struct SygusVarNumAttributeId }; typedef expr::Attribute SygusVarNumAttribute; -/** Attribute true for variables that represent any constant */ -struct SygusAnyConstAttributeId -{ -}; -typedef expr::Attribute SygusAnyConstAttribute; - /** * Attribute true for enumerators whose current model values were registered by * the datatypes sygus solver, and were not excluded by sygus symmetry breaking. diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 5e8c9c411..68445fca0 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -16,6 +16,7 @@ #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" @@ -73,6 +74,12 @@ SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe) { } +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; @@ -200,47 +207,40 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm, 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()); + std::vector 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(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"; } @@ -334,27 +334,25 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, /* creates type for element */ std::vector 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()); - to.d_cons_args_t.back().push_back(t); + std::vector 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()); - to.d_cons_args_t.back().push_back(t); - to.d_cons_args_t.back().push_back(to.d_unres_tn.toType()); + std::vector 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"; @@ -383,13 +381,13 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, 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()); - to.d_cons_args_t.back().push_back( - sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos).toType()); + std::vector 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 SygusGrammarNorm::d_tn_to_id = {}; @@ -541,21 +539,6 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, /* Creates type object for normalization */ TypeObject to(tn, unres_tn); - /* Determine normalization transformation based on sygus type and given - * operators */ - std::unique_ptr 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()); @@ -568,29 +551,31 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, && !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 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 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")) { @@ -601,8 +586,8 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, } 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) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 00c501cfe..f9c53c4ad 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -24,7 +24,7 @@ #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" @@ -178,20 +178,15 @@ class SygusGrammarNorm * 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 @@ -215,16 +210,16 @@ class SygusGrammarNorm */ 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 @@ -233,20 +228,10 @@ class SygusGrammarNorm //---------- information to build normalized type node - /* Operators for each constructor. */ - std::vector d_ops; - /* Names for each constructor. */ - std::vector d_cons_names; - /* Print callbacks for each constructor */ - std::vector> d_pc; - /* Weights for each constructor */ - std::vector d_weight; - /* List of argument types for each constructor */ - std::vector> 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 diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 84a9c2405..79b4c9caa 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -15,6 +15,7 @@ #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" diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 5f51d8dec..1ff0457c4 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -15,6 +15,7 @@ #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" -- 2.30.2