/////////////////////////////////////////////////////////////////////////////// // This file is generated automatically using Prop (version 2.3.4), // last updated on Apr 6, 1997. // The original source file is "logic.pC". /////////////////////////////////////////////////////////////////////////////// #define PROP_REWRITING_USED #define PROP_PRINTER_USED #define PROP_REGEXP_MATCHING_USED #define PROP_PARSER_USED #define PROP_QUARK_USED #include #line 1 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // // 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. // /////////////////////////////////////////////////////////////////////////////// #line 23 "logic.pC" #line 39 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // // Forward class definition for Wff // /////////////////////////////////////////////////////////////////////////////// #ifndef datatype_Wff_defined #define datatype_Wff_defined class a_Wff; typedef a_Wff * Wff; #endif # define True (Wff)0 # define False (Wff)1 /////////////////////////////////////////////////////////////////////////////// // // Base class for datatype Wff // /////////////////////////////////////////////////////////////////////////////// class a_Wff : public TermObj { public: enum Tag_Wff { tag_Var = 0, tag_And = 1, tag_Or = 2, tag_Not = 3 }; public: const Tag_Wff tag__; // variant tag protected: inline a_Wff(Tag_Wff t__) : tag__(t__) {} public: }; inline int boxed(const a_Wff * x) { return (unsigned long)x >= 2; } inline int untag(const a_Wff * x) { return boxed(x) ? x->tag__ + 2 : (int)x; } /////////////////////////////////////////////////////////////////////////////// // // Pretty printing methods for Wff // /////////////////////////////////////////////////////////////////////////////// class PrettyOStream; extern ostream& operator<<(ostream&, Wff); extern PrettyOStream& operator<<(PrettyOStream&, Wff); /////////////////////////////////////////////////////////////////////////////// // // Class for datatype constructor Wff::Var // /////////////////////////////////////////////////////////////////////////////// class Wff_Var : public a_Wff { public: #line 26 "logic.pC" Quark Var; inline Wff_Var (Quark const & x_Var) : a_Wff(tag_Var), Var(x_Var) { } }; /////////////////////////////////////////////////////////////////////////////// // // Class for datatype constructor Wff::And // /////////////////////////////////////////////////////////////////////////////// class Wff_And : public a_Wff { public: #line 26 "logic.pC" Wff _1; Wff _2; inline Wff_And (Wff x_1, Wff x_2) : a_Wff(tag_And), _1(x_1), _2(x_2) { } }; /////////////////////////////////////////////////////////////////////////////// // // Class for datatype constructor Wff::Or // /////////////////////////////////////////////////////////////////////////////// class Wff_Or : public a_Wff { public: #line 27 "logic.pC" Wff _1; Wff _2; inline Wff_Or (Wff x_1, Wff x_2) : a_Wff(tag_Or), _1(x_1), _2(x_2) { } }; /////////////////////////////////////////////////////////////////////////////// // // Class for datatype constructor Wff::Not // /////////////////////////////////////////////////////////////////////////////// class Wff_Not : public a_Wff { public: #line 28 "logic.pC" Wff Not; inline Wff_Not (Wff x_Not) : a_Wff(tag_Not), Not(x_Not) { } }; /////////////////////////////////////////////////////////////////////////////// // // Datatype constructor functions for Wff // /////////////////////////////////////////////////////////////////////////////// inline a_Wff * Var (Quark const & x_Var) { return new Wff_Var (x_Var); } inline a_Wff * And (Wff x_1, Wff x_2) { return new Wff_And (x_1, x_2); } inline a_Wff * Or (Wff x_1, Wff x_2) { return new Wff_Or (x_1, x_2); } inline a_Wff * Not (Wff x_Not) { return new Wff_Not (x_Not); } /////////////////////////////////////////////////////////////////////////////// // // Downcasting functions for Wff // /////////////////////////////////////////////////////////////////////////////// inline Wff_Var * _Var(const a_Wff * _x_) { return (Wff_Var *)_x_; } inline Wff_And * _And(const a_Wff * _x_) { return (Wff_And *)_x_; } inline Wff_Or * _Or(const a_Wff * _x_) { return (Wff_Or *)_x_; } inline Wff_Not * _Not(const a_Wff * _x_) { return (Wff_Not *)_x_; } /////////////////////////////////////////////////////////////////////////////// // Definition of law Implies /////////////////////////////////////////////////////////////////////////////// #line 36 "logic.pC" inline Wff Implies(Wff a, Wff b) { return Or(Not(a),b); } /////////////////////////////////////////////////////////////////////////////// // Definition of law Xor /////////////////////////////////////////////////////////////////////////////// #line 37 "logic.pC" inline Wff Xor(Wff a, Wff b) { return Or(And(Not(a),b),And(a,Not(b))); } /////////////////////////////////////////////////////////////////////////////// // Definition of law Equiv /////////////////////////////////////////////////////////////////////////////// #line 38 "logic.pC" inline Wff Equiv(Wff a, Wff b) { return Or(And(a,b),And(Not(a),Not(b))); } #line 39 "logic.pC" #line 39 "logic.pC" #line 41 "logic.pC" #line 41 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // // Interface specification of datatype Wff // /////////////////////////////////////////////////////////////////////////////// #line 41 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // // Pretty printing methods for Wff // /////////////////////////////////////////////////////////////////////////////// ostream& operator << (ostream& strm__, Wff obj__); PrettyOStream& operator << (PrettyOStream& strm__, Wff obj__); /////////////////////////////////////////////////////////////////////////////// // // Instantiation of datatype Wff // /////////////////////////////////////////////////////////////////////////////// #line 41 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // // Pretty printing methods for Wff // /////////////////////////////////////////////////////////////////////////////// ostream& operator << (ostream& strm__, Wff obj__) { PrettyOStream S(strm__); S << obj__; return strm__; } PrettyOStream& operator << (PrettyOStream& strm__, Wff obj__) { switch (untag(obj__)) { case ((int)True): strm__ << "True"; break; case ((int)False): strm__ << "False"; break; case 2: strm__ << _Var(obj__)->Var; // Quark break; case 3: strm__ << '('; strm__ << _And(obj__)->_1; // Wff strm__ << " and "; strm__ << _And(obj__)->_2; // Wff strm__ << ')'; break; case 4: strm__ << '('; strm__ << _Or(obj__)->_1; // Wff strm__ << " or "; strm__ << _Or(obj__)->_2; // Wff strm__ << ')'; break; case 5: strm__ << "not ("; strm__ << _Not(obj__)->Not; // Wff strm__ << ')'; break; } return strm__; } #line 41 "logic.pC" #line 41 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // // Next, we define the set of symbols used for our Wff parser. // /////////////////////////////////////////////////////////////////////////////// #line 48 "logic.pC" #line 52 "logic.pC" enum WffToken { XXflXX = 256, XXfnXX = 257, XXciXX = 258, XXcjXX = 259, XXckXX = 260, XXclXX = 261, XXcndoXX = 262, XXdmcndoXX = 263, XX_n_o_tXX = 264, XX_a_n_dXX = 265, XX_o_rXX = 266, XX_x_o_rXX = 267, XXdlXX = 268, XX_t_r_u_eXX = 269, XX_f_a_l_s_eXX = 270, XX_tXX = 271, XX_fXX = 272, ID = 273 }; /////////////////////////////////////////////////////////////////////////////// // // Pretty printing methods for WffToken // /////////////////////////////////////////////////////////////////////////////// class PrettyOStream; extern ostream& operator<<(ostream&, WffToken); extern PrettyOStream& operator<<(PrettyOStream&, WffToken); #line 52 "logic.pC" #line 52 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // // Next, we declare the interface of the parser. // /////////////////////////////////////////////////////////////////////////////// #line 59 "logic.pC" #line 64 "logic.pC" class WffParser : public LR1Parser { public: //////////////////////////////////////////////////////////////////////////// // Parser table type definitions //////////////////////////////////////////////////////////////////////////// typedef LR1Parser Super; typedef Super::Offset Offset; typedef Super::State State; typedef Super::Rule Rule; typedef Super::Symbol Symbol; typedef Super::ProductionLength ProductionLength; typedef Super::ShortSymbol ShortSymbol; typedef Super::EquivMap EquivMap; enum { INITIAL_STACK_SIZE_ = 256, MAX_STACK_SIZE_ = 8192 }; protected: //////////////////////////////////////////////////////////////////////////// // Semantic value stack //////////////////////////////////////////////////////////////////////////// union WffParser_semantic_stack_type * t__, * bot__; int stack_size__; int heap_allocated__; public: //////////////////////////////////////////////////////////////////////////// // Constructor and parsing method //////////////////////////////////////////////////////////////////////////// WffParser(); virtual void parse(); void action_driver(const Rule); private: void adjust_stack(int); void grow_semantic_stack(); #line 60 "logic.pC" IOLexerBuffer lexbuf; public: int get_token(); // retrieve a token void process (Wff); // process a Wff #line 64 "logic.pC" }; #line 64 "logic.pC" #line 64 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // // 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() { #line 74 "logic.pC" #line 77 "logic.pC" { for (;;) { { static const DFATables::Offset _X1_base [ 37 ] = { 0, 0, 0, 22, 70, 7, 9, 69, 34, 13, 0, 0, 69, 0, 63, 0, 0, 0, 0, 0, 29, 31, 62, 33, 39, 43, 62, 0, 51, 44, 50, 45, 47, 0, 34, 48, 16 }; static const DFATables::State _X1_check [ 105 ] = { 0, 0, 1, 0, 1, 0, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 3, 5, 5, 6, 6, 3, 9, 9, 36, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 8, 20, 20, 21, 34, 23, 8, 21, 23, 24, 25, 24, 29, 25, 29, 31, 35, 32, 35, 31, 30, 28, 26, 14, 12, 0, 0, 0, 0, 0, 0, 0, 0, 0, 22, 0, 0, 0, 0, 0, 0, 7, 4, 0, 0, 0, 0, 0, 0 }; static const DFATables::State _X1_next [ 105 ] = { 0, 0, 19, 0, 19, 0, 19, 18, 17, 16, 15, 14, 0, 0, 13, 12, 0, 4, 0, 11, 10, 4, 9, 4, 4, 8, 4, 7, 6, 4, 4, 5, 4, 3, 4, 4, 21, 4, 22, 4, 25, 4, 4, 4, 4, 4, 4, 4, 4, 4, 20, 4, 4, 4, 4, 4, 24, 4, 28, 4, 4, 4, 4, 29, 30, 31, 32, 4, 34, 4, 4, 4, 36, 4, 4, 35, 4, 4, 33, 27, 26, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 23, 4, 0, 0, 0, 0, 0, 0 }; static const DFATables::State _X1_def [ 37 ] = { 0, 0, 1, 0, 3, 3, 3, 3, 3, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 3, 3, 3, 3, 24, 0, 0, 24, 24, 24, 24, 24, 0, 24, 24, 24 }; static const unsigned char _X1_equiv_classes [ 256 ] = { 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 6, 5, 5, 5, 5, 5, 5, 5, 7, 8, 9, 10, 5, 11, 5, 5, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 13, 14, 15, 13, 16, 13, 13, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 19, 18, 20, 18, 18, 18, 22, 21, 21, 23, 24, 25, 21, 21, 21, 21, 21, 26, 21, 27, 28, 21, 21, 29, 30, 31, 32, 21, 21, 33, 21, 21, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, 34 }; static const DFATables::Rule _X1_accept_rule [ 37 ] = { -1, 0, 0, 18, 18, 16, 18, 18, 17, 18, -3, -2, 0, -14, 0, -7, -6, -5, -4, -20, 18, 18, 11, 18, 18, 18, 0, -8, 12, 18, 9, 18, 10, -9, 14, 18, 15 }; static const RegexMatch _X1 ( _X1_base, _X1_check, _X1_def, _X1_next, _X1_accept_rule, _X1_equiv_classes ); int rule__; const char * next; switch(rule__ = _X1.MatchText(RegexMatch::start_state,lexbuf,next)) { case 1: { L2:; #line 75 "logic.pC" return ((WffToken)(rule__ + 255)); #line 75 "logic.pC" } break; case 2: { goto L2; } break; case 3: { goto L2; } break; case 4: { goto L2; } break; case 5: { goto L2; } break; case 6: { goto L2; } break; case 7: { goto L2; } break; case 8: { goto L2; } break; case 9: { goto L2; } break; case 10: { goto L2; } break; case 11: { goto L2; } break; case 12: { goto L2; } break; case 13: { goto L2; } break; case 14: { goto L2; } break; case 15: { goto L2; } break; case 16: { goto L2; } break; case 17: { goto L2; } break; case 18: { goto L2; } break; case 19: {} break; default: { goto L1; } } } } L1:; } #line 77 "logic.pC" #line 77 "logic.pC" return EOF; } /////////////////////////////////////////////////////////////////////////////// // // The parser is defined below. Notice that the wffs are separated // by semi-colons. We call process() to simplify each one. // /////////////////////////////////////////////////////////////////////////////// #line 87 "logic.pC" #line 122 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // Encoded parser tables for syntax class WffParser /////////////////////////////////////////////////////////////////////////////// static const DFATables::Offset WffParser_base [ 38 ] = { 0, 0, 53, 2, 4, 6, 0, 0, 0, 0, 0, 27, 29, 24, 0, 0, 6, 0, 20, 19, 29, 37, 41, 43, 45, 47, 0, 0, 0, 18, 46, 0, 8, 55, 0, 0, 0, 0 }; static const DFATables::State WffParser_check [ 81 ] = { 0, 15, 1, 0, 3, 0, 4, 16, 5, 32, 1, 1, 15, 1, 32, 1, 1, 1, 1, 1, 16, 19, 1, 1, 3, 3, 4, 4, 5, 5, 12, 20, 12, 12, 12, 12, 12, 12, 12, 21, 29, 19, 19, 22, 18, 23, 13, 24, 11, 25, 30, 20, 20, 30, 2, 30, 33, 0, 0, 21, 21, 33, 0, 22, 22, 23, 23, 24, 24, 25, 25, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 }; static const DFATables::State WffParser_next [ 81 ] = { 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 3, 4, 16411, 5, 0, 16390, 16391, 16392, 16393, 16394, 16412, 0, 11, 12, 0, 16398, 0, 15, 0, 16, 16402, 0, 19, 20, 21, 22, 23, 24, 25, 0, 16421, 0, 30, 0, 29, 0, 16410, 0, 17, 0, 20, 0, 16415, 23, 13, 25, 0, 0, 0, 0, 32, 0, 0, 0, 33, 0, 16418, 0, 35, 0, 16420, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 }; static const DFATables::State WffParser_def [ 38 ] = { 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 12, 12, 0, 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 0, 0, 12, 12, 0, 30, 0, 0 }; static const DFATables::State WffParser_defact [ 38 ] = { 0, 32768, 0, 0, 0, 0, 32781, 32782, 32783, 32784, 32785, 0, 0, 32768, 32778, 0, 0, 32787, 32786, 0, 0, 0, 0, 0, 0, 0, 32770, 32779, 32780, 32768, 32771, 32772, 32773, 32774, 32775, 32776, 32777, 32769 }; static const DFATables::ProductionLength WffParser_len [ 20 ] = { 0, 4, 3, 3, 3, 3, 3, 3, 3, 3, 2, 3, 3, 1, 1, 1, 1, 1, 0, 2 }; static const DFATables::ProductionLength WffParser_ncount [ 20 ] = { 0, 3, 1, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1 }; static const DFATables::ShortSymbol WffParser_lhs [ 20 ] = { 22, 22, 22, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 24, 25 }; static const DFATables::EquivMap WffParser_equiv [ 281 ] = { 21, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 13, 14, 11, 12, 4, 3, 5, 6, 10, 7, 8, 9, 1, 16, 18, 17, 19, 15, 2, 0, 22, 23, 24, 25 }; /////////////////////////////////////////////////////////////////////////////// // Debugging tables for syntax class WffParser /////////////////////////////////////////////////////////////////////////////// #ifdef DEBUG_WffParser static const int WffParser_line[] = { 0, 0, 0, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 102, 0 }; static const char * const WffParser_symbolname[] = { "???", "\";\"", "?", "\"+\"", "\"*\"", "\"->\"", "\"<->\"", "\"and\"", "\"or\"", "\"xor\"", "\"not\"", "\"(\"", "\")\"", "\"[\"", "\"]\"", "ID", "\"true\"", "\"t\"", "\"false\"", "\"f\"", "???", "???", "command", "wff", "???", "???" }; static const DFATables::ShortSymbol WffParser_rhs_0[] = { -1 }; static const DFATables::ShortSymbol WffParser_rhs_1[] = { 23, 1, 24, 22, -1 }; static const DFATables::ShortSymbol WffParser_rhs_2[] = { 2, 1, 22, -1 }; static const DFATables::ShortSymbol WffParser_rhs_3[] = { 23, 3, 23, -1 }; static const DFATables::ShortSymbol WffParser_rhs_4[] = { 23, 4, 23, -1 }; static const DFATables::ShortSymbol WffParser_rhs_5[] = { 23, 5, 23, -1 }; static const DFATables::ShortSymbol WffParser_rhs_6[] = { 23, 6, 23, -1 }; static const DFATables::ShortSymbol WffParser_rhs_7[] = { 23, 7, 23, -1 }; static const DFATables::ShortSymbol WffParser_rhs_8[] = { 23, 8, 23, -1 }; static const DFATables::ShortSymbol WffParser_rhs_9[] = { 23, 9, 23, -1 }; static const DFATables::ShortSymbol WffParser_rhs_10[] = { 10, 23, -1 }; static const DFATables::ShortSymbol WffParser_rhs_11[] = { 11, 23, 12, -1 }; static const DFATables::ShortSymbol WffParser_rhs_12[] = { 13, 23, 14, -1 }; static const DFATables::ShortSymbol WffParser_rhs_13[] = { 15, -1 }; static const DFATables::ShortSymbol WffParser_rhs_14[] = { 16, -1 }; static const DFATables::ShortSymbol WffParser_rhs_15[] = { 17, -1 }; static const DFATables::ShortSymbol WffParser_rhs_16[] = { 18, -1 }; static const DFATables::ShortSymbol WffParser_rhs_17[] = { 19, -1 }; static const DFATables::ShortSymbol WffParser_rhs_18[] = { -1 }; static const DFATables::ShortSymbol WffParser_rhs_19[] = { 22, 21, -1 }; static const DFATables::ShortSymbol * WffParser_rhs[] = { WffParser_rhs_0, WffParser_rhs_1, WffParser_rhs_2, WffParser_rhs_3, WffParser_rhs_4, WffParser_rhs_5, WffParser_rhs_6, WffParser_rhs_7, WffParser_rhs_8, WffParser_rhs_9, WffParser_rhs_10, WffParser_rhs_11, WffParser_rhs_12, WffParser_rhs_13, WffParser_rhs_14, WffParser_rhs_15, WffParser_rhs_16, WffParser_rhs_17, WffParser_rhs_18, WffParser_rhs_19 }; #endif /////////////////////////////////////////////////////////////////////////////// // Semantic value stack for syntax class WffParser /////////////////////////////////////////////////////////////////////////////// union WffParser_semantic_stack_type { int dummy; #line 106 "logic.pC" typedef Wff ATTRIBUTE_0; ATTRIBUTE_0 _72, _69, _66, _63, _60, _57, _55, _52, _50, _48, _46, _44, _42, _41, _39, _37, _36, _34, _32, _31, _29, _27, _26, _24, _22, _21, _19, _17, _16, _14, _12, _11, _3; }; /////////////////////////////////////////////////////////////////////////////// // Parser driver for syntax class WffParser /////////////////////////////////////////////////////////////////////////////// inline void WffParser::action_driver(const Rule _r_) { WffParser_semantic_stack_type syn_; //////////////////////////////////////////////////////////////////////////// // Tracing code for syntax class WffParser //////////////////////////////////////////////////////////////////////////// #ifdef DEBUG_WffParser { cerr << "Reducing via rule " << _r_ << " at line " << WffParser_line[_r_] << ", " << WffParser_symbolname[WffParser_lhs[_r_]] << " <- "; for (const DFATables::ShortSymbol * _p_ = WffParser_rhs[_r_]; *_p_ >= 0; _p_++) cerr << WffParser_symbolname[*_p_] << ' '; cerr << '\n'; } #endif //////////////////////////////////////////////////////////////////////////// // Actions for syntax class WffParser //////////////////////////////////////////////////////////////////////////// t__ -= WffParser_ncount[_r_]; switch (_r_) { #undef to__ #define to__ 0 #undef to__ #define to__ -1 case 18: { #line 102 "logic.pC" process(t__[1+to__]._3); #line 102 "logic.pC" } break; #undef to__ #define to__ 0 case 3: { #line 106 "logic.pC" syn_._11 = Or(t__[1+to__]._12,t__[2+to__]._14); #line 106 "logic.pC" } break; case 4: { #line 107 "logic.pC" syn_._16 = And(t__[1+to__]._17,t__[2+to__]._19); #line 107 "logic.pC" } break; case 5: { #line 108 "logic.pC" syn_._21 = Implies(t__[1+to__]._22,t__[2+to__]._24); #line 108 "logic.pC" } break; case 6: { #line 109 "logic.pC" syn_._26 = Equiv(t__[1+to__]._27,t__[2+to__]._29); #line 109 "logic.pC" } break; case 7: { #line 110 "logic.pC" syn_._31 = And(t__[1+to__]._32,t__[2+to__]._34); #line 110 "logic.pC" } break; case 8: { #line 111 "logic.pC" syn_._36 = Or(t__[1+to__]._37,t__[2+to__]._39); #line 111 "logic.pC" } break; case 9: { #line 112 "logic.pC" syn_._41 = Xor(t__[1+to__]._42,t__[2+to__]._44); #line 112 "logic.pC" } break; case 10: { #line 113 "logic.pC" syn_._46 = Not(t__[1+to__]._48); #line 113 "logic.pC" } break; case 11: { #line 114 "logic.pC" syn_._50 = t__[1+to__]._52; #line 114 "logic.pC" } break; case 12: { #line 115 "logic.pC" syn_._55 = t__[1+to__]._57; #line 115 "logic.pC" } break; case 13: { #line 116 "logic.pC" syn_._60 = Var(lexbuf.text()); #line 116 "logic.pC" } break; case 14: { #line 117 "logic.pC" syn_._63 = True; #line 117 "logic.pC" } break; case 15: { #line 118 "logic.pC" syn_._66 = True; #line 118 "logic.pC" } break; case 16: { #line 119 "logic.pC" syn_._69 = False; #line 119 "logic.pC" } break; case 17: { #line 120 "logic.pC" syn_._72 = False; #line 120 "logic.pC" } break; } if (t__ >= bot__ + stack_size__) grow_semantic_stack(); *++t__ = syn_; } /////////////////////////////////////////////////////////////////////////////// // Parsing method for parser class WffParser /////////////////////////////////////////////////////////////////////////////// void WffParser::parse() { WffParser_semantic_stack_type stack__[INITIAL_STACK_SIZE_]; t__ = bot__ = stack__; stack_size__ = sizeof(stack__)/sizeof(stack__[0]) - 1; heap_allocated__ = 0; parser_prefix(); LR1ParserDriver drv; drv.driver(*this); parser_suffix(); if (bot__ != stack__) delete [] bot__; } void WffParser::adjust_stack(int offset) { t__ += offset; } void WffParser::grow_semantic_stack() { int N = (stack_size__ + 1) * 2; WffParser_semantic_stack_type * S = new WffParser_semantic_stack_type [N]; if (N >= LR1Parser::SEMANTIC_STACK_SIZE) error_report("Warning: semantic stack overflow"); memcpy(S, bot__, sizeof(WffParser_semantic_stack_type) * (stack_size__ + 1)); if (heap_allocated__) delete [] bot__; t__ = S + (t__ - bot__); bot__ = S; stack_size__ = N - 1; heap_allocated__ = 1; } WffParser::WffParser () : Super(WffParser_base,WffParser_check,WffParser_def,WffParser_defact,WffParser_next, WffParser_len,WffParser_ncount,WffParser_lhs,WffParser_equiv,274,274,277) { } #line 122 "logic.pC" #line 122 "logic.pC" /////////////////////////////////////////////////////////////////////////////// // // 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'; #line 134 "logic.pC" #line 160 "logic.pC" extern void _l_o_g_i_cco_X2_rewrite(Wff & ); _l_o_g_i_cco_X2_rewrite(wff); #line 160 "logic.pC" #line 160 "logic.pC" 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); } #line 181 "logic.pC" class _l_o_g_i_cco_X2 : public BURS { private: _l_o_g_i_cco_X2(const _l_o_g_i_cco_X2&); // no copy constructor void operator = (const _l_o_g_i_cco_X2&); // no assignment public: struct _l_o_g_i_cco_X2_StateRec * stack__, * stack_top__; public: void labeler(const char *, int&, int); void labeler(Quark, int&, int); void labeler(Wff & redex, int&, int); inline virtual void operator () (Wff & redex) { int s; labeler(redex,s,0); } private: public: inline _l_o_g_i_cco_X2() {} }; void _l_o_g_i_cco_X2_rewrite(Wff & _x_) { _l_o_g_i_cco_X2 _r_; _r_(_x_); } /////////////////////////////////////////////////////////////////////////////// // // This macro can be redefined by the user for debugging // /////////////////////////////////////////////////////////////////////////////// #ifndef DEBUG__l_o_g_i_cco_X2 #define DEBUG__l_o_g_i_cco_X2(repl,redex,file,line,rule) repl #else static const char * _l_o_g_i_cco_X2_file_name = "logic.pC"; #endif static const TreeTables::Offset _l_o_g_i_cco_X2_accept_base [ 44 ] = { 0, 0, 0, 0, 1, 3, 4, 5, 8, 12, 15, 18, 22, 25, 27, 30, 34, 38, 41, 45, 48, 52, 56, 59, 63, 65, 69, 71, 74, 77, 81, 83, 86, 89, 92, 96, 100, 102, 105, 109, 113, 115, 117, 121 }; static const TreeTables::ShortRule _l_o_g_i_cco_X2_accept_vector [ 125 ] = { -1, 15, -1, 16, -1, 1, 15, -1, 0, 1, 15, -1, 0, 15, -1, 5, 16, -1, 4, 5, 16, -1, 4, 16, -1, 8, -1, 3, 15, -1, 2, 3, 15, -1, 0, 3, 15, -1, 2, 15, -1, 1, 2, 15, -1, 7, 16, -1, 6, 7, 16, -1, 4, 7, 16, -1, 6, 16, -1, 5, 6, 16, -1, 9, -1, 15, 17, 19, -1, 15, -1, 3, 15, -1, 1, 15, -1, 16, 18, 20, -1, 16, -1, 7, 16, -1, 5, 16, -1, 13, 15, -1, 3, 13, 15, -1, 1, 13, 15, -1, 11, -1, 14, 16, -1, 7, 14, 16, -1, 5, 14, 16, -1, 12, -1, 10, -1, 15, 21, 23, -1, 16, 22, 24, -1 }; static const TreeTables::ShortState _l_o_g_i_cco_X2_theta_3[5][9] = { { 4, 7, 14, 4, 4, 4, 4, 4, 4 }, { 9, 8, 16, 9, 9, 9, 9, 9, 9 }, { 17, 18, 15, 17, 17, 17, 17, 17, 17 }, { 26, 28, 27, 25, 42, 42, 42, 42, 42 }, { 33, 35, 34, 33, 33, 33, 33, 33, 33 } }; static const TreeTables::ShortState _l_o_g_i_cco_X2_theta_4[5][9] = { { 5, 10, 19, 5, 5, 5, 5, 5, 5 }, { 12, 11, 21, 12, 12, 12, 12, 12, 12 }, { 22, 23, 20, 22, 22, 22, 22, 22, 22 }, { 30, 32, 31, 29, 43, 43, 43, 43, 43 }, { 37, 39, 38, 37, 37, 37, 37, 37, 37 } }; static const TreeTables::ShortState _l_o_g_i_cco_X2_theta_5[6] = { 6, 13, 24, 36, 40, 41 }; static const TreeTables::ShortState _l_o_g_i_cco_X2_mu_3_0[44] = { 0, 1, 2, 3, 4, 0, 0, 4, 4, 4, 0, 0, 0, 0, 4, 4, 4, 4, 4, 0, 0, 0, 0, 0, 0, 4, 4, 4, 4, 0, 0, 0, 0, 4, 4, 4, 0, 0, 0, 0, 0, 0, 4, 0 }; static const TreeTables::ShortState _l_o_g_i_cco_X2_mu_3_1[44] = { 0, 1, 2, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 5, 6, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0 }; static const TreeTables::ShortState _l_o_g_i_cco_X2_mu_4_0[44] = { 0, 1, 2, 3, 0, 4, 0, 0, 0, 0, 4, 4, 4, 0, 0, 0, 0, 0, 0, 4, 4, 4, 4, 4, 0, 0, 0, 0, 0, 4, 4, 4, 4, 0, 0, 0, 0, 4, 4, 4, 0, 0, 0, 4 }; static const TreeTables::ShortState _l_o_g_i_cco_X2_mu_4_1[44] = { 0, 1, 2, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 5, 6, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8 }; static const TreeTables::ShortState _l_o_g_i_cco_X2_mu_5_0[44] = { 0, 1, 2, 0, 3, 4, 5, 3, 3, 3, 4, 4, 4, 5, 3, 3, 3, 3, 3, 4, 4, 4, 4, 4, 5, 3, 3, 3, 3, 4, 4, 4, 4, 3, 3, 3, 5, 4, 4, 4, 5, 5, 3, 4 }; inline void _l_o_g_i_cco_X2::labeler(char const * redex,int& s__,int) { { s__ = 0; } } inline void _l_o_g_i_cco_X2::labeler(Quark redex,int& s__,int) { { s__ = 0; } } void _l_o_g_i_cco_X2::labeler (Wff & redex, int& s__, int r__) { replacement__: int cached__; if (r__ && boxed(redex) && (cached__ = redex->get_rewrite_state()) != BURS::undefined_state) { s__ = cached__; return; } if (boxed(redex)) { switch(redex->tag__) { case a_Wff::tag_Var: { int s0__; labeler(_Var(redex)->Var, s0__, r__); s__ = 3;} break; case a_Wff::tag_And: { int s0__; int s1__; labeler(_And(redex)->_1, s0__, r__); labeler(_And(redex)->_2, s1__, r__); s__ = _l_o_g_i_cco_X2_theta_3[_l_o_g_i_cco_X2_mu_3_0[s0__]][_l_o_g_i_cco_X2_mu_3_1[s1__]]; } break; case a_Wff::tag_Or: { int s0__; int s1__; labeler(_Or(redex)->_1, s0__, r__); labeler(_Or(redex)->_2, s1__, r__); s__ = _l_o_g_i_cco_X2_theta_4[_l_o_g_i_cco_X2_mu_4_0[s0__]][_l_o_g_i_cco_X2_mu_4_1[s1__]]; } break; default: { int s0__; labeler(_Not(redex)->Not, s0__, r__); s__ = _l_o_g_i_cco_X2_theta_5[_l_o_g_i_cco_X2_mu_5_0[s0__]]; } break; } } else { if (((int)redex)) {s__ = 2; } else {s__ = 1; } } const TreeTables::ShortRule * o__ = _l_o_g_i_cco_X2_accept_vector + _l_o_g_i_cco_X2_accept_base[s__]; accept__: switch (*o__) { case 24: if ((_Var(_Or(redex)->_1)->Var == _Var(_Or(_Or(redex)->_2)->_1)->Var)) { #line 159 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(Or(_Or(redex)->_1,_Or(_Or(redex)->_2)->_2),redex,_l_o_g_i_cco_X2_file_name,159,"Or (X as Var a, Or (Y as Var b, Z)) | (redex!Or.1!Var == redex!Or.2!Or.1!Var): ..."); r__ = 1; goto replacement__; } #line 160 "logic.pC" } else { ++o__; goto accept__; } break; case 23: if ((_Var(_And(redex)->_1)->Var == _Var(_And(_And(redex)->_2)->_1)->Var)) { #line 158 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(And(_And(redex)->_1,_And(_And(redex)->_2)->_2),redex,_l_o_g_i_cco_X2_file_name,158,"And (X as Var a, And (Y as Var b, Z)) | (redex!And.1!Var == redex!And.2!And.1!Var): ..."); r__ = 1; goto replacement__; } #line 159 "logic.pC" } else { ++o__; goto accept__; } break; case 22: if ((_Var(_Or(redex)->_1)->Var > _Var(_Or(_Or(redex)->_2)->_1)->Var)) { #line 157 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(Or(_Or(_Or(redex)->_2)->_1,Or(_Or(redex)->_1,_Or(_Or(redex)->_2)->_2)),redex,_l_o_g_i_cco_X2_file_name,157,"Or (X as Var a, Or (Y as Var b, Z)) | (redex!Or.1!Var > redex!Or.2!Or.1!Var): ..."); r__ = 1; goto replacement__; } #line 158 "logic.pC" } else { ++o__; goto accept__; } break; case 21: if ((_Var(_And(redex)->_1)->Var > _Var(_And(_And(redex)->_2)->_1)->Var)) { #line 156 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(And(_And(_And(redex)->_2)->_1,And(_And(redex)->_1,_And(_And(redex)->_2)->_2)),redex,_l_o_g_i_cco_X2_file_name,156,"And (X as Var a, And (Y as Var b, Z)) | (redex!And.1!Var > redex!And.2!And.1!Var): ..."); r__ = 1; goto replacement__; } #line 157 "logic.pC" } else { ++o__; goto accept__; } break; case 20: if ((_Var(_Or(redex)->_1)->Var > _Var(_Or(redex)->_2)->Var)) { #line 155 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(Or(_Or(redex)->_2,_Or(redex)->_1),redex,_l_o_g_i_cco_X2_file_name,155,"Or (X as Var a, Y as Var b) | (redex!Or.1!Var > redex!Or.2!Var): ..."); r__ = 1; goto replacement__; } #line 156 "logic.pC" } else { ++o__; goto accept__; } break; case 19: if ((_Var(_And(redex)->_1)->Var > _Var(_And(redex)->_2)->Var)) { #line 154 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(And(_And(redex)->_2,_And(redex)->_1),redex,_l_o_g_i_cco_X2_file_name,154,"And (X as Var a, Y as Var b) | (redex!And.1!Var > redex!And.2!Var): ..."); r__ = 1; goto replacement__; } #line 155 "logic.pC" } else { ++o__; goto accept__; } break; case 18: if ((_Var(_Or(redex)->_1)->Var == _Var(_Or(redex)->_2)->Var)) { #line 153 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(_Or(redex)->_1,redex,_l_o_g_i_cco_X2_file_name,153,"Or (X as Var a, Var b) | (redex!Or.1!Var == redex!Or.2!Var): ..."); r__ = 1; goto replacement__; } #line 154 "logic.pC" } else { ++o__; goto accept__; } break; case 17: if ((_Var(_And(redex)->_1)->Var == _Var(_And(redex)->_2)->Var)) { #line 152 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(_And(redex)->_1,redex,_l_o_g_i_cco_X2_file_name,152,"And (X as Var a, Var b) | (redex!And.1!Var == redex!And.2!Var): ..."); r__ = 1; goto replacement__; } #line 153 "logic.pC" } else { ++o__; goto accept__; } break; case 16: if ((_Or(redex)->_1 == _Or(redex)->_2)) { #line 151 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(_Or(redex)->_1,redex,_l_o_g_i_cco_X2_file_name,151,"Or (a, b) | (redex!Or.1 == redex!Or.2): ..."); r__ = 1; goto replacement__; } #line 152 "logic.pC" } else { ++o__; goto accept__; } break; case 15: if ((_And(redex)->_1 == _And(redex)->_2)) { #line 150 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(_And(redex)->_1,redex,_l_o_g_i_cco_X2_file_name,150,"And (a, b) | (redex!And.1 == redex!And.2): ..."); r__ = 1; goto replacement__; } #line 151 "logic.pC" } else { ++o__; goto accept__; } break; case 14: { #line 149 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(Or(_Or(_Or(redex)->_1)->_1,Or(_Or(_Or(redex)->_1)->_2,_Or(redex)->_2)),redex,_l_o_g_i_cco_X2_file_name,149,"Or (Or (X, Y), Z): ..."); r__ = 1; goto replacement__; } #line 150 "logic.pC" } break; case 13: { #line 148 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(And(_And(_And(redex)->_1)->_1,And(_And(_And(redex)->_1)->_2,_And(redex)->_2)),redex,_l_o_g_i_cco_X2_file_name,148,"And (And (X, Y), Z): ..."); r__ = 1; goto replacement__; } #line 149 "logic.pC" } break; case 12: { #line 147 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(And(Not(_Or(_Not(redex)->Not)->_1),Not(_Or(_Not(redex)->Not)->_2)),redex,_l_o_g_i_cco_X2_file_name,147,"Not Or (X, Y): ..."); r__ = 1; goto replacement__; } #line 148 "logic.pC" } break; case 11: { #line 146 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(Or(Not(_And(_Not(redex)->Not)->_1),Not(_And(_Not(redex)->Not)->_2)),redex,_l_o_g_i_cco_X2_file_name,146,"Not And (X, Y): ..."); r__ = 1; goto replacement__; } #line 147 "logic.pC" } break; case 10: { #line 145 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(_Not(_Not(redex)->Not)->Not,redex,_l_o_g_i_cco_X2_file_name,145,"Not Not X: ..."); r__ = 1; goto replacement__; } #line 146 "logic.pC" } break; case 9: { #line 144 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(True,redex,_l_o_g_i_cco_X2_file_name,144,"Not False: ..."); r__ = 1; goto replacement__; } #line 145 "logic.pC" } break; case 8: { #line 143 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(False,redex,_l_o_g_i_cco_X2_file_name,143,"Not True: ..."); r__ = 1; goto replacement__; } #line 144 "logic.pC" } break; case 7: { #line 142 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(_Or(redex)->_1,redex,_l_o_g_i_cco_X2_file_name,142,"Or (X, False): ..."); r__ = 1; goto replacement__; } #line 143 "logic.pC" } break; case 6: { #line 141 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(_Or(redex)->_2,redex,_l_o_g_i_cco_X2_file_name,141,"Or (False, X): ..."); r__ = 1; goto replacement__; } #line 142 "logic.pC" } break; case 5: { #line 140 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(True,redex,_l_o_g_i_cco_X2_file_name,140,"Or (_, True): ..."); r__ = 1; goto replacement__; } #line 141 "logic.pC" } break; case 4: { #line 139 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(True,redex,_l_o_g_i_cco_X2_file_name,139,"Or (True, _): ..."); r__ = 1; goto replacement__; } #line 140 "logic.pC" } break; case 3: { #line 138 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(False,redex,_l_o_g_i_cco_X2_file_name,138,"And (_, False): ..."); r__ = 1; goto replacement__; } #line 139 "logic.pC" } break; case 2: { #line 137 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(False,redex,_l_o_g_i_cco_X2_file_name,137,"And (False, _): ..."); r__ = 1; goto replacement__; } #line 138 "logic.pC" } break; case 1: { #line 136 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(_And(redex)->_1,redex,_l_o_g_i_cco_X2_file_name,136,"And (X, True): ..."); r__ = 1; goto replacement__; } #line 137 "logic.pC" } break; case 0: { #line 135 "logic.pC" { redex = DEBUG__l_o_g_i_cco_X2(_And(redex)->_2,redex,_l_o_g_i_cco_X2_file_name,135,"And (True, X): ..."); r__ = 1; goto replacement__; } #line 136 "logic.pC" } break; } if (boxed(redex)) { redex->set_rewrite_state(s__); } } /* ------------------------------- Statistics ------------------------------- Merge matching rules = yes Number of DFA nodes merged = 17 Number of ifs generated = 0 Number of switches generated = 1 Number of labels = 1 Number of gotos = 17 Adaptive matching = disabled Fast string matching = disabled Inline downcasts = disabled -------------------------------------------------------------------------- */