From 1252235e8875738e51c9b79dff7272c9f4a9d943 Mon Sep 17 00:00:00 2001 From: chriseth Date: Sat, 25 Sep 2021 18:34:19 +0200 Subject: [PATCH] stuff --- libsolutil/BooleanLP.cpp | 4 ++++ libsolutil/BooleanLP.h | 10 ++++++++++ 2 files changed, 14 insertions(+) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index a12341351..6edef8123 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -566,6 +566,10 @@ pair> BooleanLPSolver::runDPLL(SolvingState& CheckResult result = CheckResult::UNKNOWN; map model; + // TODO we really should do the below, and probably even before and after each boolean decision. + // It is very likely that we have some complicated boolean condition in the program, but + // the unconditional things are already unsatisfiable. + // TODO could run this check already even though not all variables are assigned // and return unsat if it is already unsat. if (_dpll.clauses.empty()) diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h index 04c6a5153..fedd53bb3 100644 --- a/libsolutil/BooleanLP.h +++ b/libsolutil/BooleanLP.h @@ -79,6 +79,16 @@ struct DPLL }; +/** + * Component that satisfies the SMT SolverInterface and uses an LP solver plus the DPLL + * algorithm internally. + * It uses a rational relaxation of the integer program and thus will not be able to answer + * "satisfiable", but its answers are still correct. + * + * TODO are integers always non-negative? + * + * Integers are unbounded. + */ class BooleanLPSolver: public smtutil::SolverInterface { public: