Add conversion of exprs to SMT2 and sending to solver process

Author: thomasspriggs

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

@@ -4,6 +4,12 @@ test.c
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)
+Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\)
+Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
+Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
+Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+Sending command to SMT2 solver - \(define-fun |B2| \(\) Bool \(|not| false\)\)
+Sending command to SMT2 solver - \(assert |B2|\)
 ^EXIT=(0|127|134|137)$
 ^SIGNAL=0$
 identifier: main::1::x

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -2,11 +2,93 @@
 
 #include "smt2_incremental_decision_procedure.h"
 
+#include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/smt_commands.h>
+#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
 #include <util/namespace.h>
+#include <util/range.h>
+#include <util/std_expr.h>
 #include <util/string_utils.h>
+#include <util/symbol.h>
+
+#include <stack>
+
+/// \brief Find all sub expressions of the given \p expr which need to be
+///   expressed as separate smt commands.
+/// \note This pass over \p expr is tightly coupled to the implementation of
+///   `convert_expr_to_smt`. This is because any sub expressions which
+///   `convert_expr_to_smt` translates into function applications, must also be
+///   returned by this`gather_dependent_expressions` function.
+static std::unordered_set<exprt, irep_hash>
+gather_dependent_expressions(const exprt &expr)
+{
+  std::unordered_set<exprt, irep_hash> dependent_expressions;
+  expr.visit_pre([&](const exprt &expr_node) {
+    if(can_cast_expr<symbol_exprt>(expr_node))
+    {
+      dependent_expressions.insert(expr_node);
+    }
+  });
+  return dependent_expressions;
+}
+
+/// \brief Defines any functions which \p expr depends on, which have not yet
+///   been defined, along with their dependencies in turn.
+void smt2_incremental_decision_proceduret::define_dependent_functions(
+  const exprt &expr)
+{
+  std::unordered_set<exprt, irep_hash> seen_expressions =
+    make_range(expression_identifiers)
+      .map([](const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
+        return expr_identifier.first;
+      });
+  std::stack<exprt> to_be_defined;
+  const auto dependencies_needed = [&](const exprt &expr) {
+    bool result = false;
+    for(const auto &dependency : gather_dependent_expressions(expr))
+    {
+      if(!seen_expressions.insert(dependency).second)
+        continue;
+      result = true;
+      to_be_defined.push(dependency);
+    }
+    return result;
+  };
+  dependencies_needed(expr);
+  while(!to_be_defined.empty())
+  {
+    const exprt current = to_be_defined.top();
+    if(dependencies_needed(current))
+      continue;
+    if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
+    {
+      const irep_idt &identifier = symbol_expr->get_identifier();
+      const symbolt *symbol = nullptr;
+      if(!ns.lookup(identifier, symbol))
+      {
+        if(dependencies_needed(symbol->value))
+          continue;
+        const smt_define_function_commandt function{
+          symbol->name, {}, convert_expr_to_smt(symbol->value)};
+        expression_identifiers.emplace(*symbol_expr, function.identifier());
+        send_to_solver(function);
+      }
+      else
+      {
+        const smt_declare_function_commandt function{
+          smt_identifier_termt(
+            identifier, convert_type_to_smt_sort(symbol_expr->type())),
+          {}};
+        expression_identifiers.emplace(*symbol_expr, function.identifier());
+        send_to_solver(function);
+      }
+    }
+    to_be_defined.pop();
+  }
+}
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
   const namespacet &_ns,
@@ -23,8 +105,27 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
     smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
 }
 
+void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
+  const exprt &expr)
+{
+  if(
+    expression_handle_identifiers.find(expr) !=
+    expression_handle_identifiers.cend())
+  {
+    return;
+  }
+
+  define_dependent_functions(expr);
+  smt_define_function_commandt function{
+    "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
+  expression_handle_identifiers.emplace(expr, function.identifier());
+  send_to_solver(function);
+}
+
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
 {
+  log.debug() << "`handle`  -\n  " << expr.pretty(2, 0) << messaget::eom;
+  ensure_handle_for_expr_defined(expr);
   return expr;
 }
 
@@ -53,9 +154,22 @@ smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
 
 void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
 {
-  UNIMPLEMENTED_FEATURE(
-    "`set_to` (" + std::string{value ? "true" : "false"} + "):\n  " +
-    expr.pretty(2, 0));
+  PRECONDITION(can_cast_type<bool_typet>(expr.type()));
+  log.debug() << "`set_to` (" << std::string{value ? "true" : "false"}
+              << ") -\n  " << expr.pretty(2, 0) << messaget::eom;
+
+  define_dependent_functions(expr);
+  auto converted_term = [&]() -> smt_termt {
+    const auto expression_handle_identifier =
+      expression_handle_identifiers.find(expr);
+    if(expression_handle_identifier != expression_handle_identifiers.cend())
+      return expression_handle_identifier->second;
+    else
+      return convert_expr_to_smt(expr);
+  }();
+  if(!value)
+    converted_term = smt_core_theoryt::make_not(converted_term);
+  send_to_solver(smt_assert_commandt{converted_term});
 }
 
 void smt2_incremental_decision_proceduret::push(

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -6,9 +6,14 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 
+#include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/stack_decision_procedure.h>
 #include <util/message.h>
 #include <util/piped_process.h>
+#include <util/std_expr.h>
+
+#include <unordered_map>
+#include <unordered_set>
 
 class smt_commandt;
 class message_handlert;
@@ -48,6 +53,10 @@ class smt2_incremental_decision_proceduret final
   /// \brief Converts given SMT2 command to SMT2 string and sends it to the
   ///    solver process.
   void send_to_solver(const smt_commandt &command);
+  /// \brief Defines any functions which \p expr depends on, which have not yet
+  ///   been defined, along with their dependencies in turn.
+  void define_dependent_functions(const exprt &expr);
+  void ensure_handle_for_expr_defined(const exprt &expr);
 
   const namespacet &ns;
 
@@ -57,6 +66,22 @@ class smt2_incremental_decision_proceduret final
 
   piped_processt solver_process;
   messaget log;
+
+  class sequencet
+  {
+    size_t next_id = 0;
+
+  public:
+    size_t operator()()
+    {
+      return next_id++;
+    }
+  } handle_sequence;
+
+  std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    expression_handle_identifiers;
+  std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    expression_identifiers;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H