{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ViewPatterns #-}

{-|
Module      : Data.CDCL
Description : Conflict-directed clause learning utilities.
Copyright   : (c) Tom Harding, 2020
License     : MIT

Each parameter in a computation has a unique identifier, which we refer to as
its 'Major' index. Each possible /value/ of a parameter is also assigned a
unique identifier, which we refer to as its 'Minor' index.

When a conflict arises in a computation, the cause of the conflict can be
identified by a set of @('Major', 'Minor')@ pairs. Then, every branch that
involves those parameters set to /those/ values can be eliminated, as we know
they'll eventually result in a conflict.*

This module takes the conflicts we encounter, and tries to generalise them to
eliminate as many redundant branches as possible.

* In practice, we don't do this exactly. Instead, we run every branch until we
spot a cell with a previously-identified "no good" provenance. This means we
don't have to enumerate all the possible branches up front, which could end up
costing us a lot of time for no reason.
-}
module Data.CDCL where

import Control.Monad (guard)
import Data.Bifunctor (first)
import Data.Function ((&))
import Data.Functor (($>))
import Data.Hashable (Hashable)
import Data.HashMap.Strict (HashMap)
import Data.Maybe (mapMaybe)
import qualified Data.HashMap.Strict as HashMap
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet

-- | The index of a parameter in our computation.
type Major = Int

-- | The index of the chosen /value/ of a parameter in our computation.
type Minor = Int

-- | A set of value identifiers and their settings.
newtype Rule
  = Rule { Rule -> HashMap (Major, Major) Bool
toHashMap :: HashMap (Major, Minor) Bool }
  deriving newtype (Major -> Rule -> Major
Rule -> Major
(Major -> Rule -> Major) -> (Rule -> Major) -> Hashable Rule
forall a. (Major -> a -> Major) -> (a -> Major) -> Hashable a
hash :: Rule -> Major
$chash :: Rule -> Major
hashWithSalt :: Major -> Rule -> Major
$chashWithSalt :: Major -> Rule -> Major
Hashable, Semigroup Rule
Rule
Semigroup Rule
-> Rule
-> (Rule -> Rule -> Rule)
-> ([Rule] -> Rule)
-> Monoid Rule
[Rule] -> Rule
Rule -> Rule -> Rule
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Rule] -> Rule
$cmconcat :: [Rule] -> Rule
mappend :: Rule -> Rule -> Rule
$cmappend :: Rule -> Rule -> Rule
mempty :: Rule
$cmempty :: Rule
$cp1Monoid :: Semigroup Rule
Monoid, b -> Rule -> Rule
NonEmpty Rule -> Rule
Rule -> Rule -> Rule
(Rule -> Rule -> Rule)
-> (NonEmpty Rule -> Rule)
-> (forall b. Integral b => b -> Rule -> Rule)
-> Semigroup Rule
forall b. Integral b => b -> Rule -> Rule
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> Rule -> Rule
$cstimes :: forall b. Integral b => b -> Rule -> Rule
sconcat :: NonEmpty Rule -> Rule
$csconcat :: NonEmpty Rule -> Rule
<> :: Rule -> Rule -> Rule
$c<> :: Rule -> Rule -> Rule
Semigroup)
  deriving stock (Rule -> Rule -> Bool
(Rule -> Rule -> Bool) -> (Rule -> Rule -> Bool) -> Eq Rule
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rule -> Rule -> Bool
$c/= :: Rule -> Rule -> Bool
== :: Rule -> Rule -> Bool
$c== :: Rule -> Rule -> Bool
Eq, Major -> Rule -> ShowS
[Rule] -> ShowS
Rule -> String
(Major -> Rule -> ShowS)
-> (Rule -> String) -> ([Rule] -> ShowS) -> Show Rule
forall a.
(Major -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rule] -> ShowS
$cshowList :: [Rule] -> ShowS
show :: Rule -> String
$cshow :: Rule -> String
showsPrec :: Major -> Rule -> ShowS
$cshowsPrec :: Major -> Rule -> ShowS
Show)

