-- | Encodes Horn problems as unit equalities.
module Jukebox.Tools.HornToUnit where

-- To translate Horn problems where the only predicate is equality, we use the
-- following translation.
--
-- We introduce a predicate $ifeq : A * A * B > B at (conceptually) each pair
-- of types A and B, together with the axiom
--   $ifeq(X, X, Y) = Y.
--
-- A conditional equation a = b => c = d is encoded as
--   $ifeq(a, b, c) = $ifeq(a, b, d)
--
-- When encoding equations with multiple conditions we proceed from the inside
-- out so that, for example
--   a = b & c = d => e = f
-- would become
--   a = b => $ifeq(c, d, e) = $ifeq(c, d, f)
-- which in turn becomes
--   $ifeq(a, b, $ifeq(c, d, e)) = $ifeq(a, b, $ifeq(c, d, f))
--
-- We encode predicates p(X) as equations p(X)=true, i.e., we introduce a new
-- type bool and term true : bool, and transform predicates into functions
-- to bool.

import Jukebox.Form
import Jukebox.Name
import Jukebox.Options
import Jukebox.Utils
import qualified Jukebox.Sat as Sat
import Data.List
import Control.Monad
import qualified Data.Set as Set
import qualified Data.Map.Strict as Map
import Control.Monad.Trans.RWS
import Control.Monad.Trans.List
import Control.Monad.Trans.Class

data HornFlags =
  HornFlags {
    HornFlags -> Bool
allowConjunctiveConjectures :: Bool,
    HornFlags -> Bool
allowDisjunctiveConjectures :: Bool,
    HornFlags -> Bool
allowNonGroundConjectures :: Bool,
    HornFlags -> Bool
allowCompoundConjectures :: Bool,
    HornFlags -> Bool
dropNonHorn :: Bool,
    HornFlags -> Bool
passivise :: Bool,
    HornFlags -> Bool
multi :: Bool,
    HornFlags -> Bool
smaller :: Bool,
    HornFlags -> Encoding
encoding :: Encoding }
  deriving Int -> HornFlags -> ShowS
[HornFlags] -> ShowS
HornFlags -> String
(Int -> HornFlags -> ShowS)
-> (HornFlags -> String)
-> ([HornFlags] -> ShowS)
-> Show HornFlags
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HornFlags] -> ShowS
$cshowList :: [HornFlags] -> ShowS
show :: HornFlags -> String
$cshow :: HornFlags -> String
showsPrec :: Int -> HornFlags -> ShowS
$cshowsPrec :: Int -> HornFlags -> ShowS
Show

data Encoding = Symmetric | Asymmetric1 | Asymmetric2 | Asymmetric3
  deriving (Encoding -> Encoding -> Bool
(Encoding -> Encoding -> Bool)
-> (Encoding -> Encoding -> Bool) -> Eq Encoding
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Encoding -> Encoding -> Bool
$c/= :: Encoding -> Encoding -> Bool
== :: Encoding -> Encoding -> Bool
$c== :: Encoding -> Encoding -> Bool
Eq, Int -> Encoding -> ShowS
[Encoding] -> ShowS
Encoding -> String
(Int -> Encoding -> ShowS)
-> (Encoding -> String) -> ([Encoding] -> ShowS) -> Show Encoding
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Encoding] -> ShowS
$cshowList :: [Encoding] -> ShowS
show :: Encoding -> String
$cshow :: Encoding -> String
showsPrec :: Int -> Encoding -> ShowS
$cshowsPrec :: Int -> Encoding -> ShowS
Show)

hornFlags :: OptionParser HornFlags
hornFlags :: OptionParser HornFlags
hornFlags =
  String -> OptionParser HornFlags -> OptionParser HornFlags
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"Horn clause encoding options" (OptionParser HornFlags -> OptionParser HornFlags)
-> OptionParser HornFlags -> OptionParser HornFlags
forall a b. (a -> b) -> a -> b
$
  Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Encoding
-> HornFlags
HornFlags (Bool
 -> Bool
 -> Bool
 -> Bool
 -> Bool
 -> Bool
 -> Bool
 -> Bool
 -> Encoding
 -> HornFlags)
-> Annotated [Flag] ParParser Bool
-> Annotated
     [Flag]
     ParParser
     (Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Encoding
      -> HornFlags)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"conjunctive-conjectures"
      [String
"Allow conjectures to be conjunctions of equations (on by default)."]
      Bool
True Annotated
  [Flag]
  ParParser
  (Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Encoding
   -> HornFlags)
-> Annotated [Flag] ParParser Bool
-> Annotated
     [Flag]
     ParParser
     (Bool
      -> Bool -> Bool -> Bool -> Bool -> Bool -> Encoding -> HornFlags)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"disjunctive-conjectures"
      [String
"Allow conjectures to be disjunctions of equations (on by default)."]
      Bool
True Annotated
  [Flag]
  ParParser
  (Bool
   -> Bool -> Bool -> Bool -> Bool -> Bool -> Encoding -> HornFlags)
-> Annotated [Flag] ParParser Bool
-> Annotated
     [Flag]
     ParParser
     (Bool -> Bool -> Bool -> Bool -> Bool -> Encoding -> HornFlags)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"non-ground-conjectures"
      [String
"Allow conjectures to be non-ground clauses (on by default)."]
      Bool
True Annotated
  [Flag]
  ParParser
  (Bool -> Bool -> Bool -> Bool -> Bool -> Encoding -> HornFlags)
-> Annotated [Flag] ParParser Bool
-> Annotated
     [Flag]
     ParParser
     (Bool -> Bool -> Bool -> Bool -> Encoding -> HornFlags)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"compound-conjectures"
      [String
"Allow conjectures to be compound terms (on by default)."]
      Bool
True Annotated
  [Flag]
  ParParser
  (Bool -> Bool -> Bool -> Bool -> Encoding -> HornFlags)
-> Annotated [Flag] ParParser Bool
-> Annotated
     [Flag] ParParser (Bool -> Bool -> Bool -> Encoding -> HornFlags)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"drop-non-horn"
      [String
"Silently drop non-Horn clauses from input problem (off by default)."]
      Bool
