{
d_constraints.reset();
d_assignment.clear();
+ d_nextIntervalId = 1;
}
void CDCAC::computeVariableOrdering()
m.pushDownPolys(d, d_variableOrdering[cur_variable]);
if (!is_minus_infinity(get_lower(i))) l = m;
if (!is_plus_infinity(get_upper(i))) u = m;
- res.emplace_back(CACInterval{i, l, u, m, d, {n}});
+ res.emplace_back(CACInterval{d_nextIntervalId++, i, l, u, m, d, {n}});
if (isProofEnabled())
{
d_proof->addDirect(
d_assignment,
sc,
i,
- n);
+ n,
+ res.back().d_id);
}
}
}
PolyVector CDCAC::requiredCoefficients(const poly::Polynomial& p)
{
- if (Trace.isOn("cdcac"))
+ if (Trace.isOn("cdcac::projection"))
{
- Trace("cdcac") << "Poly: " << p << " over " << d_assignment << std::endl;
- Trace("cdcac") << "Lazard: "
- << requiredCoefficientsLazard(p, d_assignment) << std::endl;
- Trace("cdcac") << "LMod: "
- << requiredCoefficientsLazardModified(
- p, d_assignment, d_constraints.varMapper())
- << std::endl;
- Trace("cdcac") << "Original: "
- << requiredCoefficientsOriginal(p, d_assignment)
- << std::endl;
+ Trace("cdcac::projection")
+ << "Poly: " << p << " over " << d_assignment << std::endl;
+ Trace("cdcac::projection")
+ << "Lazard: " << requiredCoefficientsLazard(p, d_assignment)
+ << std::endl;
+ Trace("cdcac::projection")
+ << "LMod: "
+ << requiredCoefficientsLazardModified(
+ p, d_assignment, d_constraints.varMapper())
+ << std::endl;
+ Trace("cdcac::projection")
+ << "Original: " << requiredCoefficientsOriginal(p, d_assignment)
+ << std::endl;
}
switch (options().arith.nlCadProjection)
{
}
for (const auto& p : i.d_mainPolys)
{
- Trace("cdcac") << "Discriminant of " << p << " -> " << discriminant(p)
- << std::endl;
+ Trace("cdcac::projection")
+ << "Discriminant of " << p << " -> " << discriminant(p) << std::endl;
// Add all discriminants
res.add(discriminant(p));
for (const auto& q : requiredCoefficients(p))
{
// Add all required coefficients
- Trace("cdcac") << "Coeff of " << p << " -> " << q << std::endl;
+ Trace("cdcac::projection")
+ << "Coeff of " << p << " -> " << q << std::endl;
res.add(q);
}
for (const auto& q : i.d_lowerPolys)
if (p == q) continue;
// Check whether p(s \times a) = 0 for some a <= l
if (!hasRootBelow(q, get_lower(i.d_interval))) continue;
- Trace("cdcac") << "Resultant of " << p << " and " << q << " -> "
- << resultant(p, q) << std::endl;
+ Trace("cdcac::projection") << "Resultant of " << p << " and " << q
+ << " -> " << resultant(p, q) << std::endl;
res.add(resultant(p, q));
}
for (const auto& q : i.d_upperPolys)
if (p == q) continue;
// Check whether p(s \times a) = 0 for some a >= u
if (!hasRootAbove(q, get_upper(i.d_interval))) continue;
- Trace("cdcac") << "Resultant of " << p << " and " << q << " -> "
- << resultant(p, q) << std::endl;
+ Trace("cdcac::projection") << "Resultant of " << p << " and " << q
+ << " -> " << resultant(p, q) << std::endl;
res.add(resultant(p, q));
}
}
{
for (const auto& q : intervals[i + 1].d_lowerPolys)
{
- Trace("cdcac") << "Resultant of " << p << " and " << q << " -> "
- << resultant(p, q) << std::endl;
+ Trace("cdcac::projection") << "Resultant of " << p << " and " << q
+ << " -> " << resultant(p, q) << std::endl;
res.add(resultant(p, q));
}
}
if (lower == upper)
{
// construct a point interval
- return CACInterval{
- poly::Interval(lower, false, upper, false), l, u, m, d, {}};
+ return CACInterval{d_nextIntervalId++,
+ poly::Interval(lower, false, upper, false),
+ l,
+ u,
+ m,
+ d,
+ {}};
}
else
{
// construct an open interval
Assert(lower < upper);
- return CACInterval{
- poly::Interval(lower, true, upper, true), l, u, m, d, {}};
+ return CACInterval{d_nextIntervalId++,
+ poly::Interval(lower, true, upper, true),
+ l,
+ u,
+ m,
+ d,
+ {}};
}
}
-std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
- bool returnFirstInterval)
+std::vector<CACInterval> CDCAC::getUnsatCoverImpl(std::size_t curVariable,
+ bool returnFirstInterval)
{
- if (isProofEnabled())
- {
- d_proof->startRecursive();
- }
Trace("cdcac") << "Looking for unsat cover for "
<< d_variableOrdering[curVariable] << std::endl;
std::vector<CACInterval> intervals = getUnsatIntervals(curVariable);
if (isProofEnabled())
{
d_proof->startScope();
+ d_proof->startRecursive();
}
// Recurse to next variable
- auto cov = getUnsatCover(curVariable + 1);
+ auto cov = getUnsatCoverImpl(curVariable + 1);
if (cov.empty())
{
// Found SAT!
intervals.emplace_back(newInterval);
if (isProofEnabled())
{
+ d_proof->endRecursive(newInterval.d_id);
auto cell = d_proof->constructCell(
d_constraints.varMapper()(d_variableOrdering[curVariable]),
newInterval,
Trace("cdcac") << "-> " << i.d_interval << std::endl;
}
}
+ return intervals;
+}
+
+std::vector<CACInterval> CDCAC::getUnsatCover(bool returnFirstInterval)
+{
+ if (isProofEnabled())
+ {
+ d_proof->startRecursive();
+ }
+ auto res = getUnsatCoverImpl(0, returnFirstInterval);
if (isProofEnabled())
{
- d_proof->endRecursive();
+ d_proof->endRecursive(0);
}
- return intervals;
+ return res;
}
void CDCAC::startNewProof()
poly::Integer below = poly::floor(value);
poly::Integer above = poly::ceil(value);
// construct var \in (below, above)
- return CACInterval{poly::Interval(below, above),
+ return CACInterval{d_nextIntervalId++,
+ poly::Interval(below, above),
{var - below},
{var - above},
{var - below, var - above},
{
if (isProofEnabled())
{
- std::vector<CACInterval> allIntervals = intervals;
cleanIntervals(intervals);
- d_proof->pruneChildren([&allIntervals, &intervals](std::size_t i) {
- return std::find(intervals.begin(), intervals.end(), allIntervals[i])
+ d_proof->pruneChildren([&intervals](std::size_t id) {
+ return std::find_if(intervals.begin(),
+ intervals.end(),
+ [id](const CACInterval& i) { return i.d_id == id; })
!= intervals.end();
});
}
std::size_t cur_variable,
const poly::Value& sample);
+ /**
+ * Internal implementation of getUnsatCover().
+ * @param curVariable The id of the variable (within d_variableOrdering) to
+ * be considered. This argument is used to manage the recursion internally and
+ * should always be zero if called externally.
+ * @param returnFirstInterval If true, the function returns after the first
+ * interval obtained from a recursive call. The result is not (necessarily) an
+ * unsat cover, but merely a list of infeasible intervals.
+ */
+ std::vector<CACInterval> getUnsatCoverImpl(std::size_t curVariable = 0,
+ bool returnFirstInterval = false);
+
/**
* Main method that checks for the satisfiability of the constraints.
* Recursively explores possible assignments and excludes regions based on the
* be obtained from d_assignment. If the covering is not empty, the result is
* UNSAT and an infeasible subset can be extracted from the returned covering.
* Implements Algorithm 2.
- * @param curVariable The id of the variable (within d_variableOrdering) to
- * be considered. This argument is used to manage the recursion internally and
- * should always be zero if called externally.
+ * This method itself only takes care of the outermost proof scope and calls
+ * out to getUnsatCoverImpl() with curVariable set to zero.
* @param returnFirstInterval If true, the function returns after the first
* interval obtained from a recursive call. The result is not (necessarily) an
* unsat cover, but merely a list of infeasible intervals.
*/
- std::vector<CACInterval> getUnsatCover(std::size_t curVariable = 0,
- bool returnFirstInterval = false);
+ std::vector<CACInterval> getUnsatCover(bool returnFirstInterval = false);
void startNewProof();
/**
/** The proof generator */
std::unique_ptr<CADProofGenerator> d_proof;
+
+ /** The next interval id */
+ size_t d_nextIntervalId = 1;
};
} // namespace cad
d_current = d_proofs.allocateProof();
}
void CADProofGenerator::startRecursive() { d_current->openChild(); }
-void CADProofGenerator::endRecursive()
+void CADProofGenerator::endRecursive(size_t intervalId)
{
- d_current->setCurrent(PfRule::ARITH_NL_CAD_RECURSIVE, {}, {d_false}, d_false);
+ d_current->setCurrent(
+ intervalId, PfRule::ARITH_NL_CAD_RECURSIVE, {}, {d_false}, d_false);
d_current->closeChild();
}
void CADProofGenerator::startScope()
}
void CADProofGenerator::endScope(const std::vector<Node>& args)
{
- d_current->setCurrent(PfRule::SCOPE, {}, args, d_false);
+ d_current->setCurrent(0, PfRule::SCOPE, {}, args, d_false);
d_current->closeChild();
}
const poly::Assignment& a,
poly::SignCondition& sc,
const poly::Interval& interval,
- Node constraint)
+ Node constraint,
+ size_t intervalId)
{
if (is_minus_infinity(get_lower(interval))
&& is_plus_infinity(get_upper(interval)))
{
// "Full conflict", constraint excludes (-inf,inf)
d_current->openChild();
- d_current->setCurrent(
- PfRule::ARITH_NL_CAD_DIRECT, {constraint}, {d_false}, d_false);
+ d_current->setCurrent(intervalId,
+ PfRule::ARITH_NL_CAD_DIRECT,
+ {constraint},
+ {d_false},
+ d_false);
d_current->closeChild();
return;
}
// Add to proof manager
startScope();
d_current->openChild();
- d_current->setCurrent(
- PfRule::ARITH_NL_CAD_DIRECT, {constraint}, {d_false}, d_false);
+ d_current->setCurrent(intervalId,
+ PfRule::ARITH_NL_CAD_DIRECT,
+ {constraint},
+ {d_false},
+ d_false);
d_current->closeChild();
endScope(res);
}
projects / cvc5.git / commitdiff