package smt
Ordering
- Alphabetic
Visibility
- Public
- Protected
Type Members
- class CompactEncoding extends AnyRef
- sealed trait SExpr extends AnyRef
- case class SExprLeaf(value: String) extends SExpr with Product with Serializable
- case class SExprNode(children: List[SExpr]) extends SExpr with Product with Serializable
- class SMTModelChecker extends IsModelChecker
SMT based bounded model checking as an alternative to dispatching to a btor2 based external solver
- case class SMTModelCheckerOptions(checkConstraints: Boolean, checkBadStatesIndividually: Boolean) extends Product with Serializable
Value Members
- object CVC4SMTLib extends Solver
- object SExprParser
simple S-Expression parser to make sense of SMTLib solver output
- object SMTModelCheckerOptions extends Serializable
- object Yices2SMTLib extends Solver
- object Z3SMTLib extends Solver