False Annotated
  [Flag] ParParser (Bool -> Bool -> Bool -> Encoding -> HornFlags)
-> Annotated [Flag] ParParser Bool
-> Annotated
     [Flag] ParParser (Bool -> Bool -> Encoding -> HornFlags)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"passivise"
      [String
"Encode problem so as to get fewer critical pairs (off by default)."]
      Bool
False Annotated [Flag] ParParser (Bool -> Bool -> Encoding -> HornFlags)
-> Annotated [Flag] ParParser Bool
-> Annotated [Flag] ParParser (Bool -> Encoding -> HornFlags)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"multi"
      [String
"Encode multiple left-hand sides at once (off by default)."]
      Bool
False Annotated [Flag] ParParser (Bool -> Encoding -> HornFlags)
-> Annotated [Flag] ParParser Bool
-> Annotated [Flag] ParParser (Encoding -> HornFlags)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"smaller"
      [String
"Swap ordering of certain equations (off by default)"]
      Bool
False Annotated [Flag] ParParser (Encoding -> HornFlags)
-> Annotated [Flag] ParParser Encoding -> OptionParser HornFlags
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    Annotated [Flag] ParParser Encoding
encoding
  where
    encoding :: Annotated [Flag] ParParser Encoding
encoding =
      String
-> [String]
-> Encoding
-> ArgParser Encoding
-> Annotated [Flag] ParParser Encoding
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"conditional-encoding"
        [String
"Which method to use to encode conditionals (if-then-else by default)."]
        Encoding
Asymmetric1
        ([(String, Encoding)] -> ArgParser Encoding
forall a. [(String, a)] -> ArgParser a
argOption
          [(String
"if-then", Encoding
Symmetric),
           (String
"if-then-else", Encoding
Asymmetric1),
           (String
"fresh", Encoding
Asymmetric2),
           (String
"if", Encoding
Asymmetric3)])

hornToUnit :: HornFlags -> Problem Clause -> IO (Either (Input Clause) (Either Answer (Problem Clause)))
hornToUnit :: HornFlags
-> Problem Clause
-> IO (Either (Input Clause) (Either Answer (Problem Clause)))
hornToUnit HornFlags
flags Problem Clause
prob = do
  Either Answer (Problem Clause -> Problem Clause)
res <- Problem Clause
-> IO (Either Answer (Problem Clause -> Problem Clause))
encodeTypesSmartly Problem Clause
prob
  Either (Input Clause) (Either Answer (Problem Clause))
-> IO (Either (Input Clause) (Either Answer (Problem Clause)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Input Clause) (Either Answer (Problem Clause))
 -> IO (Either (Input Clause) (Either Answer (Problem Clause))))
-> Either (Input Clause) (Either Answer (Problem Clause))
-> IO (Either (Input Clause) (Either Answer (Problem Clause)))
forall a b. (a -> b) -> a -> b
$
    case Either Answer (Problem Clause -> Problem Clause)
res of
      Left Answer
ans ->
        Either Answer (Problem Clause)
-> Either (Input Clause) (Either Answer (Problem Clause))
forall a b. b -> Either a b
Right (Answer -> Either Answer (Problem Clause)
forall a b. a -> Either a b
Left Answer
ans)
      Right Problem Clause -> Problem Clause
enc ->
        (Problem Clause -> Either Answer (Problem Clause))
-> Either (Input Clause) (Problem Clause)
-> Either (Input Clause) (Either Answer (Problem Clause))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Problem Clause -> Either Answer (Problem Clause)
forall a b. b -> Either a b
Right (Problem Clause -> Either Answer (Problem Clause))
-> (Problem Clause -> Problem Clause)
-> Problem Clause
-> Either Answer (Problem Clause)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Problem Clause -> Problem Clause
enc) (Either (Input Clause) (Problem Clause)
 -> Either (Input Clause) (Either Answer (Problem Clause)))
-> Either (Input Clause) (Problem Clause)
-> Either (Input Clause) (Either Answer (Problem Clause))
forall a b. (a -> b) -> a -> b
$
        HornFlags
-> Problem Clause -> Either (Input Clause) (Problem Clause)
eliminateHornClauses HornFlags
flags (Problem Clause -> Either (Input Clause) (Problem Clause))
-> Problem Clause -> Either (Input Clause) (Problem Clause)
forall a b. (a -> b) -> a -> b
$
        HornFlags -> Problem Clause -> Problem Clause
eliminateUnsuitableConjectures HornFlags
flags (Problem Clause -> Problem Clause)
-> Problem Clause -> Problem Clause
forall a b. (a -> b) -> a -> b
$
        HornFlags -> Problem Clause -> Problem Clause
eliminateMultiplePreconditions HornFlags
flags (Problem Clause -> Problem Clause)
-> Problem Clause -> Problem Clause
forall a b. (a -> b) -> a -> b
$
        Problem Clause -> Problem Clause
eliminatePredicates Problem Clause
prob

eliminatePredicates :: Problem Clause -> Problem Clause
eliminatePredicates :: Problem Clause -> Problem Clause
eliminatePredicates Problem Clause
prob =
  (Input Clause -> Input Clause) -> Problem Clause -> Problem Clause
forall a b. (a -> b) -> [a] -> [b]
map ((Clause -> Clause) -> Input Clause -> Input Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> Clause
elim) Problem Clause
prob
  where
    elim :: Clause -> Clause
elim = [Literal] -> Clause
clause ([Literal] -> Clause) -> (Clause -> [Literal]) -> Clause -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Literal -> Literal) -> [Literal] -> [Literal]
forall a b. (a -> b) -> [a] -> [b]
map ((Atomic -> Atomic) -> Literal -> Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Atomic -> Atomic
elim1) ([Literal] -> [Literal])
-> (Clause -> [Literal]) -> Clause -> [Literal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Literal]
toLiterals
    elim1 :: Atomic -> Atomic
