1 ///////////////////////////////////////////////////////////////////////////////
3 // This example program performs simplification of propositional logic
4 // formulas using rewriting. We'll also define a parser to parses a
5 // logical formula from the input.
7 ///////////////////////////////////////////////////////////////////////////////
10 #include <AD/strings/quark.h>
11 #include <AD/automata/iolexerbuf.h>
13 ///////////////////////////////////////////////////////////////////////////////
15 // First, we define the type Wff (Well Formed Formulas) to represent
16 // our logic formulas. Identifiers (type Id) are represented as
17 // atomic strings so that equality testing can be done quickly.
19 // We also use pretty printing annotations to
20 // indicate to Prop to generate a simple print routine.
22 ///////////////////////////////////////////////////////////////////////////////
23 datatype Wff :: rewrite
26 | Var (class Quark) => _
27 | Op (class Quark, Wff, Wff) => "(" 2 " " 1 " " 3 ")"
28 | Not (Wff) => "not (" _ ")"
30 ////////////////////////////////////////////////////////////////////////////
32 // The following set of laws abbreviate commonly used logical connectives.
34 ////////////////////////////////////////////////////////////////////////////
36 inline And(a,b) = Op(#"and",a,b)
37 and inline Or(a,b) = Op(#"or",a,b)
38 and inline Implies(a,b) = Op(#"->",a, b)
39 and inline Xor(a,b) = Op(#"xor",a,b)
40 and inline Equiv(a,b) = Op(#"<->",a,b)
43 instantiate datatype Wff;
45 ///////////////////////////////////////////////////////////////////////////////
47 // Next, we define the set of symbols used for our Wff parser.
49 ///////////////////////////////////////////////////////////////////////////////
50 datatype WffToken :: lexeme =
51 "[" | "]" | "(" | ")" | "*" | "+" | "->" | "<->"
52 | "not" | "and" | "or" | "xor" | ";" | "true" | "false" | "t" | "f"
53 | ID /[a-zA-Z][a-zA-Z0-9]*/
56 ///////////////////////////////////////////////////////////////////////////////
58 // Next, we declare the interface of the parser.
60 ///////////////////////////////////////////////////////////////////////////////
61 syntax class WffParser
62 { IOLexerBuffer lexbuf;
64 int get_token(); // retrieve a token
65 void process (Wff); // process a Wff
68 ///////////////////////////////////////////////////////////////////////////////
70 // The lexer simply returns the tokens one by one; it also skip over the
71 // spaces and newlines. If any unrecognized tokens are encountered,
72 // the program will terminate.
74 ///////////////////////////////////////////////////////////////////////////////
75 int WffParser::get_token()
76 { matchscan while (lexbuf)
77 { lexeme class WffToken: { return ?lexeme; }
78 | /[ \t\n]/: // skip spaces
83 ///////////////////////////////////////////////////////////////////////////////
85 // The parser is defined below. Notice that the wffs are separated
86 // by semi-colons. We call process() to simplify each one.
88 ///////////////////////////////////////////////////////////////////////////////
92 ////////////////////////////////////////////////////////////////////////////
94 // Precedences. Note that implication associates to the right.
96 ////////////////////////////////////////////////////////////////////////////
98 left: 2 "*" "and" "xor";
104 | wff ";" { process($1); } command
105 | ? ";" command // for error recover, just skip to the next ;
108 wff Wff: wff "+" wff { $$ = Or($1,$3); }
109 | wff "*" wff { $$ = And($1,$3); }
110 | wff "->" wff { $$ = Implies($1,$3); }
111 | wff "<->" wff { $$ = Equiv($1,$3); }
112 | wff "and" wff { $$ = And($1,$3); }
113 | wff "or" wff { $$ = Or($1,$3); }
114 | wff "xor" wff { $$ = Xor($1,$3); }
115 | "not" wff { $$ = Not($2); }
116 | "(" wff ")" { $$ = $2; }
117 | "[" wff "]" { $$ = $2; }
118 | ID { $$ = Var(lexbuf.text()); }
119 | "true" { $$ = True; }
121 | "false" { $$ = False; }
122 | "f" { $$ = False; }
126 ///////////////////////////////////////////////////////////////////////////////
128 // For processing, we just transform the input formula a bit,
129 // then prints it out. The rules are by no means exhaustive.
131 ///////////////////////////////////////////////////////////////////////////////
132 void WffParser::process(Wff wff)
134 cout << "input = " << wff << '\n';
136 rewrite (wff) type (Wff) of
139 | And(False,_): False
140 | And(_,False): False
148 | Not(And(X,Y)): Or(Not(X),Not(Y))
149 | Not(Or(X,Y)): And(Not(X),Not(Y))
150 | And(And(X,Y),Z): And(X,And(Y,Z))
151 | Or(Or(X,Y),Z): Or(X,Or(Y,Z))
154 | And(X as Var a,Var b) | a == b: X
155 | Or(X as Var a,Var b) | a == b: X
156 | And(X as Var a,Y as Var b) | a > b: And(Y,X)
157 | Or(X as Var a,Y as Var b) | a > b: Or(Y,X)
158 | And(X as Var a,And(Y as Var b,Z)) | a > b: And(Y,And(X,Z))
159 | Or(X as Var a,Or(Y as Var b,Z)) | a > b: Or(Y,Or(X,Z))
160 | And(X as Var a,And(Y as Var b,Z)) | a == b: Or(X,Z)
161 | Or(X as Var a,Or(Y as Var b,Z)) | a == b: Or(X,Z)
162 | Xor(a,b): Or(And(a,Not b),And(a,Not b))
163 | Equiv(a,b): Or(And(a,b),And(Not a,Not b))
164 | Implies(a,b): Or(Not a, b)
167 cout << "output = " << wff << '\n';
171 ///////////////////////////////////////////////////////////////////////////////
173 // Finally, the main program simply instantiates a copy of the parser,
174 // and invoke the parse method. By default, the input is from
175 // the standard input.
177 ///////////////////////////////////////////////////////////////////////////////
182 cerr << "Enter logical expressions terminated by a semicolon.\n";
183 cerr << "Use t for true, f for false, + for or, * for and, etc.:\n";