diff options
| -rwxr-xr-x | .travis/metaSMT.sh | 9 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 48 |
2 files changed, 5 insertions, 52 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 022056fe..2dec1873 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -288,30 +288,6 @@ 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) { - 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, @@ -319,9 +295,6 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( 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) { @@ -342,27 +315,6 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( *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; - } - } - } } assert((uint64_t *)pos); *((uint64_t *)pos) = stats::queryConstructs; |