[feat, bitwuzla] getConstraintLog implementation.

include/klee/Expr/Constraints.h

@@ -49,7 +49,11 @@ class ConstraintSet {
   bool isSymcretized(ref<Expr> expr) const;
 
   void rewriteConcretization(const Assignment &a);
-  ConstraintSet withExpr(ref<Expr> e) const;
+  ConstraintSet withExpr(ref<Expr> e) const {
+    ConstraintSet copy = ConstraintSet(*this);
+    copy.addConstraint(e, Assignment());
+    return copy;
+  }
 
   std::vector<const Array *> gatherArrays() const;
   std::vector<const Array *> gatherSymcretizedArrays() const;

lib/Solver/BitwuzlaSolver.cpp

@@ -314,7 +314,50 @@ BitwuzlaSolverImpl::BitwuzlaSolverImpl()
 }
 
 char *BitwuzlaSolverImpl::getConstraintLog(const Query &query) {
-  return strdup("unimplemented");
+  std::stringstream outputLog;
+
+  // We use a different builder here because we don't want to interfere
+  // with the solver's builder because it may change the solver builder's
+  // cache.
+  // NOTE: The builder does not set `z3LogInteractionFile` to avoid conflicting
+  // with whatever the solver's builder is set to do.
+  std::unique_ptr<BitwuzlaBuilder> tempBuilder(new BitwuzlaBuilder(false));
+  ConstantArrayFinder constant_arrays_in_query;
+
+  for (const auto array :
+       query.constraints.withExpr(query.expr).gatherArrays()) {
+    outputLog << "(declare-fun " << array->getName() << " () Array (_ BitVec "
+              << array->getDomain() << ") (_ BitVec " << array->getRange()
+              << ")))\n";
+  }
+
+  for (auto const &constraint : query.constraints.cs()) {
+    outputLog << "(assert " << tempBuilder->construct(constraint).str(10)
+              << ")\n";
+    constant_arrays_in_query.visit(constraint);
+  }
+
+  // KLEE Queries are validity queries i.e.
+  // ∀ X Constraints(X) → query(X)
+  // but Z3 works in terms of satisfiability so instead we ask the
+  // the negation of the equivalent i.e.
+  // ∃ X Constraints(X) ∧ ¬ query(X)
+  Term formula = mk_term(Kind::NOT, {tempBuilder->construct(query.expr)});
+  constant_arrays_in_query.visit(query.expr);
+
+  for (auto const &constant_array : constant_arrays_in_query.results) {
+    for (auto const &arrayIndexValueExpr :
+         tempBuilder->constant_array_assertions[constant_array]) {
+      outputLog << "(assert " << arrayIndexValueExpr.str(10) << ")\n";
+    }
+  }
+
+  outputLog << "(assert " << formula.str(10) << ")\n";
+  outputLog << "(check-sat)"
+            << "\n";
+
+  // Client is responsible for freeing the returned C-string
+  return strdup(outputLog.str().c_str());
 }
 
 bool BitwuzlaSolverImpl::computeTruth(const ConstraintQuery &query,