};
typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
+/**
+ * Attribute true for enumerators whose current model values have been excluded
+ * by sygus symmetry breaking. This is set by the datatypes sygus solver during
+ * LAST_CALL effort checks for each active sygus enumerator.
+ */
+struct SygusSymBreakExcAttributeId
+{
+};
+typedef expr::Attribute<SygusSymBreakExcAttributeId, bool>
+ SygusSymBreakExcAttribute;
+
namespace datatypes {
class DatatypesRewriter {
// register the search value ( prog -> progv ), this may invoke symmetry breaking
if( options::sygusSymBreakDynamic() ){
Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas);
+ SygusSymBreakExcAttribute ssbea;
+ prog.setAttribute(ssbea, rsv.isNull());
if (rsv.isNull())
{
Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
}
Assert(!d_this.isNull());
NodeManager* nm = NodeManager::currentNM();
+ Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s
+ << " for " << d_this << std::endl;
return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s)));
}
->toStreamSygus(ss, m_eu);
Trace("cegis") << ss.str() << std::endl;
}
+ if (m_eu.isNull())
+ {
+ // A condition enumerator was excluded by symmetry breaking, fail.
+ // TODO (#2498): either move conditions to getTermList or handle
+ // partial models in this module.
+ return false;
+ }
unif_values[index][e].push_back(m_eu);
}
// inter-enumerator symmetry breaking for return values
*/
virtual void getTermList(const std::vector<Node>& candidates,
std::vector<Node>& terms) = 0;
+ /** allow partial model
+ *
+ * This method returns true if this module does not require that all
+ * terms returned by getTermList have "proper" model values when calling
+ * constructCandidates. A term may have a model value that is not proper
+ * if is excluded by symmetry breaking, e.g. x+0 is not proper. All model
+ * values that are not proper are replaced by "null" when calling
+ * constructCandidates.
+ */
+ virtual bool allowPartialModel() { return false; }
/** construct candidate
*
* This function takes as input:
}
}
+bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); }
+
bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
Trace("sygus-pbe-enum") << " " << enums[i] << " -> ";
TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]);
Trace("sygus-pbe-enum") << std::endl;
- unsigned sz = d_tds->getSygusTermSize( enum_values[i] );
- szs.push_back(sz);
- if( i==0 || sz<min_term_size ){
- min_term_size = sz;
+ if (!enum_values[i].isNull())
+ {
+ unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
+ szs.push_back(sz);
+ if (i == 0 || sz < min_term_size)
+ {
+ min_term_size = sz;
+ }
+ }
+ else
+ {
+ szs.push_back(0);
}
}
// Assume two enumerators of types T1 and T2.
std::vector<unsigned> enum_consider;
for (unsigned i = 0, esize = enums.size(); i < esize; i++)
{
- Assert(szs[i] >= min_term_size);
- int diff = szs[i] - min_term_size;
- if (!options::sygusPbeMultiFair() || diff <= diffAllow)
+ if (!enum_values[i].isNull())
{
- enum_consider.push_back( i );
+ Assert(szs[i] >= min_term_size);
+ int diff = szs[i] - min_term_size;
+ if (!options::sygusPbeMultiFair() || diff <= diffAllow)
+ {
+ enum_consider.push_back(i);
+ }
}
}
*/
void getTermList(const std::vector<Node>& candidates,
std::vector<Node>& terms) override;
+ /**
+ * PBE allows partial models to handle multiple enumerators if we are not
+ * using a strictly fair enumeration strategy.
+ */
+ bool allowPartialModel() override;
/** construct candidates
*
* This function attempts to use unification-based approaches for constructing
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
// get the model value of the relevant terms from the master module
std::vector<Node> enum_values;
- getModelValues(terms, enum_values);
+ bool fullModel = getModelValues(terms, enum_values);
+
+ // if the master requires a full model and the model is partial, we fail
+ if (!d_master->allowPartialModel() && !fullModel)
+ {
+ Trace("cegqi-check") << "...partial model, fail." << std::endl;
+ return;
+ }
if (!constructed_cand)
{
d_ceg_si->preregisterConjecture(q);
}
-void SynthConjecture::getModelValues(std::vector<Node>& n, std::vector<Node>& v)
+bool SynthConjecture::getModelValues(std::vector<Node>& n, std::vector<Node>& v)
{
+ bool ret = true;
Trace("cegqi-engine") << " * Value is : ";
for (unsigned i = 0; i < n.size(); i++)
{
Node nv = getModelValue(n[i]);
v.push_back(nv);
+ ret = ret && !nv.isNull();
if (Trace.isOn("cegqi-engine"))
{
- TypeNode tn = nv.getType();
- Trace("cegqi-engine") << n[i] << " -> ";
+ Node onv = nv.isNull() ? d_qe->getModel()->getValue(n[i]) : nv;
+ TypeNode tn = onv.getType();
std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv);
- Trace("cegqi-engine") << ss.str() << " ";
- if (Trace.isOn("cegqi-engine-rr"))
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
+ Trace("cegqi-engine") << n[i] << " -> ";
+ if (nv.isNull())
+ {
+ Trace("cegqi-engine") << "[EXC: " << ss.str() << "] ";
+ }
+ else
{
- Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn);
- bv = Rewriter::rewrite(bv);
- Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+ Trace("cegqi-engine") << ss.str() << " ";
+ if (Trace.isOn("cegqi-engine-rr"))
+ {
+ Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn);
+ bv = Rewriter::rewrite(bv);
+ Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+ }
}
}
- Assert(!nv.isNull());
}
Trace("cegqi-engine") << std::endl;
+ return ret;
}
Node SynthConjecture::getModelValue(Node n)
{
Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
- return d_qe->getModel()->getValue(n);
+ if (n.getAttribute(SygusSymBreakExcAttribute()))
+ {
+ // if the current model value of n was excluded by symmetry breaking, then
+ // it does not have a proper model value that we should consider, thus we
+ // return null.
+ return Node::null();
+ }
+ Node mv = d_qe->getModel()->getValue(n);
+ return mv;
}
void SynthConjecture::debugPrint(const char* c)
void assign(Node q);
/** has a conjecture been assigned to this class */
bool isAssigned() { return !d_embed_quant.isNull(); }
- /** get model values for terms n, store in vector v */
- void getModelValues(std::vector<Node>& n, std::vector<Node>& v);
- /** get model value for term n */
+ /**
+ * 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.
+ */
+ bool getModelValues(std::vector<Node>& n, std::vector<Node>& v);
+ /**
+ * Get model value for term n. If n has a value that was excluded by
+ * datatypes sygus symmetry breaking, this method returns null.
+ */
Node getModelValue(Node n);
/** get utility for static preprocessing and analysis of conjectures */
bool SynthEngine::needsCheck(Theory::Effort e)
{
- return !d_quantEngine->getTheoryEngine()->needCheck()
- && e >= Theory::EFFORT_LAST_CALL;
+ return e >= Theory::EFFORT_LAST_CALL;
}
QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
projects / cvc5.git / commitdiff