{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE LambdaCase  #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE TupleSections  #-}
module Language.Fixpoint.Horn.Transformations (
    uniq
  , flatten
  , elim
  , elimPis
  , solveEbs
  , cstrToExpr
) where

import           Language.Fixpoint.Horn.Types
import           Language.Fixpoint.Horn.Info
import           Language.Fixpoint.Smt.Theories as F
import qualified Language.Fixpoint.Types      as F
import qualified Language.Fixpoint.Types.Config as F
import           Language.Fixpoint.Graph      as FG
import qualified Data.HashMap.Strict          as M
import           Data.String                  (IsString (..))
import           Data.Either                  (partitionEithers, rights)
import           Data.List                    (nub)
import qualified Data.Set                     as S
import qualified Data.HashSet                 as HS
import qualified Data.Graph                   as DG
import           Control.Monad.State
import           Data.Maybe                   (catMaybes, mapMaybe, fromMaybe)
import           Language.Fixpoint.Types.Visitor as V
import           System.Console.CmdArgs.Verbosity
import           Data.Bifunctor (second)
import System.IO (hFlush, stdout)
-- import qualified Debug.Trace as DBG

-- $setup
-- >>> :l src/Language/Fixpoint/Horn/Transformations.hs src/Language/Fixpoint/Horn/Parse.hs
-- >>> :m + *Language.Fixpoint.Horn.Parse
-- >>> import Language.Fixpoint.Parse
-- >>> :set -XOverloadedStrings

---------------
-- Debugging
---------------
trace :: String -> a -> a
-- trace _msg v = DBG.trace _msg v
trace :: String -> a -> a
trace String
_msg a
v = a
v

printPiSols :: (F.PPrint a1, F.PPrint a2, F.PPrint a3) =>
               M.HashMap a1 ((a4, a2), a3) -> IO ()
printPiSols :: HashMap a1 ((a4, a2), a3) -> IO ()
printPiSols HashMap a1 ((a4, a2), a3)
piSols =
  [IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([IO ()] -> IO ()) -> [IO ()] -> IO ()
forall a b. (a -> b) -> a -> b
$ ((\(a1
piVar, ((a4
_, a2
args), a3
cstr)) -> do
                  String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ a1 -> String
forall a. PPrint a => a -> String
F.showpp a1
piVar
                  String -> IO ()
putStr String
" := "
                  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ a2 -> String
forall a. PPrint a => a -> String
F.showpp a2
args
                  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ a3 -> String
forall a. PPrint a => a -> String
F.showpp a3
cstr
                  String -> IO ()
putStr String
"\n"
                  Handle -> IO ()
hFlush Handle
stdout) ((a1, ((a4, a2), a3)) -> IO ())
-> [(a1, ((a4, a2), a3))] -> [IO ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap a1 ((a4, a2), a3) -> [(a1, ((a4, a2), a3))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap a1 ((a4, a2), a3)
piSols)
---------------

-- type Sol a = M.HashMap F.Symbol (Either (Either [[Bind]] (Cstr a)) F.Expr)

-- | solveEbs takes a query and returns a query with the ebinds solved out
--
-- it has some preconditions
-- - pi -> k -> pi structure. That is, there are no cycles, and while ks
-- can depend on other ks, pis cannot directly depend on other pis
-- - predicate for exists binder is `true`. (TODO: is this pre stale?)

solveEbs :: (F.PPrint a) => F.Config -> Query a -> IO (Query a)
------------------------------------------------------------------------------
solveEbs :: Config -> Query a -> IO (Query a)
solveEbs Config
cfg query :: Query a
query@(Query [Qualifier]
qs [Var a]
vs Cstr a
c HashMap Symbol Sort
cons HashMap Symbol Sort
dist) = do
  -- clean up
  let normalizedC :: Cstr a
normalizedC = Cstr a -> Cstr a
forall a. Flatten a => a -> a
flatten (Cstr a -> Cstr a) -> (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
pruneTauts (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
hornify Cstr a
c
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Normalized EHC:"
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
normalizedC

  -- short circuit if no ebinds are present
  if Cstr a -> Bool
forall a. Cstr a -> Bool
isNNF Cstr a
c then Query a -> IO (Query a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Query a -> IO (Query a)) -> Query a -> IO (Query a)
forall a b. (a -> b) -> a -> b
$ [Qualifier]
-> [Var a]
-> Cstr a
-> HashMap Symbol Sort
-> HashMap Symbol Sort
-> Query a
forall a.
[Qualifier]
-> [Var a]
-> Cstr a
-> HashMap Symbol Sort
-> HashMap Symbol Sort
-> Query a
Query [Qualifier]
qs [Var a]
vs Cstr a
normalizedC HashMap Symbol Sort
cons HashMap Symbol Sort
dist else do
  let kvars :: Set Symbol
kvars = Cstr a -> Set Symbol
forall a. Cstr a -> Set Symbol
boundKvars Cstr a
normalizedC

  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Skolemized:"
  let poked :: Cstr a
poked = Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
pokec Cstr a
normalizedC
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
poked

  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Skolemized + split:"
  let (Just Cstr a
_horn, Just Cstr a
_side) = Cstr a -> (Maybe (Cstr a), Maybe (Cstr a))
forall a. Cstr a -> (Maybe (Cstr a), Maybe (Cstr a))
split Cstr a
poked
  let horn :: Cstr a
horn = Cstr a -> Cstr a
forall a. Flatten a => a -> a
flatten (Cstr a -> Cstr a) -> (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
pruneTauts (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Cstr a
_horn
  let side :: Cstr a
side = Cstr a -> Cstr a
forall a. Flatten a => a -> a
flatten (Cstr a -> Cstr a) -> (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
pruneTauts (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Cstr a
_side
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ (Cstr a, Cstr a) -> String
forall a. PPrint a => a -> String
F.showpp (Cstr a
horn, Cstr a
side)

  -- collect predicate variables
  let pivars :: Set Symbol
pivars = Cstr a -> Set Symbol
forall a. Cstr a -> Set Symbol
boundKvars Cstr a
poked Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set Symbol
kvars

  let cuts :: Set Symbol
cuts = Config -> Query a -> Cstr a -> Set Symbol
forall a. Config -> Query a -> Cstr a -> Set Symbol
calculateCuts Config
cfg Query a
query (Set Symbol -> Cstr a -> Cstr a
forall a. Set Symbol -> Cstr a -> Cstr a
forgetPiVars Set Symbol
pivars Cstr a
horn)
  let acyclicKs :: Set Symbol
acyclicKs = Set Symbol
kvars Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set Symbol
cuts

  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"solved acyclic kvars:"
  let (Cstr a
horn', Cstr a
side') = [Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
forall a. [Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
elimKs' (Set Symbol -> [Symbol]
forall a. Set a -> [a]
S.toList Set Symbol
acyclicKs) (Cstr a
horn, Cstr a
side)
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
horn'
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
side'

  -- if not $ S.null cuts then error $ F.showpp $ S.toList cuts else pure ()
  let elimCutK :: Symbol -> Cstr a -> Cstr a
elimCutK Symbol
k Cstr a
c = Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
forall a. Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [] Cstr a
c
  Cstr a
horn' <- Cstr a -> IO (Cstr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cstr a -> IO (Cstr a)) -> Cstr a -> IO (Cstr a)
forall a b. (a -> b) -> a -> b
$ (Symbol -> Cstr a -> Cstr a) -> Cstr a -> Set Symbol -> Cstr a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Symbol -> Cstr a -> Cstr a
forall a. Symbol -> Cstr a -> Cstr a
elimCutK Cstr a
horn' Set Symbol
cuts
  Cstr a
side' <- Cstr a -> IO (Cstr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cstr a -> IO (Cstr a)) -> Cstr a -> IO (Cstr a)
forall a b. (a -> b) -> a -> b
$ (Symbol -> Cstr a -> Cstr a) -> Cstr a -> Set Symbol -> Cstr a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Symbol -> Cstr a -> Cstr a
forall a. Symbol -> Cstr a -> Cstr a
elimCutK Cstr a
side' Set Symbol
cuts

  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"pi defining constraints:"
  let piSols :: HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols = [(Symbol, ((Symbol, [Symbol]), Cstr a))]
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, ((Symbol, [Symbol]), Cstr a))]
 -> HashMap Symbol ((Symbol, [Symbol]), Cstr a))
-> [(Symbol, ((Symbol, [Symbol]), Cstr a))]
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
forall a b. (a -> b) -> a -> b
$ (Symbol -> (Symbol, ((Symbol, [Symbol]), Cstr a)))
-> [Symbol] -> [(Symbol, ((Symbol, [Symbol]), Cstr a))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Symbol
pivar -> (Symbol
pivar, Symbol -> Cstr a -> ((Symbol, [Symbol]), Cstr a)
forall a. Symbol -> Cstr a -> ((Symbol, [Symbol]), Cstr a)
piDefConstr Symbol
pivar Cstr a
horn')) (Set Symbol -> [Symbol]
forall a. Set a -> [a]
S.toList Set Symbol
pivars)
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ HashMap Symbol ((Symbol, [Symbol]), Cstr a) -> IO ()
forall a1 a2 a3 a4.
(PPrint a1, PPrint a2, PPrint a3) =>
HashMap a1 ((a4, a2), a3) -> IO ()
printPiSols HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols

  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"solved pis:"
  let solvedPiCstrs :: HashMap Symbol Pred
solvedPiCstrs = Set Symbol
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> HashMap Symbol Pred
forall a.
Set Symbol
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> HashMap Symbol Pred
solPis ([Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
S.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ HashMap Symbol Sort -> [Symbol]
forall k v. HashMap k v -> [k]
M.keys HashMap Symbol Sort
cons [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ HashMap Symbol Sort -> [Symbol]
forall k v. HashMap k v -> [k]
M.keys HashMap Symbol Sort
dist) HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ HashMap Symbol Pred -> String
forall a. PPrint a => a -> String
F.showpp HashMap Symbol Pred
solvedPiCstrs

  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"solved horn:"
  let solvedHorn :: Cstr a
solvedHorn = HashMap Symbol Pred -> Cstr a -> Cstr a
forall a. HashMap Symbol Pred -> Cstr a -> Cstr a
substPiSols HashMap Symbol Pred
solvedPiCstrs Cstr a
horn'
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
solvedHorn

  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"solved side:"
  let solvedSide :: Cstr a
solvedSide = HashMap Symbol Pred -> Cstr a -> Cstr a
forall a. HashMap Symbol Pred -> Cstr a -> Cstr a
substPiSols HashMap Symbol Pred
solvedPiCstrs Cstr a
side'
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
solvedSide

  Query a -> IO (Query a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Query a -> IO (Query a)) -> Query a -> IO (Query a)
forall a b. (a -> b) -> a -> b
$ ([Qualifier]
-> [Var a]
-> Cstr a
-> HashMap Symbol Sort
-> HashMap Symbol Sort
-> Query a
forall a.
[Qualifier]
-> [Var a]
-> Cstr a
-> HashMap Symbol Sort
-> HashMap Symbol Sort
-> Query a
Query [Qualifier]
qs [Var a]
vs ([Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd [Cstr a
solvedHorn, Cstr a
solvedSide]) HashMap Symbol Sort
cons HashMap Symbol Sort
dist)

-- | Collects the defining constraint for π
-- that is, given `∀ Γ.∀ n.π => c`, returns `((π, n:Γ), c)`
piDefConstr :: F.Symbol -> Cstr a -> ((F.Symbol, [F.Symbol]), Cstr a)
piDefConstr :: Symbol -> Cstr a -> ((Symbol, [Symbol]), Cstr a)
piDefConstr Symbol
k Cstr a
c = (([Symbol] -> Symbol
forall a. [a] -> a
head [Symbol]
ns, [[Symbol]] -> [Symbol]
forall a. [a] -> a
head [[Symbol]]
formals), Cstr a
defC)
  where
    ([Symbol]
ns, [[Symbol]]
formals, Cstr a
defC) = case Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a))
forall a. Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a))
go Cstr a
c of
      ([Symbol]
ns, [[Symbol]]
formals, Just Cstr a
defC) -> ([Symbol]
ns, [[Symbol]]
formals, Cstr a
defC)
      ([Symbol]
_, [[Symbol]]
_, Maybe (Cstr a)
Nothing) -> String -> ([Symbol], [[Symbol]], Cstr a)
forall a. HasCallStack => String -> a
error (String -> ([Symbol], [[Symbol]], Cstr a))
-> String -> ([Symbol], [[Symbol]], Cstr a)
forall a b. (a -> b) -> a -> b
$ String
"pi variable " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
k String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" has no defining constraint."

    go :: Cstr a -> ([F.Symbol], [[F.Symbol]], Maybe (Cstr a))
    go :: Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a))
go (CAnd [Cstr a]
cs) = (\([[Symbol]]
as, [[[Symbol]]]
bs, [Maybe (Cstr a)]
cs) -> ([[Symbol]] -> [Symbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Symbol]]
as, [[[Symbol]]] -> [[Symbol]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Symbol]]]
bs, [Maybe (Cstr a)] -> Maybe (Cstr a)
forall a. [Maybe (Cstr a)] -> Maybe (Cstr a)
cAndMaybes [Maybe (Cstr a)]
cs)) (([[Symbol]], [[[Symbol]]], [Maybe (Cstr a)])
 -> ([Symbol], [[Symbol]], Maybe (Cstr a)))
-> ([[Symbol]], [[[Symbol]]], [Maybe (Cstr a)])
-> ([Symbol], [[Symbol]], Maybe (Cstr a))
forall a b. (a -> b) -> a -> b
$ [([Symbol], [[Symbol]], Maybe (Cstr a))]
-> ([[Symbol]], [[[Symbol]]], [Maybe (Cstr a)])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([([Symbol], [[Symbol]], Maybe (Cstr a))]
 -> ([[Symbol]], [[[Symbol]]], [Maybe (Cstr a)]))
-> [([Symbol], [[Symbol]], Maybe (Cstr a))]
-> ([[Symbol]], [[[Symbol]]], [Maybe (Cstr a)])
forall a b. (a -> b) -> a -> b
$ Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a))
forall a. Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a))
go (Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a)))
-> [Cstr a] -> [([Symbol], [[Symbol]], Maybe (Cstr a))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
    go (All b :: Bind
b@(Bind Symbol
n Sort
_ (Var Symbol
k' [Symbol]
xs)) Cstr a
c')
      | Symbol
k Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
k' = ([Symbol
n], [Set Symbol -> [Symbol]
forall a. Set a -> [a]
S.toList (Set Symbol -> [Symbol]) -> Set Symbol -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
S.fromList [Symbol]
xs Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Symbol -> Set Symbol
forall a. a -> Set a
S.singleton Symbol
n], Cstr a -> Maybe (Cstr a)
forall a. a -> Maybe a
Just Cstr a
c')
      | Bool
otherwise = (Maybe (Cstr a) -> Maybe (Cstr a))
-> ([Symbol], [[Symbol]], Maybe (Cstr a))
-> ([Symbol], [[Symbol]], Maybe (Cstr a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Cstr a -> Cstr a) -> Maybe (Cstr a) -> Maybe (Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b)) (Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a))
forall a. Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a))
go Cstr a
c')
    go (All Bind
b Cstr a
c') = (Maybe (Cstr a) -> Maybe (Cstr a))
-> ([Symbol], [[Symbol]], Maybe (Cstr a))
-> ([Symbol], [[Symbol]], Maybe (Cstr a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Cstr a -> Cstr a) -> Maybe (Cstr a) -> Maybe (Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b)) (Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a))
forall a. Cstr a -> ([Symbol], [[Symbol]], Maybe (Cstr a))
go Cstr a
c')
    go Cstr a
_ = ([], [], Maybe (Cstr a)
forall a. Maybe a
Nothing)

    cAndMaybes :: [Maybe (Cstr a)] -> Maybe (Cstr a)
    cAndMaybes :: [Maybe (Cstr a)] -> Maybe (Cstr a)
cAndMaybes [Maybe (Cstr a)]
maybeCs = case [Maybe (Cstr a)] -> [Cstr a]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Cstr a)]
maybeCs of
      [] -> Maybe (Cstr a)
forall a. Maybe a
Nothing
      [Cstr a]
cs -> Cstr a -> Maybe (Cstr a)
forall a. a -> Maybe a
Just (Cstr a -> Maybe (Cstr a)) -> Cstr a -> Maybe (Cstr a)
forall a b. (a -> b) -> a -> b
$ [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd [Cstr a]
cs

#if !MIN_VERSION_base(4,14,0)
instance Functor ((,,) a b) where
    fmap f (a, b, c) = (a, b, f c)
#endif

-- | Solve out the given pivars
solPis :: S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> M.HashMap F.Symbol Pred
solPis :: Set Symbol
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> HashMap Symbol Pred
solPis Set Symbol
measures HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols = [(Symbol, ((Symbol, [Symbol]), Cstr a))]
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> HashMap Symbol Pred
forall a.
[(Symbol, ((Symbol, [Symbol]), Cstr a))]
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> HashMap Symbol Pred
go (HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> [(Symbol, ((Symbol, [Symbol]), Cstr a))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols) HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols
  where
    go :: [(Symbol, ((Symbol, [Symbol]), Cstr a))]
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> HashMap Symbol Pred
go ((Symbol
pi, ((Symbol
n, [Symbol]
xs), Cstr a
c)):[(Symbol, ((Symbol, [Symbol]), Cstr a))]
pis) HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols = Symbol -> Pred -> HashMap Symbol Pred -> HashMap Symbol Pred
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
pi Pred
solved (HashMap Symbol Pred -> HashMap Symbol Pred)
-> HashMap Symbol Pred -> HashMap Symbol Pred
forall a b. (a -> b) -> a -> b
$ [(Symbol, ((Symbol, [Symbol]), Cstr a))]
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> HashMap Symbol Pred
go [(Symbol, ((Symbol, [Symbol]), Cstr a))]
pis HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols
      where solved :: Pred
solved = Set Symbol
-> Symbol
-> Symbol
-> Set Symbol
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> Cstr a
-> Pred
forall a.
Set Symbol
-> Symbol
-> Symbol
-> Set Symbol
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> Cstr a
-> Pred
solPi Set Symbol
measures Symbol
pi Symbol
n ([Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
S.fromList [Symbol]
xs) HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols Cstr a
c
    go [] HashMap Symbol ((Symbol, [Symbol]), Cstr a)
_ = HashMap Symbol Pred
forall a. Monoid a => a
mempty

-- TODO: rewrite to use CC
solPi :: S.Set F.Symbol -> F.Symbol -> F.Symbol -> S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> Cstr a -> Pred
solPi :: Set Symbol
-> Symbol
-> Symbol
-> Set Symbol
-> HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> Cstr a
-> Pred
solPi Set Symbol
measures Symbol
basePi Symbol
n Set Symbol
args HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols Cstr a
c = String -> Pred -> Pred
forall a. String -> a -> a
trace (String
"\n\nsolPi: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
basePi String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
n String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [Symbol] -> String
forall a. PPrint a => a -> String
F.showpp (Set Symbol -> [Symbol]
forall a. Set a -> [a]
S.toList Set Symbol
args) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [((Symbol, [Expr]), [Symbol])] -> String
forall a. PPrint a => a -> String
F.showpp ((\((Symbol, [Expr])
a, Symbol
_, [Symbol]
c) -> ((Symbol, [Expr])
a, [Symbol]
c)) (((Symbol, [Expr]), Symbol, [Symbol])
 -> ((Symbol, [Expr]), [Symbol]))
-> [((Symbol, [Expr]), Symbol, [Symbol])]
-> [((Symbol, [Expr]), [Symbol])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((Symbol, [Expr]), Symbol, [Symbol])]
edges) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [Expr] -> String
forall a. PPrint a => a -> String
F.showpp (Symbol -> [Expr]
sols Symbol
n) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [Pred] -> String
forall a. PPrint a => a -> String
F.showpp [Pred]
rewritten String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
c String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n\n") (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ [Pred] -> Pred
PAnd ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ [Pred]
rewritten
  where
    rewritten :: [Pred]
rewritten = Set Symbol -> Symbol -> Set Symbol -> [(Symbol, Expr)] -> [Pred]
rewriteWithEqualities Set Symbol
measures Symbol
n Set Symbol
args [(Symbol, Expr)]
equalities
    equalities :: [(Symbol, Expr)]
equalities = ([(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. Eq a => [a] -> [a]
nub ([(Symbol, Expr)] -> [(Symbol, Expr)])
-> (([(Symbol, Expr)], Set Symbol) -> [(Symbol, Expr)])
-> ([(Symbol, Expr)], Set Symbol)
-> [(Symbol, Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Symbol, Expr)], Set Symbol) -> [(Symbol, Expr)]
forall a b. (a, b) -> a
fst) (([(Symbol, Expr)], Set Symbol) -> [(Symbol, Expr)])
-> ([(Symbol, Expr)], Set Symbol) -> [(Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
forall a. Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
go (Symbol -> Set Symbol
forall a. a -> Set a
S.singleton Symbol
basePi) Cstr a
c
    edges :: [((Symbol, [Expr]), Symbol, [Symbol])]
edges = Set Symbol
-> HashMap Symbol ([Symbol], [Expr])
-> [(Symbol, Expr)]
-> [((Symbol, [Expr]), Symbol, [Symbol])]
eqEdges Set Symbol
args HashMap Symbol ([Symbol], [Expr])
forall a. Monoid a => a
mempty [(Symbol, Expr)]
equalities
    (Graph
eGraph, Vertex -> ((Symbol, [Expr]), Symbol, [Symbol])
vf, Symbol -> Maybe Vertex
lookupVertex) = [((Symbol, [Expr]), Symbol, [Symbol])]
-> (Graph, Vertex -> ((Symbol, [Expr]), Symbol, [Symbol]),
    Symbol -> Maybe Vertex)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
DG.graphFromEdges [((Symbol, [Expr]), Symbol, [Symbol])]
edges
    sols :: Symbol -> [Expr]
sols Symbol
x = case Symbol -> Maybe Vertex
lookupVertex Symbol
x of
      Maybe Vertex
Nothing -> []
      Just Vertex
vertex -> [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol -> Expr
F.EVar Symbol
x) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [[Expr]] -> [Expr]
forall a. Monoid a => [a] -> a
mconcat [[Expr]
es | ((Symbol
_, [Expr]
es), Symbol
_, [Symbol]
_) <- Vertex -> ((Symbol, [Expr]), Symbol, [Symbol])
vf (Vertex -> ((Symbol, [Expr]), Symbol, [Symbol]))
-> [Vertex] -> [((Symbol, [Expr]), Symbol, [Symbol])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph -> Vertex -> [Vertex]
DG.reachable Graph
eGraph Vertex
vertex]

    go :: S.Set F.Symbol -> Cstr a -> ([(F.Symbol, F.Expr)], S.Set F.Symbol)
    go :: Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
go Set Symbol
visited (Head Pred
p a
_) = (Pred -> [(Symbol, Expr)]
collectEqualities Pred
p, Set Symbol
visited)
    go Set Symbol
visited (CAnd [Cstr a]
cs) = (([(Symbol, Expr)], Set Symbol)
 -> Cstr a -> ([(Symbol, Expr)], Set Symbol))
-> ([(Symbol, Expr)], Set Symbol)
-> [Cstr a]
-> ([(Symbol, Expr)], Set Symbol)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\([(Symbol, Expr)]
eqs, Set Symbol
visited) Cstr a
c -> let ([(Symbol, Expr)]
eqs', Set Symbol
visited') = Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
forall a. Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
go Set Symbol
visited Cstr a
c in ([(Symbol, Expr)]
eqs' [(Symbol, Expr)] -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. Semigroup a => a -> a -> a
<> [(Symbol, Expr)]
eqs, Set Symbol
visited')) ([(Symbol, Expr)]
forall a. Monoid a => a
mempty, Set Symbol
visited) [Cstr a]
cs
    go Set Symbol
visited (All (Bind Symbol
_ Sort
_ (Var Symbol
pi [Symbol]
_)) Cstr a
c)
      | Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Symbol
pi Set Symbol
visited = Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
forall a. Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
go Set Symbol
visited Cstr a
c
      | Bool
otherwise = let ((Symbol, [Symbol])
_, Cstr a
defC) = (HashMap Symbol ((Symbol, [Symbol]), Cstr a)
piSols HashMap Symbol ((Symbol, [Symbol]), Cstr a)
-> Symbol -> ((Symbol, [Symbol]), Cstr a)
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.! Symbol
pi)
                        ([(Symbol, Expr)]
eqs', Set Symbol
newVisited) = Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
forall a. Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
go (Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
S.insert Symbol
pi Set Symbol
visited) Cstr a
defC
                        ([(Symbol, Expr)]
eqs'', Set Symbol
newVisited') = Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
forall a. Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
go Set Symbol
newVisited Cstr a
c in
          ([(Symbol, Expr)]
eqs' [(Symbol, Expr)] -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. Semigroup a => a -> a -> a
<> [(Symbol, Expr)]
eqs'', Set Symbol
newVisited')
    go Set Symbol
visited (All (Bind Symbol
_ Sort
_ Pred
p) Cstr a
c) = let ([(Symbol, Expr)]
eqs, Set Symbol
visited') = Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
forall a. Set Symbol -> Cstr a -> ([(Symbol, Expr)], Set Symbol)
go Set Symbol
visited Cstr a
c in
      ([(Symbol, Expr)]
eqs [(Symbol, Expr)] -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. Semigroup a => a -> a -> a
<> Pred -> [(Symbol, Expr)]
collectEqualities Pred
p, Set Symbol
visited')
    go Set Symbol
_ Any{} = String -> ([(Symbol, Expr)], Set Symbol)
forall a. HasCallStack => String -> a
error String
"exists should not be present in piSols"

------------------------------------------------------------------------------
{- | pokec skolemizes the EHC into an HC + side condition
>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind01.smt2"
>>> F.pprint $ pokec (qCstr q)
(and
 (forall ((m int) (true))
  (and
   (forall ((x1 int) (πx1 x1))
    (and
     (forall ((v int) (v == m + 1))
      (((v == x1))))
     (forall ((v int) (v == x1 + 1))
      (((v == 2 + m))))))
   (exists ((x1 int) (true))
    ((πx1 x1))))))

>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"
>>> F.pprint $ pokec (qCstr q)
(and
 (forall ((m int) (true))
  (forall ((z int) (z == m - 1))
   (and
    (forall ((v1 int) (v1 == z + 2))
     ((k v1)))
    (and
     (forall ((x1 int) (πx1 x1))
      (and
       (forall ((v2 int) (k v2))
        (((v2 == x1))))
       (forall ((v3 int) (v3 == x1 + 1))
        (((v3 == m + 2))))))
     (exists ((x1 int) (true))
      ((πx1 x1))))))))

>>> let c = doParse' hCstrP "" "(forall ((a Int) (p a)) (exists ((b Int) (q b)) (and (($k a)) (($k b)))))"
>>> F.pprint $ pokec c
(forall ((a int) (p a))
 (and
  (forall ((b int) (πb b))
   (and
    ((k a))
    ((k b))))
  (exists ((b int) (q b))
   ((πb b)))))
-}

pokec :: Cstr a -> Cstr a
pokec :: Cstr a -> Cstr a
pokec = [Symbol] -> Cstr a -> Cstr a
forall a. [Symbol] -> Cstr a -> Cstr a
go [Symbol]
forall a. Monoid a => a
mempty
  where
    go :: [Symbol] -> Cstr a -> Cstr a
go [Symbol]
_ (Head Pred
c a
l) = Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head Pred
c a
l
    go [Symbol]
xs (CAnd [Cstr a]
c)   = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ([Symbol] -> Cstr a -> Cstr a
go [Symbol]
xs (Cstr a -> Cstr a) -> [Cstr a] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
c)
    go [Symbol]
xs (All Bind
b Cstr a
c2) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ [Symbol] -> Cstr a -> Cstr a
go ((Bind -> Symbol
bSym Bind
b)Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs) Cstr a
c2
    go [Symbol]
xs (Any b :: Bind
b@(Bind Symbol
x Sort
t Pred
p) Cstr a
c2) = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd [Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b' (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd [Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head Pred
p a
l, [Symbol] -> Cstr a -> Cstr a
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs) Cstr a
c2], Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
Any Bind
b (Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head Pred
pi a
l)]
      -- TODO: actually use the renamer?
      where
        b' :: Bind
b' = Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t Pred
pi
        pi :: Pred
pi = Symbol -> [Symbol] -> Pred
piVar Symbol
x [Symbol]
xs
        l :: a
l  = Cstr a -> a
forall a. Cstr a -> a
cLabel Cstr a
c2

piVar :: F.Symbol -> [F.Symbol] -> Pred
piVar :: Symbol -> [Symbol] -> Pred
piVar Symbol
x [Symbol]
xs = Symbol -> [Symbol] -> Pred
Var (Symbol -> Symbol
piSym Symbol
x) (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs)

piSym :: F.Symbol -> F.Symbol
piSym :: Symbol -> Symbol
piSym Symbol
s = String -> Symbol
forall a. IsString a => String -> a
fromString (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
"π" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
F.symbolString Symbol
s

{- |

Now we split the poked constraint into the side conditions and the meat of
the constraint

>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind01.smt2"
>>> F.pprint $ qCstr q
(and
 (forall ((m int) (true))
  (exists ((x1 int) (true))
   (and
    (forall ((v int) (v == m + 1))
     (((v == x1))))
    (forall ((v int) (v == x1 + 1))
     (((v == 2 + m))))))))

>>> let (Just noside, Just side) = split $ pokec $ qCstr q
>>> F.pprint side
(forall ((m int) (true))
 (exists ((x1 int) (true))
  ((πx1 x1))))
>>> F.pprint noside
(forall ((m int) (true))
 (forall ((x1 int) (πx1 x1))
  (and
   (forall ((v int) (v == m + 1))
    (((v == x1))))
   (forall ((v int) (v == x1 + 1))
    (((v == 2 + m)))))))


>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"
>>> F.pprint $ qCstr q
(and
 (forall ((m int) (true))
  (forall ((z int) (z == m - 1))
   (and
    (forall ((v1 int) (v1 == z + 2))
     ((k v1)))
    (exists ((x1 int) (true))
     (and
      (forall ((v2 int) (k v2))
       (((v2 == x1))))
      (forall ((v3 int) (v3 == x1 + 1))
       (((v3 == m + 2))))))))))

>>> let (Just noside, Just side) = split $ pokec $ qCstr q
>>> F.pprint side
(forall ((m int) (true))
 (forall ((z int) (z == m - 1))
  (exists ((x1 int) (true))
   ((πx1 x1)))))
>>> F.pprint noside
(forall ((m int) (true))
 (forall ((z int) (z == m - 1))
  (and
   (forall ((v1 int) (v1 == z + 2))
    ((k v1)))
   (forall ((x1 int) (πx1 x1))
    (and
     (forall ((v2 int) (k v2))
      (((v2 == x1))))
     (forall ((v3 int) (v3 == x1 + 1))
      (((v3 == m + 2)))))))))
-}

split :: Cstr a -> (Maybe (Cstr a), Maybe (Cstr a))
split :: Cstr a -> (Maybe (Cstr a), Maybe (Cstr a))
split (CAnd [Cstr a]
cs) = ([Maybe (Cstr a)] -> Maybe (Cstr a)
forall a. [Maybe (Cstr a)] -> Maybe (Cstr a)
andMaybes [Maybe (Cstr a)]
nosides, [Maybe (Cstr a)] -> Maybe (Cstr a)
forall a. [Maybe (Cstr a)] -> Maybe (Cstr a)
andMaybes [Maybe (Cstr a)]
sides)
  where ([Maybe (Cstr a)]
nosides, [Maybe (Cstr a)]
sides) = [(Maybe (Cstr a), Maybe (Cstr a))]
-> ([Maybe (Cstr a)], [Maybe (Cstr a)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Maybe (Cstr a), Maybe (Cstr a))]
 -> ([Maybe (Cstr a)], [Maybe (Cstr a)]))
-> [(Maybe (Cstr a), Maybe (Cstr a))]
-> ([Maybe (Cstr a)], [Maybe (Cstr a)])
forall a b. (a -> b) -> a -> b
$ Cstr a -> (Maybe (Cstr a), Maybe (Cstr a))
forall a. Cstr a -> (Maybe (Cstr a), Maybe (Cstr a))
split (Cstr a -> (Maybe (Cstr a), Maybe (Cstr a)))
-> [Cstr a] -> [(Maybe (Cstr a), Maybe (Cstr a))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
split (All Bind
b Cstr a
c) = (Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b (Cstr a -> Cstr a) -> Maybe (Cstr a) -> Maybe (Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Cstr a)
c', Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b (Cstr a -> Cstr a) -> Maybe (Cstr a) -> Maybe (Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Cstr a)
c'')
    where (Maybe (Cstr a)
c',Maybe (Cstr a)
c'') = Cstr a -> (Maybe (Cstr a), Maybe (Cstr a))
forall a. Cstr a -> (Maybe (Cstr a), Maybe (Cstr a))
split Cstr a
c
split c :: Cstr a
c@Any{} = (Maybe (Cstr a)
forall a. Maybe a
Nothing, Cstr a -> Maybe (Cstr a)
forall a. a -> Maybe a
Just Cstr a
c)
split c :: Cstr a
c@Head{} = (Cstr a -> Maybe (Cstr a)
forall a. a -> Maybe a
Just Cstr a
c, Maybe (Cstr a)
forall a. Maybe a
Nothing)

andMaybes :: [Maybe (Cstr a)] -> Maybe (Cstr a)
andMaybes :: [Maybe (Cstr a)] -> Maybe (Cstr a)
andMaybes [Maybe (Cstr a)]
cs = case [Maybe (Cstr a)] -> [Cstr a]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Cstr a)]
cs of
                 [] -> Maybe (Cstr a)
forall a. Maybe a
Nothing
                 [Cstr a
c] -> Cstr a -> Maybe (Cstr a)
forall a. a -> Maybe a
Just Cstr a
c
                 [Cstr a]
cs -> Cstr a -> Maybe (Cstr a)
forall a. a -> Maybe a
Just (Cstr a -> Maybe (Cstr a)) -> Cstr a -> Maybe (Cstr a)
forall a b. (a -> b) -> a -> b
$ [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd [Cstr a]
cs

------------------------------------------------------------------------------
{- |
>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind01.smt2"
>>> let (Just noside, Just side) = split $ pokec $ qCstr q
>>> F.pprint $ elimPis ["x1"] (noside, side )
(forall ((m int) (true))
 (forall ((x1 int) (forall [v : int]
  . v == m + 1 => v == x1
&& forall [v : int]
     . v == x1 + 1 => v == 2 + m))
  (and
   (forall ((v int) (v == m + 1))
    (((v == x1))))
   (forall ((v int) (v == x1 + 1))
    (((v == 2 + m))))))) : (forall ((m int) (true))
                            (exists ((x1 int) (true))
                             ((forall [v : int]
                                 . v == m + 1 => v == x1
                               && forall [v : int]
                                    . v == x1 + 1 => v == 2 + m))))

>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"
>>> let (Just noside, Just side) = split $ pokec $ qCstr q
>>> F.pprint $ elimPis ["x1"] (noside, side )
(forall ((m int) (true))
 (forall ((z int) (z == m - 1))
  (and
   (forall ((v1 int) (v1 == z + 2))
    ((k v1)))
   (forall ((x1 int) (forall [v2 : int]
  . $k[fix$36$$954$arg$36$k$35$1:=v2] => v2 == x1
&& forall [v3 : int]
     . v3 == x1 + 1 => v3 == m + 2))
    (and
     (forall ((v2 int) (k v2))
      (((v2 == x1))))
     (forall ((v3 int) (v3 == x1 + 1))
      (((v3 == m + 2))))))))) : (forall ((m int) (true))
                                 (forall ((z int) (z == m - 1))
                                  (exists ((x1 int) (true))
                                   ((forall [v2 : int]
                                       . $k[fix$36$$954$arg$36$k$35$1:=v2] => v2 == x1
                                     && forall [v3 : int]
                                          . v3 == x1 + 1 => v3 == m + 2)))))

-}

elimPis :: [F.Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
elimPis :: [Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
elimPis [] (Cstr a, Cstr a)
cc = (Cstr a, Cstr a)
cc
elimPis (Symbol
n:[Symbol]
ns) (Cstr a
horn, Cstr a
side) = [Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
forall a. [Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
elimPis [Symbol]
ns (Cstr a -> Cstr a
apply Cstr a
horn, Cstr a -> Cstr a
apply Cstr a
side)
-- TODO: handle this error?
  where Just Cstr a
nSol = Symbol -> Cstr a -> Maybe (Cstr a)
forall a. Symbol -> Cstr a -> Maybe (Cstr a)
defs Symbol
n Cstr a
horn
        apply :: Cstr a -> Cstr a
apply = Symbol -> Cstr a -> Cstr a -> Cstr a
forall a. Symbol -> Cstr a -> Cstr a -> Cstr a
applyPi (Symbol -> Symbol
piSym Symbol
n) Cstr a
nSol

-- TODO: PAnd may be a problem
applyPi :: F.Symbol -> Cstr a -> Cstr a -> Cstr a
applyPi :: Symbol -> Cstr a -> Cstr a -> Cstr a
applyPi Symbol
k Cstr a
defs (All (Bind Symbol
x Sort
t (Var Symbol
k' [Symbol]
_xs)) Cstr a
c)
  | Symbol
k Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
k'
  = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t (Expr -> Pred
Reft (Expr -> Pred) -> Expr -> Pred
forall a b. (a -> b) -> a -> b
$ Cstr a -> Expr
forall a. Cstr a -> Expr
cstrToExpr Cstr a
defs)) Cstr a
c
applyPi Symbol
k Cstr a
bp (CAnd [Cstr a]
cs)
  = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ([Cstr a] -> Cstr a) -> [Cstr a] -> Cstr a
forall a b. (a -> b) -> a -> b
$ Symbol -> Cstr a -> Cstr a -> Cstr a
forall a. Symbol -> Cstr a -> Cstr a -> Cstr a
applyPi Symbol
k Cstr a
bp (Cstr a -> Cstr a) -> [Cstr a] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
applyPi Symbol
k Cstr a
bp (All Bind
b Cstr a
c)
  = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b (Symbol -> Cstr a -> Cstr a -> Cstr a
forall a. Symbol -> Cstr a -> Cstr a -> Cstr a
applyPi Symbol
k Cstr a
bp Cstr a
c)
applyPi Symbol
k Cstr a
bp (Any Bind
b Cstr a
c)
  = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
Any Bind
b (Symbol -> Cstr a -> Cstr a -> Cstr a
forall a. Symbol -> Cstr a -> Cstr a -> Cstr a
applyPi Symbol
k Cstr a
bp Cstr a
c)
applyPi Symbol
k Cstr a
defs (Head (Var Symbol
k' [Symbol]
_xs) a
a)
  | Symbol
k Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
k'
  -- what happens when pi's appear inside the defs for other pis?
  -- this shouldn't happen because there should be a strict
  --  pi -> k -> pi structure
  -- but that comes from the typing rules, not this format, so let's make
  -- it an invariant of solveEbs above
  = Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head (Expr -> Pred
Reft (Expr -> Pred) -> Expr -> Pred
forall a b. (a -> b) -> a -> b
$ Cstr a -> Expr
forall a. Cstr a -> Expr
cstrToExpr Cstr a
defs) a
a
applyPi Symbol
_ Cstr a
_ (Head Pred
p a
a) = Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head Pred
p a
a

-- | The defining constraints for a pivar
--
-- The defining constraints are those that bound the value of pi_x.
--
-- We're looking to lower-bound the greatest solution to pi_x.
-- If we eliminate pivars before we eliminate kvars (and then apply the kvar
-- solutions to the side conditions to solve out the pis), then we know
-- that the only constraints that mention pi in the noside case are those
-- under the corresponding pivar binder. A greatest solution for this pivar
-- can be obtained as the _weakest precondition_ of the constraints under
-- the binder
--
-- The greatest Pi that implies the constraint under it is simply that
-- constraint itself. We can leave off constraints that don't mention n,
-- see https://photos.app.goo.gl/6TorPprC3GpzV8PL7
--
-- Actually, we can really just throw away any constraints we can't QE,
-- can't we?

{- |
>>> :{
let c = doParse' hCstrP "" "\
\(forall ((m int) (true))                  \
\ (forall ((x1 int) (and (true) (πx1 x1))) \
\  (and                                    \
\   (forall ((v int) (v == m + 1))         \
\    (((v == x1))))                        \
\   (forall ((v int) (v == x1 + 1))        \
\    (((v == 2 + m)))))))"
:}

>>> F.pprint $ defs "x1" c
Just (and
      (forall ((v int) (v == m + 1))
       ((v == x1)))
      (forall ((v int) (v == x1 + 1))
       ((v == 2 + m))))

>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"
>>> let (Just noside, _) = split $ pokec $ qCstr q
>>> F.pprint $ defs "x1" noside
Just (and
      (forall ((v2 int) (k v2))
       ((v2 == x1)))
      (forall ((v3 int) (v3 == x1 + 1))
       ((v3 == m + 2))))

-}

defs :: F.Symbol -> Cstr a -> Maybe (Cstr a)
defs :: Symbol -> Cstr a -> Maybe (Cstr a)
defs Symbol
x (CAnd [Cstr a]
cs) = [Maybe (Cstr a)] -> Maybe (Cstr a)
forall a. [Maybe (Cstr a)] -> Maybe (Cstr a)
andMaybes ([Maybe (Cstr a)] -> Maybe (Cstr a))
-> [Maybe (Cstr a)] -> Maybe (Cstr a)
forall a b. (a -> b) -> a -> b
$ Symbol -> Cstr a -> Maybe (Cstr a)
forall a. Symbol -> Cstr a -> Maybe (Cstr a)
defs Symbol
x (Cstr a -> Maybe (Cstr a)) -> [Cstr a] -> [Maybe (Cstr a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
defs Symbol
x (All (Bind Symbol
x' Sort
_ Pred
_) Cstr a
c)
  | Symbol
x' Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x
  = Cstr a -> Maybe (Cstr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cstr a
c
defs Symbol
x (All Bind
_ Cstr a
c) = Symbol -> Cstr a -> Maybe (Cstr a)
forall a. Symbol -> Cstr a -> Maybe (Cstr a)
defs Symbol
x Cstr a
c
defs Symbol
_ (Head Pred
_ a
_) = Maybe (Cstr a)
forall a. Maybe a
Nothing
defs Symbol
_ (Any Bind
_ Cstr a
_) =  String -> Maybe (Cstr a)
forall a. HasCallStack => String -> a
error String
"defs should be run only after noside and poke"

cstrToExpr :: Cstr a -> F.Expr
cstrToExpr :: Cstr a -> Expr
cstrToExpr (Head Pred
p a
_) = Pred -> Expr
predToExpr Pred
p
cstrToExpr (CAnd [Cstr a]
cs) = [Expr] -> Expr
F.PAnd ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ Cstr a -> Expr
forall a. Cstr a -> Expr
cstrToExpr (Cstr a -> Expr) -> [Cstr a] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
cstrToExpr (All (Bind Symbol
x Sort
t Pred
p) Cstr a
c) = [(Symbol, Sort)] -> Expr -> Expr
F.PAll [(Symbol
x,Sort
t)] (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
F.PImp (Pred -> Expr
predToExpr Pred
p) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Cstr a -> Expr
forall a. Cstr a -> Expr
cstrToExpr Cstr a
c
cstrToExpr (Any (Bind Symbol
x Sort
t Pred
p) Cstr a
c) = [(Symbol, Sort)] -> Expr -> Expr
F.PExist [(Symbol
x,Sort
t)] (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
F.PImp (Pred -> Expr
predToExpr Pred
p) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Cstr a -> Expr
forall a. Cstr a -> Expr
cstrToExpr Cstr a
c

predToExpr :: Pred -> F.Expr
predToExpr :: Pred -> Expr
predToExpr (Reft Expr
e) = Expr
e
predToExpr (Var Symbol
k [Symbol]
xs) = KVar -> Subst -> Expr
F.PKVar (Symbol -> KVar
F.KV Symbol
k) (HashMap Symbol Expr -> Subst
F.Su (HashMap Symbol Expr -> Subst) -> HashMap Symbol Expr -> Subst
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> HashMap Symbol Expr
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol, Expr)]
su)
  where su :: [(Symbol, Expr)]
su = [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Symbol -> [Symbol]
kargs Symbol
k) (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)
predToExpr (PAnd [Pred]
ps) = [Expr] -> Expr
F.PAnd ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ Pred -> Expr
predToExpr (Pred -> Expr) -> [Pred] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps

------------------------------------------------------------------------------
{- |

Takes noside, side, piSols and solves a set of kvars in them

>>> (q, opts) <- parseFromFile hornP "tests/horn/pos/ebind02.smt2"
>>> let (Just noside, Just side) = split $ pokec $ qCstr q
>>> F.pprint $ elimKs ["k"] $ elimPis ["x1"] (noside, side)
(forall ((m int) (true))
 (forall ((z int) (z == m - 1))
  (and
   (forall ((v1 int) (v1 == z + 2))
    ((true)))
   (forall ((x1 int) (forall [v2 : int]
  . exists [v1 : int]
      . (v2 == v1)
        && v1 == z + 2 => v2 == x1
&& forall [v3 : int]
     . v3 == x1 + 1 => v3 == m + 2))
    (and
     (forall ((v1 int) (v1 == z + 2))
      (forall ((v2 int) (v2 == v1))
       (((v2 == x1)))))
     (forall ((v3 int) (v3 == x1 + 1))
      (((v3 == m + 2))))))))) : (forall ((m int) (true))
                                 (forall ((z int) (z == m - 1))
                                  (exists ((x1 int) (true))
                                   ((forall [v2 : int]
                                       . exists [v1 : int]
                                           . (v2 == v1)
                                             && v1 == z + 2 => v2 == x1
                                     && forall [v3 : int]
                                          . v3 == x1 + 1 => v3 == m + 2)))))
-}

-- TODO: make this elimKs and update tests for elimKs
elimKs' :: [F.Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
elimKs' :: [Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
elimKs' [] (Cstr a, Cstr a)
cstrs = (Cstr a, Cstr a)
cstrs
elimKs' (Symbol
k:[Symbol]
ks) (Cstr a
noside, Cstr a
side) = [Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
forall a. [Symbol] -> (Cstr a, Cstr a) -> (Cstr a, Cstr a)
elimKs' (String -> [Symbol] -> [Symbol]
forall a. String -> a -> a
trace (String
"solved kvar " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
k String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
":\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [([Bind], [Expr])] -> String
forall a. PPrint a => a -> String
F.showpp [([Bind], [Expr])]
sol) [Symbol]
ks) (Cstr a
noside', Cstr a
side')
  where
    sol :: [([Bind], [Expr])]
sol = Symbol -> Cstr a -> [([Bind], [Expr])]
forall a. Symbol -> Cstr a -> [([Bind], [Expr])]
sol1 Symbol
k (Cstr a -> [([Bind], [Expr])]) -> Cstr a -> [([Bind], [Expr])]
forall a b. (a -> b) -> a -> b
$ Symbol -> Cstr a -> Cstr a
forall a. Symbol -> Cstr a -> Cstr a
scope Symbol
k Cstr a
noside
    noside' :: Cstr a
noside' = Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
simplify (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
forall a. Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [([Bind], [Expr])]
sol Cstr a
noside
    side' :: Cstr a
side' = Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
simplify (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
forall a. Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [([Bind], [Expr])]
sol Cstr a
side

-- [NOTE-elimK-positivity]:
--
-- uh-oh I suspect this traversal is WRONG. We can build an
-- existentialPackage as a solution to a K in a negative position, but in
-- the *positive* position, the K should be solved to FALSE.
--
-- Well, this may be fine --- semantically, this is all the same, but the
-- exists in the positive positions (which will stay exists when we go to
-- prenex) may give us a lot of trouble during _quantifier elimination_
-- tx :: F.Symbol -> [[Bind]] -> Pred -> Pred
-- tx k bss = trans (defaultVisitor { txExpr = existentialPackage, ctxExpr = ctxKV }) M.empty ()
--   where
--   splitBinds xs = unzip $ (\(Bind x t p) -> ((x,t),p)) <$> xs
--   cubeSol su (Bind _ _ (Reft eqs):xs)
--     | (xts, es) <- splitBinds xs
--     = F.PExist xts $ F.PAnd (F.subst su eqs : map predToExpr es)
--   cubeSol _ _ = error "cubeSol in doelim'"
--   -- This case is a HACK. In actuality, we need some notion of
--   -- positivity...
--   existentialPackage _ (F.PAll _ (F.PImp _ (F.PKVar (F.KV k') _)))
--     | k' == k
--     = F.PTrue
--   existentialPackage m (F.PKVar (F.KV k') su)
--     | k' == k
--     , M.lookupDefault 0 k m < 2
--     = F.PAnd $ cubeSol su . reverse <$> bss
--   existentialPackage _ e = e
--   ctxKV m (F.PKVar (F.KV k) _) = M.insertWith (+) k 1 m
--   ctxKV m _ = m

-- Visitor only visit Exprs in Pred!
instance V.Visitable Pred where
  visit :: Visitor a c -> c -> Pred -> VisitM a Pred
visit Visitor a c
v c
c (PAnd [Pred]
ps) = [Pred] -> Pred
PAnd ([Pred] -> Pred) -> StateT a Identity [Pred] -> VisitM a Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pred -> VisitM a Pred) -> [Pred] -> StateT a Identity [Pred]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Visitor a c -> c -> Pred -> VisitM a Pred
forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c) [Pred]
ps
  visit Visitor a c
v c
c (Reft Expr
e) = Expr -> Pred
Reft (Expr -> Pred) -> StateT a Identity Expr -> VisitM a Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Visitor a c -> c -> Expr -> StateT a Identity Expr
forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c Expr
e
  visit Visitor a c
_ c
_ Pred
var      = Pred -> VisitM a Pred
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pred
var

instance V.Visitable (Cstr a) where
  visit :: Visitor a c -> c -> Cstr a -> VisitM a (Cstr a)
visit Visitor a c
v c
c (CAnd [Cstr a]
cs) = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ([Cstr a] -> Cstr a)
-> StateT a Identity [Cstr a] -> VisitM a (Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cstr a -> VisitM a (Cstr a))
-> [Cstr a] -> StateT a Identity [Cstr a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Visitor a c -> c -> Cstr a -> VisitM a (Cstr a)
forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c) [Cstr a]
cs
  visit Visitor a c
v c
c (Head Pred
p a
a) = Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head (Pred -> a -> Cstr a)
-> StateT a Identity Pred -> StateT a Identity (a -> Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Visitor a c -> c -> Pred -> StateT a Identity Pred
forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c Pred
p StateT a Identity (a -> Cstr a)
-> StateT a Identity a -> VisitM a (Cstr a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> StateT a Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
  visit Visitor a c
v c
ctx (All (Bind Symbol
x Sort
t Pred
p) Cstr a
c) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Bind -> Cstr a -> Cstr a)
-> StateT a Identity Bind -> StateT a Identity (Cstr a -> Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t (Pred -> Bind) -> StateT a Identity Pred -> StateT a Identity Bind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Visitor a c -> c -> Pred -> StateT a Identity Pred
forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
ctx Pred
p) StateT a Identity (Cstr a -> Cstr a)
-> VisitM a (Cstr a) -> VisitM a (Cstr a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Visitor a c -> c -> Cstr a -> VisitM a (Cstr a)
forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
ctx Cstr a
c
  visit Visitor a c
v c
ctx (Any (Bind Symbol
x Sort
t Pred
p) Cstr a
c) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Bind -> Cstr a -> Cstr a)
-> StateT a Identity Bind -> StateT a Identity (Cstr a -> Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t (Pred -> Bind) -> StateT a Identity Pred -> StateT a Identity Bind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Visitor a c -> c -> Pred -> StateT a Identity Pred
forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
ctx Pred
p) StateT a Identity (Cstr a -> Cstr a)
-> VisitM a (Cstr a) -> VisitM a (Cstr a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Visitor a c -> c -> Cstr a -> VisitM a (Cstr a)
forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
ctx Cstr a
c

------------------------------------------------------------------------------
-- | Quantifier elimination for use with implicit solver
-- qe :: Cstr a -> Cstr a
------------------------------------------------------------------------------
-- Initially this QE seemed straightforward, and does seem so in the body:
--
--    \-/ v . v = t -> r
--    ------------------
--          r[t/v]
--
-- And this works. However, the mixed quantifiers get pretty bad in the
-- side condition, which generally looks like
--    forall a1 ... an . exists n . forall v1 . ( exists karg . p ) => q
--

-- NEW STRATEGY: look under each FORALL, bottom up, compile a list of all equalities that
-- are negative, and apply some relevant one to the whole thinger.
--
-- we do first need to make the foralls from exists... so instead let's
-- just start out with foralls in doElim. They're in the wrong polarity,
-- but that's not visible from the other side of QE, so that's fine.
------------------------------------------------------------------------------
-- Now, we go through each pivar, and try to do QE in it. If there's
-- a Pi or a kvar under it, then we need to go and get the solution.
-- Since we're doing this SEPARATELY from the AD search, we can memoize.
-- In fact, we have to, because at the end of the day, we do want a
-- fully solved map.
--
-- QE:
--   (given some constraint c from an unsolved pi, we want to squash it into an expr)
--   if it's head -> if head is a kvar then lookup the kvarsol for these args and QE that
--                -> if head is a pred return that expr
--                -> if head is a pand recursive and conjunct
--   if it's any --> throw an error?
--   if it's forall equality => pred         (how do we actually find the
--     QE in pred, then apply the equality   equalities?)
--   if it's forall kvar => pred
--     lookup and then QE
--   if it's And
--      recurse and then conjunct
--
-- lookup recursively:
--   (when I want the solution for some k or pivar `x`)
--   lookup the Cstr that solves it
--   if it's an unsolved pi
--     run QE on the cstr
--     store it
--   return it

-- qe :: F.Symbol -> S.Set F.Symbol -> Cstr a -> Pred
-- qe n args c = PAnd $ ps
--   where
--     equalities = collectEqualities c
--     ps = rewriteWithEqualities n args equalities

rewriteWithEqualities :: S.Set F.Symbol -> F.Symbol -> S.Set F.Symbol -> [(F.Symbol, F.Expr)] -> [Pred]
rewriteWithEqualities :: Set Symbol -> Symbol -> Set Symbol -> [(Symbol, Expr)] -> [Pred]
rewriteWithEqualities Set Symbol
measures Symbol
n Set Symbol
args [(Symbol, Expr)]
equalities = [Pred]
preds
  where
    (Graph
eGraph, Vertex -> ((Symbol, [Expr]), Symbol, [Symbol])
vf, Symbol -> Maybe Vertex
lookupVertex) = [((Symbol, [Expr]), Symbol, [Symbol])]
-> (Graph, Vertex -> ((Symbol, [Expr]), Symbol, [Symbol]),
    Symbol -> Maybe Vertex)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
DG.graphFromEdges ([((Symbol, [Expr]), Symbol, [Symbol])]
 -> (Graph, Vertex -> ((Symbol, [Expr]), Symbol, [Symbol]),
     Symbol -> Maybe Vertex))
-> [((Symbol, [Expr]), Symbol, [Symbol])]
-> (Graph, Vertex -> ((Symbol, [Expr]), Symbol, [Symbol]),
    Symbol -> Maybe Vertex)
forall a b. (a -> b) -> a -> b
$ Set Symbol
-> HashMap Symbol ([Symbol], [Expr])
-> [(Symbol, Expr)]
-> [((Symbol, [Expr]), Symbol, [Symbol])]
eqEdges Set Symbol
args HashMap Symbol ([Symbol], [Expr])
forall a. Monoid a => a
mempty [(Symbol, Expr)]
equalities

    nResult :: (Symbol, [Expr])
nResult = (Symbol
n, Vertex -> [Expr] -> [Expr]
makeWellFormed Vertex
15 ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Symbol -> [Expr]
sols Symbol
n)
    argResults :: [(Symbol, [Expr])]
argResults = (Symbol -> (Symbol, [Expr])) -> [Symbol] -> [(Symbol, [Expr])]
forall a b. (a -> b) -> [a] -> [b]
map (\Symbol
arg -> (Symbol
arg, Vertex -> [Expr] -> [Expr]
makeWellFormed Vertex
15 ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Symbol -> [Expr]
sols Symbol
arg)) (Set Symbol -> [Symbol]
forall a. Set a -> [a]
S.toList Set Symbol
args)

    preds :: [Pred]
preds = ([[Pred]] -> [Pred]
forall a. Monoid a => [a] -> a
mconcat ([[Pred]] -> [Pred]) -> [[Pred]] -> [Pred]
forall a b. (a -> b) -> a -> b
$ (\(Symbol
x, [Expr]
es) -> [[Pred]] -> [Pred]
forall a. Monoid a => [a] -> a
mconcat ([[Pred]] -> [Pred]) -> [[Pred]] -> [Pred]
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr -> [Pred]
mkEquality Symbol
x (Expr -> [Pred]) -> [Expr] -> [[Pred]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es) ((Symbol, [Expr]) -> [Pred]) -> [(Symbol, [Expr])] -> [[Pred]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, [Expr])
nResult(Symbol, [Expr]) -> [(Symbol, [Expr])] -> [(Symbol, [Expr])]
forall a. a -> [a] -> [a]
:[(Symbol, [Expr])]
argResults))

    mkEquality :: Symbol -> Expr -> [Pred]
mkEquality Symbol
x Expr
e = [Expr -> Pred
Reft (Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Eq (Symbol -> Expr
F.EVar Symbol
x) Expr
e)]

    sols :: F.Symbol -> [F.Expr]
    sols :: Symbol -> [Expr]
sols Symbol
x = case Symbol -> Maybe Vertex
lookupVertex Symbol
x of
      Maybe Vertex
Nothing -> []
      Just Vertex
vertex -> [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol -> Expr
F.EVar Symbol
x) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [[Expr]] -> [Expr]
forall a. Monoid a => [a] -> a
mconcat [[Expr]
es | ((Symbol
_, [Expr]
es), Symbol
_, [Symbol]
_) <- Vertex -> ((Symbol, [Expr]), Symbol, [Symbol])
vf (Vertex -> ((Symbol, [Expr]), Symbol, [Symbol]))
-> [Vertex] -> [((Symbol, [Expr]), Symbol, [Symbol])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph -> Vertex -> [Vertex]
DG.reachable Graph
eGraph Vertex
vertex]

    argsAndPrims :: Set Symbol
argsAndPrims = Set Symbol
args Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
`S.union` ([Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
S.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, TheorySymbol) -> Symbol)
-> [(Symbol, TheorySymbol)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, TheorySymbol) -> Symbol
forall a b. (a, b) -> a
fst ([(Symbol, TheorySymbol)] -> [Symbol])
-> [(Symbol, TheorySymbol)] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ SEnv TheorySymbol -> [(Symbol, TheorySymbol)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv TheorySymbol -> [(Symbol, TheorySymbol)])
-> SEnv TheorySymbol -> [(Symbol, TheorySymbol)]
forall a b. (a -> b) -> a -> b
$ [DataDecl] -> SEnv TheorySymbol
F.theorySymbols []) Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
`S.union`Set Symbol
measures

    isWellFormed :: F.Expr -> Bool
    isWellFormed :: Expr -> Bool
isWellFormed Expr
e = ([Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
S.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms Expr
e) Set Symbol -> Set Symbol -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Symbol
argsAndPrims

    makeWellFormed :: Int -> [F.Expr] -> [F.Expr]
    makeWellFormed :: Vertex -> [Expr] -> [Expr]
makeWellFormed Vertex
0 [Expr]
es = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter Expr -> Bool
isWellFormed [Expr]
es -- We solved it. Maybe.
    makeWellFormed Vertex
n [Expr]
es = Vertex -> [Expr] -> [Expr]
makeWellFormed (Vertex
n Vertex -> Vertex -> Vertex
forall a. Num a => a -> a -> a
- Vertex
1) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [[Expr]] -> [Expr]
forall a. Monoid a => [a] -> a
mconcat ([[Expr]] -> [Expr]) -> [[Expr]] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
go (Expr -> [Expr]) -> [Expr] -> [[Expr]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es
      where
        go :: Expr -> [Expr]
go Expr
e = if Expr -> Bool
isWellFormed Expr
e then [Expr
e] else [(Symbol, [Expr])] -> [Expr] -> [Expr]
forall a. Subable a => [(Symbol, [Expr])] -> [a] -> [a]
rewrite [(Symbol, [Expr])]
rewrites [Expr
e]
          where
            needSolving :: Set Symbol
needSolving = ([Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
S.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms Expr
e) Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set Symbol
argsAndPrims
            rewrites :: [(Symbol, [Expr])]
rewrites = (\Symbol
x -> (Symbol
x, (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol -> Expr
F.EVar Symbol
x) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Symbol -> [Expr]
sols Symbol
x)) (Symbol -> (Symbol, [Expr])) -> [Symbol] -> [(Symbol, [Expr])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Symbol -> [Symbol]
forall a. Set a -> [a]
S.toList Set Symbol
needSolving
            rewrite :: [(Symbol, [Expr])] -> [a] -> [a]
rewrite [] [a]
es = [a]
es
            rewrite ((Symbol
x, [Expr]
rewrites):[(Symbol, [Expr])]
rewrites') [a]
es = [(Symbol, [Expr])] -> [a] -> [a]
rewrite [(Symbol, [Expr])]
rewrites' ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [Subst -> a -> a
forall a. Subable a => Subst -> a -> a
F.subst ([(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x, Expr
e')]) a
e | Expr
e' <- [Expr]
rewrites, a
e <- [a]
es]

eqEdges :: S.Set F.Symbol ->
           M.HashMap F.Symbol ([F.Symbol], [F.Expr]) ->
           [(F.Symbol, F.Expr)] ->
           [((F.Symbol, [F.Expr]), F.Symbol, [F.Symbol])]
eqEdges :: Set Symbol
-> HashMap Symbol ([Symbol], [Expr])
-> [(Symbol, Expr)]
-> [((Symbol, [Expr]), Symbol, [Symbol])]
eqEdges Set Symbol
_args HashMap Symbol ([Symbol], [Expr])
edgeMap [] = (Symbol
 -> ([Symbol], [Expr])
 -> [((Symbol, [Expr]), Symbol, [Symbol])]
 -> [((Symbol, [Expr]), Symbol, [Symbol])])
-> [((Symbol, [Expr]), Symbol, [Symbol])]
-> HashMap Symbol ([Symbol], [Expr])
-> [((Symbol, [Expr]), Symbol, [Symbol])]
forall k v a. (k -> v -> a -> a) -> a -> HashMap k v -> a
M.foldrWithKey (\Symbol
x ([Symbol]
ys, [Expr]
es) [((Symbol, [Expr]), Symbol, [Symbol])]
edges -> ((Symbol
x, [Expr]
es), Symbol
x, [Symbol]
ys)((Symbol, [Expr]), Symbol, [Symbol])
-> [((Symbol, [Expr]), Symbol, [Symbol])]
-> [((Symbol, [Expr]), Symbol, [Symbol])]
forall a. a -> [a] -> [a]
:[((Symbol, [Expr]), Symbol, [Symbol])]
edges) [] HashMap Symbol ([Symbol], [Expr])
edgeMap
eqEdges Set Symbol
args HashMap Symbol ([Symbol], [Expr])
edgeMap ((Symbol
x, Expr
e):[(Symbol, Expr)]
eqs)
  | F.EVar Symbol
y <- Expr
e
  , Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Symbol
y Set Symbol
args = Set Symbol
-> HashMap Symbol ([Symbol], [Expr])
-> [(Symbol, Expr)]
-> [((Symbol, [Expr]), Symbol, [Symbol])]
eqEdges Set Symbol
args ((([Symbol], [Expr]) -> ([Symbol], [Expr]) -> ([Symbol], [Expr]))
-> Symbol
-> ([Symbol], [Expr])
-> HashMap Symbol ([Symbol], [Expr])
-> HashMap Symbol ([Symbol], [Expr])
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith ([Symbol], [Expr]) -> ([Symbol], [Expr]) -> ([Symbol], [Expr])
forall a. Semigroup a => a -> a -> a
(<>) Symbol
x ([Symbol
y], [Symbol -> Expr
F.EVar Symbol
y]) HashMap Symbol ([Symbol], [Expr])
edgeMap) [(Symbol, Expr)]
eqs
  | F.EVar Symbol
y <- Expr
e   = Set Symbol
-> HashMap Symbol ([Symbol], [Expr])
-> [(Symbol, Expr)]
-> [((Symbol, [Expr]), Symbol, [Symbol])]
eqEdges Set Symbol
args ((([Symbol], [Expr]) -> ([Symbol], [Expr]) -> ([Symbol], [Expr]))
-> Symbol
-> ([Symbol], [Expr])
-> HashMap Symbol ([Symbol], [Expr])
-> HashMap Symbol ([Symbol], [Expr])
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith ([Symbol], [Expr]) -> ([Symbol], [Expr]) -> ([Symbol], [Expr])
forall a. Semigroup a => a -> a -> a
(<>) Symbol
x ([Symbol
y], []) HashMap Symbol ([Symbol], [Expr])
edgeMap) [(Symbol, Expr)]
eqs
  | Bool
otherwise       = Set Symbol
-> HashMap Symbol ([Symbol], [Expr])
-> [(Symbol, Expr)]
-> [((Symbol, [Expr]), Symbol, [Symbol])]
eqEdges Set Symbol
args ((([Symbol], [Expr]) -> ([Symbol], [Expr]) -> ([Symbol], [Expr]))
-> Symbol
-> ([Symbol], [Expr])
-> HashMap Symbol ([Symbol], [Expr])
-> HashMap Symbol ([Symbol], [Expr])
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith ([Symbol], [Expr]) -> ([Symbol], [Expr]) -> ([Symbol], [Expr])
forall a. Semigroup a => a -> a -> a
(<>) Symbol
x ([], [Expr
e]) HashMap Symbol ([Symbol], [Expr])
edgeMap) [(Symbol, Expr)]
eqs

collectEqualities :: Pred -> [(F.Symbol, F.Expr)]
collectEqualities :: Pred -> [(Symbol, Expr)]
collectEqualities = Pred -> [(Symbol, Expr)]
goP
  where
    goP :: Pred -> [(Symbol, Expr)]
goP (Reft Expr
e) = Expr -> [(Symbol, Expr)]
goE Expr
e
    goP (PAnd [Pred]
ps) = [[(Symbol, Expr)]] -> [(Symbol, Expr)]
forall a. Monoid a => [a] -> a
mconcat ([[(Symbol, Expr)]] -> [(Symbol, Expr)])
-> [[(Symbol, Expr)]] -> [(Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ Pred -> [(Symbol, Expr)]
goP (Pred -> [(Symbol, Expr)]) -> [Pred] -> [[(Symbol, Expr)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps
    goP Pred
_ = [(Symbol, Expr)]
forall a. Monoid a => a
mempty

    goE :: Expr -> [(Symbol, Expr)]
goE (F.PAtom Brel
F.Eq Expr
left Expr
right) = Expr -> Expr -> [(Symbol, Expr)]
extractEquality Expr
left Expr
right
    goE (F.PAnd [Expr]
es) = [[(Symbol, Expr)]] -> [(Symbol, Expr)]
forall a. Monoid a => [a] -> a
mconcat ([[(Symbol, Expr)]] -> [(Symbol, Expr)])
-> [[(Symbol, Expr)]] -> [(Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ Expr -> [(Symbol, Expr)]
goE (Expr -> [(Symbol, Expr)]) -> [Expr] -> [[(Symbol, Expr)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es
    goE Expr
_ = [(Symbol, Expr)]
forall a. Monoid a => a
mempty

extractEquality :: F.Expr -> F.Expr -> [(F.Symbol, F.Expr)]
extractEquality :: Expr -> Expr -> [(Symbol, Expr)]
extractEquality Expr
left Expr
right
  | F.EVar Symbol
x <- Expr
left, F.EVar Symbol
y <- Expr
right, Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
y = [(Symbol, Expr)]
forall a. Monoid a => a
mempty
  | F.EVar Symbol
x <- Expr
left, F.EVar Symbol
y <- Expr
right  = [(Symbol
x, Expr
right), (Symbol
y, Expr
left)]
  | F.EVar Symbol
x <- Expr
left = [(Symbol
x, Expr
right)]
  | F.EVar Symbol
x <- Expr
right = [(Symbol
x, Expr
left)]
  | Bool
otherwise = [(Symbol, Expr)]
forall a. Monoid a => a
mempty

substPiSols :: M.HashMap F.Symbol Pred -> Cstr a -> Cstr a
substPiSols :: HashMap Symbol Pred -> Cstr a -> Cstr a
substPiSols HashMap Symbol Pred
_ c :: Cstr a
c@Head{} = Cstr a
c
substPiSols HashMap Symbol Pred
piSols (CAnd [Cstr a]
cs) = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ([Cstr a] -> Cstr a) -> [Cstr a] -> Cstr a
forall a b. (a -> b) -> a -> b
$ HashMap Symbol Pred -> Cstr a -> Cstr a
forall a. HashMap Symbol Pred -> Cstr a -> Cstr a
substPiSols HashMap Symbol Pred
piSols (Cstr a -> Cstr a) -> [Cstr a] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
substPiSols HashMap Symbol Pred
piSols (All (Bind Symbol
x Sort
t Pred
p) Cstr a
c)
  | Var Symbol
k [Symbol]
_ <- Pred
p = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t (Pred -> Bind) -> Pred -> Bind
forall a b. (a -> b) -> a -> b
$ Pred -> Symbol -> HashMap Symbol Pred -> Pred
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Pred
p Symbol
k HashMap Symbol Pred
piSols) (HashMap Symbol Pred -> Cstr a -> Cstr a
forall a. HashMap Symbol Pred -> Cstr a -> Cstr a
substPiSols HashMap Symbol Pred
piSols Cstr a
c)
  | Bool
otherwise = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t Pred
p) (HashMap Symbol Pred -> Cstr a -> Cstr a
forall a. HashMap Symbol Pred -> Cstr a -> Cstr a
substPiSols HashMap Symbol Pred
piSols Cstr a
c)
substPiSols HashMap Symbol Pred
piSols (Any (Bind Symbol
n Sort
_ Pred
p) Cstr a
c)
  | Head (Var Symbol
pi [Symbol]
_) a
label <- Cstr a
c, Just Pred
sol <- Symbol -> HashMap Symbol Pred -> Maybe Pred
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
pi HashMap Symbol Pred
piSols =
    case Symbol -> Pred -> Maybe Expr
findSol Symbol
n Pred
sol of
      Just Expr
e -> Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head (Pred -> Pred
forall a. Flatten a => a -> a
flatten (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ [Pred] -> Pred
PAnd ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ (\Pred
pred -> Pred -> (Symbol, Expr) -> Pred
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Pred
pred (Symbol
n, Expr
e)) (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred
p, Pred
sol]) a
label
      Maybe Expr
Nothing -> Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head (Expr -> Pred
Reft (Expr -> Pred) -> Expr -> Pred
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
F.PAnd []) a
label
  | Bool
otherwise = String -> Cstr a
forall a. HasCallStack => String -> a
error String
"missing piSol"

findSol :: F.Symbol -> Pred -> Maybe F.Expr
findSol :: Symbol -> Pred -> Maybe Expr
findSol Symbol
x = Pred -> Maybe Expr
go
  where
    go :: Pred -> Maybe Expr
go (Reft Expr
e) = Expr -> Maybe Expr
findEq Expr
e
    go Var{} = Maybe Expr
forall a. Maybe a
Nothing
    go (PAnd [Pred]
ps) = case (Pred -> Maybe Expr) -> [Pred] -> [Expr]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Pred -> Maybe Expr
go [Pred]
ps of
      [] -> Maybe Expr
forall a. Maybe a
Nothing
      Expr
x:[Expr]
_ -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
x

    findEq :: Expr -> Maybe Expr
findEq (F.PAtom Brel
F.Eq Expr
left Expr
right)
      | F.EVar Symbol
y <- Expr
left, Symbol
y Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
right
      | F.EVar Symbol
y <- Expr
right, Symbol
y Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
left
    findEq Expr
_ = Maybe Expr
forall a. Maybe a
Nothing

------------------------------------------------------------------------------
-- | uniq makes sure each binder has a unique name
------------------------------------------------------------------------------
type RenameMap = M.HashMap F.Symbol (Integer, [Integer]) -- the first component is how many times we've seen this name. the second is the name mappings

uniq :: Cstr a -> Cstr a
uniq :: Cstr a -> Cstr a
uniq Cstr a
c = State RenameMap (Cstr a) -> RenameMap -> Cstr a
forall s a. State s a -> s -> a
evalState (Cstr a -> State RenameMap (Cstr a)
forall a. Cstr a -> State RenameMap (Cstr a)
uniq' Cstr a
c) RenameMap
forall k v. HashMap k v
M.empty

uniq' :: Cstr a -> State RenameMap (Cstr a)
uniq' :: Cstr a -> State RenameMap (Cstr a)
uniq' (Head Pred
c a
a) = Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head (Pred -> a -> Cstr a)
-> StateT RenameMap Identity Pred
-> StateT RenameMap Identity (a -> Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RenameMap -> Pred) -> StateT RenameMap Identity Pred
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Pred -> RenameMap -> Pred
rename Pred
c) StateT RenameMap Identity (a -> Cstr a)
-> StateT RenameMap Identity a -> State RenameMap (Cstr a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> StateT RenameMap Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
uniq' (CAnd [Cstr a]
c) = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ([Cstr a] -> Cstr a)
-> StateT RenameMap Identity [Cstr a] -> State RenameMap (Cstr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cstr a -> State RenameMap (Cstr a))
-> [Cstr a] -> StateT RenameMap Identity [Cstr a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cstr a -> State RenameMap (Cstr a)
forall a. Cstr a -> State RenameMap (Cstr a)
uniq' [Cstr a]
c
uniq' (All b :: Bind
b@(Bind Symbol
x Sort
_ Pred
_) Cstr a
c2) = do
    Bind
b' <- Bind -> State RenameMap Bind
uBind Bind
b
    Cstr a
c2' <- Cstr a -> State RenameMap (Cstr a)
forall a. Cstr a -> State RenameMap (Cstr a)
uniq' Cstr a
c2
    (RenameMap -> RenameMap) -> StateT RenameMap Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((RenameMap -> RenameMap) -> StateT RenameMap Identity ())
-> (RenameMap -> RenameMap) -> StateT RenameMap Identity ()
forall a b. (a -> b) -> a -> b
$ Symbol -> RenameMap -> RenameMap
popName Symbol
x
    Cstr a -> State RenameMap (Cstr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cstr a -> State RenameMap (Cstr a))
-> Cstr a -> State RenameMap (Cstr a)
forall a b. (a -> b) -> a -> b
$ Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b' Cstr a
c2'
uniq' (Any b :: Bind
b@(Bind Symbol
x Sort
_ Pred
_) Cstr a
c2) = do
    Bind
b' <- Bind -> State RenameMap Bind
uBind Bind
b
    Cstr a
c2' <- Cstr a -> State RenameMap (Cstr a)
forall a. Cstr a -> State RenameMap (Cstr a)
uniq' Cstr a
c2
    (RenameMap -> RenameMap) -> StateT RenameMap Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((RenameMap -> RenameMap) -> StateT RenameMap Identity ())
-> (RenameMap -> RenameMap) -> StateT RenameMap Identity ()
forall a b. (a -> b) -> a -> b
$ Symbol -> RenameMap -> RenameMap
popName Symbol
x
    Cstr a -> State RenameMap (Cstr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cstr a -> State RenameMap (Cstr a))
-> Cstr a -> State RenameMap (Cstr a)
forall a b. (a -> b) -> a -> b
$ Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
Any Bind
b' Cstr a
c2'

popName :: F.Symbol -> RenameMap -> RenameMap
popName :: Symbol -> RenameMap -> RenameMap
popName Symbol
x RenameMap
m = ((Integer, [Integer]) -> (Integer, [Integer]))
-> Symbol -> RenameMap -> RenameMap
forall k v.
(Eq k, Hashable k) =>
(v -> v) -> k -> HashMap k v -> HashMap k v
M.adjust (([Integer] -> [Integer])
-> (Integer, [Integer]) -> (Integer, [Integer])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [Integer] -> [Integer]
forall a. [a] -> [a]
tail) Symbol
x RenameMap
m

pushName :: Maybe (Integer, [Integer]) -> Maybe (Integer, [Integer])
pushName :: Maybe (Integer, [Integer]) -> Maybe (Integer, [Integer])
pushName Maybe (Integer, [Integer])
Nothing = (Integer, [Integer]) -> Maybe (Integer, [Integer])
forall a. a -> Maybe a
Just (Integer
0, [Integer
0])
pushName (Just (Integer
i, [Integer]
is)) = (Integer, [Integer]) -> Maybe (Integer, [Integer])
forall a. a -> Maybe a
Just (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1, (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
:[Integer]
is)

uBind :: Bind -> State RenameMap Bind
uBind :: Bind -> State RenameMap Bind
uBind (Bind Symbol
x Sort
t Pred
p) = do
   Symbol
x' <- Symbol -> State RenameMap Symbol
forall a. IsString a => Symbol -> State RenameMap a
uVariable Symbol
x
   -- nmap <- get
   Pred
p' <- (RenameMap -> Pred) -> StateT RenameMap Identity Pred
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Pred -> RenameMap -> Pred
rename Pred
p)
   Bind -> State RenameMap Bind
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bind -> State RenameMap Bind) -> Bind -> State RenameMap Bind
forall a b. (a -> b) -> a -> b
$ Symbol -> Sort -> Pred -> Bind
Bind Symbol
x' Sort
t Pred
p'

uVariable :: IsString a => F.Symbol -> State RenameMap a
uVariable :: Symbol -> State RenameMap a
uVariable Symbol
x = do
   (RenameMap -> RenameMap) -> StateT RenameMap Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Maybe (Integer, [Integer]) -> Maybe (Integer, [Integer]))
-> Symbol -> RenameMap -> RenameMap
forall k v.
(Eq k, Hashable k) =>
(Maybe v -> Maybe v) -> k -> HashMap k v -> HashMap k v
M.alter Maybe (Integer, [Integer]) -> Maybe (Integer, [Integer])
pushName Symbol
x)
   Integer
i <- (RenameMap -> Integer) -> StateT RenameMap Identity Integer
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ([Integer] -> Integer
forall a. [a] -> a
head ([Integer] -> Integer)
-> (RenameMap -> [Integer]) -> RenameMap -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, [Integer]) -> [Integer]
forall a b. (a, b) -> b
snd ((Integer, [Integer]) -> [Integer])
-> (RenameMap -> (Integer, [Integer])) -> RenameMap -> [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RenameMap -> Symbol -> (Integer, [Integer])
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.! Symbol
x))
   a -> State RenameMap a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> State RenameMap a) -> a -> State RenameMap a
forall a b. (a -> b) -> a -> b
$ Symbol -> Integer -> a
forall a. IsString a => Symbol -> Integer -> a
numSym Symbol
x Integer
i

rename :: Pred -> RenameMap -> Pred
rename :: Pred -> RenameMap -> Pred
rename Pred
e RenameMap
m = HashMap Symbol Symbol -> Pred -> Pred
substPred ((Symbol -> (Integer, [Integer]) -> Maybe Symbol)
-> RenameMap -> HashMap Symbol Symbol
forall k v1 v2.
(k -> v1 -> Maybe v2) -> HashMap k v1 -> HashMap k v2
M.mapMaybeWithKey (\Symbol
k (Integer, [Integer])
v -> case (Integer, [Integer])
v of
                                              (Integer
_, Integer
n:[Integer]
_) -> Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Symbol -> Maybe Symbol) -> Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Integer -> Symbol
forall a. IsString a => Symbol -> Integer -> a
numSym Symbol
k Integer
n
                                              (Integer, [Integer])
_ -> Maybe Symbol
forall a. Maybe a
Nothing) RenameMap
m) Pred
e

numSym :: IsString a => F.Symbol -> Integer -> a
numSym :: Symbol -> Integer -> a
numSym Symbol
s Integer
0 = String -> a
forall a. IsString a => String -> a
fromString (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ Symbol -> String
F.symbolString Symbol
s
numSym Symbol
s Integer
i = String -> a
forall a. IsString a => String -> a
fromString (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ Symbol -> String
F.symbolString Symbol
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"#" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i

substPred :: M.HashMap F.Symbol F.Symbol -> Pred -> Pred
substPred :: HashMap Symbol Symbol -> Pred -> Pred
substPred HashMap Symbol Symbol
su (Reft Expr
e) = Expr -> Pred
Reft (Expr -> Pred) -> Expr -> Pred
forall a b. (a -> b) -> a -> b
$ Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
F.subst (HashMap Symbol Expr -> Subst
F.Su (HashMap Symbol Expr -> Subst) -> HashMap Symbol Expr -> Subst
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
F.EVar (Symbol -> Expr) -> HashMap Symbol Symbol -> HashMap Symbol Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol Symbol
su) Expr
e
substPred HashMap Symbol Symbol
su (PAnd [Pred]
ps) = [Pred] -> Pred
PAnd ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ HashMap Symbol Symbol -> Pred -> Pred
substPred HashMap Symbol Symbol
su (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps
substPred HashMap Symbol Symbol
su (Var Symbol
k [Symbol]
xs) = Symbol -> [Symbol] -> Pred
Var Symbol
k ([Symbol] -> Pred) -> [Symbol] -> Pred
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol
upd (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs
  where upd :: Symbol -> Symbol
upd Symbol
x = Symbol -> Symbol -> HashMap Symbol Symbol -> Symbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
x Symbol
x HashMap Symbol Symbol
su

------------------------------------------------------------------------------
-- | elim solves all of the KVars in a Cstr (assuming no cycles...)
-- >>> elim . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test00.smt2"
-- (and (forall ((x int) (x > 0)) (forall ((y int) (y > x)) (forall ((v int) (v == x + y)) ((v > 0))))))
-- >>> elim . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test01.smt2"
-- (and (forall ((x int) (x > 0)) (and (forall ((y int) (y > x)) (forall ((v int) (v == x + y)) ((v > 0)))) (forall ((z int) (z > 100)) (forall ((v int) (v == x + z)) ((v > 100)))))))
-- >>> elim . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test02.smt2"
-- (and (forall ((x int) (x > 0)) (and (forall ((y int) (y > x + 100)) (forall ((v int) (v == x + y)) ((true)))) (forall ((y int) (y > x + 100)) (forall ((v int) (v == x + y)) (forall ((z int) (z == v)) (forall ((v int) (v == x + z)) ((v > 100)))))))))
------------------------------------------------------------------------------
elim :: Cstr a -> Cstr a
------------------------------------------------------------------------------
elim :: Cstr a -> Cstr a
elim Cstr a
c = if Set Symbol -> Bool
forall a. Set a -> Bool
S.null (Set Symbol -> Bool) -> Set Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ Cstr a -> Set Symbol
forall a. Cstr a -> Set Symbol
boundKvars Cstr a
res then Cstr a
res else String -> Cstr a
forall a. HasCallStack => String -> a
error String
"called elim on cyclic constraint"
  where
  res :: Cstr a
res = (Cstr a -> Symbol -> Cstr a) -> Cstr a -> Set Symbol -> Cstr a
forall a b. (a -> b -> a) -> a -> Set b -> a
S.foldl Cstr a -> Symbol -> Cstr a
forall a. Cstr a -> Symbol -> Cstr a
elim1 Cstr a
c (Cstr a -> Set Symbol
forall a. Cstr a -> Set Symbol
boundKvars Cstr a
c)

elim1 :: Cstr a -> F.Symbol -> Cstr a
-- Find a `sol1` solution to a kvar `k`, and then subsitute in the solution for
-- each rhs occurrence of k.
elim1 :: Cstr a -> Symbol -> Cstr a
elim1 Cstr a
c Symbol
k = Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
simplify (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
forall a. Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [([Bind], [Expr])]
sol Cstr a
c
  where sol :: [([Bind], [Expr])]
sol = Symbol -> Cstr a -> [([Bind], [Expr])]
forall a. Symbol -> Cstr a -> [([Bind], [Expr])]
sol1 Symbol
k (Symbol -> Cstr a -> Cstr a
forall a. Symbol -> Cstr a -> Cstr a
scope Symbol
k Cstr a
c)

-- |
-- >>> sc <- scope "k0" . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test02.smt2"
-- >>> sc
-- (forall ((x ... (and (forall ((y ... (forall ((v ... ((k0 v)))) (forall ((z ...

-- scope is lca
scope :: F.Symbol -> Cstr a -> Cstr a
scope :: Symbol -> Cstr a -> Cstr a
scope Symbol
k Cstr a
cstr = case Cstr a -> Either a (Cstr a)
forall a. Cstr a -> Either a (Cstr a)
go Cstr a
cstr of
                 Right Cstr a
c -> Cstr a
c
                 Left a
l -> Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head (Expr -> Pred
Reft Expr
F.PTrue) a
l
  where
    go :: Cstr a -> Either a (Cstr a)
go c :: Cstr a
c@(Head (Var Symbol
k' [Symbol]
_) a
_)
      | Symbol
k' Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
k = Cstr a -> Either a (Cstr a)
forall a b. b -> Either a b
Right Cstr a
c
    go (Head Pred
_ a
l) = a -> Either a (Cstr a)
forall a b. a -> Either a b
Left a
l
    go c :: Cstr a
c@(All (Bind Symbol
_ Sort
_ Pred
p) Cstr a
c') =
      if Symbol
k Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` (Pred -> Set Symbol
pKVars Pred
p) then Cstr a -> Either a (Cstr a)
forall a b. b -> Either a b
Right Cstr a
c else Cstr a -> Either a (Cstr a)
go Cstr a
c'
    go Any{} = String -> Either a (Cstr a)
forall a. HasCallStack => String -> a
error String
"any should not appear after poke"

    -- if kvar doesn't appear, then just return the left
    -- if kvar appears in one child, that is the lca
    -- but if kvar appear in multiple chlidren, this is the lca
    go c :: Cstr a
c@(CAnd [Cstr a]
cs) = case [Either a (Cstr a)] -> [Cstr a]
forall a b. [Either a b] -> [b]
rights (Cstr a -> Either a (Cstr a)
go (Cstr a -> Either a (Cstr a)) -> [Cstr a] -> [Either a (Cstr a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs) of
                       [] -> a -> Either a (Cstr a)
forall a b. a -> Either a b
Left (a -> Either a (Cstr a)) -> a -> Either a (Cstr a)
forall a b. (a -> b) -> a -> b
$ Cstr a -> a
forall a. Cstr a -> a
cLabel Cstr a
c
                       [Cstr a
c] -> Cstr a -> Either a (Cstr a)
forall a b. b -> Either a b
Right Cstr a
c
                       [Cstr a]
_ -> Cstr a -> Either a (Cstr a)
forall a b. b -> Either a b
Right Cstr a
c


-- | A solution is a Hyp of binders (including one anonymous binder
-- that I've singled out here).
-- (What does Hyp stand for? Hypercube? but the dims don't line up...)
--
-- >>> c <- qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test02.smt2"
-- >>> sol1 ("k0") (scope "k0" c)
-- [[((y int) (y > x + 100)),((v int) (v == x + y)),((_ bool) (κarg$k0#1 == v))]]
-- >>> c <- qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test03.smt2"
-- >>> sol1 ("k0") (scope "k0" c)
-- [[((x int) (x > 0)),((v int) (v == x)),((_ bool) (κarg$k0#1 == v))],[((y int) (k0 y)),((v int) (v == y + 1)),((_ bool) (κarg$k0#1 == v))]]
-- >>> let c = doParse' hCstrP "" "(forall ((a Int) (p a)) (forall ((b Int) (q b)) (and (($k a)) (($k b)))))"
-- >>> sol1 "k" c
-- [[((a int) (p a)),((b int) (q b)),((_ bool) (κarg$k#1 == a))],[((a int) (p a)),((b int) (q b)),((_ bool) (κarg$k#1 == b))]]

-- Naming conventions:
--  - `b` is a binder `forall . x:t .p =>`
--  - `bs` is a list of binders, or a "cube" that tracks all of the
--     information on the rhs of a given constraint
--  - `bss` is a Hyp, that tells us the solution to a Var, that is,
--     a collection of cubes that we'll want to disjunct

sol1 :: F.Symbol -> Cstr a -> [([Bind], [F.Expr])]
sol1 :: Symbol -> Cstr a -> [([Bind], [Expr])]
sol1 Symbol
k (CAnd [Cstr a]
cs) = Symbol -> Cstr a -> [([Bind], [Expr])]
forall a. Symbol -> Cstr a -> [([Bind], [Expr])]
sol1 Symbol
k (Cstr a -> [([Bind], [Expr])]) -> [Cstr a] -> [([Bind], [Expr])]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Cstr a]
cs
sol1 Symbol
k (All Bind
b Cstr a
c) = (\([Bind]
bs, [Expr]
eqs) -> (Bind
bBind -> [Bind] -> [Bind]
forall a. a -> [a] -> [a]
:[Bind]
bs, [Expr]
eqs)) (([Bind], [Expr]) -> ([Bind], [Expr]))
-> [([Bind], [Expr])] -> [([Bind], [Expr])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> Cstr a -> [([Bind], [Expr])]
forall a. Symbol -> Cstr a -> [([Bind], [Expr])]
sol1 Symbol
k Cstr a
c
sol1 Symbol
k (Head (Var Symbol
k' [Symbol]
ys) a
_) | Symbol
k Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
k'
  = [([], (Expr -> Expr -> Expr) -> [Expr] -> [Expr] -> [Expr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Eq) (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs) (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
ys))]
  where xs :: [Symbol]
xs = (Symbol -> Symbol -> Symbol) -> [Symbol] -> [Symbol] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> Symbol -> Symbol
forall a b. a -> b -> a
const (Symbol -> [Symbol]
kargs Symbol
k) [Symbol]
ys
sol1 Symbol
_ (Head Pred
_ a
_) = []
sol1 Symbol
_ (Any Bind
_ Cstr a
_) =  String -> [([Bind], [Expr])]
forall a. HasCallStack => String -> a
error String
"ebinds don't work with old elim"

kargs :: F.Symbol -> [F.Symbol]
kargs :: Symbol -> [Symbol]
kargs Symbol
k = String -> Symbol
forall a. IsString a => String -> a
fromString (String -> Symbol) -> (Integer -> String) -> Integer -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String
"κarg$" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
F.symbolString Symbol
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"#") String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Integer -> String) -> Integer -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show (Integer -> Symbol) -> [Integer] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
1..]

-- |
-- >>> LET c = doParse' hCstrP "" "(forall ((z Int) ($k0 z)) ((z = x)))"
-- >>> doelim "k0" [[Bind "v" F.boolSort (Reft $ F.EVar "v"), Bind "_" F.boolSort (Reft $ F.EVar "donkey")]]  c
-- (forall ((v bool) (v)) (forall ((z int) (donkey)) ((z == x))))

doelim :: F.Symbol -> [([Bind], [F.Expr])] -> Cstr a -> Cstr a
doelim :: Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [([Bind], [Expr])]
bss (CAnd [Cstr a]
cs)
  = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ([Cstr a] -> Cstr a) -> [Cstr a] -> Cstr a
forall a b. (a -> b) -> a -> b
$ Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
forall a. Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [([Bind], [Expr])]
bss (Cstr a -> Cstr a) -> [Cstr a] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
doelim Symbol
k [([Bind], [Expr])]
bss (All (Bind Symbol
x Sort
t Pred
p) Cstr a
c) =
  case Symbol -> Pred -> Either ([(Symbol, [Symbol])], [Pred]) Pred
findKVarInGuard Symbol
k Pred
p of
    Right Pred
_ -> Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t Pred
p) (Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
forall a. Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [([Bind], [Expr])]
bss Cstr a
c)
    Left ([(Symbol, [Symbol])]
kvars, [Pred]
preds) -> Symbol
-> Sort
-> [(Symbol, [Symbol])]
-> [Pred]
-> Cstr a
-> [([Bind], [Expr])]
-> Cstr a
forall a.
Symbol
-> Sort
-> [(Symbol, [Symbol])]
-> [Pred]
-> Cstr a
-> [([Bind], [Expr])]
-> Cstr a
demorgan Symbol
x Sort
t [(Symbol, [Symbol])]
kvars [Pred]
preds (Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
forall a. Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [([Bind], [Expr])]
bss Cstr a
c) [([Bind], [Expr])]
bss
  where
    demorgan :: F.Symbol -> F.Sort -> [(F.Symbol, [F.Symbol])] -> [Pred] -> Cstr a -> [([Bind], [F.Expr])] -> Cstr a
    demorgan :: Symbol
-> Sort
-> [(Symbol, [Symbol])]
-> [Pred]
-> Cstr a
-> [([Bind], [Expr])]
-> Cstr a
demorgan Symbol
x Sort
t [(Symbol, [Symbol])]
kvars [Pred]
preds Cstr a
c [([Bind], [Expr])]
bss = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
mkAnd ([Cstr a] -> Cstr a) -> [Cstr a] -> Cstr a
forall a b. (a -> b) -> a -> b
$ ([Bind], [Expr]) -> Cstr a
cubeSol (([Bind], [Expr]) -> Cstr a) -> [([Bind], [Expr])] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Bind], [Expr])]
bss
      where su :: Subst
su = HashMap Symbol Expr -> Subst
F.Su (HashMap Symbol Expr -> Subst) -> HashMap Symbol Expr -> Subst
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> HashMap Symbol Expr
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, Expr)] -> HashMap Symbol Expr)
-> [(Symbol, Expr)] -> HashMap Symbol Expr
forall a b. (a -> b) -> a -> b
$ [[(Symbol, Expr)]] -> [(Symbol, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Symbol, Expr)]] -> [(Symbol, Expr)])
-> [[(Symbol, Expr)]] -> [(Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ ((Symbol, [Symbol]) -> [(Symbol, Expr)])
-> [(Symbol, [Symbol])] -> [[(Symbol, Expr)]]
forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
k, [Symbol]
xs) -> [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Symbol -> [Symbol]
kargs Symbol
k) (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)) [(Symbol, [Symbol])]
kvars
            mkAnd :: [Cstr a] -> Cstr a
mkAnd [Cstr a
c] = Cstr a
c
            mkAnd [Cstr a]
cs = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd [Cstr a]
cs
            cubeSol :: ([Bind], [Expr]) -> Cstr a
cubeSol ((Bind
b:[Bind]
bs), [Expr]
eqs) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ ([Bind], [Expr]) -> Cstr a
cubeSol ([Bind]
bs, [Expr]
eqs)
            cubeSol ([], [Expr]
eqs) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t ([Pred] -> Pred
PAnd ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ (Expr -> Pred
Reft (Expr -> Pred) -> [Expr] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst -> [Expr] -> [Expr]
forall a. Subable a => Subst -> a -> a
F.subst Subst
su [Expr]
eqs) [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ (Subst -> Pred -> Pred
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
preds))) Cstr a
c
doelim Symbol
k [([Bind], [Expr])]
_ (Head (Var Symbol
k' [Symbol]
_) a
a)
  | Symbol
k Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
k'
  = Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head (Expr -> Pred
Reft Expr
F.PTrue) a
a
doelim Symbol
_ [([Bind], [Expr])]
_ (Head Pred
p a
a) = Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head Pred
p a
a

doelim Symbol
k [([Bind], [Expr])]
bss (Any (Bind Symbol
x Sort
t Pred
p) Cstr a
c) =
  case Symbol -> Pred -> Either ([(Symbol, [Symbol])], [Pred]) Pred
findKVarInGuard Symbol
k Pred
p of
    Right Pred
_ -> Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
Any (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t Pred
p) (Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
forall a. Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [([Bind], [Expr])]
bss Cstr a
c)
    Left ([(Symbol, [Symbol])]
_, [Pred]
rights) -> Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
Any (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t ([Pred] -> Pred
PAnd [Pred]
rights)) (Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
forall a. Symbol -> [([Bind], [Expr])] -> Cstr a -> Cstr a
doelim Symbol
k [([Bind], [Expr])]
bss Cstr a
c) -- TODO: for now we set the kvar to true. not sure if this is correct

-- If k is in the guard then returns a Left list of that k and the remaining preds in the guard
-- If k is not in the guard returns a Right of the pred
findKVarInGuard :: F.Symbol -> Pred -> Either ([(F.Symbol, [F.Symbol])], [Pred]) Pred
findKVarInGuard :: Symbol -> Pred -> Either ([(Symbol, [Symbol])], [Pred]) Pred
findKVarInGuard Symbol
k (PAnd [Pred]
ps) =
  if [([(Symbol, [Symbol])], [Pred])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([(Symbol, [Symbol])], [Pred])]
lefts
    then Pred -> Either ([(Symbol, [Symbol])], [Pred]) Pred
forall a b. b -> Either a b
Right ([Pred] -> Pred
PAnd [Pred]
ps) -- kvar not found
    else ([(Symbol, [Symbol])], [Pred])
-> Either ([(Symbol, [Symbol])], [Pred]) Pred
forall a b. a -> Either a b
Left (([(Symbol, [Symbol])], [Pred])
 -> Either ([(Symbol, [Symbol])], [Pred]) Pred)
-> ([(Symbol, [Symbol])], [Pred])
-> Either ([(Symbol, [Symbol])], [Pred]) Pred
forall a b. (a -> b) -> a -> b
$ ([(Symbol, [Symbol])]
newLefts, [Pred]
newRights)
  where findResults :: [Either ([(Symbol, [Symbol])], [Pred]) Pred]
findResults = Symbol -> Pred -> Either ([(Symbol, [Symbol])], [Pred]) Pred
findKVarInGuard Symbol
k (Pred -> Either ([(Symbol, [Symbol])], [Pred]) Pred)
-> [Pred] -> [Either ([(Symbol, [Symbol])], [Pred]) Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps
        ([([(Symbol, [Symbol])], [Pred])]
lefts, [Pred]
rights) = [Either ([(Symbol, [Symbol])], [Pred]) Pred]
-> ([([(Symbol, [Symbol])], [Pred])], [Pred])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either ([(Symbol, [Symbol])], [Pred]) Pred]
findResults
        newLefts :: [(Symbol, [Symbol])]
newLefts = [[(Symbol, [Symbol])]] -> [(Symbol, [Symbol])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Symbol, [Symbol])]] -> [(Symbol, [Symbol])])
-> [[(Symbol, [Symbol])]] -> [(Symbol, [Symbol])]
forall a b. (a -> b) -> a -> b
$ (([(Symbol, [Symbol])], [Pred]) -> [(Symbol, [Symbol])])
-> [([(Symbol, [Symbol])], [Pred])] -> [[(Symbol, [Symbol])]]
forall a b. (a -> b) -> [a] -> [b]
map ([(Symbol, [Symbol])], [Pred]) -> [(Symbol, [Symbol])]
forall a b. (a, b) -> a
fst [([(Symbol, [Symbol])], [Pred])]
lefts
        newRights :: [Pred]
newRights = [[Pred]] -> [Pred]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (([(Symbol, [Symbol])], [Pred]) -> [Pred]
forall a b. (a, b) -> b
snd (([(Symbol, [Symbol])], [Pred]) -> [Pred])
-> [([(Symbol, [Symbol])], [Pred])] -> [[Pred]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([(Symbol, [Symbol])], [Pred])]
lefts) [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [Pred]
rights
findKVarInGuard Symbol
k p :: Pred
p@(Var Symbol
k' [Symbol]
xs)
  | Symbol
k Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
k' = ([(Symbol, [Symbol])], [Pred])
-> Either ([(Symbol, [Symbol])], [Pred]) Pred
forall a b. a -> Either a b
Left ([(Symbol
k', [Symbol]
xs)], [])
  | Bool
otherwise = Pred -> Either ([(Symbol, [Symbol])], [Pred]) Pred
forall a b. b -> Either a b
Right Pred
p
findKVarInGuard Symbol
_ Pred
p = Pred -> Either ([(Symbol, [Symbol])], [Pred]) Pred
forall a b. b -> Either a b
Right Pred
p

-- | Returns a list of KVars with their arguments that are present as
--
-- >>> boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/ebind01.smt2"
-- ... []
-- >>> boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/ebind02.smt2"
-- ... ["k"]
-- >>> boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test00.smt2"
-- ... []
-- >>> boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test01.smt2"
-- ... []
-- >>> boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test02.smt2"
-- ... ["k0"]
-- >>> boundKvars . qCstr . fst <$> parseFromFile hornP "tests/horn/pos/test03.smt2"
-- ... ["k0"]

boundKvars :: Cstr a -> S.Set F.Symbol
boundKvars :: Cstr a -> Set Symbol
boundKvars (Head Pred
p a
_)           = Pred -> Set Symbol
pKVars Pred
p
boundKvars (CAnd [Cstr a]
c)             = [Set Symbol] -> Set Symbol
forall a. Monoid a => [a] -> a
mconcat ([Set Symbol] -> Set Symbol) -> [Set Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Cstr a -> Set Symbol
forall a. Cstr a -> Set Symbol
boundKvars (Cstr a -> Set Symbol) -> [Cstr a] -> [Set Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
c
boundKvars (All (Bind Symbol
_ Sort
_ Pred
p) Cstr a
c) = Pred -> Set Symbol
pKVars Pred
p Set Symbol -> Set Symbol -> Set Symbol
forall a. Semigroup a => a -> a -> a
<> Cstr a -> Set Symbol
forall a. Cstr a -> Set Symbol
boundKvars Cstr a
c
boundKvars (Any (Bind Symbol
_ Sort
_ Pred
p) Cstr a
c) = Pred -> Set Symbol
pKVars Pred
p Set Symbol -> Set Symbol -> Set Symbol
forall a. Semigroup a => a -> a -> a
<> Cstr a -> Set Symbol
forall a. Cstr a -> Set Symbol
boundKvars Cstr a
c

pKVars :: Pred -> S.Set F.Symbol
pKVars :: Pred -> Set Symbol
pKVars (Var Symbol
k [Symbol]
_) = Symbol -> Set Symbol
forall a. a -> Set a
S.singleton Symbol
k
pKVars (PAnd [Pred]
ps) = [Set Symbol] -> Set Symbol
forall a. Monoid a => [a] -> a
mconcat ([Set Symbol] -> Set Symbol) -> [Set Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Pred -> Set Symbol
pKVars (Pred -> Set Symbol) -> [Pred] -> [Set Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps
pKVars Pred
_         = Set Symbol
forall a. Set a
S.empty

-- | Returns true if the constraint does not contain any existential binders
isNNF :: Cstr a -> Bool
isNNF :: Cstr a -> Bool
isNNF Head{} = Bool
True
isNNF (CAnd [Cstr a]
cs) = (Cstr a -> Bool) -> [Cstr a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Cstr a -> Bool
forall a. Cstr a -> Bool
isNNF [Cstr a]
cs
isNNF (All Bind
_ Cstr a
c) = Cstr a -> Bool
forall a. Cstr a -> Bool
isNNF Cstr a
c
isNNF Any{} = Bool
False

calculateCuts :: F.Config -> Query a -> Cstr a -> S.Set F.Symbol
calculateCuts :: Config -> Query a -> Cstr a -> Set Symbol
calculateCuts Config
cfg (Query [Qualifier]
qs [Var a]
vs Cstr a
_ HashMap Symbol Sort
cons HashMap Symbol Sort
dist) Cstr a
nnf = HashSet KVar -> Set Symbol
convert (HashSet KVar -> Set Symbol) -> HashSet KVar -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Elims KVar -> HashSet KVar
forall a. Elims a -> HashSet a
FG.depCuts Elims KVar
deps
  where
    ([CEdge]
_, Elims KVar
deps) = Config -> GInfo SubC a -> ([CEdge], Elims KVar)
forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> ([CEdge], Elims KVar)
elimVars Config
cfg (Query a -> GInfo SubC a
forall a. Query a -> FInfo a
hornFInfo (Query a -> GInfo SubC a) -> Query a -> GInfo SubC a
forall a b. (a -> b) -> a -> b
$ [Qualifier]
-> [Var a]
-> Cstr a
-> HashMap Symbol Sort
-> HashMap Symbol Sort
-> Query a
forall a.
[Qualifier]
-> [Var a]
-> Cstr a
-> HashMap Symbol Sort
-> HashMap Symbol Sort
-> Query a
Query [Qualifier]
qs [Var a]
vs Cstr a
nnf HashMap Symbol Sort
cons HashMap Symbol Sort
dist)
    convert :: HashSet KVar -> Set Symbol
convert HashSet KVar
hashset = [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
S.fromList ([Symbol] -> Set Symbol) -> [Symbol] -> Set Symbol
forall a b. (a -> b) -> a -> b
$ KVar -> Symbol
F.kv (KVar -> Symbol) -> [KVar] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HashSet KVar -> [KVar]
forall a. HashSet a -> [a]
HS.toList HashSet KVar
hashset)

forgetPiVars :: S.Set F.Symbol -> Cstr a -> Cstr a
forgetPiVars :: Set Symbol -> Cstr a -> Cstr a
forgetPiVars Set Symbol
_ c :: Cstr a
c@Head{} = Cstr a
c
forgetPiVars Set Symbol
pis (CAnd [Cstr a]
cs) = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ([Cstr a] -> Cstr a) -> [Cstr a] -> Cstr a
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Cstr a -> Cstr a
forall a. Set Symbol -> Cstr a -> Cstr a
forgetPiVars Set Symbol
pis (Cstr a -> Cstr a) -> [Cstr a] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
forgetPiVars Set Symbol
pis (All (Bind Symbol
x Sort
t Pred
p) Cstr a
c)
  | Var Symbol
k [Symbol]
_ <- Pred
p, Symbol
k Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Symbol
pis = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t ([Pred] -> Pred
PAnd [])) (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Cstr a -> Cstr a
forall a. Set Symbol -> Cstr a -> Cstr a
forgetPiVars Set Symbol
pis Cstr a
c
  | Bool
otherwise = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t Pred
p) (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Cstr a -> Cstr a
forall a. Set Symbol -> Cstr a -> Cstr a
forgetPiVars Set Symbol
pis Cstr a
c
forgetPiVars Set Symbol
_ Any{} = String -> Cstr a
forall a. HasCallStack => String -> a
error String
"shouldn't be present"

-----------------------------------------------------------------------------------
-- | Cleanup Horn Constraint
-- We want to simplify the Query a little bit, and make sure it is Horn,
-- that is, only a kvar-free (ie concrete) predicate or a single kvar in
-- each head
-----------------------------------------------------------------------------------

simplify :: Cstr a -> Cstr a
simplify :: Cstr a -> Cstr a
simplify = Cstr a -> Cstr a
forall a. Flatten a => a -> a
flatten (Cstr a -> Cstr a) -> (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
pruneTauts (Cstr a -> Cstr a) -> (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
removeDuplicateBinders

{- | flatten removes redundant `and`s and empty conjuncts.

For example:
>>> :{
flatten $ doParse' hCstrP "" "(forall ((VV##15 int) (VV##15 == anf##3)) \
            \      ((and (and \
            \        ($k13 VV##15 anf##3 moo##5) \
            \        (true)))))"
:}
(forall ((VV##15 int) (VV##15 == anf##3)) ((k13 VV##15 anf##3 moo##5)))
-}

class Flatten a where
  flatten :: a -> a

instance Flatten (Cstr a) where
  flatten :: Cstr a -> Cstr a
flatten (CAnd [Cstr a]
cs) = case [Cstr a] -> [Cstr a]
forall a. Flatten a => a -> a
flatten [Cstr a]
cs of
                        [Cstr a
c] -> Cstr a
c
                        [Cstr a]
cs -> [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd [Cstr a]
cs
  flatten (Head Pred
p a
a) = Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head (Pred -> Pred
forall a. Flatten a => a -> a
flatten Pred
p) a
a
  flatten (All (Bind Symbol
x Sort
t Pred
p) Cstr a
c) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t (Pred -> Pred
forall a. Flatten a => a -> a
flatten Pred
p)) (Cstr a -> Cstr a
forall a. Flatten a => a -> a
flatten Cstr a
c)
  flatten (Any (Bind Symbol
x Sort
t Pred
p) Cstr a
c) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
Any (Symbol -> Sort -> Pred -> Bind
Bind Symbol
x Sort
t (Pred -> Pred
forall a. Flatten a => a -> a
flatten Pred
p)) (Cstr a -> Cstr a
forall a. Flatten a => a -> a
flatten Cstr a
c)

instance Flatten [Cstr a] where
  flatten :: [Cstr a] -> [Cstr a]
flatten (CAnd [Cstr a]
cs : [Cstr a]
xs) = [Cstr a] -> [Cstr a]
forall a. Flatten a => a -> a
flatten [Cstr a]
cs [Cstr a] -> [Cstr a] -> [Cstr a]
forall a. [a] -> [a] -> [a]
++ [Cstr a] -> [Cstr a]
forall a. Flatten a => a -> a
flatten [Cstr a]
xs
  flatten (Cstr a
x:[Cstr a]
xs)
    | Head (Reft Expr
p) a
_ <- Cstr a
fx
    , Expr -> Bool
F.isTautoPred Expr
p            = [Cstr a] -> [Cstr a]
forall a. Flatten a => a -> a
flatten [Cstr a]
xs
    | Bool
otherwise                  = Cstr a
fxCstr a -> [Cstr a] -> [Cstr a]
forall a. a -> [a] -> [a]
:[Cstr a] -> [Cstr a]
forall a. Flatten a => a -> a
flatten [Cstr a]
xs
    where fx :: Cstr a
fx = Cstr a -> Cstr a
forall a. Flatten a => a -> a
flatten Cstr a
x
  flatten [] = []

instance Flatten Pred where
  flatten :: Pred -> Pred
flatten (PAnd [Pred]
ps) = case [Pred] -> [Pred]
forall a. Flatten a => a -> a
flatten [Pred]
ps of
                        [Pred
p] -> Pred
p
                        [Pred]
ps  -> [Pred] -> Pred
PAnd [Pred]
ps
  flatten Pred
p = Pred
p

instance Flatten [Pred] where
  flatten :: [Pred] -> [Pred]
flatten (PAnd [Pred]
ps' : [Pred]
ps) = [Pred] -> [Pred]
forall a. Flatten a => a -> a
flatten [Pred]
ps' [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [Pred] -> [Pred]
forall a. Flatten a => a -> a
flatten [Pred]
ps
  flatten (Pred
p : [Pred]
ps)
    | Reft Expr
e <- Pred
fp
    , Expr -> Bool
F.isTautoPred Expr
e     = [Pred] -> [Pred]
forall a. Flatten a => a -> a
flatten [Pred]
ps
    | Bool
otherwise           = Pred
fp Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred] -> [Pred]
forall a. Flatten a => a -> a
flatten [Pred]
ps
    where fp :: Pred
fp = Pred -> Pred
forall a. Flatten a => a -> a
flatten Pred
p
  flatten []              = []

instance Flatten F.Expr where
  flatten :: Expr -> Expr
flatten (F.PAnd [Expr]
ps) = case [Expr] -> [Expr]
forall a. Flatten a => a -> a
flatten [Expr]
ps of
                         [Expr
p] -> Expr
p
                         [Expr]
ps  -> [Expr] -> Expr
F.PAnd [Expr]
ps
  flatten Expr
p = Expr
p

instance Flatten [F.Expr] where
  flatten :: [Expr] -> [Expr]
flatten (F.PAnd [Expr]
ps' : [Expr]
ps) = [Expr] -> [Expr]
forall a. Flatten a => a -> a
flatten [Expr]
ps' [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr] -> [Expr]
forall a. Flatten a => a -> a
flatten [Expr]
ps
  flatten (Expr
p : [Expr]
ps)
    | Expr -> Bool
F.isTautoPred Expr
fp    = [Expr] -> [Expr]
forall a. Flatten a => a -> a
flatten [Expr]
ps
    | Bool
otherwise           = Expr
fp Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr] -> [Expr]
forall a. Flatten a => a -> a
flatten [Expr]
ps
    where fp :: Expr
fp = Expr -> Expr
forall a. Flatten a => a -> a
flatten Expr
p
  flatten []              = []

-- | Split heads into one for each kvar so that queries are always horn constraints
hornify :: Cstr a -> Cstr a
hornify :: Cstr a -> Cstr a
hornify (Head (PAnd [Pred]
ps) a
a) = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ((Pred -> a -> Cstr a) -> a -> Pred -> Cstr a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head a
a (Pred -> Cstr a) -> [Pred] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps')
  where ps' :: [Pred]
ps' = let ([Pred]
ks, [Pred]
qs) = [Pred] -> [Pred] -> [Pred] -> ([Pred], [Pred])
split [] [] ([Pred] -> [Pred]
forall a. Flatten a => a -> a
flatten [Pred]
ps) in [Pred] -> Pred
PAnd [Pred]
qs Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ks

        split :: [Pred] -> [Pred] -> [Pred] -> ([Pred], [Pred])
split [Pred]
kacc [Pred]
pacc ((Var Symbol
x [Symbol]
xs):[Pred]
qs) = [Pred] -> [Pred] -> [Pred] -> ([Pred], [Pred])
split ((Symbol -> [Symbol] -> Pred
Var Symbol
x [Symbol]
xs)Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
:[Pred]
kacc) [Pred]
pacc [Pred]
qs
        split [Pred]
kacc [Pred]
pacc (Pred
q:[Pred]
qs) = [Pred] -> [Pred] -> [Pred] -> ([Pred], [Pred])
split [Pred]
kacc (Pred
qPred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
:[Pred]
pacc) [Pred]
qs
        split [Pred]
kacc [Pred]
pacc [] = ([Pred]
kacc, [Pred]
pacc)
hornify (Head (Reft Expr
r) a
a) = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ((Pred -> a -> Cstr a) -> a -> Pred -> Cstr a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head a
a (Pred -> Cstr a) -> [Pred] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Expr -> Pred
Reft (Expr -> Pred) -> Expr -> Pred
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
F.PAnd [Expr]
ps)Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
:(Expr -> Pred
Reft (Expr -> Pred) -> [Expr] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ks)))
  where ([Expr]
ks, [Expr]
ps) = [Expr] -> [Expr] -> [Expr] -> ([Expr], [Expr])
split [] [] ([Expr] -> ([Expr], [Expr])) -> [Expr] -> ([Expr], [Expr])
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
F.splitPAnd Expr
r
        split :: [Expr] -> [Expr] -> [Expr] -> ([Expr], [Expr])
split [Expr]
kacc [Expr]
pacc (r :: Expr
r@F.PKVar{}:[Expr]
rs) = [Expr] -> [Expr] -> [Expr] -> ([Expr], [Expr])
split (Expr
rExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
kacc) [Expr]
pacc [Expr]
rs
        split [Expr]
kacc [Expr]
pacc (Expr
r:[Expr]
rs) = [Expr] -> [Expr] -> [Expr] -> ([Expr], [Expr])
split [Expr]
kacc (Expr
rExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
pacc) [Expr]
rs
        split [Expr]
kacc [Expr]
pacc [] = ([Expr]
kacc,[Expr]
pacc)
hornify (Head Pred
h a
a) = Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head Pred
h a
a
hornify (All Bind
b Cstr a
c) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
hornify Cstr a
c
hornify (Any Bind
b Cstr a
c) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
Any Bind
b (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
hornify Cstr a
c
hornify (CAnd [Cstr a]
cs) = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ([Cstr a] -> Cstr a) -> [Cstr a] -> Cstr a
forall a b. (a -> b) -> a -> b
$ Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
hornify (Cstr a -> Cstr a) -> [Cstr a] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs

removeDuplicateBinders :: Cstr a -> Cstr a
removeDuplicateBinders :: Cstr a -> Cstr a
removeDuplicateBinders = Set Symbol -> Cstr a -> Cstr a
forall a. Set Symbol -> Cstr a -> Cstr a
go Set Symbol
forall a. Set a
S.empty
  where
    go :: Set Symbol -> Cstr a -> Cstr a
go Set Symbol
_ c :: Cstr a
c@Head{} = Cstr a
c
    go Set Symbol
xs (CAnd [Cstr a]
cs) = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd ([Cstr a] -> Cstr a) -> [Cstr a] -> Cstr a
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Cstr a -> Cstr a
go Set Symbol
xs (Cstr a -> Cstr a) -> [Cstr a] -> [Cstr a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cstr a]
cs
    go Set Symbol
xs (All b :: Bind
b@(Bind Symbol
x Sort
_ Pred
_) Cstr a
c) = if Symbol
x Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Symbol
xs then Set Symbol -> Cstr a -> Cstr a
go Set Symbol
xs Cstr a
c else Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Cstr a -> Cstr a
go (Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
S.insert Symbol
x Set Symbol
xs) Cstr a
c
    go Set Symbol
xs (Any Bind
b Cstr a
c) = Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
Any Bind
b (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Cstr a -> Cstr a
go Set Symbol
xs Cstr a
c

pruneTauts :: Cstr a -> Cstr a
pruneTauts :: Cstr a -> Cstr a
pruneTauts = Cstr a -> Maybe (Cstr a) -> Cstr a
forall a. a -> Maybe a -> a
fromMaybe ([Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd []) (Maybe (Cstr a) -> Cstr a)
-> (Cstr a -> Maybe (Cstr a)) -> Cstr a -> Cstr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cstr a -> Maybe (Cstr a)
forall a. Cstr a -> Maybe (Cstr a)
go
  where
    go :: Cstr a -> Maybe (Cstr a)
go (Head Pred
p a
l) = do
      Pred
p' <- Pred -> Maybe Pred
goP Pred
p
      Cstr a -> Maybe (Cstr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cstr a -> Maybe (Cstr a)) -> Cstr a -> Maybe (Cstr a)
forall a b. (a -> b) -> a -> b
$ Pred -> a -> Cstr a
forall a. Pred -> a -> Cstr a
Head Pred
p' a
l
    go (CAnd [Cstr a]
cs) = if [Cstr a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Cstr a]
cs' then Maybe (Cstr a)
forall a. Maybe a
Nothing else Cstr a -> Maybe (Cstr a)
forall a. a -> Maybe a
Just (Cstr a -> Maybe (Cstr a)) -> Cstr a -> Maybe (Cstr a)
forall a b. (a -> b) -> a -> b
$ [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
CAnd [Cstr a]
cs'
      where cs' :: [Cstr a]
cs' = (Cstr a -> Maybe (Cstr a)) -> [Cstr a] -> [Cstr a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Cstr a -> Maybe (Cstr a)
go [Cstr a]
cs
    go (All Bind
b Cstr a
c) = do
      Cstr a
c' <- Cstr a -> Maybe (Cstr a)
go Cstr a
c
      Cstr a -> Maybe (Cstr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bind -> Cstr a -> Cstr a
forall a. Bind -> Cstr a -> Cstr a
All Bind
b Cstr a
c')
    go c :: Cstr a
c@Any{} = Cstr a -> Maybe (Cstr a)
forall a. a -> Maybe a
Just Cstr a
c

    goP :: Pred -> Maybe Pred
goP (Reft Expr
e) = if Expr -> Bool
F.isTautoPred Expr
e then Maybe Pred
forall a. Maybe a
Nothing else Pred -> Maybe Pred
forall a. a -> Maybe a
Just (Pred -> Maybe Pred) -> Pred -> Maybe Pred
forall a b. (a -> b) -> a -> b
$ Expr -> Pred
Reft Expr
e
    goP p :: Pred
p@Var{} = Pred -> Maybe Pred
forall a. a -> Maybe a
Just Pred
p
    goP (PAnd [Pred]
ps) = if [Pred] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pred]
ps' then Maybe Pred
forall a. Maybe a
Nothing else Pred -> Maybe Pred
forall a. a -> Maybe a
Just (Pred -> Maybe Pred) -> Pred -> Maybe Pred
forall a b. (a -> b) -> a -> b
$ [Pred] -> Pred
PAnd [Pred]
ps'
      where ps' :: [Pred]
ps' = (Pred -> Maybe Pred) -> [Pred] -> [Pred]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Pred -> Maybe Pred
goP [Pred]
ps