-- | Generate unique rules for a set of possible values for a given parameter.
-- For example, if we assign parameter @#1@ possible values @[1 .. 4]@, this
-- function might generate something like:
--
-- @
-- [ ( -(1, 0) && -(1, 1), 1 )
-- , ( -(1, 0) &&  (1, 1), 2 )
-- , (  (1, 1) && -(1, 1), 3 )
-- , (  (1, 1) &&  (1, 1), 4 )
-- ]
-- @
index :: Major -> [ x ] -> [( Rule, x )]
index :: Major -> [x] -> [(Rule, x)]
index Major
major [x]
items = (([Bool], x) -> (Rule, x)) -> [([Bool], x)] -> [(Rule, x)]
forall a b. (a -> b) -> [a] -> [b]
map (([Bool] -> Rule) -> ([Bool], x) -> (Rule, x)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first [Bool] -> Rule
rulify) ([x] -> [([Bool], x)]
forall x. [x] -> [([Bool], x)]
go [x]
items)
  where
    rulify :: [Bool] -> Rule
rulify = HashMap (Major, Major) Bool -> Rule
Rule (HashMap (Major, Major) Bool -> Rule)
-> ([Bool] -> HashMap (Major, Major) Bool) -> [Bool] -> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((Major, Major), Bool)] -> HashMap (Major, Major) Bool
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList ([((Major, Major), Bool)] -> HashMap (Major, Major) Bool)
-> ([Bool] -> [((Major, Major), Bool)])
-> [Bool]
-> HashMap (Major, Major) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Major -> Bool -> ((Major, Major), Bool))
-> [Major] -> [Bool] -> [((Major, Major), Bool)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Major -> Bool -> ((Major, Major), Bool)
forall b b. b -> b -> ((Major, b), b)
zipper [Major
0 ..]
    zipper :: b -> b -> ((Major, b), b)
zipper b
minor b
value = ((Major
major, b
minor), b
value)

    go :: [ x ] -> [( [Bool], x )]
    go :: [x] -> [([Bool], x)]
go = \case
      [ ] -> []
      [x
x] -> ([Bool], x) -> [([Bool], x)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Bool]
forall a. Monoid a => a
mempty, x
x)

      xs :: [x]
xs@([x] -> Major
forall (t :: * -> *) a. Foldable t => t a -> Major
length -> Major
count) -> do
        let ([x] -> [([Bool], x)]
forall x. [x] -> [([Bool], x)]
go -> [([Bool], x)]
true, [x] -> [([Bool], x)]
forall x. [x] -> [([Bool], x)]
go -> [([Bool], x)]
false) = Major -> [x] -> ([x], [x])
forall a. Major -> [a] -> ([a], [a])
splitAt (Major
count Major -> Major -> Major
forall a. Integral a => a -> a -> a
`div` Major
2) [x]
xs
        (([Bool], x) -> ([Bool], x)) -> [([Bool], x)] -> [([Bool], x)]
forall a b. (a -> b) -> [a] -> [b]
map (([Bool] -> [Bool]) -> ([Bool], x) -> ([Bool], x)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Bool
True Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:)) [([Bool], x)]
true [([Bool], x)] -> [([Bool], x)] -> [([Bool], x)]
forall a. Semigroup a => a -> a -> a
<> (([Bool], x) -> ([Bool], x)) -> [([Bool], x)] -> [([Bool], x)]
forall a b. (a -> b) -> [a] -> [b]
map (([Bool] -> [Bool]) -> ([Bool], x) -> ([Bool], x)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Bool
False Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:)) [([Bool], x)]
false

