Add "pour_853_4" puzzle to examples

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/docs/examples/puzzles/pour_853_to_4.sby b/docs/examples/puzzles/pour_853_to_4.sby
new file mode 100644 (file)
index 0000000..16c4173
--- /dev/null
+++ b/docs/examples/puzzles/pour_853_to_4.sby
@@ -0,0 +1,13 @@
+[options]
+mode cover
+depth 100
+
+[engines]
+smtbmc
+
+[script]
+read -formal pour_853_to_4.sv
+prep -top pour_853_to_4
+
+[files]
+pour_853_to_4.sv

diff --git a/docs/examples/puzzles/pour_853_to_4.sv b/docs/examples/puzzles/pour_853_to_4.sv
new file mode 100644 (file)
index 0000000..ac3fe16
--- /dev/null
+++ b/docs/examples/puzzles/pour_853_to_4.sv
@@ -0,0 +1,44 @@
+// You are given an 8 litre bucket of water, and two empty buckets which can
+// contain 5 and 3 litre respectively. You are required to divide the water into
+// two by pouring water between buckets (that is, to end up with 4 litre in the 8
+// litre bucket, and 4 litre in the 5 litre bucket).
+//
+// Inspired by:
+// https://github.com/DennisYurichev/random_notes/blob/master/Z3/pour.py
+
+module pour_853_to_4 (
+       input clk,
+       input [1:0] src, dst
+);
+       reg [3:0] state [0:2];
+       reg [3:0] max_amount [0:2];
+       reg [3:0] xfer_amount;
+
+       initial begin
+               state[0] = 8;
+               state[1] = 0;
+               state[2] = 0;
+
+               max_amount[0] = 8;
+               max_amount[1] = 5;
+               max_amount[2] = 3;
+       end
+
+       always @* begin
+               assume (src < 3);
+               assume (dst < 3);
+               assume (src != dst);
+
+               if (state[src] > (max_amount[dst] - state[dst]))
+                       xfer_amount = max_amount[dst] - state[dst];
+               else
+                       xfer_amount = state[src];
+
+               cover (state[0] == 4 && state[1] == 4);
+       end
+
+       always @(posedge clk) begin
+               state[src] <= state[src] - xfer_amount;
+               state[dst] <= state[dst] + xfer_amount;
+       end
+endmodule