【问题标题】:Change the parsing language更改解析语言
【发布时间】:2015-07-13 21:40:33
【问题描述】:

我正在使用模态 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 = $1;}       
;

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

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

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

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

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

atomic_expression: CONC NUM {$$ = Make_formula_nary(atom_code,$2,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($1,$2);}
| {$$ = 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 {$$ = $2;}
;

%% /* 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 =&gt; B) &lt;=&gt; (~B v A))。
  • ALL RO 现在写成 [r0]
  • SOME RO 现在写成 &lt;r0&gt;
  • IFF (A B) 现在写成 (~B | A) &amp; (~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;

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

但我请你帮忙以确切地知道如何写下来:/

提前致谢!

【问题讨论】:

    标签: logic bison flex-lexer boolean-logic modal-logic


    【解决方案1】:

    Tommi Junttila 的BC Package 使用BisonFlex 实现了Boolean 表达式和电路的语言。

    学习源文件并不能完全取代通过正确的Bison/Flex 教程,但它肯定会给你一个好的开始。

    【讨论】:

    • 好吧,我已经完成了一些 bison/flex 教程,并且布尔表达式的解析已经开始工作了。它甚至已经适用于一种特定的模态逻辑语法,我的目标是:如何解析第二种语法,不幸的是,这与我在教程中可以找到的完全不同...:/
    • 我只能尝试鼓励您浏览 BC 包。它实现了“不寻常的”布尔运算符,将其转换为您的要求应该不会太难。
    【解决方案2】:

    对于遇到完全相同问题的人(我认为这个问题非常罕见:))

    有了好的词汇,用谷歌搜索问题并找到解决方案会容易得多。

    第一个符号

    (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 格式。

    还有一个名为公式翻译工具(“ftt”)的工具与斯巴达克斯(http://www.ps.uni-saarland.de/spartacus/)一起开发和捆绑。它可以在所有证明者格式之间进行转换。

    使用这个工具是避免使用 Flex/Bison 语言的小技巧。

    只需将一个问题翻译成另一个问题,问题将是等价的,翻译速度非常快。

    【讨论】: