goto symex now uses decision_proceduret interface

Use the the decision_proceduret interface in goto_symext instead of
prop_convt.  literalt values are replaced by handles.

Author: Daniel Kroening

src/goto-checker/bmc_util.cpp

@@ -56,9 +56,9 @@ ssa_step_matches_failing_property(const irep_idt &property_id)
 {
   return [property_id](
            symex_target_equationt::SSA_stepst::const_iterator step,
-           const prop_convt &prop_conv) {
+           const decision_proceduret &decision_procedure) {
     return step->is_assert() && step->get_property_id() == property_id &&
-           prop_conv.get(step->cond_handle).is_false();
+           decision_procedure.get(step->cond_handle).is_false();
   };
 }
 

src/goto-checker/counterexample_beautification.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol.h>
 #include <util/threeval.h>
 
-#include <solvers/prop/literal_expr.h>
 #include <solvers/prop/prop_minimize.h>
 
 counterexample_beautificationt::counterexample_beautificationt(

src/goto-checker/goto_symex_fault_localizer.cpp

@@ -58,11 +58,11 @@ const SSA_stept &goto_symex_fault_localizert::collect_guards(
       step.assignment_type == symex_targett::assignment_typet::STATE &&
       !step.ignore)
     {
-      if(!step.guard_handle.is_constant())
+      literalt l = solver.convert(step.guard_handle);
+      if(!l.is_constant())
       {
         auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);
-        literalt guard_literal = solver.convert(step.guard_handle);
-        localization_points.emplace(guard_literal, emplace_result.first);
+        localization_points.emplace(l, emplace_result.first);
       }
     }
 

src/goto-checker/goto_symex_fault_localizer.h

@@ -18,6 +18,8 @@ Author: Peter Schrammel
 
 #include <goto-symex/symex_target_equation.h>
 
+#include <solvers/prop/prop_conv.h>
+
 #include "fault_localization_provider.h"
 
 class goto_symex_fault_localizert

src/goto-symex/build_goto_trace.cpp

@@ -20,13 +20,12 @@ Author: Daniel Kroening
 
 #include <goto-programs/goto_functions.h>
 
-#include <solvers/prop/prop_conv.h>
-#include <solvers/prop/prop.h>
+#include <solvers/decision_procedure.h>
 
 #include "partial_order_concurrency.h"
 
 static exprt build_full_lhs_rec(
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   const exprt &src_original, // original identifiers
   const exprt &src_ssa)      // renamed identifiers
