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 ///////////////////////////////////////////////////////////////////////////////
26 Rewrite() : state(BURS::undefined_state) {}
27 int get_wff_state() const { return state; }
28 void set_wff_state(int s) { state = s; }
31 datatype Wff : public Rewrite
34 | Var (class Quark) => _
35 | And (Wff, Wff) => "(" _ " and " _ ")"
36 | Or (Wff, Wff) => "(" _ " or " _ ")"
37 | Not (Wff) => "not (" _ ")"
39 ////////////////////////////////////////////////////////////////////////////
41 // The following set of laws abbreviate commonly used logical connectives.
43 ////////////////////////////////////////////////////////////////////////////
44 law inline Implies(a,b) = Or(Not a, b)
45 and inline Xor(a,b) = Or(And(Not a,b),And(a,Not b))
46 and inline Equiv(a,b) = Or(And(a,b),And(Not a,Not b))
49 instantiate datatype Wff;
51 ///////////////////////////////////////////////////////////////////////////////
53 // Next, we define the set of symbols used for our Wff parser.
55 ///////////////////////////////////////////////////////////////////////////////
56 datatype WffToken :: lexeme =
57 "[" | "]" | "(" | ")" | "*" | "+" | "->" | "<->"
58 | "not" | "and" | "or" | "xor" | ";" | "true" | "false" | "t" | "f"
59 | ID /[a-zA-Z][a-zA-Z0-9]*/
62 ///////////////////////////////////////////////////////////////////////////////
64 // Next, we declare the interface of the parser.
66 ///////////////////////////////////////////////////////////////////////////////
67 syntax class WffParser
68 { IOLexerBuffer lexbuf;
70 int get_token(); // retrieve a token
71 void process (Wff); // process a Wff
74 ///////////////////////////////////////////////////////////////////////////////
76 // The lexer simply returns the tokens one by one; it also skip over the
77 // spaces and newlines. If any unrecognized tokens are encountered,
78 // the program will terminate.
80 ///////////////////////////////////////////////////////////////////////////////
81 int WffParser::get_token()
82 { matchscan while (lexbuf)
83 { lexeme class WffToken: { return ?lexeme; }
84 | /[ \t\n]/: // skip spaces
89 ///////////////////////////////////////////////////////////////////////////////
91 // The parser is defined below. Notice that the wffs are separated
92 // by semi-colons. We call process() to simplify each one.
94 ///////////////////////////////////////////////////////////////////////////////
98 ////////////////////////////////////////////////////////////////////////////
100 // Precedences. Note that implication associates to the right.
102 ////////////////////////////////////////////////////////////////////////////
104 left: 2 "*" "and" "xor";
110 | wff ";" { process($1); } command
111 | ? ";" command // for error recover, just skip to the next ;
114 wff Wff: wff "+" wff { $$ = Or($1,$3); }
115 | wff "*" wff { $$ = And($1,$3); }
116 | wff "->" wff { $$ = Implies($1,$3); }
117 | wff "<->" wff { $$ = Equiv($1,$3); }
118 | wff "and" wff { $$ = And($1,$3); }
119 | wff "or" wff { $$ = Or($1,$3); }
120 | wff "xor" wff { $$ = Xor($1,$3); }
121 | "not" wff { $$ = Not($2); }
122 | "(" wff ")" { $$ = $2; }
123 | "[" wff "]" { $$ = $2; }
124 | ID { $$ = Var(lexbuf.text()); }
125 | "true" { $$ = True; }
127 | "false" { $$ = False; }
128 | "f" { $$ = False; }
132 ///////////////////////////////////////////////////////////////////////////////
134 // For processing, we just transform the input formula a bit,
135 // then prints it out. The rules are by no means exhaustive.
137 ///////////////////////////////////////////////////////////////////////////////
138 void WffParser::process(Wff wff)
140 cout << "input = " << wff << '\n';
142 rewrite (wff) type (Wff) of
147 | And(False,_): False
148 | And(_,False): False
156 | Not(And(X,Y)): Or(Not(X),Not(Y))
157 | Not(Or(X,Y)): And(Not(X),Not(Y))
158 | And(And(X,Y),Z): And(X,And(Y,Z))
159 | Or(Or(X,Y),Z): Or(X,Or(Y,Z))
162 | And(X as Var a,Var b) | a == b: X
163 | Or(X as Var a,Var b) | a == b: X
164 | And(X as Var a,Y as Var b) | a > b: And(Y,X)
165 | Or(X as Var a,Y as Var b) | a > b: Or(Y,X)
166 | And(X as Var a,And(Y as Var b,Z)) | a > b: And(Y,And(X,Z))
167 | Or(X as Var a,Or(Y as Var b,Z)) | a > b: Or(Y,Or(X,Z))
168 | And(X as Var a,And(Y as Var b,Z)) | a == b: Or(X,Z)
169 | Or(X as Var a,Or(Y as Var b,Z)) | a == b: Or(X,Z)
172 cout << "output = " << wff << '\n';
176 ///////////////////////////////////////////////////////////////////////////////
178 // Finally, the main program simply instantiates a copy of the parser,
179 // and invoke the parse method. By default, the input is from
180 // the standard input.
182 ///////////////////////////////////////////////////////////////////////////////
187 cerr << "Enter logical expressions terminated by a semicolon.\n";
188 cerr << "Use t for true, f for false, + for or, * for and, etc.:\n";