* Initial revision of mapping sygus enumeration terms to CegConjectures. This will allow us to generalize conjecture-specific symmetry breaking.
* Change function names, simplify.
* Fix assertion, minor optimization
* Cleanup, documentation, simplification.
* Address review.
* Apply clang format.
** Implementation of sygus utilities for theory of datatypes
**/
+#include "theory/datatypes/datatypes_sygus.h"
#include "expr/node_manager.h"
#include "options/quantifiers_options.h"
#include "theory/datatypes/datatypes_rewriter.h"
-#include "theory/datatypes/datatypes_sygus.h"
+#include "theory/datatypes/theory_datatypes.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
#include "theory/quantifiers/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/datatypes/theory_datatypes.h"
#include "theory/theory_model.h"
using namespace CVC4;
std::map< Node, Node >::iterator it = d_term_to_anchor.find( n[0] );
if( it!=d_term_to_anchor.end() ) {
d_term_to_anchor[n] = it->second;
- d_term_to_anchor_root[n] = d_term_to_anchor_root[n[0]];
+ d_term_to_anchor_conj[n] = d_term_to_anchor_conj[n[0]];
d = d_term_to_depth[n[0]] + 1;
is_top_level = computeTopLevel( tn, n[0] );
success = true;
registerSizeTerm( n, lemmas );
if( d_register_st[n] ){
d_term_to_anchor[n] = n;
- d_term_to_anchor_root[n] = d_tds->isMeasuredTerm( n );
+ d_term_to_anchor_conj[n] = d_tds->getConjectureFor(n);
// this assertion fails if we have a sygus term in the search that is unmeasured
- Assert( !d_term_to_anchor_root[n].isNull() );
+ Assert(d_term_to_anchor_conj[n] != NULL);
d = 0;
is_top_level = true;
success = true;
}
}
+/** EquivSygusInvarianceTest
+*
+* This class is used to construct a minimal shape of a term that is equivalent
+* up to rewriting to a RHS value,
+* given as input bvr.
+*
+* For example,
+*
+* ite( t>0, 0, 0 ) + s*0 ----> 0
+*
+* can be minimized to:
+*
+* ite( _, 0, 0 ) + _*0 ----> 0
+*
+* It also manages the case where the rewriting is invariant wrt a finite set of
+* examples occurring in the conjecture.
+*
+* It is an instance of quantifiers::SygusInvarianceTest which is the standard
+* interface for term generalization via
+* the TermRecBuild utility, which traverses the AST of a given term, replaces
+* each subterm by a fresh variable and
+* check whether the invariant, as specified by this class (equivalent up to
+* rewriting to a RHS) holds.
+*
+* For details, see Reynolds et al SYNT 2017.
+*/
class EquivSygusInvarianceTest : public quantifiers::SygusInvarianceTest {
public:
EquivSygusInvarianceTest(){}
~EquivSygusInvarianceTest(){}
- Node d_ex_ar;
- Node d_bvr;
- std::vector< Node > d_exo;
- void init( quantifiers::TermDbSygus * tds, TypeNode tn, Node ar, Node bvr ) {
+ /** initialize this invariance test
+ * tn is the sygus type for e
+ * aconj/e are used for conjecture-specific symmetry breaking
+ * bvr is the builtin version of the right hand side of the rewrite that we are
+ * checking for invariance
+ */
+ void init(quantifiers::TermDbSygus* tds, TypeNode tn,
+ quantifiers::CegConjecture* aconj, Node e, Node bvr) {
//compute the current examples
d_bvr = bvr;
- if( tds->hasPbeExamples( ar ) ){
- d_ex_ar = ar;
- unsigned nex = tds->getNumPbeExamples( ar );
+ if (aconj->getPbe()->hasExamples(e)) {
+ d_conj = aconj;
+ d_enum = e;
+ unsigned nex = aconj->getPbe()->getNumExamples(e);
for( unsigned i=0; i<nex; i++ ){
- d_exo.push_back( tds->evaluateBuiltin( tn, bvr, ar, i ) );
+ d_exo.push_back(d_conj->getPbe()->evaluateBuiltin(tn, bvr, e, i));
}
}
}
protected:
- bool invariant( quantifiers::TermDbSygus * tds, Node nvn, Node x ){
- TypeNode tn = nvn.getType();
- Node nbv = tds->sygusToBuiltin( nvn, tn );
- Node nbvr = tds->extendedRewrite( nbv );
- Trace("sygus-sb-mexp-debug") << " min-exp check : " << nbv << " -> " << nbvr << std::endl;
- bool exc_arg = false;
- // equivalent / singular up to normalization
- if( nbvr==d_bvr ){
- // gives the same result : then the explanation for the child is irrelevant
- exc_arg = true;
- Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin( nvn ) << " is rewritten to " << nbvr;
- Trace("sygus-sb-mexp") << " regardless of the content of " << tds->sygusToBuiltin( x ) << std::endl;
- }else{
- if( nbvr.isVar() ){
- TypeNode xtn = x.getType();
- if( xtn==tn ){
- Node bx = tds->sygusToBuiltin( x, xtn );
- Assert( bx.getType()==nbvr.getType() );
- if( nbvr==bx ){
- Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin( nvn ) << " always rewrites to argument " << nbvr << std::endl;
- // rewrites to the variable : then the explanation of this is irrelevant as well
- exc_arg = true;
- d_bvr = nbvr;
- }
- }
- }
- }
- // equivalent under examples
- if( !exc_arg ){
- if( !d_ex_ar.isNull() ){
- bool ex_equiv = true;
- for( unsigned j=0; j<d_exo.size(); j++ ){
- Node nbvr_ex = tds->evaluateBuiltin( tn, nbvr, d_ex_ar, j );
- if( nbvr_ex!=d_exo[j] ){
- ex_equiv = false;
- break;
- }
- }
- if( ex_equiv ){
- Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin( nvn );
- Trace("sygus-sb-mexp") << " is the same w.r.t. examples regardless of the content of " << tds->sygusToBuiltin( x ) << std::endl;
- exc_arg = true;
- }
- }
- }
- return exc_arg;
+ /** does nvn still rewrite to d_bvr? */
+ bool invariant(quantifiers::TermDbSygus* tds, Node nvn, Node x) {
+ TypeNode tn = nvn.getType();
+ Node nbv = tds->sygusToBuiltin(nvn, tn);
+ Node nbvr = tds->extendedRewrite(nbv);
+ Trace("sygus-sb-mexp-debug") << " min-exp check : " << nbv << " -> " << nbvr
+ << std::endl;
+ bool exc_arg = false;
+ // equivalent / singular up to normalization
+ if (nbvr == d_bvr) {
+ // gives the same result : then the explanation for the child is irrelevant
+ exc_arg = true;
+ Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
+ << " is rewritten to " << nbvr;
+ Trace("sygus-sb-mexp") << " regardless of the content of "
+ << tds->sygusToBuiltin(x) << std::endl;
+ } else {
+ if (nbvr.isVar()) {
+ TypeNode xtn = x.getType();
+ if (xtn == tn) {
+ Node bx = tds->sygusToBuiltin(x, xtn);
+ Assert(bx.getType() == nbvr.getType());
+ if (nbvr == bx) {
+ Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
+ << " always rewrites to argument " << nbvr
+ << std::endl;
+ // rewrites to the variable : then the explanation of this is
+ // irrelevant as well
+ exc_arg = true;
+ d_bvr = nbvr;
+ }
+ }
+ }
+ }
+ // equivalent under examples
+ if (!exc_arg) {
+ if (!d_enum.isNull()) {
+ bool ex_equiv = true;
+ for (unsigned j = 0; j < d_exo.size(); j++) {
+ Node nbvr_ex = d_conj->getPbe()->evaluateBuiltin(tn, nbvr, d_enum, j);
+ if (nbvr_ex != d_exo[j]) {
+ ex_equiv = false;
+ break;
+ }
+ }
+ if (ex_equiv) {
+ Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn);
+ Trace("sygus-sb-mexp")
+ << " is the same w.r.t. examples regardless of the content of "
+ << tds->sygusToBuiltin(x) << std::endl;
+ exc_arg = true;
+ }
+ }
+ }
+ return exc_arg;
}
+
+ private:
+ /** the conjecture associated with the enumerator d_enum */
+ quantifiers::CegConjecture* d_conj;
+ /** the enumerator associated with the term we are doing an invariance test
+ * for */
+ Node d_enum;
+ /** the RHS of the evaluation */
+ Node d_bvr;
+ /** the result of the examples
+ * This is a finer-grained version of d_bvr, where for example if our input
+ * examples are:
+ * (x,y,z) = (3,2,4), (5,2,6), (3,2,1)
+ * On these examples, we have:
+ *
+ * ite( x>y, z, 0) ---> 4,6,1
+ *
+ * which can be minimized to:
+ *
+ * ite( x>y, z, _) ---> 4,6,1
+ */
+ std::vector<Node> d_exo;
};
if( d_cache[a].d_search_val_proc.find( nv )==d_cache[a].d_search_val_proc.end() ){
d_cache[a].d_search_val_proc[nv] = true;
// get the root (for PBE symmetry breaking)
- Assert( d_term_to_anchor_root.find( a )!=d_term_to_anchor_root.end() );
- Node ar = d_term_to_anchor_root[a];
- Assert( !ar.isNull() );
+ Assert(d_term_to_anchor_conj.find(a) != d_term_to_anchor_conj.end());
+ quantifiers::CegConjecture* aconj = d_term_to_anchor_conj[a];
+ Assert(aconj != NULL);
Trace("sygus-sb-debug") << " ...register search value " << nv << ", type=" << tn << std::endl;
Node bv = d_tds->sygusToBuiltin( nv, tn );
Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl;
Node bad_val_bvr;
bool by_examples = false;
if( itsv==d_cache[a].d_search_val[tn].end() ){
+ // TODO (github #1210) conjecture-specific symmetry breaking
+ // this should be generalized and encapsulated within the CegConjecture
+ // class
// is it equivalent under examples?
- Node bvr_equiv = d_tds->addPbeSearchVal( tn, ar, bvr );
+ Node bvr_equiv;
+ if (aconj->getPbe()->hasExamples(a)) {
+ bvr_equiv = aconj->getPbe()->addSearchVal(tn, a, bvr);
+ }
if( !bvr_equiv.isNull() ){
if( bvr_equiv!=bvr ){
Trace("sygus-sb-debug") << "......adding search val for " << bvr << " returned " << bvr_equiv << std::endl;
// do analysis of the evaluation FIXME: does not work (evaluation is non-constant)
EquivSygusInvarianceTest eset;
- eset.init( d_tds, tn, ar, bvr );
+ eset.init(d_tds, tn, aconj, a, bvr);
Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl;
d_tds->getExplanationFor( x, bad_val, exp, eset, bad_val_o, sz );
do_exclude = true;
if( e.getType().isDatatype() ){
const Datatype& dt = ((DatatypeType)(e.getType()).toType()).getDatatype();
if( dt.isSygus() ){
- if( !d_tds->isMeasuredTerm( e ).isNull() ){
+ if (d_tds->isMeasuredTerm(e)) {
d_register_st[e] = true;
Node ag = d_tds->getActiveGuardForMeasureTerm( e );
if( !ag.isNull() ){
#include <iostream>
#include <map>
-#include "expr/node.h"
-#include "expr/datatype.h"
-#include "context/context.h"
#include "context/cdchunk_list.h"
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdo.h"
+#include "context/context.h"
+#include "expr/datatype.h"
+#include "expr/node.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
#include "theory/quantifiers/term_database.h"
namespace CVC4 {
Node d_zero;
private:
std::map< Node, Node > d_term_to_anchor;
- std::map< Node, Node > d_term_to_anchor_root;
+ std::map<Node, quantifiers::CegConjecture*> d_term_to_anchor_conj;
std::map< Node, unsigned > d_term_to_depth;
std::map< Node, bool > d_is_top_level;
void registerTerm( Node n, std::vector< Node >& lemmas );
if( !isSingleInvocation() ){
if( options::sygusPbe() ){
d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas );
- }
- for( unsigned i=0; i<d_candidates.size(); i++ ){
- Node e = d_candidates[i];
- if( options::sygusPbe() ){
- std::vector< std::vector< Node > > exs;
- std::vector< Node > exos;
- std::vector< Node > exts;
- // 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 );
- }
- }else{
- d_qe->getTermDatabaseSygus()->registerMeasuredTerm( e, e );
+ } else {
+ for (unsigned i = 0; i < d_candidates.size(); i++) {
+ Node e = d_candidates[i];
+ d_qe->getTermDatabaseSygus()->registerMeasuredTerm(e, this);
}
}
}
namespace theory {
namespace quantifiers {
-/** a synthesis conjecture */
+/** a synthesis conjecture
+ * 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.
+ */
class CegConjecture {
public:
CegConjecture( QuantifiersEngine * qe );
Node getNextDecisionRequest( unsigned& priority );
/** 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 do_Check below */
+ /** whether the conjecture is waiting for a call to doCheck below */
bool needsCheck( std::vector< Node >& lem );
/** whether the conjecture is waiting for a call to doRefine below */
bool needsRefinement();
Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
/** get refinement lemma */
Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; }
+ /** get program by examples utility */
+ CegConjecturePbe* getPbe() { return d_ceg_pbe; }
/** print out debug information about this conjecture */
void debugPrint( const char * c );
private:
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], candidates[i] );
+ d_qe->getTermDatabaseSygus()->registerMeasuredTerm(candidates[i],
+ d_parent);
}
}
}
-bool CegConjecturePbe::getPbeExamples( Node v, std::vector< std::vector< Node > >& exs,
- std::vector< Node >& exos, std::vector< Node >& exts ) {
- std::map< Node, bool >::iterator itx = d_examples_invalid.find( v );
- if( itx==d_examples_invalid.end() ){
- Assert( d_examples.find( v )!=d_examples.end() );
- exs = d_examples[v];
- Assert( d_examples_out.find( v )!=d_examples_out.end() );
- exos = d_examples_out[v];
- Assert( d_examples_term.find( v )!=d_examples_term.end() );
- exts = d_examples_term[v];
- return true;
+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()) {
+ d_lazy_child = b;
+ }
+ return d_lazy_child;
+ } else {
+ std::vector<Node> ex;
+ if (d_children.empty()) {
+ if (d_lazy_child.isNull()) {
+ d_lazy_child = b;
+ return d_lazy_child;
+ } else {
+ // evaluate the lazy child
+ Assert(cpbe->d_examples.find(e) != cpbe->d_examples.end());
+ Assert(index < cpbe->d_examples[e].size());
+ ex = cpbe->d_examples[e][index];
+ addPbeExampleEval(etn, e, d_lazy_child, ex, cpbe, index, ntotal);
+ Assert(!d_children.empty());
+ d_lazy_child = Node::null();
+ }
+ } else {
+ Assert(cpbe->d_examples.find(e) != cpbe->d_examples.end());
+ Assert(index < cpbe->d_examples[e].size());
+ ex = cpbe->d_examples[e][index];
+ }
+ return addPbeExampleEval(etn, e, b, ex, cpbe, index, ntotal);
+ }
+}
+
+Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b,
+ std::vector<Node>& ex,
+ CegConjecturePbe* cpbe,
+ unsigned index,
+ unsigned ntotal) {
+ Node eb = cpbe->d_tds->evaluateBuiltin(etn, b, ex);
+ return d_children[eb].addPbeExample(etn, e, b, cpbe, index + 1, ntotal);
+}
+
+bool CegConjecturePbe::hasExamples(Node e) {
+ if (isPbe()) {
+ e = getCandidateForEnumerator(e);
+ 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();
+ }
}
return false;
}
+unsigned CegConjecturePbe::getNumExamples(Node e) {
+ e = getCandidateForEnumerator(e);
+ std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+ d_examples.find(e);
+ if (it != d_examples.end()) {
+ return it->second.size();
+ } else {
+ return 0;
+ }
+}
+
+void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) {
+ e = getCandidateForEnumerator(e);
+ std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+ d_examples.find(e);
+ if (it != d_examples.end()) {
+ Assert(i < it->second.size());
+ ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
+ } else {
+ Assert(false);
+ }
+}
+
+Node CegConjecturePbe::getExampleOut(Node e, unsigned i) {
+ e = getCandidateForEnumerator(e);
+ std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
+ if (it != d_examples_out.end()) {
+ Assert(i < it->second.size());
+ return it->second[i];
+ } else {
+ Assert(false);
+ return Node::null();
+ }
+}
+
+Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) {
+ Assert(isPbe());
+ Assert(!e.isNull());
+ e = getCandidateForEnumerator(e);
+ std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+ if (itx == d_examples_invalid.end()) {
+ unsigned nex = d_examples[e].size();
+ Node ret = d_pbe_trie[e][tn].addPbeExample(tn, e, bvr, this, 0, nex);
+ Assert(ret.getType() == bvr.getType());
+ return ret;
+ }
+ return Node::null();
+}
+
+Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e,
+ unsigned i) {
+ e = getCandidateForEnumerator(e);
+ 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 =
+ d_examples.find(e);
+ if (it != d_examples.end()) {
+ Assert(i < it->second.size());
+ return d_tds->evaluateBuiltin(tn, bn, it->second[i]);
+ }
+ }
+ return Rewriter::rewrite(bn);
+}
+
+Node CegConjecturePbe::getCandidateForEnumerator(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
d_cinfo[c].d_esym_list.push_back( et );
d_einfo[et].d_enum_slave.push_back( et );
//register measured term with database
- d_qe->getTermDatabaseSygus()->registerMeasuredTerm( et, c, true );
+ 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 );
}else{
Trace("sygus-unif-debug") << "Make " << et << " a slave of " << itn->second << std::endl;
}
}
-
// ------------------------------------------- solution construction from enumeration
void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ) {
Node d_ar;
std::vector< Node > d_exo;
std::vector< unsigned > d_neg_con_indices;
-
- void init( quantifiers::TermDbSygus * tds, Node ar, std::vector< Node >& exo, std::vector< unsigned >& ncind ) {
- if( tds->hasPbeExamples( ar ) ){
- Assert( tds->getNumPbeExamples( ar )==exo.size() );
+ 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;
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:
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 = tds->evaluateBuiltin( tn, nbvr, d_ar, ii );
+ Node nbvre = d_cpbe->evaluateBuiltin(tn, nbvr, d_ar, 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;
- tds->getPbeExample( d_ar, ii, ex );
+ d_cpbe->getExample(d_ar, ii, ex);
for( unsigned j=0; j<ex.size(); j++ ){
Trace("sygus-pbe-cterm") << ex[j] << " ";
}
if( !cmp_indices.empty() ){
//set up the inclusion set
NegContainsSygusInvarianceTest ncset;
- ncset.init( d_tds, c, itxo->second, cmp_indices );
+ ncset.init(this, c, 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;
class CegConjecturePbe;
class CegEntailmentInfer;
+/** CegConjecturePbe
+*
+* This class implements optimizations that target Programming-By-Examples (PBE)
+* synthesis conjectures.
+* [EX#1] An example of a PBE synthesis conjecture is:
+*
+* 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.
+*/
class CegConjecturePbe {
private:
QuantifiersEngine* d_qe;
quantifiers::TermDbSygus * d_tds;
CegConjecture* d_parent;
+ /** for each candidate variable f (a function-to-synthesize), whether the
+ * conjecture is purely PBE for that variable
+ * In other words, all occurrences of f are guarded by equalities that
+ * constraint its arguments to constants.
+ */
std::map< Node, bool > d_examples_invalid;
+ /** for each candidate variable (function-to-synthesize), whether the
+ * conjecture is purely PBE for that variable.
+ * An example of a conjecture for which d_examples_invalid is false but
+ * d_examples_out_invalid is true is:
+ * exists f. forall x. ( x = 0 => f( x ) > 2 )
+ */
std::map< Node, bool > d_examples_out_invalid;
+ /** for each candidate variable (function-to-synthesize), input of I/O
+ * examples */
std::map< Node, std::vector< std::vector< Node > > > d_examples;
+ /** 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 ) */
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;
+
void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol );
bool d_is_pbe;
public:
void initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas );
bool getPbeExamples( Node v, std::vector< std::vector< Node > >& exs,
std::vector< Node >& exos, std::vector< Node >& exts);
+ /** is PBE enabled for any enumerator? */
bool isPbe() { return d_is_pbe; }
-private: // for registration
+ /** get candidate for enumerator */
+ Node getCandidateForEnumerator(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 */
+ unsigned getNumExamples(Node e);
+ /** get the input arguments for i^th I/O example for e, which is added to the
+ * vector ex */
+ 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);
+ int getExampleId(Node n);
+ /** add the search val, returns an equivalent value (possibly the same) */
+ Node addSearchVal(TypeNode tn, Node e, Node bvr);
+ /** evaluate builtin */
+ Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
+
+ private:
+ /** this class is an index of candidate solutions for PBE synthesis */
+ class PbeTrie {
+ private:
+ Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex,
+ CegConjecturePbe* cpbe, unsigned index,
+ unsigned ntotal);
+
+ public:
+ PbeTrie() {}
+ ~PbeTrie() {}
+ Node d_lazy_child;
+ std::map<Node, PbeTrie> d_children;
+ void clear() { d_children.clear(); }
+ Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe,
+ unsigned index, unsigned ntotal);
+ };
+ /** trie of candidate solutions tried, for each (enumerator, type),
+ * where type is a type in the grammar of the space of solutions for a subterm
+ * of e
+ */
+ std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
+
+ private: // for 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 );
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
-#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/theory_quantifiers.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
}
}
-void TermDbSygus::registerMeasuredTerm( Node e, Node root, bool mkActiveGuard ) {
- Assert( d_measured_term.find( e )==d_measured_term.end() );
- Trace("sygus-db") << "Register measured term : " << e << " with root " << root << std::endl;
- d_measured_term[e] = root;
+void TermDbSygus::registerMeasuredTerm(Node e, 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;
if( mkActiveGuard ){
// make the guard
Node eg = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "eG", NodeManager::currentNM()->booleanType() ) );
Node lem = NodeManager::currentNM()->mkNode( OR, eg, eg.negate() );
Trace("cegqi-lemma") << "Cegqi::Lemma : enumerator : " << lem << std::endl;
d_quantEngine->getOutputChannel().lemma( lem );
- d_measured_term_active_guard[e] = eg;
+ d_enum_to_active_guard[e] = eg;
}
}
-void TermDbSygus::registerPbeExamples( Node e, std::vector< std::vector< Node > >& exs,
- std::vector< Node >& exos, std::vector< Node >& exts ) {
- Trace("sygus-db") << "Register " << exs.size() << " PBE examples with " << e << std::endl;
- Assert( d_measured_term.find( e )==d_measured_term.end() || isMeasuredTerm( e )==e );
- Assert( d_pbe_exs.find( e )==d_pbe_exs.end() );
- Assert( exs.size()==exos.size() );
- d_pbe_exs[e] = exs;
- d_pbe_exos[e] = exos;
- for( unsigned i=0; i<exts.size(); i++ ){
- Trace("sygus-db-debug") << " # " << i << " : " << exts[i] << std::endl;
- Assert( exts[i].getKind()==APPLY_UF );
- Assert( exts[i][0]==e );
- d_pbe_term_id[exts[i]] = i;
- }
+bool TermDbSygus::isMeasuredTerm(Node e) const {
+ return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end();
}
-Node TermDbSygus::isMeasuredTerm( Node e ) {
- std::map< Node, Node >::iterator itm = d_measured_term.find( e );
- if( itm!=d_measured_term.end() ){
+CegConjecture* TermDbSygus::getConjectureFor(Node e) {
+ std::map<Node, CegConjecture*>::iterator itm = d_enum_to_conjecture.find(e);
+ if (itm != d_enum_to_conjecture.end()) {
return itm->second;
}else{
- return Node::null();
+ return NULL;
}
}
Node TermDbSygus::getActiveGuardForMeasureTerm( Node e ) {
- std::map< Node, Node >::iterator itag = d_measured_term_active_guard.find( e );
- if( itag!=d_measured_term_active_guard.end() ){
+ std::map<Node, Node>::iterator itag = d_enum_to_active_guard.find(e);
+ if (itag != d_enum_to_active_guard.end()) {
return itag->second;
}else{
return Node::null();
}
void TermDbSygus::getMeasuredTerms( std::vector< Node >& mts ) {
- for( std::map< Node, Node >::iterator itm = d_measured_term.begin(); itm != d_measured_term.end(); ++itm ){
+ for (std::map<Node, CegConjecture*>::iterator itm =
+ d_enum_to_conjecture.begin();
+ itm != d_enum_to_conjecture.end(); ++itm) {
mts.push_back( itm->first );
}
}
-bool TermDbSygus::hasPbeExamples( Node e ) {
- return d_pbe_exs.find( e )!=d_pbe_exs.end();
-}
-
-unsigned TermDbSygus::getNumPbeExamples( Node e ) {
- std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_pbe_exs.find( e );
- if( it!=d_pbe_exs.end() ){
- return it->second.size();
- }else{
- return 0;
- }
-}
-
-void TermDbSygus::getPbeExample( Node e, unsigned i, std::vector< Node >& ex ) {
- std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_pbe_exs.find( e );
- if( it!=d_pbe_exs.end() ){
- Assert( i<it->second.size() );
- Assert( i<d_pbe_exos[e].size() );
- ex.insert( ex.end(), it->second[i].begin(), it->second[i].end() );
- }else{
- Assert( false );
- }
-}
-Node TermDbSygus::getPbeExampleOut( Node e, unsigned i ) {
- std::map< Node, std::vector< Node > >::iterator it = d_pbe_exos.find( e );
- if( it!=d_pbe_exos.end() ){
- Assert( i<it->second.size() );
- return it->second[i];
- }else{
- Assert( false );
- return Node::null();
- }
-}
-
-int TermDbSygus::getPbeExampleId( Node n ) {
- std::map< Node, unsigned >::iterator it = d_pbe_term_id.find( n );
- if( it!=d_pbe_term_id.end() ){
- return it->second;
- }else{
- return -1;
- }
-}
-
bool TermDbSygus::isRegistered( TypeNode tn ) {
return d_register.find( tn )!=d_register.end();
}
void TermDbSygus::registerEvalTerm( Node n ) {
if( options::sygusDirectEval() ){
if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
- Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl;
+ Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n
+ << std::endl;
TypeNode tn = n[0].getType();
if( tn.isDatatype() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
Node f = n.getOperator();
Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl;
if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
- // check if it directly occurs in an input/ouput example
- int pbe_id = getPbeExampleId( n );
- if( pbe_id!=-1 ){
- Node n_res = getPbeExampleOut( n[0], pbe_id );
- if( !n_res.isNull() ){
- Trace("sygus-eager") << "......do not evaluate " << n << " since it is an input/output example : " << n_res << std::endl;
- return;
- }
- }
d_evals[n[0]].push_back( n );
TypeNode tn = n[0].getType();
Assert( tn.isDatatype() );
}
}
-Node TermDbSygus::evaluateBuiltin( TypeNode tn, Node bn, Node ar, unsigned i ) {
- std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_pbe_exs.find( ar );
- if( it!=d_pbe_exs.end() ){
- Assert( i<it->second.size() );
- return evaluateBuiltin( tn, bn, it->second[i] );
- }else{
- return Rewriter::rewrite( bn );
- }
-}
-
Node TermDbSygus::evaluateWithUnfolding( Node n, std::map< Node, Node >& visited ) {
std::map< Node, Node >::iterator it = visited.find( n );
if( it==visited.end() ){
}
}
-Node TermDbSygus::PbeTrie::addPbeExample( TypeNode etn, Node e, Node b, quantifiers::TermDbSygus * tds, unsigned index, unsigned ntotal ) {
- Assert( tds->getNumPbeExamples( e )==ntotal );
- if( index==ntotal ){
- //lazy child holds the leaf data
- if( d_lazy_child.isNull() ){
- d_lazy_child = b;
- }
- return d_lazy_child;
- }else{
- std::vector< Node > ex;
- if( d_children.empty() ){
- if( d_lazy_child.isNull() ){
- d_lazy_child = b;
- return d_lazy_child;
- }else{
- //evaluate the lazy child
- tds->getPbeExample( e, index, ex );
- addPbeExampleEval( etn, e, d_lazy_child, ex, tds, index, ntotal );
- Assert( !d_children.empty() );
- d_lazy_child = Node::null();
- }
- }else{
- tds->getPbeExample( e, index, ex );
- }
- return addPbeExampleEval( etn, e, b, ex, tds, index, ntotal );
- }
-}
-
-Node TermDbSygus::PbeTrie::addPbeExampleEval( TypeNode etn, Node e, Node b, std::vector< Node >& ex, quantifiers::TermDbSygus * tds, unsigned index, unsigned ntotal ) {
- Node eb = tds->evaluateBuiltin( etn, b, ex );
- return d_children[eb].addPbeExample( etn, e, b, tds, index+1, ntotal );
-}
-
-Node TermDbSygus::addPbeSearchVal( TypeNode tn, Node e, Node bvr ){
- Assert( !e.isNull() );
- if( hasPbeExamples( e ) ){
- unsigned nex = getNumPbeExamples( e );
- Node ret = d_pbe_trie[e][tn].addPbeExample( tn, e, bvr, this, 0, nex );
- Assert( ret.getType()==bvr.getType() );
- return ret;
- }
- return Node::null();
-}
-
Node TermDbSygus::extendedRewritePullIte( Node n ) {
// generalize this?
Assert( n.getNumChildren()==2 );
namespace theory {
namespace quantifiers {
+class CegConjecture;
+
class SygusInvarianceTest {
protected:
// check whether nvn[ x ] should be excluded
bool invariant( quantifiers::TermDbSygus * tds, Node nvn, Node x );
};
+// TODO :issue #1235 split and document this class
class TermDbSygus {
private:
/** reference to the quantifiers engine */
void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth );
bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
private:
- // stores root
- std::map< Node, Node > d_measured_term;
- std::map< Node, Node > d_measured_term_active_guard;
- //information for sygus types
- std::map< TypeNode, TypeNode > d_register; //stores sygus -> builtin type
- std::map< TypeNode, std::vector< Node > > d_var_list;
- std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
- std::map< TypeNode, std::map< Kind, int > > d_kinds;
- std::map< TypeNode, std::map< int, Node > > d_arg_const;
- std::map< TypeNode, std::map< Node, int > > d_consts;
- std::map< TypeNode, std::map< Node, int > > d_ops;
- std::map< TypeNode, std::map< int, Node > > d_arg_ops;
- std::map< TypeNode, std::vector< int > > d_id_funcs;
- std::map< TypeNode, std::vector< Node > > d_const_list; //sorted list of constants for type
- std::map< TypeNode, unsigned > d_const_list_pos;
- std::map< TypeNode, std::map< Node, Node > > d_semantic_skolem;
- //information for builtin types
- std::map< TypeNode, std::map< int, Node > > d_type_value;
- std::map< TypeNode, Node > d_type_max_value;
- std::map< TypeNode, std::map< Node, std::map< int, Node > > > d_type_value_offset;
- std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status;
- //normalized map
- std::map< TypeNode, std::map< Node, Node > > d_normalized;
- std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin;
- std::map< TypeNode, std::map< Node, Node > > d_builtin_const_to_sygus;
- // grammar information
- // root -> type -> _
- std::map< TypeNode, std::map< TypeNode, unsigned > > d_min_type_depth;
- //std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > > d_consider_const;
- // type -> cons -> _
- std::map< TypeNode, unsigned > d_min_term_size;
- std::map< TypeNode, std::map< unsigned, unsigned > > d_min_cons_term_size;
+ /** 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 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".
+ */
+ std::map<Node, Node> d_enum_to_active_guard;
+ // information for sygus types
+ std::map<TypeNode, TypeNode> d_register; // stores sygus -> builtin type
+ std::map<TypeNode, std::vector<Node> > d_var_list;
+ std::map<TypeNode, std::map<int, Kind> > d_arg_kind;
+ std::map<TypeNode, std::map<Kind, int> > d_kinds;
+ std::map<TypeNode, std::map<int, Node> > d_arg_const;
+ std::map<TypeNode, std::map<Node, int> > d_consts;
+ std::map<TypeNode, std::map<Node, int> > d_ops;
+ std::map<TypeNode, std::map<int, Node> > d_arg_ops;
+ std::map<TypeNode, std::vector<int> > d_id_funcs;
+ std::map<TypeNode, std::vector<Node> >
+ d_const_list; // sorted list of constants for type
+ std::map<TypeNode, unsigned> d_const_list_pos;
+ std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
+ // information for builtin types
+ std::map<TypeNode, std::map<int, Node> > d_type_value;
+ std::map<TypeNode, Node> d_type_max_value;
+ std::map<TypeNode, std::map<Node, std::map<int, Node> > > d_type_value_offset;
+ std::map<TypeNode, std::map<Node, std::map<int, int> > >
+ d_type_value_offset_status;
+ // normalized map
+ std::map<TypeNode, std::map<Node, Node> > d_normalized;
+ std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin;
+ std::map<TypeNode, std::map<Node, Node> > d_builtin_const_to_sygus;
+ // grammar information
+ // root -> type -> _
+ std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
+ // std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > >
+ // d_consider_const;
+ // type -> cons -> _
+ std::map<TypeNode, unsigned> d_min_term_size;
+ std::map<TypeNode, std::map<unsigned, unsigned> > d_min_cons_term_size;
public:
TermDbSygus( context::Context* c, QuantifiersEngine* qe );
~TermDbSygus(){}
public:
/** register the sygus type */
void registerSygusType( TypeNode tn );
- /** register a term that we will do enumerative search on */
- void registerMeasuredTerm( Node e, Node root, bool mkActiveGuard = false );
- /** is measured term */
- Node isMeasuredTerm( Node e );
- /** get active guard */
+ /** register a variable e that we will do enumerative search on
+ * conj is the conjecture that the enumeration for e is for.
+ * mkActiveGuard is whether we want to make a active guard for e (see
+ * d_enum_to_active_guard)
+ */
+ void registerMeasuredTerm(Node e, CegConjecture* conj,
+ bool mkActiveGuard = false);
+ /** is e a measured term (enumerator)? */
+ bool isMeasuredTerm(Node e) const;
+ /** return the conjecture e is associated with */
+ CegConjecture* getConjectureFor(Node e);
+ /** get active guard for e */
Node getActiveGuardForMeasureTerm( Node e );
- /** get measured terms */
+ /** get all registered measure terms (enumerators) */
void getMeasuredTerms( std::vector< Node >& mts );
public: //general sygus utilities
bool isRegistered( TypeNode tn );
void getExplanationFor( Node n, Node vn, std::vector< Node >& exp, SygusInvarianceTest& et );
// builtin evaluation, returns rewrite( bn [ args / vars(tn) ] )
Node evaluateBuiltin( TypeNode tn, Node bn, std::vector< Node >& args );
- Node evaluateBuiltin( TypeNode tn, Node bn, Node ar, unsigned i );
// evaluate with unfolding
Node evaluateWithUnfolding( Node n, std::map< Node, Node >& visited );
Node evaluateWithUnfolding( Node n );
public:
bool isGenericRedundant( TypeNode tn, unsigned i );
-//sygus pbe
-private:
- std::map< Node, std::vector< std::vector< Node > > > d_pbe_exs;
- std::map< Node, std::vector< Node > > d_pbe_exos;
- std::map< Node, unsigned > d_pbe_term_id;
-private:
- class PbeTrie {
- private:
- Node addPbeExampleEval( TypeNode etn, Node e, Node b, std::vector< Node >& ex, quantifiers::TermDbSygus * tds, unsigned index, unsigned ntotal );
- public:
- PbeTrie(){}
- ~PbeTrie(){}
- Node d_lazy_child;
- std::map< Node, PbeTrie > d_children;
- void clear() { d_children.clear(); }
- Node addPbeExample( TypeNode etn, Node e, Node b, TermDbSygus * tds, unsigned index, unsigned ntotal );
- };
- std::map< Node, std::map< TypeNode, PbeTrie > > d_pbe_trie;
-public:
- /** register examples for an enumerative search term.
- This should be a comprehensive set of examples. */
- void registerPbeExamples( Node e, std::vector< std::vector< Node > >& exs,
- std::vector< Node >& exos, std::vector< Node >& exts );
- /** get examples */
- bool hasPbeExamples( Node e );
- unsigned getNumPbeExamples( Node e );
- /** return value is the required value for the example */
- void getPbeExample( Node e, unsigned i, std::vector< Node >& ex );
- Node getPbeExampleOut( Node e, unsigned i );
- int getPbeExampleId( Node n );
- /** add the search val, returns an equivalent value (possibly the same) */
- Node addPbeSearchVal( TypeNode tn, Node e, Node bvr );
-
// extended rewriting
private:
std::map< Node, Node > d_ext_rewrite_cache;
projects / cvc5.git / commitdiff