summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/sygus/cegis.cpp24
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.cpp21
-rw-r--r--src/theory/quantifiers/sygus/enum_stream_substitution.cpp13
-rw-r--r--src/theory/quantifiers/sygus/enum_stream_substitution.h8
-rw-r--r--src/theory/quantifiers/sygus/sygus_enumerator.cpp183
-rw-r--r--src/theory/quantifiers/sygus/sygus_enumerator.h17
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.cpp378
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.h3
-rw-r--r--src/theory/quantifiers/sygus/sygus_pbe.cpp18
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp88
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.h26
-rw-r--r--src/theory/quantifiers/sygus/term_database_sygus.cpp128
-rw-r--r--src/theory/quantifiers/sygus/term_database_sygus.h61
13 files changed, 644 insertions, 324 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 79bec60ee..6aca71ca3 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -69,17 +69,10 @@ bool Cegis::processInitialize(Node n,
{
Trace("cegis") << "Initialize cegis..." << std::endl;
unsigned csize = candidates.size();
- // We only can use actively-generated enumerators if there is only one
- // function-to-synthesize. Otherwise, we would have to generate a "product" of
- // two actively-generated enumerators. That is, given a conjecture with two
- // functions-to-synthesize with enumerators e_f and e_g, if:
- // e_f -> t1, ..., tn
- // e_g -> s1, ..., sm
- // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj)
- // for each i,j. We do not do this and revert to the default behavior of
- // this module instead.
- bool isActiveGen =
- options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1;
+ // The role of enumerators is to be either the single solution or part of
+ // a solution involving multiple enumerators.
+ EnumeratorRole erole =
+ csize == 1 ? ROLE_ENUM_SINGLE_SOLUTION : ROLE_ENUM_MULTI_SOLUTION;
// initialize an enumerator for each candidate
for (unsigned i = 0; i < csize; i++)
{
@@ -98,13 +91,8 @@ bool Cegis::processInitialize(Node n,
}
}
Trace("cegis") << std::endl;
- // variable agnostic enumerators require an active guard
- d_tds->registerEnumerator(candidates[i],
- candidates[i],
- d_parent,
- isActiveGen,
- do_repair_const,
- isActiveGen);
+ d_tds->registerEnumerator(
+ candidates[i], candidates[i], d_parent, erole, do_repair_const);
}
return true;
}
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index dbde79aae..18e313bf0 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -44,7 +44,12 @@ bool CegisUnif::processInitialize(Node n,
std::map<Node, Node> pt_to_cond;
// strategy lemmas for each strategy point
std::map<Node, std::vector<Node>> strategy_lemmas;
- // Initialize strategies for all functions-to-synhesize
+ // Initialize strategies for all functions-to-synthesize
+ // The role of non-unification enumerators is to be either the single solution
+ // or part of a solution involving multiple enumerators.
+ EnumeratorRole eroleNonUnif = candidates.size() == 1
+ ? ROLE_ENUM_SINGLE_SOLUTION
+ : ROLE_ENUM_MULTI_SOLUTION;
for (const Node& f : candidates)
{
// Init UNIF util for this candidate
@@ -53,7 +58,7 @@ bool CegisUnif::processInitialize(Node n,
if (!d_sygus_unif.usingUnif(f))
{
Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
- d_tds->registerEnumerator(f, f, d_parent);
+ d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif);
d_non_unif_candidates.push_back(f);
}
else
@@ -462,7 +467,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
exclude_cons,
term_irrelevant);
d_virtual_enum = nm->mkSkolem("_ve", vtn);
- d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent);
+ d_tds->registerEnumerator(
+ d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
}
// if new_size is a power of two, then isPow2 returns log2(new_size)+1
// otherwise, this returns 0. In the case it returns 0, we don't care
@@ -606,20 +612,17 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
}
// register the enumerator
si.d_enums[index].push_back(e);
- bool mkActiveGuard = false;
- bool isActiveGen = false;
+ EnumeratorRole erole = ROLE_ENUM_CONSTRAINED;
// if we are using a single independent enumerator for conditions, then we
// allocate an active guard, and are eligible to use variable-agnostic
// enumeration.
if (options::sygusUnifCondIndependent() && index == 1)
{
- mkActiveGuard = true;
- isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE;
+ erole = ROLE_ENUM_POOL;
}
Trace("cegis-unif-enum") << "* Registering new enumerator " << e
<< " to strategy point " << si.d_pt << "\n";
- d_tds->registerEnumerator(
- e, si.d_pt, d_parent, mkActiveGuard, false, isActiveGen);
+ d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, false);
}
void CegisUnifEnumDecisionStrategy::registerEvalPts(
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 24770ade0..e8daa4256 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -608,8 +608,17 @@ bool EnumStreamSubstitution::CombinationState::getNextCombination()
}
void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); }
-void EnumStreamConcrete::addValue(Node v) { d_ess.resetValue(v); }
-Node EnumStreamConcrete::getNext() { return d_ess.getNext(); }
+void EnumStreamConcrete::addValue(Node v)
+{
+ d_ess.resetValue(v);
+ d_currTerm = d_ess.getNext();
+}
+bool EnumStreamConcrete::increment()
+{
+ d_currTerm = d_ess.getNext();
+ return !d_currTerm.isNull();
+}
+Node EnumStreamConcrete::getCurrent() { return d_currTerm; }
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h
index 38fa0627b..476a364ea 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.h
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h
@@ -286,12 +286,16 @@ class EnumStreamConcrete : public EnumValGenerator
void initialize(Node e) override;
/** get that value v was enumerated */
void addValue(Node v) override;
- /** get the next value enumerated by this class */
- Node getNext() override;
+ /** increment */
+ bool increment() override;
+ /** get the current value enumerated by this class */
+ Node getCurrent() override;
private:
/** stream substitution utility */
EnumStreamSubstitution d_ess;
+ /** the current term generated by this class */
+ Node d_currTerm;
};
} // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 61ab9007a..5c3e44a33 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -25,21 +25,78 @@ namespace theory {
namespace quantifiers {
SygusEnumerator::SygusEnumerator(TermDbSygus* tds, SynthConjecture* p)
- : d_tds(tds),
- d_parent(p),
- d_tlEnum(nullptr),
- d_abortSize(-1),
- d_firstTime(false)
+ : d_tds(tds), d_parent(p), d_tlEnum(nullptr), d_abortSize(-1)
{
}
void SygusEnumerator::initialize(Node e)
{
+ Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl;
d_enum = e;
d_etype = d_enum.getType();
+ Assert(d_etype.isDatatype());
+ Assert(d_etype.getDatatype().isSygus());
d_tlEnum = getMasterEnumForType(d_etype);
d_abortSize = options::sygusAbortSize();
- d_firstTime = true;
+
+ // Get the statically registered symmetry breaking clauses for e, see if they
+ // can be used for speeding up the enumeration.
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> sbl;
+ d_tds->getSymBreakLemmas(e, sbl);
+ Node ag = d_tds->getActiveGuardForEnumerator(e);
+ Node truen = nm->mkConst(true);
+ // use TNode for substitute below
+ TNode agt = ag;
+ TNode truent = truen;
+ Assert(d_tcache.find(d_etype) != d_tcache.end());
+ const Datatype& dt = d_etype.getDatatype();
+ for (const Node& lem : sbl)
+ {
+ if (!d_tds->isSymBreakLemmaTemplate(lem))
+ {
+ // substitute its active guard by true and rewrite
+ Node slem = lem.substitute(agt, truent);
+ slem = Rewriter::rewrite(slem);
+ // break into conjuncts
+ std::vector<Node> sblc;
+ if (slem.getKind() == AND)
+ {
+ for (const Node& slemc : slem)
+ {
+ sblc.push_back(slemc);
+ }
+ }
+ else
+ {
+ sblc.push_back(slem);
+ }
+ for (const Node& sbl : sblc)
+ {
+ Trace("sygus-enum")
+ << " symmetry breaking lemma : " << sbl << std::endl;
+ // if its a negation of a unit top-level tester, then this specifies
+ // that we should not enumerate terms whose top symbol is that
+ // constructor
+ if (sbl.getKind() == NOT)
+ {
+ Node a;
+ int tst = datatypes::DatatypesRewriter::isTester(sbl[0], a);
+ if (tst >= 0)
+ {
+ if (a == e)
+ {
+ Node cons = Node::fromExpr(dt[tst].getConstructor());
+ Trace("sygus-enum") << " ...unit exclude constructor #" << tst
+ << ", constructor " << cons << std::endl;
+ d_sbExcTlCons.insert(cons);
+ }
+ }
+ }
+ // other symmetry breaking lemmas such as disjunctions are not used
+ }
+ }
+ }
}
void SygusEnumerator::addValue(Node v)
@@ -47,17 +104,9 @@ void SygusEnumerator::addValue(Node v)
// do nothing
}
-Node SygusEnumerator::getNext()
+bool SygusEnumerator::increment() { return d_tlEnum->increment(); }
+Node SygusEnumerator::getCurrent()
{
- if (d_firstTime)
- {
- d_firstTime = false;
- }
- else if (!d_tlEnum->increment())
- {
- // no more values
- return Node::null();
- }
if (d_abortSize >= 0)
{
int cs = static_cast<int>(d_tlEnum->getCurrentSize());
@@ -70,14 +119,30 @@ Node SygusEnumerator::getNext()
}
}
Node ret = d_tlEnum->getCurrent();
- Trace("sygus-enum") << "Enumerate : " << d_tds->sygusToBuiltin(ret)
- << std::endl;
+ if (!ret.isNull() && !d_sbExcTlCons.empty())
+ {
+ Assert(ret.hasOperator());
+ // might be excluded by an externally provided symmetry breaking clause
+ if (d_sbExcTlCons.find(ret.getOperator()) != d_sbExcTlCons.end())
+ {
+ Trace("sygus-enum-exc")
+ << "Exclude (external) : " << d_tds->sygusToBuiltin(ret) << std::endl;
+ ret = Node::null();
+ }
+ }
+ if (Trace.isOn("sygus-enum"))
+ {
+ Trace("sygus-enum") << "Enumerate : ";
+ TermDbSygus::toStreamSygus("sygus-enum", ret);
+ Trace("sygus-enum") << std::endl;
+ }
return ret;
}
SygusEnumerator::TermCache::TermCache()
: d_tds(nullptr),
d_pbe(nullptr),
+ d_isSygusType(false),
d_numConClasses(0),
d_sizeEnum(0),
d_isComplete(false)
@@ -241,33 +306,37 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
d_terms.push_back(n);
return true;
}
- Node bn = d_tds->sygusToBuiltin(n);
- Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
- // must be unique up to rewriting
- if (d_bterms.find(bnr) != d_bterms.end())
- {
- Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
- return false;
- }
- // if we are doing PBE symmetry breaking
- if (d_pbe != nullptr)
+ Assert(!n.isNull());
+ if (options::sygusSymBreakDynamic())
{
- // Is it equivalent under examples?
- Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr);
- if (!bne.isNull())
+ Node bn = d_tds->sygusToBuiltin(n);
+ Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
+ // must be unique up to rewriting
+ if (d_bterms.find(bnr) != d_bterms.end())
{
- if (bnr != bne)
+ Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
+ return false;
+ }
+ // if we are doing PBE symmetry breaking
+ if (d_pbe != nullptr)
+ {
+ // Is it equivalent under examples?
+ Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr);
+ if (!bne.isNull())
{
- Trace("sygus-enum-exc") << "Exclude (by examples): " << bn
- << ", since we already have " << bne
- << "!=" << bnr << std::endl;
- return false;
+ if (bnr != bne)
+ {
+ Trace("sygus-enum-exc") << "Exclude (by examples): " << bn
+ << ", since we already have " << bne
+ << "!=" << bnr << std::endl;
+ return false;
+ }
}
}
+ Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
+ d_bterms.insert(bnr);
}
- Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
d_terms.push_back(n);
- d_bterms.insert(bnr);
return true;
}
void SygusEnumerator::TermCache::pushEnumSizeIndex()
@@ -302,7 +371,12 @@ void SygusEnumerator::TermCache::setComplete() { d_isComplete = true; }
unsigned SygusEnumerator::TermEnum::getCurrentSize() { return d_currSize; }
SygusEnumerator::TermEnum::TermEnum() : d_se(nullptr), d_currSize(0) {}
SygusEnumerator::TermEnumSlave::TermEnumSlave()
- : TermEnum(), d_sizeLim(0), d_index(0), d_indexNextEnd(0), d_master(nullptr)
+ : TermEnum(),
+ d_sizeLim(0),
+ d_index(0),
+ d_indexNextEnd(0),
+ d_hasIndexNextEnd(false),
+ d_master(nullptr)
{
}
@@ -384,7 +458,7 @@ bool SygusEnumerator::TermEnumSlave::validateIndex()
Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : validate index...\n";
SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
// ensure that index is in the range
- if (d_index >= tc.getNumTerms())
+ while (d_index >= tc.getNumTerms())
{
Assert(d_index == tc.getNumTerms());
Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n";
@@ -494,6 +568,7 @@ SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
SygusEnumerator::TermEnumMaster::TermEnumMaster()
: TermEnum(),
d_isIncrementing(false),
+ d_currTermSet(false),
d_consClassNum(0),
d_ccWeight(0),
d_consNum(0),
@@ -515,6 +590,7 @@ bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se,
d_currChildSize = 0;
d_ccCons.clear();
d_isIncrementing = false;
+ d_currTermSet = false;
bool ret = increment();
Trace("sygus-enum-debug") << "master(" << tn
<< "): finish init, ret = " << ret << "\n";
@@ -523,10 +599,11 @@ bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se,
Node SygusEnumerator::TermEnumMaster::getCurrent()
{
- if (!d_currTerm.isNull())
+ if (d_currTermSet)
{
return d_currTerm;
}
+ d_currTermSet = true;
// construct based on the children
std::vector<Node> children;
const Datatype& dt = d_tn.getDatatype();
@@ -538,7 +615,13 @@ Node SygusEnumerator::TermEnumMaster::getCurrent()
for (unsigned i = 0, nargs = dt[cnum].getNumArgs(); i < nargs; i++)
{
Assert(d_children.find(i) != d_children.end());
- children.push_back(d_children[i].getCurrent());
+ Node cc = d_children[i].getCurrent();
+ if (cc.isNull())
+ {
+ d_currTerm = cc;
+ return cc;
+ }
+ children.push_back(cc);
}
d_currTerm = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
return d_currTerm;
@@ -705,21 +788,27 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal()
Assert(d_childrenValid == d_ccTypes.size());
// do we have more constructors for the given children?
- while (d_consNum < d_ccCons.size())
+ if (d_consNum < d_ccCons.size())
{
Trace("sygus-enum-debug2") << "master(" << d_tn << "): try constructor "
<< d_consNum << std::endl;
// increment constructor index
// we will build for the current constructor and the given children
d_consNum++;
+ d_currTermSet = false;
d_currTerm = Node::null();
Node c = getCurrent();
- if (tc.addTerm(c))
+ if (!c.isNull())
{
- return true;
+ if (!tc.addTerm(c))
+ {
+ // the term was not unique based on rewriting
+ Trace("sygus-enum-debug2") << "master(" << d_tn
+ << "): failed addTerm\n";
+ d_currTerm = Node::null();
+ }
}
- Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed addTerm\n";
- // the term was not unique based on rewriting
+ return true;
}
// finished constructors for this set of children, must increment children
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index 10a44da03..af6bb03f0 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -50,8 +50,10 @@ class SygusEnumerator : public EnumValGenerator
void initialize(Node e) override;
/** Inform this generator that abstract value v was enumerated. */
void addValue(Node v) override;
+ /** increment */
+ bool increment() override;
/** Get the next concrete value generated by this class. */
- Node getNext() override;
+ Node getCurrent() override;
private:
/** pointer to term database sygus */
@@ -322,6 +324,8 @@ class SygusEnumerator : public EnumValGenerator
bool d_isIncrementing;
/** cache for getCurrent() */
Node d_currTerm;
+ /** is d_currTerm set */
+ bool d_currTermSet;
//----------------------------- current constructor class information
/** the next constructor class we are using */
unsigned d_consClassNum;
@@ -429,10 +433,17 @@ class SygusEnumerator : public EnumValGenerator
TermEnum* d_tlEnum;
/** the abort size, caches the value of --sygus-abort-size */
int d_abortSize;
- /** this flag is true for the first time to getNext() after initialize(e) */
- bool d_firstTime;
/** get master enumerator for type tn */
TermEnum* getMasterEnumForType(TypeNode tn);
+ //-------------------------------- externally specified symmetry breaking
+ /** set of constructors we disallow at top level
+ *
+ * A constructor C is disallowed at the top level if a symmetry breaking
+ * lemma that entails ~is-C( d_enum ) was registered to
+ * TermDbSygus::registerSymBreakLemma.
+ */
+ std::unordered_set<Node, NodeHashFunction> d_sbExcTlCons;
+ //-------------------------------- end externally specified symmetry breaking
};
} // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 47c701cf6..d6dfb3d26 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -374,18 +374,24 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
// TODO #1178 : add other missing types
}
-void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){
+void CegGrammarConstructor::collectSygusGrammarTypesFor(
+ TypeNode range, std::vector<TypeNode>& types)
+{
if( !range.isBoolean() ){
if( std::find( types.begin(), types.end(), range )==types.end() ){
Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl;
types.push_back( range );
if( range.isDatatype() ){
- const Datatype& dt = ((DatatypeType)range.toType()).getDatatype();
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() );
- sels[crange].push_back( dt[i][j] );
- collectSygusGrammarTypesFor( crange, types, sels );
+ const Datatype& dt = range.getDatatype();
+ for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
+ {
+ for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args;
+ ++j)
+ {
+ collectSygusGrammarTypesFor(
+ TypeNode::fromType(static_cast<SelectorType>(dt[i][j].getType())
+ .getRangeType()),
+ types);
}
}
}
@@ -408,76 +414,87 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
<< range << std::endl;
// collect the variables
std::vector<Node> sygus_vars;
- if( !bvl.isNull() ){
- for( unsigned i=0; i<bvl.getNumChildren(); i++ ){
+ if (!bvl.isNull())
+ {
+ for (unsigned i = 0, size = bvl.getNumChildren(); i < size; ++i)
+ {
if (term_irrelevant.find(bvl[i]) == term_irrelevant.end())
{
sygus_vars.push_back(bvl[i]);
}
else
{
- Trace("sygus-grammar-def") << "...synth var " << bvl[i]
- << " has been marked irrelevant."
- << std::endl;
+ Trace("sygus-grammar-def")
+ << "...synth var " << bvl[i] << " has been marked irrelevant."
+ << std::endl;
}
}
}
- //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
- // parseError("No default grammar for type.");
- //}
- std::vector< std::vector< Expr > > ops;
+ // operators for each constructor in type
+ std::vector<std::vector<Expr>> ops;
+ // names for the operators
+ std::vector<std::vector<std::string>> cnames;
+ // argument types of operators
+ std::vector<std::vector<std::vector<Type>>> cargs;
+ // set of callbacks for each constructor
+ std::vector<std::vector<std::shared_ptr<SygusPrintCallback>>> pcs;
+ // weights for each constructor
+ std::vector<std::vector<int>> weights;
+ // index of top datatype, i.e. the datatype for the range type
int startIndex = -1;
std::map< Type, Type > sygus_to_builtin;
- std::vector< TypeNode > types;
- std::map< TypeNode, std::vector< DatatypeConstructorArg > > sels;
- //types for each of the variables of parametric sort
- for( unsigned i=0; i<sygus_vars.size(); i++ ){
- collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels );
+ std::vector<TypeNode> types;
+ // collect connected types for each of the variables
+ for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
+ {
+ collectSygusGrammarTypesFor(sygus_vars[i].getType(), types);
}
- //types connected to range
- collectSygusGrammarTypesFor( range, types, sels );
+ // collect connected types to range
+ collectSygusGrammarTypesFor(range, types);
- //name of boolean sort
+ // create placeholder for boolean type (kept apart since not collected)
std::stringstream ssb;
ssb << fun << "_Bool";
std::string dbname = ssb.str();
Type unres_bt = mkUnresolvedType(ssb.str(), unres).toType();
+ // create placeholders for collected types
std::vector< Type > unres_types;
std::map< TypeNode, Type > type_to_unres;
- for( unsigned i=0; i<types.size(); i++ ){
+ for (unsigned i = 0, size = types.size(); i < size; ++i)
+ {
std::stringstream ss;
ss << fun << "_" << types[i];
std::string dname = ss.str();
datatypes.push_back(Datatype(dname));
ops.push_back(std::vector< Expr >());
+ cnames.push_back(std::vector<std::string>());
+ cargs.push_back(std::vector<std::vector<Type>>());
+ pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>());
+ weights.push_back(std::vector<int>());
//make unresolved type
Type unres_t = mkUnresolvedType(dname, unres).toType();
unres_types.push_back(unres_t);
type_to_unres[types[i]] = unres_t;
sygus_to_builtin[unres_t] = types[i].toType();
}
- for( unsigned i=0; i<types.size(); i++ ){
+ for (unsigned i = 0, size = types.size(); i < size; ++i)
+ {
Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
- std::vector<std::string> cnames;
- std::vector<std::vector<CVC4::Type> > cargs;
- /* Print callbacks for each constructor */
- std::vector<std::shared_ptr<SygusPrintCallback>> pcs;
- /* Weights for each constructor */
- std::vector<int> weights;
Type unres_t = unres_types[i];
//add variables
- for( unsigned j=0; j<sygus_vars.size(); j++ ){
+ for (unsigned j = 0, size_j = sygus_vars.size(); j < size_j; ++j)
+ {
if( sygus_vars[j].getType()==types[i] ){
std::stringstream ss;
ss << sygus_vars[j];
Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
ops[i].push_back( sygus_vars[j].toExpr() );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(ss.str());
+ cargs[i].push_back(std::vector<Type>());
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
}
//add constants
@@ -486,33 +503,35 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
std::map< TypeNode, std::vector< Node > >::iterator itec = extra_cons.find( types[i] );
if( itec!=extra_cons.end() ){
//consts.insert( consts.end(), itec->second.begin(), itec->second.end() );
- for( unsigned j=0; j<itec->second.size(); j++ ){
+ for (unsigned j = 0, size_j = itec->second.size(); j < size_j; ++j)
+ {
if( std::find( consts.begin(), consts.end(), itec->second[j] )==consts.end() ){
consts.push_back( itec->second[j] );
}
}
}
- for( unsigned j=0; j<consts.size(); j++ ){
+ for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j)
+ {
std::stringstream ss;
ss << consts[j];
Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl;
ops[i].push_back( consts[j].toExpr() );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(ss.str());
+ cargs[i].push_back(std::vector<Type>());
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
- //ITE
- CVC4::Kind k = kind::ITE;
+ // ITE
+ Kind k = ITE;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back( kind::kindToString(k) );
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_bt);
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_bt);
+ cargs[i].back().push_back(unres_t);
+ cargs[i].back().push_back(unres_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
if (types[i].isReal())
{
@@ -521,16 +540,17 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
Kind k = j == 0 ? PLUS : MINUS;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kind::kindToString(k));
- cargs.push_back(std::vector<CVC4::Type>());
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_t);
+ cargs[i].back().push_back(unres_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
if (!types[i].isInteger())
{
- Trace("sygus-grammar-def") << "...Dedicate to Real\n";
+ Trace("sygus-grammar-def")
+ << " ...create auxiliary Positive Integers grammar\n";
/* Creating type for positive integers */
std::stringstream ss;
ss << fun << "_PosInt";
@@ -546,7 +566,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
/* Add operator 1 */
Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n";
ops_pos_int.push_back(nm->mkConst(Rational(1)).toExpr());
- ss << "_1";
+ ss.str("");
+ ss << "1";
cnames_pos_int.push_back(ss.str());
cargs_pos_int.push_back(std::vector<Type>());
/* Add operator PLUS */
@@ -558,23 +579,23 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
cargs_pos_int.back().push_back(unres_pos_int_t);
cargs_pos_int.back().push_back(unres_pos_int_t);
datatypes.back().setSygus(types[i].toType(), bvl.toExpr(), true, true);
- for (unsigned j = 0; j < ops_pos_int.size(); j++)
+ for (unsigned j = 0, size_j = ops_pos_int.size(); j < size_j; ++j)
{
datatypes.back().addSygusConstructor(
ops_pos_int[j], cnames_pos_int[j], cargs_pos_int[j]);
}
Trace("sygus-grammar-def")
- << "...built datatype " << datatypes.back() << " ";
+ << " ...built datatype " << datatypes.back() << " ";
/* Adding division at root */
k = DIVISION;
Trace("sygus-grammar-def") << "\t...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<Type>());
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_pos_int_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_t);
+ cargs[i].back().push_back(unres_pos_int_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
}
else if (types[i].isBitVector())
@@ -585,11 +606,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
{
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<Type>());
- cargs.back().push_back(unres_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
// binary apps
std::vector<Kind> bin_kinds = {BITVECTOR_AND,
@@ -609,56 +630,65 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
{
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<Type>());
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_t);
+ cargs[i].back().push_back(unres_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
}
else if (types[i].isDatatype())
{
Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
- const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
- for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+ const Datatype& dt = types[i].getDatatype();
+ for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
+ {
Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl;
ops[i].push_back( dt[k].getConstructor() );
- cnames.push_back( dt[k].getName() );
- cargs.push_back( std::vector< CVC4::Type >() );
- for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){
- TypeNode crange = TypeNode::fromType( ((SelectorType)dt[k][j].getType()).getRangeType() );
- //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
- cargs.back().push_back( type_to_unres[crange] );
+ cnames[i].push_back(dt[k].getName());
+ cargs[i].push_back(std::vector<Type>());
+ Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
+ for (unsigned j = 0, size_j = dt[k].getNumArgs(); j < size_j; ++j)
+ {
+ Trace("sygus-grammar-def")
+ << "...for " << dt[k][j].getName() << std::endl;
+ TypeNode crange = TypeNode::fromType(
+ static_cast<SelectorType>(dt[k][j].getType()).getRangeType());
+ Assert(type_to_unres.find(crange) != type_to_unres.end());
+ cargs[i].back().push_back(type_to_unres[crange]);
+ // add to the selector type the selector operator
+
+ Assert(std::find(types.begin(), types.end(), crange) != types.end());
+ unsigned i_selType = std::distance(
+ types.begin(), std::find(types.begin(), types.end(), crange));
+ TypeNode arg_type = TypeNode::fromType(
+ static_cast<SelectorType>(dt[k][j].getType()).getDomain());
+ ops[i_selType].push_back(dt[k][j].getSelector());
+ cnames[i_selType].push_back(dt[k][j].getName());
+ cargs[i_selType].push_back(std::vector<Type>());
+ Assert(type_to_unres.find(arg_type) != type_to_unres.end());
+ cargs[i_selType].back().push_back(type_to_unres[arg_type]);
+ pcs[i_selType].push_back(nullptr);
+ weights[i_selType].push_back(-1);
}
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
}else{
std::stringstream sserr;
sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
throw LogicException(sserr.str());
}
- //add for all selectors to this type
- if( !sels[types[i]].empty() ){
- Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
- for( unsigned j=0; j<sels[types[i]].size(); j++ ){
- Trace("sygus-grammar-def") << "...for " << sels[types[i]][j].getName() << std::endl;
- TypeNode arg_type = TypeNode::fromType( ((SelectorType)sels[types[i]][j].getType()).getDomain() );
- ops[i].push_back( sels[types[i]][j].getSelector() );
- cnames.push_back( sels[types[i]][j].getName() );
- cargs.push_back( std::vector< CVC4::Type >() );
- //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() );
- cargs.back().push_back( type_to_unres[arg_type] );
- pcs.push_back(nullptr);
- weights.push_back(-1);
- }
- }
+ }
+ // make datatypes
+ for (unsigned i = 0, size = types.size(); i < size; ++i)
+ {
Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl;
datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true );
std::map<TypeNode, std::vector<Node>>::iterator itexc =
exc_cons.find(types[i]);
- for (unsigned j = 0, size = ops[i].size(); j < size; j++)
+ for (unsigned j = 0, size = ops[i].size(); j < size; ++j)
{
// add the constructor if it is not excluded
Node opn = Node::fromExpr(ops[i][j]);
@@ -667,12 +697,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
== itexc->second.end())
{
datatypes[i].addSygusConstructor(
- ops[i][j], cnames[j], cargs[j], pcs[j], weights[j]);
+ ops[i][j], cnames[i][j], cargs[i][j], pcs[i][j], weights[i][j]);
}
}
- Trace("sygus-grammar-def")
- << "...built datatype " << datatypes[i] << " ";
- //sorts.push_back( types[i] );
+ Trace("sygus-grammar-def") << "...built datatype " << datatypes[i] << " ";
//set start index if applicable
if( types[i]==range ){
startIndex = i;
@@ -683,94 +711,96 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
TypeNode btype = nm->booleanType();
datatypes.push_back(Datatype(dbname));
ops.push_back(std::vector<Expr>());
- std::vector<std::string> cnames;
- std::vector<std::vector< Type > > cargs;
- /* Print callbacks for each constructor */
- std::vector<std::shared_ptr<SygusPrintCallback>> pcs;
- /* Weights for each constructor */
- std::vector<int> weights;
+ cnames.push_back(std::vector<std::string>());
+ cargs.push_back(std::vector<std::vector<Type>>());
+ pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>());
+ weights.push_back(std::vector<int>());
Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
//add variables
- for( unsigned i=0; i<sygus_vars.size(); i++ ){
+ for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
+ {
if( sygus_vars[i].getType().isBoolean() ){
std::stringstream ss;
ss << sygus_vars[i];
Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
ops.back().push_back( sygus_vars[i].toExpr() );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- pcs.push_back(nullptr);
- weights.push_back(1);
+ cnames.back().push_back(ss.str());
+ cargs.back().push_back(std::vector<Type>());
+ pcs.back().push_back(nullptr);
+ // make boolean variables weight as non-nullary constructors
+ weights.back().push_back(1);
}
}
- //add constants
+ // add constants
std::vector<Node> consts;
mkSygusConstantsForType(btype, consts);
- for (unsigned j = 0; j < consts.size(); j++)
+ for (unsigned i = 0, size = consts.size(); i < size; ++i)
{
std::stringstream ss;
- ss << consts[j];
+ ss << consts[i];
Trace("sygus-grammar-def") << "...add for constant " << ss.str()
<< std::endl;
- ops.back().push_back(consts[j].toExpr());
- cnames.push_back(ss.str());
- cargs.push_back(std::vector<CVC4::Type>());
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ ops.back().push_back(consts[i].toExpr());
+ cnames.back().push_back(ss.str());
+ cargs.back().push_back(std::vector<Type>());
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
- //add predicates for types
- for( unsigned i=0; i<types.size(); i++ ){
+ // add predicates for types
+ for (unsigned i = 0, size = types.size(); i < size; ++i)
+ {
Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
//add equality per type
- CVC4::Kind k = kind::EQUAL;
+ Kind k = EQUAL;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(nm->operatorOf(k).toExpr());
std::stringstream ss;
- ss << kind::kindToString(k) << "_" << types[i];
- cnames.push_back(ss.str());
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_types[i]);
- cargs.back().push_back(unres_types[i]);
- pcs.push_back(nullptr);
- weights.push_back(-1);
- //type specific predicates
+ ss << kindToString(k) << "_" << types[i];
+ cnames.back().push_back(ss.str());
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_types[i]);
+ cargs.back().back().push_back(unres_types[i]);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
+ // type specific predicates
if (types[i].isReal())
{
- CVC4::Kind k = kind::LEQ;
+ Kind k = LEQ;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kind::kindToString(k));
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_types[i]);
- cargs.back().push_back(unres_types[i]);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames.back().push_back(kindToString(k));
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_types[i]);
+ cargs.back().back().push_back(unres_types[i]);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
else if (types[i].isBitVector())
{
Kind k = BITVECTOR_ULT;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<Type>());
- cargs.back().push_back(unres_types[i]);
- cargs.back().push_back(unres_types[i]);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames.back().push_back(kindToString(k));
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_types[i]);
+ cargs.back().back().push_back(unres_types[i]);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
else if (types[i].isDatatype())
{
//add for testers
Trace("sygus-grammar-def") << "...add for testers" << std::endl;
- const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
- for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+ const Datatype& dt = types[i].getDatatype();
+ for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
+ {
Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl;
ops.back().push_back(dt[k].getTester());
- cnames.push_back(dt[k].getTesterName());
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_types[i]);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames.back().push_back(dt[k].getTesterName());
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_types[i]);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
}
}
@@ -790,19 +820,19 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
}
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<CVC4::Type>());
- cargs.back().push_back(unres_bt);
+ cnames.back().push_back(kindToString(k));
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_bt);
if (k != NOT)
{
- cargs.back().push_back(unres_bt);
+ cargs.back().back().push_back(unres_bt);
if (k == ITE)
{
- cargs.back().push_back(unres_bt);
+ cargs.back().back().push_back(unres_bt);
}
}
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
}
if( range==btype ){
@@ -810,15 +840,19 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
}
Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl;
datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true );
- for( unsigned j=0; j<ops.back().size(); j++ ){
- datatypes.back().addSygusConstructor(
- ops.back()[j], cnames[j], cargs[j], pcs[j], weights[j]);
+ for (unsigned i = 0, size = ops.back().size(); i < size; ++i)
+ {
+ datatypes.back().addSygusConstructor(ops.back()[i],
+ cnames.back()[i],
+ cargs.back()[i],
+ pcs.back()[i],
+ weights.back()[i]);
}
- //sorts.push_back( btype );
+ Trace("sygus-grammar-def") << "...built datatype " << datatypes.back() << " ";
Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl;
-
+ // make first datatype be the top level datatype
if( startIndex>0 ){
- CVC4::Datatype tmp_dt = datatypes[0];
+ Datatype tmp_dt = datatypes[0];
datatypes[0] = datatypes[startIndex];
datatypes[startIndex] = tmp_dt;
}
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 0c5b67656..3afc4c689 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -131,7 +131,8 @@ public:
// helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres);
// collect the list of types that depend on type range
- static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels );
+ static void collectSygusGrammarTypesFor(TypeNode range,
+ std::vector<TypeNode>& types);
/** helper function for function mkSygusDefaultType
* Collects a set of mutually recursive datatypes "datatypes" corresponding to
* encoding type "range" to SyGuS.
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index b49c29c53..ee7247121 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -179,7 +179,6 @@ bool SygusPbe::initialize(Node n,
return false;
}
}
- bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE;
for (const Node& c : candidates)
{
Assert(d_examples.find(c) != d_examples.end());
@@ -203,7 +202,7 @@ bool SygusPbe::initialize(Node n,
for (const Node& e : d_candidate_to_enum[c])
{
TypeNode etn = e.getType();
- d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen);
+ d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false);
d_enum_to_candidate[e] = c;
TNode te = e;
// initialize static symmetry breaking lemmas for it
@@ -229,13 +228,24 @@ bool SygusPbe::initialize(Node n,
{
lem = lem.substitute(tsp, te);
}
- disj.push_back(lem);
+ if (std::find(disj.begin(), disj.end(), lem) == disj.end())
+ {
+ disj.push_back(lem);
+ }
}
}
+ // add its active guard
+ Node ag = d_tds->getActiveGuardForEnumerator(e);
+ Assert(!ag.isNull());
+ disj.push_back(ag.negate());
Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj);
Trace("sygus-pbe") << " static redundant op lemma : " << lem
<< std::endl;
- lemmas.push_back(lem);
+ // Register as a symmetry breaking lemma with the term database.
+ // This will either be processed via a lemma on the output channel
+ // of the sygus extension of the datatypes solver, or internally
+ // encoded as a constraint to an active enumerator.
+ d_tds->registerSymBreakLemma(e, lem, etn, 0, false);
}
}
Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 21079aedc..2bfde2d80 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -346,14 +346,17 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
{
// get the model value of the relevant terms from the master module
std::vector<Node> enum_values;
- bool fullModel = getEnumeratedValues(terms, enum_values);
+ bool activeIncomplete = false;
+ bool fullModel = getEnumeratedValues(terms, enum_values, activeIncomplete);
// if the master requires a full model and the model is partial, we fail
if (!d_master->allowPartialModel() && !fullModel)
{
// we retain the values in d_ev_active_gen_waiting
Trace("cegqi-engine") << "...partial model, fail." << std::endl;
- return true;
+ // if we are partial due to an active enumerator, we may still succeed
+ // on the next call
+ return !activeIncomplete;
}
// the waiting values are passed to the module below, clear
d_ev_active_gen_waiting.clear();
@@ -396,7 +399,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
if (emptyModel)
{
Trace("cegqi-engine") << "...empty model, fail." << std::endl;
- return true;
+ return !activeIncomplete;
}
Assert(candidate_values.empty());
constructed_cand = d_master->constructCandidates(
@@ -650,7 +653,8 @@ void SynthConjecture::preregisterConjecture(Node q)
}
bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
- std::vector<Node>& v)
+ std::vector<Node>& v,
+ bool& activeIncomplete)
{
std::vector<Node> ncheck = n;
n.clear();
@@ -670,7 +674,7 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
continue;
}
}
- Node nv = getEnumeratedValue(e);
+ Node nv = getEnumeratedValue(e, activeIncomplete);
n.push_back(e);
v.push_back(nv);
ret = ret && !nv.isNull();
@@ -692,42 +696,50 @@ class EnumValGeneratorBasic : public EnumValGenerator
/** initialize (do nothing) */
void initialize(Node e) override {}
/** initialize (do nothing) */
- void addValue(Node v) override {}
+ void addValue(Node v) override { d_currTerm = *d_te; }
/**
* Get next returns the next (T-rewriter-unique) value based on the type
* enumerator.
*/
- Node getNext() override
+ bool increment() override
{
+ ++d_te;
if (d_te.isFinished())
{
- return Node::null();
+ d_currTerm = Node::null();
+ return false;
}
- Node next = *d_te;
- ++d_te;
- Node nextb = d_tds->sygusToBuiltin(next);
+ d_currTerm = *d_te;
if (options::sygusSymBreakDynamic())
{
+ Node nextb = d_tds->sygusToBuiltin(d_currTerm);
nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
+ if (d_cache.find(nextb) == d_cache.end())
+ {
+ d_cache.insert(nextb);
+ // only return the current term if not unique
+ }
+ else
+ {
+ d_currTerm = Node::null();
+ }
}
- if (d_cache.find(nextb) == d_cache.end())
- {
- d_cache.insert(nextb);
- return next;
- }
- return getNext();
+ return true;
}
-
+ /** get the current term */
+ Node getCurrent() override { return d_currTerm; }
private:
/** pointer to term database sygus */
TermDbSygus* d_tds;
/** the type enumerator */
TypeEnumerator d_te;
+ /** the current term */
+ Node d_currTerm;
/** cache of (enumerated) builtin values we have enumerated so far */
std::unordered_set<Node, NodeHashFunction> d_cache;
};
-Node SynthConjecture::getEnumeratedValue(Node e)
+Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
{
bool isEnum = d_tds->isEnumerator(e);
@@ -761,15 +773,18 @@ Node SynthConjecture::getEnumeratedValue(Node e)
else
{
// Actively-generated enumerators are currently either variable agnostic
- // or basic.
+ // or basic. The auto mode always prefers the optimized enumerator over
+ // the basic one.
Assert(d_tds->isBasicEnumerator(e));
- if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM)
+ if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM_BASIC)
{
- d_evg[e].reset(new SygusEnumerator(d_tds, this));
+ d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
}
else
{
- d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
+ Assert(options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM
+ || options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO);
+ d_evg[e].reset(new SygusEnumerator(d_tds, this));
}
}
Trace("sygus-active-gen")
@@ -790,6 +805,7 @@ Node SynthConjecture::getEnumeratedValue(Node e)
// Check if there is an (abstract) value absE we were actively generating
// values based on.
Node absE = d_ev_curr_active_gen[e];
+ bool firstTime = false;
if (absE.isNull())
{
// None currently exist. The next abstract value is the model value for e.
@@ -804,9 +820,22 @@ Node SynthConjecture::getEnumeratedValue(Node e)
}
d_ev_curr_active_gen[e] = absE;
iteg->second->addValue(absE);
+ firstTime = true;
}
- Node v = iteg->second->getNext();
- if (v.isNull())
+ bool inc = true;
+ if (!firstTime)
+ {
+ inc = iteg->second->increment();
+ }
+ Node v;
+ if (inc)
+ {
+ v = iteg->second->getCurrent();
+ }
+ Trace("sygus-active-gen-debug") << "...generated " << v
+ << ", with increment success : " << inc
+ << std::endl;
+ if (!inc)
{
// No more concrete values generated from absE.
NodeManager* nm = NodeManager::currentNM();
@@ -852,7 +881,14 @@ Node SynthConjecture::getEnumeratedValue(Node e)
else
{
// We are waiting to send e -> v to the module that requested it.
- d_ev_active_gen_waiting[e] = v;
+ if (v.isNull())
+ {
+ activeIncomplete = true;
+ }
+ else
+ {
+ d_ev_active_gen_waiting[e] = v;
+ }
if (Trace.isOn("sygus-active-gen"))
{
Trace("sygus-active-gen") << "Active-gen : " << e << " : ";
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index ef1b4459f..3a43eb83d 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -49,8 +49,14 @@ class EnumValGenerator
virtual void initialize(Node e) = 0;
/** Inform this generator that abstract value v was enumerated. */
virtual void addValue(Node v) = 0;
- /** Get the next concrete value generated by this class. */
- virtual Node getNext() = 0;
+ /**
+ * Increment this value generator. If this returns false, then we are out of
+ * values. If this returns true, getCurrent(), if non-null, returns the
+ * current term.
+ */
+ virtual bool increment() = 0;
+ /** Get the current concrete value generated by this class. */
+ virtual Node getCurrent() = 0;
};
/** a synthesis conjecture
@@ -193,15 +199,25 @@ class SynthConjecture
* Get model values for terms n, store in vector v. This method returns true
* if and only if all values added to v are non-null.
*
+ * The argument activeIncomplete indicates whether n contains an active
+ * enumerator that is currently not finished enumerating values, but returned
+ * null on a call to getEnumeratedValue. This value is used for determining
+ * whether we should call getEnumeratedValues again within a call to
+ * SynthConjecture::check.
+ *
* It removes terms from n that correspond to "inactive" enumerators, that
* is, enumerators whose values have been exhausted.
*/
- bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v);
+ bool getEnumeratedValues(std::vector<Node>& n,
+ std::vector<Node>& v,
+ bool& activeIncomplete);
/**
* Get model value for term n. If n has a value that was excluded by
- * datatypes sygus symmetry breaking, this method returns null.
+ * datatypes sygus symmetry breaking, this method returns null. It sets
+ * activeIncomplete to true if there is an actively-generated enumerator whose
+ * current value is null but it has not finished generating values.
*/
- Node getEnumeratedValue(Node n);
+ Node getEnumeratedValue(Node n, bool& activeIncomplete);
/** enumerator generators for each actively-generated enumerator */
std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg;
/**
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 435e1a00f..9198f7e56 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -58,6 +58,19 @@ void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign,
}
}
+std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
+{
+ switch (r)
+ {
+ case ROLE_ENUM_POOL: os << "POOL"; break;
+ case ROLE_ENUM_SINGLE_SOLUTION: os << "SINGLE_SOLUTION"; break;
+ case ROLE_ENUM_MULTI_SOLUTION: os << "MULTI_SOLUTION"; break;
+ case ROLE_ENUM_CONSTRAINED: os << "CONSTRAINED"; break;
+ default: os << "enum_" << static_cast<unsigned>(r); break;
+ }
+ return os;
+}
+
TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
: d_quantEngine(qe),
d_syexp(new SygusExplain(this)),
@@ -454,9 +467,8 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
void TermDbSygus::registerEnumerator(Node e,
Node f,
SynthConjecture* conj,
- bool mkActiveGuard,
- bool useSymbolicCons,
- bool isActiveGen)
+ EnumeratorRole erole,
+ bool useSymbolicCons)
{
if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
{
@@ -470,13 +482,6 @@ void TermDbSygus::registerEnumerator(Node e,
d_enum_to_conjecture[e] = conj;
d_enum_to_synth_fun[e] = f;
NodeManager* nm = NodeManager::currentNM();
- if( mkActiveGuard ){
- // make the guard
- Node ag = nm->mkSkolem("eG", nm->booleanType());
- // must ensure it is a literal immediately here
- ag = d_quantEngine->getValuation().ensureLiteral(ag);
- d_enum_to_active_guard[e] = ag;
- }
Trace("sygus-db") << " registering symmetry breaking clauses..."
<< std::endl;
@@ -554,6 +559,66 @@ void TermDbSygus::registerEnumerator(Node e,
}
Trace("sygus-db") << " ...finished" << std::endl;
+ // determine if we are actively-generated
+ bool isActiveGen = false;
+ if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE)
+ {
+ if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED)
+ {
+ // If the enumerator is a solution for a conjecture with multiple
+ // functions, we do not use active generation. If we did, we would have to
+ // generate a "product" of two actively-generated enumerators. That is,
+ // given a conjecture with two functions-to-synthesize with enumerators
+ // e_f and e_g, and if these enumerators generated:
+ // e_f -> t1, ..., tn
+ // e_g -> s1, ..., sm
+ // The sygus module in charge of this conjecture would expect
+ // constructCandidates calls of the form
+ // (e_f,e_g) -> (ti, sj)
+ // for each i,j. We instead use passive enumeration in this case.
+ //
+ // If the enumerator is constrained, it cannot be actively generated.
+ }
+ else if (erole == ROLE_ENUM_POOL)
+ {
+ // If the enumerator is used for generating a pool of values, we always
+ // use active generation.
+ isActiveGen = true;
+ }
+ else if (erole == ROLE_ENUM_SINGLE_SOLUTION)
+ {
+ // If the enumerator is the single function-to-synthesize, if auto is
+ // enabled, we infer whether it is better to enable active generation.
+ if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO)
+ {
+ // We use active generation if the grammar of the enumerator does not
+ // have ITE and is not Boolean. Experimentally, it is better to
+ // use passive generation for these cases since it enables useful
+ // search space pruning techniques, e.g. evaluation unfolding,
+ // conjecture-specific symmetry breaking. Also, if sygus-stream is
+ // enabled, we always use active generation, since the use cases of
+ // sygus stream are to find many solutions to an easy problem, where
+ // the bottleneck often becomes the large number of "exclude the current
+ // solution" clauses.
+ const Datatype& dt = et.getDatatype();
+ if (options::sygusStream()
+ || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean()))
+ {
+ isActiveGen = true;
+ }
+ }
+ else
+ {
+ isActiveGen = true;
+ }
+ }
+ else
+ {
+ Unreachable("Unknown enumerator mode in registerEnumerator");
+ }
+ }
+ Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole
+ << " returned " << isActiveGen << std::endl;
// Currently, actively-generated enumerators are either basic or variable
// agnostic.
bool isVarAgnostic =
@@ -607,6 +672,22 @@ void TermDbSygus::registerEnumerator(Node e,
}
d_enum_active_gen[e] = isActiveGen;
d_enum_basic[e] = isActiveGen && !isVarAgnostic;
+
+ // We make an active guard if we will be explicitly blocking solutions for
+ // the enumerator. This is the case if the role of the enumerator is to
+ // populate a pool of terms, or (some cases) of when it is actively generated.
+ if (isActiveGen || erole == ROLE_ENUM_POOL)
+ {
+ // make the guard
+ Node ag = nm->mkSkolem("eG", nm->booleanType());
+ // must ensure it is a literal immediately here
+ ag = d_quantEngine->getValuation().ensureLiteral(ag);
+ // must ensure that it is asserted as a literal before we begin solving
+ Node lem = nm->mkNode(OR, ag, ag.negate());
+ d_quantEngine->getOutputChannel().requirePhase(ag, true);
+ d_quantEngine->getOutputChannel().lemma(lem);
+ d_enum_to_active_guard[e] = ag;
+ }
}
bool TermDbSygus::isEnumerator(Node e) const
@@ -694,14 +775,13 @@ void TermDbSygus::getEnumerators(std::vector<Node>& mts)
}
}
-void TermDbSygus::registerSymBreakLemma(Node e,
- Node lem,
- TypeNode tn,
- unsigned sz)
+void TermDbSygus::registerSymBreakLemma(
+ Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl)
{
d_enum_to_sb_lemmas[e].push_back(lem);
d_sb_lemma_to_type[lem] = tn;
d_sb_lemma_to_size[lem] = sz;
+ d_sb_lemma_to_isTempl[lem] = isTempl;
}
bool TermDbSygus::hasSymBreakLemmas(std::vector<Node>& enums) const
@@ -740,6 +820,13 @@ unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const
return it->second;
}
+bool TermDbSygus::isSymBreakLemmaTemplate(Node lem) const
+{
+ std::map<Node, bool>::const_iterator it = d_sb_lemma_to_isTempl.find(lem);
+ Assert(it != d_sb_lemma_to_isTempl.end());
+ return it->second;
+}
+
void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); }
bool TermDbSygus::isRegistered(TypeNode tn) const
@@ -756,9 +843,16 @@ void TermDbSygus::toStreamSygus(const char* c, Node n)
{
if (Trace.isOn(c))
{
- std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n);
- Trace(c) << ss.str();
+ if (n.isNull())
+ {
+ Trace(c) << n;
+ }
+ else
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n);
+ Trace(c) << ss.str();
+ }
}
}
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 713e322a4..7a522ded6 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -48,6 +48,23 @@ class TypeNodeIdTrie
void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount);
};
+/** role for registering an enumerator */
+enum EnumeratorRole
+{
+ /** The enumerator populates a pool of terms (e.g. for PBE). */
+ ROLE_ENUM_POOL,
+ /** The enumerator is the single solution of the problem. */
+ ROLE_ENUM_SINGLE_SOLUTION,
+ /**
+ * The enumerator is part of the solution of the problem (e.g. multiple
+ * functions to synthesize).
+ */
+ ROLE_ENUM_MULTI_SOLUTION,
+ /** The enumerator must satisfy some set of constraints */
+ ROLE_ENUM_CONSTRAINED,
+};
+std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
+
// TODO :issue #1235 split and document this class
class TermDbSygus {
public:
@@ -80,29 +97,32 @@ class TermDbSygus {
//------------------------------enumerators
/**
* Register a variable e that we will do enumerative search on.
+ *
* conj : the conjecture that the enumeration of e is for.
- * f : the synth-fun that the enumeration of e is for.
- * mkActiveGuard : whether we want to make an active guard for e
- * (see d_enum_to_active_guard),
- * useSymbolicCons : whether we want model values for e to include symbolic
- * constructors like the "any constant" variable.
- * isActiveGen : if this flag is true, the enumerator will be
- * actively-generated based on the mode specified by --sygus-active-gen.
+ *
+ * f : the synth-fun that the enumeration of e is for.Notice that enumerator
+ * e may not be one-to-one with f in synthesis-through-unification approaches
+ * (e.g. decision tree construction for PBE synthesis).
+ *
+ * erole : the role of this enumerator (see definition of EnumeratorRole).
+ * Depending on this and the policy for actively-generated enumerators
+ * (--sygus-active-gen), the enumerator may be "actively-generated".
* For example, if --sygus-active-gen=var-agnostic, then the enumerator will
* only generate values whose variables are in canonical order (only x1-x2
* and not x2-x1 will be generated, assuming x1 and x2 are in the same
* "subclass", see getSubclassForVar).
*
- * Notice that enumerator e may not be one-to-one with f in
- * synthesis-through-unification approaches (e.g. decision tree construction
- * for PBE synthesis).
+ * useSymbolicCons : whether we want model values for e to include symbolic
+ * constructors like the "any constant" variable.
+ *
+ * An "active guard" may be allocated by this method for e based on erole
+ * and the policies for active generation.
*/
void registerEnumerator(Node e,
Node f,
SynthConjecture* conj,
- bool mkActiveGuard = false,
- bool useSymbolicCons = false,
- bool isActiveGen = false);
+ EnumeratorRole erole,
+ bool useSymbolicCons = false);
/** is e an enumerator registered with this class? */
bool isEnumerator(Node e) const;
/** return the conjecture e is associated with */
@@ -150,12 +170,13 @@ class TermDbSygus {
*
* tn : the (sygus datatype) type that lem applies to, i.e. the
* type of terms that lem blocks models for,
- * sz : the minimum size of terms that the lem blocks.
- *
- * Notice that the symmetry breaking lemma template should be relative to x,
- * where x is returned by the call to getFreeVar( tn, 0 ) in this class.
+ * sz : the minimum size of terms that the lem blocks,
+ * isTempl : if this flag is false, then lem is a (concrete) lemma.
+ * If this flag is true, then lem is a symmetry breaking lemma template
+ * over x, where x is returned by the call to getFreeVar( tn, 0 ).
*/
- void registerSymBreakLemma(Node e, Node lem, TypeNode tn, unsigned sz);
+ void registerSymBreakLemma(
+ Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl = true);
/** Has symmetry breaking lemmas been added for any enumerator? */
bool hasSymBreakLemmas(std::vector<Node>& enums) const;
/** Get symmetry breaking lemmas
@@ -168,6 +189,8 @@ class TermDbSygus {
TypeNode getTypeForSymBreakLemma(Node lem) const;
/** Get the minimum size of terms symmetry breaking lemma lem applies to */
unsigned getSizeForSymBreakLemma(Node lem) const;
+ /** Returns true if lem is a lemma template, false if lem is a lemma */
+ bool isSymBreakLemmaTemplate(Node lem) const;
/** Clear information about symmetry breaking lemmas for enumerator e */
void clearSymBreakLemmas(Node e);
//------------------------------end enumerators
@@ -324,6 +347,8 @@ class TermDbSygus {
std::map<Node, TypeNode> d_sb_lemma_to_type;
/** mapping from symmetry breaking lemmas to size */
std::map<Node, unsigned> d_sb_lemma_to_size;
+ /** mapping from symmetry breaking lemmas to whether they are templates */
+ std::map<Node, bool> d_sb_lemma_to_isTempl;
/** enumerators to whether they are actively-generated */
std::map<Node, bool> d_enum_active_gen;
/** enumerators to whether they are variable agnostic */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback