Merge pull request #487 from hoangmle/master

Upgraded to boolector-2.2.0 and some cleanup and refactoring of the metaSMT support.

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)