diff --git a/parser/tau.tgf b/parser/tau.tgf index 7e74ed55..d96512ae 100644 --- a/parser/tau.tgf +++ b/parser/tau.tgf @@ -73,7 +73,7 @@ timed_capture => ws 't' ws. variable => var | timed. timed => (in | out) timed_offset. - +bool_variable => '?' chars. # TODO (HIGH) capture t is reserved for timed variables, so we should check that is not used here capture => '$' chars. # TODO (MEDIUM) remove '?' from timed variables @@ -115,7 +115,7 @@ wff_body => wff | bf_eq_cb | bf_neq_cb | wff_has_clashing_subformulas_cb # TODO (MEDIUM) check programatically that no capture is use in a rec_relation as wff wff => wff_ref | wff_and | wff_neg | wff_xor | wff_conditional | wff_or | wff_all | wff_ex | wff_imply | wff_equiv - | wff_t | wff_f | capture | variable | wff_ball | wff_bex + | wff_t | wff_f | capture | bool_variable | wff_ball | wff_bex | bf_eq | bf_neq | bf_less | bf_less_equal | bf_greater. wff_ref => sym offsets wff_ref_args. wff_ref_args => open_parenthesis (variable)* close_parenthesis. @@ -128,8 +128,8 @@ wff_imply => open_parenthesis wff wff_imply_sym wff close_parenthesis. wff_equiv => open_parenthesis wff wff_equiv_sym wff close_parenthesis. wff_all => wff_all_sym ws_required (variable|capture) ws_required wff. wff_ex => wff_ex_sym ws_required (variable|capture) ws_required wff. -wff_ball => wff_ball_sym ws_required (variable|capture) ws_required wff. -wff_bex => wff_bex_sym ws_required (variable|capture) ws_required wff. +wff_ball => wff_ball_sym ws_required (bool_variable|capture) ws_required wff. +wff_bex => wff_bex_sym ws_required (bool_variable|capture) ws_required wff. # relational operators # diff --git a/parser/tau_parser.generated.h b/parser/tau_parser.generated.h index 0361fcdc..564d9ccf 100644 --- a/parser/tau_parser.generated.h +++ b/parser/tau_parser.generated.h @@ -8,7 +8,7 @@ struct tau_parser { tau_parser() : nts(load_nonterminals()), cc(load_cc()), - g(nts, load_prods(), nt(224), cc), p(g, load_opts()) {} + g(nts, load_prods(), nt(225), cc), p(g, load_opts()) {} std::unique_ptr::pforest> parse( const char* data, size_t size = 0, size_t max_l = 0, char eof = std::char_traits::eof()) @@ -37,24 +37,24 @@ struct tau_parser { _Rchars_4, _Rchars_5, char_class, digits, _Rdigits_6, _Rdigits_7, definition, dot, open_parenthesis, close_parenthesis, open_bracket, close_bracket, open_brace, close_brace, minus, colon, semicolon, less, comma, sym, offsets, step, offset, _Roffsets_8, _Roffsets_9, num, capture, shift, timed_offset, timed_step, - timed_capture, timed_shift, variable, var, timed, in, out, _Rtimed_10, tau_rule, tau_matcher, - tau_body, tau, tau_collapse_positives_cb, tau_positives_upwards_cb, wff, tau_and, tau_or, tau_neg, tau_t, tau_f, - tau_and_sym, tau_or_sym, tau_neg_sym, wff_rule, wff_matcher, wff_body, wff_rec_relation, wff_ref, bf_eq_cb, bf_neq_cb, - wff_has_clashing_subformulas_cb, wff_has_subformula_cb, wff_remove_existential_cb, wff_remove_bexistential_cb, wff_remove_buniversal_cb, wff_and, wff_neg, wff_xor, wff_conditional, wff_or, - wff_all, wff_ex, wff_imply, wff_equiv, wff_t, wff_f, wff_ball, wff_bex, bf_eq, bf_neq, - bf_less, bf_less_equal, bf_greater, wff_ref_args, _Rwff_ref_args_11, _Rwff_ref_args_12, wff_and_sym, wff_or_sym, wff_xor_sym, wff_conditional_sym, - wff_neg_sym, wff_imply_sym, wff_equiv_sym, wff_all_sym, _Rwff_all_13, wff_ex_sym, _Rwff_ex_14, wff_ball_sym, _Rwff_ball_15, wff_bex_sym, - _Rwff_bex_16, bf, bf_equality_sym, bf_nequality_sym, bf_less_sym, bf_less_equal_sym, bf_greater_sym, bf_rule, bf_matcher, bf_body, - bf_rec_relation, bf_ref, bf_is_zero_cb, bf_is_one_cb, bf_has_clashing_subformulas_cb, bf_has_subformula_cb, bf_constant, bf_and, bf_neg, bf_xor, - bf_or, bf_all, bf_ex, bf_subs_cb, bf_t, bf_f, bf_ref_args, _Rbf_ref_args_17, _Rbf_ref_args_18, bf_and_sym, - bf_or_sym, bf_xor_sym, bf_neg_sym, bf_all_sym, _Rbf_all_19, bf_ex_sym, _Rbf_ex_20, constant, binding, bf_and_cb, - bf_or_cb, bf_xor_cb, bf_neg_cb, source_binding, named_binding, type, source, source0, _Rsource_21, _Rsource_22, - bf_cb_arg, bf_and_cb_sym, bf_or_cb_sym, bf_xor_cb_sym, bf_neg_cb_sym, bf_subs_cb_sym, bf_eq_cb_sym, wff_cb_arg, bf_neq_cb_sym, bf_is_zero_cb_sym, - bf_is_one_cb_sym, bf_has_clashing_subformulas_cb_sym, wff_has_clashing_subformulas_cb_sym, bf_has_subformula_cb_sym, wff_has_subformula_cb_sym, wff_remove_existential_cb_sym, wff_remove_bexistential_cb_sym, wff_remove_buniversal_cb_sym, tau_collapse_positives_cb_sym, tau_cb_arg, - _Rtau_collapse_positives_cb_23, _Rtau_collapse_positives_cb_24, tau_positives_upwards_cb_sym, input, inputs, _Rinputs_25, _Rinputs_26, main, rule, rules, - _Rrules_27, _Rrules_28, rec_relation, rec_relations, _Rrec_relations_29, _Rrec_relations_30, formula, library, builder, builder_head, - builder_body, _Rbuilder_head_31, _Rbuilder_head_32, gssotc, start, __neg_0, __neg_1, __neg_2, __neg_3, __neg_4, - __neg_5, + timed_capture, timed_shift, variable, var, timed, in, out, _Rtimed_10, bool_variable, tau_rule, + tau_matcher, tau_body, tau, tau_collapse_positives_cb, tau_positives_upwards_cb, wff, tau_and, tau_or, tau_neg, tau_t, + tau_f, tau_and_sym, tau_or_sym, tau_neg_sym, wff_rule, wff_matcher, wff_body, wff_rec_relation, wff_ref, bf_eq_cb, + bf_neq_cb, wff_has_clashing_subformulas_cb, wff_has_subformula_cb, wff_remove_existential_cb, wff_remove_bexistential_cb, wff_remove_buniversal_cb, wff_and, wff_neg, wff_xor, wff_conditional, + wff_or, wff_all, wff_ex, wff_imply, wff_equiv, wff_t, wff_f, wff_ball, wff_bex, bf_eq, + bf_neq, bf_less, bf_less_equal, bf_greater, wff_ref_args, _Rwff_ref_args_11, _Rwff_ref_args_12, wff_and_sym, wff_or_sym, wff_xor_sym, + wff_conditional_sym, wff_neg_sym, wff_imply_sym, wff_equiv_sym, wff_all_sym, _Rwff_all_13, wff_ex_sym, _Rwff_ex_14, wff_ball_sym, _Rwff_ball_15, + wff_bex_sym, _Rwff_bex_16, bf, bf_equality_sym, bf_nequality_sym, bf_less_sym, bf_less_equal_sym, bf_greater_sym, bf_rule, bf_matcher, + bf_body, bf_rec_relation, bf_ref, bf_is_zero_cb, bf_is_one_cb, bf_has_clashing_subformulas_cb, bf_has_subformula_cb, bf_constant, bf_and, bf_neg, + bf_xor, bf_or, bf_all, bf_ex, bf_subs_cb, bf_t, bf_f, bf_ref_args, _Rbf_ref_args_17, _Rbf_ref_args_18, + bf_and_sym, bf_or_sym, bf_xor_sym, bf_neg_sym, bf_all_sym, _Rbf_all_19, bf_ex_sym, _Rbf_ex_20, constant, binding, + bf_and_cb, bf_or_cb, bf_xor_cb, bf_neg_cb, source_binding, named_binding, type, source, source0, _Rsource_21, + _Rsource_22, bf_cb_arg, bf_and_cb_sym, bf_or_cb_sym, bf_xor_cb_sym, bf_neg_cb_sym, bf_subs_cb_sym, bf_eq_cb_sym, wff_cb_arg, bf_neq_cb_sym, + bf_is_zero_cb_sym, bf_is_one_cb_sym, bf_has_clashing_subformulas_cb_sym, wff_has_clashing_subformulas_cb_sym, bf_has_subformula_cb_sym, wff_has_subformula_cb_sym, wff_remove_existential_cb_sym, wff_remove_bexistential_cb_sym, wff_remove_buniversal_cb_sym, tau_collapse_positives_cb_sym, + tau_cb_arg, _Rtau_collapse_positives_cb_23, _Rtau_collapse_positives_cb_24, tau_positives_upwards_cb_sym, input, inputs, _Rinputs_25, _Rinputs_26, main, rule, + rules, _Rrules_27, _Rrules_28, rec_relation, rec_relations, _Rrec_relations_29, _Rrec_relations_30, formula, library, builder, + builder_head, builder_body, _Rbuilder_head_31, _Rbuilder_head_32, gssotc, start, __neg_0, __neg_1, __neg_2, __neg_3, + __neg_4, __neg_5, }; size_t id(const std::basic_string& name) { return nts.get(name); } private: @@ -63,7 +63,7 @@ struct tau_parser { '`', 'a', 'l', 'n', 'm', 'p', 'h', 'b', 'k', 'c', 't', 'r', 'd', 'i', 'g', 'e', 'o', 'f', 'w', 's', ':', '=', '.', '(', ')', '[', ']', '{', '}', '-', - ';', '<', ',', '$', '?', '_', 'T', 'F', '&', '|', + ';', '<', ',', '?', '$', '_', 'T', 'F', '&', '|', '%', '^', '!', '>', '+', '~', '1', '0', 'v', 'q', 'z', }; @@ -86,24 +86,24 @@ struct tau_parser { "_Rchars_4", "_Rchars_5", "char_class", "digits", "_Rdigits_6", "_Rdigits_7", "definition", "dot", "open_parenthesis", "close_parenthesis", "open_bracket", "close_bracket", "open_brace", "close_brace", "minus", "colon", "semicolon", "less", "comma", "sym", "offsets", "step", "offset", "_Roffsets_8", "_Roffsets_9", "num", "capture", "shift", "timed_offset", "timed_step", - "timed_capture", "timed_shift", "variable", "var", "timed", "in", "out", "_Rtimed_10", "tau_rule", "tau_matcher", - "tau_body", "tau", "tau_collapse_positives_cb", "tau_positives_upwards_cb", "wff", "tau_and", "tau_or", "tau_neg", "tau_t", "tau_f", - "tau_and_sym", "tau_or_sym", "tau_neg_sym", "wff_rule", "wff_matcher", "wff_body", "wff_rec_relation", "wff_ref", "bf_eq_cb", "bf_neq_cb", - "wff_has_clashing_subformulas_cb", "wff_has_subformula_cb", "wff_remove_existential_cb", "wff_remove_bexistential_cb", "wff_remove_buniversal_cb", "wff_and", "wff_neg", "wff_xor", "wff_conditional", "wff_or", - "wff_all", "wff_ex", "wff_imply", "wff_equiv", "wff_t", "wff_f", "wff_ball", "wff_bex", "bf_eq", "bf_neq", - "bf_less", "bf_less_equal", "bf_greater", "wff_ref_args", "_Rwff_ref_args_11", "_Rwff_ref_args_12", "wff_and_sym", "wff_or_sym", "wff_xor_sym", "wff_conditional_sym", - "wff_neg_sym", "wff_imply_sym", "wff_equiv_sym", "wff_all_sym", "_Rwff_all_13", "wff_ex_sym", "_Rwff_ex_14", "wff_ball_sym", "_Rwff_ball_15", "wff_bex_sym", - "_Rwff_bex_16", "bf", "bf_equality_sym", "bf_nequality_sym", "bf_less_sym", "bf_less_equal_sym", "bf_greater_sym", "bf_rule", "bf_matcher", "bf_body", - "bf_rec_relation", "bf_ref", "bf_is_zero_cb", "bf_is_one_cb", "bf_has_clashing_subformulas_cb", "bf_has_subformula_cb", "bf_constant", "bf_and", "bf_neg", "bf_xor", - "bf_or", "bf_all", "bf_ex", "bf_subs_cb", "bf_t", "bf_f", "bf_ref_args", "_Rbf_ref_args_17", "_Rbf_ref_args_18", "bf_and_sym", - "bf_or_sym", "bf_xor_sym", "bf_neg_sym", "bf_all_sym", "_Rbf_all_19", "bf_ex_sym", "_Rbf_ex_20", "constant", "binding", "bf_and_cb", - "bf_or_cb", "bf_xor_cb", "bf_neg_cb", "source_binding", "named_binding", "type", "source", "source0", "_Rsource_21", "_Rsource_22", - "bf_cb_arg", "bf_and_cb_sym", "bf_or_cb_sym", "bf_xor_cb_sym", "bf_neg_cb_sym", "bf_subs_cb_sym", "bf_eq_cb_sym", "wff_cb_arg", "bf_neq_cb_sym", "bf_is_zero_cb_sym", - "bf_is_one_cb_sym", "bf_has_clashing_subformulas_cb_sym", "wff_has_clashing_subformulas_cb_sym", "bf_has_subformula_cb_sym", "wff_has_subformula_cb_sym", "wff_remove_existential_cb_sym", "wff_remove_bexistential_cb_sym", "wff_remove_buniversal_cb_sym", "tau_collapse_positives_cb_sym", "tau_cb_arg", - "_Rtau_collapse_positives_cb_23", "_Rtau_collapse_positives_cb_24", "tau_positives_upwards_cb_sym", "input", "inputs", "_Rinputs_25", "_Rinputs_26", "main", "rule", "rules", - "_Rrules_27", "_Rrules_28", "rec_relation", "rec_relations", "_Rrec_relations_29", "_Rrec_relations_30", "formula", "library", "builder", "builder_head", - "builder_body", "_Rbuilder_head_31", "_Rbuilder_head_32", "gssotc", "start", "__neg_0", "__neg_1", "__neg_2", "__neg_3", "__neg_4", - "__neg_5", + "timed_capture", "timed_shift", "variable", "var", "timed", "in", "out", "_Rtimed_10", "bool_variable", "tau_rule", + "tau_matcher", "tau_body", "tau", "tau_collapse_positives_cb", "tau_positives_upwards_cb", "wff", "tau_and", "tau_or", "tau_neg", "tau_t", + "tau_f", "tau_and_sym", "tau_or_sym", "tau_neg_sym", "wff_rule", "wff_matcher", "wff_body", "wff_rec_relation", "wff_ref", "bf_eq_cb", + "bf_neq_cb", "wff_has_clashing_subformulas_cb", "wff_has_subformula_cb", "wff_remove_existential_cb", "wff_remove_bexistential_cb", "wff_remove_buniversal_cb", "wff_and", "wff_neg", "wff_xor", "wff_conditional", + "wff_or", "wff_all", "wff_ex", "wff_imply", "wff_equiv", "wff_t", "wff_f", "wff_ball", "wff_bex", "bf_eq", + "bf_neq", "bf_less", "bf_less_equal", "bf_greater", "wff_ref_args", "_Rwff_ref_args_11", "_Rwff_ref_args_12", "wff_and_sym", "wff_or_sym", "wff_xor_sym", + "wff_conditional_sym", "wff_neg_sym", "wff_imply_sym", "wff_equiv_sym", "wff_all_sym", "_Rwff_all_13", "wff_ex_sym", "_Rwff_ex_14", "wff_ball_sym", "_Rwff_ball_15", + "wff_bex_sym", "_Rwff_bex_16", "bf", "bf_equality_sym", "bf_nequality_sym", "bf_less_sym", "bf_less_equal_sym", "bf_greater_sym", "bf_rule", "bf_matcher", + "bf_body", "bf_rec_relation", "bf_ref", "bf_is_zero_cb", "bf_is_one_cb", "bf_has_clashing_subformulas_cb", "bf_has_subformula_cb", "bf_constant", "bf_and", "bf_neg", + "bf_xor", "bf_or", "bf_all", "bf_ex", "bf_subs_cb", "bf_t", "bf_f", "bf_ref_args", "_Rbf_ref_args_17", "_Rbf_ref_args_18", + "bf_and_sym", "bf_or_sym", "bf_xor_sym", "bf_neg_sym", "bf_all_sym", "_Rbf_all_19", "bf_ex_sym", "_Rbf_ex_20", "constant", "binding", + "bf_and_cb", "bf_or_cb", "bf_xor_cb", "bf_neg_cb", "source_binding", "named_binding", "type", "source", "source0", "_Rsource_21", + "_Rsource_22", "bf_cb_arg", "bf_and_cb_sym", "bf_or_cb_sym", "bf_xor_cb_sym", "bf_neg_cb_sym", "bf_subs_cb_sym", "bf_eq_cb_sym", "wff_cb_arg", "bf_neq_cb_sym", + "bf_is_zero_cb_sym", "bf_is_one_cb_sym", "bf_has_clashing_subformulas_cb_sym", "wff_has_clashing_subformulas_cb_sym", "bf_has_subformula_cb_sym", "wff_has_subformula_cb_sym", "wff_remove_existential_cb_sym", "wff_remove_bexistential_cb_sym", "wff_remove_buniversal_cb_sym", "tau_collapse_positives_cb_sym", + "tau_cb_arg", "_Rtau_collapse_positives_cb_23", "_Rtau_collapse_positives_cb_24", "tau_positives_upwards_cb_sym", "input", "inputs", "_Rinputs_25", "_Rinputs_26", "main", "rule", + "rules", "_Rrules_27", "_Rrules_28", "rec_relation", "rec_relations", "_Rrec_relations_29", "_Rrec_relations_30", "formula", "library", "builder", + "builder_head", "builder_body", "_Rbuilder_head_31", "_Rbuilder_head_32", "gssotc", "start", "__neg_0", "__neg_1", "__neg_2", "__neg_3", + "__neg_4", "__neg_5", }) nts.get(nt); return nts; } @@ -170,19 +170,19 @@ struct tau_parser { // _Rchar_punct_3 => esc q_bqstr. q(nt(24), (nt(17)+nt(20))); // __neg_0 => q_char. - q(nt(225), (nt(18))); + q(nt(226), (nt(18))); // __neg_1 => q_str. - q(nt(226), (nt(19))); + q(nt(227), (nt(19))); // __neg_2 => q_bqstr. - q(nt(227), (nt(20))); + q(nt(228), (nt(20))); // __neg_3 => _Rchar_punct_1. - q(nt(228), (nt(22))); + q(nt(229), (nt(22))); // __neg_4 => _Rchar_punct_2. - q(nt(229), (nt(23))); + q(nt(230), (nt(23))); // __neg_5 => _Rchar_punct_3. - q(nt(230), (nt(24))); + q(nt(231), (nt(24))); // char_punct => punct & ~( __neg_0 ) & ~( __neg_1 ) & ~( __neg_2 ) & ~( __neg_3 ) & ~( __neg_4 ) & ~( __neg_5 ). - q(nt(21), (nt(7)) & ~(nt(225)) & ~(nt(226)) & ~(nt(227)) & ~(nt(228)) & ~(nt(229)) & ~(nt(230))); + q(nt(21), (nt(7)) & ~(nt(226)) & ~(nt(227)) & ~(nt(228)) & ~(nt(229)) & ~(nt(230)) & ~(nt(231))); // char0 => space. q(nt(25), (nt(2))); // char0 => alnum. @@ -331,504 +331,506 @@ struct tau_parser { q(nt(67), (nt(66))); // timed => _Rtimed_10 timed_offset. q(nt(64), (nt(67)+nt(58))); + // bool_variable => '?' chars. + q(nt(68), (t(42)+nt(29))); // capture => '$' chars. - q(nt(56), (t(42)+nt(29))); + q(nt(56), (t(43)+nt(29))); // var => chars. q(nt(63), (nt(29))); // in => '?' 'i' '_' chars. - q(nt(65), (t(43)+t(22)+t(44)+nt(29))); + q(nt(65), (t(42)+t(22)+t(44)+nt(29))); // out => '?' 'o' '_' chars. - q(nt(66), (t(43)+t(25)+t(44)+nt(29))); + q(nt(66), (t(42)+t(25)+t(44)+nt(29))); // tau_rule => tau_matcher definition tau_body dot. - q(nt(68), (nt(69)+nt(36)+nt(70)+nt(37))); + q(nt(69), (nt(70)+nt(36)+nt(71)+nt(37))); // tau_matcher => tau. - q(nt(69), (nt(71))); + q(nt(70), (nt(72))); // tau_body => tau. - q(nt(70), (nt(71))); + q(nt(71), (nt(72))); // tau_body => tau_collapse_positives_cb. - q(nt(70), (nt(72))); + q(nt(71), (nt(73))); // tau_body => tau_positives_upwards_cb. - q(nt(70), (nt(73))); + q(nt(71), (nt(74))); // tau => capture. - q(nt(71), (nt(56))); + q(nt(72), (nt(56))); // tau => wff. - q(nt(71), (nt(74))); + q(nt(72), (nt(75))); // tau => tau_and. - q(nt(71), (nt(75))); + q(nt(72), (nt(76))); // tau => tau_or. - q(nt(71), (nt(76))); + q(nt(72), (nt(77))); // tau => tau_neg. - q(nt(71), (nt(77))); + q(nt(72), (nt(78))); // tau => tau_t. - q(nt(71), (nt(78))); + q(nt(72), (nt(79))); // tau => tau_f. - q(nt(71), (nt(79))); + q(nt(72), (nt(80))); // tau_and => open_parenthesis tau tau_and_sym tau close_parenthesis. - q(nt(75), (nt(38)+nt(71)+nt(80)+nt(71)+nt(39))); + q(nt(76), (nt(38)+nt(72)+nt(81)+nt(72)+nt(39))); // tau_or => open_parenthesis tau tau_or_sym tau close_parenthesis. - q(nt(76), (nt(38)+nt(71)+nt(81)+nt(71)+nt(39))); + q(nt(77), (nt(38)+nt(72)+nt(82)+nt(72)+nt(39))); // tau_neg => tau_neg_sym tau. - q(nt(77), (nt(82)+nt(71))); + q(nt(78), (nt(83)+nt(72))); // tau_t => ws 'T' ws. - q(nt(78), (nt(13)+t(45)+nt(13))); + q(nt(79), (nt(13)+t(45)+nt(13))); // tau_f => ws 'F' ws. - q(nt(79), (nt(13)+t(46)+nt(13))); + q(nt(80), (nt(13)+t(46)+nt(13))); // tau_and_sym => ws '&' '&' '&' ws. - q(nt(80), (nt(13)+t(47)+t(47)+t(47)+nt(13))); + q(nt(81), (nt(13)+t(47)+t(47)+t(47)+nt(13))); // tau_or_sym => ws '|' '|' '|' ws. - q(nt(81), (nt(13)+t(48)+t(48)+t(48)+nt(13))); + q(nt(82), (nt(13)+t(48)+t(48)+t(48)+nt(13))); // tau_neg_sym => ws '%' ws. - q(nt(82), (nt(13)+t(49)+nt(13))); + q(nt(83), (nt(13)+t(49)+nt(13))); // wff_rule => wff_matcher definition wff_body dot. - q(nt(83), (nt(84)+nt(36)+nt(85)+nt(37))); + q(nt(84), (nt(85)+nt(36)+nt(86)+nt(37))); // wff_rec_relation => wff_ref definition wff dot. - q(nt(86), (nt(87)+nt(36)+nt(74)+nt(37))); + q(nt(87), (nt(88)+nt(36)+nt(75)+nt(37))); // wff_matcher => wff. - q(nt(84), (nt(74))); + q(nt(85), (nt(75))); // wff_matcher => wff_ref. - q(nt(84), (nt(87))); + q(nt(85), (nt(88))); // wff_body => wff. - q(nt(85), (nt(74))); + q(nt(86), (nt(75))); // wff_body => bf_eq_cb. - q(nt(85), (nt(88))); + q(nt(86), (nt(89))); // wff_body => bf_neq_cb. - q(nt(85), (nt(89))); + q(nt(86), (nt(90))); // wff_body => wff_has_clashing_subformulas_cb. - q(nt(85), (nt(90))); + q(nt(86), (nt(91))); // wff_body => wff_has_subformula_cb. - q(nt(85), (nt(91))); + q(nt(86), (nt(92))); // wff_body => wff_remove_existential_cb. - q(nt(85), (nt(92))); + q(nt(86), (nt(93))); // wff_body => wff_remove_bexistential_cb. - q(nt(85), (nt(93))); + q(nt(86), (nt(94))); // wff_body => wff_remove_buniversal_cb. - q(nt(85), (nt(94))); + q(nt(86), (nt(95))); // wff => capture. - q(nt(74), (nt(56))); - // wff => variable. - q(nt(74), (nt(62))); + q(nt(75), (nt(56))); + // wff => bool_variable. + q(nt(75), (nt(68))); // wff => wff_ref. - q(nt(74), (nt(87))); + q(nt(75), (nt(88))); // wff => wff_and. - q(nt(74), (nt(95))); + q(nt(75), (nt(96))); // wff => wff_neg. - q(nt(74), (nt(96))); + q(nt(75), (nt(97))); // wff => wff_xor. - q(nt(74), (nt(97))); + q(nt(75), (nt(98))); // wff => wff_conditional. - q(nt(74), (nt(98))); + q(nt(75), (nt(99))); // wff => wff_or. - q(nt(74), (nt(99))); + q(nt(75), (nt(100))); // wff => wff_all. - q(nt(74), (nt(100))); + q(nt(75), (nt(101))); // wff => wff_ex. - q(nt(74), (nt(101))); + q(nt(75), (nt(102))); // wff => wff_imply. - q(nt(74), (nt(102))); + q(nt(75), (nt(103))); // wff => wff_equiv. - q(nt(74), (nt(103))); + q(nt(75), (nt(104))); // wff => wff_t. - q(nt(74), (nt(104))); + q(nt(75), (nt(105))); // wff => wff_f. - q(nt(74), (nt(105))); + q(nt(75), (nt(106))); // wff => wff_ball. - q(nt(74), (nt(106))); + q(nt(75), (nt(107))); // wff => wff_bex. - q(nt(74), (nt(107))); + q(nt(75), (nt(108))); // wff => bf_eq. - q(nt(74), (nt(108))); + q(nt(75), (nt(109))); // wff => bf_neq. - q(nt(74), (nt(109))); + q(nt(75), (nt(110))); // wff => bf_less. - q(nt(74), (nt(110))); + q(nt(75), (nt(111))); // wff => bf_less_equal. - q(nt(74), (nt(111))); + q(nt(75), (nt(112))); // wff => bf_greater. - q(nt(74), (nt(112))); + q(nt(75), (nt(113))); // wff_ref => sym offsets wff_ref_args. - q(nt(87), (nt(49)+nt(50)+nt(113))); + q(nt(88), (nt(49)+nt(50)+nt(114))); // _Rwff_ref_args_11 => variable. - q(nt(114), (nt(62))); + q(nt(115), (nt(62))); // _Rwff_ref_args_12 => null. - q(nt(115), (nul)); + q(nt(116), (nul)); // _Rwff_ref_args_12 => _Rwff_ref_args_11 _Rwff_ref_args_12. - q(nt(115), (nt(114)+nt(115))); + q(nt(116), (nt(115)+nt(116))); // wff_ref_args => open_parenthesis _Rwff_ref_args_12 close_parenthesis. - q(nt(113), (nt(38)+nt(115)+nt(39))); + q(nt(114), (nt(38)+nt(116)+nt(39))); // wff_and => open_parenthesis wff wff_and_sym wff close_parenthesis. - q(nt(95), (nt(38)+nt(74)+nt(116)+nt(74)+nt(39))); + q(nt(96), (nt(38)+nt(75)+nt(117)+nt(75)+nt(39))); // wff_or => open_parenthesis wff wff_or_sym wff close_parenthesis. - q(nt(99), (nt(38)+nt(74)+nt(117)+nt(74)+nt(39))); + q(nt(100), (nt(38)+nt(75)+nt(118)+nt(75)+nt(39))); // wff_xor => open_parenthesis wff wff_xor_sym wff close_parenthesis. - q(nt(97), (nt(38)+nt(74)+nt(118)+nt(74)+nt(39))); + q(nt(98), (nt(38)+nt(75)+nt(119)+nt(75)+nt(39))); // wff_conditional => open_parenthesis wff wff_conditional_sym wff colon wff close_parenthesis. - q(nt(98), (nt(38)+nt(74)+nt(119)+nt(74)+nt(45)+nt(74)+nt(39))); + q(nt(99), (nt(38)+nt(75)+nt(120)+nt(75)+nt(45)+nt(75)+nt(39))); // wff_neg => wff_neg_sym wff. - q(nt(96), (nt(120)+nt(74))); + q(nt(97), (nt(121)+nt(75))); // wff_imply => open_parenthesis wff wff_imply_sym wff close_parenthesis. - q(nt(102), (nt(38)+nt(74)+nt(121)+nt(74)+nt(39))); + q(nt(103), (nt(38)+nt(75)+nt(122)+nt(75)+nt(39))); // wff_equiv => open_parenthesis wff wff_equiv_sym wff close_parenthesis. - q(nt(103), (nt(38)+nt(74)+nt(122)+nt(74)+nt(39))); + q(nt(104), (nt(38)+nt(75)+nt(123)+nt(75)+nt(39))); // _Rwff_all_13 => capture. - q(nt(124), (nt(56))); + q(nt(125), (nt(56))); // _Rwff_all_13 => variable. - q(nt(124), (nt(62))); + q(nt(125), (nt(62))); // wff_all => wff_all_sym ws_required _Rwff_all_13 ws_required wff. - q(nt(100), (nt(123)+nt(12)+nt(124)+nt(12)+nt(74))); + q(nt(101), (nt(124)+nt(12)+nt(125)+nt(12)+nt(75))); // _Rwff_ex_14 => capture. - q(nt(126), (nt(56))); + q(nt(127), (nt(56))); // _Rwff_ex_14 => variable. - q(nt(126), (nt(62))); + q(nt(127), (nt(62))); // wff_ex => wff_ex_sym ws_required _Rwff_ex_14 ws_required wff. - q(nt(101), (nt(125)+nt(12)+nt(126)+nt(12)+nt(74))); + q(nt(102), (nt(126)+nt(12)+nt(127)+nt(12)+nt(75))); // _Rwff_ball_15 => capture. - q(nt(128), (nt(56))); - // _Rwff_ball_15 => variable. - q(nt(128), (nt(62))); + q(nt(129), (nt(56))); + // _Rwff_ball_15 => bool_variable. + q(nt(129), (nt(68))); // wff_ball => wff_ball_sym ws_required _Rwff_ball_15 ws_required wff. - q(nt(106), (nt(127)+nt(12)+nt(128)+nt(12)+nt(74))); + q(nt(107), (nt(128)+nt(12)+nt(129)+nt(12)+nt(75))); // _Rwff_bex_16 => capture. - q(nt(130), (nt(56))); - // _Rwff_bex_16 => variable. - q(nt(130), (nt(62))); + q(nt(131), (nt(56))); + // _Rwff_bex_16 => bool_variable. + q(nt(131), (nt(68))); // wff_bex => wff_bex_sym ws_required _Rwff_bex_16 ws_required wff. - q(nt(107), (nt(129)+nt(12)+nt(130)+nt(12)+nt(74))); + q(nt(108), (nt(130)+nt(12)+nt(131)+nt(12)+nt(75))); // bf_eq => open_parenthesis bf bf_equality_sym bf close_parenthesis. - q(nt(108), (nt(38)+nt(131)+nt(132)+nt(131)+nt(39))); + q(nt(109), (nt(38)+nt(132)+nt(133)+nt(132)+nt(39))); // bf_neq => open_parenthesis bf bf_nequality_sym bf close_parenthesis. - q(nt(109), (nt(38)+nt(131)+nt(133)+nt(131)+nt(39))); + q(nt(110), (nt(38)+nt(132)+nt(134)+nt(132)+nt(39))); // bf_less => open_parenthesis bf bf_less_sym bf close_parenthesis. - q(nt(110), (nt(38)+nt(131)+nt(134)+nt(131)+nt(39))); + q(nt(111), (nt(38)+nt(132)+nt(135)+nt(132)+nt(39))); // bf_less_equal => open_parenthesis bf bf_less_equal_sym bf close_parenthesis. - q(nt(111), (nt(38)+nt(131)+nt(135)+nt(131)+nt(39))); + q(nt(112), (nt(38)+nt(132)+nt(136)+nt(132)+nt(39))); // bf_greater => open_parenthesis bf bf_greater_sym bf close_parenthesis. - q(nt(112), (nt(38)+nt(131)+nt(136)+nt(131)+nt(39))); + q(nt(113), (nt(38)+nt(132)+nt(137)+nt(132)+nt(39))); // wff_and_sym => ws '&' '&' ws. - q(nt(116), (nt(13)+t(47)+t(47)+nt(13))); + q(nt(117), (nt(13)+t(47)+t(47)+nt(13))); // wff_or_sym => ws '|' '|' ws. - q(nt(117), (nt(13)+t(48)+t(48)+nt(13))); + q(nt(118), (nt(13)+t(48)+t(48)+nt(13))); // wff_xor_sym => ws '^' ws. - q(nt(118), (nt(13)+t(50)+nt(13))); + q(nt(119), (nt(13)+t(50)+nt(13))); // wff_conditional_sym => ws '?' ws. - q(nt(119), (nt(13)+t(43)+nt(13))); + q(nt(120), (nt(13)+t(42)+nt(13))); // wff_neg_sym => ws '!' ws. - q(nt(120), (nt(13)+t(51)+nt(13))); + q(nt(121), (nt(13)+t(51)+nt(13))); // wff_imply_sym => ws '-' '>' ws. - q(nt(121), (nt(13)+t(38)+t(52)+nt(13))); + q(nt(122), (nt(13)+t(38)+t(52)+nt(13))); // wff_equiv_sym => ws '<' '-' '>' ws. - q(nt(122), (nt(13)+t(40)+t(38)+t(52)+nt(13))); + q(nt(123), (nt(13)+t(40)+t(38)+t(52)+nt(13))); // wff_all_sym => ws 'a' 'l' 'l' ws. - q(nt(123), (nt(13)+t(10)+t(11)+t(11)+nt(13))); + q(nt(124), (nt(13)+t(10)+t(11)+t(11)+nt(13))); // wff_ex_sym => ws 'e' 'x' ws. - q(nt(125), (nt(13)+t(24)+t(5)+nt(13))); + q(nt(126), (nt(13)+t(24)+t(5)+nt(13))); // wff_ball_sym => ws 'b' 'a' 'l' 'l' ws. - q(nt(127), (nt(13)+t(16)+t(10)+t(11)+t(11)+nt(13))); + q(nt(128), (nt(13)+t(16)+t(10)+t(11)+t(11)+nt(13))); // wff_bex_sym => ws 'b' 'e' 'x' ws. - q(nt(129), (nt(13)+t(16)+t(24)+t(5)+nt(13))); + q(nt(130), (nt(13)+t(16)+t(24)+t(5)+nt(13))); // wff_t => ws 'T' ws. - q(nt(104), (nt(13)+t(45)+nt(13))); + q(nt(105), (nt(13)+t(45)+nt(13))); // wff_f => ws 'F' ws. - q(nt(105), (nt(13)+t(46)+nt(13))); + q(nt(106), (nt(13)+t(46)+nt(13))); // bf_rule => bf_matcher definition bf_body dot. - q(nt(137), (nt(138)+nt(36)+nt(139)+nt(37))); + q(nt(138), (nt(139)+nt(36)+nt(140)+nt(37))); // bf_rec_relation => bf_ref definition bf dot. - q(nt(140), (nt(141)+nt(36)+nt(131)+nt(37))); + q(nt(141), (nt(142)+nt(36)+nt(132)+nt(37))); // bf_matcher => bf. - q(nt(138), (nt(131))); + q(nt(139), (nt(132))); // bf_body => bf. - q(nt(139), (nt(131))); + q(nt(140), (nt(132))); // bf_body => bf_is_zero_cb. - q(nt(139), (nt(142))); + q(nt(140), (nt(143))); // bf_body => bf_is_one_cb. - q(nt(139), (nt(143))); + q(nt(140), (nt(144))); // bf_body => bf_has_clashing_subformulas_cb. - q(nt(139), (nt(144))); + q(nt(140), (nt(145))); // bf_body => bf_has_subformula_cb. - q(nt(139), (nt(145))); + q(nt(140), (nt(146))); // bf => capture. - q(nt(131), (nt(56))); + q(nt(132), (nt(56))); // bf => variable. - q(nt(131), (nt(62))); + q(nt(132), (nt(62))); // bf => bf_ref. - q(nt(131), (nt(141))); + q(nt(132), (nt(142))); // bf => bf_constant. - q(nt(131), (nt(146))); + q(nt(132), (nt(147))); // bf => bf_and. - q(nt(131), (nt(147))); + q(nt(132), (nt(148))); // bf => bf_neg. - q(nt(131), (nt(148))); + q(nt(132), (nt(149))); // bf => bf_xor. - q(nt(131), (nt(149))); + q(nt(132), (nt(150))); // bf => bf_or. - q(nt(131), (nt(150))); + q(nt(132), (nt(151))); // bf => bf_all. - q(nt(131), (nt(151))); + q(nt(132), (nt(152))); // bf => bf_ex. - q(nt(131), (nt(152))); + q(nt(132), (nt(153))); // bf => bf_subs_cb. - q(nt(131), (nt(153))); + q(nt(132), (nt(154))); // bf => bf_t. - q(nt(131), (nt(154))); + q(nt(132), (nt(155))); // bf => bf_f. - q(nt(131), (nt(155))); + q(nt(132), (nt(156))); // bf_ref => sym offsets bf_ref_args. - q(nt(141), (nt(49)+nt(50)+nt(156))); + q(nt(142), (nt(49)+nt(50)+nt(157))); // _Rbf_ref_args_17 => variable. - q(nt(157), (nt(62))); + q(nt(158), (nt(62))); // _Rbf_ref_args_18 => null. - q(nt(158), (nul)); + q(nt(159), (nul)); // _Rbf_ref_args_18 => _Rbf_ref_args_17 _Rbf_ref_args_18. - q(nt(158), (nt(157)+nt(158))); + q(nt(159), (nt(158)+nt(159))); // bf_ref_args => open_parenthesis _Rbf_ref_args_18 close_parenthesis. - q(nt(156), (nt(38)+nt(158)+nt(39))); + q(nt(157), (nt(38)+nt(159)+nt(39))); // bf_and => open_parenthesis bf bf_and_sym bf close_parenthesis. - q(nt(147), (nt(38)+nt(131)+nt(159)+nt(131)+nt(39))); + q(nt(148), (nt(38)+nt(132)+nt(160)+nt(132)+nt(39))); // bf_or => open_parenthesis bf bf_or_sym bf close_parenthesis. - q(nt(150), (nt(38)+nt(131)+nt(160)+nt(131)+nt(39))); + q(nt(151), (nt(38)+nt(132)+nt(161)+nt(132)+nt(39))); // bf_xor => open_parenthesis bf bf_xor_sym ws bf close_parenthesis. - q(nt(149), (nt(38)+nt(131)+nt(161)+nt(13)+nt(131)+nt(39))); + q(nt(150), (nt(38)+nt(132)+nt(162)+nt(13)+nt(132)+nt(39))); // bf_neg => bf_neg_sym bf. - q(nt(148), (nt(162)+nt(131))); + q(nt(149), (nt(163)+nt(132))); // _Rbf_all_19 => capture. - q(nt(164), (nt(56))); + q(nt(165), (nt(56))); // _Rbf_all_19 => variable. - q(nt(164), (nt(62))); + q(nt(165), (nt(62))); // bf_all => bf_all_sym ws_required _Rbf_all_19 ws_required bf. - q(nt(151), (nt(163)+nt(12)+nt(164)+nt(12)+nt(131))); + q(nt(152), (nt(164)+nt(12)+nt(165)+nt(12)+nt(132))); // _Rbf_ex_20 => capture. - q(nt(166), (nt(56))); + q(nt(167), (nt(56))); // _Rbf_ex_20 => variable. - q(nt(166), (nt(62))); + q(nt(167), (nt(62))); // bf_ex => bf_ex_sym ws_required _Rbf_ex_20 ws_required bf. - q(nt(152), (nt(165)+nt(12)+nt(166)+nt(12)+nt(131))); + q(nt(153), (nt(166)+nt(12)+nt(167)+nt(12)+nt(132))); // bf_and_sym => ws '&' ws. - q(nt(159), (nt(13)+t(47)+nt(13))); + q(nt(160), (nt(13)+t(47)+nt(13))); // bf_or_sym => ws '|' ws. - q(nt(160), (nt(13)+t(48)+nt(13))); + q(nt(161), (nt(13)+t(48)+nt(13))); // bf_xor_sym => ws '+' ws. - q(nt(161), (nt(13)+t(53)+nt(13))); + q(nt(162), (nt(13)+t(53)+nt(13))); // bf_neg_sym => ws '~' ws. - q(nt(162), (nt(13)+t(54)+nt(13))); + q(nt(163), (nt(13)+t(54)+nt(13))); // bf_equality_sym => ws '=' ws. - q(nt(132), (nt(13)+t(30)+nt(13))); + q(nt(133), (nt(13)+t(30)+nt(13))); // bf_nequality_sym => ws '!' '=' ws. - q(nt(133), (nt(13)+t(51)+t(30)+nt(13))); + q(nt(134), (nt(13)+t(51)+t(30)+nt(13))); // bf_less_sym => ws '<' ws. - q(nt(134), (nt(13)+t(40)+nt(13))); + q(nt(135), (nt(13)+t(40)+nt(13))); // bf_less_equal_sym => ws '<' '=' ws. - q(nt(135), (nt(13)+t(40)+t(30)+nt(13))); + q(nt(136), (nt(13)+t(40)+t(30)+nt(13))); // bf_greater_sym => ws '>' ws. - q(nt(136), (nt(13)+t(52)+nt(13))); + q(nt(137), (nt(13)+t(52)+nt(13))); // bf_all_sym => ws 'f' 'a' 'l' 'l' ws. - q(nt(163), (nt(13)+t(26)+t(10)+t(11)+t(11)+nt(13))); + q(nt(164), (nt(13)+t(26)+t(10)+t(11)+t(11)+nt(13))); // bf_ex_sym => ws 'f' 'e' 'x' ws. - q(nt(165), (nt(13)+t(26)+t(24)+t(5)+nt(13))); + q(nt(166), (nt(13)+t(26)+t(24)+t(5)+nt(13))); // bf_t => ws '1' ws. - q(nt(154), (nt(13)+t(55)+nt(13))); + q(nt(155), (nt(13)+t(55)+nt(13))); // bf_f => ws '0' ws. - q(nt(155), (nt(13)+t(56)+nt(13))); + q(nt(156), (nt(13)+t(56)+nt(13))); // bf_constant => open_brace constant close_brace. - q(nt(146), (nt(42)+nt(167)+nt(43))); + q(nt(147), (nt(42)+nt(168)+nt(43))); // constant => capture. - q(nt(167), (nt(56))); + q(nt(168), (nt(56))); // constant => binding. - q(nt(167), (nt(168))); + q(nt(168), (nt(169))); // constant => bf_and_cb. - q(nt(167), (nt(169))); + q(nt(168), (nt(170))); // constant => bf_or_cb. - q(nt(167), (nt(170))); + q(nt(168), (nt(171))); // constant => bf_xor_cb. - q(nt(167), (nt(171))); + q(nt(168), (nt(172))); // constant => bf_neg_cb. - q(nt(167), (nt(172))); - // binding => source_binding. q(nt(168), (nt(173))); + // binding => source_binding. + q(nt(169), (nt(174))); // binding => named_binding. - q(nt(168), (nt(174))); + q(nt(169), (nt(175))); // named_binding => chars. - q(nt(174), (nt(29))); + q(nt(175), (nt(29))); // source_binding => type colon source. - q(nt(173), (nt(175)+nt(45)+nt(176))); + q(nt(174), (nt(176)+nt(45)+nt(177))); // type => null. - q(nt(175), (nul)); + q(nt(176), (nul)); // type => chars. - q(nt(175), (nt(29))); + q(nt(176), (nt(29))); // source0 => space. - q(nt(177), (nt(2))); + q(nt(178), (nt(2))); // source0 => alnum. - q(nt(177), (nt(6))); + q(nt(178), (nt(6))); // source0 => char_escape_encode. - q(nt(177), (nt(16))); + q(nt(178), (nt(16))); // source0 => char_punct. - q(nt(177), (nt(21))); + q(nt(178), (nt(21))); // _Rsource_21 => source0. - q(nt(178), (nt(177))); - // _Rsource_22 => _Rsource_21. q(nt(179), (nt(178))); + // _Rsource_22 => _Rsource_21. + q(nt(180), (nt(179))); // _Rsource_22 => _Rsource_21 _Rsource_22. - q(nt(179), (nt(178)+nt(179))); + q(nt(180), (nt(179)+nt(180))); // source => _Rsource_22. - q(nt(176), (nt(179))); + q(nt(177), (nt(180))); // bf_and_cb => bf_cb_arg bf_and_cb_sym bf_cb_arg. - q(nt(169), (nt(180)+nt(181)+nt(180))); + q(nt(170), (nt(181)+nt(182)+nt(181))); // bf_or_cb => bf_cb_arg bf_or_cb_sym bf_cb_arg. - q(nt(170), (nt(180)+nt(182)+nt(180))); + q(nt(171), (nt(181)+nt(183)+nt(181))); // bf_xor_cb => bf_cb_arg bf_xor_cb_sym bf_cb_arg. - q(nt(171), (nt(180)+nt(183)+nt(180))); + q(nt(172), (nt(181)+nt(184)+nt(181))); // bf_neg_cb => bf_neg_cb_sym bf_cb_arg. - q(nt(172), (nt(184)+nt(180))); + q(nt(173), (nt(185)+nt(181))); // bf_subs_cb => bf_subs_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg. - q(nt(153), (nt(185)+nt(180)+nt(12)+nt(180)+nt(12)+nt(180))); + q(nt(154), (nt(186)+nt(181)+nt(12)+nt(181)+nt(12)+nt(181))); // bf_eq_cb => bf_eq_cb_sym bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg. - q(nt(88), (nt(186)+nt(180)+nt(12)+nt(187)+nt(12)+nt(187))); + q(nt(89), (nt(187)+nt(181)+nt(12)+nt(188)+nt(12)+nt(188))); // bf_neq_cb => bf_neq_cb_sym bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg. - q(nt(89), (nt(188)+nt(180)+nt(12)+nt(187)+nt(12)+nt(187))); + q(nt(90), (nt(189)+nt(181)+nt(12)+nt(188)+nt(12)+nt(188))); // bf_is_zero_cb => bf_is_zero_cb_sym bf_cb_arg ws_required bf_cb_arg. - q(nt(142), (nt(189)+nt(180)+nt(12)+nt(180))); + q(nt(143), (nt(190)+nt(181)+nt(12)+nt(181))); // bf_is_one_cb => bf_is_one_cb_sym bf_cb_arg ws_required bf_cb_arg. - q(nt(143), (nt(190)+nt(180)+nt(12)+nt(180))); + q(nt(144), (nt(191)+nt(181)+nt(12)+nt(181))); // bf_has_clashing_subformulas_cb => bf_has_clashing_subformulas_cb_sym bf_cb_arg ws_required bf_cb_arg. - q(nt(144), (nt(191)+nt(180)+nt(12)+nt(180))); + q(nt(145), (nt(192)+nt(181)+nt(12)+nt(181))); // wff_has_clashing_subformulas_cb => wff_has_clashing_subformulas_cb_sym wff_cb_arg ws_required wff_cb_arg. - q(nt(90), (nt(192)+nt(187)+nt(12)+nt(187))); + q(nt(91), (nt(193)+nt(188)+nt(12)+nt(188))); // bf_has_subformula_cb => bf_has_subformula_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg. - q(nt(145), (nt(193)+nt(180)+nt(12)+nt(180)+nt(12)+nt(180))); + q(nt(146), (nt(194)+nt(181)+nt(12)+nt(181)+nt(12)+nt(181))); // wff_has_subformula_cb => wff_has_subformula_cb_sym wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg. - q(nt(91), (nt(194)+nt(187)+nt(12)+nt(187)+nt(12)+nt(187))); + q(nt(92), (nt(195)+nt(188)+nt(12)+nt(188)+nt(12)+nt(188))); // wff_remove_existential_cb => wff_remove_existential_cb_sym wff_cb_arg ws_required wff_cb_arg. - q(nt(92), (nt(195)+nt(187)+nt(12)+nt(187))); + q(nt(93), (nt(196)+nt(188)+nt(12)+nt(188))); // wff_remove_bexistential_cb => wff_remove_bexistential_cb_sym wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg. - q(nt(93), (nt(196)+nt(187)+nt(12)+nt(187)+nt(12)+nt(187)+nt(12)+nt(187))); + q(nt(94), (nt(197)+nt(188)+nt(12)+nt(188)+nt(12)+nt(188)+nt(12)+nt(188))); // wff_remove_buniversal_cb => wff_remove_buniversal_cb_sym wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg. - q(nt(94), (nt(197)+nt(187)+nt(12)+nt(187)+nt(12)+nt(187)+nt(12)+nt(187))); + q(nt(95), (nt(198)+nt(188)+nt(12)+nt(188)+nt(12)+nt(188)+nt(12)+nt(188))); // bf_has_clashing_subformulas_cb_sym => ws 'b' 'f' '_' 'h' 'a' 's' '_' 'c' 'l' 'a' 's' 'h' 'i' 'n' 'g' '_' 's' 'u' 'b' 'f' 'o' 'r' 'm' 'u' 'l' 'a' 's' '_' 'c' 'b' ws. - q(nt(191), (nt(13)+t(16)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(18)+t(11)+t(10)+t(28)+t(15)+t(22)+t(12)+t(23)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(28)+t(44)+t(18)+t(16)+nt(13))); + q(nt(192), (nt(13)+t(16)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(18)+t(11)+t(10)+t(28)+t(15)+t(22)+t(12)+t(23)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(28)+t(44)+t(18)+t(16)+nt(13))); // bf_has_subformula_cb_sym => ws 'b' 'f' '_' 'h' 'a' 's' '_' 's' 'u' 'b' 'f' 'o' 'r' 'm' 'u' 'l' 'a' '_' 'c' 'b' ws. - q(nt(193), (nt(13)+t(16)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(44)+t(18)+t(16)+nt(13))); + q(nt(194), (nt(13)+t(16)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(44)+t(18)+t(16)+nt(13))); // wff_has_clashing_subformulas_cb_sym => ws 'w' 'f' 'f' '_' 'h' 'a' 's' '_' 'c' 'l' 'a' 's' 'h' 'i' 'n' 'g' '_' 's' 'u' 'b' 'f' 'o' 'r' 'm' 'u' 'l' 'a' 's' '_' 'c' 'b' ws. - q(nt(192), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(18)+t(11)+t(10)+t(28)+t(15)+t(22)+t(12)+t(23)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(28)+t(44)+t(18)+t(16)+nt(13))); + q(nt(193), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(18)+t(11)+t(10)+t(28)+t(15)+t(22)+t(12)+t(23)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(28)+t(44)+t(18)+t(16)+nt(13))); // wff_has_subformula_cb_sym => ws 'w' 'f' 'f' '_' 'h' 'a' 's' '_' 's' 'u' 'b' 'f' 'o' 'r' 'm' 'u' 'l' 'a' '_' 'c' 'b' ws. - q(nt(194), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(44)+t(18)+t(16)+nt(13))); + q(nt(195), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(44)+t(18)+t(16)+nt(13))); // wff_remove_existential_cb_sym => ws 'w' 'f' 'f' '_' 'r' 'e' 'm' 'o' 'v' 'e' '_' 'e' 'x' 'i' 's' 't' 'e' 'n' 't' 'i' 'a' 'l' '_' 'c' 'b' ws. - q(nt(195), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(20)+t(24)+t(13)+t(25)+t(57)+t(24)+t(44)+t(24)+t(5)+t(22)+t(28)+t(19)+t(24)+t(12)+t(19)+t(22)+t(10)+t(11)+t(44)+t(18)+t(16)+nt(13))); + q(nt(196), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(20)+t(24)+t(13)+t(25)+t(57)+t(24)+t(44)+t(24)+t(5)+t(22)+t(28)+t(19)+t(24)+t(12)+t(19)+t(22)+t(10)+t(11)+t(44)+t(18)+t(16)+nt(13))); // wff_remove_bexistential_cb_sym => ws 'w' 'f' 'f' '_' 'r' 'e' 'm' 'o' 'v' 'e' '_' 'b' 'e' 'x' 'i' 's' 't' 'e' 'n' 't' 'i' 'a' 'l' '_' 'c' 'b' ws. - q(nt(196), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(20)+t(24)+t(13)+t(25)+t(57)+t(24)+t(44)+t(16)+t(24)+t(5)+t(22)+t(28)+t(19)+t(24)+t(12)+t(19)+t(22)+t(10)+t(11)+t(44)+t(18)+t(16)+nt(13))); + q(nt(197), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(20)+t(24)+t(13)+t(25)+t(57)+t(24)+t(44)+t(16)+t(24)+t(5)+t(22)+t(28)+t(19)+t(24)+t(12)+t(19)+t(22)+t(10)+t(11)+t(44)+t(18)+t(16)+nt(13))); // wff_remove_buniversal_cb_sym => ws 'w' 'f' 'f' '_' 'r' 'e' 'm' 'o' 'v' 'e' '_' 'b' 'u' 'n' 'i' 'v' 'e' 'r' 's' 'a' 'l' '_' 'c' 'b' ws. - q(nt(197), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(20)+t(24)+t(13)+t(25)+t(57)+t(24)+t(44)+t(16)+t(6)+t(12)+t(22)+t(57)+t(24)+t(20)+t(28)+t(10)+t(11)+t(44)+t(18)+t(16)+nt(13))); + q(nt(198), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(20)+t(24)+t(13)+t(25)+t(57)+t(24)+t(44)+t(16)+t(6)+t(12)+t(22)+t(57)+t(24)+t(20)+t(28)+t(10)+t(11)+t(44)+t(18)+t(16)+nt(13))); // bf_cb_arg => capture. - q(nt(180), (nt(56))); + q(nt(181), (nt(56))); // bf_cb_arg => bf. - q(nt(180), (nt(131))); + q(nt(181), (nt(132))); // wff_cb_arg => capture. - q(nt(187), (nt(56))); + q(nt(188), (nt(56))); // wff_cb_arg => wff. - q(nt(187), (nt(74))); + q(nt(188), (nt(75))); // bf_and_cb_sym => ws 'b' 'f' '_' 'a' 'n' 'd' '_' 'c' 'b' ws. - q(nt(181), (nt(13)+t(16)+t(26)+t(44)+t(10)+t(12)+t(21)+t(44)+t(18)+t(16)+nt(13))); + q(nt(182), (nt(13)+t(16)+t(26)+t(44)+t(10)+t(12)+t(21)+t(44)+t(18)+t(16)+nt(13))); // bf_or_cb_sym => ws 'b' 'f' '_' 'o' 'r' '_' 'c' 'b' ws. - q(nt(182), (nt(13)+t(16)+t(26)+t(44)+t(25)+t(20)+t(44)+t(18)+t(16)+nt(13))); + q(nt(183), (nt(13)+t(16)+t(26)+t(44)+t(25)+t(20)+t(44)+t(18)+t(16)+nt(13))); // bf_xor_cb_sym => ws 'b' 'f' '_' 'x' 'o' 'r' '_' 'c' 'b' ws. - q(nt(183), (nt(13)+t(16)+t(26)+t(44)+t(5)+t(25)+t(20)+t(44)+t(18)+t(16)+nt(13))); + q(nt(184), (nt(13)+t(16)+t(26)+t(44)+t(5)+t(25)+t(20)+t(44)+t(18)+t(16)+nt(13))); // bf_neg_cb_sym => ws 'b' 'f' '_' 'n' 'e' 'g' '_' 'c' 'b' ws. - q(nt(184), (nt(13)+t(16)+t(26)+t(44)+t(12)+t(24)+t(23)+t(44)+t(18)+t(16)+nt(13))); + q(nt(185), (nt(13)+t(16)+t(26)+t(44)+t(12)+t(24)+t(23)+t(44)+t(18)+t(16)+nt(13))); // bf_subs_cb_sym => ws 'b' 'f' '_' 's' 'u' 'b' 's' '_' 'c' 'b' ws. - q(nt(185), (nt(13)+t(16)+t(26)+t(44)+t(28)+t(6)+t(16)+t(28)+t(44)+t(18)+t(16)+nt(13))); + q(nt(186), (nt(13)+t(16)+t(26)+t(44)+t(28)+t(6)+t(16)+t(28)+t(44)+t(18)+t(16)+nt(13))); // bf_eq_cb_sym => ws 'b' 'f' '_' 'e' 'q' '_' 'c' 'b' ws. - q(nt(186), (nt(13)+t(16)+t(26)+t(44)+t(24)+t(58)+t(44)+t(18)+t(16)+nt(13))); + q(nt(187), (nt(13)+t(16)+t(26)+t(44)+t(24)+t(58)+t(44)+t(18)+t(16)+nt(13))); // bf_neq_cb_sym => ws 'b' 'f' '_' 'n' 'e' 'q' '_' 'c' 'b' ws. - q(nt(188), (nt(13)+t(16)+t(26)+t(44)+t(12)+t(24)+t(58)+t(44)+t(18)+t(16)+nt(13))); + q(nt(189), (nt(13)+t(16)+t(26)+t(44)+t(12)+t(24)+t(58)+t(44)+t(18)+t(16)+nt(13))); // bf_is_zero_cb_sym => ws 'b' 'f' '_' 'i' 's' '_' 'z' 'e' 'r' 'o' '_' 'c' 'b' ws. - q(nt(189), (nt(13)+t(16)+t(26)+t(44)+t(22)+t(28)+t(44)+t(59)+t(24)+t(20)+t(25)+t(44)+t(18)+t(16)+nt(13))); + q(nt(190), (nt(13)+t(16)+t(26)+t(44)+t(22)+t(28)+t(44)+t(59)+t(24)+t(20)+t(25)+t(44)+t(18)+t(16)+nt(13))); // bf_is_one_cb_sym => ws 'b' 'f' '_' 'i' 's' '_' 'o' 'n' 'e' '_' 'c' 'b' ws. - q(nt(190), (nt(13)+t(16)+t(26)+t(44)+t(22)+t(28)+t(44)+t(25)+t(12)+t(24)+t(44)+t(18)+t(16)+nt(13))); + q(nt(191), (nt(13)+t(16)+t(26)+t(44)+t(22)+t(28)+t(44)+t(25)+t(12)+t(24)+t(44)+t(18)+t(16)+nt(13))); // _Rtau_collapse_positives_cb_23 => tau_collapse_positives_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg ws_required tau_cb_arg. - q(nt(200), (nt(198)+nt(12)+nt(199)+nt(12)+nt(199)+nt(12)+nt(199))); + q(nt(201), (nt(199)+nt(12)+nt(200)+nt(12)+nt(200)+nt(12)+nt(200))); // _Rtau_collapse_positives_cb_24 => tau_collapse_positives_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg. - q(nt(201), (nt(198)+nt(12)+nt(199)+nt(12)+nt(199))); + q(nt(202), (nt(199)+nt(12)+nt(200)+nt(12)+nt(200))); // tau_collapse_positives_cb => _Rtau_collapse_positives_cb_23. - q(nt(72), (nt(200))); + q(nt(73), (nt(201))); // tau_collapse_positives_cb => _Rtau_collapse_positives_cb_24. - q(nt(72), (nt(201))); + q(nt(73), (nt(202))); // tau_positives_upwards_cb => tau_positives_upwards_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg. - q(nt(73), (nt(202)+nt(12)+nt(199)+nt(12)+nt(199))); + q(nt(74), (nt(203)+nt(12)+nt(200)+nt(12)+nt(200))); // tau_cb_arg => capture. - q(nt(199), (nt(56))); + q(nt(200), (nt(56))); // tau_cb_arg => tau. - q(nt(199), (nt(71))); + q(nt(200), (nt(72))); // tau_collapse_positives_cb_sym => ws 't' 'a' 'u' '_' 'c' 'o' 'l' 'l' 'a' 'p' 's' 'e' '_' 'p' 'o' 's' 'i' 't' 'i' 'v' 'e' 's' '_' 'c' 'b' ws. - q(nt(198), (nt(13)+t(19)+t(10)+t(6)+t(44)+t(18)+t(25)+t(11)+t(11)+t(10)+t(14)+t(28)+t(24)+t(44)+t(14)+t(25)+t(28)+t(22)+t(19)+t(22)+t(57)+t(24)+t(28)+t(44)+t(18)+t(16)+nt(13))); + q(nt(199), (nt(13)+t(19)+t(10)+t(6)+t(44)+t(18)+t(25)+t(11)+t(11)+t(10)+t(14)+t(28)+t(24)+t(44)+t(14)+t(25)+t(28)+t(22)+t(19)+t(22)+t(57)+t(24)+t(28)+t(44)+t(18)+t(16)+nt(13))); // tau_positives_upwards_cb_sym => ws 't' 'a' 'u' '_' 'p' 'o' 's' 'i' 't' 'i' 'v' 'e' 's' '_' 'u' 'p' 'w' 'a' 'r' 'd' 's' '_' 'c' 'b' ws. - q(nt(202), (nt(13)+t(19)+t(10)+t(6)+t(44)+t(14)+t(25)+t(28)+t(22)+t(19)+t(22)+t(57)+t(24)+t(28)+t(44)+t(6)+t(14)+t(27)+t(10)+t(20)+t(21)+t(28)+t(44)+t(18)+t(16)+nt(13))); + q(nt(203), (nt(13)+t(19)+t(10)+t(6)+t(44)+t(14)+t(25)+t(28)+t(22)+t(19)+t(22)+t(57)+t(24)+t(28)+t(44)+t(6)+t(14)+t(27)+t(10)+t(20)+t(21)+t(28)+t(44)+t(18)+t(16)+nt(13))); // input => in colon open_brace source_binding close_brace. - q(nt(203), (nt(65)+nt(45)+nt(42)+nt(173)+nt(43))); + q(nt(204), (nt(65)+nt(45)+nt(42)+nt(174)+nt(43))); // _Rinputs_25 => input. - q(nt(205), (nt(203))); + q(nt(206), (nt(204))); // _Rinputs_26 => null. - q(nt(206), (nul)); + q(nt(207), (nul)); // _Rinputs_26 => _Rinputs_25 _Rinputs_26. - q(nt(206), (nt(205)+nt(206))); + q(nt(207), (nt(206)+nt(207))); // inputs => less input _Rinputs_26 dot. - q(nt(204), (nt(47)+nt(203)+nt(206)+nt(37))); + q(nt(205), (nt(47)+nt(204)+nt(207)+nt(37))); // main => wff dot. - q(nt(207), (nt(74)+nt(37))); + q(nt(208), (nt(75)+nt(37))); // rule => tau_rule. - q(nt(208), (nt(68))); + q(nt(209), (nt(69))); // rule => wff_rule. - q(nt(208), (nt(83))); + q(nt(209), (nt(84))); // rule => bf_rule. - q(nt(208), (nt(137))); + q(nt(209), (nt(138))); // _Rrules_27 => rule. - q(nt(210), (nt(208))); + q(nt(211), (nt(209))); // _Rrules_28 => null. - q(nt(211), (nul)); + q(nt(212), (nul)); // _Rrules_28 => _Rrules_27 _Rrules_28. - q(nt(211), (nt(210)+nt(211))); + q(nt(212), (nt(211)+nt(212))); // rules => _Rrules_28. - q(nt(209), (nt(211))); + q(nt(210), (nt(212))); // rec_relation => wff_rec_relation dot. - q(nt(212), (nt(86)+nt(37))); + q(nt(213), (nt(87)+nt(37))); // rec_relation => bf_rec_relation. - q(nt(212), (nt(140))); + q(nt(213), (nt(141))); // _Rrec_relations_29 => rec_relation. - q(nt(214), (nt(212))); + q(nt(215), (nt(213))); // _Rrec_relations_30 => null. - q(nt(215), (nul)); + q(nt(216), (nul)); // _Rrec_relations_30 => _Rrec_relations_29 _Rrec_relations_30. - q(nt(215), (nt(214)+nt(215))); + q(nt(216), (nt(215)+nt(216))); // rec_relations => _Rrec_relations_30. - q(nt(213), (nt(215))); + q(nt(214), (nt(216))); // formula => rec_relations main. - q(nt(216), (nt(213)+nt(207))); + q(nt(217), (nt(214)+nt(208))); // library => rules. - q(nt(217), (nt(209))); + q(nt(218), (nt(210))); // builder => builder_head definition builder_body dot. - q(nt(218), (nt(219)+nt(36)+nt(220)+nt(37))); + q(nt(219), (nt(220)+nt(36)+nt(221)+nt(37))); // _Rbuilder_head_31 => ws_required capture. - q(nt(221), (nt(12)+nt(56))); + q(nt(222), (nt(12)+nt(56))); // _Rbuilder_head_32 => null. - q(nt(222), (nul)); + q(nt(223), (nul)); // _Rbuilder_head_32 => _Rbuilder_head_31 _Rbuilder_head_32. - q(nt(222), (nt(221)+nt(222))); + q(nt(223), (nt(222)+nt(223))); // builder_head => open_parenthesis capture _Rbuilder_head_32 close_parenthesis. - q(nt(219), (nt(38)+nt(56)+nt(222)+nt(39))); + q(nt(220), (nt(38)+nt(56)+nt(223)+nt(39))); // builder_body => tau. - q(nt(220), (nt(71))); + q(nt(221), (nt(72))); // builder_body => wff. - q(nt(220), (nt(74))); + q(nt(221), (nt(75))); // builder_body => bf. - q(nt(220), (nt(131))); + q(nt(221), (nt(132))); // gssotc => tau semicolon. - q(nt(223), (nt(71)+nt(46))); + q(nt(224), (nt(72)+nt(46))); // start => inputs. - q(nt(224), (nt(204))); + q(nt(225), (nt(205))); // start => formula. - q(nt(224), (nt(216))); + q(nt(225), (nt(217))); // start => library. - q(nt(224), (nt(217))); + q(nt(225), (nt(218))); // start => builder. - q(nt(224), (nt(218))); + q(nt(225), (nt(219))); // start => gssotc. - q(nt(224), (nt(223))); + q(nt(225), (nt(224))); return q; } }; diff --git a/tests/integration/test_integration-bdd1.cpp b/tests/integration/test_integration-bdd1.cpp index 6851e6cb..7139b04f 100644 --- a/tests/integration/test_integration-bdd1.cpp +++ b/tests/integration/test_integration-bdd1.cpp @@ -357,8 +357,8 @@ TEST_SUITE("formulas: variables, no bindings and quantifiers") { CHECK( check.has_value() ); } - TEST_CASE("bex P P") { - const char* sample = "bex P P."; + TEST_CASE("bex ?P ?P") { + const char* sample = "bex ?P ?P."; auto sample_src = make_tau_source(sample); bdd_test_factory bf; factory_binder fb(bf); @@ -370,8 +370,8 @@ TEST_SUITE("formulas: variables, no bindings and quantifiers") { CHECK( check.has_value() ); } - TEST_CASE("ball P P") { - const char* sample = "ball P P."; + TEST_CASE("ball ?P ?P") { + const char* sample = "ball ?P ?P."; auto sample_src = make_tau_source(sample); bdd_test_factory bf; factory_binder fb(bf); @@ -383,8 +383,8 @@ TEST_SUITE("formulas: variables, no bindings and quantifiers") { CHECK( check.has_value() ); } - TEST_CASE("ball P bex Q (P || Q)") { - const char* sample = "ball P bex Q (P || Q)."; + TEST_CASE("ball ?P bex ?Q (?P || ?Q)") { + const char* sample = "ball ?P bex ?Q (?P || ?Q)."; auto sample_src = make_tau_source(sample); bdd_test_factory bf; factory_binder fb(bf); @@ -396,8 +396,8 @@ TEST_SUITE("formulas: variables, no bindings and quantifiers") { CHECK( check.has_value() ); } - TEST_CASE("bex P ball Q (P || Q)") { - const char* sample = "bex P ball Q (P || Q)."; + TEST_CASE("bex ?P ball ?Q (?P || ?Q)") { + const char* sample = "bex ?P ball ?Q (?P || ?Q)."; auto sample_src = make_tau_source(sample); bdd_test_factory bf; factory_binder fb(bf);