diff options
| -rwxr-xr-x | .travis/metaSMT.sh | 9 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 107 |
2 files changed, 27 insertions, 89 deletions
diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh index 7a0d1eef..7195ceb0 100755 --- a/.travis/metaSMT.sh +++ b/.travis/metaSMT.sh @@ -11,10 +11,11 @@ git clone git://github.com/agra-uni-bremen/dependencies.git # Bootstrap export BOOST_ROOT=/usr sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack -./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-1.5.118 --build minisat-git -DZ3_DIR=/usr -sudo cp deps/boolector-1.5.118/lib/* /usr/lib/ # -sudo cp deps/minisat-git/lib/* /usr/lib/ # hack -sudo cp deps/stp-git-basic/lib/* /usr/lib/ # +./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 -DZ3_DIR=/usr +sudo cp deps/boolector-2.2.0/lib/* /usr/lib/ # +sudo cp deps/lingeling-ayv-86bf266-140429/lib/* /usr/lib/ # +sudo cp deps/minisat-git/lib/* /usr/lib/ # hack +sudo cp deps/stp-git-basic/lib/* /usr/lib/ # # Build make -C build install 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) |