// Streaming is incompatible with techniques that focus the search towards
// finding a single solution. This currently includes the PBE solver and
// static template inference for invariant synthesis.
- if (!options::sygusSymBreakPbe.wasSetByUser())
- {
- options::sygusSymBreakPbe.set(false);
- }
if (!options::sygusUnifPbe.wasSetByUser())
{
options::sygusUnifPbe.set(false);
+ // also disable PBE-specific symmetry breaking unless PBE was enabled
+ if (!options::sygusSymBreakPbe.wasSetByUser())
+ {
+ options::sygusSymBreakPbe.set(false);
+ }
}
if (!options::sygusInvTemplMode.wasSetByUser())
{
namespace theory {
namespace quantifiers {
-SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
+SygusUnif::SygusUnif()
+ : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false)
+{
+}
SygusUnif::~SygusUnif() {}
void SygusUnif::initializeCandidate(
d_strategy[f].initialize(qe, f, enums);
}
+Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
+{
+ unsigned minSize = 0;
+ Node minTerm;
+ std::map<Node, unsigned>::iterator it;
+ for (const Node& n : terms)
+ {
+ it = d_termToSize.find(n);
+ unsigned ssize = 0;
+ if (it == d_termToSize.end())
+ {
+ ssize = d_tds->getSygusTermSize(n);
+ d_termToSize[n] = ssize;
+ }
+ else
+ {
+ ssize = it->second;
+ }
+ if (minTerm.isNull() || ssize < minSize)
+ {
+ minTerm = n;
+ minSize = ssize;
+ }
+ }
+ return minTerm;
+}
+
Node SygusUnif::constructBestSolvedTerm(Node e, const std::vector<Node>& solved)
{
Assert(!solved.empty());
+ if (d_enableMinimality)
+ {
+ return getMinimalTerm(solved);
+ }
return solved[0];
}
const std::map<Node, unsigned>& total_inc,
const std::map<Node, std::vector<unsigned> >& incr);
//------------------------------ end constructing solutions
+ /** map terms to their sygus size */
+ std::map<Node, unsigned> d_termToSize;
+ /**
+ * Whether to ensure terms selected by the above methods lead to minimal
+ * solutions.
+ */
+ bool d_enableMinimality;
+ /** returns the term whose sygus size is minimal among those in terms */
+ Node getMinimalTerm(const std::vector<Node>& terms);
};
} /* CVC4::theory::quantifiers namespace */
if (!d_term.isNull())
{
subsumed.push_back(d_term);
- if (!checkExistsOnly)
- {
- // remove it if checkExistsOnly = false
- d_term = Node::null();
- }
+ // If we are only interested in feasibility, we could set d_term to null
+ // here. However, d_term still could be useful, since it may be
+ // smaller than t and suffice as a solution under some condition.
+ // As a simple example, consider predicate synthesis and a case where we
+ // enumerate a C that is correct for all I/O points whose output is
+ // true. Then, C subsumes true. However, true may be preferred, e.g.
+ // to generate a solution ite( C, true, D ) instead of ite( C, C, D ),
+ // since true is conditionally correct under C, and is smaller than C.
}
}
else
SygusUnifIo::SygusUnifIo()
: d_check_sol(false),
d_cond_count(0),
+ d_sol_term_size(0),
d_sol_cons_nondet(false),
d_solConsUsingInfoGain(false)
{
Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
{
Node c = d_candidate;
- if (!d_solution.isNull())
+ if (!d_solution.isNull() && !options::sygusStream())
{
// already has a solution
return d_solution;
Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
<< std::endl;
d_check_sol = false;
+ Node newSolution;
d_solConsUsingInfoGain = false;
// try multiple times if we have done multiple conditions, due to
// non-determinism
- unsigned sol_term_size = 0;
for (unsigned i = 0; i <= d_cond_count; i++)
{
Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
if (!vcc.isNull()
&& (d_solution.isNull()
|| (!d_solution.isNull()
- && d_tds->getSygusTermSize(vcc) < sol_term_size)))
+ && d_tds->getSygusTermSize(vcc) < d_sol_term_size)))
{
Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc
<< std::endl;
Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
d_solution = vcc;
- sol_term_size = d_tds->getSygusTermSize(vcc);
+ newSolution = vcc;
+ d_sol_term_size = d_tds->getSygusTermSize(vcc);
+ Trace("sygus-pbe-sol")
+ << "PBE solution size: " << d_sol_term_size << std::endl;
// We've determined its feasible, now, enable information gain and
// retry. We do this since information gain comes with an overhead,
// and we want testing feasibility to be fast.
if (!d_solConsUsingInfoGain)
{
+ // we permanently enable information gain and minimality now
d_solConsUsingInfoGain = true;
+ d_enableMinimality = true;
i = 0;
}
}
break;
}
}
- if (!d_solution.isNull())
+ if (!newSolution.isNull())
{
- return d_solution;
+ return newSolution;
}
Trace("sygus-pbe") << "...failed to solve." << std::endl;
}
// initially set minEntropy to > 1.0.
double minEntropy = 2.0;
unsigned bestIndex = 0;
+ int numEqual = 1;
for (unsigned j = 0; j < nconds; j++)
{
// To compute the entropy for a condition C, for pair of terms (s, t), let
}
}
Trace("sygus-sui-dt-igain") << "..." << entropySum << std::endl;
- if (entropySum < minEntropy)
+ // either less, or equal and coin flip passes
+ bool doSet = false;
+ if (entropySum == minEntropy)
+ {
+ numEqual++;
+ if (Random::getRandom().pickWithProb(double(1) / double(numEqual)))
+ {
+ doSet = true;
+ }
+ }
+ else if (entropySum < minEntropy)
+ {
+ doSet = true;
+ numEqual = 1;
+ }
+ if (doSet)
{
minEntropy = entropySum;
bestIndex = j;
projects / cvc5.git / commitdiff