更改解析语言

Question

我正在使用模态 SAT 求解器。不幸的是，这个求解器使用的是 Flex 和 Bison，这两种语言我都不掌握...

我想将一种语法更改为另一种语法，但我遇到了一些问题，即使在学习了有关 Flex-Lexer 和 Bison 的教程之后也是如此。

问题来了：

我希望能够解析这样的模态逻辑公式：

在以前的符号中，这样的公式是这样写的：

(NOT (IMP (AND (ALL R0 (IMP C0 C1)) (ALL R0 C0)) (ALL R0 C1)))

下面是用于解析它们的 Flex/Bisons 文件：

alc.y

%{

#include "fnode.h"

#define YYMAXDEPTH 1000000

fnode_t *formula_as_tree;

%} 

%union {
   int     l;
   int     i;
   fnode_t *f;  
}

/* Tokens and types */

%token LP RP
%token ALL SOME
%token AND IMP OR IFF NOT
%token TOP BOT
%token RULE CONC
%token <l> NUM 

%type <f> formula 
%type <f> boolean_expression rule_expression atomic_expression
%type <f> other
%type <i> uboolop bboolop nboolop ruleop
%type <l> rule 

%% /* Grammar rules */

input: formula {formula_as_tree = ;}       
;

formula: boolean_expression {$$ = ;}
| rule_expression {$$ = ;}
| atomic_expression {$$ = ;}
;

boolean_expression: LP uboolop formula RP 
{$$ = Make_formula_nary(,empty_code,);}

| LP bboolop formula formula RP 
{$$ = Make_formula_nary(,empty_code, Make_operand_nary(,));}

| LP nboolop formula other RP 
{$$ = Make_formula_nary(,empty_code,Make_operand_nary(,));}
;

rule_expression: LP ruleop rule formula RP {$$ = Make_formula_nary(,,);}
;

atomic_expression: CONC NUM {$$ = Make_formula_nary(atom_code,,Make_empty());}
| TOP {$$ = Make_formula_nary(top_code,empty_code,Make_empty());}
| BOT {$$ = Make_formula_nary(bot_code,empty_code,Make_empty());}
;

other: formula other {$$ = Make_operand_nary(,);}
| {$$ = Make_empty();}
;

uboolop: NOT {$$ = not_code;}  
;

bboolop: IFF {$$ = iff_code;} 
|        IMP {$$ = imp_code;}
;

nboolop: AND {$$ = and_code;} 
|        OR  {$$ = or_code;} 
;

ruleop: SOME {$$ = dia_code;}
| ALL {$$ = box_code;}       

rule: RULE NUM {$$ = ;}
;

%% /* End of grammar rules */

int yyerror(char *s)  
{
  printf("%s\n", s);
  exit(0);
}

alc.lex

%{
#include <stdio.h>

#include "fnode.h"
#include "y.tab.h"

int number;
%}

%%

[ \n\t] ;    
"("      return LP;
")"      return RP; 
"ALL"    return ALL;         
"SOME"   return SOME;
"AND"    return AND; 
"IMP"    return IMP;
"OR"     return OR;
"IFF"    return IFF;
"NOT"    return NOT;
"TOP"    return TOP;
"BOTTOM" return BOT;
"R"      return RULE;
"C"      return CONC;

0|[1-9][0-9]* {   
  sscanf(yytext,"%d",&number);
  yylval.l=number;
  return NUM;
}

.  { 
  /* Error function */
  fprintf(stderr,"Illegal character\n");
  return -1;
}
%%

现在，让我们编写示例，但使用我想使用的新语法：

begin
(([r0](~pO | p1) & [r0]p0) | [r0]p1) 
end

阻碍我正确解析这个新语法的主要问题是：

IMP (A B) 现在写成 ~B | A（如布尔逻辑 (A => B) <=> (~B v A)）。
ALL RO现在写成[r0]。
SOME RO现在写成<r0>.
IFF (A B)现在写成(~B | A) & (~A | B)。（IFF 代表for if and only if）

这是新符号的小列表，即使我不知道如何解析它们：

"("      return LP;
")"      return RP; 
"[]"    return ALL;         
"<>"   return SOME;
"&"    return AND; 
"IMP"    return IMP;
"|"     return OR;
"IFF"    return IFF;
"~"    return NOT;
"true"    return TOP;
"false" return BOT;
"r"      return RULE;
"p"      return CONC;

我假设只有这 2 个文件会改变，因为它应该仍然能够通过使用其他 .y 和 .lex 编译源代码来读取以前的语法

但我想请你帮忙知道具体如何写下来:/

提前致谢！

Answer 1

Tommi Junttila 的 BC Package 使用 Bison 和 Flex 为 Boolean 表达式和电路实现了一种语言。

学习源文件并不能完全取代学习正确的 Bison/Flex 教程，但它肯定会给您一个良好的开端。

Answer 2

对于遇到完全相同问题的人（我认为这个问题很少见:)）

有了好的词汇，google问题和找到解决方案就容易多了。

第一个符号

(NOT (IMP (AND (ALL R0 (IMP C0 C1)) (ALL R0 C0)) (ALL R0 C1)))

是ALC格式。

其他表示法

begin (([r0](~pO | p1) & [r0]p0) | [r0]p1) end

是InToHyLo格式。

还有一个与 Spartacus (http://www.ps.uni-saarland.de/spartacus/) 一起开发并捆绑的工具，称为公式翻译工具 ("ftt")。它可以在证明者的所有格式之间进行翻译。

使用此工具是避免与 Flex/Bison 语言打交道的小窍门。

只需要将一个问题转化为另一个问题，问题是等价的，转化速度非常快。

更改解析语言

Change the parsing language

logic

boolean-logic

bison

flex-lexer

modal-logic

alc.y

alc.lex