Computer Science
Jaspereric
fwd.zipdune-workspace
(lang dune 1.0) (context default) (profile release)
_tags
<src/**>: include
dune-project
(lang dune 1.0)
Makefile
build: main main: main.byte %.native: src/*.* @ocamlbuild $@ %.byte: src/*.* @ocamlbuild -tag debug $@ clean: @ocamlbuild -clean
dune
(library (name cs314) (modules final))
final.ml
open Stdlib let _ = Random.self_init () type term = | Constant of string | Variable of string | Function of string * term list type head = term type body = term list type clause = Fact of head | Rule of head * body type program = clause list type goal = term list let rec string_of_f_list f tl = let _, s = List.fold_left (fun (first, s) t -> let prefix = if first then "" else s ^ ", " in false, prefix ^ (f t)) (true,"") tl in s let rec string_of_term t = match t with | Constant c -> c | Variable v -> v | Function (f,tl) -> f ^ "(" ^ (string_of_f_list string_of_term tl) ^ ")" let string_of_term_list fl = string_of_f_list string_of_term fl let string_of_goal g = "?- " ^ (string_of_term_list g) let string_of_clause c = match c with | Fact f -> string_of_term f ^ "." | Rule (h,b) -> string_of_term h ^ " :- " ^ (string_of_term_list b) ^ "." let string_of_program p = let rec loop p acc = match p with | [] -> acc | [c] -> acc ^ (string_of_clause c) | c::t -> loop t (acc ^ (string_of_clause c) ^ "\n") in loop p "" let var v = Variable v let const c = Constant c let func f l = Function (f,l) let fact f = Fact f let rule h b = Rule (h,b) (* Problem 1 *) let rec occurs_check v t = raise (Failure "Problem 1 Not implemented") (* Problem 2 *) module VarSet = Set.Make(struct type t = term let compare = Stdlib.compare end) (* API Docs for Set : https://caml.inria.fr/pub/docs/manual-ocaml/libref/Set.S.html *) let rec variables_of_term t = raise (Failure "Problem 2 Not implemented") let variables_of_clause c = raise (Failure "Problem 2 Not implemented") (* Problem 3 *) module Substitution = Map.Make(struct type t = term let compare = Stdlib.compare end) (* See API docs for OCaml Map: https://caml.inria.fr/pub/docs/manual-ocaml/libref/Map.S.html *) let string_of_substitution s = "{" ^ ( Substitution.fold ( fun v t s -> match v with | Variable v -> s ^ "; " ^ v ^ " -> " ^ (string_of_term t) | Constant _ -> assert false (* substitution maps a variable to a term *) | Function _ -> assert false (* substitution maps a variable to a term *) ) s "" ) ^ "}" let rec substitute_in_term s t = raise (Failure "Problem 3 Not implemented") let substitute_in_clause s c = raise (Failure "Problem 3 Not implemented") (* Problem 4 *) let counter = ref 0 let fresh () = let c = !counter in counter := !counter + 1; Variable ("_G" ^ string_of_int c) let freshen c = let vars = variables_of_clause c in let s = VarSet.fold (fun v s -> Substitution.add v (fresh()) s) vars Substitution.empty in substitute_in_clause s c (* let c = (rule (func "p" [var "X"; var "Y"; const "a"]) [func "q" [var "X"; const "b"; const "a"]]) let _ = print_endline (string_of_clause c) let _ = print_endline (string_of_clause (freshen c)) *) exception Not_unifiable let unify t1 t2 = raise (Failure "Problem 4 Not implemented") (* Problem 5 *) let nondet_query program goal = raise (Failure "Problem 5 Not implemented") (* Problem Bonus *) let det_query program goal = raise (Failure "Problem Bonus Not implemented")
main.ml
open Final let test_final_1_1 ctxt = assert (occurs_check (var "X") (var "X")) let test_final_1_2 ctxt = assert (not (occurs_check (var "X") (var "Y"))) let test_final_1_3 ctxt = assert (occurs_check (var "X") (func "f" [var "X"])) let test_final_1_4 ctxt = assert (occurs_check (var "E") (func "cons" [const "a"; const "b"; var "E"])) let test_final_2_1 ctxt = assert (VarSet.equal (variables_of_term (func "f" [var "X"; var "Y"; const "a"])) (VarSet.of_list [var "X"; var "Y"])) let test_final_2_2 ctxt = assert (VarSet.equal (variables_of_term (func "p" [var "X"; var "Y"; const "a"])) (VarSet.of_list [var "X"; var "Y"])) let test_final_2_3 ctxt = assert (VarSet.equal (variables_of_clause (fact (func "p" [var "X"; var "Y"; const "a"]))) (VarSet.of_list [var "X"; var "Y"])) let test_final_2_4 ctxt = assert (VarSet.equal (variables_of_clause (rule (func "p" [var "X"; var "Y"; const "a"]) [func "q" [const "a"; const "b"; const "a"]])) (VarSet.of_list [var "X"; var "Y"])) let s = Substitution.add (var "Y") (const "0") (Substitution.add (var "X") (var "Y") Substitution.empty) let test_final_3_1 ctxt = assert (substitute_in_term s (func "f" [var "X"; var "Y"; const "a"]) = func "f" [var "Y"; const "0"; const "a"]) let test_final_3_2 ctxt = assert (substitute_in_term s (func "p" [var "X"; var "Y"; const "a"]) = func "p" [var "Y"; const "0"; const "a"]) let test_final_3_3 ctxt = assert (substitute_in_clause s (fact (func "p" [var "X"; var "Y"; const "a"])) = (fact (func "p" [var "Y"; const "0"; const "a"]))) let test_final_3_4 ctxt = assert (substitute_in_clause s (rule (func "p" [var "X"; var "Y"; const "a"]) [func "q" [const "a"; const "b"; const "a"]]) = (rule (func "p" [var "Y"; const "0"; const "a"]) [func "q" [const "a"; const "b"; const "a"]])) let test_final_4_1 ctxt = assert ((unify (var "X") (var "Y")) = Substitution.singleton (var "Y") (var "X") || (unify (var "X") (var "Y")) = Substitution.singleton (var "X") (var "Y")) let test_final_4_2 ctxt = assert ((unify (var "Y") (var "X")) = Substitution.singleton (var "X") (var "Y") || (unify (var "Y") (var "X")) = Substitution.singleton (var "Y") (var "X")) let test_final_4_3 ctxt = assert (unify (var "Y") (var "Y") = Substitution.empty) let test_final_4_4 ctxt = assert (unify (const "0") (const "0") = Substitution.empty) let test_final_4_5 ctxt = assert (unify (const "0") (var "Y") = Substitution.singleton (var "Y") (const "0")) let test_final_4_6 ctxt = assert ( match unify (const "0") (const "1") with | _ -> false | exception Not_unifiable -> true) let test_final_4_7 ctxt = assert ( match unify (func "f" [const "0"]) (func "g" [const "1"]) with | _ -> false | exception Not_unifiable -> true) let test_final_4_8 ctxt = assert (unify (func "f" [var "X"]) (func "f" [var "Y"]) = Substitution.singleton (var "X") (var "Y") || unify (func "f" [var "X"]) (func "f" [var "Y"]) = Substitution.singleton (var "Y") (var "X")) let s9 = Substitution.add (var "Z") (const "a") (Substitution.add (var "Y") (const "a") (Substitution.add (var "X") (const "a") Substitution.empty)) let test_final_4_9 ctxt = let t1 = Function("f", [Variable "X"; Variable "Y"; Variable "Y"]) in let t2 = Function("f", [Variable "Y"; Variable "Z"; Constant "a"]) in let u = unify t1 t2 in assert (Substitution.equal (=) u s9) (* Test on a simple program *) let psimple = [fact @@ func "f" [const "a"; const "b"]] let test_final_5_1 ctxt = let _ = print_endline "Testing the non-deterministic abstract interpreter" in let _ = print_endline ("Program:\n" ^ (string_of_program psimple)) in let g = [func "f" [const "a"; const "b"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query psimple g in assert (g' = [func "f" [const "a"; const "b"]]); print_endline ("Solution:\n" ^ (string_of_goal g')) let test_final_5_2 ctxt = let g = [func "f" [var "X"; const "b"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query psimple g in assert (g' = [func "f" [const "a"; const "b"]]); print_endline ("Solution:\n" ^ (string_of_goal g')) let test_final_5_3 ctxt = let g = [func "f" [var "X"; var "Y"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query psimple g in assert (g' = [func "f" [const "a"; const "b"]]); print_endline ("Solution:\n" ^ (string_of_goal g') ^ "\n") (* Test on the House Stark program *) let ancestor x y = func "ancestor" [x;y] let father x y = func "father" [x;y] let father_consts x y = father (Constant x) (Constant y) let f1 = Fact (father_consts "rickard" "ned") let f2 = Fact (father_consts "ned" "robb") let r1 = Rule (ancestor (var "X") (var "Y"), [father (var "X") (var "Y")]) let r2 = Rule (ancestor (var "X") (var "Y"), [father (var "X") (var "Z"); ancestor (var "Z") (var "Y")]) let pstark = [f1;f2;r1;r2] let test_final_5_4 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pstark)) in let g = [ancestor (const "rickard") (const "ned")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pstark g in print_endline ("Solution:\n" ^ string_of_goal g'); assert (g' = [ancestor (const "rickard") (const "ned")]) let test_final_5_5 ctxt = let g = [ancestor (const "rickard") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pstark g in print_endline ("Solution:\n" ^ (string_of_goal g')); assert (g' = [ancestor (const "rickard") (const "robb")]) let test_final_5_6 ctxt = let g = [ancestor (var "X") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pstark g in print_endline ("Solution:\n" ^ (string_of_goal g') ^ "\n"); assert (g' = [ancestor (const "ned") (const "robb")] || g' = [ancestor (const "rickard") (const "robb")]) (* Test on the list append program *) let nil = const "nil" let cons h t = func "cons" [h;t] let append x y z = func "append" [x;y;z] let c1 = fact @@ append nil (var "Q") (var "Q") let c2 = rule (append (cons (var "H") (var "P")) (var "Q") (cons (var "H") (var "R"))) [append (var "P") (var "Q") (var "R")] let pappend = [c1;c2] let test_final_5_7 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pappend)) in let g = [append (var "X") (var "Y") (cons (const "1") (cons (const "2") (cons (const "3") nil)))] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pappend g in print_endline ("Solution:\n" ^ (string_of_goal g') ^ "\n"); assert ( g' = [append nil (cons (const "1") (cons (const "2") (cons (const "3") nil))) (cons (const "1") (cons (const "2") (cons (const "3") nil)))] || g' = [append (cons (const "1") nil) (cons (const "2") (cons (const "3") nil)) (cons (const "1") (cons (const "2") (cons (const "3") nil)))] || g' = [append (cons (const "1") (cons (const "2") nil)) (cons (const "3") nil) (cons (const "1") (cons (const "2") (cons (const "3") nil)))] || g' = [append (cons (const "1") (cons (const "2") (cons (const "3") nil))) nil (cons (const "1") (cons (const "2") (cons (const "3") nil)))] ) (* Test on the simple program *) let test_final_bonus_1 ctxt = let _ = print_endline "Testing the deterministic interpreter" in let _ = print_endline ("Program:\n" ^ (string_of_program psimple)) in (* Tests query failure *) let g = [func "f" [const "a"; const "c"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in assert (det_query psimple g = []); print_endline ("Solution:\n" ^ "Empty solution\n") (* Test on the Stark House program *) let test_final_bonus_2 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pstark)) in (* Tests backtracking *) let g = [ancestor (const "rickard") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = match det_query pstark g with [v] -> v | _ -> failwith "error" in print_endline ("Solution:\n" ^ (string_of_goal g')); assert (g' = g) let test_final_bonus_3 ctxt = (* Tests choice points *) let g = [ancestor (var "X") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g1,g2 = match det_query pstark g with [v1;v2] -> v1,v2 | _ -> failwith "error" in print_endline ("Solution:\n" ^ (string_of_goal g1)); print_endline ("Solution:\n" ^ (string_of_goal g2) ^ "\n"); assert (g1 = [ancestor (const "ned") (const "robb")]); assert (g2 = [ancestor (const "rickard") (const "robb")]) (* Test on the list append program *) let test_final_bonus_4 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pappend)) in (* Tests choice points *) let g = [append (var "X") (var "Y") (cons (const "1") (cons (const "2") (cons (const "3") nil)))] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = det_query pappend g in assert (List.length g' = 4); List.iter (fun g -> print_endline ("Solution:\n" ^ (string_of_goal g))) g' let _ = test_final_1_1 (); test_final_1_2 (); test_final_1_3 (); test_final_1_4 (); test_final_2_1 (); test_final_2_2 (); test_final_2_3 (); test_final_2_4 (); test_final_3_1 (); test_final_3_2 (); test_final_3_3 (); test_final_3_4 (); test_final_4_1 (); test_final_4_2 (); test_final_4_3 (); test_final_4_4 (); test_final_4_5 (); test_final_4_6 (); test_final_4_7 (); test_final_4_8 (); test_final_4_9 (); test_final_5_1 (); test_final_5_2 (); test_final_5_3 (); test_final_5_4 (); test_final_5_5 (); test_final_5_6 (); test_final_5_7 () (* ; test_final_bonus_1 (); test_final_bonus_2 (); test_final_bonus_3 (); test_final_bonus_4 () *) let _ = Printf.printf "All tests passed.\n"
testUtils.ml
open OUnit2 let assert_true x = assert_equal true x;; let assert_false x = assert_equal false x;;
dune_1
(tests (names public) (libraries cs314 oUnit qcheck))
public.ml
open OUnit2 open Cs314.Final open TestUtils let test_final_1_1 ctxt = assert_equal true @@ (occurs_check (var "X") (var "X")) let test_final_1_2 ctxt = assert_equal true @@ (not (occurs_check (var "X") (var "Y"))) let test_final_1_3 ctxt = assert_equal true @@ (occurs_check (var "X") (func "f" [var "X"])) let test_final_1_4 ctxt = assert_equal true @@ (occurs_check (var "E") (func "cons" [const "a"; const "b"; var "E"])) let test_final_2_1 ctxt = assert_equal true @@ (VarSet.equal (variables_of_term (func "f" [var "X"; var "Y"; const "a"])) (VarSet.of_list [var "X"; var "Y"])) let test_final_2_2 ctxt = assert_equal true @@ (VarSet.equal (variables_of_term (func "p" [var "X"; var "Y"; const "a"])) (VarSet.of_list [var "X"; var "Y"])) let test_final_2_3 ctxt = assert_equal true @@ (VarSet.equal (variables_of_clause (fact (func "p" [var "X"; var "Y"; const "a"]))) (VarSet.of_list [var "X"; var "Y"])) let test_final_2_4 ctxt = assert_equal true @@ (VarSet.equal (variables_of_clause (rule (func "p" [var "X"; var "Y"; const "a"]) [func "q" [const "a"; const "b"; const "a"]])) (VarSet.of_list [var "X"; var "Y"])) let s = Substitution.add (var "Y") (const "0") (Substitution.add (var "X") (var "Y") Substitution.empty) let test_final_3_1 ctxt = assert_equal true @@ (substitute_in_term s (func "f" [var "X"; var "Y"; const "a"]) = func "f" [var "Y"; const "0"; const "a"]) let test_final_3_2 ctxt = assert_equal true @@ (substitute_in_term s (func "p" [var "X"; var "Y"; const "a"]) = func "p" [var "Y"; const "0"; const "a"]) let test_final_3_3 ctxt = assert_equal true @@ (substitute_in_clause s (fact (func "p" [var "X"; var "Y"; const "a"])) = (fact (func "p" [var "Y"; const "0"; const "a"]))) let test_final_3_4 ctxt = assert_equal true @@ (substitute_in_clause s (rule (func "p" [var "X"; var "Y"; const "a"]) [func "q" [const "a"; const "b"; const "a"]]) = (rule (func "p" [var "Y"; const "0"; const "a"]) [func "q" [const "a"; const "b"; const "a"]])) let test_final_4_1 ctxt = assert_equal true @@ ((unify (var "X") (var "Y")) = Substitution.singleton (var "Y") (var "X") || (unify (var "X") (var "Y")) = Substitution.singleton (var "X") (var "Y")) let test_final_4_2 ctxt = assert_equal true @@ ((unify (var "Y") (var "X")) = Substitution.singleton (var "X") (var "Y") || (unify (var "Y") (var "X")) = Substitution.singleton (var "Y") (var "X")) let test_final_4_3 ctxt = assert_equal true @@ (unify (var "Y") (var "Y") = Substitution.empty) let test_final_4_4 ctxt = assert_equal true @@ (unify (const "0") (const "0") = Substitution.empty) let test_final_4_5 ctxt = assert_equal true @@ (unify (const "0") (var "Y") = Substitution.singleton (var "Y") (const "0")) let test_final_4_6 ctxt = assert_equal true @@ ( match unify (const "0") (const "1") with | _ -> false | exception Not_unifiable -> true) let test_final_4_7 ctxt = assert_equal true @@ ( match unify (func "f" [const "0"]) (func "g" [const "1"]) with | _ -> false | exception Not_unifiable -> true) let test_final_4_8 ctxt = assert_equal true @@ (unify (func "f" [var "X"]) (func "f" [var "Y"]) = Substitution.singleton (var "X") (var "Y") || unify (func "f" [var "X"]) (func "f" [var "Y"]) = Substitution.singleton (var "Y") (var "X")) let s9 = Substitution.add (var "Z") (const "a") (Substitution.add (var "Y") (const "a") (Substitution.add (var "X") (const "a") Substitution.empty)) let test_final_4_9 ctxt = let t1 = Function("f", [Variable "X"; Variable "Y"; Variable "Y"]) in let t2 = Function("f", [Variable "Y"; Variable "Z"; Constant "a"]) in let u = unify t1 t2 in assert_equal true @@ (Substitution.equal (=) u s9) (* Test on a simple program *) let psimple = [fact @@ func "f" [const "a"; const "b"]] let test_final_5_1 ctxt = let _ = print_endline "Testing the non-deterministic abstract interpreter" in let _ = print_endline ("Program:\n" ^ (string_of_program psimple)) in let g = [func "f" [const "a"; const "b"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query psimple g in assert_equal true @@ (g' = [func "f" [const "a"; const "b"]]); print_endline ("Solution:\n" ^ (string_of_goal g')) let test_final_5_2 ctxt = let g = [func "f" [var "X"; const "b"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query psimple g in assert_equal true @@ (g' = [func "f" [const "a"; const "b"]]); print_endline ("Solution:\n" ^ (string_of_goal g')) let test_final_5_3 ctxt = let g = [func "f" [var "X"; var "Y"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query psimple g in assert_equal true @@ (g' = [func "f" [const "a"; const "b"]]); print_endline ("Solution:\n" ^ (string_of_goal g') ^ "\n") (* Test on the House Stark program *) let ancestor x y = func "ancestor" [x;y] let father x y = func "father" [x;y] let father_consts x y = father (Constant x) (Constant y) let f1 = Fact (father_consts "rickard" "ned") let f2 = Fact (father_consts "ned" "robb") let r1 = Rule (ancestor (var "X") (var "Y"), [father (var "X") (var "Y")]) let r2 = Rule (ancestor (var "X") (var "Y"), [father (var "X") (var "Z"); ancestor (var "Z") (var "Y")]) let pstark = [f1;f2;r1;r2] let test_final_5_4 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pstark)) in let g = [ancestor (const "rickard") (const "ned")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pstark g in print_endline ("Solution:\n" ^ string_of_goal g'); assert_equal true @@ (g' = [ancestor (const "rickard") (const "ned")]) let test_final_5_5 ctxt = let g = [ancestor (const "rickard") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pstark g in print_endline ("Solution:\n" ^ (string_of_goal g')); assert_equal true @@ (g' = [ancestor (const "rickard") (const "robb")]) let test_final_5_6 ctxt = let g = [ancestor (var "X") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pstark g in print_endline ("Solution:\n" ^ (string_of_goal g') ^ "\n"); assert_equal true @@ (g' = [ancestor (const "ned") (const "robb")] || g' = [ancestor (const "rickard") (const "robb")]) (* Test on the list append program *) let nil = const "nil" let cons h t = func "cons" [h;t] let append x y z = func "append" [x;y;z] let c1 = fact @@ append nil (var "Q") (var "Q") let c2 = rule (append (cons (var "H") (var "P")) (var "Q") (cons (var "H") (var "R"))) [append (var "P") (var "Q") (var "R")] let pappend = [c1;c2] let test_final_5_7 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pappend)) in let g = [append (var "X") (var "Y") (cons (const "1") (cons (const "2") (cons (const "3") nil)))] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pappend g in print_endline ("Solution:\n" ^ (string_of_goal g') ^ "\n"); assert_equal true @@ ( g' = [append nil (cons (const "1") (cons (const "2") (cons (const "3") nil))) (cons (const "1") (cons (const "2") (cons (const "3") nil)))] || g' = [append (cons (const "1") nil) (cons (const "2") (cons (const "3") nil)) (cons (const "1") (cons (const "2") (cons (const "3") nil)))] || g' = [append (cons (const "1") (cons (const "2") nil)) (cons (const "3") nil) (cons (const "1") (cons (const "2") (cons (const "3") nil)))] || g' = [append (cons (const "1") (cons (const "2") (cons (const "3") nil))) nil (cons (const "1") (cons (const "2") (cons (const "3") nil)))] ) (* Test on the simple program *) let test_final_bonus_1 ctxt = let _ = print_endline "Testing the deterministic interpreter" in let _ = print_endline ("Program:\n" ^ (string_of_program psimple)) in (* Tests query failure *) let g = [func "f" [const "a"; const "c"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in assert_equal true @@ (det_query psimple g = []); print_endline ("Solution:\n" ^ "Empty solution\n") (* Test on the Stark House program *) let test_final_bonus_2 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pstark)) in (* Tests backtracking *) let g = [ancestor (const "rickard") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = match det_query pstark g with [v] -> v | _ -> failwith "error" in print_endline ("Solution:\n" ^ (string_of_goal g')); assert_equal true @@ (g' = g) let test_final_bonus_3 ctxt = (* Tests choice points *) let g = [ancestor (var "X") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g1,g2 = match det_query pstark g with [v1;v2] -> v1,v2 | _ -> failwith "error" in print_endline ("Solution:\n" ^ (string_of_goal g1)); print_endline ("Solution:\n" ^ (string_of_goal g2) ^ "\n"); assert_equal true @@ (g1 = [ancestor (const "ned") (const "robb")]); assert_equal true @@ (g2 = [ancestor (const "rickard") (const "robb")]) (* Test on the list append program *) let test_final_bonus_4 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pappend)) in (* Tests choice points *) let g = [append (var "X") (var "Y") (cons (const "1") (cons (const "2") (cons (const "3") nil)))] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = det_query pappend g in assert_equal true @@ (List.length g' = 4); List.iter (fun g -> print_endline ("Solution:\n" ^ (string_of_goal g))) g' let suite = "public" >::: [ "test_final_1_1">:: test_final_1_1; "test_final_1_2">:: test_final_1_2; "test_final_1_3">:: test_final_1_3; "test_final_1_4">:: test_final_1_4; "test_final_2_1">:: test_final_2_1; "test_final_2_2">:: test_final_2_2; "test_final_2_3">:: test_final_2_3; "test_final_2_4">:: test_final_2_4; "test_final_3_1">:: test_final_3_1; "test_final_3_2">:: test_final_3_2; "test_final_3_3">:: test_final_3_3; "test_final_3_4">:: test_final_3_4; "test_final_4_1">:: test_final_4_1; "test_final_4_2">:: test_final_4_2; "test_final_4_3">:: test_final_4_3; "test_final_4_4">:: test_final_4_4; "test_final_4_5">:: test_final_4_5; "test_final_4_6">:: test_final_4_6; "test_final_4_7">:: test_final_4_7; "test_final_4_8">:: test_final_4_8; "test_final_4_9">:: test_final_4_9; "test_final_5_1">:: test_final_5_1; "test_final_5_2">:: test_final_5_2; "test_final_5_3">:: test_final_5_3; "test_final_5_4">:: test_final_5_4; "test_final_5_5">:: test_final_5_5; "test_final_5_6">:: test_final_5_6; "test_final_5_7">:: test_final_5_7; (*"test_final_bonus_1">:: test_final_bonus_1; "test_final_bonus_2">:: test_final_bonus_2; "test_final_bonus_3">:: test_final_bonus_3; "test_final_bonus_4">:: test_final_bonus_4;*) ] let _ = run_test_tt_main suite
