search

fritzo / pomagma

An inference engine for extensional untyped λ-calculus
Other
17 stars 2 forks source link

Filter pomagma.theorist.solve define results #32

Open fritzo opened 9 years ago

fritzo commented 9 years ago

Example results contain garbage SECTION,RETRACT variables:

$ pomagma analyze skja 24575 &
$ pomagma.theorist.solve define unit
# python /home/fritz/.virtualenvs/pomagma/bin/pomagma.theorist.solve define unit
connecting to analyst at tcp://localhost:34936
Necessary:
Possible:
  UNIT
  APP SECTION B
  APP RETRACT B
  APP BOOL B
  APP SECTION CB
  APP RETRACT CB
  APP RETRACT C
  APP SECTION C
  APP BOOL CB
  COMP SECTION B
  APP SECTION TOP
  APP RETRACT TOP
  APP A CI
  APP SECTION CI
  APP RETRACT CI
  APP SECTION BOT
  COMP SECTION CB
  COMP RETRACT CB
  APP BOOL CI
  APP SECTION I
  APP RETRACT I
  APP DIV SECTION
  APP DIV RETRACT
  COMP BOOL CB
  COMP RETRACT TOP
  COMP SECTION TOP
  JOIN B SECTION
  APP BOOL I
  APP Y SECTION
  COMP RETRACT CI
  COMP SECTION CI
  APP SECTION Y
define took 310.57 sec

$ pomagma.theorist.solve define semi
# python /home/fritz/.virtualenvs/pomagma/bin/pomagma.theorist.solve define semi
connecting to analyst at tcp://localhost:34936
Necessary:
Possible:
  SEMI
  APP SECTION B
  APP RETRACT B
  APP BOOL B
  APP SECTION CB
  APP RETRACT CB
  APP RETRACT C
  APP SECTION C
  COMP SECTION B
  COMP RETRACT B
  APP SECTION TOP
  APP RETRACT TOP
  APP A CI
  APP SECTION CI
  APP RETRACT CI
  COMP BOOL B
  APP SECTION BOT
  COMP SECTION CB
  COMP RETRACT CB
  APP SECTION I
  APP RETRACT I
  APP DIV SECTION
  APP DIV RETRACT
  COMP RETRACT TOP
  COMP SECTION TOP
  JOIN B SECTION
  JOIN B RETRACT
  APP BOOL I
  APP Y SECTION
  COMP RETRACT CI
  COMP SECTION CI
  APP SECTION Y
define took 251.566 sec