elim1 (Term
t :=: Term
u) = Term
t Term -> Term -> Atomic
:=: Term
u
    elim1 (Tru ((Name
p ::: FunType [Type]
tys Type
_) :@: [Term]
ts)) =
      ((Name
p Name -> FunType -> Name ::: FunType
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType [Type]
tys Type
bool) (Name ::: FunType) -> [Term] -> Term
:@: [Term]
ts) Term -> Term -> Atomic
:=: Term
true

    (Type
bool, Term
true) = Problem Clause -> NameM (Type, Term) -> (Type, Term)
forall a b. Symbolic a => a -> NameM b -> b
run_ Problem Clause
prob (NameM (Type, Term) -> (Type, Term))
-> NameM (Type, Term) -> (Type, Term)
forall a b. (a -> b) -> a -> b
$ do
      Type
bool <- Name -> NameM Type
forall a. Named a => a -> NameM Type
newType (String -> Name -> Name
withLabel String
"bool" (String -> Name
forall a. Named a => a -> Name
name String
"bool"))
      Name ::: FunType
true <- Name -> [Type] -> Type -> NameM (Name ::: FunType)
forall a.
Named a =>
a -> [Type] -> Type -> NameM (Name ::: FunType)
newFunction (String -> Name -> Name
withLabel String
"true" (String -> Name
forall a. Named a => a -> Name
name String
"true")) [] Type
bool
      (Type, Term) -> NameM (Type, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
bool, Name ::: FunType
true (Name ::: FunType) -> [Term] -> Term
:@: [])

eliminateMultiplePreconditions :: HornFlags -> Problem Clause -> Problem Clause
eliminateMultiplePreconditions :: HornFlags -> Problem Clause -> Problem Clause
eliminateMultiplePreconditions HornFlags
flags Problem Clause
prob
  | Bool
otherwise =
    (Input Clause -> Input Clause) -> Problem Clause -> Problem Clause
forall a b. (a -> b) -> [a] -> [b]
map Input Clause -> Input Clause
elim Problem Clause
prob
    where
      elim :: Input Clause -> Input Clause
elim Input Clause
inp
        | ([Literal] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Literal]
poss Bool -> Bool -> Bool
&& [Literal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Literal]
negs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1 Bool -> Bool -> Bool
&& Bool -> Bool
not (HornFlags -> Bool
allowConjunctiveConjectures HornFlags
flags)) Bool -> Bool -> Bool
||
          (Bool -> Bool
not ([Literal] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Literal]
poss) Bool -> Bool -> Bool
&& [Literal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Literal]
negs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 Bool -> Bool -> Bool
&& HornFlags -> Bool
multi HornFlags
flags) =
          Input Clause
inp{what :: Clause
what = [Literal] -> Clause
clause (Atomic -> Literal
forall a. a -> Signed a
Neg (([Type] -> Name ::: FunType
tuple [Type]
tys (Name ::: FunType) -> [Term] -> Term
:@: [Term]
ts) Term -> Term -> Atomic
:=: ([Type] -> Name ::: FunType
tuple [Type]
tys (Name ::: FunType) -> [Term] -> Term
:@: [Term]
us))Literal -> [Literal] -> [Literal]
forall a. a -> [a] -> [a]
:[Literal]
poss)}
        where
          ([Literal]
poss, [Literal]
negs) = (Literal -> Bool) -> [Literal] -> ([Literal], [Literal])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Literal -> Bool
forall a. Signed a -> Bool
pos (Clause -> [Literal]
toLiterals (Input Clause -> Clause
forall a. Input a -> a
what Input Clause
inp))
          ts :: [Term]
ts = [Term
t | Literal
l <- [Literal]
negs, let Neg (Term
t :=: Term
_) = Literal
l]
          us :: [Term]
us = [Term
u | Literal
l <- [Literal]
negs, let Neg (Term
_ :=: Term
u) = Literal
l]
          tys :: [Type]
tys = (Term -> Type) -> [Term] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Type
forall a. Typed a => a -> Type
typ [Term]
ts
      elim Input Clause
inp = Input Clause
inp

      tuple :: [Type] -> Name ::: FunType
tuple = Problem Clause
-> NameM ([Type] -> Name ::: FunType) -> [Type] -> Name ::: FunType
forall a b. Symbolic a => a -> NameM b -> b
run_ Problem Clause
prob (NameM ([Type] -> Name ::: FunType) -> [Type] -> Name ::: FunType)
-> NameM ([Type] -> Name ::: FunType) -> [Type] -> Name ::: FunType
forall a b. (a -> b) -> a -> b
$ do
        Name
tupleType <- Name -> NameM Name
forall a. Named a => a -> NameM Name
newName (String -> Name -> Name
withLabel String
"tuple" (String -> Name
forall a. Named a => a -> Name
name String
"tuple"))
        Name
tuple <- Name -> NameM Name
forall a. Named a => a -> NameM Name
newName (String -> Name -> Name
withLabel String
"tuple" (String -> Name
forall a. Named a => a -> Name
name String
"tuple"))
        ([Type] -> Name ::: FunType) -> NameM ([Type] -> Name ::: FunType)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Type] -> Name ::: FunType)
 -> NameM ([Type] -> Name ::: FunType))
-> ([Type] -> Name ::: FunType)
-> NameM ([Type] -> Name ::: FunType)
forall a b. (a -> b) -> a -> b
$ \[Type]
args ->
          Name -> [Type] -> Name
forall a b. (Named a, Named b) => a -> [b] -> Name
variant Name
tuple [Type]
args Name -> FunType -> Name ::: FunType
forall a b. a -> b -> a ::: b
:::
          [Type] -> Type -> FunType
FunType [Type]
args (Name -> Type
Type (Name -> [Type] -> Name
forall a b. (Named a, Named b) => a -> [b] -> Name
variant Name
tupleType [Type]
args))

eliminateUnsuitableConjectures :: HornFlags -> Problem Clause -> Problem Clause
eliminateUnsuitableConjectures :: HornFlags -> Problem Clause -> Problem Clause
eliminateUnsuitableConjectures HornFlags
flags Problem Clause
prob
  | Problem Clause -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Problem Clause
bad = Problem Clause
prob
  | Bool
otherwise =
    Problem Clause
good Problem Clause -> Problem Clause -> Problem Clause
forall a. [a] -> [a] -> [a]
++ (Input Clause -> Input Clause) -> Problem Clause -> Problem Clause
forall a b. (a -> b) -> [a] -> [b]
map ((Clause -> Clause) -> Input Clause -> Input Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> Clause
addConjecture) Problem Clause
bad Problem Clause -> Problem Clause -> Problem Clause
forall a. [a] -> [a] -> [a]
++
    [Input :: forall a. String -> Kind -> InputSource -> a -> Input a
Input { tag :: String
tag = String
"goal", kind :: Kind
kind = AxKind -> Kind
Ax AxKind
NegatedConjecture, source :: InputSource
source = InputSource
Unknown,
             what :: Clause
what = [Literal] -> Clause
clause [Atomic -> Literal
forall a. a -> Signed a
Neg (Term
a Term -> Term -> Atomic
:=: Term
b)] }]
  where
    (Problem Clause
bad, Problem Clause
good) = (Input Clause -> Bool)
-> Problem Clause -> (Problem Clause, Problem Clause)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Input Clause -> Bool
unsuitable Problem Clause
prob

    ngoals :: Int
ngoals = Problem Clause -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Problem Clause -> Int) -> Problem Clause -> Int
forall a b. (a -> b) -> a -> b
$ (Input Clause -> Bool) -> Problem Clause -> Problem Clause
forall a. (a -> Bool) -> [a] -> [a]
filter ((Literal -> Bool) -> [Literal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Literal -> Bool) -> Literal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Bool
forall a. Signed a -> Bool
pos) ([Literal] -> Bool)
-> (Input Clause -> [Literal]) -> Input Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Literal]
toLiterals (Clause -> [Literal])
-> (Input Clause -> Clause) -> Input Clause -> [Literal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Input Clause -> Clause
forall a. Input a -> a
what) Problem Clause
prob

    unsuitable :: Input Clause -> Bool
unsuitable Input Clause
c =
      (Literal -> Bool) -> [Literal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Literal -> Bool) -> Literal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Bool
forall a. Signed a -> Bool
pos) [Literal]
ls Bool -> Bool -> Bool
&&
      ((Bool -> Bool
not (HornFlags -> Bool
allowCompoundConjectures HornFlags
flags) Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Term -> Int
size Term
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 | Term
t <- [Literal] -> [Term]
forall a. Symbolic a => a -> [Term]
terms [Literal]
ls]) Bool -> Bool -> Bool
||
       (Bool -> Bool
not (HornFlags -> Bool
allowDisjunctiveConjectures HornFlags
flags) Bool -> Bool -> Bool
&& Int
ngoals Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) Bool -> Bool -> Bool
||
       (Bool -> Bool
not (HornFlags -> Bool
allowNonGroundConjectures HornFlags
flags) Bool -> Bool -> Bool
&& Bool -> Bool
not ([Literal] -> Bool
forall a. Symbolic a => a -> Bool
ground [Literal]
ls)))
      where
        ls :: [Literal]
ls = Clause -> [Literal]
toLiterals (Input Clause -> Clause
forall a. Input a -> a
what Input Clause
c)

    addConjecture :: Clause -> Clause
addConjecture Clause
c = [Literal] -> Clause
clause (Atomic -> Literal
forall a. a -> Signed a
Pos (Term
a Term -> Term -> Atomic
:=: Term
b)Literal -> [Literal] -> [Literal]
forall a. a -> [a] -> [a]
:Clause -> [Literal]
toLiterals Clause
c)

    (Term
a, Term
b) = Problem Clause -> NameM (Term, Term) -> (Term, Term)
forall a b. Symbolic a => a -> NameM b -> b
run_ Problem Clause
prob (NameM (Term, Term) -> (Term, Term))
-> NameM (Term, Term) -> (Term, Term)
forall a b. (a -> b) -> a -> b
$ do
      Type
token <- Name -> NameM Type
forall a. Named a => a -> NameM Type
newType (String -> Name -> Name
withLabel String
"token" (String -> Name
forall a. Named a => a -> Name
name String
"token"))
      Name ::: FunType
a <- Name -> [Type] -> Type -> NameM (Name ::: FunType)
forall a.
Named a =>
a -> [Type] -> Type -> NameM (Name ::: FunType)
newFunction (String -> Name -> Name
withLabel String
"token_a" (String -> Name
forall a. Named a => a -> Name
name String
"a")) [] Type
token
      Name ::: FunType
b <- Name -> [Type] -> Type -> NameM (Name ::: FunType)
forall a.
Named a =>
a -> [Type] -> Type -> NameM (Name ::: FunType)
newFunction (String -> Name -> Name
withLabel String
"token_b" (String -> Name
forall a. Named a => a -> Name
name String
"b")) [] Type
token
      (Term, Term) -> NameM (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ::: FunType
a (Name ::: FunType) -> [Term] -> Term
:@: [], Name ::: FunType
b (Name ::: FunType) -> [Term] -> Term
:@: [])

eliminateHornClauses :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause)
eliminateHornClauses :: HornFlags
-> Problem Clause -> Either (Input Clause) (Problem Clause)
eliminateHornClauses HornFlags
flags Problem Clause
prob = do
  ([Problem Clause]
prob, [(String, Atomic)]
funs) <- RWST
  () [(String, Atomic)] Int (Either (Input Clause)) [Problem Clause]
-> ()
-> Int
-> Either (Input Clause) ([Problem Clause], [(String, Atomic)])
forall (m :: * -> *) r w s a.
Monad m =>
RWST r w s m a -> r -> s -> m (a, w)
evalRWST ((Input Clause
 -> RWST
      () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause))
-> Problem Clause
-> RWST
     () [(String, Atomic)] Int (Either (Input Clause)) [Problem Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Input Clause
-> RWST
     () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause)
