!
! A very simplistic tableau calculus-based solver for propositional logic.
!
! Andreas Bolka
! Viktor  Pavlu
!
USING: kernel sequences math arrays generic strings io ;

SYMBOL: imp
SYMBOL: eq

! --- example propositions ---

: tree [
   eq [ imp [ and [ 1 ] 
                  [ 2 ] ] 
            [ 3 ] ] 
      [ imp [ not [  not [ 1 ] [ ] ] [ ] ] 
            [ imp [ 1 ] 
                  [ not [ 3 ] [ ] ] ] ]
] ;

! --- misc helpers ---

: node-head first ;
: node-left second ;
: node-right third ;
: node-children dup node-left swap node-right ; 

: is-not? ( a -- ? ) node-head \ not = ;
: is-and? ( a -- ? ) node-head \ and = ;
: is-or?  ( a -- ? ) node-head \ or  = ;
: is-imp? ( a -- ? ) node-head \ imp = ;
: is-eq?  ( a -- ? ) node-head \ eq  = ;
: is-lit? ( a -- ? ) node-head integer? ;

: enlist ( a -- seq )
  1array >quotation ;

: 2enlist ( a b -- seq )
  2array >quotation ; 

: adjoin ( a b -- c )
  enlist swap enlist swap append flatten >quotation ; 

: pairwise ( seq1 seq2 -- newseq )
  [ swap [ swap adjoin ] map-with ] map-with concat ;

SYMBOL: L
SYMBOL: R

! replaces all occurences of L with value l, R with value r (deep)
GENERIC: subst-LR ( l r tree1 -- tree2 ) 
M: quotation subst-LR [ >r 2dup r> subst-LR ] map 2nip ;
M: object    subst-LR 
  {
    { [ dup \ L = ] [ 2drop ] }
    { [ dup \ R = ] [ drop swap drop ] }
    { [ t ] [ 2nip ] }
  } cond ;

! --- string creation ---

: sign-to-s ( i -- str )
  0 > [ "" ] [ "-" ] if ;

: i-to-s ( i -- str )
  dup sign-to-s swap
  abs 96 + ch>string append ;

: errmsg ( object str1 -- str2 )
  enlist swap node-head add ;

: mold-tree ( tree -- str )
  {
    { [ dup is-not? ] [ node-left     mold-tree      [ ]            [ "-(" L ")"            ] subst-LR concat ] }
    { [ dup is-and? ] [ node-children mold-tree swap mold-tree swap [ "(" L ") && (" R ")"  ] subst-LR concat ] }
    { [ dup is-or?  ] [ node-children mold-tree swap mold-tree swap [ "(" L ") || (" R ")"  ] subst-LR concat ] }
    { [ dup is-imp? ] [ node-children mold-tree swap mold-tree swap [ "(" L ") -> (" R ")"  ] subst-LR concat ] }
    { [ dup is-eq?  ] [ node-children mold-tree swap mold-tree swap [ "(" L ") <-> (" R ")" ] subst-LR concat ] }
    { [ dup is-lit? ] [ node-head i-to-s ] }
    { [ t ] [ "mold-tree:" errmsg  ] }
  } cond ;

! --- negation normal form ---

: remove-impl ( tree -- tree )
  {
    { [ dup is-not? ] [ node-left     remove-impl      [ ]              [ not L [ ] ] subst-LR ] }
    { [ dup is-and? ] [ node-children remove-impl swap remove-impl swap [ and L  R  ] subst-LR ] }
    { [ dup is-or?  ] [ node-children remove-impl swap remove-impl swap [ or  L  R  ] subst-LR ] }
    { [ dup is-imp? ] [ node-children remove-impl swap remove-impl swap [ or [ not L [ ] ] R ] subst-LR ] }
    { [ dup is-eq?  ] [ node-children remove-impl swap remove-impl swap [ and [ or [ not L [ ] ] R ] [ or [ not R [ ] ] L ] ] subst-LR ] }
    { [ dup is-lit? ] [ node-head enlist ] }
    { [ t ] [ "remove-impl:" errmsg  ] }
  } cond ;


DEFER: movedown-not
: de-morgan ( tree -- tree )
  {
    { [ dup is-lit? ] [ node-head neg enlist ] }
    { [ dup is-not? ] [ node-left ] }
    { [ dup is-and? ] [ node-children movedown-not swap movedown-not swap [ or  [ not L [ ] ] [ not R [ ] ] ] subst-LR ] } 
    { [ dup is-or?  ] [ node-children movedown-not swap movedown-not swap [ and [ not L [ ] ] [ not R [ ] ] ] subst-LR ] } 
    { [ t ] [ ] }
  } cond ;

: movedown-not ( tree -- tree )
  {
    { [ dup is-lit? ] [ ] } ! identity
    { [ dup is-not? ] [ node-left de-morgan ] }
    { [ t ]           [ dup node-head >r
                        node-children movedown-not swap movedown-not swap
                        r> enlist [ L R ] append subst-LR ] }
  } cond ;

: (to-nnf) ( tree -- tree )
  dup movedown-not dup rot = [ ] [ (to-nnf) ] if ;

: to-nnf ( tree -- tree )
  remove-impl (to-nnf) ;

! --- disjunctive normal form ---

: nnf-to-dnf ( nnf -- dnf )
  {
    { [ dup is-and? ] [ dup node-left nnf-to-dnf 
                        swap node-right nnf-to-dnf 
                        pairwise ] }
    { [ dup is-or? ]  [ dup node-left nnf-to-dnf 
                        swap node-right nnf-to-dnf 
                        append ] }
    { [ dup is-lit? ] [ enlist ] }
  } cond ; 

! --- generation all variations with [1..n] inverted literals ---

: (bit-block) ( n -- seq ) 
  ! 3 -> [ 0 0 0 ]
  [ ] swap [ drop 0 add ] each ;

: bit-block ( len n -- seq ) 
  ! n as binary digits in a block of length len
  >bin [ ] swap [ 48 - add ] each
  dup length rot swap -
  (bit-block)
  swap append ;

: inv ( seq n -- seq ) 
  ! n-th variation of seq
  over length swap bit-block 
  [ 0 = [ ] [ neg ] if ] 2map ;

: n-inverts ( seq -- n ) 
  ! (2^length) - 1
  2 swap ^ 1 - ;

: gen-inverts ( seq -- seq ) 
  ! all variations of seq
  dup length n-inverts [ 1 + dupd inv ] map >quotation swap drop ;

! --- model handling ---

: contradiction? ( seq -- ? ) 
  dup [ neg swap member? not ] all-with? not ;

: compact ( dnf -- dnf )
  [ prune ] map
  [ contradiction? not ] subset 
  prune ;

: get-models ( seq -- seq )
  [ gen-inverts ] map     ! [ [ all variations ] [ all variations ] ... ]
  [ [ ] ] [ pairwise ] accumulate drop ;

: print-models ( seq -- )
  [ [ i-to-s 2 CHAR: \s pad-left ] map ] map
  [ natural-sort " " join write "\n" write ] each
  ;

! --- entry point ---

: negate ( tree -- newtree )
  enlist [ not ] append reverse ;

: solve ( tree -- seq )
  negate
  to-nnf
  nnf-to-dnf
  compact
  get-models
  compact
  ;

: go tree solve print-models ;

! vim: set ts=2 sts=2 sw=2 expandtab: