Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/benchmarks/programs/boyer/boyer.sml
ViewVC logotype

Annotation of /sml/trunk/benchmarks/programs/boyer/boyer.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 193 - (view) (download)

1 : monnier 193 (* boyer.sml:
2 :     *
3 :     * Tautology checker
4 :     *)
5 :    
6 :     signature BOYER =
7 :     sig
8 :     include TERMS
9 :     val tautp: term -> bool
10 :     end
11 :    
12 :     structure Boyer: BOYER =
13 :     struct
14 :    
15 :     open Terms
16 :    
17 :     fun mem x [] = false
18 :     | mem x (y::L) = x=y orelse mem x L
19 :    
20 :     fun truep (x, lst) =
21 :     case x of
22 :     Prop(head, _) =>
23 :     headname head = "true" orelse mem x lst
24 :     | _ =>
25 :     mem x lst
26 :    
27 :     and falsep (x, lst) =
28 :     case x of
29 :     Prop(head, _) =>
30 :     headname head = "false" orelse mem x lst
31 :     | _ =>
32 :     mem x lst
33 :    
34 :     fun tautologyp (x, true_lst, false_lst) =
35 :     if truep (x, true_lst) then true else
36 :     if falsep (x, false_lst) then false else
37 :     (case x of
38 :     Var _ => false
39 :     | Prop (head,[test, yes, no]) =>
40 :     if headname head = "if" then
41 :     if truep (test, true_lst) then
42 :     tautologyp (yes, true_lst, false_lst)
43 :     else if falsep (test, false_lst) then
44 :     tautologyp (no, true_lst, false_lst)
45 :     else tautologyp (yes, test::true_lst, false_lst) andalso
46 :     tautologyp (no, true_lst, test::false_lst)
47 :     else
48 :     false)
49 :    
50 :     fun tautp x = tautologyp(rewrite x, [], []);
51 :    
52 :     end; (* Boyer *)
53 :    
54 :     (* the benchmark *)
55 :     structure Main : BMARK =
56 :     struct
57 :    
58 :     open Terms;
59 :     open Boyer;
60 :    
61 :     val subst =
62 :     [Bind(23,
63 :     Prop
64 :     (get "f",
65 :     [Prop
66 :     (get "plus",
67 :     [Prop (get "plus",[Var 0, Var 1]),
68 :     Prop (get "plus",[Var 2, Prop (get "zero",[])])])])),
69 :     Bind(24,
70 :     Prop
71 :     (get "f",
72 :     [Prop
73 :     (get "times",
74 :     [Prop (get "times",[Var 0, Var 1]),
75 :     Prop (get "plus",[Var 2, Var 3])])])),
76 :     Bind(25,
77 :     Prop
78 :     (get "f",
79 :     [Prop
80 :     (get "reverse",
81 :     [Prop
82 :     (get "append",
83 :     [Prop (get "append",[Var 0, Var 1]),
84 :     Prop (get "nil",[])])])])),
85 :     Bind(20,
86 :     Prop
87 :     (get "equal",
88 :     [Prop (get "plus",[Var 0, Var 1]),
89 :     Prop (get "difference",[Var 23, Var 24])])),
90 :     Bind(22,
91 :     Prop
92 :     (get "lt",
93 :     [Prop (get "remainder",[Var 0, Var 1]),
94 :     Prop (get "member",[Var 0, Prop (get "length",[Var 1])])]))]
95 :    
96 :     val term =
97 :     Prop
98 :     (get "implies",
99 :     [Prop
100 :     (get "and",
101 :     [Prop (get "implies",[Var 23, Var 24]),
102 :     Prop
103 :     (get "and",
104 :     [Prop (get "implies",[Var 24, Var 25]),
105 :     Prop
106 :     (get "and",
107 :     [Prop (get "implies",[Var 25, Var 20]),
108 :     Prop (get "implies",[Var 20, Var 22])])])]),
109 :     Prop (get "implies",[Var 23, Var 22])])
110 :    
111 :     fun testit outstrm = if tautp (apply_subst subst term)
112 :     then TextIO.output (outstrm, "Proved!\n")
113 :     else TextIO.output (outstrm, "Cannot prove!\n")
114 :    
115 :     fun doit () = (tautp (apply_subst subst term); ())
116 :    
117 :     end; (* Main *)

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0