* Initial infrastructure for static preprocessing for sygus conjectures.
* Initial infrastructure.
* Minor change in terminology, move enumerator to synth-fun mapping to sygus term database, minor fix and add documentation to NegContainsInvarianceTest.
* Clang format
* Fixing comments, more initial infrastructure.
* More
* Minor
* New clang format.
* Address review.
theory/quantifiers/rewrite_engine.h \
theory/quantifiers/sygus_grammar_cons.cpp \
theory/quantifiers/sygus_grammar_cons.h \
+ theory/quantifiers/sygus_process_conj.cpp \
+ theory/quantifiers/sygus_process_conj.h \
theory/quantifiers/symmetry_breaking.cpp \
theory/quantifiers/symmetry_breaking.h \
theory/quantifiers/term_database.cpp \
registerSizeTerm( n, lemmas );
if( d_register_st[n] ){
d_term_to_anchor[n] = n;
- d_term_to_anchor_conj[n] = d_tds->getConjectureFor(n);
+ d_term_to_anchor_conj[n] = d_tds->getConjectureForEnumerator(n);
// this assertion fails if we have a sygus term in the search that is unmeasured
Assert(d_term_to_anchor_conj[n] != NULL);
d = 0;
Trace("sygus-sb-fair-debug") << "Tester " << exp << " is for depth " << d << " term in search size " << ssz << std::endl;
//Assert( d<=ssz );
if( options::sygusSymBreakLazy() ){
+ // dynamic symmetry breaking
addSymBreakLemmasFor( ntn, n, d, lemmas );
}
-
- // process simple symmetry breaking
+
unsigned max_depth = ssz>=d ? ssz-d : 0;
unsigned min_depth = d_simple_proc[exp];
if( min_depth<=max_depth ){
TNode x = getFreeVar( ntn );
- Node rlv = getRelevancyCondition( n );
- for( unsigned d=0; d<=max_depth; d++ ){
- Node simple_sb_pred = getSimpleSymBreakPred( ntn, tindex, d );
- if( !simple_sb_pred.isNull() ){
- simple_sb_pred = simple_sb_pred.substitute( x, n );
- if( !rlv.isNull() ){
- simple_sb_pred = NodeManager::currentNM()->mkNode( kind::OR, rlv.negate(), simple_sb_pred );
+ std::vector<Node> sb_lemmas;
+ for (unsigned ds = 0; ds <= max_depth; ds++)
+ {
+ // static conjecture-independent symmetry breaking
+ Node ipred = getSimpleSymBreakPred(ntn, tindex, ds);
+ if (!ipred.isNull())
+ {
+ sb_lemmas.push_back(ipred);
+ }
+ // static conjecture-dependent symmetry breaking
+ std::map<Node, quantifiers::CegConjecture*>::iterator itc =
+ d_term_to_anchor_conj.find(n);
+ if (itc != d_term_to_anchor_conj.end())
+ {
+ quantifiers::CegConjecture* conj = itc->second;
+ Assert(conj != NULL);
+ Node dpred = conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds);
+ if (!dpred.isNull())
+ {
+ sb_lemmas.push_back(dpred);
}
- lemmas.push_back( simple_sb_pred );
}
}
+
+ // add the above symmetry breaking predicates to lemmas
+ Node rlv = getRelevancyCondition(n);
+ for (unsigned i = 0; i < sb_lemmas.size(); i++)
+ {
+ Node pred = sb_lemmas[i].substitute(x, n);
+ if (!rlv.isNull())
+ {
+ pred = NodeManager::currentNM()->mkNode(kind::OR, rlv.negate(), pred);
+ }
+ lemmas.push_back(pred);
+ }
}
d_simple_proc[exp] = max_depth + 1;
-
- // add back testers for the children if they exist
+
+ // now activate the children those testers were previously asserted in this
+ // context and are awaiting activation, if they exist.
if( options::sygusSymBreakLazy() ){
for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( ntn.toType(), j ) ), n );
if( e.getType().isDatatype() ){
const Datatype& dt = ((DatatypeType)(e.getType()).toType()).getDatatype();
if( dt.isSygus() ){
- if (d_tds->isMeasuredTerm(e)) {
+ if (d_tds->isEnumerator(e))
+ {
d_register_st[e] = true;
- Node ag = d_tds->getActiveGuardForMeasureTerm( e );
+ Node ag = d_tds->getActiveGuardForEnumerator(e);
if( !ag.isNull() ){
d_anchor_to_active_guard[e] = ag;
}
Trace("sygus-sb-debug2") << "get search size for anchor : " << a << std::endl;
std::map< Node, Node >::iterator it = d_anchor_to_measure_term.find( a );
Assert( it!=d_anchor_to_measure_term.end() );
- return getSearchSizeForMeasureTerm( it->second );
+ return getSearchSizeForMeasureTerm(it->second);
}
-unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm( Node m ) {
+unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m)
+{
Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl;
std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m );
Assert( its!=d_szinfo.end() );
}
//register any measured terms that we haven't encountered yet (should only be invoked on first call to check
std::vector< Node > mts;
- d_tds->getMeasuredTerms( mts );
+ d_tds->getEnumerators(mts);
for( unsigned i=0; i<mts.size(); i++ ){
registerSizeTerm( mts[i], lemmas );
}
void registerMeasureTerm( Node m );
unsigned getSearchSizeFor( Node n );
unsigned getSearchSizeForAnchor( Node n );
- unsigned getSearchSizeForMeasureTerm( Node m );
-private:
+ unsigned getSearchSizeForMeasureTerm(Node m);
+
+ private:
unsigned processSelectorChain( Node n, std::map< TypeNode, Node >& top_level,
std::map< Node, unsigned >& tdepth, std::vector< Node >& lemmas );
bool debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas );
d_refine_count = 0;
d_ceg_si = new CegConjectureSingleInv(qe, this);
d_ceg_pbe = new CegConjecturePbe(qe, this);
+ d_ceg_proc = new CegConjectureProcess(qe);
d_ceg_gc = new CegGrammarConstructor(qe);
}
CegConjecture::~CegConjecture() {
delete d_ceg_si;
delete d_ceg_pbe;
+ delete d_ceg_proc;
delete d_ceg_gc;
}
Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
d_quant = q;
+ // simplify the quantified formula based on the process utility
+ d_simp_quant = d_ceg_proc->simplify(d_quant);
+
std::map< Node, Node > templates;
std::map< Node, Node > templates_arg;
//register with single invocation if applicable
- if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){
- d_ceg_si->initialize( d_quant );
- q = d_ceg_si->getSimplifiedConjecture();
+ if (d_qe->getQuantAttributes()->isSygus(q))
+ {
+ d_ceg_si->initialize(d_simp_quant);
+ d_simp_quant = d_ceg_si->getSimplifiedConjecture();
// carry the templates
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
Node v = q[0][i];
}
// convert to deep embedding and finalize single invocation here
- d_embed_quant = d_ceg_gc->process( q, templates, templates_arg );
+ d_embed_quant = d_ceg_gc->process(d_simp_quant, 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->getQuantAttributes()->isSygus( d_quant ) ){
+ if (d_qe->getQuantAttributes()->isSygus(q))
+ {
d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted(), d_ceg_gc->hasSyntaxITE() );
}
Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl;
//construct base instantiation
d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( d_embed_quant, vars, d_candidates ) );
-
- // register this term with sygus database
+ Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
+
+ // register this term with sygus database and other utilities that impact
+ // the enumerative sygus search
std::vector< Node > guarded_lemmas;
if( !isSingleInvocation() ){
+ d_ceg_proc->initialize(d_base_inst, d_candidates);
if( options::sygusPbe() ){
- d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas );
+ d_ceg_pbe->initialize(d_base_inst, d_candidates, guarded_lemmas);
} else {
for (unsigned i = 0; i < d_candidates.size(); i++) {
Node e = d_candidates[i];
- d_qe->getTermDatabaseSygus()->registerMeasuredTerm(e, this);
+ d_qe->getTermDatabaseSygus()->registerEnumerator(e, e, this);
}
}
}
-
- Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
- if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){
+
+ if (d_qe->getQuantAttributes()->isSygus(q))
+ {
collectDisjuncts( d_base_inst, d_base_disj );
Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
//store the inner variables for each disjunct
}
}
d_syntax_guided = true;
- }else if( d_qe->getQuantAttributes()->isSynthesis( d_quant ) ){
+ }
+ else if (d_qe->getQuantAttributes()->isSynthesis(q))
+ {
d_syntax_guided = false;
}else{
Assert( false );
}
}
+Node CegConjecture::getSymmetryBreakingPredicate(
+ Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
+{
+ std::vector<Node> sb_lemmas;
+
+ // based on simple preprocessing
+ Node ppred =
+ d_ceg_proc->getSymmetryBreakingPredicate(x, e, tn, tindex, depth);
+ if (!ppred.isNull())
+ {
+ sb_lemmas.push_back(ppred);
+ }
+
+ // other static conjecture-dependent symmetry breaking goes here
+
+ if (!sb_lemmas.empty())
+ {
+ return sb_lemmas.size() == 1
+ ? sb_lemmas[0]
+ : NodeManager::currentNM()->mkNode(kind::AND, sb_lemmas);
+ }
+ else
+ {
+ return Node::null();
+ }
+}
+
}/* namespace CVC4::theory::quantifiers */
}/* namespace CVC4::theory */
}/* namespace CVC4 */
#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
-#include "theory/quantifiers/ce_guided_single_inv.h"
#include "theory/quantifiers/ce_guided_pbe.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
#include "theory/quantifiers/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus_process_conj.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
* This class implements approaches for a synthesis conecjture, given by data
* member d_quant.
* This includes both approaches for synthesis in Reynolds et al CAV 2015. It
- * determines
- * which approach and optimizations are applicable to the conjecture, and has
- * interfaces for
- * implementing them.
+ * determines which approach and optimizations are applicable to the
+ * conjecture, and has interfaces for implementing them.
*/
class CegConjecture {
public:
Node getEmbeddedConjecture() { return d_embed_quant; }
/** get next decision request */
Node getNextDecisionRequest( unsigned& priority );
- /** increment the number of times we have successfully done candidate refinement */
+
+ //-------------------------------for counterexample-guided check/refine
+ /** increment the number of times we have successfully done candidate
+ * refinement */
void incrementRefineCount() { d_refine_count++; }
/** whether the conjecture is waiting for a call to doCheck below */
bool needsCheck( std::vector< Node >& lem );
/** Print the synthesis solution
* singleInvocation is whether the solution was found by single invocation techniques.
*/
+ //-------------------------------end for counterexample-guided check/refine
+
void printSynthSolution( std::ostream& out, bool singleInvocation );
/** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */
Node getGuard();
void getModelValues( std::vector< Node >& n, std::vector< Node >& v );
/** get model value for term n */
Node getModelValue( Node n );
+
+ //-----------------------------------refinement lemmas
/** get number of refinement lemmas we have added so far */
unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
/** get refinement lemma */
Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
/** get refinement lemma */
Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; }
+ //-----------------------------------end refinement lemmas
+
/** get program by examples utility */
CegConjecturePbe* getPbe() { return d_ceg_pbe; }
+ /** get the symmetry breaking predicate for type */
+ Node getSymmetryBreakingPredicate(
+ Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
/** print out debug information about this conjecture */
void debugPrint( const char * c );
private:
CegConjectureSingleInv * d_ceg_si;
/** program by examples utility */
CegConjecturePbe * d_ceg_pbe;
+ /** utility for static preprocessing and analysis of conjectures */
+ CegConjectureProcess* d_ceg_proc;
/** grammar utility */
CegGrammarConstructor * d_ceg_gc;
- /** list of constants for quantified formula */
+ /** list of constants for quantified formula
+ * The Skolems for the negation of d_embed_quant.
+ */
std::vector< Node > d_candidates;
- /** base instantiation */
+ /** base instantiation
+ * If d_embed_quant is forall d. exists y. P( d, y ), then
+ * this is the formula P( candidates, y ).
+ */
Node d_base_inst;
/** expand base inst to disjuncts */
std::vector< Node > d_base_disj;
std::vector< std::vector< Node > > d_inner_vars_disj;
/** current extential quantifeirs whose couterexamples we must refine */
std::vector< std::vector< Node > > d_ce_sk;
+
+ //-----------------------------------refinement lemmas
/** refinement lemmas */
std::vector< Node > d_refinement_lemmas;
std::vector< Node > d_refinement_lemmas_base;
+ //-----------------------------------end refinement lemmas
+
/** quantified formula asserted */
Node d_quant;
- /** quantified formula (after processing) */
+ /** quantified formula (after simplification) */
+ Node d_simp_quant;
+ /** quantified formula (after simplification, conversion to deep embedding) */
Node d_embed_quant;
/** candidate information */
class CandidateInfo {
}
}
-void CegConjecturePbe::print_role( const char * c, unsigned r ){
+void CegConjecturePbe::print_role(const char* c, unsigned r)
+{
switch(r){
case CegConjecturePbe::enum_io:Trace(c) << "IO";break;
case CegConjecturePbe::enum_ite_condition:Trace(c) << "CONDITION";break;
}
}
-void CegConjecturePbe::print_strat( const char * c, unsigned s ){
- switch(s){
- case CegConjecturePbe::strat_ITE:Trace(c) << "ITE";break;
- case CegConjecturePbe::strat_CONCAT:Trace(c) << "CONCAT";break;
- case CegConjecturePbe::strat_ID:Trace(c) << "ID";break;
- default:Trace(c) << "strat_" << s;break;
+void CegConjecturePbe::print_strat(const char* c, unsigned s)
+{
+ switch (s)
+ {
+ case CegConjecturePbe::strat_ITE: Trace(c) << "ITE"; break;
+ case CegConjecturePbe::strat_CONCAT: Trace(c) << "CONCAT"; break;
+ case CegConjecturePbe::strat_ID: Trace(c) << "ID"; break;
+ default: Trace(c) << "strat_" << s; break;
}
}
}
}
-void CegConjecturePbe::initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas ) {
+void CegConjecturePbe::initialize(Node n,
+ std::vector<Node>& candidates,
+ std::vector<Node>& lemmas)
+{
Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
for( unsigned i=0; i<candidates.size(); i++ ){
if( !d_is_pbe ){
Trace("sygus-unif") << "Do not do PBE optimizations, register..." << std::endl;
for( unsigned i=0; i<candidates.size(); i++ ){
- d_qe->getTermDatabaseSygus()->registerMeasuredTerm(candidates[i],
- d_parent);
+ d_qe->getTermDatabaseSygus()->registerEnumerator(
+ candidates[i], candidates[i], d_parent);
}
}
}
Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b,
CegConjecturePbe* cpbe,
unsigned index, unsigned ntotal) {
- Assert(cpbe->getNumExamples(e) == ntotal);
if (index == ntotal) {
// lazy child holds the leaf data
if (d_lazy_child.isNull()) {
bool CegConjecturePbe::hasExamples(Node e) {
if (isPbe()) {
- e = getSynthFunctionForEnumerator(e);
+ e = d_tds->getSynthFunForEnumerator(e);
+ Assert(!e.isNull());
std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
if (itx == d_examples_invalid.end()) {
return d_examples.find(e) != d_examples.end();
}
unsigned CegConjecturePbe::getNumExamples(Node e) {
- e = getSynthFunctionForEnumerator(e);
+ e = d_tds->getSynthFunForEnumerator(e);
+ Assert(!e.isNull());
std::map<Node, std::vector<std::vector<Node> > >::iterator it =
d_examples.find(e);
if (it != d_examples.end()) {
}
void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) {
- e = getSynthFunctionForEnumerator(e);
+ e = d_tds->getSynthFunForEnumerator(e);
+ Assert(!e.isNull());
std::map<Node, std::vector<std::vector<Node> > >::iterator it =
d_examples.find(e);
if (it != d_examples.end()) {
}
Node CegConjecturePbe::getExampleOut(Node e, unsigned i) {
- e = getSynthFunctionForEnumerator(e);
+ e = d_tds->getSynthFunForEnumerator(e);
+ Assert(!e.isNull());
std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
if (it != d_examples_out.end()) {
Assert(i < it->second.size());
Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) {
Assert(isPbe());
Assert(!e.isNull());
- e = getSynthFunctionForEnumerator(e);
+ e = d_tds->getSynthFunForEnumerator(e);
+ Assert(!e.isNull());
std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
if (itx == d_examples_invalid.end()) {
unsigned nex = d_examples[e].size();
Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
unsigned i) {
- e = getSynthFunctionForEnumerator(e);
+ e = d_tds->getSynthFunForEnumerator(e);
+ Assert(!e.isNull());
std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
if (itx == d_examples_invalid.end()) {
std::map<Node, std::vector<std::vector<Node> > >::iterator it =
return Rewriter::rewrite(bn);
}
-Node CegConjecturePbe::getSynthFunctionForEnumerator(Node e) {
- std::map<Node, Node>::const_iterator it = d_enum_to_candidate.find(e);
- if (it != d_enum_to_candidate.end()) {
- return it->second;
- } else {
- return e;
- }
-}
-
// ----------------------------- establishing enumeration types
Trace("sygus-unif-debug") << ", role = ";
print_role( "sygus-unif-debug", enum_role );
Trace("sygus-unif-debug") << ", in search = " << inSearch << std::endl;
- d_einfo[et].initialize( c, enum_role );
+ d_einfo[et].initialize(c, enum_role);
// if we are actually enumerating this (could be a compound node in the strategy)
if( inSearch ){
std::map< TypeNode, Node >::iterator itn = d_cinfo[c].d_search_enum.find( tn );
d_cinfo[c].d_esym_list.push_back( et );
d_einfo[et].d_enum_slave.push_back( et );
//register measured term with database
- d_enum_to_candidate[et] = c;
- d_qe->getTermDatabaseSygus()->registerMeasuredTerm(et, d_parent, true);
- d_einfo[et].d_active_guard = d_qe->getTermDatabaseSygus()->getActiveGuardForMeasureTerm( et );
+ d_qe->getTermDatabaseSygus()->registerEnumerator(et, c, d_parent, true);
+ d_einfo[et].d_active_guard =
+ d_qe->getTermDatabaseSygus()->getActiveGuardForEnumerator(et);
}else{
Trace("sygus-unif-debug") << "Make " << et << " a slave of " << itn->second << std::endl;
d_einfo[itn->second].d_enum_slave.push_back( et );
std::map< Node, std::map< unsigned, Node > > cop_to_child_templ_arg;
std::map< Node, unsigned > cop_to_strat;
std::map< Node, unsigned > cop_to_cindex;
-
- // look at builtin operartors first (when r=0), then defined operators (when r=1)
+
+ // look at builtin operartors first (when r=0), then defined operators
+ // (when r=1)
for( unsigned r=0; r<2; r++ ){
for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
Node cop = Node::fromExpr( dt[j].getConstructor() );
}
}
if( cop_to_strat.find( cop )!=cop_to_strat.end() ){
- Trace("sygus-unif") << "...type " << dt.getName() << " has strategy ";
- print_strat("sygus-unif",cop_to_strat[cop]);
+ Trace("sygus-unif") << "...type " << dt.getName()
+ << " has strategy ";
+ print_strat("sygus-unif", cop_to_strat[cop]);
Trace("sygus-unif") << "..." << std::endl;
// add child types
for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
cop_to_strat[cop] = strat_ITE;
}
}else if( eut.getKind()==kind::STRING_CONCAT ){
- if( dt[j].getNumArgs()>=eut.getNumChildren() && eut.getNumChildren()==2 ){
+ if (dt[j].getNumArgs() >= eut.getNumChildren()
+ && eut.getNumChildren() == 2)
+ {
cop_to_strat[cop] = strat_CONCAT;
}
}else if( eut.getKind()==kind::APPLY_UF ){
}
if( cop_to_strat.find( cop )!=cop_to_strat.end() ){
Trace("sygus-unif") << "...type " << dt.getName() << " has defined constructor matching strategy ";
- print_strat("sygus-unif",cop_to_strat[cop]);
+ print_strat("sygus-unif", cop_to_strat[cop]);
Trace("sygus-unif") << "..." << std::endl;
for( unsigned k=0; k<eut.getNumChildren(); k++ ){
Assert( templ_injection.find( k )!=templ_injection.end() );
Trace("sygus-unif-debug") << std::endl;
Assert( !et.isNull() );
d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.push_back( et );
- // need to make this take into account template
- //Assert( et.getType()==e.getType() || d_einfo[et].getRole()!=enum_io );
}
Trace("sygus-unif") << "Initialized strategy ";
print_strat( "sygus-unif", strat );
std::map< Node, EnumInfo >::iterator itns = d_einfo.find( es );
Assert( itns!=d_einfo.end() );
Trace("sygus-unif") << " " << es << ", role = ";
- print_role( "sygus-unif", itns->second.getRole() );
+ print_role("sygus-unif", itns->second.getRole());
Trace("sygus-unif") << std::endl;
}
}
Assert( itv!=d_einfo.end() );
Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
//bool prevIsCover = false;
- if( itv->second.getRole()==enum_io ){
+ if (itv->second.getRole() == enum_io)
+ {
Trace("sygus-pbe-enum") << " IO-Eval of ";
//prevIsCover = itv->second.isFeasible();
}else{
Assert( res.isConst() );
}
Node resb;
- if( itv->second.getRole()==enum_io ){
+ if (itv->second.getRole() == enum_io)
+ {
Node out = itxo->second[j];
Assert( out.isConst() );
resb = res==out ? d_true : d_false;
}
}
bool keep = false;
- if( itv->second.getRole()==enum_io ){
+ if (itv->second.getRole() == enum_io)
+ {
if( cond_vals.find( d_true )!=cond_vals.end() || cond_vals.empty() ){ // latter is the degenerate case of no examples
//check subsumbed/subsuming
std::vector< Node > subsume;
if( Trace.isOn("sygus-pbe-enum") ){
if( itv->second.getRole()==enum_io ){
if( !prevIsCover && itv->second.isFeasible() ){
- Trace("sygus-pbe-enum") << "...PBE : success : Evaluation of " << xs << " now covers all examples." << std::endl;
+ Trace("sygus-pbe-enum") << "...PBE : success : Evaluation of "
+ << xs << " now covers all examples." << std::endl;
}
}
}
}
}
-
-
+/** NegContainsSygusInvarianceTest
+*
+* This class is used to construct a minimal shape of a term that cannot
+* be contained in at least one output of an I/O pair.
+*
+* Say our PBE conjecture is:
+*
+* exists f.
+* f( "abc" ) = "abc abc" ^
+* f( "de" ) = "de de"
+*
+* Then, this class is used when there is a candidate solution t[x1] such that
+* either
+* contains( "abc abc", t["abc"] ) ---> false or
+* contains( "de de", t["de"] ) ---> false
+*
+* In particular it is used to determine whether certain generalizations of t[x1]
+* are still sufficient to falsify one of the above containments.
+*
+* For example:
+*
+* str.++( x1, "d" ) can be minimized to str.++( _, "d" )
+* ...since contains( "abc abc", str.++( y, "d" ) ) ---> false,
+* for any y.
+* str.replace( "de", x1, "b" ) can be minimized to str.replace( "de", x1, _ )
+* ...since contains( "abc abc", str.replace( "de", "abc", y ) ) ---> false,
+* for any y.
+*
+* It is an instance of quantifiers::SygusInvarianceTest, which
+* traverses the AST of a given term, replaces each subterm by a
+* fresh variable y and checks whether an invariance test (such as
+* the one specified by this class) holds.
+*
+*/
class NegContainsSygusInvarianceTest : public quantifiers::SygusInvarianceTest {
public:
NegContainsSygusInvarianceTest(){}
~NegContainsSygusInvarianceTest(){}
- Node d_ar;
- std::vector< Node > d_exo;
- std::vector< unsigned > d_neg_con_indices;
- quantifiers::CegConjecturePbe* d_cpbe;
-
- void init(quantifiers::CegConjecturePbe* cpbe, Node ar,
- std::vector<Node>& exo, std::vector<unsigned>& ncind) {
- if (cpbe->hasExamples(ar)) {
- Assert(cpbe->getNumExamples(ar) == exo.size());
- d_ar = ar;
+ /** initialize this invariance test
+ * cpbe is the conjecture utility.
+ * e is the enumerator which we are reasoning about (associated with a synth
+ * fun).
+ * exo is the list of outputs of the PBE conjecture.
+ * ncind is the set of possible indices of the PBE conjecture to check
+ * invariance of non-containment.
+ * For example, in the above example, when t[x1] = "ab", then this
+ * has the index 1 since contains("de de", "ab") ---> false but not
+ * the index 0 since contains("abc abc","ab") ---> true.
+ */
+ void init(quantifiers::CegConjecturePbe* cpbe,
+ Node e,
+ std::vector<Node>& exo,
+ std::vector<unsigned>& ncind)
+ {
+ if (cpbe->hasExamples(e))
+ {
+ Assert(cpbe->getNumExamples(e) == exo.size());
+ d_enum = e;
d_exo.insert( d_exo.end(), exo.begin(), exo.end() );
d_neg_con_indices.insert( d_neg_con_indices.end(), ncind.begin(), ncind.end() );
d_cpbe = cpbe;
}
}
-protected:
+
+ protected:
+ /** checks whether contains( out_i, nvn[in_i] ) --> false for some I/O pair i.
+ */
bool invariant( quantifiers::TermDbSygus * tds, Node nvn, Node x ){
- if( !d_ar.isNull() ){
+ if (!d_enum.isNull())
+ {
TypeNode tn = nvn.getType();
Node nbv = tds->sygusToBuiltin( nvn, tn );
Node nbvr = tds->extendedRewrite( nbv );
for( unsigned i=0; i<d_neg_con_indices.size(); i++ ){
unsigned ii = d_neg_con_indices[i];
Assert( ii<d_exo.size() );
- Node nbvre = d_cpbe->evaluateBuiltin(tn, nbvr, d_ar, ii);
+ Node nbvre = d_cpbe->evaluateBuiltin(tn, nbvr, d_enum, ii);
Node out = d_exo[ii];
Node cont = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, out, nbvre );
Node contr = Rewriter::rewrite( cont );
Trace("sygus-pbe-cterm") << nbv << " for any " << tds->sygusToBuiltin( x ) << " since " << std::endl;
Trace("sygus-pbe-cterm") << " PBE-cterm : for input example : ";
std::vector< Node > ex;
- d_cpbe->getExample(d_ar, ii, ex);
+ d_cpbe->getExample(d_enum, ii, ex);
for( unsigned j=0; j<ex.size(); j++ ){
Trace("sygus-pbe-cterm") << ex[j] << " ";
}
}
return false;
}
+
+ private:
+ /** The enumerator whose value we are considering in this invariance test */
+ Node d_enum;
+ /** The output examples for the enumerator */
+ std::vector<Node> d_exo;
+ /** The set of I/O pair indices i such that
+ * contains( out_i, nvn[in_i] ) ---> false
+ */
+ std::vector<unsigned> d_neg_con_indices;
+ /** reference to the PBE utility */
+ quantifiers::CegConjecturePbe* d_cpbe;
};
if( ei.d_enum_slave.size()==1 ){
// this check whether the example evaluates to something that is larger than the output
// if so, then this term is never useful when using a concatenation strategy
- if( ei.getRole()==enum_concat_term ){
+ if (ei.getRole() == enum_concat_term)
+ {
if( Trace.isOn("sygus-pbe-cterm-debug") ){
Trace("sygus-pbe-enum") << std::endl;
}
if( !cmp_indices.empty() ){
//set up the inclusion set
NegContainsSygusInvarianceTest ncset;
- ncset.init(this, c, itxo->second, cmp_indices);
+ ncset.init(this, x, itxo->second, cmp_indices);
d_tds->getExplanationFor( x, v, exp, ncset );
Trace("sygus-pbe-cterm") << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin( v ) << " due to negative containment." << std::endl;
return true;
d_enum_vals_res.push_back( results );
/*
if( getRole()==enum_io ){
- // compute
+ // compute
if( d_enum_total.empty() ){
d_enum_total = results;
}else if( !d_enum_total_true ){
std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e );
Assert( itn!=d_einfo.end() );
Node ret_dt;
- if( itn->second.getRole()==enum_any ){
+ if (itn->second.getRole() == enum_any)
+ {
indent("sygus-pbe-dt", ind);
ret_dt = constructBestSolvedTerm( itn->second.d_enum_vals, x );
Trace("sygus-pbe-dt") << "return PBE: success : use any " << d_tds->sygusToBuiltin( ret_dt ) << std::endl;
Assert( !ret_dt.isNull() );
- }else if( itn->second.getRole()==enum_io && !x.isReturnValueModified() && itn->second.isSolved() ){
+ }
+ else if (itn->second.getRole() == enum_io && !x.isReturnValueModified()
+ && itn->second.isSolved())
+ {
// this type has a complete solution
ret_dt = itn->second.getSolved();
indent("sygus-pbe-dt", ind);
// get the term enumerator for this type
bool success = true;
std::map< Node, EnumInfo >::iterator itet;
- if( itn->second.getRole()==enum_concat_term ){
+ if (itn->second.getRole() == enum_concat_term)
+ {
itet = itn;
}else{
std::map< unsigned, Node >::iterator itnt = itt->second.d_enum.find( enum_concat_term );
Trace("sygus-pbe-dt-debug") << " ...not currently string solved." << std::endl;
}
}
- }else if( itn->second.getRole()==enum_io && !x.isReturnValueModified() ){
+ }
+ else if (itn->second.getRole() == enum_io && !x.isReturnValueModified())
+ {
// it has an enumerated value that is conditionally correct under the current assumptions
std::vector< Node > subsumed_by;
itn->second.d_term_trie.getSubsumedBy( this, x.d_vals, true, subsumed_by );
Node incr_val;
int incr_type = 0;
std::map< Node, std::vector< unsigned > > incr;
-
+
// construct the child order based on heuristics
std::vector< unsigned > corder;
- std::unordered_set< unsigned > cused;
+ std::unordered_set<unsigned> cused;
if( strat==strat_CONCAT ){
for( unsigned r=0; r<2; r++ ){
// Concatenate strategy can only be applied from the endpoints.
- // This chooses the appropriate endpoint for which we stay within the same SyGuS type.
- // In other words, if we are synthesizing based on a production rule ( T -> str.++( T1, ..., Tn ) ), then we
- // prefer recursing on the 1st argument of the concat if T1 = T, and the last argument if Tn = T.
+ // This chooses the appropriate endpoint for which we stay within
+ // the same SyGuS type.
+ // In other words, if we are synthesizing based on a production
+ // rule ( T -> str.++( T1, ..., Tn ) ), then we
+ // prefer recursing on the 1st argument of the concat if T1 = T,
+ // and the last argument if Tn = T.
unsigned sc = r==0 ? 0 : itts->second.d_cenum.size()-1;
Node ce = itts->second.d_cenum[sc];
if( ce.getType()==etn ){
// prefer simple recursion (self type)
Assert( d_einfo.find( ce )!=d_einfo.end() );
- Assert( d_einfo[ce].getRole()==enum_concat_term );
+ Assert(d_einfo[ce].getRole() == enum_concat_term);
corder.push_back( sc );
- cused.insert( sc );
+ cused.insert(sc);
break;
}
}
}
// fill remaining children for which there is no preference
- for( unsigned sc=0; sc<itts->second.d_cenum.size(); sc++ ){
- if( cused.find( sc )==cused.end() ){
+ for (unsigned sc = 0; sc < itts->second.d_cenum.size(); sc++)
+ {
+ if (cused.find(sc) == cused.end())
+ {
corder.push_back( sc );
}
}
std::map< Node, EnumInfo >::iterator itsc = d_einfo.find( ce );
Assert( itsc!=d_einfo.end() );
// ensured by the child order we set above
- Assert( itsc->second.getRole()==enum_concat_term );
+ Assert(itsc->second.getRole() == enum_concat_term);
// check if each return value is a prefix/suffix of all open examples
incr_type = sc==0 ? -1 : 1;
if( x.d_has_string_pos==0 || x.d_has_string_pos==incr_type ){
* that are in Programming-By-Examples (PBE) form.
*
* [EX#1] An example of a synthesis conjecture in PBE form is :
-* exists f. forall x.
+* exists f. forall x.
* ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 )
*
* We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8.
* (1) Infers whether the input conjecture is in PBE form or not.
* (2) Based on this information and on the syntactic restrictions, it
* devises a strategy for enumerating terms and construction solutions,
-* which is inspired by Alur et al. "Scaling Enumerative Program Synthesis
-* via Divide and Conquer" TACAS 2017. In particular, it may consider strategies
-* for constructing decision trees when the grammar permits ITEs and a
-* strategy for divide-and-conquer string synthesis when the grammar permits
-* string concatenation. This is stored in a set of data structures within
-* d_cinfo.
-* (3) It makes (possibly multiple) calls to
+* which is inspired by Alur et al. "Scaling Enumerative Program Synthesis
+* via Divide and Conquer" TACAS 2017. In particular, it may consider
+* strategies for constructing decision trees when the grammar permits ITEs
+* and a strategy for divide-and-conquer string synthesis when the grammar
+* permits string concatenation. This is stored in a set of data structures
+* within d_cinfo.
+* (3) It makes (possibly multiple) calls to
* TermDatabaseSygus::registerMeasuredTerm(...) based
* on the strategy, which inform the rest of the system to enumerate values
-* of particular types in the grammar through use of fresh variables which
+* of particular types in the grammar through use of fresh variables which
* we call "enumerators".
*
* Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...).
*
-* Notice that each enumerator is associated with a single function-to-synthesize,
+* Notice that each enumerator is associated with a single
+* function-to-synthesize,
* but a function-to-sythesize may be mapped to multiple enumerators.
* Some public functions of this class expect an enumerator as input, which we
-* map to a function-to-synthesize via getSynthFunctionForEnumerator.
+* map to a function-to-synthesize via TermDatabaseSygus::getSynthFunFor(e).
*
* An enumerator is initially "active" but may become inactive if the enumeration
-* exhausts all possible values in the datatype corresponding to syntactic restrictions
+* exhausts all possible values in the datatype corresponding to syntactic
+* restrictions
* for it. The search may continue unless all enumerators become inactive.
*
-* (4) During search, the extension of quantifier-free datatypes procedure for SyGuS
-* datatypes may ask this class whether current candidates can be discarded based on
-* inferring when two candidate solutions are equivalent up to examples.
-* For example, the candidate solutions:
-* f = \x ite( x<0, x+1, x ) and f = \x x
-* are equivalent up to examples on the above conjecture, since they have the same
-* value on the points x = 0,5,6. Hence, we need only consider one of them.
-* The interface for querying this is CegConjecturePbe::addSearchVal(...).
+* (4) During search, the extension of quantifier-free datatypes procedure for
+* SyGuS datatypes may ask this class whether current candidates can be
+* discarded based on
+* inferring when two candidate solutions are equivalent up to examples.
+* For example, the candidate solutions:
+* f = \x ite( x<0, x+1, x ) and f = \x x
+* are equivalent up to examples on the above conjecture, since they have the
+* same value on the points x = 0,5,6. Hence, we need only consider one of
+* them. The interface for querying this is
+* CegConjecturePbe::addSearchVal(...).
* For details, see Reynolds et al. SYNT 2017.
-*
-* (5) When the extension of quantifier-free datatypes procedure for SyGuS datatypes
-* terminates with a model, the parent of this class calls
-* CegConjecturePbe::getCandidateList(...), where this class returns the list of
-* active enumerators.
-* (6) The parent class subsequently calls CegConjecturePbe::constructValues(...), which
-* informs this class that new values have been enumerated for active enumerators,
-* as indicated by the current model. This call also requests that based on these
-* newly enumerated values, whether this class is now able to construct a solution
-* based on the high-level strategy (stored in d_c_info).
*
-* This class is not designed to work in incremental mode, since there is no way to
+* (5) When the extension of quantifier-free datatypes procedure for SyGuS
+* datatypes terminates with a model, the parent of this class calls
+* CegConjecturePbe::getCandidateList(...), where this class returns the list
+* of active enumerators.
+* (6) The parent class subsequently calls
+* CegConjecturePbe::constructValues(...), which
+* informs this class that new values have been enumerated for active
+* enumerators, as indicated by the current model. This call also requests
+* that based on these
+* newly enumerated values, whether this class is now able to construct a
+* solution based on the high-level strategy (stored in d_c_info).
+*
+* This class is not designed to work in incremental mode, since there is no way
+* to
* specify incremental problems in SyguS.
*
*/
class CegConjecturePbe {
-public:
- CegConjecturePbe( QuantifiersEngine * qe, CegConjecture * p );
+ public:
+ CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p);
~CegConjecturePbe();
-
- /** initialize this class */
- void initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas );
+
+ /** initialize this class
+ *
+ * n is the "base instantiation" of the deep-embedding version of
+ * the synthesis conjecture under "candidates".
+ * (see CegConjecture::d_base_inst)
+ *
+ * This function may add lemmas to the vector lemmas corresponding
+ * to initial lemmas regarding static analysis of enumerators it
+ * introduced. For example, we may say that the top-level symbol
+ * of an enumerator is not ITE if it is being used to construct
+ * return values for decision trees.
+ */
+ void initialize(Node n,
+ std::vector<Node>& candidates,
+ std::vector<Node>& lemmas);
/** get candidate list
- * Adds all active enumerators associated with functions-to-synthesize in candidates to clist.
+ * Adds all active enumerators associated with functions-to-synthesize in
+ * candidates to clist.
*/
- void getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist );
- /** construct candidates
- * (1) Indicates that the list of enumerators in "enums" currently have model values "enum_values".
- * (2) Asks whether based on these new enumerated values, we can construct a solution for
- * the functions-to-synthesize in "candidates". If so, this function returns "true" and
+ void getCandidateList(std::vector<Node>& candidates,
+ std::vector<Node>& clist);
+ /** construct candidates
+ * (1) Indicates that the list of enumerators in "enums" currently have model
+ * values "enum_values".
+ * (2) Asks whether based on these new enumerated values, we can construct a
+ * solution for
+ * the functions-to-synthesize in "candidates". If so, this function
+ * returns "true" and
* adds solutions for candidates into "candidate_values".
- * During this class, this class may add auxiliary lemmas to "lems", which the caller
- * should send on the output channel via lemma(...).
+ * During this class, this class may add auxiliary lemmas to "lems", which the
+ * caller should send on the output channel via lemma(...).
*/
- bool constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values,
- std::vector< Node >& candidates, std::vector< Node >& candidate_values,
- std::vector< Node >& lems );
+ bool constructCandidates(std::vector<Node>& enums,
+ std::vector<Node>& enum_values,
+ std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ std::vector<Node>& lems);
/** is PBE enabled for any enumerator? */
bool isPbe() { return d_is_pbe; }
- /** get candidate for enumerator */
- Node getSynthFunctionForEnumerator(Node e);
/** is the enumerator e associated with I/O example pairs? */
bool hasExamples(Node e);
/** get number of I/O example pairs for enumerator e */
void getExample(Node e, unsigned i, std::vector<Node>& ex);
/** get the output value of the i^th I/O example for enumerator e */
Node getExampleOut(Node e, unsigned i);
-
+
/** add the search val
- * This function is called by the extension of quantifier-free datatypes procedure
- * for SyGuS datatypes when we are considering a value of enumerator e of sygus
- * type tn whose analog in the signature of builtin theory is bvr.
- *
- * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) and
+ * This function is called by the extension of quantifier-free datatypes
+ * procedure for SyGuS datatypes when we are considering a value of
+ * enumerator e of sygus type tn whose analog in the signature of builtin
+ * theory is bvr.
+ *
+ * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) and
* tn is a sygus datatype that encodes a subsignature of the integers.
*
* This returns either:
- * - A SyGuS term whose analog is equivalent to bvr up to examples, in the above example,
- * it may return a term t of the form Plus( One(), x() ), such that this function was
- * previously called with t as input.
+ * - A SyGuS term whose analog is equivalent to bvr up to examples, in the
+ * above example,
+ * it may return a term t of the form Plus( One(), x() ), such that this
+ * function was previously called with t as input.
* - e, indicating that no previous terms are equivalent to e up to examples.
*/
Node addSearchVal(TypeNode tn, Node e, Node bvr);
/** evaluate builtin
- * This returns the evaluation of bn on the i^th example for the function-to-synthesis
- * associated with enumerator e. If there are not at least i examples, it returns
- * the rewritten form of bn.
- * For example, if bn = x+5, e is an enumerator for f in the above example [EX#1], then
+ * This returns the evaluation of bn on the i^th example for the
+ * function-to-synthesis
+ * associated with enumerator e. If there are not at least i examples, it
+ * returns the rewritten form of bn.
+ * For example, if bn = x+5, e is an enumerator for f in the above example
+ * [EX#1], then
* evaluateBuiltin( tn, bn, e, 0 ) = 7
* evaluateBuiltin( tn, bn, e, 1 ) = 9
* evaluateBuiltin( tn, bn, e, 2 ) = 10
*/
- Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
-private:
+ Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
+
+ private:
/** quantifiers engine associated with this class */
QuantifiersEngine* d_qe;
/** sygus term database of d_qe */
Node d_true;
Node d_false;
/** parent conjecture
- * This is the data structure that contains global information about the conjecture.
+ * This is the data structure that contains global information about the
+ * conjecture.
*/
CegConjecture* d_parent;
/** is this a PBE conjecture for any function? */
* exists f. forall x. ( x = 0 => f( x ) > 2 )
* another example is:
* exists f. forall x. ( ( x = 0 => f( x ) = 2 ) V ( x = 3 => f( x ) = 3 ) )
- * since the formula is not a conjunction (the example values are not entailed).
+ * since the formula is not a conjunction (the example values are not
+ * entailed).
* However, the domain of f in both cases is finite, which can be used for
* search space pruning.
*/
/** for each candidate variable (function-to-synthesize), output of I/O
* examples */
std::map< Node, std::vector< Node > > d_examples_out;
- /** the list of example terms
- * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
+ /** the list of example terms
+ * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
*/
std::map< Node, std::vector< Node > > d_examples_term;
- /** map from enumerators to candidate varaibles (function-to-synthesize). An
- * enumerator may not be equivalent
- * to the candidate variable it maps so in synthesis-through-unification
- * approaches (e.g. decision tree construction).
- */
- std::map<Node, Node> d_enum_to_candidate;
- /** collect the PBE examples in n
+ /** collect the PBE examples in n
* This is called on the input conjecture, and will populate the above vectors.
* hasPol/pol denote the polarity of n in the conjecture.
*/
void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol );
-
+
//--------------------------------- PBE search values
/** this class is an index of candidate solutions for PBE synthesis */
class PbeTrie {
- public:
+ public:
PbeTrie() {}
~PbeTrie() {}
Node d_lazy_child;
void clear() { d_children.clear(); }
Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe,
unsigned index, unsigned ntotal);
- private:
+
+ private:
Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex,
CegConjecturePbe* cpbe, unsigned index,
unsigned ntotal);
*/
std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
//--------------------------------- end PBE search values
-
+
// -------------------------------- decision tree learning
- //index filter
+ // index filter
class IndexFilter {
public:
IndexFilter(){}
unsigned next( unsigned i );
void clear() { d_next.clear(); }
bool isEq( std::vector< Node >& vs, Node v );
- };
+ };
// subsumption trie
class SubsumeTrie {
public:
d_term = Node::null();
d_children.clear();
}
- private:
+
+ private:
/** the term at this node */
Node d_term;
/** the children nodes of this trie */
- std::map< Node, SubsumeTrie > d_children;
+ std::map<Node, SubsumeTrie> d_children;
/** helper function for above functions */
- Node addTermInternal( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, bool spol, IndexFilter * f,
- unsigned index, int status, bool checkExistsOnly, bool checkSubsume );
+ Node addTermInternal(CegConjecturePbe* pbe,
+ Node t,
+ std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed,
+ bool spol,
+ IndexFilter* f,
+ unsigned index,
+ int status,
+ bool checkExistsOnly,
+ bool checkSubsume);
/** helper function for above functions */
- void getLeavesInternal( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f,
- unsigned index, int status );
+ void getLeavesInternal(CegConjecturePbe* pbe,
+ std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v,
+ IndexFilter* f,
+ unsigned index,
+ int status);
};
// -------------------------------- end decision tree learning
-
+
//------------------------------ representation of a enumeration strategy
-
+
/** roles for enumerators */
enum {
enum_io,
enum_any,
};
/** print the role with Trace c. */
- static void print_role( const char * c, unsigned r );
+ static void print_role(const char* c, unsigned r);
/** strategies for SyGuS datatype types */
- enum {
+ enum
+ {
strat_ITE,
strat_CONCAT,
strat_ID,
- };
+ };
/** print the strategy with Trace c. */
- static void print_strat( const char * c, unsigned s );
-
+ static void print_strat(const char* c, unsigned s);
+
/** information about an enumerator */
class EnumInfo {
public:
EnumInfo() : d_role( enum_io ){}
- /** initialize this class
- * c is the parent function-to-synthesize
+ /** initialize this class
+ * c is the parent function-to-synthesize
* role is the "role" the enumerator plays in the high-level strategy,
* which is one of enum_* above.
*/
- void initialize( Node c, unsigned role ){
+ void initialize(Node c, unsigned role)
+ {
d_parent_candidate = c;
d_role = role;
}
bool isTemplated() { return !d_template.isNull(); }
- void addEnumValue( CegConjecturePbe * pbe, Node v, std::vector< Node >& results );
- void setSolved( Node slv );
+ void addEnumValue(CegConjecturePbe* pbe,
+ Node v,
+ std::vector<Node>& results);
+ void setSolved(Node slv);
bool isSolved() { return !d_enum_solved.isNull(); }
Node getSolved() { return d_enum_solved; }
unsigned getRole() { return d_role; }
-
Node d_parent_candidate;
// for template
Node d_template;
std::vector< Node > d_enum_subsume;
std::map< Node, unsigned > d_enum_val_to_index;
SubsumeTrie d_term_trie;
- private:
- /** whether an enumerated value for this conjecture has solved the entire conjecture */
+
+ private:
+ /** whether an enumerated value for this conjecture has solved the entire
+ * conjecture */
Node d_enum_solved;
/** the role of this enumerator (one of enum_* above). */
unsigned d_role;
};
/** maps enumerators to the information above */
std::map< Node, EnumInfo > d_einfo;
-
-
+
class CandidateInfo;
/** represents a strategy for a SyGuS datatype type */
class EnumTypeInfoStrat {
std::vector< TypeNode > d_csol_cts;
std::vector< Node > d_cenum;
};
-
-
+
/** stores enumerators and strategies for a SyGuS datatype type */
class EnumTypeInfo {
public:
std::map< Node, EnumTypeInfoStrat > d_strat;
bool isSolved( CegConjecturePbe * pbe );
};
-
-
- /** stores strategy and enumeration information for a function-to-synthesize */
+
+ /** stores strategy and enumeration information for a function-to-synthesize
+ */
class CandidateInfo {
public:
CandidateInfo() : d_check_sol( false ), d_cond_count( 0 ){}
* of solutions.
*/
TypeNode d_root;
- /** Information for each SyGuS datatype type occurring in a field of d_root */
+ /** Information for each SyGuS datatype type occurring in a field of d_root
+ */
std::map< TypeNode, EnumTypeInfo > d_tinfo;
/** list of all enumerators for the function-to-synthesize */
std::vector< Node > d_esym_list;
};
/** maps a function-to-synthesize to the above information */
std::map< Node, CandidateInfo > d_cinfo;
-
+
//------------------------------ representation of an enumeration strategy
/** add enumerated value */
void addEnumeratedValue( Node x, Node v, std::vector< Node >& lems );
bool getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp );
-
+
//------------------------------ strategy registration
- void collectEnumeratorTypes( Node c, TypeNode tn, unsigned enum_role );
- void registerEnumerator( Node et, Node c, TypeNode tn, unsigned enum_role, bool inSearch );
- void staticLearnRedundantOps( Node c, std::vector< Node >& lemmas );
- void staticLearnRedundantOps( Node c, Node e, std::map< Node, bool >& visited, std::vector< Node >& redundant,
- std::vector< Node >& lemmas, int ind );
+ void collectEnumeratorTypes(Node c, TypeNode tn, unsigned enum_role);
+ void registerEnumerator(
+ Node et, Node c, TypeNode tn, unsigned enum_role, bool inSearch);
+ void staticLearnRedundantOps(Node c, std::vector<Node>& lemmas);
+ void staticLearnRedundantOps(Node c,
+ Node e,
+ std::map<Node, bool>& visited,
+ std::vector<Node>& redundant,
+ std::vector<Node>& lemmas,
+ int ind);
/** register candidate conditional */
- bool inferTemplate( unsigned k, Node n, std::map< Node, unsigned >& templ_var_index, std::map< unsigned, unsigned >& templ_injection );
- //------------------------------ end strategy registration
-
-
+ bool inferTemplate(unsigned k,
+ Node n,
+ std::map<Node, unsigned>& templ_var_index,
+ std::map<unsigned, unsigned>& templ_injection);
+ //------------------------------ end strategy registration
+
//------------------------------ constructing solutions
class UnifContext {
public:
* in context x, where ind is the term depth of the context.
*/
Node constructSolution( Node c, Node e, UnifContext& x, int ind );
- /** Heuristically choose the best solved term from solved in context x, currently return the first. */
+ /** Heuristically choose the best solved term from solved in context x,
+ * currently return the first. */
Node constructBestSolvedTerm( std::vector< Node >& solved, UnifContext& x );
- /** Heuristically choose the best solved string term from solved in context x, currently return the first. */
+ /** Heuristically choose the best solved string term from solved in context
+ * x, currently return the first. */
Node constructBestStringSolvedTerm( std::vector< Node >& solved, UnifContext& x );
- /** heuristically choose the best solved conditional term from solved in context x, currently random */
+ /** heuristically choose the best solved conditional term from solved in
+ * context x, currently random */
Node constructBestSolvedConditional( std::vector< Node >& solved, UnifContext& x );
- /** heuristically choose the best conditional term from conds in context x, currently random */
+ /** heuristically choose the best conditional term from conds in context x,
+ * currently random */
Node constructBestConditional( std::vector< Node >& conds, UnifContext& x );
- /** heuristically choose the best string to concatenate from strs to the solution in context x, currently random
- * incr stores the vector of indices that are incremented by this solution in example outputs.
+ /** heuristically choose the best string to concatenate from strs to the
+ * solution in context x, currently random
+ * incr stores the vector of indices that are incremented by this solution in
+ * example outputs.
* total_inc[x] is the sum of incr[x] for each x in strs.
*/
Node constructBestStringToConcat( std::vector< Node > strs,
std::map< Node, std::vector< unsigned > > incr,
UnifContext& x );
//------------------------------ end constructing solutions
-
- /** get guard status
+
+ /** get guard status
* Returns 1 if g is asserted true in the SAT solver.
* Returns -1 if g is asserted false in the SAT solver.
* Returns 0 otherwise.
*/
- int getGuardStatus( Node g );
+ int getGuardStatus(Node g);
};
--- /dev/null
+/********************* */
+/*! \file sygus_process_conj.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 techniqures for static preprocessing and analysis
+ ** of sygus conjectures.
+ **/
+#include "theory/quantifiers/sygus_process_conj.h"
+
+#include <stack>
+
+#include "expr/datatype.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 {
+namespace quantifiers {
+
+CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) : d_qe(qe) {}
+CegConjectureProcess::~CegConjectureProcess() {}
+Node CegConjectureProcess::simplify(Node q)
+{
+ Trace("sygus-process") << "Simplify conjecture : " << q << std::endl;
+
+ return q;
+}
+
+void CegConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
+{
+ if (Trace.isOn("sygus-process"))
+ {
+ Trace("sygus-process") << "Process conjecture : " << n
+ << " with candidates: " << std::endl;
+ for (unsigned i = 0; i < candidates.size(); i++)
+ {
+ Trace("sygus-process") << " " << candidates[i] << std::endl;
+ }
+ }
+ Node base;
+ if (n.getKind() == NOT && n[0].getKind() == FORALL)
+ {
+ base = n[0][1];
+ }
+ else
+ {
+ base = n;
+ }
+
+ std::vector<Node> conj;
+ if (base.getKind() == AND)
+ {
+ for (unsigned i = 0; i < base.getNumChildren(); i++)
+ {
+ conj.push_back(base[i]);
+ }
+ }
+ else
+ {
+ conj.push_back(base);
+ }
+
+ // initialize the information for synth funs
+ for (unsigned i = 0; i < candidates.size(); i++)
+ {
+ Node e = candidates[i];
+ // d_sf_info[e].d_arg_independent
+ }
+
+ // process the conjunctions
+ for (unsigned i = 0; i < conj.size(); i++)
+ {
+ processConjunct(conj[i]);
+ }
+}
+
+void CegConjectureProcess::processConjunct(Node c) {}
+Node CegConjectureProcess::getSymmetryBreakingPredicate(
+ Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
+{
+ return Node::null();
+}
+
+void CegConjectureProcess::debugPrint(const char* c) {}
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
--- /dev/null
+/********************* */
+/*! \file sygus_process_conj.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 Techniqures for static preprocessing and analysis of
+ ** sygus conjectures.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PPROCESS_CONJ_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESSS_CONJ_H
+
+#include "expr/node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** This structure stores information regarding conjecture-specific
+* analysis of a function to synthesize.
+*/
+struct CegSynthFunProcessInfo
+{
+ public:
+ CegSynthFunProcessInfo() {}
+ ~CegSynthFunProcessInfo() {}
+ /** the set of arguments that this synth-fun is independent of */
+ std::map<unsigned, bool> d_arg_independent;
+};
+
+/** Ceg Conjecture Process
+*
+* This class implements static techniques for preprocessing and analysis of
+* sygus conjectures.
+*
+* It is used as a back-end to CegConjecture, which calls it using the following
+* interface:
+* (1) When a sygus conjecture is asserted, we call
+* CegConjectureProcess::simplify( q ),
+* where q is the sygus conjecture in original form.
+*
+* (2) After a sygus conjecture is simplified and converted to deep
+* embedding form, we call CegConjectureProcess::initialize( n, candidates ).
+*
+* (3) During enumerative SyGuS search, calls may be made by
+* the extension of the quantifier-free datatypes decision procedure for
+* sygus to CegConjectureProcess::getSymmetryBreakingPredicate(...), which are
+* used for pruning search space based on conjecture-specific analysis.
+*/
+class CegConjectureProcess
+{
+ public:
+ CegConjectureProcess(QuantifiersEngine* qe);
+ ~CegConjectureProcess();
+ /** simplify the synthesis conjecture q
+ * Returns a formula that is equivalent to q.
+ */
+ Node simplify(Node q);
+ /** initialize
+ *
+ * n is the "base instantiation" of the deep-embedding version of
+ * the synthesis conjecture under "candidates".
+ * (see CegConjecture::d_base_inst)
+ */
+ void initialize(Node n, std::vector<Node>& candidates);
+ /** get symmetry breaking predicate
+ *
+ * Returns a formula that restricts the enumerative search space (for a given
+ * depth) for a term x of sygus type tn whose top symbol is the tindex^{th}
+ * constructor, where x is a subterm of enumerator e.
+ */
+ Node getSymmetryBreakingPredicate(
+ Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
+ /** print out debug information about this conjecture */
+ void debugPrint(const char* c);
+
+ private:
+ /** process conjunct */
+ void processConjunct(Node c);
+ /** for each synth-fun, information that is specific to this conjecture */
+ std::map<Node, CegSynthFunProcessInfo> d_sf_info;
+ /** reference to quantifier engine */
+ QuantifiersEngine* d_qe;
+};
+
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
+
+#endif
}
}
-void TermDbSygus::registerMeasuredTerm(Node e, CegConjecture* conj,
- bool mkActiveGuard) {
+void TermDbSygus::registerEnumerator(Node e,
+ Node f,
+ CegConjecture* conj,
+ bool mkActiveGuard)
+{
Assert(d_enum_to_conjecture.find(e) == d_enum_to_conjecture.end());
Trace("sygus-db") << "Register measured term : " << e << std::endl;
d_enum_to_conjecture[e] = conj;
+ d_enum_to_synth_fun[e] = f;
if( mkActiveGuard ){
// make the guard
Node eg = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "eG", NodeManager::currentNM()->booleanType() ) );
}
}
-bool TermDbSygus::isMeasuredTerm(Node e) const {
+bool TermDbSygus::isEnumerator(Node e) const
+{
return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end();
}
-CegConjecture* TermDbSygus::getConjectureFor(Node e) {
+CegConjecture* TermDbSygus::getConjectureForEnumerator(Node e)
+{
std::map<Node, CegConjecture*>::iterator itm = d_enum_to_conjecture.find(e);
if (itm != d_enum_to_conjecture.end()) {
return itm->second;
}
}
-Node TermDbSygus::getActiveGuardForMeasureTerm( Node e ) {
+Node TermDbSygus::getSynthFunForEnumerator(Node e)
+{
+ std::map<Node, Node>::iterator itsf = d_enum_to_synth_fun.find(e);
+ if (itsf != d_enum_to_synth_fun.end())
+ {
+ return itsf->second;
+ }
+ else
+ {
+ return Node::null();
+ }
+}
+
+Node TermDbSygus::getActiveGuardForEnumerator(Node e)
+{
std::map<Node, Node>::iterator itag = d_enum_to_active_guard.find(e);
if (itag != d_enum_to_active_guard.end()) {
return itag->second;
}
}
-void TermDbSygus::getMeasuredTerms( std::vector< Node >& mts ) {
+void TermDbSygus::getEnumerators(std::vector<Node>& mts)
+{
for (std::map<Node, CegConjecture*>::iterator itm =
d_enum_to_conjecture.begin();
itm != d_enum_to_conjecture.end(); ++itm) {
private:
/** mapping from enumerator terms to the conjecture they are associated with */
std::map<Node, CegConjecture*> d_enum_to_conjecture;
+ /** mapping from enumerator terms to the function-to-synthesize they are
+ * associated with */
+ std::map<Node, Node> d_enum_to_synth_fun;
/** mapping from enumerator terms to the guard they are associated with
* The guard G for an enumerator e has the semantics
* "if G is true, then there are more values of e to enumerate".
/** register the sygus type */
void registerSygusType( TypeNode tn );
/** register a variable e that we will do enumerative search on
- * conj is the conjecture that the enumeration for e is for.
+ * conj is the conjecture that the enumeration of e is for.
+ * f is the synth-fun that the enumeration of e is for.
* mkActiveGuard is whether we want to make a active guard for e (see
* d_enum_to_active_guard)
+ *
+ * Notice that enumerator e may not be equivalent
+ * to f in synthesis-through-unification approaches
+ * (e.g. decision tree construction for PBE synthesis).
*/
- void registerMeasuredTerm(Node e, CegConjecture* conj,
- bool mkActiveGuard = false);
- /** is e a measured term (enumerator)? */
- bool isMeasuredTerm(Node e) const;
+ void registerEnumerator(Node e,
+ Node f,
+ CegConjecture* conj,
+ bool mkActiveGuard = false);
+ /** is e an enumerator? */
+ bool isEnumerator(Node e) const;
/** return the conjecture e is associated with */
- CegConjecture* getConjectureFor(Node e);
+ CegConjecture* getConjectureForEnumerator(Node e);
+ /** return the function-to-synthesize e is associated with */
+ Node getSynthFunForEnumerator(Node e);
/** get active guard for e */
- Node getActiveGuardForMeasureTerm( Node e );
- /** get all registered measure terms (enumerators) */
- void getMeasuredTerms( std::vector< Node >& mts );
-public: //general sygus utilities
+ Node getActiveGuardForEnumerator(Node e);
+ /** get all registered enumerators */
+ void getEnumerators(std::vector<Node>& mts);
+
+ public: // general sygus utilities
bool isRegistered( TypeNode tn );
// get the minimum depth of type in its parent grammar
unsigned getMinTypeDepth( TypeNode root_tn, TypeNode tn );
projects / cvc5.git / commitdiff