From b3ebc940f521005e232389268177b1200a79616b Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Wed, 26 Oct 2016 13:17:50 +0200 Subject: remove outdated FIXME (metaSMT-Z3 implements assumption via push/pop) --- lib/Solver/MetaSMTSolver.cpp | 9 --------- 1 file changed, 9 deletions(-) (limited to 'lib/Solver/MetaSMTSolver.cpp') diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 6bfd79c1..e1261ad2 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -173,13 +173,6 @@ bool MetaSMTSolverImpl::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(); @@ -211,8 +204,6 @@ bool MetaSMTSolverImpl::computeInitialValues( } } - // pop(_meta_solver); - return (success); } -- cgit 1.4.1 From fafc1ea17a3c9955a4c1cfb49d8d39ecc426457e Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Wed, 26 Oct 2016 13:34:24 +0200 Subject: change signature of runAndGetCex() to match runAndGetCexForked() --- lib/Solver/MetaSMTSolver.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'lib/Solver/MetaSMTSolver.cpp') diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index e1261ad2..19f11617 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -78,7 +78,7 @@ public: bool &hasSolution); SolverImpl::SolverRunStatus - runAndGetCex(ref query_expr, const std::vector &objects, + runAndGetCex(const Query &query, const std::vector &objects, std::vector > &values, bool &hasSolution); @@ -192,7 +192,7 @@ bool MetaSMTSolverImpl::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; } @@ -209,11 +209,11 @@ bool MetaSMTSolverImpl::computeInitialValues( template SolverImpl::SolverRunStatus MetaSMTSolverImpl::runAndGetCex( - ref query_expr, const std::vector &objects, + const Query &query, const std::vector &objects, std::vector > &values, bool &hasSolution) { // 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) { -- cgit 1.4.1 From 68becff3ce3bdf27510c2868c3db67bd44eb137a Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Wed, 26 Oct 2016 13:45:58 +0200 Subject: move the query creation part into runAndGetCex() (to be consistent with runAndGetCexForked()) --- lib/Solver/MetaSMTSolver.cpp | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'lib/Solver/MetaSMTSolver.cpp') diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 19f11617..022056fe 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -173,15 +173,6 @@ bool MetaSMTSolverImpl::computeInitialValues( TimerStatIncrementer t(stats::queryTime); assert(_builder); - 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; @@ -212,6 +203,12 @@ SolverImpl::SolverRunStatus MetaSMTSolverImpl::runAndGetCex( const Query &query, const std::vector &objects, 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)); + } // assume the negation of the query assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr))); hasSolution = solve(_meta_solver); -- cgit 1.4.1 From dac2e7ba3f12c839ae7c69aaec6626fcbe05e7e2 Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Thu, 27 Oct 2016 17:49:47 +0200 Subject: upgrade to boolector-2.2.0 & remove the no longer needed aux array vector --- .travis/metaSMT.sh | 9 +++++---- lib/Solver/MetaSMTSolver.cpp | 48 -------------------------------------------- 2 files changed, 5 insertions(+), 52 deletions(-) (limited to 'lib/Solver/MetaSMTSolver.cpp') 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::runAndGetCexForked( // assumption(_meta_solver, _builder->construct(*it)); } - std::vector > - aux_arr_exprs; - if (MetaSMTBackend == METASMT_BACKEND_BOOLECTOR) { - for (std::vector::const_iterator it = objects.begin(), - ie = objects.end(); - it != ie; ++it) { - - std::vector 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::runAndGetCexForked( unsigned res = solve(_meta_solver); if (res) { - - if (MetaSMTBackend != METASMT_BACKEND_BOOLECTOR) { - for (std::vector::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { @@ -342,27 +315,6 @@ MetaSMTSolverImpl::runAndGetCexForked( *pos++ = elem_value; } } - } else { - typename std::vector< - std::vector >::const_iterator - eit = aux_arr_exprs.begin(), - eie = aux_arr_exprs.end(); - for (std::vector::const_iterator it = objects.begin(), - ie = objects.end(); - it != ie, eit != eie; ++it, ++eit) { - const Array *array = *it; - const std::vector &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; -- cgit 1.4.1 From 71214ea259ee62e3484b1ca6ff516a6c2a66fdc2 Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Thu, 27 Oct 2016 17:50:13 +0200 Subject: update comments --- lib/Solver/MetaSMTSolver.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/Solver/MetaSMTSolver.cpp') diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 2dec1873..a34e26d0 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -281,6 +281,7 @@ MetaSMTSolverImpl::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) { @@ -288,9 +289,8 @@ MetaSMTSolverImpl::runAndGetCexForked( // assumption(_meta_solver, _builder->construct(*it)); } - // assume the negation of the query - // can be also asserted instead of assumed as we are in a child process - assumption(_meta_solver, + // 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); -- cgit 1.4.1 From 393e4a2d3e4b477b04bd31c53e84fc4690e3544b Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Thu, 27 Oct 2016 17:51:29 +0200 Subject: apply clang-format --- lib/Solver/MetaSMTSolver.cpp | 45 +++++++++++++++++++++----------------------- 1 file changed, 21 insertions(+), 24 deletions(-) (limited to 'lib/Solver/MetaSMTSolver.cpp') diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index a34e26d0..a453de40 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -28,7 +28,7 @@ #undef Expr #undef Type #undef STP - + #include #include #include @@ -36,7 +36,6 @@ #include #include - 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 @@ -205,7 +204,7 @@ SolverImpl::SolverRunStatus MetaSMTSolverImpl::runAndGetCex( // assume the constraints of the query for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); + ie = query.constraints.end(); it != ie; ++it) { assumption(_meta_solver, _builder->construct(*it)); } @@ -291,30 +290,29 @@ MetaSMTSolverImpl::runAndGetCexForked( // asssert the negation of the query as we are in a child process assertion(_meta_solver, - _builder->construct(Expr::createIsZero(query.expr))); + _builder->construct(Expr::createIsZero(query.expr))); unsigned res = solve(_meta_solver); if (res) { - for (std::vector::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; - } + for (std::vector::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; } + } } assert((uint64_t *)pos); *((uint64_t *)pos) = stats::queryConstructs; @@ -385,7 +383,6 @@ MetaSMTSolverImpl::getOperationStatusCode() { return _runStatusCode; } - template MetaSMTSolver::MetaSMTSolver(bool useForked, bool optimizeDivides) -- cgit 1.4.1