BMC with iterative constraint strengthening

This implements "iterative constraint strengthening" in the word-level BMC
engine (VMCAI 2009, Query-driven Program Testing), and makes it the default.
The previous, assumption-based method remains available with
--bmc-with-assumptions.

When using MiniSat, the benefit on hwmcc08 is barely measurable.  When using
Cadical, the benefit is around 10%.

MiniSat iterative   88.27s
MiniSat asumptions  88.73s
Cadical iterative  103.41s
Cadical asumptions 117.74s

CHANGELOG

@@ -1,6 +1,8 @@
 # EBMC 5.4
 
 * BMC: Cadical support with --cadical
+* BMC: iterative constraint strengthening is now default;
+  use --bmc-with-assumptions to re-enable the previous algorithm.
 
 # EBMC 5.3
 

regression/ebmc/assumptions/assume2.bmc-with-assumptions.desc

@@ -0,0 +1,8 @@
+CORE
+assume2.sv
+--bound 0 --bmc-with-assumptions
+^\[main\.a1\] assume always 10 <= main\.a && main\.a <= 100: ASSUMED$
+^\[main\.p1\] always main\.a != 200: PROVED up to bound 0$
+^\[main\.p2\] always main.a != 20: REFUTED$
+^EXIT=10$
+^SIGNAL=0$

regression/ebmc/example4_trace/test.desc

@@ -3,6 +3,6 @@ example4.sv
 --bound 10 --trace
 ^\[counter\.assert\.1\] .* PROVED up to bound 10$
 ^\[counter\.assert\.2\] .* REFUTED$
-^  counter\.state = 254 \(11111110\)$
+^  counter\.state = \d+ \([01]+\)$
 ^EXIT=10$
 ^SIGNAL=0$

regression/verilog/functioncall/functioncall2.desc

@@ -3,6 +3,6 @@ functioncall2.v
 --module main --bound 1
 ^EXIT=0$
 ^SIGNAL=0$
-^UNSAT: No counterexample found within bound$
+^UNSAT: .*$
 --
 ^warning: ignoring

regression/verilog/functioncall/functioncall3.desc

@@ -3,6 +3,6 @@ functioncall3.v
 --module main --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^UNSAT: No counterexample found within bound$
+^UNSAT: .*$
 --
 ^warning: ignoring

regression/verilog/functioncall/functioncall4.desc

@@ -3,7 +3,7 @@ functioncall4.v
 --module main --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^UNSAT: No counterexample found within bound$
+^UNSAT: .*$
 --
 ^warning: ignoring
 --

src/ebmc/bmc.cpp

@@ -17,9 +17,184 @@ Author: Daniel Kroening, [email protected]
 #include <chrono>
 #include <fstream>
 
