cerc-io/solidity
11
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

rewrite

Browse Source
This commit is contained in:
chriseth
2022-04-07 18:12:40 +02:00
parent aebe9753ff
commit f9ab7cc635
5 changed files with 603 additions and 1331 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolutil/BooleanLP.cpp
+23 -29
View File
@@ -136,7 +136,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
{
LinearExpression data = *left - *right;
data[0] *= -1;
Constraint c{move(data), _expr.name == "=", {}};
Constraint c{move(data), _expr.name == "="};
if (!tryAddDirectBounds(c))
state().fixedConstraints.emplace_back(move(c));
cout << "Added as fixed constraint" << endl;
@@ -186,7 +186,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
{
LinearExpression data = *left - *right;
data[0] *= -1;
Constraint c{move(data), _expr.name == "=", {}};
Constraint c{move(data), _expr.name == "="};
if (!tryAddDirectBounds(c))
state().fixedConstraints.emplace_back(move(c));
}
@@ -220,10 +220,24 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
std::vector<std::string> booleanVariables;
std::vector<Clause> clauses = state().clauses;
SolvingState lpState;
// TODO we start building up a new set of solver
// for each query, but we should also keep some
// kind of cache across queries.
std::vector<std::pair<size_t, LPSolver>> lpSolvers;
lpSolvers.emplace_back(0, LPSolver{});
LPSolver& lpSolver = lpSolvers.back().second;
for (auto&& [index, bound]: state().bounds)
resizeAndSet(lpState.bounds, index, bound);
lpState.constraints = state().fixedConstraints;
{
if (bound.lower)
lpSolver.addLowerBound(index, *bound.lower);
if (bound.upper)
lpSolver.addUpperBound(index, *bound.upper);
}
for (Constraint const& c: state().fixedConstraints)
lpSolver.addConstraint(c);
// TODO this way, it will result in a lot of gaps in both sets of variables.
// should we compress them and store a mapping?
// Is it even a problem if the indices overlap?
@@ -231,23 +245,9 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
if (state().isBooleanVariable.at(index) || isConditionalConstraint(index))
resizeAndSet(booleanVariables, index, name);
else
resizeAndSet(lpState.variableNames, index, name);
lpSolver.setVariableName(index, name);
// TODO keep a cache as a member that is never reset.
// TODO We can also keep the split unconditionals across push/pop
// We only need to be careful to update the number of variables.
std::vector<std::pair<size_t, LPSolver>> lpSolvers;
// TODO We start afresh here. If we want this to reuse the existing results
// from previous invocations of the boolean solver, we still have to use
// a cache.
// The current optimization is only for CDCL.
lpSolvers.emplace_back(0, LPSolver{&m_lpCache});
if (
lpSolvers.back().second.setState(lpState) == LPResult::Infeasible ||
lpSolvers.back().second.check().first == LPResult::Infeasible
)
if (lpSolver.check().first == LPResult::Infeasible)
{
cout << "----->>>>> unsatisfiable" << endl;
return {CheckResult::UNSATISFIABLE, {}};
@@ -263,8 +263,7 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
continue;
// "reason" is already stored for those constraints.
Constraint const& constraint = state().conditionalConstraints.at(constraintIndex);
solAssert(constraint.reasons.size() == 1 && *constraint.reasons.begin() == constraintIndex);
lpSolvers.back().second.addConstraint(constraint);
lpSolvers.back().second.addConstraint(constraint, constraintIndex);
}
auto&& [result, modelOrReason] = lpSolvers.back().second.check();
// We can only really use the result "infeasible". Everything else should be "sat".
@@ -365,7 +364,7 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
LinearExpression data = *left - *right;
data[0] *= -1;
return Literal{true, addConditionalConstraint(Constraint{move(data), _expr.name == "=", {}})};
return Literal{true, addConditionalConstraint(Constraint{move(data), _expr.name == "="})};
}
else if (_expr.name == ">=")
return parseLiteral(_expr.arguments.at(1) <= _expr.arguments.at(0));
@@ -390,7 +389,6 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
Constraint le = c;
le.equality = false;
le.data[0] -= 1;
le.reasons.clear();
Literal leL{true, addConditionalConstraint(le)};
// X >= b + 1
@@ -399,7 +397,6 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
ge.equality = false;
ge.data *= -1;
ge.data[0] -= 1;
ge.reasons.clear();
Literal geL{true, addConditionalConstraint(ge)};
@@ -419,7 +416,6 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
Constraint negated = c;
negated.data *= -1;
negated.data[0] -= 1;
negated.reasons.clear();
return Literal{true, addConditionalConstraint(negated)};
}
}
@@ -561,8 +557,6 @@ size_t BooleanLPSolver::addConditionalConstraint(Constraint _constraint)
// - integers
declareVariable(name, false);
size_t index = state().variables.at(name);
solAssert(_constraint.reasons.empty());
_constraint.reasons.emplace(index);
state().conditionalConstraints[index] = move(_constraint);
return index;
}
libsolutil/BooleanLP.h
+7 -4
View File
@@ -40,8 +40,14 @@ struct State
std::map<size_t, Constraint> conditionalConstraints;
std::vector<Clause> clauses;
struct Bounds
{
std::optional<rational> lower;
std::optional<rational> upper;
};
// Unconditional bounds on variables
std::map<size_t, SolvingState::Bounds> bounds;
std::map<size_t, Bounds> bounds;
// Unconditional constraints
std::vector<Constraint> fixedConstraints;
};
@@ -122,9 +128,6 @@ private:
/// Stack of state, to allow for push()/pop().
std::vector<State> m_state{{State{}}};
std::unordered_map<SolvingState, LPResult> m_lpCache;
};
libsolutil/LP.cpp
+378 -1096
View File
File diff suppressed because it is too large Load Diff
libsolutil/LP.h
+65 -131
View File
@@ -42,8 +42,6 @@ struct Constraint
{
LinearExpression data;
bool equality = false;
/// Set of literals the conjunction of which implies this constraint.
std::set<size_t> reasons = {};
bool operator<(Constraint const& _other) const;
bool operator==(Constraint const& _other) const;
@@ -171,156 +169,92 @@ enum class LPResult
Infeasible ///< System does not have any solution.
};
class SimplexWithBounds
{
public:
explicit SimplexWithBounds(SolvingState _state);
LPResult check();
size_t addVariable(std::string _name);
void addConstraint(Constraint _constraint);
std::string toString() const;
private:
/// Set value of non-basic variable.
void update(size_t _var, rational const& _value);
/// @returns the index of the first basic variable violating its bounds.
std::optional<size_t> firstConflictingBasicVariable() const;
std::optional<size_t> firstReplacementVar(size_t _basicVarToReplace, bool _increasing) const;
void pivot(size_t _old, size_t _new);
void pivotAndUpdate(size_t _oldBasicVar, rational const& _newValue, size_t _newBasicVar);
SolvingState m_state;
std::vector<rational> m_assignments;
/// Variable index to row it controls.
std::map<size_t, size_t> m_basicVariables;
};
/**
* Applies several strategies to simplify a given solving state.
* During these simplifications, it can sometimes already be determined if the
* state is feasible or not.
* Since some variables can be fixed to specific values, it returns a
* (partial) model.
*
* - Constraints with exactly one nonzero coefficient represent "a x <= b"
* and thus are turned into bounds.
* - Constraints with zero nonzero coefficients are constant relations.
* If such a relation is false, answer "infeasible", otherwise remove the constraint.
* - Empty columns can be removed.
* - Variables with matching bounds can be removed from the problem by substitution.
*
* Holds a reference to the solving state that is modified during operation.
*/
class SolvingStateSimplifier
{
public:
SolvingStateSimplifier(SolvingState& _state):
m_state(_state) {}
std::pair<LPResult, std::variant<std::map<size_t, rational>, ReasonSet>> simplify();
private:
/// Remove variables that have equal lower and upper bound.
/// @returns reason / set of conflicting clauses if infeasible.
std::optional<ReasonSet> removeFixedVariables();
/// Removes constraints of the form 0 <= b or 0 == b (no variables) and
/// turns constraints of the form a * x <= b (one variable) into bounds.
/// @returns reason / set of conflicting clauses if infeasible.
std::optional<ReasonSet> extractDirectConstraints();
/// Removes all-zeros columns.
void removeEmptyColumns();
/// Set to true by the strategies if they performed some changes.
bool m_changed = false;
SolvingState& m_state;
std::map<size_t, rational> m_fixedVariables;
};
/**
* Splits a given linear program into multiple linear programs with disjoint sets of variables.
* The initial program is feasible if and only if all sub-programs are feasible.
*/
class ProblemSplitter
{
public:
explicit ProblemSplitter(SolvingState const& _state);
/// @returns true if there are still sub-problems to split out.
operator bool() const { return m_column < m_state.variableNames.size(); }
/// @returns the next sub-problem.
std::pair<std::vector<bool>, std::vector<bool>> next();
private:
SolvingState const& m_state;
/// Next column to start the search for a connected component.
size_t m_column = 1;
/// The columns we have already split out.
std::vector<bool> m_seenColumns;
};
/**
* LP solver for rational problems.
* LP solver for rational problems, based on "A Fast Linear-Arithmetic Solver for DPLL(T)*"
* by Dutertre and Moura.
*
* Does not solve integer problems!
*
* Tries to split a given problem into sub-problems and utilizes a cache to quickly solve
* similar problems.
* Tries to split incoming bounds and constraints into unrelated sub-problems.
* Maintains lower/upper bounds for all variables.
* Adds one slack variable per constraint and stores all constraints as "= 0" equations.
* Splits variables into basic and non-basic. For each row there is exactly one
* basic variable that has a factor of -1.
* The equations are satisfied at all times and non-basic variables are always within their bounds.
* Non-basic variables might violate their bounds.
* It attempts to resolve these violations in turn, swapping a basic variables with a non-basic
* variables that can still move in the required direction.
*
* Can be used in a mode where it does not support returning models. In that case, the
* cache is more efficient.
* It is perfectly fine to add new bounds, variable or constraints after a call to "check".
* The solver can be copied at low cost and it uses a "copy on write" mechanism for the sub-problems.
*/
class LPSolver
{
public:
explicit LPSolver(bool _supportModels = true);
explicit LPSolver(std::unordered_map<SolvingState, LPResult>* _cache):
m_cache(_cache) {}
void addConstraint(Constraint const& _constraint, std::optional<size_t> _reason = std::nullopt);
void setVariableName(size_t _variable, std::string _name);
void addLowerBound(size_t _variable, rational _bound);
void addUpperBound(size_t _variable, rational _bound);
LPResult setState(SolvingState _state);
void addConstraint(Constraint _constraint);
std::pair<LPResult, std::variant<Model, ReasonSet>> check();
private:
void combineSubProblems(size_t _combineInto, size_t _combineFrom);
void addConstraintToSubProblem(size_t _subProblem, Constraint _constraint);
void updateSubProblems();
std::string toString() const;
/// Ground state for CDCL. This is shared by copies of the solver.
/// Only ``setState`` changes the state. Copies will only use
/// ``addConstraint`` which does not change m_state.
std::shared_ptr<SolvingState> m_state;
private:
struct Bounds
{
std::optional<rational> lower;
std::optional<rational> upper;
};
struct Variable
{
std::string name = {};
rational value = 0;
Bounds bounds = {};
};
struct SubProblem
{
// TODO now we could actually put the constraints here again.
std::vector<Constraint> removableConstraints;
bool dirty = true;
LPResult result = LPResult::Unknown;
std::vector<boost::rational<bigint>> model = {};
std::set<size_t> variables = {};
std::optional<SimplexWithBounds> simplex = std::nullopt;
/// Set to true on "check". Needs a copy for adding a constraint or bound if set to true.
bool sealed = false;
std::optional<LPResult> result = std::nullopt;
std::vector<LinearExpression> factors;
std::vector<Variable> variables;
/// Variable index to constraint it controls.
std::map<size_t, size_t> basicVariables;
/// Maps outer indices to inner indices.
std::map<size_t, size_t> varMapping = {};
std::set<size_t> reasons;
LPResult check();
std::string toString() const;
private:
/// Set value of non-basic variable.
void update(size_t _varIndex, rational const& _value);
/// @returns the index of the first basic variable violating its bounds.
std::optional<size_t> firstConflictingBasicVariable() const;
std::optional<size_t> firstReplacementVar(size_t _basicVarToReplace, bool _increasing) const;
void pivot(size_t _old, size_t _new);
void pivotAndUpdate(size_t _oldBasicVar, rational const& _newValue, size_t _newBasicVar);
};
std::pair<SolvingState, std::map<size_t, size_t>> stateFromSubProblem(size_t _index) const;
ReasonSet reasonSetForSubProblem(SubProblem const& _subProblem);
std::shared_ptr<std::map<size_t, rational>> m_fixedVariables;
SubProblem& unseal(size_t _problem);
/// Unseals the problem for the given variable or creates a new one.
SubProblem& unsealForVariable(size_t _outerIndex);
void combineSubProblems(size_t _combineInto, size_t _combineFrom);
void addConstraintToSubProblem(size_t _subProblem, Constraint const& _constraint, std::optional<size_t> _reason);
void addOuterVariableToSubProblem(size_t _subProblem, size_t _outerIndex);
size_t addNewVariableToSubProblem(size_t _subProblem);
std::map<std::string, rational> model() const;
/// These use "copy on write".
std::vector<std::shared_ptr<SubProblem>> m_subProblems;
std::vector<size_t> m_subProblemsPerVariable;
std::vector<size_t> m_subProblemsPerConstraint;
/// TODO also store the first infeasible subproblem?
/// TODO still retain the cache?
std::unordered_map<SolvingState, LPResult>* m_cache = nullptr;
/// Maps outer indices to sub problems.
std::map<size_t, size_t> m_subProblemsPerVariable;
/// Counter to enable unique names for the slack variables.
size_t m_slackVariableCounter = 0;
};