/////////////////////////////////////////////////////////////////////////////// // // This example program performs simplification of propositional logic // formulas using rewriting. We'll also define a parser to parses a // logical formula from the input. // /////////////////////////////////////////////////////////////////////////////// #include #include #include #include /////////////////////////////////////////////////////////////////////////////// // // First, we define the type Wff (Well Formed Formulas) to represent // our logic formulas. Identifiers (type Id) are represented as // atomic strings so that equality testing can be done quickly. // // We also use pretty printing annotations to // indicate to Prop to generate a simple print routine. // /////////////////////////////////////////////////////////////////////////////// datatype Wff :: rewrite = True | False | Var (class Quark) => _ | And (Wff, Wff) => "(" _ " and " _ ")" | Or (Wff, Wff) => "(" _ " or " _ ")" | Not (Wff) => "not (" _ ")" //////////////////////////////////////////////////////////////////////////// // // The following set of laws abbreviate commonly used logical connectives. // //////////////////////////////////////////////////////////////////////////// law inline Implies(a,b) = Or(Not a, b) and inline Xor(a,b) = Or(And(Not a,b),And(a,Not b)) and inline Equiv(a,b) = Or(And(a,b),And(Not a,Not b)) ; instantiate datatype Wff; /////////////////////////////////////////////////////////////////////////////// // // Next, we define the set of symbols used for our Wff parser. // /////////////////////////////////////////////////////////////////////////////// datatype WffToken :: lexeme = "[" | "]" | "(" | ")" | "*" | "+" | "->" | "<->" | "not" | "and" | "or" | "xor" | ";" | "true" | "false" | "t" | "f" | ID /[a-zA-Z][a-zA-Z0-9]*/ ; /////////////////////////////////////////////////////////////////////////////// // // Next, we declare the interface of the parser. // /////////////////////////////////////////////////////////////////////////////// syntax class WffParser { IOLexerBuffer lexbuf; public: int get_token(); // retrieve a token void process (Wff); // process a Wff }; /////////////////////////////////////////////////////////////////////////////// // // The lexer simply returns the tokens one by one; it also skip over the // spaces and newlines. If any unrecognized tokens are encountered, // the program will terminate. // /////////////////////////////////////////////////////////////////////////////// int WffParser::get_token() { matchscan while (lexbuf) { lexeme class WffToken: { return ?lexeme; } | /[ \t\n]/: // skip spaces } return EOF; } /////////////////////////////////////////////////////////////////////////////// // // The parser is defined below. Notice that the wffs are separated // by semi-colons. We call process() to simplify each one. // /////////////////////////////////////////////////////////////////////////////// syntax WffParser { //////////////////////////////////////////////////////////////////////////// // // Precedences. Note that implication associates to the right. // //////////////////////////////////////////////////////////////////////////// left: 1 "not"; left: 2 "*" "and" "xor"; left: 3 "+" "or"; right: 4 "->"; left: 5 "<->"; command: | wff ";" { process(\$1); } command | ? ";" command // for error recover, just skip to the next ; ; wff Wff: wff "+" wff { \$\$ = Or(\$1,\$3); } | wff "*" wff { \$\$ = And(\$1,\$3); } | wff "->" wff { \$\$ = Implies(\$1,\$3); } | wff "<->" wff { \$\$ = Equiv(\$1,\$3); } | wff "and" wff { \$\$ = And(\$1,\$3); } | wff "or" wff { \$\$ = Or(\$1,\$3); } | wff "xor" wff { \$\$ = Xor(\$1,\$3); } | "not" wff { \$\$ = Not(\$2); } | "(" wff ")" { \$\$ = \$2; } | "[" wff "]" { \$\$ = \$2; } | ID { \$\$ = Var(lexbuf.text()); } | "true" { \$\$ = True; } | "t" { \$\$ = True; } | "false" { \$\$ = False; } | "f" { \$\$ = False; } ; }; /////////////////////////////////////////////////////////////////////////////// // // For processing, we just transform the input formula a bit, // then prints it out. The rules are by no means exhaustive. // /////////////////////////////////////////////////////////////////////////////// void WffParser::process(Wff wff) { cout << "input = " << wff << '\n'; rewrite (wff) type (Wff) of And(True,X): X | And(X,True): X | And(False,_): False | And(_,False): False | Or(True,_): True | Or(_,True): True | Or(False,X): X | Or(X,False): X | Not True: False | Not False: True | Not(Not X): X | Not(And(X,Y)): Or(Not(X),Not(Y)) | Not(Or(X,Y)): And(Not(X),Not(Y)) | And(And(X,Y),Z): And(X,And(Y,Z)) | Or(Or(X,Y),Z): Or(X,Or(Y,Z)) | And(a,b) | a==b: a | Or(a,b) | a==b: a | And(X as Var a,Var b) | a == b: X | Or(X as Var a,Var b) | a == b: X | And(X as Var a,Y as Var b) | a > b: And(Y,X) | Or(X as Var a,Y as Var b) | a > b: Or(Y,X) | And(X as Var a,And(Y as Var b,Z)) | a > b: And(Y,And(X,Z)) | Or(X as Var a,Or(Y as Var b,Z)) | a > b: Or(Y,Or(X,Z)) | And(X as Var a,And(Y as Var b,Z)) | a == b: And(X,Z) | Or(X as Var a,Or(Y as Var b,Z)) | a == b: Or(X,Z) end rewrite; cout << "output = " << wff << '\n'; } /////////////////////////////////////////////////////////////////////////////// // // Finally, the main program simply instantiates a copy of the parser, // and invoke the parse method. By default, the input is from // the standard input. // /////////////////////////////////////////////////////////////////////////////// int main() { WffParser P; P.parse(); exit(0); }