Seminarska naloga P - Testi

(* DISPLAY TESTI *)
val displayTest = AND(NEG(VAR("p")),OR(VAR("q"),VAR("r")));
val displayTest2 = AND(OR(NEG(VAR("p")), VAR "q"),OR(VAR("q"),VAR("r")));
val displayTest3 = AND(VAR("p"), AND(OR(VAR("q"),VAR("r")), OR(VAR ("n"), VAR ("y"))));
val displayTest4 = AND(VAR("p"), AND(VAR("q"),NEG (VAR("r"))));
val displayTest5 = NEG(NEG(VAR("p")));
val displayTest6 = AND(NEG(VAR("p")),OR(VAR("q"),VAR("r")));
val displayTest7 = OR(AND(NEG(VAR("p")),VAR("q")),VAR("r"));
val displayTest8 = AND(VAR("p"), AND(VAR("q"), VAR("r")));
val displayTest9 = NEG(NEG((AND(VAR("a"),NEG(OR(VAR("b"), VAR("c")))))));
val displayTest10 = AND(NEG(VAR("a")), NEG(VAR("b")));

"~ p & (q | r)" = display(displayTest);
"(~ p | q) & (q | r)" = display(displayTest2);
"p & (q | r) & (n | y)" = display(displayTest3);
"p & q & ~ r" = display(displayTest4);
"~ (~ p)" = display(displayTest5);
"~ p & (q | r)" = display(displayTest6);
"~ p & q | r" = display(displayTest7);
"p & q & r" = display(displayTest8);
"~ (~ (a & ~ (b | c)))" = display(displayTest9);
"~ a & ~ b" = display(displayTest10);

(* NNF TESTI *)
val nnfTest = nnf(NEG(AND(OR(NEG(VAR("p")),VAR("q")),VAR("r"))));
val nnfTest2 = nnf( NEG(OR(NEG(AND(NEG(VAR("a")),VAR("b"))),AND(NEG(VAR("b")),NEG(AND(VAR("a"),VAR("b")))))) );
val nnfTest3 = nnf(NEG(AND(VAR("a"), NEG(VAR("b")))));
val nnfTest4 = nnf(NEG(NEG(NEG(NEG(VAR("b"))))));
val nnfTest5 = nnf((NEG(NEG(NEG(VAR("b"))))));

OR (AND (VAR "p",NEG (VAR "q")),NEG (VAR "r")) = nnf(nnfTest);
AND (AND (NEG (VAR "a"),VAR "b"),OR (VAR "b",AND (VAR "a",VAR "b"))) = nnf(nnfTest2);
OR(NEG(VAR("a")), VAR("b")) = nnf(nnfTest3);
VAR("b") = nnf(nnfTest4);
NEG(VAR("b")) = nnf(nnfTest5);

(* CNF TEST *)
val cnfTest = OR(NEG(VAR("p")),AND(VAR("q"),VAR("r")));
val cnfTest2 = OR(OR(AND(VAR("p1"), VAR("q1")), AND(VAR("p2"), VAR("q2"))),AND(VAR("p3"), VAR("q3")));

[[NEG (VAR "p"),VAR "q"],[NEG (VAR "p"),VAR "r"]] = cnf(cnfTest);
[[VAR "p1",VAR "p2",VAR "p3"],[VAR "p1",VAR "p2",VAR "q3"],
[VAR "p1",VAR "q2",VAR "p3"],[VAR "p1",VAR "q2",VAR "q3"],
[VAR "q1",VAR "p2",VAR "p3"],[VAR "q1",VAR "p2",VAR "q3"],
[VAR "q1",VAR "q2",VAR "p3"],[VAR "q1",VAR "q2",VAR "q3"]] = cnf(cnfTest2);

(* ISTAUT TEST *)
isTaut(OR(VAR("p"),NEG(VAR("p"))));
isTaut(OR(AND(VAR("p"),VAR("q")),OR(NEG(VAR("p")),NEG(VAR("q")))));
false = isTaut(OR(VAR("p"),NEG(VAR("q"))));
false = isTaut(AND(VAR("p"), NEG(VAR("p"))));

(* ISUNSAT *)
false = isUnsat(OR(VAR("p"),NEG(VAR("p"))));
isUnsat(AND(VAR("p"),NEG(VAR("p"))));
false = isUnsat(AND(VAR("p"), VAR("p")));
isUnsat(AND(OR(VAR("p"),VAR("q")),AND(NEG(VAR("p")),NEG(VAR("q")))));

(* CHECK *)
check(OR(VAR("p"),VAR("q"))) [VAR("q")];
false = check(AND(VAR("p"),VAR("q"))) [VAR("p")];
check(AND(VAR("p"),VAR("q"))) [OR(NEG(VAR("r")),VAR("p")),VAR("r"),VAR("q")];
check(VAR("z")) [VAR("q"), VAR("p"), OR(NEG(VAR("r")), VAR("q")), AND(VAR("z"),VAR("r"))];

(* SAT *)
val satTest = sat(OR(VAR("p"),VAR("q")));
val satTest2 = sat(AND(VAR("p"),VAR("q")));
[[("p",true)]] = sat(OR(VAR("p"),OR(VAR("p"),VAR("p"))));
[[("p",true)]] = sat(VAR("p"));
[[("q",false)]] = sat(NEG(VAR("q")));
[] = sat (AND(VAR("p"), NEG(VAR("p"))));

(* SATEX *)

val testSatEx = satEx (AND_EX(VAR_EX("p"),USER_EX(VAR_EX("p"), VAR_EX("q")))) evalUser;

fun evalUser (x,y) =
    case (x,y) of
        (false,false) => true
      | (false,true) => false
      | (true,false) => false
      | (true,true) => false
      ;
[]= (satEx (USER_EX(VAR_EX("p"), NEG_EX(VAR_EX("p")))) evalUser);