+void bmc_with_assumptions(
+  std::size_t bound,
+  const transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  decision_proceduret &solver,
+  message_handlert &message_handler)
+{
+  messaget message(message_handler);
+  const namespacet ns(transition_system.symbol_table);
+
+  // Use assumptions to check the properties separately
+
+  for(auto &property : properties.properties)
+  {
+    if(property.is_disabled() || property.is_failure() || property.is_assumed())
+    {
+      continue;
+    }
+
+    message.status() << "Checking " << property.name << messaget::eom;
+
+    auto assumption = not_exprt{conjunction(property.timeframe_handles)};
+
+    decision_proceduret::resultt dec_result = solver(assumption);
+
+    switch(dec_result)
+    {
+    case decision_proceduret::resultt::D_SATISFIABLE:
+      if(property.is_exists_path())
+      {
+        property.proved();
+        message.result() << "SAT: path found" << messaget::eom;
+      }
+      else // universal path property
+      {
+        property.refuted();
+        message.result() << "SAT: counterexample found" << messaget::eom;
+      }
+
+      property.witness_trace = compute_trans_trace(
+        property.timeframe_handles,
+        solver,
+        bound + 1,
+        ns,
+        transition_system.main_symbol->name);
+      break;
+
+    case decision_proceduret::resultt::D_UNSATISFIABLE:
+      if(property.is_exists_path())
+      {
+        message.result() << "UNSAT: No path found within bound"
+                         << messaget::eom;
+        property.refuted_with_bound(bound);
+      }
+      else // universal path property
+      {
+        message.result() << "UNSAT: No counterexample found within bound"
+                         << messaget::eom;
+        property.proved_with_bound(bound);
+      }
+      break;
+
+    case decision_proceduret::resultt::D_ERROR:
+      message.error() << "Error from decision procedure" << messaget::eom;
+      property.failure();
+      break;
+
+    default:
+      property.failure();
+      throw ebmc_errort() << "Unexpected result from decision procedure";
+    }
+  }
+}
+
+/// VMCAI 2009 Query-driven program testing,
+/// "iterative constraint strengthening"
+void bmc_with_iterative_constraint_strengthening(
+  std::size_t bound,
+  const transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  decision_proceduret &solver,
+  message_handlert &message_handler)
+{
+  messaget message(message_handler);
+  const namespacet ns(transition_system.symbol_table);
+
+  auto trace_found = [&solver](const ebmc_propertiest::propertyt &property)
+  {
+    for(auto &h : property.timeframe_handles)
+      if(solver.get(h).is_false())
+        return true;
+    return false;
+  };
+
+  while(true)
+  {
+    // At least one of the remaining properties
+    // should be falsified.
+    exprt::operandst disjuncts;
+
+    for(auto &property : properties.properties)
+    {
+      if(property.is_unknown())
+      {
+        for(auto &h : property.timeframe_handles)
+          disjuncts.push_back(not_exprt{h});
+      }
+    }
+
+    // This constraint is strenthened in each iteration.
+    solver.set_to_true(disjunction(disjuncts));
+
+    decision_proceduret::resultt dec_result = solver();
+
+    switch(dec_result)
+    {
+    case decision_proceduret::resultt::D_SATISFIABLE:
+      // Found a trace for at least one further property with unknown state
+      message.result() << "SAT: path found" << messaget::eom;
+
+      for(auto &property : properties.properties)
+      {
+        if(property.is_unknown() && trace_found(property))
+        {
+          if(property.is_exists_path())
+            property.proved();
+          else // universal path property
+            property.refuted();
+
+          property.witness_trace = compute_trans_trace(
+            property.timeframe_handles,
+            solver,
+            bound + 1,
+            ns,
+            transition_system.main_symbol->name);
+        }
+      }
+      break; // next iteration of while loop
+
+    case decision_proceduret::resultt::D_UNSATISFIABLE:
+      message.result() << "UNSAT: No path found within bound" << messaget::eom;
+
+      for(auto &property : properties.properties)
+      {
+        if(property.is_unknown())
+        {
+          if(property.is_exists_path())
+            property.refuted_with_bound(bound);
+          else // universal path property
+            property.proved_with_bound(bound);
+        }
+      }
+      return;
+
+    case decision_proceduret::resultt::D_ERROR:
+      for(auto &property : properties.properties)
+      {
+        if(property.is_unknown())
+          property.failure();
+      }
+      message.error() << "Error from decision procedure" << messaget::eom;
+      return;
+
+    default:
+      for(auto &property : properties.properties)
+      {
+        if(property.is_unknown())
+          property.failure();
+      }
+      throw ebmc_errort() << "Unexpected result from decision procedure";
+    }
+  }
+}
+
 void bmc(
   std::size_t bound,
   bool convert_only,
+  bool bmc_with_assumptions,
   const transition_systemt &transition_system,
   ebmc_propertiest &properties,
   const ebmc_solver_factoryt &solver_factory,
@@ -76,12 +251,25 @@ void bmc(
 
   if(convert_only)
   {
+    // At least one property must be violated in at least one
+    // timeframe.
+    exprt::operandst disjuncts;
+
     for(const auto &property : properties.properties)
     {
-      if(!property.is_disabled())
-        solver.set_to_false(conjunction(property.timeframe_handles));
+      if(property.is_assumed())
+      {
+        // already added as constraint above
+      }
+      else if(!property.is_disabled())
+      {
+        for(auto &h : property.timeframe_handles)
+          disjuncts.push_back(not_exprt{h});
+      }
     }
 
+    solver.set_to_true(disjunction(disjuncts));
+
     // Call decision_proceduret::dec_solve to finish the conversion
     // process.
     (void)solver();
@@ -93,69 +281,15 @@ void bmc(
 
     auto sat_start_time = std::chrono::steady_clock::now();
 
-    // Use assumptions to check the properties separately
-
-    for(auto &property : properties.properties)
+    if(bmc_with_assumptions)
     {
-      if(
-        property.is_disabled() || property.is_failure() ||
-        property.is_assumed())
-      {
-        continue;
-      }
-
-      message.status() << "Checking " << property.name << messaget::eom;
-
-      auto assumption = not_exprt{conjunction(property.timeframe_handles)};
-
-      decision_proceduret::resultt dec_result = solver(assumption);
-
-      switch(dec_result)
-      {
-      case decision_proceduret::resultt::D_SATISFIABLE:
-        if(property.is_exists_path())
-        {
-          property.proved();
-          message.result() << "SAT: path found" << messaget::eom;
-        }
-        else // universal path property
-        {
-          property.refuted();
-          message.result() << "SAT: counterexample found" << messaget::eom;
-        }
-
-        property.witness_trace = compute_trans_trace(
-          property.timeframe_handles,
-          solver,
-          bound + 1,
-          ns,
-          transition_system.main_symbol->name);
-        break;
-
-      case decision_proceduret::resultt::D_UNSATISFIABLE:
-        if(property.is_exists_path())
-        {
-          message.result() << "UNSAT: No path found within bound"
-                           << messaget::eom;
-          property.refuted_with_bound(bound);
-        }
-        else // universal path property
-        {
-          message.result() << "UNSAT: No counterexample found within bound"
-                           << messaget::eom;
-          property.proved_with_bound(bound);
-        }
-        break;
-
-      case decision_proceduret::resultt::D_ERROR:
-        message.error() << "Error from decision procedure" << messaget::eom;
-        property.failure();
-        break;
-
-      default:
-        property.failure();
-        throw ebmc_errort() << "Unexpected result from decision procedure";
-      }
+      ::bmc_with_assumptions(
+        bound, transition_system, properties, solver, message_handler);
+    }
+    else
+    {
+      ::bmc_with_iterative_constraint_strengthening(
+        bound, transition_system, properties, solver, message_handler);
     }
 
     auto sat_stop_time = std::chrono::steady_clock::now();

src/ebmc/bmc.h

@@ -22,6 +22,7 @@ class transition_systemt;
 void bmc(
   std::size_t bound,
   bool convert_only,
+  bool bmc_with_assumptions,
   const transition_systemt &,
   ebmc_propertiest &,
   const ebmc_solver_factoryt &,

src/ebmc/ebmc_parse_options.h

@@ -47,6 +47,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(compute-ct)(dot-netlist)(smv-netlist)(vcd):"
         "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
+        "(bmc-with-assumptions)"
         "(liveness-to-safety)"
         "I:D:(preprocess)(systemverilog)(vl2smv-extensions)"
         "(warn-implicit-nets)",

src/ebmc/k_induction.cpp

@@ -202,7 +202,8 @@ void k_inductiont::induction_base()
 
   bmc(
     k,
-    false,
+    false, // convert_only
+    false, // bmc_with_assumptions
     transition_system,
     properties,
     solver_factory,

src/ebmc/property_checker.cpp

@@ -80,9 +80,12 @@ property_checker_resultt word_level_bmc(
         if(properties.properties.empty())
           throw "no properties";
 
+      bool bmc_with_assumptions = cmdline.isset("bmc-with-assumptions");
+
       bmc(
         bound,
         convert_only,
+        bmc_with_assumptions,
         transition_system,
         properties,
         solver_factory,