• API
• FAQ
• Tools
• Trends
• Archive
daily pastebin goal
23%
SHARE
TWEET

# CNF calculator

a guest Feb 13th, 2012 430 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. datatype logicexpr = Var of string
2.                      | Neg of logicexpr
3.                      | And of logicexpr * logicexpr
4.                      | Or of logicexpr * logicexpr;
5. datatype logiccontext = CNeg | CAnd | COr;
6. datatype logiclex = LVar of string | LLeft | LRight | LNeg | LAnd | LOr;
7.
8. fun distributeLeft(X, And(e,f)) = And(distributeLeft(X,e),distributeLeft(X,f))
9. | distributeLeft(X, Y) = Or(X, Y);
10.
11. fun distributeOr(And(e,f), Y) = And(distributeOr(e,Y),distributeOr(f,Y))
12. | distributeOr(X, Y) = distributeLeft(X, Y);
13.
14. fun makeCNF(Var x) = Var x
15. | makeCNF(Neg(Var x)) = Neg(Var x)
16. | makeCNF(Neg(Neg e)) = makeCNF e
17. | makeCNF(Neg(And(e,f))) = makeCNF(Or(Neg e, Neg f))
18. | makeCNF(Neg(Or(e,f))) = makeCNF(And(Neg e, Neg f))
19. | makeCNF(And(e,f)) = And(makeCNF e, makeCNF f)
20. | makeCNF(Or(e,f)) = distributeOr(makeCNF e, makeCNF f);
21.
22. fun displayLogic(E) = let
23.    fun dispLogic(Var x,_) = x
24.    | dispLogic(Neg(X),_) = "!" ^ dispLogic(X,CNeg)
25.    | dispLogic(And(X,Y),CNeg) = "(" ^ dispLogic(X,CAnd) ^ "&" ^ dispLogic(Y,CAnd) ^ ")"
26.    | dispLogic(And(X,Y),_) = dispLogic(X,CAnd) ^ "&" ^ dispLogic(Y,CAnd)
27.    | dispLogic(Or(X,Y),COr) = dispLogic(X,COr) ^ "|" ^ dispLogic(Y,COr)
28.    | dispLogic(Or(X,Y),_) = "(" ^ dispLogic(X,COr) ^ "|" ^ dispLogic(Y,COr) ^ ")";
29. in
30.    dispLogic(E,COr)
31. end;
32.
33. fun parseLogic(s) = let
34.    fun collect a [] = (LVar (implode a),[])
35.    | collect a (c::r) = if Char.isAlpha c then collect (a@[c]) r else (LVar (implode a),c::r);
36.    fun lex [] = []
37.    | lex (#"("::r) = LLeft :: lex r
38.    | lex (#")"::r) = LRight :: lex r
39.    | lex (#"!"::r) = LNeg :: lex r
40.    | lex (#"&"::r) = LAnd :: lex r
41.    | lex (#"|"::r) = LOr :: lex r
42.    | lex (c::r) = if Char.isAlpha c then let val (v,s) = collect [] (c::r); in v :: lex s end
43.       else lex r;
44.    fun parseExpr e = let val (l,u) = parseAnd e; in
45.       if u = [] then (l,[])
46.       else if hd u = LOr then let val (r,v) = parseExpr(tl u); in (Or(l,r),v) end
47.       else (l,u)
48.    end
49.    and parseAnd e = let val (l,u) = parseNot e; in
50.       if u = [] then (l,[])
51.       else if hd u = LAnd then let val (r,v) = parseAnd (tl u); in (And(l,r),v) end
52.       else (l,u)
53.    end
54.    and parseNot (LNeg::t) = let val (r,u) = parseNot t; in (Neg(r),u) end
55.    | parseNot s = parseTerm s
56.    and parseTerm (LVar(x)::t) = (Var(x),t)
57.    | parseTerm (LLeft::t) = let val (e,LRight::u) = parseExpr t; in (e,u) end;
58.    val (parse,leftover) = parseExpr(lex(explode s));
59. in parse end;
60.
61. fun printCNF expr = print(displayLogic(makeCNF(parseLogic(expr))) ^ "\n");
RAW Paste Data
Top