-- | List all the @(Major, Minor)@ pairs in a 'Rule'.
variables :: Rule -> [(Major, Minor)]
variables :: Rule -> [(Major, Major)]
variables = HashMap (Major, Major) Bool -> [(Major, Major)]
forall k v. HashMap k v -> [k]
HashMap.keys (HashMap (Major, Major) Bool -> [(Major, Major)])
-> (Rule -> HashMap (Major, Major) Bool)
-> Rule
-> [(Major, Major)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> HashMap (Major, Major) Bool
toHashMap

-- | Toggle the boolean switch of a @(Major, Minor)@ pair.
invert :: (Major, Minor) -> Rule -> Rule
invert :: (Major, Major) -> Rule -> Rule
invert (Major, Major)
key = HashMap (Major, Major) Bool -> Rule
Rule (HashMap (Major, Major) Bool -> Rule)
-> (Rule -> HashMap (Major, Major) Bool) -> Rule -> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Maybe Bool)
-> (Major, Major)
-> HashMap (Major, Major) Bool
-> HashMap (Major, Major) Bool
forall k a.
(Eq k, Hashable k) =>
(a -> Maybe a) -> k -> HashMap k a -> HashMap k a
HashMap.update (Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> (Bool -> Bool) -> Bool -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not) (Major, Major)
key (HashMap (Major, Major) Bool -> HashMap (Major, Major) Bool)
-> (Rule -> HashMap (Major, Major) Bool)
-> Rule
-> HashMap (Major, Major) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> HashMap (Major, Major) Bool
toHashMap

-- | Remove a @(Major, Minor)@ pair from a 'Rule'.
remove :: (Major, Minor) -> Rule -> Rule
remove :: (Major, Major) -> Rule -> Rule
remove (Major, Major)
key = HashMap (Major, Major) Bool -> Rule
Rule (HashMap (Major, Major) Bool -> Rule)
-> (Rule -> HashMap (Major, Major) Bool) -> Rule -> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Major, Major)
-> HashMap (Major, Major) Bool -> HashMap (Major, Major) Bool
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HashMap.delete (Major, Major)
key (HashMap (Major, Major) Bool -> HashMap (Major, Major) Bool)
-> (Rule -> HashMap (Major, Major) Bool)
-> Rule
-> HashMap (Major, Major) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> HashMap (Major, Major) Bool
toHashMap

-- | A set of rules. We use this to represent our global list of "no good"
-- configurations. If any cell's provenance ever contains one of the rules in
-- our global set, we know this computation will eventually end in failure.
newtype Group
  = Group { Group -> HashSet Rule
toSet :: HashSet Rule }
  deriving newtype (Semigroup Group
Group
Semigroup Group
-> Group
-> (Group -> Group -> Group)
-> ([Group] -> Group)
-> Monoid Group
[Group] -> Group
Group -> Group -> Group
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Group] -> Group
$cmconcat :: [Group] -> Group
mappend :: Group -> Group -> Group
$cmappend :: Group -> Group -> Group
mempty :: Group
$cmempty :: Group
$cp1Monoid :: Semigroup Group
Monoid)

instance Semigroup Group where
  Group HashSet Rule
these <> :: Group -> Group -> Group
<> Group HashSet Rule
those
    = (Rule -> Group -> Group) -> Group -> HashSet Rule -> Group
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Rule -> Group -> Group
resolve Group
forall a. Monoid a => a
mempty (HashSet Rule
these HashSet Rule -> HashSet Rule -> HashSet Rule
forall a. Semigroup a => a -> a -> a
<> HashSet Rule
those)

-- | If a group implies @(A && B)@ /and/ @(A && -B)@ then the @B@ seems to be
-- irrelevant, so we can refine the 'Rule' to @A@. This hopefully means we can
-- eliminate /more/ branches, and get to an answer faster!
refinements :: Rule -> Group -> [Rule]
refinements :: Rule -> Group -> [Rule]
refinements Rule
rule Group
group = Rule -> [(Major, Major)]
variables Rule
rule [(Major, Major)] -> ([(Major, Major)] -> [Rule]) -> [Rule]
forall a b. a -> (a -> b) -> b
& ((Major, Major) -> Maybe Rule) -> [(Major, Major)] -> [Rule]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe \(Major, Major)
key ->
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Group
group Group -> Rule -> Bool
`implies` (Major, Major) -> Rule -> Rule
invert (Major, Major)
key Rule
rule) Maybe () -> Rule -> Maybe Rule
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (Major, Major) -> Rule -> Rule
remove (Major, Major)
key Rule
rule

