From bca2ee1c42332abc8deb57d620b0fc32b5394634 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 3 Oct 2017 10:19:27 -0500 Subject: [PATCH] Move sygus grammar utilities to separate file. (#1184) * Move sygus grammar utilities to separate file. * Minor * Move includes --- src/Makefile.am | 2 + .../quantifiers/ce_guided_conjecture.cpp | 208 +----- src/theory/quantifiers/ce_guided_conjecture.h | 8 +- src/theory/quantifiers/sygus_grammar_cons.cpp | 594 ++++++++++++++++++ src/theory/quantifiers/sygus_grammar_cons.h | 89 +++ .../quantifiers/term_database_sygus.cpp | 355 ----------- src/theory/quantifiers/term_database_sygus.h | 33 - 7 files changed, 712 insertions(+), 577 deletions(-) create mode 100644 src/theory/quantifiers/sygus_grammar_cons.cpp create mode 100644 src/theory/quantifiers/sygus_grammar_cons.h diff --git a/src/Makefile.am b/src/Makefile.am index 7b9a607a1..cfb8e379d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -414,6 +414,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/relevant_domain.h \ theory/quantifiers/rewrite_engine.cpp \ theory/quantifiers/rewrite_engine.h \ + theory/quantifiers/sygus_grammar_cons.cpp \ + theory/quantifiers/sygus_grammar_cons.h \ theory/quantifiers/symmetry_breaking.cpp \ theory/quantifiers/symmetry_breaking.h \ theory/quantifiers/term_database.cpp \ diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index e53a95a2b..0fe246964 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -46,218 +46,58 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe) d_refine_count = 0; d_ceg_si = new CegConjectureSingleInv(qe, this); d_ceg_pbe = new CegConjecturePbe(qe, this); + d_ceg_gc = new CegGrammarConstructor(qe); } CegConjecture::~CegConjecture() { delete d_ceg_si; delete d_ceg_pbe; + delete d_ceg_gc; } -Node CegConjecture::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ){ - std::map< Node, Node >::iterator it = visited.find( n ); - if( it==visited.end() ){ - Node ret = n; - - std::vector< Node > children; - bool childChanged = false; - bool madeOp = false; - Kind ret_k = n.getKind(); - Node op; - if( n.getNumChildren()>0 ){ - if( n.getKind()==kind::APPLY_UF ){ - op = n.getOperator(); - } - }else{ - op = n; - } - // is it a synth function? - std::map< Node, Node >::iterator its = synth_fun_vars.find( op ); - if( its!=synth_fun_vars.end() ){ - Assert( its->second.getType().isDatatype() ); - // make into evaluation function - const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype(); - Assert( dt.isSygus() ); - children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) ); - children.push_back( its->second ); - madeOp = true; - childChanged = true; - ret_k = kind::APPLY_UF; - } - if( n.getNumChildren()>0 || childChanged ){ - if( !madeOp ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - } - for( unsigned i=0; imkNode( ret_k, children ); - } - } - visited[n] = ret; - return ret; - }else{ - return it->second; - } -} - -void CegConjecture::collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( n.isConst() ){ - TypeNode tn = n.getType(); - Node nc = n; - if( tn.isReal() ){ - nc = NodeManager::currentNM()->mkConst( n.getConst().abs() ); - } - if( std::find( consts[tn].begin(), consts[tn].end(), nc )==consts[tn].end() ){ - Trace("cegqi-debug") << "...consider const : " << nc << std::endl; - consts[tn].push_back( nc ); - } - } - - for( unsigned i=0; i templates; + std::map< Node, Node > templates_arg; //register with single invocation if applicable if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){ d_ceg_si->initialize( d_quant ); - simp_quant = d_ceg_si->getSimplifiedConjecture(); - } - - // convert to deep embedding and finalize single invocation here - // now, construct the grammar - Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; - std::map< TypeNode, std::vector< Node > > extra_cons; - Trace("cegqi") << "CegConjecture : collect constants..." << std::endl; - if( options::sygusAddConstGrammar() ){ - std::map< Node, bool > visited; - collectConstants( q[1], extra_cons, visited ); - } - bool has_ites = true; - bool is_syntax_restricted = false; - std::vector< Node > qchildren; - std::map< Node, Node > visited; - std::map< Node, Node > synth_fun_vars; - std::vector< Node > ebvl; - Node qbody_subs = simp_quant[1]; - for( unsigned i=0; igetTermDatabaseSygus()->mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons ); - } - Node templ = d_ceg_si->getTemplate( sf ); - if( !templ.isNull() ){ - TNode templ_arg = d_ceg_si->getTemplateArg( sf ); - Assert( !templ_arg.isNull() ); - Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl; - // if there is a template for this argument, make a sygus type on top of it - if( options::sygusTemplEmbedGrammar() ){ - Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl; - tn = d_qe->getTermDatabaseSygus()->mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() ); - }else{ - // otherwise, apply it as a preprocessing pass - Trace("cegqi-debug") << " apply this template as a substituion during preprocess..." << std::endl; - std::vector< Node > schildren; - std::vector< Node > largs; - for( unsigned j=0; jmkBoundVar( sfvl[j].getType() ) ); - } - std::vector< Node > subsfn_children; - subsfn_children.push_back( sf ); - subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() ); - Node subsfn = NodeManager::currentNM()->mkNode( kind::APPLY_UF, subsfn_children ); - TNode subsf = subsfn; - Trace("cegqi-debug") << " substitute arg : " << templ_arg << " -> " << subsf << std::endl; - templ = templ.substitute( templ_arg, subsf ); - // substitute lambda arguments - templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() ); - Node subsn = NodeManager::currentNM()->mkNode( kind::LAMBDA, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, largs ), templ ); - TNode var = sf; - TNode subs = subsn; - Trace("cegqi-debug") << " substitute : " << var << " -> " << subs << std::endl; - qbody_subs = qbody_subs.substitute( var, subs ); - Trace("cegqi-debug") << " body is now : " << qbody_subs << std::endl; - } - } - d_qe->getTermDatabaseSygus()->registerSygusType( tn ); - // check grammar restrictions - if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ - if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ - has_ites = false; + q = d_ceg_si->getSimplifiedConjecture(); + // carry the templates + for( unsigned i=0; igetTemplate(sf); + if( !templ.isNull() ){ + templates[sf] = templ; + templates_arg[sf] = d_ceg_si->getTemplateArg(sf); } } - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Assert( dt.isSygus() ); - if( !dt.getSygusAllowAll() ){ - is_syntax_restricted = true; - } - - // ev is the first-order variable corresponding to this synth fun - std::stringstream ssf; - ssf << "f" << sf; - Node ev = NodeManager::currentNM()->mkBoundVar( ssf.str(), tn ); - ebvl.push_back( ev ); - synth_fun_vars[sf] = ev; - Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl; } - qchildren.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) ); - if( qbody_subs!=simp_quant[1] ){ - Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl; - qbody_subs = Rewriter::rewrite( qbody_subs ); - Trace("cegqi") << "...got : " << qbody_subs << std::endl; - } - qchildren.push_back( convertToEmbedding( qbody_subs, synth_fun_vars, visited ) ); - if( q.getNumChildren()==3 ){ - qchildren.push_back( q[2] ); - } - q = NodeManager::currentNM()->mkNode( kind::FORALL, qchildren ); - Trace("cegqi") << "CegConjecture : converted to embedding : " << q << std::endl; - d_embed_quant = q; + + // convert to deep embedding and finalize single invocation here + d_embed_quant = d_ceg_gc->process( q, templates, templates_arg ); + Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl; // we now finalize the single invocation module, based on the syntax restrictions if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){ - d_ceg_si->finishInit( is_syntax_restricted, has_ites ); + d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted(), d_ceg_gc->hasSyntaxITE() ); } Assert( d_candidates.empty() ); std::vector< Node > vars; - for( unsigned i=0; imkSkolem( "e", q[0][i].getType() ); + for( unsigned i=0; imkSkolem( "e", d_embed_quant[0][i].getType() ); d_candidates.push_back( e ); } - Trace("cegqi") << "Base quantified formula is : " << q << std::endl; + Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl; //construct base instantiation - d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) ); + d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( d_embed_quant, vars, d_candidates ) ); // register this term with sygus database std::vector< Node > guarded_lemmas; @@ -271,7 +111,7 @@ void CegConjecture::assign( Node q ) { std::vector< std::vector< Node > > exs; std::vector< Node > exos; std::vector< Node > exts; - // use the PBE examples, regardless of the search algorith, since these help search space pruning + // use the PBE examples, regardless of the search algorithm, since these help search space pruning if( d_ceg_pbe->getPbeExamples( e, exs, exos, exts ) ){ d_qe->getTermDatabaseSygus()->registerPbeExamples( e, exs, exos, exts ); } diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h index 1263778d3..c99867ac7 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.h +++ b/src/theory/quantifiers/ce_guided_conjecture.h @@ -18,9 +18,9 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H -#include "context/cdhashmap.h" #include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/ce_guided_pbe.h" +#include "theory/quantifiers/sygus_grammar_cons.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -103,6 +103,8 @@ private: CegConjectureSingleInv * d_ceg_si; /** program by examples utility */ CegConjecturePbe * d_ceg_pbe; + /** grammar utility */ + CegGrammarConstructor * d_ceg_gc; /** list of constants for quantified formula */ std::vector< Node > d_candidates; /** base instantiation */ @@ -131,10 +133,6 @@ private: std::map< Node, CandidateInfo > d_cinfo; /** number of times we have called doRefine */ unsigned d_refine_count; - /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */ - Node convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ); - /** collect constants */ - void collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ); /** construct candidates */ bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, std::vector< Node >& lems ); diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp new file mode 100644 index 000000000..194e32b61 --- /dev/null +++ b/src/theory/quantifiers/sygus_grammar_cons.cpp @@ -0,0 +1,594 @@ +/********************* */ +/*! \file sygus_grammar_cons.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 constructing inductive datatypes that correspond to + ** grammars that encode syntactic restrictions for SyGuS. + **/ +#include "theory/quantifiers/sygus_grammar_cons.h" + +#include + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" +#include "theory/quantifiers/term_database_sygus.h" + +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + + +CegGrammarConstructor::CegGrammarConstructor( QuantifiersEngine * qe ) : +d_qe( qe ), d_is_syntax_restricted(false), d_has_ite(true){ + +} + +void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts ){ + std::unordered_map visited; + std::unordered_map::iterator it; + std::stack visit; + TNode cur; + visit.push(n); + do { + cur = visit.top(); + visit.pop(); + it = visited.find(cur); + if (it == visited.end()) { + visited[cur] = true; + // is this a constant? + if( cur.isConst() ){ + TypeNode tn = cur.getType(); + Node c = cur; + if( tn.isReal() ){ + c = NodeManager::currentNM()->mkConst( c.getConst().abs() ); + } + if( std::find( consts[tn].begin(), consts[tn].end(), c )==consts[tn].end() ){ + Trace("cegqi-debug") << "...consider const : " << c << std::endl; + consts[tn].push_back( c ); + } + } + // recurse + for (unsigned i = 0; i < cur.getNumChildren(); i++) { + visit.push(cur[i]); + } + } + } while (!visit.empty()); +} + + + +Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, std::map< Node, Node >& templates_arg ) { + // convert to deep embedding and finalize single invocation here + // now, construct the grammar + Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; + std::map< TypeNode, std::vector< Node > > extra_cons; + if( options::sygusAddConstGrammar() ){ + Trace("cegqi") << "CegConjecture : collect constants..." << std::endl; + collectTerms( q[1], extra_cons ); + } + + std::vector< Node > qchildren; + std::map< Node, Node > synth_fun_vars; + std::vector< Node > ebvl; + Node qbody_subs = q[1]; + for( unsigned i=0; i::iterator itt = templates.find( sf ); + if( itt!=templates.end() ){ + Node templ = itt->second; + TNode templ_arg = templates_arg[sf]; + Assert( !templ_arg.isNull() ); + Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl; + // if there is a template for this argument, make a sygus type on top of it + if( options::sygusTemplEmbedGrammar() ){ + Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl; + tn = mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() ); + }else{ + // otherwise, apply it as a preprocessing pass + Trace("cegqi-debug") << " apply this template as a substituion during preprocess..." << std::endl; + std::vector< Node > schildren; + std::vector< Node > largs; + for( unsigned j=0; jmkBoundVar( sfvl[j].getType() ) ); + } + std::vector< Node > subsfn_children; + subsfn_children.push_back( sf ); + subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() ); + Node subsfn = NodeManager::currentNM()->mkNode( kind::APPLY_UF, subsfn_children ); + TNode subsf = subsfn; + Trace("cegqi-debug") << " substitute arg : " << templ_arg << " -> " << subsf << std::endl; + templ = templ.substitute( templ_arg, subsf ); + // substitute lambda arguments + templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() ); + Node subsn = NodeManager::currentNM()->mkNode( kind::LAMBDA, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, largs ), templ ); + TNode var = sf; + TNode subs = subsn; + Trace("cegqi-debug") << " substitute : " << var << " -> " << subs << std::endl; + qbody_subs = qbody_subs.substitute( var, subs ); + Trace("cegqi-debug") << " body is now : " << qbody_subs << std::endl; + } + } + d_qe->getTermDatabaseSygus()->registerSygusType( tn ); + // check grammar restrictions + if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ + if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ + d_has_ite = false; + } + } + Assert( tn.isDatatype() ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isSygus() ); + if( !dt.getSygusAllowAll() ){ + d_is_syntax_restricted = true; + } + + // ev is the first-order variable corresponding to this synth fun + std::stringstream ssf; + ssf << "f" << sf; + Node ev = NodeManager::currentNM()->mkBoundVar( ssf.str(), tn ); + ebvl.push_back( ev ); + synth_fun_vars[sf] = ev; + Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl; + } + qchildren.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) ); + if( qbody_subs!=q[1] ){ + Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl; + qbody_subs = Rewriter::rewrite( qbody_subs ); + Trace("cegqi") << "...got : " << qbody_subs << std::endl; + } + qchildren.push_back( convertToEmbedding( qbody_subs, synth_fun_vars ) ); + if( q.getNumChildren()==3 ){ + qchildren.push_back( q[2] ); + } + return NodeManager::currentNM()->mkNode( kind::FORALL, qchildren ); +} + +Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ){ + std::unordered_map visited; + std::unordered_map::iterator it; + std::stack visit; + TNode cur; + visit.push(n); + do { + cur = visit.top(); + visit.pop(); + it = visited.find(cur); + if (it == visited.end()) { + visited[cur] = Node::null(); + visit.push(cur); + for (unsigned i = 0; i < cur.getNumChildren(); i++) { + visit.push(cur[i]); + } + } else if (it->second.isNull()) { + Node ret = cur; + Kind ret_k = cur.getKind(); + Node op; + bool childChanged = false; + std::vector children; + // get the potential operator + if( cur.getNumChildren()>0 ){ + if( cur.getKind()==kind::APPLY_UF ){ + op = cur.getOperator(); + } + }else{ + op = cur; + } + // is the operator a synth function? + if( !op.isNull() ){ + std::map< Node, Node >::iterator its = synth_fun_vars.find( op ); + if( its!=synth_fun_vars.end() ){ + Assert( its->second.getType().isDatatype() ); + // will make into an application of an evaluation function + const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype(); + Assert( dt.isSygus() ); + children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) ); + children.push_back( its->second ); + childChanged = true; + ret_k = kind::APPLY_UF; + } + } + if( !childChanged ){ + // otherwise, we apply the previous operator + if( cur.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( cur.getOperator() ); + } + } + for (unsigned i = 0; i < cur.getNumChildren(); i++) { + it = visited.find(cur[i]); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cur[i] != it->second; + children.push_back(it->second); + } + if (childChanged) { + ret = NodeManager::currentNM()->mkNode(ret_k, children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + + +TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name, std::set& unres) { + TypeNode unresolved = NodeManager::currentNM()->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER); + unres.insert( unresolved.toType() ); + return unresolved; +} + +void CegGrammarConstructor::mkSygusConstantsForType( TypeNode type, std::vector& ops ) { + if( type.isInteger() ){ + ops.push_back(NodeManager::currentNM()->mkConst(Rational(0))); + ops.push_back(NodeManager::currentNM()->mkConst(Rational(1))); + }else if( type.isBitVector() ){ + unsigned sz = ((BitVectorType)type.toType()).getSize(); + BitVector bval0(sz, (unsigned int)0); + ops.push_back( NodeManager::currentNM()->mkConst(bval0) ); + BitVector bval1(sz, (unsigned int)1); + ops.push_back( NodeManager::currentNM()->mkConst(bval1) ); + }else if( type.isBoolean() ){ + ops.push_back(NodeManager::currentNM()->mkConst(true)); + ops.push_back(NodeManager::currentNM()->mkConst(false)); + } + //TODO : others? +} + +void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){ + if( !range.isBoolean() ){ + if( std::find( types.begin(), types.end(), range )==types.end() ){ + Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl; + types.push_back( range ); + if( range.isDatatype() ){ + const Datatype& dt = ((DatatypeType)range.toType()).getDatatype(); + for( unsigned i=0; i >& extra_cons, + std::vector< CVC4::Datatype >& datatypes, std::set& unres ) { + // collect the variables + std::vector sygus_vars; + if( !bvl.isNull() ){ + for( unsigned i=0; i > ops; + int startIndex = -1; + Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " << range << std::endl; + std::map< Type, Type > sygus_to_builtin; + + std::vector< TypeNode > types; + std::map< TypeNode, std::vector< DatatypeConstructorArg > > sels; + //types for each of the variables of parametric sort + for( unsigned i=0; i unres_types; + std::map< TypeNode, Type > type_to_unres; + for( unsigned i=0; i()); + //make unresolved type + Type unres_t = mkUnresolvedType(dname, unres).toType(); + unres_types.push_back(unres_t); + type_to_unres[types[i]] = unres_t; + sygus_to_builtin[unres_t] = types[i].toType(); + } + for( unsigned i=0; i cnames; + std::vector > cargs; + Type unres_t = unres_types[i]; + //add variables + for( unsigned j=0; j() ); + } + } + //add constants + std::vector< Node > consts; + mkSygusConstantsForType( types[i], consts ); + std::map< TypeNode, std::vector< Node > >::iterator itec = extra_cons.find( types[i] ); + if( itec!=extra_cons.end() ){ + //consts.insert( consts.end(), itec->second.begin(), itec->second.end() ); + for( unsigned j=0; jsecond.size(); j++ ){ + if( std::find( consts.begin(), consts.end(), itec->second[j] )==consts.end() ){ + consts.push_back( itec->second[j] ); + } + } + } + for( unsigned j=0; j() ); + } + //ITE + CVC4::Kind k = kind::ITE; + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + cnames.push_back( kind::kindToString(k) ); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(unres_bt); + cargs.back().push_back(unres_t); + cargs.back().push_back(unres_t); + + if( types[i].isInteger() ){ + for( unsigned j=0; j<2; j++ ){ + CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS; + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(unres_t); + cargs.back().push_back(unres_t); + } + }else if( types[i].isDatatype() ){ + Trace("sygus-grammar-def") << "...add for constructors" << std::endl; + const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); + for( unsigned k=0; k() ); + for( unsigned j=0; j() ); + //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() ); + cargs.back().push_back( type_to_unres[arg_type] ); + } + } + Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl; + datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true ); + for( unsigned j=0; jbooleanType(); + datatypes.push_back(Datatype(dbname)); + ops.push_back(std::vector()); + std::vector cnames; + std::vector > cargs; + Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl; + //add variables + for( unsigned i=0; i() ); + } + } + //add constants if no variables and no connected types + if( ops.back().empty() && types.empty() ){ + std::vector< Node > consts; + mkSygusConstantsForType( btype, consts ); + for( unsigned j=0; j() ); + } + } + //add operators + for( unsigned i=0; i<3; i++ ){ + CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR ); + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + if( k==kind::NOT ){ + cargs.back().push_back(unres_bt); + }else if( k==kind::AND || k==kind::OR ){ + cargs.back().push_back(unres_bt); + cargs.back().push_back(unres_bt); + } + } + //add predicates for types + for( unsigned i=0; ioperatorOf(k).toExpr()); + std::stringstream ss; + ss << kind::kindToString(k) << "_" << types[i]; + cnames.push_back(ss.str()); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(unres_types[i]); + cargs.back().push_back(unres_types[i]); + //type specific predicates + if( types[i].isInteger() ){ + CVC4::Kind k = kind::LEQ; + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(unres_types[i]); + cargs.back().push_back(unres_types[i]); + }else if( types[i].isDatatype() ){ + //add for testers + Trace("sygus-grammar-def") << "...add for testers" << std::endl; + const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); + for( unsigned k=0; k() ); + cargs.back().push_back(unres_types[i]); + } + } + } + if( range==btype ){ + startIndex = datatypes.size()-1; + } + Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl; + datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true ); + for( unsigned j=0; j0 ){ + CVC4::Datatype tmp_dt = datatypes[0]; + datatypes[0] = datatypes[startIndex]; + datatypes[startIndex] = tmp_dt; + } +} + + +TypeNode CegGrammarConstructor::mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, + std::map< TypeNode, std::vector< Node > >& extra_cons ) { + Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl; + for( std::map< TypeNode, std::vector< Node > >::iterator it = extra_cons.begin(); it != extra_cons.end(); ++it ){ + Trace("sygus-grammar-def") << " ...using " << it->second.size() << " extra constants for " << it->first << std::endl; + } + std::set unres; + std::vector< CVC4::Datatype > datatypes; + mkSygusDefaultGrammar( range, bvl, fun, extra_cons, datatypes, unres ); + Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl; + Assert( !datatypes.empty() ); + std::vector types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres); + Assert( types.size()==datatypes.size() ); + return TypeNode::fromType( types[0] ); +} + +TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, + const std::string& fun, unsigned& tcount ) { + if( templ==templ_arg ){ + //Assert( templ_arg.getType()==sygusToBuiltinType( templ_arg_sygus_type ) ); + return templ_arg_sygus_type; + }else{ + tcount++; + std::set unres; + std::vector< CVC4::Datatype > datatypes; + std::stringstream ssd; + ssd << fun << "_templ_" << tcount; + std::string dbname = ssd.str(); + datatypes.push_back(Datatype(dbname)); + Node op; + std::vector< Type > argTypes; + if( templ.getNumChildren()==0 ){ + // TODO : can short circuit to this case when !TermDb::containsTerm( templ, templ_arg ) + op = templ; + }else{ + Assert( templ.hasOperator() ); + op = templ.getOperator(); + // make constructor taking arguments types from children + for( unsigned i=0; i types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres); + Assert( types.size()==1 ); + return TypeNode::fromType( types[0] ); + } +} + +TypeNode CegGrammarConstructor::mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, + const std::string& fun ) { + unsigned tcount = 0; + return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount ); +} + +}/* namespace CVC4::theory::quantifiers */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus_grammar_cons.h b/src/theory/quantifiers/sygus_grammar_cons.h new file mode 100644 index 000000000..e8b09293c --- /dev/null +++ b/src/theory/quantifiers/sygus_grammar_cons.h @@ -0,0 +1,89 @@ +/********************* */ +/*! \file sygus_grammar_cons.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 constructing inductive datatypes that correspond to + ** grammars that encode syntactic restrictions for SyGuS. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** utility for constructing datatypes that correspond to syntactic restrictions, +* and applying the deep embedding from Section 4 of Reynolds et al CAV 2015. +*/ +class CegGrammarConstructor +{ +public: + CegGrammarConstructor( QuantifiersEngine * qe ); + ~CegGrammarConstructor(){} + /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */ + Node process( Node q, std::map< Node, Node >& templates, std::map< Node, Node >& templates_arg ); + /** is the syntax restricted? */ + bool isSyntaxRestricted() { return d_is_syntax_restricted; } + /** does the syntax allow ITE expressions? */ + bool hasSyntaxITE() { return d_has_ite; } + // make the default sygus datatype type corresponding to builtin type range + // bvl is the set of free variables to include in the grammar + // fun is for naming + // extra_cons is a set of extra constant symbols to include in the grammar + static TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons ); + // make the default sygus datatype type corresponding to builtin type range + static TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun ){ + std::map< TypeNode, std::vector< Node > > extra_cons; + return mkSygusDefaultType( range, bvl, fun, extra_cons ); + } + // make the sygus datatype type that encodes the solution space (lambda templ_arg. templ[templ_arg]) where templ_arg + // has syntactic restrictions encoded by sygus type templ_arg_sygus_type + // bvl is the set of free variables to include in the frammar + // fun is for naming + static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun ); +private: + /** reference to quantifier engine */ + QuantifiersEngine * d_qe; + /** is the syntax restricted? */ + bool d_is_syntax_restricted; + /** does the syntax allow ITE expressions? */ + bool d_has_ite; + /** collect terms */ + void collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts ); + /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */ + Node convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ); + //---------------- grammar construction + // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) + static TypeNode mkUnresolvedType(const std::string& name, std::set& unres); + // make the builtin constants for type type that should be included in a sygus grammar + static void mkSygusConstantsForType( TypeNode type, std::vector& ops ); + // collect the list of types that depend on type range + static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); + // helper function for function mkSygusDefaultGrammar + // collects a set of mutually recursive datatypes "datatypes" corresponding to encoding type "range" to SyGuS + // unres is used for the resulting call to mkMutualDatatypeTypes + static void mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, + std::vector< CVC4::Datatype >& datatypes, std::set& unres ); + // helper function for mkSygusTemplateType + static TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, + const std::string& fun, unsigned& tcount ); + //---------------- end grammar construction +}; + +} /* namespace CVC4::theory::quantifiers */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ + +#endif diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index a0af545e1..61bb20987 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -2694,361 +2694,6 @@ Node TermDbSygus::extendedRewrite( Node n ) { } - - - - -TypeNode TermDbSygus::mkUnresolvedType(const std::string& name, std::set& unres) { - TypeNode unresolved = NodeManager::currentNM()->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER); - unres.insert( unresolved.toType() ); - return unresolved; -} - -void TermDbSygus::mkSygusConstantsForType( TypeNode type, std::vector& ops ) { - if( type.isInteger() ){ - ops.push_back(NodeManager::currentNM()->mkConst(Rational(0))); - ops.push_back(NodeManager::currentNM()->mkConst(Rational(1))); - }else if( type.isBitVector() ){ - unsigned sz = ((BitVectorType)type.toType()).getSize(); - BitVector bval0(sz, (unsigned int)0); - ops.push_back( NodeManager::currentNM()->mkConst(bval0) ); - BitVector bval1(sz, (unsigned int)1); - ops.push_back( NodeManager::currentNM()->mkConst(bval1) ); - }else if( type.isBoolean() ){ - ops.push_back(NodeManager::currentNM()->mkConst(true)); - ops.push_back(NodeManager::currentNM()->mkConst(false)); - } - //TODO : others? -} - -void TermDbSygus::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){ - if( !range.isBoolean() ){ - if( std::find( types.begin(), types.end(), range )==types.end() ){ - Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl; - types.push_back( range ); - if( range.isDatatype() ){ - const Datatype& dt = ((DatatypeType)range.toType()).getDatatype(); - for( unsigned i=0; i >& extra_cons, - std::vector< CVC4::Datatype >& datatypes, std::set& unres ) { - // collect the variables - std::vector sygus_vars; - if( !bvl.isNull() ){ - for( unsigned i=0; i > ops; - int startIndex = -1; - Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " << range << std::endl; - std::map< Type, Type > sygus_to_builtin; - - std::vector< TypeNode > types; - std::map< TypeNode, std::vector< DatatypeConstructorArg > > sels; - //types for each of the variables of parametric sort - for( unsigned i=0; i unres_types; - std::map< TypeNode, Type > type_to_unres; - for( unsigned i=0; i()); - //make unresolved type - Type unres_t = mkUnresolvedType(dname, unres).toType(); - unres_types.push_back(unres_t); - type_to_unres[types[i]] = unres_t; - sygus_to_builtin[unres_t] = types[i].toType(); - } - for( unsigned i=0; i cnames; - std::vector > cargs; - Type unres_t = unres_types[i]; - //add variables - for( unsigned j=0; j() ); - } - } - //add constants - std::vector< Node > consts; - mkSygusConstantsForType( types[i], consts ); - std::map< TypeNode, std::vector< Node > >::iterator itec = extra_cons.find( types[i] ); - if( itec!=extra_cons.end() ){ - //consts.insert( consts.end(), itec->second.begin(), itec->second.end() ); - for( unsigned j=0; jsecond.size(); j++ ){ - if( std::find( consts.begin(), consts.end(), itec->second[j] )==consts.end() ){ - consts.push_back( itec->second[j] ); - } - } - } - for( unsigned j=0; j() ); - } - //ITE - CVC4::Kind k = kind::ITE; - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); - cnames.push_back( kind::kindToString(k) ); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_bt); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - - if( types[i].isInteger() ){ - for( unsigned j=0; j<2; j++ ){ - CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS; - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); - cnames.push_back(kind::kindToString(k)); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - } - }else if( types[i].isDatatype() ){ - Trace("sygus-grammar-def") << "...add for constructors" << std::endl; - const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); - for( unsigned k=0; k() ); - for( unsigned j=0; j() ); - //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() ); - cargs.back().push_back( type_to_unres[arg_type] ); - } - } - Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl; - datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true ); - for( unsigned j=0; jbooleanType(); - datatypes.push_back(Datatype(dbname)); - ops.push_back(std::vector()); - std::vector cnames; - std::vector > cargs; - Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl; - //add variables - for( unsigned i=0; i() ); - } - } - //add constants if no variables and no connected types - if( ops.back().empty() && types.empty() ){ - std::vector< Node > consts; - mkSygusConstantsForType( btype, consts ); - for( unsigned j=0; j() ); - } - } - //add operators - for( unsigned i=0; i<3; i++ ){ - CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR ); - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); - cnames.push_back(kind::kindToString(k)); - cargs.push_back( std::vector< CVC4::Type >() ); - if( k==kind::NOT ){ - cargs.back().push_back(unres_bt); - }else if( k==kind::AND || k==kind::OR ){ - cargs.back().push_back(unres_bt); - cargs.back().push_back(unres_bt); - } - } - //add predicates for types - for( unsigned i=0; ioperatorOf(k).toExpr()); - std::stringstream ss; - ss << kind::kindToString(k) << "_" << types[i]; - cnames.push_back(ss.str()); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - //type specific predicates - if( types[i].isInteger() ){ - CVC4::Kind k = kind::LEQ; - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); - cnames.push_back(kind::kindToString(k)); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - }else if( types[i].isDatatype() ){ - //add for testers - Trace("sygus-grammar-def") << "...add for testers" << std::endl; - const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); - for( unsigned k=0; k() ); - cargs.back().push_back(unres_types[i]); - } - } - } - if( range==btype ){ - startIndex = datatypes.size()-1; - } - Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl; - datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true ); - for( unsigned j=0; j0 ){ - CVC4::Datatype tmp_dt = datatypes[0]; - datatypes[0] = datatypes[startIndex]; - datatypes[startIndex] = tmp_dt; - } -} - - -TypeNode TermDbSygus::mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, - std::map< TypeNode, std::vector< Node > >& extra_cons ) { - Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl; - for( std::map< TypeNode, std::vector< Node > >::iterator it = extra_cons.begin(); it != extra_cons.end(); ++it ){ - Trace("sygus-grammar-def") << " ...using " << it->second.size() << " extra constants for " << it->first << std::endl; - } - std::set unres; - std::vector< CVC4::Datatype > datatypes; - mkSygusDefaultGrammar( range, bvl, fun, extra_cons, datatypes, unres ); - Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl; - Assert( !datatypes.empty() ); - std::vector types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres); - Assert( types.size()==datatypes.size() ); - return TypeNode::fromType( types[0] ); -} - -TypeNode TermDbSygus::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, - const std::string& fun, unsigned& tcount ) { - if( templ==templ_arg ){ - //Assert( templ_arg.getType()==sygusToBuiltinType( templ_arg_sygus_type ) ); - return templ_arg_sygus_type; - }else{ - tcount++; - std::set unres; - std::vector< CVC4::Datatype > datatypes; - std::stringstream ssd; - ssd << fun << "_templ_" << tcount; - std::string dbname = ssd.str(); - datatypes.push_back(Datatype(dbname)); - Node op; - std::vector< Type > argTypes; - if( templ.getNumChildren()==0 ){ - // TODO : can short circuit to this case when !TermDb::containsTerm( templ, templ_arg ) - op = templ; - }else{ - Assert( templ.hasOperator() ); - op = templ.getOperator(); - // make constructor taking arguments types from children - for( unsigned i=0; i types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres); - Assert( types.size()==1 ); - return TypeNode::fromType( types[0] ); - } -} - -TypeNode TermDbSygus::mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, - const std::string& fun ) { - unsigned tcount = 0; - return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount ); -} - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index 0ddfbaa75..8f55f55bd 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -295,39 +295,6 @@ private: Node extendedRewritePullIte( Node n ); public: Node extendedRewrite( Node n ); - -// for grammar construction -private: - // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) - TypeNode mkUnresolvedType(const std::string& name, std::set& unres); - // make the builtin constants for type type that should be included in a sygus grammar - void mkSygusConstantsForType( TypeNode type, std::vector& ops ); - // collect the list of types that depend on type range - void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); - // helper function for function mkSygusDefaultGrammar below - // collects a set of mutually recursive datatypes "datatypes" corresponding to encoding type "range" to SyGuS - // unres is used for the resulting call to mkMutualDatatypeTypes - void mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, - std::vector< CVC4::Datatype >& datatypes, std::set& unres ); - // helper function for mkSygusTemplateType - TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, - const std::string& fun, unsigned& tcount ); -public: - // make the default sygus datatype type corresponding to builtin type range - // bvl is the set of free variables to include in the grammar - // fun is for naming - // extra_cons is a set of extra constant symbols to include in the grammar - TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons ); - // make the default sygus datatype type corresponding to builtin type range - TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun ){ - std::map< TypeNode, std::vector< Node > > extra_cons; - return mkSygusDefaultType( range, bvl, fun, extra_cons ); - } - // make the sygus datatype type that encodes the solution space (lambda templ_arg. templ[templ_arg]) where templ_arg - // has syntactic restrictions encoded by sygus type templ_arg_sygus_type - // bvl is the set of free variables to include in the frammar - // fun is for naming - TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun ); }; }/* CVC4::theory::quantifiers namespace */ -- 2.30.2