toysolver-0.9.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2020
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010
Extensions
  • ScopedTypeVariables
  • BangPatterns
  • TypeSynonymInstances
  • FlexibleInstances
  • ConstrainedClassMethods
  • MultiParamTypeClasses
  • ExplicitForAll

ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer

Description

 

Documentation

data Encoder m Source #

Constructors

Encoder (Encoder m) (MutVar (PrimState m) (Map LitSet (Vector Var))) 

Instances

Instances details
Monad m => AddClause m (Encoder m) Source # 
Instance details

Defined in ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer

Methods

addClause :: Encoder m -> Clause -> m () Source #

Monad m => NewVar m (Encoder m) Source # 
Instance details

Defined in ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer

Methods

newVar :: Encoder m -> m Var Source #

newVars :: Encoder m -> Int -> m [Var] Source #

newVars_ :: Encoder m -> Int -> m () Source #

newEncoder :: PrimMonad m => Encoder m -> m (Encoder m) Source #

type Definitions = [(Vector Var, LitSet)] Source #

getDefinitions :: PrimMonad m => Encoder m -> m Definitions Source #

evalDefinitions :: IModel m => m -> Definitions -> [(Var, Bool)] Source #

addAtLeast :: PrimMonad m => Encoder m -> AtLeast -> m () Source #

encodeAtLeastWithPolarity :: PrimMonad m => Encoder m -> Polarity -> AtLeast -> m Lit Source #

addCardinality :: PrimMonad m => Encoder m -> [Lit] -> (Int, Int) -> m () Source #

encodeCardinalityWithPolarity :: PrimMonad m => Encoder m -> Polarity -> [Lit] -> (Int, Int) -> m Lit Source #

encodeSum :: PrimMonad m => Encoder m -> [Lit] -> m [Lit] Source #