2 files changed, 17 insertions(+), 0 deletions(-)

M check.ml
M solver.ml

@@ 148,6 148,19 @@ let graph () =
   Printf.printf "unfenced graph closed: %d states, %d edges, %d violating states\n%!"
     (Array.length graph.states) graph.edges (List.length graph.violations)
 
+let constraints () =
+  List.iter (fun (count, clauses) ->
+    rejects (fun () -> ignore (Solver.candidate ~count ~budget:1 clauses))
+      "invalid fence constraint")
+    [-1, []; 1, [[-1]]; 1, [[1]]; 0, [[0]]];
+  let solve count budget clauses = Solver.solve (Solver.candidate ~count ~budget clauses) in
+  require (solve 0 0 [] = Solver.Sat []) "empty candidate set satisfies zero budget";
+  require (solve 0 (-1) [] = Solver.Unsat) "negative lower budget remains unsatisfiable";
+  require (solve 2 0 [[0; 1]] = Solver.Unsat) "zero budget cannot hit a nonempty clause";
+  require (solve 2 1 [[0]; [1]] = Solver.Unsat) "independent singleton clauses require two fences";
+  require (solve 2 2 [[0]; [1]] = Solver.Sat [Solver.Truth true; Solver.Truth true])
+    "candidate values follow clause indices"
+
 let validation () =
   let case = read "buffering" in
   let open Sexp in


@@ 207,6 220,7 @@ let () =
   buffers ();
   outcomes ();
   graph ();
+  constraints ();
   validation ();
   repair folder;
   Printf.printf "%d checks passed; %d bounded reference states; %.1fs\n%!"

@@ 204,6 204,9 @@ let compile ?(timeout=300000) ?fixed ?(require_goal=true) ?(blocks=[]) case mode
   {source = Buffer.contents buffer; probes}
 
 let candidate ~count ~budget clauses =
+  if count < 0 then invalid_arg "negative fence candidate count";
+  List.iter (List.iter (fun index ->
+    if index < 0 || index >= count then invalid_arg "fence constraint index outside candidates")) clauses;
   let lines = ref [Store.read (Filename.concat (Store.root ()) "smt/fences.smt2")] in
   let add line = lines := line :: !lines in
   for i = 0 to count - 1 do add (Printf.sprintf "(declare-const f%d Bool)" i) done;