elim1 Problem Clause
prob) () Int
0
  Problem Clause -> Either (Input Clause) (Problem Clause)
forall (m :: * -> *) a. Monad m => a -> m a
return (((String, Atomic) -> Input Clause)
-> [(String, Atomic)] -> Problem Clause
forall a b. (a -> b) -> [a] -> [b]
map (String, Atomic) -> Input Clause
toInput ([(String, Atomic)] -> [(String, Atomic)]
forall a. Ord a => [a] -> [a]
usort [(String, Atomic)]
funs) Problem Clause -> Problem Clause -> Problem Clause
forall a. [a] -> [a] -> [a]
++ [Problem Clause] -> Problem Clause
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Problem Clause]
prob)
  where
    fresh :: a -> t (RWST r w a m) Name
fresh a
base = RWST r w a m Name -> t (RWST r w a m) Name
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RWST r w a m Name -> t (RWST r w a m) Name)
-> RWST r w a m Name -> t (RWST r w a m) Name
forall a b. (a -> b) -> a -> b
$ do
      a
n <- RWST r w a m a
forall w (m :: * -> *) r s. (Monoid w, Monad m) => RWST r w s m s
get
      a -> RWST r w a m ()
forall w (m :: * -> *) s r.
(Monoid w, Monad m) =>
s -> RWST r w s m ()
put (a -> RWST r w a m ()) -> a -> RWST r w a m ()
forall a b. (a -> b) -> a -> b
$! a
na -> a -> a
forall a. Num a => a -> a -> a
+a
1
      Name -> RWST r w a m Name
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> [Name] -> Name
forall a b. (Named a, Named b) => a -> [b] -> Name
variant a
base [String -> Name
forall a. Named a => a -> Name
name (a -> String
forall a. Show a => a -> String
show a
n)])

    passiveFresh :: (Name ::: b) -> t (RWST r w a m) (Name ::: b)
passiveFresh (Name
x ::: b
ty)
      | HornFlags -> Bool
passivise HornFlags
flags = (Name -> Name ::: b)
-> t (RWST r w a m) Name -> t (RWST r w a m) (Name ::: b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> b -> Name ::: b
forall a b. a -> b -> a ::: b
::: b
ty) (Name -> t (RWST r w a m) Name
forall (t :: (* -> *) -> * -> *) w (m :: * -> *) a a r.
(MonadTrans t, Monoid w, Monad m, Num a, Named a, Show a) =>
a -> t (RWST r w a m) Name
fresh Name
x)
      | Bool
otherwise = (Name ::: b) -> t (RWST r w a m) (Name ::: b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x Name -> b -> Name ::: b
forall a b. a -> b -> a ::: b
::: b
ty)

    passive :: Term -> Term
passive (Var Variable
x) = Variable -> Term
Var Variable
x
    passive ((Name
f ::: FunType
ty) :@: [Term]
ts) =
      (Name -> [Name] -> Name
forall a b. (Named a, Named b) => a -> [b] -> Name
variant Name
f [Name
passiveName] Name -> FunType -> Name ::: FunType
forall a b. a -> b -> a ::: b
::: FunType
ty) (Name ::: FunType) -> [Term] -> Term
:@: (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
passive [Term]
ts

    elim1 :: Input Clause -> RWST () [(String, Atomic)] Int (Either (Input Clause)) [Input Clause]
    elim1 :: Input Clause
-> RWST
     () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause)
elim1 Input Clause
c =
      case (Literal -> Bool) -> [Literal] -> ([Literal], [Literal])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Literal -> Bool
forall a. Signed a -> Bool
pos (Clause -> [Literal]
toLiterals (Input Clause -> Clause
forall a. Input a -> a
what Input Clause
c)) of
        ([], [Literal]
_) -> Problem Clause
-> RWST
     () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause)
forall (m :: * -> *) a. Monad m => a -> m a
return [Input Clause
c]
        ([Pos Atomic
l], [Literal]
ls) -> ListT
  (RWST () [(String, Atomic)] Int (Either (Input Clause)))
  (Input Clause)
-> RWST
     () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause)
forall (m :: * -> *) a. ListT m a -> m [a]
runListT (ListT
   (RWST () [(String, Atomic)] Int (Either (Input Clause)))
   (Input Clause)
 -> RWST
      () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause))
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause)))
     (Input Clause)
-> RWST
     () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause)
forall a b. (a -> b) -> a -> b
$ do
          Atomic
l <- (Atomic
 -> Literal
 -> ListT
      (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic)
-> Atomic
-> [Literal]
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (String
-> Atomic
-> Literal
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
encode (Input Clause -> String
forall a. Input a -> String
tag Input Clause
c)) Atomic
l [Literal]
ls
          Input Clause
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause)))
     (Input Clause)
forall (m :: * -> *) a. Monad m => a -> m a
return Input Clause
c { what :: Clause
what = [Literal] -> Clause
clause [Atomic -> Literal
forall a. a -> Signed a
Pos Atomic
l] }
        ([Literal], [Literal])
_ ->
          if HornFlags -> Bool
dropNonHorn HornFlags
flags then
            Problem Clause
-> RWST
     () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause)
forall (m :: * -> *) a. Monad m => a -> m a
return []
          else
            Either (Input Clause) (Problem Clause)
-> RWST
     () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Either (Input Clause) (Problem Clause)
 -> RWST
      () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause))
-> Either (Input Clause) (Problem Clause)
-> RWST
     () [(String, Atomic)] Int (Either (Input Clause)) (Problem Clause)
forall a b. (a -> b) -> a -> b
$ Input Clause -> Either (Input Clause) (Problem Clause)
forall a b. a -> Either a b
Left Input Clause
c

    encode :: String -> Atomic -> Literal -> ListT (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
    encode :: String
-> Atomic
-> Literal
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
encode String
tag (Term
c :=: Term
d) (Neg (Term
a :=: Term
b)) =
      let
        ty1 :: Type
ty1 = Term -> Type
forall a. Typed a => a -> Type
typ Term
a
        ty2 :: Type
ty2 = Term -> Type
forall a. Typed a => a -> Type
typ Term
c
        x :: Term
x = Variable -> Term
Var (Name
xvar Name -> Type -> Variable
forall a b. a -> b -> a ::: b
::: Type
ty1)
        y :: Term
y = Variable -> Term
Var (Name
yvar Name -> Type -> Variable
forall a b. a -> b -> a ::: b
::: Type
ty2)
        z :: Term
z = Variable -> Term
Var (Name
zvar Name -> Type -> Variable
forall a b. a -> b -> a ::: b
::: Type
ty2)
      in case HornFlags -> Encoding
encoding HornFlags
flags of
        -- ifeq(x, x, y) = y
        -- ifeq(a, b, c) = ifeq(a, b, d)
        Encoding
Symmetric -> do
          Name ::: FunType
ifeq <- (Name ::: FunType)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause)))
     (Name ::: FunType)
forall (t :: (* -> *) -> * -> *) w a (m :: * -> *) r b.
(MonadTrans t, Monoid w, Num a, Show a, Monad m,
 Monad (t (RWST r w a m))) =>
(Name ::: b) -> t (RWST r w a m) (Name ::: b)
passiveFresh (Name -> [Name] -> Name
forall a b. (Named a, Named b) => a -> [b] -> Name
variant Name
ifeqName [Type -> Name
forall a. Named a => a -> Name
name Type
ty1, Type -> Name
forall a. Named a => a -> Name
name Type
ty2] Name -> FunType -> Name ::: FunType
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType [Type
ty1, Type
ty1, Type
ty2] Type
ty2)
          if HornFlags -> Bool
passivise HornFlags
flags then do
            (String, Atomic)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a r s.
(MonadTrans t, Monad m) =>
a -> t (RWST r [a] s m) ()
axiom (String
tag, Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
x, Term
x, Term -> Term
passive Term
c] Term -> Term -> Atomic
:=: Term
c)
            (String, Atomic)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a r s.
(MonadTrans t, Monad m) =>
a -> t (RWST r [a] s m) ()
axiom (String
tag, Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
x, Term
x, Term -> Term
passive Term
d] Term -> Term -> Atomic
:=: Term
d)
            Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
a, Term
b, Term -> Term
passive Term
c] Term -> Term -> Atomic
:=: Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
a, Term
b, Term -> Term
passive Term
d])
           else do
            (String, Atomic)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a r s.
(MonadTrans t, Monad m) =>
a -> t (RWST r [a] s m) ()
axiom (String
"ifeq_axiom", Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
x, Term
x, Term
y] Term -> Term -> Atomic
:=: Term
y)
            Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
a, Term
b, Term
c] Term -> Term -> Atomic
:=: Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
a, Term
b, Term
d])
        -- ifeq(x, x, y, z) = y
        -- ifeq(a, b, c, d) = d
        Encoding
Asymmetric1 -> do
          Name ::: FunType
ifeq <- (Name ::: FunType)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause)))
     (Name ::: FunType)
forall (t :: (* -> *) -> * -> *) w a (m :: * -> *) r b.
(MonadTrans t, Monoid w, Num a, Show a, Monad m,
 Monad (t (RWST r w a m))) =>
(Name ::: b) -> t (RWST r w a m) (Name ::: b)
passiveFresh (Name -> [Name] -> Name
forall a b. (Named a, Named b) => a -> [b] -> Name
variant Name
ifeqName [Type -> Name
forall a. Named a => a -> Name
name Type
ty1, Type -> Name
forall a. Named a => a -> Name
name Type
ty2] Name -> FunType -> Name ::: FunType
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType [Type
ty1, Type
ty1, Type
ty2, Type
ty2] Type
ty2)
          (Term
c :=: Term
d) <- Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> Int) -> Atomic -> Atomic
forall a. Ord a => (Term -> a) -> Atomic -> Atomic
swap Term -> Int
size (Term
c Term -> Term -> Atomic
:=: Term
d))
          if HornFlags -> Bool
passivise HornFlags
flags then do
            (String, Atomic)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a r s.
(MonadTrans t, Monad m) =>
a -> t (RWST r [a] s m) ()
axiom (String
"ifeq_axiom", Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
x, Term
x, Term -> Term
passive Term
c, Term
y] Term -> Term -> Atomic
:=: Term
c)
            Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
a, Term
b, Term -> Term
passive Term
c, Term -> Term
passive Term
d] Term -> Term -> Atomic
:=: Term
d)
           else do
            (String, Atomic)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a r s.
(MonadTrans t, Monad m) =>
a -> t (RWST r [a] s m) ()
axiom (String
"ifeq_axiom", Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
x, Term
x, Term
y, Term
z] Term -> Term -> Atomic
:=: Term
y)
            Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: [Term
a, Term
b, Term
c, Term
d] Term -> Term -> Atomic
:=: Term
d)
        -- f(a, sigma) = c
        -- f(b, sigma) = d
        -- where sigma = FV(a, b, c, d)
        Encoding
Asymmetric2 -> do
          Name
ifeqName <- Name
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Name
forall (t :: (* -> *) -> * -> *) w (m :: * -> *) a a r.
(MonadTrans t, Monoid w, Monad m, Num a, Named a, Show a) =>
a -> t (RWST r w a m) Name
fresh Name
freshName
          (Term
a :=: Term
b) <- Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> Int) -> Atomic -> Atomic
forall a. Ord a => (Term -> a) -> Atomic -> Atomic
swap Term -> Int
size (Term
a Term -> Term -> Atomic
:=: Term
b))
          (Term
c :=: Term
d) <- Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> Int) -> Atomic -> Atomic
forall a. Ord a => (Term -> a) -> Atomic -> Atomic
swap Term -> Int
size (Term
c Term -> Term -> Atomic
:=: Term
d))
          let
            vs :: [Term]
vs =
              if HornFlags -> Bool
