Merge pull request #737 from diffblue/property-no-solver

word-level BMC: remove parameters for solver + ns

Author: tautschnig

src/ebmc/k_induction.cpp

@@ -261,7 +261,7 @@ void k_inductiont::induction_step()
         const exprt &p = to_unary_expr(property.normalized_expr).op();
         for(std::size_t c = 0; c < no_timeframes; c++)
         {
-          exprt tmp = instantiate(p, c, no_timeframes, ns);
+          exprt tmp = instantiate(p, c, no_timeframes);
           solver.set_to_true(tmp);
         }
       }
@@ -272,15 +272,13 @@ void k_inductiont::induction_step()
     // assumption: time frames 0,...,k-1
     for(std::size_t c = 0; c < no_timeframes - 1; c++)
     {
-      exprt tmp=
-        instantiate(p, c, no_timeframes-1, ns);
+      exprt tmp = instantiate(p, c, no_timeframes - 1);
       solver.set_to_true(tmp);
     }
 
     // property: time frame k
     {
-      exprt tmp=
-        instantiate(p, no_timeframes-1, no_timeframes, ns);
+      exprt tmp = instantiate(p, no_timeframes - 1, no_timeframes);
       solver.set_to_false(tmp);
     }
 

src/ebmc/random_traces.cpp

@@ -478,8 +478,7 @@ void random_tracest::freeze(
   {
     for(auto &symbol : symbols)
     {
-      auto symbol_in_timeframe =
-        instantiate(symbol, i, number_of_timeframes, ns);
+      auto symbol_in_timeframe = instantiate(symbol, i, number_of_timeframes);
       (void)solver.handle(symbol_in_timeframe);
     }
   }
@@ -508,7 +507,7 @@ std::vector<exprt> random_tracest::random_input_constraints(
   {
     for(auto &input : inputs)
     {
-      auto input_in_timeframe = instantiate(input, i, number_of_timeframes, ns);
+      auto input_in_timeframe = instantiate(input, i, number_of_timeframes);
       auto constraint =
         equal_exprt(input_in_timeframe, random_value(input.type()));
       result.push_back(constraint);
@@ -538,7 +537,7 @@ std::vector<exprt> random_tracest::random_initial_state_constraints(
 
   for(auto &symbol : state_variables)
   {
-    auto symbol_in_timeframe = instantiate(symbol, 0, 1, ns);
+    auto symbol_in_timeframe = instantiate(symbol, 0, 1);
     auto constraint =
       equal_exprt(symbol_in_timeframe, random_value(symbol.type()));
     result.push_back(std::move(constraint));

src/ebmc/ranking_function.cpp

@@ -171,14 +171,13 @@ std::pair<tvt, std::optional<trans_tracet>> is_ranking_function(
   // c) p holds in timeframe 1
 
   exprt ranking_function_decreases = less_than_exprt(
-    instantiate(ranking_function, 1, 2, ns),
-    instantiate(ranking_function, 0, 2, ns));
+    instantiate(ranking_function, 1, 2), instantiate(ranking_function, 0, 2));
   solver.set_to_false(ranking_function_decreases);
 
-  exprt p_at_0 = instantiate(p, 0, 2, ns);
+  exprt p_at_0 = instantiate(p, 0, 2);
   solver.set_to_false(p_at_0);
 
-  exprt p_at_1 = instantiate(p, 1, 2, ns);
+  exprt p_at_1 = instantiate(p, 1, 2);
   solver.set_to_false(p_at_1);
 
   decision_proceduret::resultt dec_result = solver();

src/trans-word-level/counterexample_word_level.cpp

@@ -6,15 +6,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <iostream>
+#include "counterexample_word_level.h"
+
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 #include <langapi/language_util.h>
+#include <solvers/decision_procedure.h>
 
 #include "instantiate_word_level.h"
-#include "counterexample_word_level.h"
 
-#include <util/std_expr.h>
-#include <util/symbol_table.h>
+#include <iostream>
 
 /*******************************************************************\
 

src/trans-word-level/instantiate_word_level.cpp

@@ -72,8 +72,8 @@ symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt src)
 class wl_instantiatet
 {
 public:
-  wl_instantiatet(const mp_integer &_no_timeframes, const namespacet &_ns)
-    : no_timeframes(_no_timeframes), ns(_ns)
+  explicit wl_instantiatet(const mp_integer &_no_timeframes)
+    : no_timeframes(_no_timeframes)
   {
   }
 
@@ -86,7 +86,6 @@ class wl_instantiatet
 
 protected:
   const mp_integer &no_timeframes;
-  const namespacet &ns;
 
   [[nodiscard]] std::pair<mp_integer, exprt>
   instantiate_rec(exprt, const mp_integer &t) const;
@@ -145,7 +144,7 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
   {
     // sequence expressions -- these may have multiple potential
     // match points, and evaluate to true if any of them matches
-    const auto match_points = instantiate_sequence(expr, t, no_timeframes, ns);
+    const auto match_points = instantiate_sequence(expr, t, no_timeframes);
     exprt::operandst disjuncts;
     disjuncts.reserve(match_points.size());
     mp_integer max = t;
@@ -228,10 +227,9 @@ Function: instantiate
 exprt instantiate(
   const exprt &expr,
   const mp_integer &t,
-  const mp_integer &no_timeframes,
-  const namespacet &ns)
+  const mp_integer &no_timeframes)
 {
-  wl_instantiatet wl_instantiate(no_timeframes, ns);
+  wl_instantiatet wl_instantiate(no_timeframes);
   return wl_instantiate(expr, t).second;
 }
 
@@ -250,9 +248,8 @@ Function: instantiate_property
 std::pair<mp_integer, exprt> instantiate_property(
   const exprt &expr,
   const mp_integer &current,
-  const mp_integer &no_timeframes,
-  const namespacet &ns)
+  const mp_integer &no_timeframes)
 {
-  wl_instantiatet wl_instantiate(no_timeframes, ns);
+  wl_instantiatet wl_instantiate(no_timeframes);
   return wl_instantiate(expr, current);
 }

src/trans-word-level/instantiate_word_level.h

@@ -10,21 +10,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_BMC_INSTANTIATE_WORD_LEVEL_H
 
 #include <util/mp_arith.h>
-#include <util/namespace.h>
-
-#include <solvers/prop/prop_conv.h>
+#include <util/std_expr.h>
 
 exprt instantiate(
   const exprt &expr,
   const mp_integer &current,
-  const mp_integer &no_timeframes,
-  const namespacet &);
+  const mp_integer &no_timeframes);
 
 std::pair<mp_integer, exprt> instantiate_property(
   const exprt &,
   const mp_integer &current,
-  const mp_integer &no_timeframes,
-  const namespacet &);
+  const mp_integer &no_timeframes);
 
 std::string
 timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier);