module Data.Logic.Harrison.Herbrand where
import Control.Applicative.Error (Failing(..))
import Data.Logic.Classes.Atom (Atom(substitute, freeVariables))
import Data.Logic.Classes.FirstOrder (FirstOrderFormula)
import Data.Logic.Classes.Formula (Formula(..))
import Data.Logic.Classes.Literal (Literal)
import Data.Logic.Classes.Negate ((.~.))
import Data.Logic.Classes.Propositional (PropositionalFormula)
import Data.Logic.Classes.Term (Term, fApp)
import Data.Logic.Harrison.DP (dpll)
import Data.Logic.Harrison.FOL (generalize)
import Data.Logic.Harrison.Lib (distrib', allpairs)
import Data.Logic.Harrison.Normal (trivial)
import Data.Logic.Harrison.Prop (eval, simpcnf, simpdnf)
import Data.Logic.Harrison.Skolem (runSkolem, skolemize, functions)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.String (IsString(..))
pholds :: (PropositionalFormula formula atom, Ord atom) => (Map.Map atom Bool) -> formula -> Bool
pholds d fm = eval fm d
herbfuns :: forall pf atom term v f. (PropositionalFormula pf atom, Formula pf atom, Atom atom term v, Term term v f, IsString f, Ord f) =>
(atom -> Set.Set (f, Int))
-> pf
-> (Set.Set (f, Int), Set.Set (f, Int))
herbfuns fa fm =
let (cns,fns) = Set.partition (\ (_,ar) -> ar == 0) (functions fa fm) in
if Set.null cns then (Set.singleton (fromString "c",0),fns) else (cns,fns)
groundterms :: forall term v f. (Term term v f) =>
Set.Set term -> Set.Set (f, Int) -> Int -> Set.Set term
groundterms cntms _ 0 = cntms
groundterms cntms funcs n =
Set.fold terms Set.empty funcs
where
terms (f,m) l = Set.union (Set.map (fApp f) (groundtuples cntms funcs (n 1) m)) l
groundtuples :: forall term v f. (Term term v f) =>
Set.Set term -> Set.Set (f, Int) -> Int -> Int -> Set.Set [term]
groundtuples _ _ 0 0 = Set.singleton []
groundtuples _ _ _ 0 = Set.empty
groundtuples cntms funcs n m =
Set.fold tuples Set.empty (Set.fromList [0 .. n])
where
tuples k l = Set.union (allpairs (:) (groundterms cntms funcs k) (groundtuples cntms funcs (n k) (m 1))) l
herbloop :: forall lit atom v term f. (Literal lit atom, Term term v f, Atom atom term v) =>
(Set.Set (Set.Set lit) -> (lit -> lit) -> Set.Set (Set.Set lit) -> Set.Set (Set.Set lit))
-> (Set.Set (Set.Set lit) -> Failing Bool)
-> Set.Set (Set.Set lit)
-> Set.Set term
-> Set.Set (f, Int)
-> [v]
-> Int
-> Set.Set (Set.Set lit)
-> Set.Set [term]
-> Set.Set [term]
-> Failing (Set.Set [term])
herbloop mfn tfn fl0 cntms funcs fvs n fl tried tuples =
case Set.minView tuples of
Nothing ->
let newtups = groundtuples cntms funcs n (length fvs) in
herbloop mfn tfn fl0 cntms funcs fvs (n + 1) fl tried newtups
Just (tup, tups) ->
let fpf' = Map.fromList (zip fvs tup) in
let fl' = mfn fl0 (subst' fpf') fl in
case tfn fl' of
Failure msgs -> Failure msgs
Success x ->
if not x
then Success (Set.insert tup tried)
else herbloop mfn tfn fl0 cntms funcs fvs n fl' (Set.insert tup tried) tups
subst' :: forall lit atom term v f. (Literal lit atom, Atom atom term v, Term term v f) => Map.Map v term -> lit -> lit
subst' env fm =
mapAtoms (atomic . substitute') fm
where substitute' :: atom -> atom
substitute' = substitute env
gilmore_loop :: (Literal lit atom, Term term v f, Atom atom term v, Ord lit) =>
Set.Set (Set.Set lit)
-> Set.Set term
-> Set.Set (f, Int)
-> [v]
-> Int
-> Set.Set (Set.Set lit)
-> Set.Set [term]
-> Set.Set [term]
-> Failing (Set.Set [term])
gilmore_loop =
herbloop mfn (Success . not . Set.null)
where
mfn djs0 ifn djs = Set.filter (not . trivial) (distrib' (Set.map (Set.map ifn) djs0) djs)
gilmore :: forall fof pf atom term v f.
(FirstOrderFormula fof atom v,
PropositionalFormula pf atom,
Literal pf atom,
Term term v f,
Atom atom term v,
IsString f,
Ord pf) =>
pf -> (atom -> Set.Set (f, Int)) -> fof -> Failing Int
gilmore _ fa fm =
let sfm = runSkolem (skolemize id ((.~.)(generalize fm))) :: pf in
let fvs = Set.toList (foldAtoms (\ s (a :: atom) -> Set.union s (freeVariables a)) Set.empty sfm)
(consts,funcs) = herbfuns fa sfm in
let cntms = Set.map (\ (c,_) -> fApp c []) consts in
gilmore_loop (simpdnf sfm :: Set.Set (Set.Set pf)) cntms funcs (fvs) 0 Set.empty Set.empty Set.empty >>= return . Set.size
dp_mfn :: (Ord b, Ord a) =>
Set.Set (Set.Set a)
-> (a -> b)
-> Set.Set (Set.Set b)
-> Set.Set (Set.Set b)
dp_mfn cjs0 ifn cjs = Set.union (Set.map (Set.map ifn) cjs0) cjs
dp_loop :: forall lit atom v term f. (Literal lit atom, Term term v f, Atom atom term v, Ord lit) =>
Set.Set (Set.Set lit)
-> Set.Set term
-> Set.Set (f, Int)
-> [v]
-> Int
-> Set.Set (Set.Set lit)
-> Set.Set [term]
-> Set.Set [term]
-> Failing (Set.Set [term])
dp_loop = herbloop dp_mfn dpll
davisputnam :: forall fof atom term v lit f.
(FirstOrderFormula fof atom v,
PropositionalFormula lit atom,
Literal lit atom,
Term term v f,
Atom atom term v,
IsString f,
Ord lit) =>
lit -> (atom -> Set.Set (f, Int)) -> fof -> Failing Int
davisputnam _ fa fm =
let (sfm :: lit) = runSkolem (skolemize id ((.~.)(generalize fm))) in
let fvs = Set.toList (foldAtoms (\ s (a :: atom) -> Set.union (freeVariables a) s) Set.empty sfm)
(consts,funcs) = herbfuns fa sfm in
let cntms = Set.map (\ (c,_) -> fApp c [] :: term) consts in
dp_loop (simpcnf sfm :: Set.Set (Set.Set lit)) cntms funcs fvs 0 Set.empty Set.empty Set.empty >>= return . Set.size
dp_refine :: (Literal lit atom, Atom atom term v, Term term v f) =>
Set.Set (Set.Set lit) -> [v] -> Set.Set [term] -> Set.Set [term] -> Failing (Set.Set [term])
dp_refine cjs0 fvs dknow need =
case Set.minView dknow of
Nothing -> Success need
Just (cl, dknow') ->
let mfn = dp_mfn cjs0 . subst' . Map.fromList . zip fvs in
dpll (Set.fold mfn Set.empty (Set.union need dknow')) >>= \ flag ->
if flag then return (Set.insert cl need) else return need >>=
dp_refine cjs0 fvs dknow'
dp_refine_loop :: forall lit atom term v f. (Literal lit atom, Term term v f, Atom atom term v) =>
Set.Set (Set.Set lit)
-> Set.Set term
-> Set.Set (f, Int)
-> [v]
-> Int
-> Set.Set (Set.Set lit)
-> Set.Set [term]
-> Set.Set [term]
-> Failing (Set.Set [term])
dp_refine_loop cjs0 cntms funcs fvs n cjs tried tuples =
dp_loop cjs0 cntms funcs fvs n cjs tried tuples >>= \ tups ->
dp_refine cjs0 fvs tups Set.empty
davisputnam' :: forall fof atom term lit v f pf.
(FirstOrderFormula fof atom v,
Literal lit atom,
PropositionalFormula pf atom,
Term term v f,
Atom atom term v,
IsString f) =>
lit -> pf -> (atom -> Set.Set (f, Int)) -> fof -> Failing Int
davisputnam' _ _ fa fm =
let (sfm :: pf) = runSkolem (skolemize id ((.~.)(generalize fm))) in
let fvs = Set.toList (foldAtoms (\ s (a :: atom) -> Set.union (freeVariables a) s) Set.empty sfm)
(consts,funcs) = herbfuns fa sfm in
let cntms = Set.map (\ (c,_) -> fApp c []) consts in
dp_refine_loop (simpcnf sfm :: Set.Set (Set.Set lit)) cntms funcs fvs 0 Set.empty Set.empty Set.empty >>= return . Set.size