passivise HornFlags
flags then
                (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
passive [Term
a, Term
b, Term
c, Term
d]
              else
                (Variable -> Term) -> [Variable] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Term
Var (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList ([Set Variable] -> Set Variable
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((Term -> Set Variable) -> [Term] -> [Set Variable]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Set Variable
forall a. Symbolic a => a -> Set Variable
free [Term
a, Term
b, Term
c, Term
d])))
            ifeq :: Name ::: FunType
ifeq = Name
ifeqName Name -> FunType -> Name ::: FunType
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType (Type
ty1Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:(Term -> Type) -> [Term] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Type
forall a. Typed a => a -> Type
typ [Term]
vs) Type
ty2
            app :: Term -> Term
app Term
t = Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: (Term
tTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
vs)
          if HornFlags -> Bool
smaller HornFlags
flags then do
            (String, Atomic)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a r s.
(MonadTrans t, Monad m) =>
a -> t (RWST r [a] s m) ()
axiom (String
tag, Term -> Term
app Term
b Term -> Term -> Atomic
:=: Term
d)
            Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
app Term
a Term -> Term -> Atomic
:=: Term
c)
           else do
            (String, Atomic)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a r s.
(MonadTrans t, Monad m) =>
a -> t (RWST r [a] s m) ()
axiom (String
tag, Term -> Term
app Term
a Term -> Term -> Atomic
:=: Term
c)
            Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
app Term
b Term -> Term -> Atomic
:=: Term
d)
        -- f(a, b, sigma) = c
        -- f(x, x, sigma) = d
        -- where sigma = FV(c, d)
        Encoding
Asymmetric3 -> do
          Name
ifeqName <- Name
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Name
forall (t :: (* -> *) -> * -> *) w (m :: * -> *) a a r.
(MonadTrans t, Monoid w, Monad m, Num a, Named a, Show a) =>
a -> t (RWST r w a m) Name
fresh Name
freshName
          (Term
c :=: Term
d) <- Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> Int) -> Atomic -> Atomic
forall a. Ord a => (Term -> a) -> Atomic -> Atomic
swap Term -> Int
size (Term
c Term -> Term -> Atomic
:=: Term
d))
          let
            vs :: [Term]
vs =
              if HornFlags -> Bool
passivise HornFlags
flags then
                (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
passive [Term
c, Term
d]
              else
                (Variable -> Term) -> [Variable] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Term
Var (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList ([Set Variable] -> Set Variable
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((Term -> Set Variable) -> [Term] -> [Set Variable]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Set Variable
forall a. Symbolic a => a -> Set Variable
free [Term
c, Term
d])))
            ifeq :: Name ::: FunType
ifeq = Name
ifeqName Name -> FunType -> Name ::: FunType
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType (Type
ty1Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:Type
ty1Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:(Term -> Type) -> [Term] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Type
forall a. Typed a => a -> Type
typ [Term]
vs) Type
ty2
            app :: Term -> Term -> Term
app Term
t Term
u = Name ::: FunType
ifeq (Name ::: FunType) -> [Term] -> Term
:@: (Term
tTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:Term
uTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
vs)
            x :: Term
x = Variable -> Term
Var (Name
xvar Name -> Type -> Variable
forall a b. a -> b -> a ::: b
::: Type
ty1)
          (String, Atomic)
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a r s.
(MonadTrans t, Monad m) =>
a -> t (RWST r [a] s m) ()
axiom (String
tag, Term -> Term -> Term
app Term
x Term
x Term -> Term -> Atomic
:=: Term
c)
          Atomic
-> ListT
     (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
app Term
a Term
b Term -> Term -> Atomic
:=: Term
d)

    swap :: (Term -> a) -> Atomic -> Atomic
swap Term -> a
f (Term
t :=: Term
u) =
      (\(Term
t :=: Term
u) -> if HornFlags -> Bool
smaller HornFlags
flags then Term
u Term -> Term -> Atomic
:=: Term
t else Term
t Term -> Term -> Atomic
:=: Term
u) (Atomic -> Atomic) -> Atomic -> Atomic
forall a b. (a -> b) -> a -> b
$
      if Term -> a
f Term
t a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= Term -> a
f Term
u then (Term
t Term -> Term -> Atomic
:=: Term
u) else (Term
u Term -> Term -> Atomic
:=: Term
t)

    axiom :: a -> t (RWST r [a] s m) ()
axiom a
l = RWST r [a] s m () -> t (RWST r [a] s m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RWST r [a] s m () -> t (RWST r [a] s m) ())
-> RWST r [a] s m () -> t (RWST r [a] s m) ()
forall a b. (a -> b) -> a -> b
$ [a] -> RWST r [a] s m ()
forall (m :: * -> *) w r s. Monad m => w -> RWST r w s m ()
tell [a
l]

    toInput :: (String, Atomic) -> Input Clause
toInput (String
tag, Atomic
l) =
      Input :: forall a. String -> Kind -> InputSource -> a -> Input a
Input {
        tag :: String
tag = String
tag,
        kind :: Kind
kind = AxKind -> Kind
Ax AxKind
Axiom,
        source :: InputSource
source = InputSource
Unknown,
        what :: Clause
what = [Literal] -> Clause
clause [Atomic -> Literal
forall a. a -> Signed a
Pos Atomic
l] }

    (Name
ifeqName, Name
freshName, Name
passiveName, Name
xvar, Name
yvar, Name
zvar) = Problem Clause
-> NameM (Name, Name, Name, Name, Name, Name)
-> (Name, Name, Name, Name, Name, Name)
forall a b. Symbolic a => a -> NameM b -> b
run_ Problem Clause
prob (NameM (Name, Name, Name, Name, Name, Name)
 -> (Name, Name, Name, Name, Name, Name))
-> NameM (Name, Name, Name, Name, Name, Name)
-> (Name, Name, Name, Name, Name, Name)
forall a b. (a -> b) -> a -> b
$ do
      Name
ifeqName <- Name -> NameM Name
forall a. Named a => a -> NameM Name
newName (String -> Name -> Name
withLabel String
"ifeq" (String -> Name
forall a. Named a => a -> Name
name String
"ifeq"))
      Name
freshName <- Name -> NameM Name
forall a. Named a => a -> NameM Name
newName (String -> Name -> Name
withLabel String
"fresh" (String -> Name
forall a. Named a => a -> Name
name String
"fresh"))
      Name
passiveName <- Name -> NameM Name
forall a. Named a => a -> NameM Name
newName (String -> Name -> Name
withLabel String
"passive" (String -> Name
forall a. Named a => a -> Name
name String
"passive"))
      Name
xvar <- String -> NameM Name
forall a. Named a => a -> NameM Name
newName String
"A"
      Name
yvar <- String -> NameM Name
forall a. Named a => a -> NameM Name
newName String
"B"
      Name
zvar <- String -> NameM Name
forall a. Named a => a -> NameM Name
newName String
"C"
      (Name, Name, Name, Name, Name, Name)
-> NameM (Name, Name, Name, Name, Name, Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
ifeqName, Name
freshName, Name
passiveName, Name
xvar, Name
yvar, Name
zvar)

-- Soundly encode types, but try to erase them if possible.
-- Based on the observation that if the input problem is untyped,
-- erasure is sound unless:
--   * the problem is satisfiable
--   * but the only model is of size 1.
-- We therefore check if there is a model of size 1. This is easy
-- (the term structure collapses), and if so, we return the SZS
-- status directly instead.
encodeTypesSmartly :: Problem Clause -> IO (Either Answer (Problem Clause -> Problem Clause))
encodeTypesSmartly :: Problem Clause
-> IO (Either Answer (Problem Clause -> Problem Clause))
encodeTypesSmartly Problem Clause
prob
  | Problem Clause -> Bool
forall a. Symbolic a => a -> Bool
isFof Problem Clause
prob = do
    Bool
sat <- Problem Clause -> IO Bool
hasSizeOneModel Problem Clause
prob
    if Bool
sat then
      Either Answer (Problem Clause -> Problem Clause)
-> IO (Either Answer (Problem Clause -> Problem Clause))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Answer (Problem Clause -> Problem Clause)
 -> IO (Either Answer (Problem Clause -> Problem Clause)))
