diff options
author | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-10-27 17:49:47 +0200 |
---|---|---|
committer | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-10-27 17:49:47 +0200 |
commit | dac2e7ba3f12c839ae7c69aaec6626fcbe05e7e2 (patch) | |
tree | 1740c06d269bb309c4bef31e5c647ccf9300697e /lib | |
parent | 68becff3ce3bdf27510c2868c3db67bd44eb137a (diff) | |
download | klee-dac2e7ba3f12c839ae7c69aaec6626fcbe05e7e2.tar.gz |
upgrade to boolector-2.2.0 & remove the no longer needed aux array vector
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 48 |
1 files changed, 0 insertions, 48 deletions
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; |