--
-- This file has been auto-generated by egison-translator.
--

deleteLiteral l cnf :=
  map
    (\c -> matchAll c as multiset integer with
        | ((!#l) & $x) :: _ -> x)
    cnf

deleteClausesWith l cnf :=
  matchAll cnf as multiset (multiset integer) with
    | ((!(#l :: _)) & $c) :: _ -> c

assignTrue l cnf := deleteLiteral (neg l) (deleteClausesWith l cnf)

resolveOn v cnf :=
  matchAll cnf as multiset (multiset integer) with
    | {(#v :: (@ & $xs)) :: (#(neg v) :: (@ & $ys)) :: _,
       !( $l :: _, #(neg l) :: _ )} ->
      unique (xs ++ ys)

dp vars cnf :=
  match (vars, cnf) as (multiset integer, multiset (multiset integer)) with
  | (_, []) -> True
  | (_, [] :: _) -> False
  -- 1-literal rule
  | (_, [$l] :: _) -> dp (delete (abs l) vars) (assignTrue l cnf)
  -- pure literal rule (positive)
  | ($v :: $vs, !((#(neg v) :: _) :: _)) -> dp vs (assignTrue v cnf)
  -- pure literal rule (negative)
  | ($v :: $vs, !((#v :: _) :: _)) -> dp vs (assignTrue (neg v) cnf)
  -- otherwise
  | ($v :: $vs, _) ->
    dp vs
       ((resolveOn v cnf) ++ (deleteClausesWith v (deleteClausesWith (neg v) cnf)))

dp [1] [[1]]
dp [1] [[1], [-1]]
dp [1, 2, 3] [[1, 2], [-1, 3], [1, -3]]
dp [1, 2] [[1, 2], [-1, -2], [1, -2]]
dp [1, 2] [[1, 2], [-1, -2], [1, -2], [-1, 2]]
dp [1, 2, 3, 4, 5]
   [[-1, -2, 3], [-1, -2, -3], [1, 2, 3, 4], [-4, -2, 3], [5, 1, 2, -3], [-3, 1, -5], [1, -2, 3, 4], [1, -2, -3, 5]]
dp [1, 2] [[-1, -2], [1]]