-> Either Answer (Problem Clause -> Problem Clause)
-> IO (Either Answer (Problem Clause -> Problem Clause))
forall a b. (a -> b) -> a -> b
$ Answer -> Either Answer (Problem Clause -> Problem Clause)
forall a b. a -> Either a b
Left (Answer -> Either Answer (Problem Clause -> Problem Clause))
-> Answer -> Either Answer (Problem Clause -> Problem Clause)
forall a b. (a -> b) -> a -> b
$
        SatReason -> Maybe [String] -> Answer
Sat SatReason
Satisfiable (Maybe [String] -> Answer) -> Maybe [String] -> Answer
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just
         [String
"There is a model where all terms are equal, ![X,Y]:X=Y."]
      else Either Answer (Problem Clause -> Problem Clause)
-> IO (Either Answer (Problem Clause -> Problem Clause))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Problem Clause -> Problem Clause)
-> Either Answer (Problem Clause -> Problem Clause)
forall a b. b -> Either a b
Right Problem Clause -> Problem Clause
forall a. Symbolic a => a -> a
eraseTypes)
  | Bool
otherwise =
    Either Answer (Problem Clause -> Problem Clause)
-> IO (Either Answer (Problem Clause -> Problem Clause))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Problem Clause -> Problem Clause)
-> Either Answer (Problem Clause -> Problem Clause)
forall a b. b -> Either a b
Right Problem Clause -> Problem Clause
forall a. a -> a
id)

-- Check if a problem has a model of size 1.
-- Done by erasing all terms from the problem.
hasSizeOneModel :: Problem Clause -> IO Bool
hasSizeOneModel :: Problem Clause -> IO Bool
hasSizeOneModel Problem Clause
p = do
  Solver
s <- IO Solver
Sat.newSolver
  let funs :: [Name ::: FunType]
funs = Problem Clause -> [Name ::: FunType]
forall a. Symbolic a => a -> [Name ::: FunType]
functions Problem Clause
p
  [Lit]
lits <- Int -> IO Lit -> IO [Lit]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([Name ::: FunType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name ::: FunType]
funs) (Solver -> IO Lit
forall s. SatSolver s => s -> IO Lit
Sat.newLit Solver
s)
  let
    funMap :: Map (Name ::: FunType) Lit
funMap = [(Name ::: FunType, Lit)] -> Map (Name ::: FunType) Lit
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Name ::: FunType] -> [Lit] -> [(Name ::: FunType, Lit)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name ::: FunType]
funs [Lit]
lits)
    transClause :: Clause -> [Lit]
transClause (Clause (Bind Set Variable
_ [Literal]
ls)) =
      (Literal -> Lit) -> [Literal] -> [Lit]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> Lit
transLit [Literal]
ls
    transLit :: Literal -> Lit
transLit (Pos Atomic
a) = Atomic -> Lit
transAtom Atomic
a
    transLit (Neg Atomic
a) = Lit -> Lit
Sat.neg (Atomic -> Lit
transAtom Atomic
a)
    transAtom :: Atomic -> Lit
transAtom (Tru (Name ::: FunType
p :@: [Term]
_)) =
      Lit -> (Name ::: FunType) -> Map (Name ::: FunType) Lit -> Lit
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Lit
forall a. HasCallStack => a
undefined Name ::: FunType
p Map (Name ::: FunType) Lit
funMap
    transAtom (Term
_ :=: Term
_) = Lit
Sat.true
  (Clause -> IO ()) -> [Clause] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> IO ()
Sat.addClause Solver
s ([Lit] -> IO ()) -> (Clause -> [Lit]) -> Clause -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Lit]
transClause) ((Input Clause -> Clause) -> Problem Clause -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Input Clause -> Clause
forall a. Input a -> a
what Problem Clause
p)
  Solver -> [Lit] -> IO Bool
forall s. SatSolver s => s -> [Lit] -> IO Bool
Sat.solve Solver
s [] IO Bool -> IO () -> IO Bool
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Solver -> IO ()
Sat.deleteSolver Solver
s