Contains helper functions to query CafeSat solvers on formulas.
Here is a simple example to get you started, we build a very simple formula
and then send it as a parameter to solveForSatisfiability
that returns an option of a Model:
import FormulaBuilder._
import Formulas._
val a: PropVar = propVar("a")
val b: PropVar = propVar("b")
val f: Formula = a && (!a || b)
Solver.solveForSatisfiability(f) match {
caseNone=> {
println("There is no solution")
}
caseSome(model) => {
val valueA: Boolean = model(a)
val valueB: Boolean = model(b)
println("a is: " valueA)
println("b is: " valueB)
}
}
Contains helper functions to query CafeSat solvers on formulas.
Here is a simple example to get you started, we build a very simple formula and then send it as a parameter to solveForSatisfiability that returns an option of a Model: