summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/nl/cad/cdcac.cpp46
-rw-r--r--src/theory/arith/nl/cad/cdcac.h9
-rw-r--r--src/theory/arith/nl/cad_solver.cpp43
-rw-r--r--src/theory/arith/nl/cad_solver.h8
-rw-r--r--src/theory/arith/nl/poly_conversion.cpp13
5 files changed, 92 insertions, 27 deletions
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index 9c58a0007..0dcf7f7a7 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -344,15 +344,16 @@ CACInterval CDCAC::intervalFromCharacterization(
}
}
-std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
+std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
+ bool returnFirstInterval)
{
Trace("cdcac") << "Looking for unsat cover for "
- << d_variableOrdering[cur_variable] << std::endl;
- std::vector<CACInterval> intervals = getUnsatIntervals(cur_variable);
+ << d_variableOrdering[curVariable] << std::endl;
+ std::vector<CACInterval> intervals = getUnsatIntervals(curVariable);
if (Trace.isOn("cdcac"))
{
- Trace("cdcac") << "Unsat intervals for " << d_variableOrdering[cur_variable]
+ Trace("cdcac") << "Unsat intervals for " << d_variableOrdering[curVariable]
<< ":" << std::endl;
for (const auto& i : intervals)
{
@@ -362,30 +363,30 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
}
poly::Value sample;
- while (sampleOutsideWithInitial(intervals, sample, cur_variable))
+ while (sampleOutsideWithInitial(intervals, sample, curVariable))
{
- if (!checkIntegrality(cur_variable, sample))
+ if (!checkIntegrality(curVariable, sample))
{
// the variable is integral, but the sample is not.
Trace("cdcac") << "Used " << sample << " for integer variable "
- << d_variableOrdering[cur_variable] << std::endl;
- auto new_interval = buildIntegralityInterval(cur_variable, sample);
- Trace("cdcac") << "Adding integrality interval "
- << new_interval.d_interval << std::endl;
- intervals.emplace_back(new_interval);
+ << d_variableOrdering[curVariable] << std::endl;
+ auto newInterval = buildIntegralityInterval(curVariable, sample);
+ Trace("cdcac") << "Adding integrality interval " << newInterval.d_interval
+ << std::endl;
+ intervals.emplace_back(newInterval);
cleanIntervals(intervals);
continue;
}
- d_assignment.set(d_variableOrdering[cur_variable], sample);
+ d_assignment.set(d_variableOrdering[curVariable], sample);
Trace("cdcac") << "Sample: " << d_assignment << std::endl;
- if (cur_variable == d_variableOrdering.size() - 1)
+ if (curVariable == d_variableOrdering.size() - 1)
{
// We have a full assignment. SAT!
Trace("cdcac") << "Found full assignment: " << d_assignment << std::endl;
return {};
}
// Recurse to next variable
- auto cov = getUnsatCover(cur_variable + 1);
+ auto cov = getUnsatCover(curVariable + 1);
if (cov.empty())
{
// Found SAT!
@@ -396,12 +397,17 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
auto characterization = constructCharacterization(cov);
Trace("cdcac") << "Characterization: " << characterization << std::endl;
- d_assignment.unset(d_variableOrdering[cur_variable]);
+ d_assignment.unset(d_variableOrdering[curVariable]);
+
+ auto newInterval =
+ intervalFromCharacterization(characterization, curVariable, sample);
+ newInterval.d_origins = collectConstraints(cov);
+ intervals.emplace_back(newInterval);
- auto new_interval =
- intervalFromCharacterization(characterization, cur_variable, sample);
- new_interval.d_origins = collectConstraints(cov);
- intervals.emplace_back(new_interval);
+ if (returnFirstInterval)
+ {
+ return intervals;
+ }
Trace("cdcac") << "Added " << intervals.back().d_interval << std::endl;
Trace("cdcac") << "\tlower: " << intervals.back().d_lowerPolys
@@ -421,7 +427,7 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
if (Trace.isOn("cdcac"))
{
Trace("cdcac") << "Returning intervals for "
- << d_variableOrdering[cur_variable] << ":" << std::endl;
+ << d_variableOrdering[curVariable] << ":" << std::endl;
for (const auto& i : intervals)
{
Trace("cdcac") << "-> " << i.d_interval << std::endl;
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 3434b23e6..a6049ad61 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -131,8 +131,15 @@ class CDCAC
* 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.
+ * @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 cur_variable = 0);
+ std::vector<CACInterval> getUnsatCover(std::size_t curVariable = 0,
+ bool returnFirstInterval = false);
private:
/**
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index a2fc1e1f1..bb1ef9911 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -106,6 +106,49 @@ std::vector<NlLemma> CadSolver::checkFull()
#endif
}
+std::vector<NlLemma> CadSolver::checkPartial()
+{
+#ifdef CVC4_POLY_IMP
+ std::vector<NlLemma> lems;
+ auto covering = d_CAC.getUnsatCover(0, true);
+ if (covering.empty())
+ {
+ d_foundSatisfiability = true;
+ Trace("nl-cad") << "SAT: " << d_CAC.getModel() << std::endl;
+ }
+ else
+ {
+ auto* nm = NodeManager::currentNM();
+ Node first_var =
+ d_CAC.getConstraints().varMapper()(d_CAC.getVariableOrdering()[0]);
+ for (const auto& interval : covering)
+ {
+ Node premise;
+ Assert(!interval.d_origins.empty());
+ if (interval.d_origins.size() == 1)
+ {
+ premise = interval.d_origins[0];
+ }
+ else
+ {
+ premise = nm->mkNode(Kind::AND, interval.d_origins);
+ }
+ Node conclusion =
+ excluding_interval_to_lemma(first_var, interval.d_interval);
+ Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion);
+ Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl;
+ lems.emplace_back(lemma, Inference::CAD_EXCLUDED_INTERVAL);
+ }
+ }
+ return lems;
+#else
+ Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
+ "with --poly."
+ << std::endl;
+ return {};
+#endif
+}
+
bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions)
{
#ifdef CVC4_POLY_IMP
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 9fb243897..6f6c0d43c 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -55,6 +55,14 @@ class CadSolver
std::vector<NlLemma> checkFull();
/**
+ * Perform a partial check, returning either {} or a list of lemmas.
+ * If the result is empty, the input is satisfiable and a model is available
+ * for construct_model_if_available. Otherwise, the lemmas exclude some part
+ * of the search space.
+ */
+ std::vector<NlLemma> checkPartial();
+
+ /**
* If a model is available (indicated by the last call to check_full() or
* check_partial()) this method puts a satisfying assignment in d_model,
* clears the list of assertions, and returns true.
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index 8345fc5a1..e3bf4712d 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -360,17 +360,18 @@ Node excluding_interval_to_lemma(const Node& variable,
if (is_algebraic_number(lv))
{
return nm->mkNode(
- Kind::AND,
+ Kind::OR,
nm->mkNode(
- Kind::GT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))),
- nm->mkNode(Kind::LT,
+ Kind::LT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))),
+ nm->mkNode(Kind::GT,
variable,
nm->mkConst(poly_utils::toRationalAbove(lv))));
}
else
{
- return nm->mkNode(
- Kind::EQUAL, variable, nm->mkConst(poly_utils::toRationalBelow(lv)));
+ return nm->mkNode(Kind::DISTINCT,
+ variable,
+ nm->mkConst(poly_utils::toRationalBelow(lv)));
}
}
if (li)
@@ -384,7 +385,7 @@ Node excluding_interval_to_lemma(const Node& variable,
Kind::LT, variable, nm->mkConst(poly_utils::toRationalBelow(lv)));
}
return nm->mkNode(
- Kind::AND,
+ Kind::OR,
nm->mkNode(
Kind::GT, variable, nm->mkConst(poly_utils::toRationalAbove(uv))),
nm->mkNode(
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback