Add "pour_853_4" puzzle to examples

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

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

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