@@ -39,17 +38,18 @@ static exprt build_full_lhs_rec(
   if(id==ID_index)
   {
     // get index value from src_ssa
-    exprt index_value=prop_conv.get(to_index_expr(src_ssa).index());
+    exprt index_value = decision_procedure.get(to_index_expr(src_ssa).index());
 
     if(index_value.is_not_nil())
     {
       simplify(index_value, ns);
       index_exprt tmp=to_index_expr(src_original);
       tmp.index()=index_value;
-      tmp.array()=
-        build_full_lhs_rec(prop_conv, ns,
-          to_index_expr(src_original).array(),
-          to_index_expr(src_ssa).array());
+      tmp.array() = build_full_lhs_rec(
+        decision_procedure,
+        ns,
+        to_index_expr(src_original).array(),
+        to_index_expr(src_ssa).array());
       return std::move(tmp);
     }
 
@@ -58,22 +58,29 @@ static exprt build_full_lhs_rec(
   else if(id==ID_member)
   {
     member_exprt tmp=to_member_expr(src_original);
-    tmp.struct_op()=build_full_lhs_rec(
-      prop_conv, ns,
+    tmp.struct_op() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
       to_member_expr(src_original).struct_op(),
       to_member_expr(src_ssa).struct_op());
   }
   else if(id==ID_if)
   {
     if_exprt tmp2=to_if_expr(src_original);
 
-    tmp2.false_case()=build_full_lhs_rec(prop_conv, ns,
-      tmp2.false_case(), to_if_expr(src_ssa).false_case());
+    tmp2.false_case() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
+      tmp2.false_case(),
+      to_if_expr(src_ssa).false_case());
 
-    tmp2.true_case()=build_full_lhs_rec(prop_conv, ns,
-      tmp2.true_case(), to_if_expr(src_ssa).true_case());
+    tmp2.true_case() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
+      tmp2.true_case(),
+      to_if_expr(src_ssa).true_case());
 
-    exprt tmp=prop_conv.get(to_if_expr(src_ssa).cond());
+    exprt tmp = decision_procedure.get(to_if_expr(src_ssa).cond());
 
     if(tmp.is_true())
       return tmp2.true_case();
@@ -85,16 +92,19 @@ static exprt build_full_lhs_rec(
   else if(id==ID_typecast)
   {
     typecast_exprt tmp=to_typecast_expr(src_original);
-    tmp.op()=build_full_lhs_rec(prop_conv, ns,
-      to_typecast_expr(src_original).op(), to_typecast_expr(src_ssa).op());
+    tmp.op() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
+      to_typecast_expr(src_original).op(),
+      to_typecast_expr(src_ssa).op());
     return std::move(tmp);
   }
   else if(id==ID_byte_extract_little_endian ||
           id==ID_byte_extract_big_endian)
   {
     byte_extract_exprt tmp = to_byte_extract_expr(src_original);
     tmp.op() = build_full_lhs_rec(
-      prop_conv, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
+      decision_procedure, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
 
     // re-write into big case-split
   }
@@ -169,7 +179,8 @@ static void update_internal_field(
 
 /// Replace nondet values that appear in \p type by their values as found by
 /// \p solver.
-static void replace_nondet_in_type(typet &type, const prop_convt &solver)
+static void
+replace_nondet_in_type(typet &type, const decision_proceduret &solver)
 {
   if(type.id() == ID_array)
   {
@@ -182,7 +193,8 @@ static void replace_nondet_in_type(typet &type, const prop_convt &solver)
 
 /// Replace nondet values that appear in the type of \p expr and its
 /// subexpressions type by their values as found by \p solver.
-static void replace_nondet_in_type(exprt &expr, const prop_convt &solver)
+static void
+replace_nondet_in_type(exprt &expr, const decision_proceduret &solver)
 {
   replace_nondet_in_type(expr.type(), solver);
   for(auto &sub : expr.operands())
@@ -192,7 +204,7 @@ static void replace_nondet_in_type(exprt &expr, const prop_convt &solver)
 void build_goto_trace(
   const symex_target_equationt &target,
   ssa_step_predicatet is_last_step_to_keep,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
@@ -218,14 +230,14 @@ void build_goto_trace(
   {
     if(
       last_step_to_keep == target.SSA_steps.end() &&
-      is_last_step_to_keep(it, prop_conv))
+      is_last_step_to_keep(it, decision_procedure))
     {
       last_step_to_keep = it;
     }
 
     const SSA_stept &SSA_step = *it;
 
-    if(!prop_conv.get(SSA_step.guard_handle).is_true())
+    if(!decision_procedure.get(SSA_step.guard_handle).is_true())
       continue;
 
     if(it->is_constraint() ||
@@ -250,7 +262,7 @@ void build_goto_trace(
         // these are just used to get the time stamp -- the clock type is
         // computed to be of the minimal necessary size, but we don't need to
         // know it to get the value so just use typeless
-        exprt clock_value = prop_conv.get(
+        exprt clock_value = decision_procedure.get(
           symbol_exprt::typeless(partial_order_concurrencyt::rw_clock_id(it)));
 
         const auto cv = numeric_cast<mp_integer>(clock_value);
@@ -342,7 +354,7 @@ void build_goto_trace(
       goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
 
       for(auto &arg : goto_trace_step.function_arguments)
-        arg = prop_conv.get(arg);
+        arg = decision_procedure.get(arg);
 
       // update internal field for specific variables in the counterexample
       update_internal_field(SSA_step, goto_trace_step, ns);
@@ -359,15 +371,20 @@ void build_goto_trace(
       if(SSA_step.original_full_lhs.is_not_nil())
       {
         goto_trace_step.full_lhs = build_full_lhs_rec(
-          prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
-        replace_nondet_in_type(goto_trace_step.full_lhs, prop_conv);
+          decision_procedure,
+          ns,
+          SSA_step.original_full_lhs,
+          SSA_step.ssa_full_lhs);
+        replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure);
       }
 
       if(SSA_step.ssa_full_lhs.is_not_nil())
       {
-        goto_trace_step.full_lhs_value = prop_conv.get(SSA_step.ssa_full_lhs);
+        goto_trace_step.full_lhs_value =
+          decision_procedure.get(SSA_step.ssa_full_lhs);
         simplify(goto_trace_step.full_lhs_value, ns);
-        replace_nondet_in_type(goto_trace_step.full_lhs_value, prop_conv);
+        replace_nondet_in_type(
+          goto_trace_step.full_lhs_value, decision_procedure);
       }
 
       for(const auto &j : SSA_step.converted_io_args)
@@ -378,7 +395,7 @@ void build_goto_trace(
         }
         else
         {
-          exprt tmp = prop_conv.get(j);
+          exprt tmp = decision_procedure.get(j);
           goto_trace_step.io_args.push_back(tmp);
         }
       }
@@ -388,7 +405,7 @@ void build_goto_trace(
         goto_trace_step.cond_expr = SSA_step.cond_expr;
 
         goto_trace_step.cond_value =
-          prop_conv.get(SSA_step.cond_handle).is_true();
+          decision_procedure.get(SSA_step.cond_handle).is_true();
       }
 
       if(ssa_step_it == last_step_to_keep)
@@ -400,31 +417,33 @@ void build_goto_trace(
 void build_goto_trace(
   const symex_target_equationt &target,
   symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
-  const auto is_last_step_to_keep = [last_step_to_keep](
-    symex_target_equationt::SSA_stepst::const_iterator it, const prop_convt &) {
-    return last_step_to_keep == it;
-  };
+  const auto is_last_step_to_keep =
+    [last_step_to_keep](
+      symex_target_equationt::SSA_stepst::const_iterator it,
+      const decision_proceduret &) { return last_step_to_keep == it; };
 
   return build_goto_trace(
-    target, is_last_step_to_keep, prop_conv, ns, goto_trace);
+    target, is_last_step_to_keep, decision_procedure, ns, goto_trace);
 }
 
 static bool is_failed_assertion_step(
   symex_target_equationt::SSA_stepst::const_iterator step,
-  const prop_convt &prop_conv)
+  const decision_proceduret &decision_procedure)
 {
-  return step->is_assert() && prop_conv.get(step->cond_handle).is_false();
+  return step->is_assert() &&
+         decision_procedure.get(step->cond_handle).is_false();
 }
 
 void build_goto_trace(
   const symex_target_equationt &target,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
-  build_goto_trace(target, is_failed_assertion_step, prop_conv, ns, goto_trace);
+  build_goto_trace(
+    target, is_failed_assertion_step, decision_procedure, ns, goto_trace);
 }

src/goto-symex/build_goto_trace.h

@@ -20,45 +20,46 @@ Date: July 2005
 /// Build a trace by going through the steps of \p target and stopping at the
 /// first failing assertion
 /// \param target: SSA form of the program
-/// \param prop_conv: solver from which to get valuations
+/// \param decision_procedure: solver from which to get valuations
 /// \param ns: namespace
 /// \param [out] goto_trace: trace to which the steps of the trace get appended
 void build_goto_trace(
   const symex_target_equationt &target,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace);
 
 /// Build a trace by going through the steps of \p target and stopping after
 /// the given step
 /// \param target: SSA form of the program
 /// \param last_step_to_keep: iterator pointing to the last step to keep
-/// \param prop_conv: solver from which to get valuations
+/// \param decision_procedure: solver from which to get valuations
 /// \param ns: namespace
 /// \param [out] goto_trace: trace to which the steps of the trace get appended
 void build_goto_trace(
   const symex_target_equationt &target,
   symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace);
 
-typedef std::function<
-  bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)>
+typedef std::function<bool(
+  symex_target_equationt::SSA_stepst::const_iterator,
+  const decision_proceduret &)>
   ssa_step_predicatet;
 
 /// Build a trace by going through the steps of \p target and stopping after
 /// the step matching a given condition
 /// \param target: SSA form of the program
 /// \param stop_after_predicate: function with an SSA step iterator and solver
 ///   as argument, which should return true for the last step to keep
-/// \param prop_conv: solver from which to get valuations
+/// \param decision_procedure: solver from which to get valuations
 /// \param ns: namespace
 /// \param [out] goto_trace: trace to which the steps of the trace get appended
 void build_goto_trace(
   const symex_target_equationt &target,
   ssa_step_predicatet stop_after_predicate,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace);