Browse Source

clean code and repo layout

master
zapashcanon 1 year ago
parent
commit
03b10bbf65
Signed by: zapashcanon GPG Key ID: 8981C3C62D1D28F1
40 changed files with 344 additions and 1335 deletions
  1. +1
    -0
      .gitignore
  2. +13
    -13
      bench/bench.ml
  3. +4
    -0
      bench/dune
  4. +8
    -0
      scripts/landmarks.sh
  5. +1
    -1
      scripts/numlink.sh
  6. +0
    -9
      scripts/printer.ml
  7. +55
    -37
      src/bdd/common.ml
  8. +5
    -0
      src/bdd/dune
  9. +2
    -2
      src/bdd/hashconsed.ml
  10. +1
    -1
      src/bdd/naive.ml
  11. +0
    -0
      src/bdd/utils.ml
  12. +0
    -29
      src/comp.ml
  13. +0
    -37
      src/dune
  14. +2
    -4
      src/expr/cli.ml
  15. +51
    -0
      src/expr/comp.ml
  16. +12
    -0
      src/expr/dune
  17. +0
    -0
      src/expr/lang.ml
  18. +0
    -0
      src/expr/lexer.mll
  19. +0
    -0
      src/expr/parser.mly
  20. +0
    -31
      src/hashcons.ml
  21. +6
    -0
      src/hashcons/dune
  22. +34
    -0
      src/hashcons/hashcons.ml
  23. +5
    -0
      src/memo/dune
  24. +8
    -12
      src/memo/memo.ml
  25. +0
    -241
      src/numlink.ml
  26. +2
    -0
      src/numlink/dune
  27. +84
    -4
      src/numlink/main.ml
  28. +24
    -132
      src/numlink/numlink.ml
  29. +0
    -9
      src/printer.ml
  30. +1
    -0
      test10.numlink
  31. +2
    -0
      test11.numlink
  32. +2
    -0
      test2.numlink
  33. +2
    -0
      test3.numlink
  34. +1
    -0
      test4.numlink
  35. +1
    -0
      test5.numlink
  36. +4
    -0
      test6.numlink
  37. +3
    -0
      test7.numlink
  38. +0
    -667
      tests/test.txt
  39. +0
    -96
      tests/test2.txt
  40. +10
    -10
      tests/tests.ml

+ 1
- 0
.gitignore View File

@ -2,3 +2,4 @@ _build/
_coverage/
*.merlin
*.out
*.json

src/bench.ml → bench/bench.ml View File

@ -1,9 +1,9 @@
module Make2 (M: Bdd.S) = struct
module Make2 (M: Bdd.Common.S) = struct
module M = Bdd.Make(M)
module M = Bdd.Common.Make(M)
let rec build l r i =
let v = Bdd.Base.var_of_string (string_of_int i) in
let v = Bdd.Common.Base.var_of_string (string_of_int i) in
if i = 1 then M.node v l r
else
let b = if i mod 2 = 0 then
@ -24,9 +24,9 @@ module Make2 (M: Bdd.S) = struct
end
module Make (M: Bdd.S) = struct
module Make (M: Bdd.Common.S) = struct
module M = Bdd.Make(M)
module M = Bdd.Common.Make(M)
let bench_one tbl expr =
let start = Unix.gettimeofday () in
@ -50,17 +50,17 @@ end
let _ =
let expr = Cli.get_expr () in
let expr = Expr.Cli.get_expr () in
let tbl = Hashtbl.create 512 in
let v = Bdd.Base.var_of_string in
let v = Bdd.Common.Base.var_of_string in
Hashtbl.add tbl (v "x") false;
Hashtbl.add tbl (v "y") true;
let module I1 = Bdd_naive.Make(Memo.Fake) in
let module I2 = Bdd_naive.Make(Memo.Make) in
let module I3 = Bdd_hashcons.Make(Memo.Fake) in
let module I4 = Bdd_hashcons.Make(Memo.Make) in
let module I1 = Bdd.Naive.Make(Memo.Fake) in
let module I2 = Bdd.Naive.Make(Memo.Make) in
let module I3 = Bdd.Hashconsed.Make(Memo.Fake) in
let module I4 = Bdd.Hashconsed.Make(Memo.Make) in
let n = 1 in
@ -84,11 +84,11 @@ let _ =
(* B3.bench_one "hashcons: ";*)
B4.bench_one "hashcons + memo:";
let module T = Bdd.Make(I4) in
let module T = Bdd.Common.Make(I4) in
let sat = T.all_sat (T.of_expr expr) in
List.iter (fun l -> print_endline "One sat is:";
List.iter (fun (v, b) ->
Printf.printf "%s = %B\n" (Bdd.Base.string_of_var v) b
Printf.printf "%s = %B\n" (Bdd.Common.Base.string_of_var v) b
) l
) sat;

+ 4
- 0
bench/dune View File

@ -0,0 +1,4 @@
(executable
(name bench)
(libraries unix bdd expr)
(modules bench))

+ 8
- 0
scripts/landmarks.sh View File

@ -0,0 +1,8 @@
#!/bin/sh
set -eu
( cd "$(dirname "$0")/../"
eval "$(opam env)"
export OCAML_LANDMARKS="output=landmarks.json,format=json,allocation"
)

+ 1
- 1
scripts/numlink.sh View File

@ -5,5 +5,5 @@ set -eu
( cd "$(dirname "$0")/../"
eval "$(opam env)"
dune exec src/numlink.exe --profile release -- "$@"
dune exec src/numlink/numlink.exe --profile release -- "$@"
)

+ 0
- 9
scripts/printer.ml View File

@ -1,9 +0,0 @@
#!/bin/sh
set -eu
( cd "$(dirname "$0")/../"
eval "$(opam env)"
dune exec src/printer.exe -- "$@"
)

src/bdd.ml → src/bdd/common.ml View File

@ -2,22 +2,24 @@ module Base = struct
type var = int
type expr = Expr.Lang.t
(* TODO *)
let inv_tbl = Hashtbl.create 512
let string_of_var = Hashtbl.find inv_tbl
let var_of_string, reset =
let var_of_string, reset, max_var =
let tbl = Hashtbl.create 512 in
let gen, reset = Utils.gen_tag () in
(fun x -> match Hashtbl.find tbl x with
| exception Not_found ->
(fun x ->
try Hashtbl.find tbl x
with Not_found ->
let v = gen () in
Hashtbl.add tbl x v;
Printf.printf "added %s -> %d\n" x v;
flush stdout;
Hashtbl.add inv_tbl v x;
v
| v -> v),
(fun () -> reset ())
Hashtbl.add tbl x v;
(* Printf.printf "added %s -> %d\n" x v;
flush stdout;*)
v),
(fun () -> reset ()),
(fun () -> Hashtbl.length tbl)
end
module type S = sig
@ -57,27 +59,52 @@ module Make (M: S) = struct
let var_bdd v = node v false_bdd true_bdd
let to_string = Mem.memo (fun to_string ->
fview (function
| True -> "true"
| False -> "false"
let to_string bdd =
let b = Buffer.create 512 in
let rec aux bdd = match view bdd with
| True -> Buffer.add_string b "true"
| False -> Buffer.add_string b "false"
| Node (var, low, high) ->
(Base.string_of_var var) ^ "(" ^ string_of_int var ^ ")" ^ " ? "
^ "(" ^ (to_string high) ^ ")"
^ ": (" ^ (to_string low) ^ ")"))
Buffer.add_string b (Base.string_of_var var);
Buffer.add_string b ("(" ^ (string_of_int var) ^ ") ? (");
aux high;
Buffer.add_string b ") : (";
aux low;
Buffer.add_string b ")"
in
aux bdd;
Buffer.contents b
let of_bool = function
| true -> true_bdd
| false -> false_bdd
let neg = Mem.memo (fun neg ->
let neg x = Mem.memo (fun neg ->
fview (function
| True -> false_bdd
| False -> true_bdd
| Node (var, low, high) -> node var (neg low) (neg high)))
| Node (var, low, high) -> node var (neg low) (neg high))) x
(* let rec comb_comm op n1 n2 =
let comb_comm = comb_comm op in *)
let comb_comm op x y = Mem.memo2 (fun comb_comm n1 n2 ->
match view n1, view n2 with
| Node (v1, l1, h1), Node (v2, l2, h2) when v1 = v2 ->
node v1 (comb_comm l1 l2) (comb_comm h1 h2)
| Node (v1, l1, h1), Node (v2, _, _) when v1 < v2 ->
node v1 (comb_comm l1 n2) (comb_comm h1 n2)
| Node (_, _, _), Node (v2, l2, h2) ->
node v2 (comb_comm n1 l2) (comb_comm n1 h2)
| True, Node (v, l, h) | Node (v, l, h), True ->
node v (comb_comm l true_bdd) (comb_comm h true_bdd)
| False, Node (v, l, h) | Node (v, l, h), False ->
node v (comb_comm l false_bdd) (comb_comm h false_bdd)
| False, False -> of_bool (op false false)
| False, True | True, False -> of_bool (op true false)
| True, True -> of_bool (op true true)
) x y
let comb op = Mem.memo2 (fun comb n1 n2 ->
let comb op x y = Mem.memo2 (fun comb n1 n2 ->
match view n1, view n2 with
| Node (v1, l1, h1), Node (v2, l2, h2) when v1 = v2 ->
node v1 (comb l1 l2) (comb h1 h2)
@ -96,12 +123,12 @@ module Make (M: S) = struct
| False, False -> of_bool (op false false)
| False, True -> of_bool (op false true)
| True, False -> of_bool (op true false)
| True, True -> of_bool (op true true))
| True, True -> of_bool (op true true)) x y
let conj = comb (fun x y -> x && y)
let disj = comb (fun x y -> x || y)
let conj = comb_comm (fun x y -> x && y)
let disj = comb_comm (fun x y -> x || y)
let imp = comb (fun x y -> (not x) || y)
let eq = comb (fun x y -> x = y)
let eq = comb_comm (fun x y -> x = y)
let compute tbl =
let compute_aux = Mem.memo (fun compute_aux ->
@ -126,27 +153,18 @@ module Make (M: S) = struct
E.And (E.Var (Base.string_of_var v), (to_expr l)),
E.And (E.Neg (E.Var (Base.string_of_var v)), (to_expr h)))))
module MemoExpr = Memo.Fake(struct
type t = Base.expr
let equal = (=)
let hash = Hashtbl.hash
end)
(* TODO: call reset each time *)
let of_expr = MemoExpr.memo (fun of_expr ->
let rec of_expr =
let module E = Expr.Lang in function
| E.True -> true_bdd
| E.False -> false_bdd
| E.Var v -> (try var_bdd (int_of_string v) with
| _ -> var_bdd (Base.var_of_string (E.var_to_string v)))
| E.Var v -> (try var_bdd (int_of_string v) with _ -> var_bdd (Base.var_of_string (E.var_to_string v)))
| E.Neg e -> neg (of_expr e)
| E.And (e1, e2) -> conj (of_expr e1) (of_expr e2)
| E.Or (e1, e2) -> disj (of_expr e1) (of_expr e2)
| E.Imp (e1, e2) -> imp (of_expr e1) (of_expr e2)
| E.Eq (e1, e2) -> eq (of_expr e1) (of_expr e2)
(* TODO: there's probably a better way without having to construct the full expr *)
| E.BigAnd e -> of_expr (Seq.fold_left (fun acc el -> E.And (el, acc)) E.True e)
| E.BigOr e -> of_expr (Seq.fold_left (fun acc el -> E.Or (el, acc)) E.False e))
| E.BigAnd e -> Seq.fold_left (fun acc el -> conj (of_expr el) acc) true_bdd e
| E.BigOr e -> Seq.fold_left (fun acc el -> disj (of_expr el) acc) false_bdd e
let of_string s = of_expr (Expr.Comp.from_string s)

+ 5
- 0
src/bdd/dune View File

@ -0,0 +1,5 @@
(library
(name bdd)
(modules common hashconsed naive utils)
(preprocess (pps bisect_ppx -conditional landmarks.ppx --auto))
(libraries expr memo hashcons landmarks))

src/bdd_hashcons.ml → src/bdd/hashconsed.ml View File

@ -6,7 +6,7 @@ module Make(M: Memo.F) = struct
and view =
| True
| False
| Node of Bdd.Base.var * hidden * hidden
| Node of Common.Base.var * hidden * hidden
module Hbdd = Hashcons.Make(struct
type t = view
@ -17,7 +17,7 @@ module Make(M: Memo.F) = struct
let hash = function
| True -> 1
| False -> 0
| Node (v, l, r) -> 19191919 * v * l.tag * r.tag + 2
| Node (v, l, r) -> 19 * (19 * v + l.tag) + r.tag + 2
end)
module Hash = struct

src/bdd_naive.ml → src/bdd/naive.ml View File

@ -4,7 +4,7 @@ module Make(M: Memo.F) = struct
and view =
| True
| False
| Node of Bdd.Base.var * hidden * hidden
| Node of Common.Base.var * hidden * hidden
module Hash = struct
type t = hidden

src/utils.ml → src/bdd/utils.ml View File


+ 0
- 29
src/comp.ml View File

@ -1,29 +0,0 @@
exception Stop
let from_lexing buf =
match Parser.expr_final Lexer.token buf with
| exception Lexer.Error msg -> failwith ("lexer: " ^ msg)
| exception _ ->
let err_pos = Lexing.lexeme_start buf in
let err_line, line_offset = ref 1, ref 0 in
( try List.iter (fun x -> if x > err_pos then raise Stop; incr err_line; line_offset := x) (Lexer.get_mem_new_line ())
with | Stop -> ());
failwith (Printf.sprintf "parser: On line %d, at offset %d, syntax error." (!err_line) (err_pos - !line_offset))
| res -> res
let from_file f =
let chan = open_in f in
let buf = Lexing.from_channel chan in
let res = from_lexing buf in
close_in chan;
res
let from_string s =
let buf = Lexing.from_string s in
from_lexing buf
let list_to_conj =
List.fold_left (fun acc el -> Lang.And (el, acc)) True

+ 0
- 37
src/dune View File

@ -1,37 +0,0 @@
(executable
(name bench)
(libraries unix bdd cli)
(modules bench))
(executable
(name printer)
(libraries cli bdd expr)
(modules printer))
(executable
(name numlink)
(libraries expr bdd)
(modules numlink))
(library
(name cli)
(libraries expr)
(modules cli))
(library
(name expr)
(modules lang comp parser lexer))
(library
(name bdd)
(modules bdd bdd_naive bdd_hashcons hashcons utils memo)
(wrapped false)
(preprocess (pps bisect_ppx -conditional))
(libraries expr))
(ocamllex
(modules lexer))
(menhir
(modules parser)
(flags ("--explain" "--dump")))

src/cli.ml → src/expr/cli.ml View File

@ -8,10 +8,8 @@ let get_expr () =
("-e", Arg.String (fun s -> e := Some s), "expression");
] (fun _ -> ()) "get_expr";
let module E = Expr.Comp in
match !e, !f with
| Some _, Some _ -> raise (Arg.Bad "file or expression, not both")
| Some e, _ -> E.from_string e
| _, Some f -> E.from_file f
| Some e, _ -> Comp.from_string e
| _, Some f -> Comp.from_file f
| None, None -> raise (Arg.Bad "file or expression needed")

+ 51
- 0
src/expr/comp.ml View File

@ -0,0 +1,51 @@
exception Stop
open Lang
let from_lexing buf =
match Parser.expr_final Lexer.token buf with
| exception Lexer.Error msg -> failwith ("lexer: " ^ msg)
| exception _ ->
let err_pos = Lexing.lexeme_start buf in
let err_line, line_offset = ref 1, ref 0 in
( try List.iter (fun x -> if x > err_pos then raise Stop; incr err_line; line_offset := x) (Lexer.get_mem_new_line ())
with | Stop -> ());
failwith (Printf.sprintf "parser: On line %d, at offset %d, syntax error." (!err_line) (err_pos - !line_offset))
| res -> res
let from_file f =
let chan = open_in f in
let buf = Lexing.from_channel chan in
let res = from_lexing buf in
close_in chan;
res
let from_string s =
let buf = Lexing.from_string s in
from_lexing buf
let list_to_conj l =
Lang.BigAnd (List.to_seq l)
let rec print fmt = function
| True -> Format.fprintf fmt "true"
| False -> Format.fprintf fmt "false"
| Var v -> Format.fprintf fmt "@[%S@]" v
| Neg e -> Format.fprintf fmt "(@[NOT %a@])" print e
| And (e1, e2) -> Format.fprintf fmt "(@[%a AND@ %a@])" print e1 print e2
| Or (e1, e2) -> Format.fprintf fmt "(@[%a OR@ %a@])" print e1 print e2
| Imp (e1, e2) -> Format.fprintf fmt "(@[%a =>@ %a@])" print e1 print e2
| Eq (e1, e2) -> Format.fprintf fmt "(@[%a <=>@ %a@])" print e1 print e2
| BigAnd s ->
Format.fprintf fmt "(@[%a@])"
(Format.pp_print_list
~pp_sep:(fun fmt -> fun () -> Format.fprintf fmt " AND@ ")
print)
(List.of_seq s)
| BigOr s ->
Format.fprintf fmt "(@[%a@])"
(Format.pp_print_list
~pp_sep:(fun fmt -> fun () -> Format.fprintf fmt " OR@ ")
print) (List.of_seq s)

+ 12
- 0
src/expr/dune View File

@ -0,0 +1,12 @@
(library
(name expr)
(libraries landmarks)
(preprocess (pps landmarks.ppx --auto))
(modules lang comp parser lexer cli))
(ocamllex
(modules lexer))
(menhir
(modules parser)
(flags ("--explain" "--dump")))

src/lang.ml → src/expr/lang.ml View File


src/lexer.mll → src/expr/lexer.mll View File


src/parser.mly → src/expr/parser.mly View File


+ 0
- 31
src/hashcons.ml View File

@ -1,31 +0,0 @@
type 'a hash_consed = {
node: 'a;
tag: int;
}
module Make(H: Hashtbl.HashedType) = struct
type key = H.t
type data = key hash_consed
module E = Ephemeron.K1.Make(H)
type t = data E.t
let create = E.create
let clear = E.clear
let iter = E.iter
let hashcons =
let gen, _ = Utils.gen_tag () in
fun tbl k ->
match E.find tbl k with
| exception Not_found -> (
let v = {
tag = gen ();
node = k;
} in
E.add tbl k v;
v)
| v -> v
end

+ 6
- 0
src/hashcons/dune View File

@ -0,0 +1,6 @@
(library
(name hashcons)
(modules hashcons)
(wrapped false)
(libraries landmarks)
(preprocess (pps bisect_ppx -conditional landmarks.ppx --auto)))

+ 34
- 0
src/hashcons/hashcons.ml View File

@ -0,0 +1,34 @@
type 'a hash_consed = {
node: 'a;
tag: int;
}
module Make(H: Hashtbl.HashedType) = struct
type key = H.t
type data = key hash_consed
module E = Ephemeron.K1.Make(H)
type t = data E.t
let create n =
let tbl = E.create n in
at_exit (fun () ->
Format.printf "alive bindings: %d@." (E.stats_alive tbl).num_bindings;
E.clean tbl;
Format.printf "alive bindings: %d@." (E.stats_alive tbl).num_bindings);
tbl
let clear = E.clear
let iter = E.iter
let hashcons =
let gen =
let count = ref (-1) in
fun () -> incr count; !count
in
fun tbl k ->
try E.find tbl k with
| Not_found -> let v = {tag = gen (); node = k} in
E.add tbl k v; v
end

+ 5
- 0
src/memo/dune View File

@ -0,0 +1,5 @@
(library
(name memo)
(libraries landmarks)
(preprocess (pps landmarks.ppx --auto))
(modules memo))

src/memo.ml → src/memo/memo.ml View File

@ -11,12 +11,10 @@ module Make (H: Hashtbl.HashedType) = struct
module Hash = Hashtbl.Make(H)
let memo ff =
let tbl = Hash.create 512 in
let rec f k = match Hash.find tbl k with
| exception Not_found ->
let v = ff f k in
Hash.add tbl k v;
v
| v -> v
let rec f k =
try Hash.find tbl k
with Not_found ->
let v = ff f k in Hash.add tbl k v; v
in
f
module Hash2 = Hashtbl.Make(struct
@ -26,12 +24,10 @@ module Make (H: Hashtbl.HashedType) = struct
end)
let memo2 ff =
let tbl = Hash2.create 512 in
let rec f k1 k2 = match Hash2.find tbl (k1, k2) with
| exception Not_found ->
let v = ff f k1 k2 in
Hash2.add tbl (k1, k2) v;
v
| v -> v
let rec f k1 k2 =
try Hash2.find tbl (k1, k2)
with Not_found ->
let v = ff f k1 k2 in Hash2.add tbl (k1, k2) v; v
in
f
end

+ 0
- 241
src/numlink.ml View File

@ -1,241 +0,0 @@
let empty_set () = Hashtbl.create 512
let set_add s el = Hashtbl.add s el ()
let set_iter f = Hashtbl.iter (fun k _ -> f k)
let set_mem = Hashtbl.mem
let empty_graph () = empty_set (), empty_set ()
let add_vertex g v = set_add (fst g) v
let add_edge g v v' = set_add (snd g) (v, v')
let set_to_list s = List.of_seq (Hashtbl.to_seq_keys s)
let set_length = Hashtbl.length
module E = Expr.Lang
let set_conj f s =
List.fold_left (fun acc el ->
E.And (f el, acc)
) E.True (set_to_list s)
let set_disj f s =
List.fold_left (fun acc el ->
E.Or (f el, acc)
) E.False (set_to_list s)
let matrix3 l1 l2 l3 =
List.fold_left (fun acc el ->
(List.fold_left (fun acc' el' ->
(List.fold_left (fun acc'' el'' ->
(el, el', el'')::acc''
) [] l3) @ acc'
) [] l2) @ acc
) [] l1
let path_pos _ = empty_set ()
let pos_occupied_once_in_path _ _ = E.True
let range_list n =
let res = ref [] in
for i = n - 1 downto 0 do
res := i::(!res)
done;
!res
let filter_vertex s v =
Seq.filter (fun (el, _, _) -> el = v) s
let var_to_string (v, path, pos) =
let v = match v with
| None -> "phantom"
| Some (vx, vy) -> Printf.sprintf "(%d,%d)" vx vy
in
Printf.sprintf "vertex %s is on path %d at pos %d" v path pos
let has_vertex v x =
let v', _, _ = x in
if v = v' then E.Var (var_to_string x)
else E.False
let has_path p x =
let _, p', _ = x in
if p = p' then E.Var (var_to_string x)
else E.False
let has_pos p x =
let _, _, p'= x in
if p = p' then E.Var (var_to_string x)
else E.False
let is_pos_lt n x =
let _, _, p = x in
if p < n then E.Var (var_to_string x)
else E.False
let filter_path s p =
Seq.filter (fun (_, el, _) -> el = p) s
let filter_pos s p =
Seq.filter (fun (_, _, el) -> el = p) s
(* takes a seq x0 x1 ... xn and builds:
* ( x0 && !x1 && !x2 ... && !xn)
* || (!x0 && x1 && !x2 ... && !xn)
* || (...)
* || (!x0 && !x1 && !x2 ... && xn) *)
let one_and_only_one s =
E.BigOr (Seq.map (fun x ->
E.BigAnd (Seq.map (fun x' ->
let xv = E.Var (var_to_string x') in
if x = x' then xv else E.Neg xv
) s)
) s)
let for_all e f =
E.BigAnd (Seq.map f e)
let exists e f =
E.BigOr (Seq.map f e)
let exists_unique e f =
E.BigOr (Seq.map (fun x ->
E.BigAnd (Seq.map (fun x' ->
if x = x' then f x else E.Neg (f x')
) e)
) e)
let without_phantom = Seq.filter (function None -> false | _ -> true)
let vertex_appears_once vars vertices =
for_all (vertices |> without_phantom) (fun vertex ->
one_and_only_one (filter_vertex vars vertex))
let path_pos_occupied_once vertices paths positions =
for_all paths (fun path ->
for_all positions (fun pos ->
exists_unique vertices (fun vertex -> E.Var (var_to_string (vertex, path, pos)) )))
let are_adjacent edges v v' = match v, v' with
| None, _ | _, None -> false
| Some v, Some v' -> set_mem edges (v, v') || set_mem edges (v', v)
let path_finished paths positions n =
for_all paths (fun path ->
for_all positions (fun pos ->
if pos < n - 1 then
E.Imp (
E.Var (var_to_string (None, path, pos)),
E.Var (var_to_string (None, path, pos + 1)))
else E.True))
let conseq_in_path_imply_adjacent paths positions vertices edges n =
for_all paths (fun path ->
for_all positions (fun pos ->
if pos < (n - 1) then begin
for_all (vertices |> without_phantom) (fun vertex ->
for_all (vertices |> without_phantom) (fun vertex' ->
let v1 = E.Var (var_to_string (vertex, path, pos)) in
let v2 = E.Var (var_to_string (vertex', path, pos + 1)) in
if are_adjacent edges vertex vertex' then E.True else E.Neg (E.And (v1, v2))))
end
else E.True))
let check_src_dst to_connect positions n paths =
let to_connect = set_to_list to_connect in
for_all paths (fun i ->
let src, dst = List.nth to_connect i in
let v_src = E.Var (var_to_string (Some src, i, 0)) in
E.And (v_src,
exists positions (fun pos ->
let v_dst = E.Var (var_to_string (Some dst, i, pos)) in
E.And (v_dst, if pos < n - 1 then E.Var (var_to_string (None, i, pos +
1)) else E.True))
))
let build_expr (vertices, edges) to_connect =
(* adding the phantom vertex as None and making others Some *)
let vertices' = empty_set () in
set_iter (fun x -> set_add vertices' (Some x)) vertices;
set_add vertices' None;
let vertices = vertices' in
let k = set_length to_connect in
let n = set_length vertices - 1 in (* we don't count the phantom vertex ! *)
let vertices = set_to_list vertices in
let paths = range_list k in
let positions = range_list n in
let vars = matrix3 vertices paths positions in
let vars = List.to_seq vars in
let vertices = List.to_seq vertices in
let paths = List.to_seq paths in
let positions = List.to_seq positions in
let c1 = vertex_appears_once vars vertices in
let c2 = path_pos_occupied_once vertices paths positions in
let c3 = path_finished paths positions n in
let c4 = conseq_in_path_imply_adjacent paths positions vertices edges n in
let c5 = check_src_dst to_connect positions n paths in
Expr.Comp.list_to_conj [
c1;
c2;
c3;
c4;
c5;
]
let _ =
let graph = empty_graph () in
let pairs = empty_set () in
List.iter (add_vertex graph) [
(0, 0);
(0, 1);
(1, 0);
(1, 1);
];
let add_edge = add_edge graph in
add_edge (0, 0) (0, 1);
add_edge (0, 0) (1, 0);
add_edge (1, 1) (0, 1);
add_edge (1, 1) (1, 0);
let add_pair x y = set_add pairs (x, y) in
add_pair (0, 0) (1, 0);
add_pair (0, 1) (1, 1);
let to_solve = build_expr graph pairs in
let module M = Bdd.Make(Bdd_hashcons.Make(Memo.Make)) in
let bdd = M.of_expr to_solve in
print_endline (M.to_string bdd);
let print_sol = List.iter (fun (n, v) -> if v then Printf.printf "%s -> %B\n"
(Bdd.Base.string_of_var n) v) in
(*
( match M.any_sat bdd with
| None -> print_endline "no solution"
| Some sol -> List.iter (fun (n, v) -> Printf.printf "%s -> %B\n" (Bdd.Base.string_of_var n) v) sol );
*)
List.iter ( fun l -> print_sol l; print_endline "======="
) (M.all_sat bdd);
Printf.printf "number of sol: %d\n" (List.length (M.all_sat bdd));

+ 2
- 0
src/numlink/dune View File

@ -1,5 +1,7 @@
(executable
(name main)
(libraries expr bdd landmarks)
(preprocess (pps landmarks.ppx --auto))
(modules main parser lexer numlink))
(ocamllex


+ 84
- 4
src/numlink/main.ml View File

@ -42,21 +42,36 @@ let get_cli () =
| None, None -> raise (Arg.Bad "file or expression needed")
let print_parsed_list =
Format.printf "parsed grid is:@.";
List.iter (fun el ->
List.iter (function
| None -> print_string "x"
| Some i -> print_int i
) el; print_endline ""
| None -> Format.printf "x"
| Some i -> Format.printf "%d" i
) el; Format.printf "@."
)
let assert_correct_size = function
| [] | [_] -> ()
| [] -> ()
| x::s ->
let len = List.length x in
List.iter (fun el ->
assert ((List.length el) = len)
) s
let assert_correct_num m =
let tbl = Hashtbl.create 256 in
List.iter (fun el ->
List.iter (function
| None -> ()
| Some el -> (match Hashtbl.find tbl el with
| exception Not_found -> Hashtbl.add tbl el 1
| x -> Hashtbl.replace tbl el (x + 1))
) el
) m;
Hashtbl.iter (fun _ v ->
assert (v = 2)
) tbl
let _ =
let map = get_cli () in
@ -64,6 +79,71 @@ let _ =
print_parsed_list map;
assert_correct_size map;
assert_correct_num map;
let height = List.length map in
let width = match map with
| [] -> failwith "invalid map size"
| x::_ -> List.length x
in
(* Format.printf "width = %d ; height = %d@." width height; *)
let tbl = Hashtbl.create 256 in
List.iteri (fun j el->
List.iteri (fun i -> function
| None -> ()
| Some el -> (match Hashtbl.find tbl el with
| exception Not_found -> Hashtbl.add tbl el [(i, j)]
| x -> Hashtbl.replace tbl el ([i, j] @ x))
) el
) map;
let graph = Numlink.empty_graph () in
let pairs = Numlink.empty_set () in
for i = 0 to width - 1 do
for j = 0 to height - 1 do
Numlink.add_vertex graph (i, j)
done;
done;
let is_in_graph (x, y) =
x >= 0 && y >= 0 && x < width && y < height
in
let add_if_in_graph p p' =
if is_in_graph p' then Numlink.add_edge graph p p'
in
for i = 0 to width - 1 do
for j = 0 to height - 1 do
add_if_in_graph (i, j) (i + 1, j);
add_if_in_graph (i, j) (i, j + 1)
done;
done;
Hashtbl.iter (fun _ -> function
| x::y::[] -> Numlink.set_add pairs (x, y)
| _ -> failwith "not a pair..."
) tbl;
Format.printf "building the expression...@.";
let to_solve = Numlink.build_expr graph pairs in
let module M = Bdd.Common.Make(Bdd.Hashconsed.Make(Memo.Make)) in
Format.printf "building bdd...@.";
let bdd = M.of_expr to_solve in
Format.printf "done !@.";
let max_var = Bdd.Common.Base.max_var () in
Format.printf "size = %d ; max_var = %d@." (M.size bdd) max_var;
Format.printf "count_sat = %d@." (M.count_sat max_var bdd);
let res = M.any_sat bdd in
match res with
| None -> Format.printf "pas de solution@."
| Some l -> List.iter (fun (v, b) -> if b then Format.printf "%s@."
(Bdd.Common.Base.string_of_var v)) l
;
()

+ 24
- 132
src/numlink/numlink.ml View File

@ -10,29 +10,6 @@ let set_length = Hashtbl.length
module E = Expr.Lang
let set_conj f s =
List.fold_left (fun acc el ->
E.And (f el, acc)
) E.True (set_to_list s)
let set_disj f s =
List.fold_left (fun acc el ->
E.Or (f el, acc)
) E.False (set_to_list s)
let matrix3 l1 l2 l3 =
List.fold_left (fun acc el ->
(List.fold_left (fun acc' el' ->
(List.fold_left (fun acc'' el'' ->
(el, el', el'')::acc''
) [] l3) @ acc'
) [] l2) @ acc
) [] l1
let path_pos _ = empty_set ()
let pos_occupied_once_in_path _ _ = E.True
let range_list n =
let res = ref [] in
@ -51,46 +28,7 @@ let var_to_string (v, path, pos) =
| None -> "phantom"
| Some (vx, vy) -> Printf.sprintf "(%d,%d)" vx vy
in
Printf.sprintf "vertex %s is on path %d at pos %d" v path pos
let has_vertex v x =
let v', _, _ = x in
if v = v' then E.Var (var_to_string x)
else E.False
let has_path p x =
let _, p', _ = x in
if p = p' then E.Var (var_to_string x)
else E.False
let has_pos p x =
let _, _, p'= x in
if p = p' then E.Var (var_to_string x)
else E.False
let is_pos_lt n x =
let _, _, p = x in
if p < n then E.Var (var_to_string x)
else E.False
let filter_path s p =
Seq.filter (fun (_, el, _) -> el = p) s
let filter_pos s p =
Seq.filter (fun (_, _, el) -> el = p) s
(* takes a seq x0 x1 ... xn and builds:
* ( x0 && !x1 && !x2 ... && !xn)
* || (!x0 && x1 && !x2 ... && !xn)
* || (...)
* || (!x0 && !x1 && !x2 ... && xn) *)
let one_and_only_one s =
E.BigOr (Seq.map (fun x ->
E.BigAnd (Seq.map (fun x' ->
let xv = E.Var (var_to_string x') in
if x = x' then xv else E.Neg xv
) s)
) s)
Printf.sprintf "%s: path %d, pos %d" v path pos
let for_all e f =
E.BigAnd (Seq.map f e)
@ -107,14 +45,20 @@ let exists_unique e f =
let without_phantom = Seq.filter (function None -> false | _ -> true)
let vertex_appears_once vars vertices =
let mk vertex path pos =
E.Var (var_to_string (vertex, path, pos))
let vertex_appears_once vertices paths positions =
for_all (vertices |> without_phantom) (fun vertex ->
one_and_only_one (filter_vertex vars vertex))
exists_unique paths (fun path ->
exists_unique positions (fun pos ->
mk vertex path pos)))
let path_pos_occupied_once vertices paths positions =
for_all paths (fun path ->
for_all positions (fun pos ->
exists_unique vertices (fun vertex -> E.Var (var_to_string (vertex, path, pos)) )))
exists_unique vertices (fun vertex ->
mk vertex path pos)))
let are_adjacent edges v v' = match v, v' with
| None, _ | _, None -> false
@ -123,10 +67,7 @@ let are_adjacent edges v v' = match v, v' with
let path_finished paths positions n =
for_all paths (fun path ->
for_all positions (fun pos ->
if pos < n - 1 then
E.Imp (
E.Var (var_to_string (None, path, pos)),
E.Var (var_to_string (None, path, pos + 1)))
if pos < n - 1 then E.Imp (mk None path pos, mk None path (pos + 1))
else E.True))
let conseq_in_path_imply_adjacent paths positions vertices edges n =
@ -136,9 +77,8 @@ let conseq_in_path_imply_adjacent paths positions vertices edges n =
if pos < (n - 1) then begin
for_all (vertices |> without_phantom) (fun vertex ->
for_all (vertices |> without_phantom) (fun vertex' ->
let v1 = E.Var (var_to_string (vertex, path, pos)) in
let v2 = E.Var (var_to_string (vertex', path, pos + 1)) in
if are_adjacent edges vertex vertex' then E.True else E.Neg (E.And (v1, v2))))
if are_adjacent edges vertex vertex' then E.True
else E.Neg (E.And (mk vertex path pos, mk vertex' path (pos + 1)))))
end
else E.True))
@ -146,16 +86,14 @@ let check_src_dst to_connect positions n paths =
let to_connect = set_to_list to_connect in
for_all paths (fun i ->
let src, dst = List.nth to_connect i in
let v_src = E.Var (var_to_string (Some src, i, 0)) in
E.And (v_src,
E.And (mk (Some src) i 0,
exists positions (fun pos ->
let v_dst = E.Var (var_to_string (Some dst, i, pos)) in
E.And (v_dst, if pos < n - 1 then E.Var (var_to_string (None, i, pos +
1)) else E.True))
))
let v = mk (Some dst) i pos in
if pos < n - 1 then
E.And (v, mk None i (pos + 1))
else v)))
let build_expr (vertices, edges) to_connect =
@ -172,18 +110,20 @@ let build_expr (vertices, edges) to_connect =
let paths = range_list k in
let positions = range_list n in
let vars = matrix3 vertices paths positions in
let vars = List.to_seq vars in
let vertices = List.to_seq vertices in
let paths = List.to_seq paths in
let positions = List.to_seq positions in
let c1 = vertex_appears_once vars vertices in
let c1 = vertex_appears_once vertices paths positions in
(*Expr.Comp.print (Format.formatter_of_out_channel stdout) c1;*)
let c2 = path_pos_occupied_once vertices paths positions in
(*Expr.Comp.print (Format.formatter_of_out_channel stdout) c2;*)
let c3 = path_finished paths positions n in
(*Expr.Comp.print (Format.formatter_of_out_channel stdout) c3;*)
let c4 = conseq_in_path_imply_adjacent paths positions vertices edges n in
(*Expr.Comp.print (Format.formatter_of_out_channel stdout) c4;*)
let c5 = check_src_dst to_connect positions n paths in
(*Expr.Comp.print (Format.formatter_of_out_channel stdout) c5;*)
Expr.Comp.list_to_conj [
c1;
@ -192,51 +132,3 @@ let build_expr (vertices, edges) to_connect =
c4;
c5;
]
let _ =
let graph = empty_graph () in
let pairs = empty_set () in
List.iter (add_vertex graph) [
(0, 0);
(0, 1);
(1, 0);
(1, 1);
];
let add_edge = add_edge graph in
add_edge (0, 0) (0, 1);
add_edge (0, 0) (1, 0);
add_edge (1, 1) (0, 1);
add_edge (1, 1) (1, 0);
let add_pair x y = set_add pairs (x, y) in
add_pair (0, 0) (1, 0);
add_pair (0, 1) (1, 1);
let to_solve = build_expr graph pairs in
let module M = Bdd.Make(Bdd_hashcons.Make(Memo.Make)) in
let bdd = M.of_expr to_solve in
print_endline (M.to_string bdd);
let print_sol = List.iter (fun (n, v) -> if v then Printf.printf "%s -> %B\n"
(Bdd.Base.string_of_var n) v) in
(*
( match M.any_sat bdd with
| None -> print_endline "no solution"
| Some sol -> List.iter (fun (n, v) -> Printf.printf "%s -> %B\n" (Bdd.Base.string_of_var n) v) sol );
*)
List.iter ( fun l -> print_sol l; print_endline "======="
) (M.all_sat bdd);
Printf.printf "number of sol: %d\n" (List.length (M.all_sat bdd));

+ 0
- 9
src/printer.ml View File

@ -1,9 +0,0 @@
let _ =
let expr = Cli.get_expr () in
let module I = Bdd.Make(Bdd_naive.Make(Memo.Make)) in
print_endline (I.to_string (I.of_expr expr));
Printf.printf "%d\n" (I.count_sat 2 (I.of_expr expr))

+ 1
- 0
test10.numlink View File

@ -0,0 +1 @@
1xxxxxxxx1

+ 2
- 0
test11.numlink View File

@ -0,0 +1,2 @@
1x1
2x2

+ 2
- 0
test2.numlink View File

@ -0,0 +1,2 @@
1xxxx
xxxx1

+ 2
- 0
test3.numlink View File

@ -0,0 +1,2 @@
1xx
xx1

+ 1
- 0
test4.numlink View File

@ -0,0 +1 @@
1x1

+ 1
- 0
test5.numlink View File

@ -0,0 +1 @@
11

+ 4
- 0
test6.numlink View File

@ -0,0 +1,4 @@
123
xx3
xxx
x12

+ 3
- 0
test7.numlink View File

@ -0,0 +1,3 @@
1xx
xxx
xx1

+ 0
- 667
tests/test.txt View File

@ -1,667 +0,0 @@
(0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x