test seminarska sml

tests.sml

(*TESTI*)
val display_test_1 = display(AND(NEG(VAR("p")),OR(VAR("q"),VAR("r"))));
val display_resu_1 = "~ p & (q | r)";
val display_test_2 = display(AND(VAR("p"), AND(VAR("q"),VAR("r"))));
val display_resu_2 = "p & q & r";
val display_test_3 = display(AND(VAR("p"), NEG((AND(VAR("q"),VAR("r"))))));
val display_resu_3 = "p & ~ (q & r)";
val display_test_4 = display(NEG(((OR(VAR("q"),VAR("r")))))); 
val display_resu_4 = "~ (q | r)";
val nnf_test_1 = nnf(NEG(AND(OR(NEG(VAR("p")),VAR("q")),VAR("r"))));
val nnf_resu_1 = OR (AND (VAR "p",NEG (VAR "q")),NEG (VAR "r"));
val cnf_test_1 = cnf(OR(NEG(VAR("p")),AND(VAR("q"),VAR("r"))));
val cnf_resu_1 = [[NEG (VAR "p"),VAR "q"],[NEG (VAR "p"),VAR "r"]];
val cnf_test_2 = cnf(OR(AND(VAR("p"),VAR("q")),OR(NEG(VAR("p")),NEG(VAR("q")))));
val cnf_resu_2 = [[VAR "p",NEG (VAR "p"),NEG (VAR "q")], [VAR "q",NEG (VAR "p"),NEG (VAR "q")]];
val cnf_test_3 = cnf(OR(VAR("p"),NEG(VAR("p"))));
val cnf_resu_3 = [[VAR "p",NEG (VAR "p")]];
val cnf_test_4 = cnf(OR(OR(VAR("p"),OR(VAR("q"),NEG(VAR("r")))),NEG(VAR("s"))));
val cnf_resu_4 = [[VAR "p",VAR "q",NEG (VAR "r"),NEG (VAR "s")]];
val cnf_test_5 = cnf(OR(AND(VAR("p"),VAR("q")),AND(NEG(VAR("p")),NEG(VAR("q")))));
val cnf_resu_5 = [[VAR "p",NEG (VAR "p")], [VAR "p",NEG (VAR "q")], [VAR "q",NEG (VAR "p")], [VAR "q",NEG (VAR "q")]];
val cnf_test_6 = cnf(OR(AND(VAR("p"),VAR("q")),AND(AND(NEG(VAR("a")),NEG(VAR("b"))),NEG(VAR("q")))));
val cnf_resu_6 = [[VAR "p",NEG (VAR "a")], [VAR "p",NEG (VAR "b")], [VAR "p",NEG (VAR "q")], [VAR "q",NEG (VAR "a")], [VAR "q",NEG (VAR "b")], [VAR "q",NEG (VAR "q")]];
val cnf_test_7 = cnf(AND(VAR("p"),NEG(VAR("p")))); 
val cnf_resu_7 = [[VAR ("p")], [NEG (VAR "p")]];
val taut_test_1 = isTaut(OR(VAR("p"),NEG(VAR("p"))));
val taut_resu_1 = true;
val taut_test_2 = isTaut(OR(AND(VAR("p"),VAR("q")),OR(NEG(VAR("p")),NEG(VAR("q")))));
val taut_resu_2 = true;
val taut_test_3 = isTaut(OR(VAR("p"),NEG(VAR("q")))); 
val taut_resu_3 = false;
val taut_test_4 = isTaut(OR(AND(VAR("p"),VAR("q")),OR(OR(NEG(VAR("p")),NEG(VAR("q"))),NEG(VAR("q")))));
val taut_resu_4 = true;
val unsat_test_1 = isUnsat(OR(VAR("p"),NEG(VAR("p")))); (*  [[VAR "p",NEG (VAR "p")]] *)
val unsat_resu_1 = false;
val unsat_test_2 = isUnsat(AND(VAR("p"),NEG(VAR("p")))); (* [[VAR "p"],[NEG (VAR "p")]] *)
val unsat_resu_2 = true;
val unsat_test_3 = isUnsat(AND(VAR("p"),NEG(VAR("p")))); (* [[VAR "p",VAR "q"],[NEG (VAR "q"),NEG (VAR "p")]] *)
val unsat_resu_3 = true;
val check_test_1 = check (OR(VAR("p"),VAR("q"))) [VAR("q")];
val check_resu_1 = true;
val check_test_2 = check (AND(VAR("p"),VAR("q"))) [VAR("p")];
val check_resu_2 = false;
val check_test_3 = check (AND(VAR("p"),VAR("q"))) [OR(NEG(VAR("r")),VAR("p")),VAR("r"),VAR("q")];
val check_resu_3 = true;
val check_test_4 = check (AND(VAR("p"),VAR("q"))) [VAR("r"),VAR("q"),OR(NEG(VAR("r")),VAR("p"))];
val check_resu_4 = true;
val check_test_5 = check (AND(VAR("p"),VAR("q"))) [AND(VAR("r"),VAR("p")),VAR("r"),VAR("q")];
val check_resu_5 = true;
val check_test_6 = check (AND(VAR("p"),VAR("q"))) [AND(VAR("r"),NEG(VAR("p"))),VAR("r"),VAR("q")];
val check_resu_6 = false;
val check_test_7 = check (AND(VAR("p"),VAR("q"))) [AND(VAR("r"),AND(VAR("q"),VAR("p"))),VAR("r"),VAR("q")];
val check_resu_7 = true;
val check_test_8 = check (AND(VAR("p"),VAR("q"))) [AND(AND(VAR("r"),VAR("q")),VAR("p")),VAR("r"),VAR("q")];
val check_resu_8 = true;
val check_test_9_1 = check (OR(VAR("p"),VAR("q"))) [AND(VAR("p"), VAR("q"))];
val check_resu_9_1 = true;
val check_test_9_2 = check (OR(VAR("p"),VAR("q"))) [AND(VAR("p"), NEG(VAR("q")))];
val check_resu_9_2 = true;
val check_test_9_3 = check (OR(VAR("p"),VAR("q"))) [AND(NEG(VAR("p")), VAR("q"))];
val check_resu_9_3 = true;
val check_test_9_4 = check (OR(VAR("p"),VAR("q"))) [AND(NEG(VAR("p")), NEG(VAR("q")))];
val check_resu_9_4 = false;
val sat_test_1 = sat(OR(VAR("p"),VAR("q")));
val sat_resu_1 = [[("p",false),("q",true)],[("p",true),("q",false)],[("p",true),("q",true)]];
val sat_test_2 = sat(AND(VAR("p"),VAR("q")));
val sat_resu_2 = [[("p",true),("q",true)]];
val sat_test_3 = sat(OR(VAR("p"),OR(VAR("p"),VAR("p"))));
val sat_resu_3 = [[("p",true)]];
val sat_test_4 = sat(AND(VAR("p"),NEG(VAR("p"))));
val sat_resu_4 = [];


