cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

stuff

Browse Source
This commit is contained in:
chriseth 2021-09-25 18:34:19 +02:00
parent 99fd9d54fc
commit 1252235e88
2 changed files with 14 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolutil/BooleanLP.cpp
View File

@ -566,6 +566,10 @@ pair<CheckResult, map<string, rational>> BooleanLPSolver::runDPLL(SolvingState&
CheckResult result = CheckResult::UNKNOWN; CheckResult result = CheckResult::UNKNOWN;
map<string, rational> model; map<string, rational> 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 // TODO could run this check already even though not all variables are assigned
// and return unsat if it is already unsat. // and return unsat if it is already unsat.
if (_dpll.clauses.empty()) if (_dpll.clauses.empty())

10
libsolutil/BooleanLP.h
View File

@ -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 class BooleanLPSolver: public smtutil::SolverInterface
{ {
public: public: