From a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 27 Mar 2019 11:33:07 +0000 Subject: Separate constraint set and constraint manager --- lib/Solver/AssignmentValidatingSolver.cpp | 20 +++++++------------- lib/Solver/CachingSolver.cpp | 8 ++++---- lib/Solver/FastCexSolver.cpp | 14 ++++++-------- lib/Solver/IndependentSolver.cpp | 29 +++++++++++++---------------- lib/Solver/MetaSMTSolver.cpp | 14 +++++--------- lib/Solver/Solver.cpp | 7 +++---- lib/Solver/ValidatingSolver.cpp | 10 ++++------ 7 files changed, 42 insertions(+), 60 deletions(-) (limited to 'lib/Solver') diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index 7e1ccd38..54d6ec8c 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -63,10 +63,7 @@ bool AssignmentValidatingSolver::computeInitialValues( // we can't compute a constant and flag this as a problem. Assignment assignment(objects, values, /*_allowFreeValues=*/true); // Check computed assignment satisfies query - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); - it != ie; ++it) { - ref constraint = *it; + for (const auto &constraint : query.constraints) { ref constraintEvaluated = assignment.evaluate(constraint); ConstantExpr *CE = dyn_cast(constraintEvaluated); if (CE == NULL) { @@ -124,16 +121,13 @@ void AssignmentValidatingSolver::dumpAssignmentQuery( const Query &query, const Assignment &assignment) { // Create a Query that is augmented with constraints that // enforce the given assignment. - std::vector > constraints; - assignment.createConstraintsFromAssignment(constraints); + auto constraints = assignment.createConstraintsFromAssignment(); + // Add Constraints from `query` - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); - it != ie; ++it) { - constraints.push_back(*it); - } - ConstraintManager augmentedConstraints(constraints); - Query augmentedQuery(augmentedConstraints, query.expr); + for (const auto &constraint : query.constraints) + constraints.push_back(constraint); + + Query augmentedQuery(constraints, query.expr); // Ask the solver for the log for this query. char *logText = solver->getConstraintLog(augmentedQuery); diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index 5e2d45a2..4a4c8e28 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -32,13 +32,13 @@ private: IncompleteSolver::PartialValidity &result); struct CacheEntry { - CacheEntry(const ConstraintManager &c, ref q) - : constraints(c), query(q) {} + CacheEntry(const ConstraintSet &c, ref q) + : constraints(c), query(q) {} CacheEntry(const CacheEntry &ce) : constraints(ce.constraints), query(ce.query) {} - - ConstraintManager constraints; + + ConstraintSet constraints; ref query; bool operator==(const CacheEntry &b) const { diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index d3062407..a45a8f17 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -1007,10 +1007,9 @@ FastCexSolver::~FastCexSolver() { } /// \return - True if the propogation was able to prove validity or invalidity. static bool propogateValues(const Query& query, CexData &cd, bool checkExpr, bool &isValid) { - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) { - cd.propogatePossibleValue(*it, 1); - cd.propogateExactValue(*it, 1); + for (const auto &constraint : query.constraints) { + cd.propogatePossibleValue(constraint, 1); + cd.propogateExactValue(constraint, 1); } if (checkExpr) { cd.propogatePossibleValue(query.expr, 0); @@ -1032,14 +1031,13 @@ static bool propogateValues(const Query& query, CexData &cd, } } - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) { - if (hasSatisfyingAssignment && !cd.evaluatePossible(*it)->isTrue()) + for (const auto &constraint : query.constraints) { + if (hasSatisfyingAssignment && !cd.evaluatePossible(constraint)->isTrue()) hasSatisfyingAssignment = false; // If this constraint is known to be false, then we can prove anything, so // the query is valid. - if (cd.evaluateExact(*it)->isFalse()) { + if (cd.evaluateExact(constraint)->isFalse()) { isValid = true; return true; } diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 72623645..62632cd0 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -271,15 +271,13 @@ getAllIndependentConstraintsSets(const Query &query) { factors->push_back(IndependentElementSet(neg)); } - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); - it != ie; ++it) { + for (const auto &constraint : query.constraints) { // iterate through all the previously separated constraints. Until we // actually return, factors is treated as a queue of expressions to be // evaluated. If the queue property isn't maintained, then the exprs // could be returned in an order different from how they came it, negatively // affecting later stages. - factors->push_back(IndependentElementSet(*it)); + factors->push_back(IndependentElementSet(constraint)); } bool doneLoop = false; @@ -325,9 +323,9 @@ IndependentElementSet getIndependentConstraints(const Query& query, IndependentElementSet eltsClosure(query.expr); std::vector< std::pair, IndependentElementSet> > worklist; - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) - worklist.push_back(std::make_pair(*it, IndependentElementSet(*it))); + for (const auto &constraint : query.constraints) + worklist.push_back( + std::make_pair(constraint, IndependentElementSet(constraint))); // XXX This should be more efficient (in terms of low level copy stuff). bool done = false; @@ -355,11 +353,10 @@ IndependentElementSet getIndependentConstraints(const Query& query, errs() << "Q: " << query.expr << "\n"; errs() << "\telts: " << IndependentElementSet(query.expr) << "\n"; int i = 0; - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) { - errs() << "C" << i++ << ": " << *it; - errs() << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n"; - errs() << "\telts: " << IndependentElementSet(*it) << "\n"; + for (const auto &constraint: query.constraints) { + errs() << "C" << i++ << ": " << constraint; + errs() << " " << (reqset.count(constraint) ? "(required)" : "(independent)") << "\n"; + errs() << "\telts: " << IndependentElementSet(constraint) << "\n"; } errs() << "elts closure: " << eltsClosure << "\n"; ); @@ -415,7 +412,7 @@ bool IndependentSolver::computeValidity(const Query& query, std::vector< ref > required; IndependentElementSet eltsClosure = getIndependentConstraints(query, required); - ConstraintManager tmp(required); + ConstraintSet tmp(required); return solver->impl->computeValidity(Query(tmp, query.expr), result); } @@ -424,7 +421,7 @@ bool IndependentSolver::computeTruth(const Query& query, bool &isValid) { std::vector< ref > required; IndependentElementSet eltsClosure = getIndependentConstraints(query, required); - ConstraintManager tmp(required); + ConstraintSet tmp(required); return solver->impl->computeTruth(Query(tmp, query.expr), isValid); } @@ -433,7 +430,7 @@ bool IndependentSolver::computeValue(const Query& query, ref &result) { std::vector< ref > required; IndependentElementSet eltsClosure = getIndependentConstraints(query, required); - ConstraintManager tmp(required); + ConstraintSet tmp(required); return solver->impl->computeValue(Query(tmp, query.expr), result); } @@ -496,7 +493,7 @@ bool IndependentSolver::computeInitialValues(const Query& query, if (arraysInFactor.size() == 0){ continue; } - ConstraintManager tmp(it->exprs); + ConstraintSet tmp(it->exprs); std::vector > tempValues; if (!solver->impl->computeInitialValues(Query(tmp, ConstantExpr::alloc(0, Expr::Bool)), arraysInFactor, tempValues, hasSolution)){ diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index fbb7da61..0f78bb5b 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -225,11 +225,9 @@ SolverImpl::SolverRunStatus MetaSMTSolverImpl::runAndGetCex( std::vector > &values, bool &hasSolution) { // assume the constraints of the query - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); - it != ie; ++it) { - assumption(_meta_solver, _builder->construct(*it)); - } + for (auto &constraint : query.constraints) + assumption(_meta_solver, _builder->construct(constraint)); + // assume the negation of the query assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr))); hasSolution = solve(_meta_solver); @@ -303,10 +301,8 @@ MetaSMTSolverImpl::runAndGetCexForked( } // assert constraints as we are in a child process - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); - it != ie; ++it) { - assertion(_meta_solver, _builder->construct(*it)); + for (const auto &constraint : query.constraints) { + assertion(_meta_solver, _builder->construct(constraint)); // assumption(_meta_solver, _builder->construct(*it)); } diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 855f7102..12cfb180 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -223,10 +223,9 @@ std::pair< ref, ref > Solver::getRange(const Query& query) { void Query::dump() const { llvm::errs() << "Constraints [\n"; - for (ConstraintManager::const_iterator i = constraints.begin(); - i != constraints.end(); i++) { - (*i)->dump(); - } + for (const auto &constraint : constraints) + constraint->dump(); + llvm::errs() << "]\n"; llvm::errs() << "Query [\n"; expr->dump(); diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index 93d743db..5d4dab39 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -93,7 +93,7 @@ bool ValidatingSolver::computeInitialValues( if (hasSolution) { // Assert the bindings as constraints, and verify that the // conjunction of the actual constraints is satisfiable. - std::vector > bindings; + ConstraintSet bindings; for (unsigned i = 0; i != values.size(); ++i) { const Array *array = objects[i]; assert(array); @@ -107,12 +107,10 @@ bool ValidatingSolver::computeInitialValues( } ConstraintManager tmp(bindings); ref constraints = Expr::createIsZero(query.expr); - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); - it != ie; ++it) - constraints = AndExpr::create(constraints, *it); + for (auto const &constraint : query.constraints) + constraints = AndExpr::create(constraints, constraint); - if (!oracle->impl->computeTruth(Query(tmp, constraints), answer)) + if (!oracle->impl->computeTruth(Query(bindings, constraints), answer)) return false; if (!answer) assert(0 && "invalid solver result (computeInitialValues)"); -- cgit 1.4.1