diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 107 |
1 files changed, 22 insertions, 85 deletions
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 6bfd79c1..a453de40 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -28,7 +28,7 @@ #undef Expr #undef Type #undef STP - + #include <errno.h> #include <unistd.h> #include <signal.h> @@ -36,7 +36,6 @@ #include <sys/ipc.h> #include <sys/shm.h> - static unsigned char *shared_memory_ptr; static int shared_memory_id = 0; // Darwin by default has a very small limit on the maximum amount of shared @@ -78,7 +77,7 @@ public: bool &hasSolution); SolverImpl::SolverRunStatus - runAndGetCex(ref<Expr> query_expr, const std::vector<const Array *> &objects, + runAndGetCex(const Query &query, const std::vector<const Array *> &objects, std::vector<std::vector<unsigned char> > &values, bool &hasSolution); @@ -173,22 +172,6 @@ bool MetaSMTSolverImpl<SolverContext>::computeInitialValues( TimerStatIncrementer t(stats::queryTime); assert(_builder); - /* - * FIXME push() and pop() work for Z3 but not for Boolector. - * If using Z3, use push() and pop() and assert constraints. - * If using Boolector, assume constrainsts instead of asserting them. - */ - // push(_meta_solver); - - if (!_useForked) { - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); - it != ie; ++it) { - // assertion(_meta_solver, _builder->construct(*it)); - assumption(_meta_solver, _builder->construct(*it)); - } - } - ++stats::queries; ++stats::queryCounterexamples; @@ -199,7 +182,7 @@ bool MetaSMTSolverImpl<SolverContext>::computeInitialValues( success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) || (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode)); } else { - _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution); + _runStatusCode = runAndGetCex(query, objects, values, hasSolution); success = true; } @@ -211,18 +194,22 @@ bool MetaSMTSolverImpl<SolverContext>::computeInitialValues( } } - // pop(_meta_solver); - return (success); } template <typename SolverContext> SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex( - ref<Expr> query_expr, const std::vector<const Array *> &objects, + const Query &query, const std::vector<const Array *> &objects, std::vector<std::vector<unsigned char> > &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)); + } // assume the negation of the query - assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr))); + assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr))); hasSolution = solve(_meta_solver); if (hasSolution) { @@ -293,6 +280,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( ::alarm(std::max(1, (int)timeout)); } + // assert constraints as we are in a child process for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { @@ -300,79 +288,29 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( // assumption(_meta_solver, _builder->construct(*it)); } - std::vector<std::vector<typename SolverContext::result_type> > - aux_arr_exprs; - if (MetaSMTBackend == METASMT_BACKEND_BOOLECTOR) { + // asssert the negation of the query as we are in a child process + assertion(_meta_solver, + _builder->construct(Expr::createIsZero(query.expr))); + unsigned res = solve(_meta_solver); + + if (res) { for (std::vector<const Array *>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { - std::vector<typename SolverContext::result_type> aux_arr; const Array *array = *it; assert(array); typename SolverContext::result_type array_exp = _builder->getInitialArray(array); for (unsigned offset = 0; offset < array->size; offset++) { + typename SolverContext::result_type elem_exp = evaluate( _meta_solver, metaSMT::logic::Array::select( array_exp, bvuint(offset, array->getDomain()))); - aux_arr.push_back(elem_exp); - } - aux_arr_exprs.push_back(aux_arr); - } - assert(aux_arr_exprs.size() == objects.size()); - } - - // assume the negation of the query - // can be also asserted instead of assumed as we are in a child process - assumption(_meta_solver, - _builder->construct(Expr::createIsZero(query.expr))); - unsigned res = solve(_meta_solver); - - if (res) { - - if (MetaSMTBackend != METASMT_BACKEND_BOOLECTOR) { - - for (std::vector<const Array *>::const_iterator it = objects.begin(), - ie = objects.end(); - it != ie; ++it) { - - const Array *array = *it; - assert(array); - typename SolverContext::result_type array_exp = - _builder->getInitialArray(array); - - for (unsigned offset = 0; offset < array->size; offset++) { - - typename SolverContext::result_type elem_exp = - evaluate(_meta_solver, - metaSMT::logic::Array::select( - array_exp, bvuint(offset, array->getDomain()))); - unsigned char elem_value = - metaSMT::read_value(_meta_solver, elem_exp); - *pos++ = elem_value; - } - } - } else { - typename std::vector< - std::vector<typename SolverContext::result_type> >::const_iterator - eit = aux_arr_exprs.begin(), - eie = aux_arr_exprs.end(); - for (std::vector<const Array *>::const_iterator it = objects.begin(), - ie = objects.end(); - it != ie, eit != eie; ++it, ++eit) { - const Array *array = *it; - const std::vector<typename SolverContext::result_type> &arr_exp = - *eit; - assert(array); - assert(array->size == arr_exp.size()); - - for (unsigned offset = 0; offset < array->size; offset++) { - unsigned char elem_value = - metaSMT::read_value(_meta_solver, arr_exp[offset]); - *pos++ = elem_value; - } + unsigned char elem_value = + metaSMT::read_value(_meta_solver, elem_exp); + *pos++ = elem_value; } } } @@ -445,7 +383,6 @@ MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() { return _runStatusCode; } - template <typename SolverContext> MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) |