diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-15 16:11:34 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-15 16:11:34 -0600 |
commit | 5482ab60880e4611354354d863367411a99d540c (patch) | |
tree | b284e08e9ee45e009d6952d90964b80944d6296a /src/expr | |
parent | 7d43fe797c2ec03b76dd55cdb5485fb62d0dfb3a (diff) |
Introduce SyGuS datatype API (#3465)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/expr/sygus_datatype.cpp | 81 | ||||
-rw-r--r-- | src/expr/sygus_datatype.h | 110 |
3 files changed, 193 insertions, 0 deletions
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<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 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 <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 |