-- | Does any 'Rule' in this 'Group' subsume the given 'Rule'?
implies :: Group -> Rule -> Bool
implies :: Group -> Rule -> Bool
implies (Group HashSet Rule
group) Rule
candidate = (Rule -> Bool) -> HashSet Rule -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Rule -> Rule -> Bool
`subsumes` Rule
candidate) HashSet Rule
group

-- | If @x@ 'subsumes' @y@, then the set of switches in @x@ is a strict
-- __subset__ of the switches in @y@. In other words, the @x@ 'Rule' will match
-- /everything/ that @y@ will.
subsumes :: Rule -> Rule -> Bool
subsumes :: Rule -> Rule -> Bool
subsumes (Rule HashMap (Major, Major) Bool
these) (Rule HashMap (Major, Major) Bool
those) = ((Major, Major) -> Bool -> Bool -> Bool)
-> Bool -> HashMap (Major, Major) Bool -> Bool
forall k v a. (k -> v -> a -> a) -> a -> HashMap k v -> a
HashMap.foldrWithKey (Major, Major) -> Bool -> Bool -> Bool
check Bool
True HashMap (Major, Major) Bool
these
  where check :: (Major, Major) -> Bool -> Bool -> Bool
check (Major, Major)
key Bool
value Bool
acc = (Major, Major) -> HashMap (Major, Major) Bool -> Maybe Bool
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup (Major, Major)
key HashMap (Major, Major) Bool
those Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
value Bool -> Bool -> Bool
&& Bool
acc

-- | Add a new 'Rule' to a 'Group'. Attempt to calculate any 'refinements' of
-- the rule, and generalise the 'Group' as far as possible.
resolve :: Rule -> Group -> Group
resolve :: Rule -> Group -> Group
resolve Rule
rule Group
group | Group
group Group -> Rule -> Bool
`implies` Rule
rule = Group
group
resolve rule :: Rule
rule@(Rule HashMap (Major, Major) Bool
config) group :: Group
group@(Group HashSet Rule
rules)
  = case Rule -> Group -> [Rule]
refinements Rule
rule Group
group of
      [] -> HashSet Rule -> Group
Group case HashMap (Major, Major) Bool -> [((Major, Major), Bool)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap (Major, Major) Bool
config of
        [ ((Major, Major)
key, Bool
value) ] -> do -- Unit propagation
          Rule -> HashSet Rule -> HashSet Rule
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert Rule
rule (HashSet Rule -> HashSet Rule) -> HashSet Rule -> HashSet Rule
forall a b. (a -> b) -> a -> b
$ HashSet Rule
rules HashSet Rule -> (HashSet Rule -> HashSet Rule) -> HashSet Rule
forall a b. a -> (a -> b) -> b
& (Rule -> Rule) -> HashSet Rule -> HashSet Rule
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
HashSet.map \(Rule HashMap (Major, Major) Bool
current) -> do
            if (Major, Major) -> HashMap (Major, Major) Bool -> Maybe Bool
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup (Major, Major)
key HashMap (Major, Major) Bool
current Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
value
              then HashMap (Major, Major) Bool -> Rule
Rule ((Major, Major)
-> HashMap (Major, Major) Bool -> HashMap (Major, Major) Bool
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HashMap.delete (Major, Major)
key HashMap (Major, Major) Bool
current)
              else Rule
rule

        [((Major, Major), Bool)]
_ -> HashSet Rule
rules HashSet Rule -> (HashSet Rule -> HashSet Rule) -> HashSet Rule
forall a b. a -> (a -> b) -> b
& (Rule -> Bool) -> HashSet Rule -> HashSet Rule
forall a. (a -> Bool) -> HashSet a -> HashSet a
HashSet.filter (Bool -> Bool
not (Bool -> Bool) -> (Rule -> Bool) -> Rule -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule
rule Rule -> Rule -> Bool
`subsumes`))
                   HashSet Rule -> (HashSet Rule -> HashSet Rule) -> HashSet Rule
forall a b. a -> (a -> b) -> b
& Rule -> HashSet Rule -> HashSet Rule
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert Rule
rule

      [Rule]
better -> (Rule -> Group -> Group) -> Group -> [Rule] -> Group
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Rule -> Group -> Group
resolve Group
group [Rule]
better