Module

Mycroft.SmtLib

Package: purescript-mycroft
Repository: afcondon/purescript-mycroft

The typed veneer: untyped Terms built by smart constructors, simple-smt style. Enough SMTLib2 for finite-domain work — enum sorts, Int arithmetic for cardinality, uninterpreted functions, named assertions, models, unsat cores.

#Sort Source

newtype Sort

Constructors

Sort SExpr

#Term Source

newtype Term

Constructors

Term SExpr

Instances

Eq Term

#Result Source

data Result

Constructors

Instances

Eq Result
Show Result

#Model Source

type Model = Map String SExpr

Constant assignments from get-model: name ↦ value s-expression.

#setOption Source

setOption :: Solver -> String -> String -> Aff Unit

#produceModels Source

produceModels :: Solver -> Aff Unit

#produceUnsatCores Source

produceUnsatCores :: Solver -> Aff Unit

#declareEnum Source

declareEnum :: Solver -> { ctors :: Array String, name :: String } -> Aff Sort

(declare-datatypes ((Name 0)) (((c1) (c2) …))) — a nullary datatype, i.e. an enumeration.

#declareConst Source

declareConst :: Solver -> String -> Sort -> Aff Term

#declareFun Source

declareFun :: Solver -> String -> Array Sort -> Sort -> Aff Term

#assert Source

assert :: Solver -> Term -> Aff Unit

#assertNamed Source

assertNamed :: Solver -> String -> Term -> Aff Unit

(assert (! t :named n)) — named assertions are what unsat cores are made of.

#checkSat Source

checkSat :: Solver -> Aff Result

#getModel Source

getModel :: Solver -> Aff Model

#getUnsatCore Source

getUnsatCore :: Solver -> Aff (Array String)

#push Source

push :: Solver -> Aff Unit

#pop Source

pop :: Solver -> Aff Unit

#inNewScope Source

inNewScope :: forall a. Solver -> Aff a -> Aff a

Run an action inside a push/pop scope; the pop happens even if the action throws.

#tBool Source

tBool :: Sort

#tInt Source

tInt :: Sort

#var Source

var :: String -> Term

#app Source

app :: String -> Array Term -> Term

#eqT Source

eqT :: Term -> Term -> Term

#neqT Source

neqT :: Term -> Term -> Term

#distinct Source

distinct :: Array Term -> Term

#andT Source

andT :: Array Term -> Term

#orT Source

orT :: Array Term -> Term

#notT Source

notT :: Term -> Term

#implies Source

implies :: Term -> Term -> Term

#ite Source

ite :: Term -> Term -> Term -> Term

#boolLit Source

boolLit :: Boolean -> Term

#intLit Source

intLit :: Int -> Term

#addT Source

addT :: Array Term -> Term

#countEq Source

countEq :: Array Term -> Term -> Term

How many of the given terms equal the target — the sum-of-ite cardinality encoding, for hand-size style constraints.

#lookupAtom Source

lookupAtom :: Model -> String -> Maybe String

Read a model value that should be a bare atom (an Int literal or an enum constructor).

Modules: Mycroft.SExpr; Mycroft.SmtLib; Mycroft.Solver