SAT-based neural ranking engine

This adds a variant of neural ranking that uses a SAT solver to compute the
weights and biases in the neural network.

Author: kroening

regression/ebmc/solver-neural-liveness/counter1.desc

@@ -0,0 +1,9 @@
+CORE
+counter1.sv
+--traces 1 --solver-neural-liveness
+^weight: nn::fc1\.n0\.w0 = 1$
+^bias: nn::fc1\.n0\.b = 0$
+^\[main\.property\.p0\] always s_eventually main\.counter == 0: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/solver-neural-liveness/counter1.sv

@@ -0,0 +1,16 @@
+// count down from 10 to 0
+
+module main(input clk);
+
+  reg [7:0] counter;
+
+  initial counter = 10;
+
+  always @(posedge clk)
+    if(counter != 0)
+      counter = counter - 1;
+
+  // expected to pass
+  p0: assert property (s_eventually counter == 0);
+
+endmodule

regression/ebmc/solver-neural-liveness/wrap_around1.desc

@@ -0,0 +1,9 @@
+CORE
+wrap_around1.sv
+--traces 1 --solver-neural-liveness
+^weight: nn::fc1\.n0\.w0 = -1$
+^bias: nn::fc1\.n0\.b = 9$
+^\[main\.property\.p0\] always s_eventually main\.counter == 10: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/solver-neural-liveness/wrap_around1.sv

@@ -0,0 +1,18 @@
+// count up from 0 to 10
+
+module main(input clk);
+
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(counter == 10)
+      counter = 0;
+    else
+      counter = counter + 1;
+
+  // expected to pass
+  p0: assert property (s_eventually counter == 10);
+
+endmodule

src/ebmc/Makefile

@@ -23,10 +23,12 @@ SRC = \
       output_verilog.cpp \
       random_traces.cpp \
       ranking_function.cpp \
+      ranking_net.cpp \
       report_results.cpp \
       show_formula_solver.cpp \
       show_properties.cpp \
       show_trans.cpp \
+      solver_neural_liveness.cpp \
       transition_system.cpp \
       waveform.cpp \
       #empty line

src/ebmc/ebmc_parse_options.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include "random_traces.h"
 #include "ranking_function.h"
 #include "show_trans.h"
+#include "solver_neural_liveness.h"
 
 #include <iostream>
 
@@ -162,6 +163,9 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("neural-liveness"))
       return do_neural_liveness(cmdline, ui_message_handler);
 
+    if(cmdline.isset("solver-neural-liveness"))
+      return do_solver_neural_liveness(cmdline, ui_message_handler);
+
     if(cmdline.isset("ranking-function"))
       return do_ranking_function(cmdline, ui_message_handler);
 

src/ebmc/ebmc_parse_options.h

@@ -34,6 +34,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(po)(cegar)(k-induction)(2pi)(bound2):"
         "(outfile):(xml-ui)(verbosity):(gui)(json-result):"
         "(neural-liveness)(neural-engine):"
+        "(solver-neural-liveness)"
         "(reset):"
         "(version)(verilog-rtl)(verilog-netlist)"
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"

src/ebmc/ebmc_solver_factory.h

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/decision_procedure.h>
 #include <solvers/prop/prop.h>
 
-#include <iosfwd>
+#include <fstream>
 #include <memory>
 
 class ebmc_solvert final

src/ebmc/ranking_net.cpp

@@ -0,0 +1,106 @@
+/*******************************************************************\
+
+Module: Ranking Neural Net
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "ranking_net.h"
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/std_expr.h>
+
+exprt wrap_around(exprt expr)
+{
+  // map negative values to positive ones, wrap around:
+  // -1 --> int_max-1, -2 --> int_max-2, etc.
+  auto int_max = to_signedbv_type(expr.type()).largest_expr();
+  return if_exprt{sign_exprt{expr}, plus_exprt{int_max, expr}, expr};
+}
+
+tuple_exprt wrap_around_tuple(tuple_exprt expr)
+{
+  // map negative values to positive ones, wrap around:
+  // -1 --> int_max-1, -2 --> int_max-2, etc.
+  for(auto &op : expr.operands())
+    op = wrap_around(op);
+
+  return expr;
+}
+
+tuple_exprt ranking_nett::forward(const tuple_exprt &inputs) const
+{
+  auto fc1_out = fc1.forward(inputs);
+  auto w_out = wrap_around_tuple(fc1_out);
+  return w_out;
+}
+
+ranking_nett::lineart::lineart(
+  const irep_idt &__name,
+  std::size_t in,
+  std::size_t out,
+  const typet &type)
+  : name(__name)
+{
+  neurons.reserve(out);
+
+  for(std::size_t i = 0; i < out; i++)
+  {
+    irep_idt identifier = id2string(__name) + ".n" + std::to_string(i);
+    neurons.emplace_back(identifier, in, type);
+  }
+}
+
+ranking_nett::lineart::neuront::neuront(
+  const irep_idt &__name,
+  std::size_t in,
+  const typet &type)
+  : name(__name)
+{
+  {
+    irep_idt identifier = id2string(__name) + ".b";
+    bias = symbol_exprt(identifier, type);
+  }
+
+  weights.reserve(in);
+
+  for(std::size_t i = 0; i < in; i++)
+  {
+    irep_idt identifier = id2string(__name) + ".w" + std::to_string(i);
+    weights.emplace_back(symbol_exprt{identifier, type});
+  }
+}
+
+exprt ranking_nett::lineart::neuront::forward(const tuple_exprt &input) const
+{
+  exprt::operandst result;
+  result.reserve(weights.size() + 1); // one more for bias
+
+  result.push_back(bias);
+
+  PRECONDITION(weights.size() == input.operands().size());
+
+  for(std::size_t i = 0; i < weights.size(); i++)
+    result.push_back(mult_exprt{weights[i], input.operands()[i]});
+
+  return plus_exprt{std::move(result), bias.type()};
+}
+
+exprt relu(exprt expr)
+{
+  auto zero = from_integer(0, expr.type());
+  return if_exprt{greater_than_or_equal_exprt{expr, zero}, expr, zero};
+}
+
+tuple_exprt ranking_nett::lineart::forward(const tuple_exprt &input) const
+{
+  tuple_exprt::operandst result;
+  result.reserve(neurons.size());
+
+  for(auto &neuron : neurons)
+    result.push_back(neuron.forward(input));
+
+  return tuple_exprt{std::move(result)};
+}

src/ebmc/ranking_net.h

@@ -0,0 +1,58 @@
+/*******************************************************************\
+
+Module: Ranking Neural Net
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef EBMC_RANKING_NET_H
+#define EBMC_RANKING_NET_H
+
+#include <util/mathematical_expr.h>
+
+exprt relu(exprt);
+exprt wrap_around(exprt);
+
+class ranking_nett
+{
+public:
+  explicit ranking_nett(
+    std::size_t number_of_state_variables,
+    const typet &__type)
+    : fc1("nn::fc1", number_of_state_variables, 1, __type)
+  {
+  }
+
+  tuple_exprt forward(const tuple_exprt &inputs) const;
+
+  class lineart
+  {
+  public:
+    lineart(
+      const irep_idt &name,
+      std::size_t in,
+      std::size_t out,
+      const typet &);
+
+    irep_idt name;
+
+    class neuront
+    {
+    public:
+      std::vector<exprt> weights;
+      exprt bias;
+      irep_idt name;
+      neuront(const irep_idt &name, std::size_t in, const typet &);
+      exprt forward(const tuple_exprt &) const;
+    };
+
+    std::vector<neuront> neurons;
+
+    tuple_exprt forward(const tuple_exprt &) const;
+  };
+
+  lineart fc1;
+};
+
+#endif // EBMC_RANKING_NET