From b2f4485e9d079806da4e95983dc849b1741c7823 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 21 Nov 2017 17:33:35 -0600 Subject: [PATCH] Adding infrastructure for normalizing SyGuS grammars (#1397) * minor Using string previously computed * adding option * starting module for simplifying grammars * more * more * fix * fix * fix * fix * fix * removing unused command * removing unused command * removing unnecessary quantifier engine * adding lambda support * transient * reverting changes * starting normalization of integers * removing unnecessary objects * using for_each * rebuilding given datatypes * recrating types as given * bug fixing * minor * reverting space changes * addressing review * addressing review --- src/Makefile.am | 2 + src/options/quantifiers_options | 2 + src/theory/quantifiers/sygus_grammar_cons.cpp | 8 +- src/theory/quantifiers/sygus_grammar_norm.cpp | 168 ++++++++++++++++++ src/theory/quantifiers/sygus_grammar_norm.h | 149 ++++++++++++++++ 5 files changed, 328 insertions(+), 1 deletion(-) create mode 100644 src/theory/quantifiers/sygus_grammar_norm.cpp create mode 100644 src/theory/quantifiers/sygus_grammar_norm.h diff --git a/src/Makefile.am b/src/Makefile.am index f5694dc71..dc0a2b62a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -445,6 +445,8 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 8106c5e5d..1a4275d77 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -272,6 +272,8 @@ option sygusMinGrammarAgg --sygus-min-grammar-agg bool :default false 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 diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp index 68926eb34..05aa599b1 100644 --- a/src/theory/quantifiers/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus_grammar_cons.cpp @@ -20,11 +20,11 @@ #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 { @@ -118,6 +118,12 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, 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() ){ diff --git a/src/theory/quantifiers/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus_grammar_norm.cpp new file mode 100644 index 000000000..ea7722df0 --- /dev/null +++ b/src/theory/quantifiers/sygus_grammar_norm.cpp @@ -0,0 +1,168 @@ +/********************* */ +/*! \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& tos, + std::map& tn_to_unres, + std::map& 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(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(arg.getType()).getRangeType()), + tos, + tn_to_unres, + visited); + } + } +} + +void SygusGrammarNorm::normalizeSygusInt(unsigned ind, + std::vector& tos, + std::map& tn_to_unres, + Node sygus_vars) +{ + const Datatype& dt = + static_cast(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 tos; + /* Allows retrieving respective unresolved types for the sygus types of the + * original type nodes */ + std::map tn_to_unres; + std::map 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(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()); + 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(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 dts; + std::set unres_all; + for (TypeObject& to : tos) + { + dts.push_back(to.d_dt); + unres_all.insert(to.d_unres_t); + } + std::vector 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 diff --git a/src/theory/quantifiers/sygus_grammar_norm.h b/src/theory/quantifiers/sygus_grammar_norm.h new file mode 100644 index 000000000..bd63f5fdb --- /dev/null +++ b/src/theory/quantifiers/sygus_grammar_norm.h @@ -0,0 +1,149 @@ +/********************* */ +/*! \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 d_ops; + /* Names for each constructor. */ + std::vector d_cons_names; + /* List of argument types for each constructor */ + std::vector> 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& tos, + std::map& 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& tos, + std::map& tn_to_unres, + std::map& visited); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif -- 2.30.2