theory/quantifiers/sygus_invariance.h \
theory/quantifiers/sygus_grammar_cons.cpp \
theory/quantifiers/sygus_grammar_cons.h \
+ theory/quantifiers/sygus_grammar_norm.cpp \
+ theory/quantifiers/sygus_grammar_norm.h \
theory/quantifiers/sygus_process_conj.cpp \
theory/quantifiers/sygus_process_conj.h \
theory/quantifiers/symmetry_breaking.cpp \
aggressively minimize sygus grammars
option sygusAddConstGrammar --sygus-add-const-grammar bool :default true
statically add constants appearing in conjecture to grammars
+option sygusNormalizeGrammar --sygus-norm-grammar bool :default false
+ statically normalize sygus grammars based on flattening
option sygusTemplEmbedGrammar --sygus-templ-embed-grammar bool :default false
embed sygus templates into grammars
#include "options/quantifiers_options.h"
#include "theory/quantifiers/ce_guided_conjecture.h"
#include "theory/quantifiers/sygus_process_conj.h"
+#include "theory/quantifiers/sygus_grammar_norm.h"
#include "theory/quantifiers/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
using namespace CVC4::kind;
-using namespace std;
namespace CVC4 {
namespace theory {
tn = mkSygusDefaultType(
v.getType(), sfvl, ss.str(), extra_cons, term_irrelevant);
}
+ // normalize type
+ if (options::sygusNormalizeGrammar())
+ {
+ SygusGrammarNorm sygus_norm(d_qe, d_parent);
+ tn = sygus_norm.normalizeSygusType(tn, sfvl);
+ }
// check if there is a template
std::map< Node, Node >::iterator itt = templates.find( sf );
if( itt!=templates.end() ){
--- /dev/null
+/********************* */
+/*! \file sygus_grammar_norm.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa
+ ** 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 class for for simplifying SyGuS grammars after they
+ ** are encoded into datatypes.
+ **/
+
+#include "theory/quantifiers/sygus_grammar_norm.h"
+
+#include "expr/datatype.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
+#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+TypeObject::TypeObject(std::string type_name) : d_dt(Datatype(type_name))
+{
+ d_tn = TypeNode::null();
+ /* Create an unresolved type */
+ d_unres_t = NodeManager::currentNM()
+ ->mkSort(type_name, ExprManager::SORT_FLAG_PLACEHOLDER)
+ .toType();
+}
+
+TypeObject::TypeObject(TypeNode src_tn, std::string type_name)
+ : d_dt(Datatype(type_name))
+{
+ d_tn = src_tn;
+ /* Create an unresolved type */
+ d_unres_t = NodeManager::currentNM()
+ ->mkSort(type_name, ExprManager::SORT_FLAG_PLACEHOLDER)
+ .toType();
+}
+
+SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe, CegConjecture* p)
+ : d_qe(qe), d_parent(p), d_tds(d_qe->getTermDatabaseSygus())
+{
+}
+
+/* recursion depth is limited by the height of the types, which is small */
+void SygusGrammarNorm::collectInfoFor(TypeNode tn,
+ std::vector<TypeObject>& tos,
+ std::map<TypeNode, Type>& tn_to_unres,
+ std::map<TypeNode, bool>& visited)
+{
+ if (visited.find(tn) != visited.end())
+ {
+ return;
+ }
+ visited[tn] = true;
+ Assert(tn.isDatatype());
+ /* Create new type name */
+ std::stringstream ss;
+ ss << tn << "_norm";
+ std::string type_name = ss.str();
+ /* Add to global accumulators */
+ tos.push_back(TypeObject(tn, type_name));
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ tn_to_unres[tn] = tos.back().d_unres_t;
+ /* Visit types of constructor arguments */
+ for (const DatatypeConstructor& cons : dt)
+ {
+ for (const DatatypeConstructorArg& arg : cons)
+ {
+ collectInfoFor(
+ TypeNode::fromType(
+ static_cast<SelectorType>(arg.getType()).getRangeType()),
+ tos,
+ tn_to_unres,
+ visited);
+ }
+ }
+}
+
+void SygusGrammarNorm::normalizeSygusInt(unsigned ind,
+ std::vector<TypeObject>& tos,
+ std::map<TypeNode, Type>& tn_to_unres,
+ Node sygus_vars)
+{
+ const Datatype& dt =
+ static_cast<DatatypeType>(tos[ind].d_tn.toType()).getDatatype();
+ Trace("sygus-grammar-normalize")
+ << "Normalizing integer type " << tos[ind].d_tn << " from datatype\n"
+ << dt << std::endl;
+}
+
+TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
+{
+ /* Make int_type and zero */
+ NodeManager* nm = NodeManager::currentNM();
+ /* Accumulates all typing information for normalization and reconstruction */
+ std::vector<TypeObject> tos;
+ /* Allows retrieving respective unresolved types for the sygus types of the
+ * original type nodes */
+ std::map<TypeNode, Type> tn_to_unres;
+ std::map<TypeNode, bool> visited;
+ collectInfoFor(tn, tos, tn_to_unres, visited);
+ /* Build datatypes TODO and normalize accordingly #1304 */
+ for (unsigned i = 0, size = tos.size(); i < size; ++i)
+ {
+ const Datatype& dt =
+ static_cast<DatatypeType>(tos[i].d_tn.toType()).getDatatype();
+ Trace("sygus-grammar-normalize")
+ << "Rebuild " << tos[i].d_tn << " from " << dt << std::endl;
+ /* Collect information to rebuild constructors */
+ for (const DatatypeConstructor& cons : dt)
+ {
+ Trace("sygus-grammar-normalize")
+ << "...for " << cons.getName() << std::endl;
+ /* Recover the sygus operator to not lose reference to the original
+ * operator (NOT, ITE, etc) */
+ tos[i].d_ops.push_back(cons.getSygusOp());
+ tos[i].d_cons_names.push_back(cons.getName());
+ tos[i].d_cons_args_t.push_back(std::vector<Type>());
+ for (const DatatypeConstructorArg& arg : cons)
+ {
+ /* Collect unresolved types corresponding to the typenode of the
+ * arguments */
+ tos[i].d_cons_args_t.back().push_back(tn_to_unres[TypeNode::fromType(
+ static_cast<SelectorType>(arg.getType()).getRangeType())]);
+ }
+ }
+ /* Use the sygus type to not lose reference to the original types (Bool,
+ * Int, etc) */
+ tos[i].d_dt.setSygus(dt.getSygusType(),
+ sygus_vars.toExpr(),
+ dt.getSygusAllowConst(),
+ dt.getSygusAllowAll());
+ for (unsigned j = 0, size_d_ops = tos[i].d_ops.size(); j < size_d_ops; ++j)
+ {
+ tos[i].d_dt.addSygusConstructor(
+ tos[i].d_ops[j], tos[i].d_cons_names[j], tos[i].d_cons_args_t[j]);
+ }
+ Trace("sygus-grammar-normalize")
+ << "...built datatype " << tos[i].d_dt << std::endl;
+ }
+ /* Resolve types */
+ std::vector<Datatype> dts;
+ std::set<Type> unres_all;
+ for (TypeObject& to : tos)
+ {
+ dts.push_back(to.d_dt);
+ unres_all.insert(to.d_unres_t);
+ }
+ std::vector<DatatypeType> types =
+ nm->toExprManager()->mkMutualDatatypeTypes(dts, unres_all);
+ Assert(types.size() == dts.size());
+ /* By construction the normalized type node will be first one considered */
+ return TypeNode::fromType(types[0]);
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file sygus_grammar_norm.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa
+ ** 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 class for simplifying SyGuS grammars after they are encoded into
+ ** datatypes.
+ **/
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_SIMP_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_SIMP_H
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegConjecture;
+
+/** Keeps the necessary information about a sygus type:
+ *
+ * the original typenode, from which the datatype representation can be
+ * extracted
+ *
+ * the operators, names and argument types for each constructor
+ *
+ * the unresolved type used as placeholder for references of the yet to be built
+ * type
+ *
+ * a datatype to represent the structure of the typenode for the new type */
+struct TypeObject
+{
+ /* Both constructors create an unresolved type and datatype with the given
+ * name. An original typenode is optional, since normalized types can be
+ * created from scratch during normalization */
+ TypeObject(TypeNode src_tn, std::string type_name);
+ TypeObject(std::string type_name);
+ ~TypeObject() {}
+
+ /* The original typenode this TypeObject is built from */
+ TypeNode d_tn;
+ /* Operators for each constructor. */
+ std::vector<Expr> d_ops;
+ /* Names for each constructor. */
+ std::vector<std::string> d_cons_names;
+ /* List of argument types for each constructor */
+ std::vector<std::vector<Type>> d_cons_args_t;
+ /* Unresolved type placeholder */
+ Type d_unres_t;
+ /* Datatype to represent type's structure */
+ Datatype d_dt;
+};
+
+/** Utility for normalizing SyGuS grammars and avoid spurious enumarations
+ *
+ * Uses the datatype representation of a SyGuS grammar to identify entries that
+ * can normalized in order to have less possible enumerations. An example is
+ * with integer types, e.g.:
+ *
+ * Int -> x | y | Int + Int | Int - Int | 0 | 1 | ite( Bool, Int, Int ) |
+ * c1...cn
+ *
+ * where c1...cn are additional constants (in the case of large constants
+ * appearing in the conjecture).
+ *
+ * becomes
+ *
+ * Int -> ite( Bool, Int, Int ) | IntN
+ * IntN -> IntX | Int0 - IntX
+ * Int0 -> 0
+ * IntX -> IntXX + IntX | IntY
+ * IntXX -> x
+ * IntY -> IntYY + IntY | IntC
+ * IntYY -> y
+ * IntC -> IntCC + IntC | IntV
+ * IntCC -> 1
+ * IntV -> 0 | c1...cn */
+class SygusGrammarNorm
+{
+ public:
+ SygusGrammarNorm(QuantifiersEngine* qe, CegConjecture* p);
+ ~SygusGrammarNorm() {}
+ /** creates a normalized typenode from a given one.
+ *
+ * In a normalized typenode all of its types that can be normalized (e.g. Int)
+ * are so and its other types are structurally identical to the original
+ * typenode it normalizes.
+ *
+ * sygus_vars are the input variables for the function to be synthesized,
+ * which are used as input for the built datatypes. */
+ TypeNode normalizeSygusType(TypeNode tn, Node sygus_vars);
+
+ private:
+ /** reference to quantifier engine */
+ QuantifiersEngine* d_qe;
+ /** parent conjecture
+ *
+ * This contains global information about the synthesis conjecture. */
+ CegConjecture* d_parent;
+
+ /** sygus term database associated with this utility */
+ TermDbSygus* d_tds;
+
+ /** normalize integer type
+ *
+ * TODO actually perform the normalization #1304
+ *
+ * ind is the index of the analyzed typeobject in tos
+ *
+ * New types created during normalization will be added to tos and
+ * tn_to_unres
+ *
+ * sygus_vars is used as above for datatype construction */
+ void normalizeSygusInt(unsigned ind,
+ std::vector<TypeObject>& tos,
+ std::map<TypeNode, Type>& tn_to_unres,
+ Node sygus_vars);
+
+ /** Traverses the datatype representation of src_tn and collects the types it
+ * contains
+ *
+ * For each new typenode a TypeObject is created, with an unresolved type and
+ * a datatype to be later resolved and constructed, respectively. These are
+ * accumulated in tos.
+ *
+ * tn_to_unres maps the sygus types that the typenodes stand for into
+ * the unresolved type to be built for the typenodes normalizations.
+ *
+ * visited caches visited nodes
+ */
+ void collectInfoFor(TypeNode src_tn,
+ std::vector<TypeObject>& tos,
+ std::map<TypeNode, Type>& tn_to_unres,
+ std::map<TypeNode, bool>& visited);
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif
projects / cvc5.git / commitdiff