module Data.Presburger.Omega.LowLevel
(
Presburger,
OmegaSet, newOmegaSet,
OmegaRel, newOmegaRel,
queryDNFSet, queryDNFRelation,
lowerBoundSatisfiable, upperBoundSatisfiable,
obviousTautology, definiteTautology,
exact, inexact, unknown,
upperBound, lowerBound,
equal, union, intersection, composition,
restrictDomain, restrictRange,
difference, crossProduct,
Effort(..),
gist,
transitiveClosure,
domain, range, inverse, complement,
deltas, approximate,
Formula,
true, false,
conjunction, disjunction, negation,
VarHandle,
qForall, qExists,
Coefficient(..),
inequality, equality
)
where
import Control.Monad
import Data.Int
import Data.List(findIndex)
import Data.Word
import Foreign.C
import Foreign.ForeignPtr
import qualified Foreign.Marshal.Alloc as ForeignAlloc
import Foreign.Marshal.Array
import Foreign.Ptr
import Foreign.Storable
import System.IO.Unsafe(unsafePerformIO)
data Relation
data Form
data F_And
data F_Declaration
data Var_Decl
data DNF_Iterator
data Conjunct
data Tuple_Iterator a
data EQ_Iterator
data EQ_Handle
data GEQ_Iterator
data GEQ_Handle
data Constr_Vars_Iter
class Constraint a
instance Constraint EQ_Handle
instance Constraint GEQ_Handle
type C_Relation = Ptr Relation
type C_Form = Ptr Form
type C_And = Ptr F_And
type C_Quantifier = Ptr F_Declaration
type C_Var = Ptr Var_Decl
type C_DNF_Iterator = Ptr DNF_Iterator
type C_Conjunct = Ptr Conjunct
type C_Tuple_Iterator a = Ptr (Tuple_Iterator a)
type C_EQ_Iterator = Ptr EQ_Iterator
type C_EQ_Handle = Ptr EQ_Handle
type C_GEQ_Iterator = Ptr GEQ_Iterator
type C_GEQ_Handle = Ptr GEQ_Handle
type C_Constr_Vars_Iter = Ptr Constr_Vars_Iter
data Effort = Light | Moderate | Strenuous
deriving (Eq, Show, Enum)
class Logical f where
add_and :: f -> IO C_Form
add_or :: f -> IO C_Form
add_not :: f -> IO C_Form
add_forall :: f -> IO C_Quantifier
add_exists :: f -> IO C_Quantifier
convert_to_and :: f -> IO C_And
finalize :: f -> IO ()
instance Logical C_Relation where
add_and = hsw_relation_add_and
add_or = hsw_relation_add_or
add_not = hsw_relation_add_not
add_forall = hsw_relation_add_forall
add_exists = hsw_relation_add_exists
convert_to_and r = liftM castPtr $ hsw_relation_add_and r
finalize = hsw_relation_finalize
instance Logical C_Form where
add_and = hsw_formula_add_and
add_or = hsw_formula_add_or
add_not = hsw_formula_add_not
add_forall = hsw_formula_add_forall
add_exists = hsw_formula_add_exists
convert_to_and = hsw_formula_to_and
finalize = hsw_formula_finalize
instance Logical C_And where
add_and = hsw_formula_add_and . castPtr
add_or = hsw_formula_add_or . castPtr
add_not = hsw_formula_add_not . castPtr
add_forall = hsw_formula_add_forall . castPtr
add_exists = hsw_formula_add_exists . castPtr
convert_to_and = return
finalize = hsw_formula_finalize . castPtr
instance Logical C_Quantifier where
add_and = hsw_formula_add_and . castPtr
add_or = hsw_formula_add_or . castPtr
add_not = hsw_formula_add_not . castPtr
add_forall = hsw_formula_add_forall . castPtr
add_exists = hsw_formula_add_exists . castPtr
convert_to_and = hsw_formula_to_and . castPtr
finalize = hsw_formula_finalize . castPtr
foreign import ccall safe free :: Ptr a -> IO ()
foreign import ccall safe hsw_new_relation
:: CInt -> CInt -> IO C_Relation
foreign import ccall safe hsw_new_set
:: CInt -> IO C_Relation
foreign import ccall safe hsw_free_relation
:: C_Relation -> IO ()
foreign import ccall "&hsw_free_relation" ptr_to_free_relation
:: FunPtr (C_Relation -> IO ())
foreign import ccall safe hsw_relation_show
:: C_Relation -> IO CString
foreign import ccall safe hsw_num_input_vars
:: C_Relation -> IO CInt
foreign import ccall safe hsw_num_output_vars
:: C_Relation -> IO CInt
foreign import ccall safe hsw_num_set_vars
:: C_Relation -> IO CInt
foreign import ccall safe hsw_input_var
:: C_Relation -> CInt -> IO C_Var
foreign import ccall safe hsw_output_var
:: C_Relation -> CInt -> IO C_Var
foreign import ccall safe hsw_set_var
:: C_Relation -> CInt -> IO C_Var
foreign import ccall safe hsw_is_lower_bound_satisfiable
:: C_Relation -> IO Bool
foreign import ccall safe hsw_is_upper_bound_satisfiable
:: C_Relation -> IO Bool
foreign import ccall safe hsw_is_obvious_tautology
:: C_Relation -> IO Bool
foreign import ccall safe hsw_is_definite_tautology
:: C_Relation -> IO Bool
foreign import ccall safe hsw_is_exact
:: C_Relation -> IO Bool
foreign import ccall safe hsw_is_inexact
:: C_Relation -> IO Bool
foreign import ccall safe hsw_is_unknown
:: C_Relation -> IO Bool
foreign import ccall safe hsw_upper_bound
:: C_Relation -> IO C_Relation
foreign import ccall safe hsw_lower_bound
:: C_Relation -> IO C_Relation
foreign import ccall safe hsw_equal
:: C_Relation -> C_Relation -> IO CInt
foreign import ccall safe hsw_union
:: C_Relation -> C_Relation -> IO C_Relation
foreign import ccall safe hsw_intersection
:: C_Relation -> C_Relation -> IO C_Relation
foreign import ccall safe hsw_composition
:: C_Relation -> C_Relation -> IO C_Relation
foreign import ccall safe hsw_restrict_domain
:: C_Relation -> C_Relation -> IO C_Relation
foreign import ccall safe hsw_restrict_range
:: C_Relation -> C_Relation -> IO C_Relation
foreign import ccall safe hsw_difference
:: C_Relation -> C_Relation -> IO C_Relation
foreign import ccall safe hsw_cross_product
:: C_Relation -> C_Relation -> IO C_Relation
foreign import ccall safe hsw_gist
:: C_Relation -> C_Relation -> CInt -> IO C_Relation
foreign import ccall safe hsw_transitive_closure
:: C_Relation -> IO C_Relation
foreign import ccall safe hsw_domain
:: C_Relation -> IO C_Relation
foreign import ccall safe hsw_range
:: C_Relation -> IO C_Relation
foreign import ccall safe hsw_inverse
:: C_Relation -> IO C_Relation
foreign import ccall safe hsw_complement
:: C_Relation -> IO C_Relation
foreign import ccall safe hsw_deltas
:: C_Relation -> IO C_Relation
foreign import ccall safe hsw_approximate
:: C_Relation -> IO C_Relation
foreign import ccall safe hsw_relation_add_and
:: C_Relation -> IO C_Form
foreign import ccall safe hsw_relation_add_or
:: C_Relation -> IO C_Form
foreign import ccall safe hsw_relation_add_not
:: C_Relation -> IO C_Form
foreign import ccall safe hsw_relation_add_forall
:: C_Relation -> IO C_Quantifier
foreign import ccall safe hsw_relation_add_exists
:: C_Relation -> IO C_Quantifier
foreign import ccall safe hsw_relation_finalize
:: C_Relation -> IO ()
foreign import ccall safe hsw_formula_add_and
:: C_Form -> IO C_Form
foreign import ccall safe hsw_formula_add_or
:: C_Form -> IO C_Form
foreign import ccall safe hsw_formula_add_not
:: C_Form -> IO C_Form
foreign import ccall safe hsw_formula_add_forall
:: C_Form -> IO C_Quantifier
foreign import ccall safe hsw_formula_add_exists
:: C_Form -> IO C_Quantifier
foreign import ccall safe hsw_formula_finalize
:: C_Form -> IO ()
foreign import ccall safe hsw_declaration_declare
:: C_Quantifier -> IO C_Var
foreign import ccall safe hsw_formula_to_and
:: C_Form -> IO C_And
foreign import ccall safe hsw_add_constraint
:: C_And -> Bool -> CInt -> Ptr CInt -> Ptr C_Var -> CInt -> IO ()
foreign import ccall safe separate_relation_dimensions
:: Ptr C_Relation -> C_Relation -> IO ()
foreign import ccall safe hsw_query_dnf
:: C_Relation -> IO C_DNF_Iterator
foreign import ccall safe hsw_dnf_iterator_next
:: C_DNF_Iterator -> IO C_Conjunct
foreign import ccall safe hsw_dnf_iterator_free
:: C_DNF_Iterator -> IO ()
foreign import ccall safe hsw_get_conjunct_variables
:: C_Conjunct -> IO (C_Tuple_Iterator C_Var)
foreign import ccall safe hsw_tuple_iterator_next
:: (C_Tuple_Iterator (Ptr a)) -> IO (Ptr a)
foreign import ccall safe hsw_tuple_iterator_free
:: (C_Tuple_Iterator a) -> IO ()
foreign import ccall safe hsw_get_eqs
:: C_Conjunct -> IO C_EQ_Iterator
foreign import ccall safe hsw_eqs_next
:: C_EQ_Iterator -> IO C_EQ_Handle
foreign import ccall safe hsw_eqs_free
:: C_EQ_Iterator -> IO ()
foreign import ccall safe hsw_eq_handle_free
:: C_EQ_Handle -> IO ()
foreign import ccall safe hsw_get_geqs
:: C_Conjunct -> IO C_GEQ_Iterator
foreign import ccall safe hsw_geqs_next
:: C_GEQ_Iterator -> IO C_GEQ_Handle
foreign import ccall safe hsw_geqs_free
:: C_GEQ_Iterator -> IO ()
foreign import ccall safe hsw_geq_handle_free
:: C_GEQ_Handle -> IO ()
foreign import ccall safe hsw_constraint_get_const
:: Ptr a -> IO Int64
foreign import ccall safe hsw_constraint_get_coefficients
:: Ptr a -> IO C_Constr_Vars_Iter
foreign import ccall safe hsw_constr_vars_next
:: Ptr Coefficient -> C_Constr_Vars_Iter -> IO Bool
foreign import ccall safe hsw_constr_vars_free
:: C_Constr_Vars_Iter -> IO ()
foreign import ccall safe hsw_debug_print_eq
:: C_EQ_Handle -> IO ()
foreign import ccall safe hsw_debug_print_geq
:: C_GEQ_Handle -> IO ()
class Iterator i a | i -> a where next :: i -> IO a
instance Iterator C_DNF_Iterator C_Conjunct where
next = hsw_dnf_iterator_next
instance Iterator (C_Tuple_Iterator (Ptr a)) (Ptr a) where
next = hsw_tuple_iterator_next
instance Iterator C_EQ_Iterator C_EQ_Handle where
next = hsw_eqs_next
instance Iterator C_GEQ_Iterator C_GEQ_Handle where
next = hsw_geqs_next
foreach :: Iterator i (Ptr b) => (a -> Ptr b -> IO a) -> a -> i -> IO a
foreach f x iter = visit x
where
visit x = do y <- next iter
if y == nullPtr
then return x
else visit =<< f x y
iterateDNF :: (a -> C_Conjunct -> IO a) -> a -> C_Relation -> IO a
iterateDNF f x rel = do
iter <- hsw_query_dnf rel
x' <- foreach f x iter
hsw_dnf_iterator_free iter
return x'
iterateConjVars :: (a -> C_Var -> IO a) -> a -> C_Conjunct -> IO a
iterateConjVars f x conj = do
iter <- hsw_get_conjunct_variables conj
x' <- foreach f x iter
hsw_tuple_iterator_free iter
return x'
iterateEqs :: (a -> C_EQ_Handle -> IO a) -> a -> C_Conjunct -> IO a
iterateEqs f x conj = do
iter <- hsw_get_eqs conj
x' <- foreach wrapped_f x iter
hsw_eqs_free iter
return x'
where
wrapped_f x eqHdl = do
x' <- f x eqHdl
hsw_eq_handle_free eqHdl
return x'
iterateGeqs :: (a -> C_GEQ_Handle -> IO a) -> a -> C_Conjunct -> IO a
iterateGeqs f x conj = do
iter <- hsw_get_geqs conj
x' <- foreach wrapped_f x iter
hsw_geqs_free iter
return x'
where
wrapped_f x geqHdl = do
x' <- f x geqHdl
hsw_geq_handle_free geqHdl
return x'
peekConstraintVars :: Constraint a => Ptr a -> IO [Coefficient]
peekConstraintVars cst = do
iter <- hsw_constraint_get_coefficients cst
c_var_info <- ForeignAlloc.malloc
coeffs <- getCoefficients iter c_var_info []
ForeignAlloc.free c_var_info
hsw_constr_vars_free iter
return coeffs
where
getCoefficients iter c_var_info coeffs = do
ok <- hsw_constr_vars_next c_var_info iter
if not ok then return coeffs else do
coeff <- peek c_var_info
getCoefficients iter c_var_info (coeff:coeffs)
peekInputVars, peekOutputVars, peekSetVars
:: CInt -> C_Relation -> IO [VarHandle]
peekInputVars n rel =
mapM (liftM VarHandle . hsw_input_var rel) [n, n 1 .. 1]
peekOutputVars n rel =
mapM (liftM VarHandle . hsw_output_var rel) [n, n 1 .. 1]
peekSetVars n rel =
mapM (liftM VarHandle . hsw_set_var rel) [n, n 1 .. 1]
queryConstraint :: Constraint c =>
([Coefficient] -> Int -> a -> a)
-> a
-> Ptr c
-> IO a
queryConstraint f acc eq = do
coefficients <- peekConstraintVars eq
constant <- hsw_constraint_get_const eq
return $ f coefficients (fromIntegral constant) acc
class Presburger a where
pPtr :: a -> ForeignPtr Relation
sameArity :: a -> a -> Bool
fromPtr :: Ptr Relation -> IO a
withPresburger :: Presburger a => a -> (C_Relation -> IO b) -> IO b
withPresburger p = withForeignPtr (pPtr p)
withPresburger2 :: (Presburger a, Presburger b) =>
a -> b -> (C_Relation -> C_Relation -> IO c) -> IO c
withPresburger2 p q f = withForeignPtr (pPtr p) $ \ptr ->
withForeignPtr (pPtr q) $ \ptr2 ->
f ptr ptr2
data OmegaSet = OmegaSet { sPtr :: !(ForeignPtr Relation)
, sDom :: [VarHandle]
}
instance Show OmegaSet where
show rel = unsafePerformIO $ withPresburger rel $ \ptr -> do
cStr <- hsw_relation_show ptr
str <- peekCString cStr
free cStr
return str
instance Presburger OmegaSet where
pPtr = sPtr
sameArity s1 s2 =
length (sDom s1) == length (sDom s2)
fromPtr ptr = do
numVars <- hsw_num_set_vars ptr
varIDs <- peekSetVars numVars ptr
wrapOmegaSet ptr varIDs
wrapOmegaSet :: C_Relation -> [VarHandle] -> IO OmegaSet
wrapOmegaSet ptr dom = do
foreignptr <- newForeignPtr ptr_to_free_relation ptr
return $! OmegaSet { sPtr = foreignptr
, sDom = dom
}
newOmegaSet :: Int
-> ([VarHandle] -> Formula)
-> IO OmegaSet
newOmegaSet numVars init = do
rel <- hsw_new_set (fromIntegral numVars)
freeVarIDs <- peekSetVars (fromIntegral numVars) rel
runFD (init freeVarIDs) rel
wrapOmegaSet rel freeVarIDs
queryDNFSet :: ([VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> a -> a)
-> a
-> ([VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> b -> b)
-> b
-> ([VarHandle] -> [VarHandle] -> a -> b -> c -> c)
-> c
-> OmegaSet
-> IO ([VarHandle], c)
queryDNFSet readEq unitEq readGeq unitGeq readConj unitConj s = do
conjuncts <- withPresburger s $ iterateDNF doConjunct unitConj
return (sDom s, conjuncts)
where
doConjunct acc conjunct = do
wildcardVars <- iterateConjVars findWildcards [] conjunct
let wc = map VarHandle wildcardVars
eqs <- iterateEqs (queryConstraint $ readEq (sDom s) wc)
unitEq conjunct
geqs <- iterateGeqs (queryConstraint $ readGeq (sDom s) wc)
unitGeq conjunct
return $ readConj (sDom s) wc eqs geqs acc
findWildcards acc var =
case findIndex (var ==) (map unVarHandle $ sDom s)
of Just n -> return acc
Nothing ->
return $ var : acc
data OmegaRel = OmegaRel { rPtr :: !(ForeignPtr Relation)
, rDom :: [VarHandle]
, rRng :: [VarHandle]
}
instance Show OmegaRel where
show rel = unsafePerformIO $ withPresburger rel $ \ptr -> do
cStr <- hsw_relation_show ptr
str <- peekCString cStr
free cStr
return str
instance Presburger OmegaRel where
pPtr = rPtr
sameArity r1 r2 =
length (rDom r1) == length (rDom r2) &&
length (rRng r1) == length (rRng r2)
fromPtr ptr = do
numOutputs <- hsw_num_output_vars ptr
outputVarIDs <- peekOutputVars numOutputs ptr
numInputs <- hsw_num_input_vars ptr
inputVarIDs <- peekInputVars numInputs ptr
wrapOmegaRel ptr inputVarIDs outputVarIDs
wrapOmegaRel :: C_Relation -> [VarHandle] -> [VarHandle] -> IO OmegaRel
wrapOmegaRel ptr dom rng = do
foreignptr <- newForeignPtr ptr_to_free_relation ptr
return $! OmegaRel { rPtr = foreignptr
, rDom = dom
, rRng = rng }
newOmegaRel :: Int
-> Int
-> ([VarHandle] -> [VarHandle] -> Formula)
-> IO OmegaRel
newOmegaRel numInputs numOutputs init = do
rel <- hsw_new_relation (fromIntegral numInputs) (fromIntegral numOutputs)
outputVarIds <- peekOutputVars (fromIntegral numOutputs) rel
inputVarIds <- peekInputVars (fromIntegral numInputs) rel
runFD (init inputVarIds outputVarIds) rel
wrapOmegaRel rel inputVarIds outputVarIds
queryDNFRelation :: ([VarHandle] -> [VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> a -> a)
-> a
-> ([VarHandle] -> [VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> b -> b)
-> b
-> ([VarHandle] -> [VarHandle] -> [VarHandle] -> a -> b -> c -> c)
-> c
-> OmegaRel
-> IO ([VarHandle], [VarHandle], c)
queryDNFRelation readEq unitEq readGeq unitGeq readConj unitConj r = do
conjuncts <- withPresburger r $ iterateDNF doConjunct unitConj
return (rDom r, rRng r, conjuncts)
where
doConjunct acc conjunct = do
wildcardVars <- iterateConjVars findWildcards [] conjunct
let wc = map VarHandle wildcardVars
eqs <- iterateEqs (queryConstraint $ readEq (rDom r) (rRng r) wc)
unitEq conjunct
geqs <- iterateGeqs (queryConstraint $ readGeq (rDom r) (rRng r) wc)
unitGeq conjunct
return $ readConj (rDom r) (rRng r) wc eqs geqs acc
findWildcards acc var =
case findIndex (var ==) (map unVarHandle $ rDom r ++ rRng r)
of Just n -> return acc
Nothing ->
return $ var : acc
separateRelationDimensions :: OmegaRel -> IO [OmegaRel]
separateRelationDimensions r = do
allocaArray numOutputs $ \outputArray -> do
withPresburger r $ \ptr -> separate_relation_dimensions outputArray ptr
mapM readRelation =<< peekArray numOutputs outputArray
where
numInputs = length $ rDom r
numOutputs = length $ rRng r
readRelation rel = do
outputVarIds <- peekOutputVars (fromIntegral numOutputs) rel
inputVarIds <- peekInputVars (fromIntegral numInputs) rel
wrapOmegaRel rel inputVarIds outputVarIds
lowerBoundSatisfiable :: Presburger a => a -> IO Bool
upperBoundSatisfiable :: Presburger a => a -> IO Bool
obviousTautology :: Presburger a => a -> IO Bool
definiteTautology :: Presburger a => a -> IO Bool
exact :: Presburger a => a -> IO Bool
inexact :: Presburger a => a -> IO Bool
unknown :: Presburger a => a -> IO Bool
lowerBoundSatisfiable rel = withPresburger rel hsw_is_lower_bound_satisfiable
upperBoundSatisfiable rel = withPresburger rel hsw_is_upper_bound_satisfiable
obviousTautology rel = withPresburger rel hsw_is_obvious_tautology
definiteTautology rel = withPresburger rel hsw_is_definite_tautology
exact rel = withPresburger rel hsw_is_exact
inexact rel = withPresburger rel hsw_is_inexact
unknown rel = withPresburger rel hsw_is_unknown
upperBound :: Presburger a => a -> IO a
upperBound rel = fromPtr =<< withPresburger rel hsw_upper_bound
lowerBound :: Presburger a => a -> IO a
lowerBound rel = fromPtr =<< withPresburger rel hsw_lower_bound
equal :: Presburger a => a -> a -> IO Bool
equal rel1 rel2
| sameArity rel1 rel2 = do
eq <- withPresburger2 rel1 rel2 hsw_equal
return $! eq /= 0
| otherwise = error "equal: arguments have different arities"
union :: Presburger a => a -> a -> IO a
union rel1 rel2
| sameArity rel1 rel2 =
fromPtr =<< withPresburger2 rel1 rel2 hsw_union
| otherwise = error "union: arguments have different arities"
intersection :: Presburger a => a -> a -> IO a
intersection rel1 rel2
| sameArity rel1 rel2 =
fromPtr =<< withPresburger2 rel1 rel2 hsw_intersection
| otherwise = error "intersection: arguments have different arities"
composition :: OmegaRel -> OmegaRel -> IO OmegaRel
composition rel1 rel2
| length (rDom rel1) == length (rRng rel2) =
fromPtr =<< withPresburger2 rel1 rel2 hsw_composition
| otherwise = error "composition: argument arities do not agree"
restrictDomain :: OmegaRel -> OmegaSet -> IO OmegaRel
restrictDomain rel1 set
| length (rDom rel1) == length (sDom set) =
fromPtr =<< withPresburger2 rel1 set hsw_restrict_domain
| otherwise = error "restrictDomain: argument arities do not agree"
restrictRange :: OmegaRel -> OmegaSet -> IO OmegaRel
restrictRange rel1 set
| length (rDom rel1) == length (sDom set) =
fromPtr =<< withPresburger2 rel1 set hsw_restrict_range
| otherwise = error "restrictRange: argument arities do not agree"
difference :: Presburger a => a -> a -> IO a
difference rel1 rel2
| sameArity rel1 rel2 =
fromPtr =<< withPresburger2 rel1 rel2 hsw_difference
| otherwise = error "difference: arguments have different arities"
crossProduct :: OmegaSet -> OmegaSet -> IO OmegaRel
crossProduct set1 set2 =
fromPtr =<< withPresburger2 set1 set2 hsw_cross_product
gist :: Presburger a => Effort -> a -> a -> IO a
gist effort rel given
| sameArity rel given =
withPresburger2 rel given $ \ptr ptrGiven ->
fromPtr =<< hsw_gist ptr ptrGiven (fromIntegral $ fromEnum effort)
| otherwise = error "gist: arguments have different arities"
transitiveClosure :: OmegaRel -> IO OmegaRel
transitiveClosure rel = fromPtr =<< withPresburger rel hsw_transitive_closure
domain :: OmegaRel -> IO OmegaSet
domain rel = fromPtr =<< withPresburger rel hsw_domain
range :: OmegaRel -> IO OmegaSet
range rel = fromPtr =<< withPresburger rel hsw_range
inverse :: OmegaRel -> IO OmegaRel
inverse rel = fromPtr =<< withPresburger rel hsw_inverse
complement :: Presburger a => a -> IO a
complement rel = fromPtr =<< withPresburger rel hsw_complement
deltas :: OmegaRel -> IO OmegaSet
deltas rel
| length (rDom rel) == length (rRng rel) =
fromPtr =<< withPresburger rel hsw_deltas
| otherwise =
error "deltas: relation has different input and output dimensionality"
approximate :: Presburger a => a -> IO a
approximate rel = fromPtr =<< withPresburger rel hsw_approximate
newtype Formula = FD {runFD :: forall a. Logical a => a -> IO ()}
conjunction :: [Formula] -> Formula
conjunction formulaDefs = FD $ \f -> do
newF <- add_and f
mapM_ (\func -> runFD func newF) formulaDefs
finalize newF
disjunction :: [Formula] -> Formula
disjunction formulaDefs = FD $ \f -> do
newF <- add_or f
mapM_ (\func -> runFD func newF) formulaDefs
finalize newF
negation :: Formula -> Formula
negation formulaDef = FD $ \f -> do
newF <- add_not f
runFD formulaDef newF
finalize newF
qForall :: (VarHandle -> Formula) -> Formula
qForall makeBody = FD $ \f -> do
newFormula <- add_forall f
localVar <- hsw_declaration_declare newFormula
runFD (makeBody (VarHandle localVar)) newFormula
finalize newFormula
qExists :: (VarHandle -> Formula) -> Formula
qExists makeBody = FD $ \f -> do
newFormula <- add_exists f
localVar <- hsw_declaration_declare newFormula
runFD (makeBody (VarHandle localVar)) newFormula
finalize newFormula
addConstraint :: Bool -> [Coefficient] -> Int -> C_And -> IO ()
addConstraint kind terms constant formula = do
let numTerms = length terms
numTermsCInt = fromIntegral numTerms
constantCInt = fromIntegral constant
coefficients = map (fromIntegral . coeffValue) terms
variables = map ((\(VarHandle h) -> h) . coeffVar) terms
withArray coefficients $ \coeffPtr ->
withArray variables $ \varPtr ->
hsw_add_constraint formula kind numTermsCInt coeffPtr varPtr constantCInt
inequality :: [Coefficient] -> Int -> Formula
inequality terms constant = FD $ \formula ->
addConstraint False terms constant =<< convert_to_and formula
equality :: [Coefficient] -> Int -> Formula
equality terms constant = FD $ \formula ->
addConstraint True terms constant =<< convert_to_and formula
true :: Formula
true = equality [] 0
false :: Formula
false = equality [] 1
newtype VarHandle = VarHandle { unVarHandle :: C_Var } deriving(Eq)
data Coefficient =
Coefficient { coeffVar :: !VarHandle
, coeffValue :: !Int
}
instance Show Coefficient where
show (Coefficient v n) =
"(" ++ show n ++ " * " ++ show (unVarHandle v) ++ ")"
instance Storable Coefficient where
sizeOf _ = (12)
alignment _ = 4
peek p = do
var <- (\hsc_ptr -> peekByteOff hsc_ptr 0) p :: IO C_Var
coef <- (\hsc_ptr -> peekByteOff hsc_ptr 4) p :: IO Int64
return $ Coefficient { coeffVar = VarHandle var
, coeffValue = fromIntegral coef
}