fun evalUser (x,y) =
	case (x,y) of
	(false,false) => true
	| (false,true) => true
	| (true,false) => false
	| (true,true) => true

fun evalUser2 (x,y) =
case (x,y) of
(false,false) => true
| (false,true) => true
| (true,false) => true
| (true,true) => true

fun evalUser3 (x,y) =
case (x,y) of
(false,false) => false
| (false,true) => true
| (true,false) => true
| (true,true) => false


val satEx_test_1 = satEx (AND_EX(VAR_EX("p"),USER_EX(VAR_EX("p"), VAR_EX("q")))) evalUser;
val satEx_resu_1 = [[("p",true),("q",true)]];
val satEx_test_2 = satEx (AND_EX(VAR_EX("p"),NEG_EX(USER_EX(VAR_EX("p"), VAR_EX("q"))))) evalUser;
val satEx_resu_2 = [[("p",true),("q",false)]];
val satEx_test_3 = satEx (AND_EX(OR_EX(VAR_EX("p"),NEG_EX(USER_EX(VAR_EX("p"), VAR_EX("q")))),USER_EX(VAR_EX("q"), VAR_EX("r")))) evalUser;
val satEx_resu_3 = [[("p",true),("q",true),("r",true)],[("p",true),("q",false),("r",true)],
   					[("p",true),("q",false),("r",false)]]

val satEx_test_4 = satEx (AND_EX(VAR_EX("p"),NEG_EX(USER_EX(VAR_EX("p"), VAR_EX("q"))))) evalUser2;
val satEx_resu_4 = [];
val satEx_test_5 = satEx (OR_EX(VAR_EX("p"),USER_EX(VAR_EX("p"), VAR_EX("q")))) evalUser2;
val satEx_resu_5 = [[("p",true),("q",true)],[("p",true),("q",false)],[("p",false),("q",true)],
   [("p",false),("q",false)]]
val satEx_test_6 = satEx (USER_EX(OR_EX(VAR_EX("p"),USER_EX(VAR_EX("p"), VAR_EX("q"))),AND_EX(VAR_EX("q"),VAR_EX("z")))) evalUser3;
val satEx_resu_6 = [[("p",true),("q",true),("z",false)],[("p",true),("q",false),("z",true)],
   					[("p",true),("q",false),("z",false)],[("p",false),("q",true),("z",false)]]
val satEx_test_7 = satEx (USER_EX(NEG_EX(USER_EX(VAR_EX("p"),USER_EX(VAR_EX("p"), VAR_EX("q")))),AND_EX(NEG_EX(VAR_EX("q")),VAR_EX("z")))) evalUser3;
val resu_7 = [[("p",true),("q",false),("z",false)],[("p",false),("q",false),("z",false)]]

val isUnsat_test_4 = isUnsat(OR(AND(VAR("p"),VAR("q")),AND(VAR("r"),AND(VAR("p"),AND(NEG(VAR("r")),NEG(VAR("q")))))    )    );
val isUnsat_resu_4 = false

val isTaut_test_5 = isTaut(OR(AND(VAR("p"),VAR("q")),AND(VAR("r"),AND(VAR("p"),AND(NEG(VAR("r")),NEG(VAR("q")))))));
val isTaut_resu_5 = false

NAVODILA: tole daš na konc fajla pa ko poženeš pogledaš če je isto