api

Provides a simple abstraction on top of CafeSat functionalities.

This is the expected entry point to use CafeSat as a library. It provides a simple and high-level abstraction over formulas with an opaque type Formulas.Formula, along with a simple language to build formulas and query their satisfiability.

Formulas contains the main definitions for the core types used to represent formulas.

FormulaBuilder provides the main building blocks to build formulas. You typically start a formula with a FormulaBuilder.propVar to obtain a propositional variable and then you can use boolean operators to build a more complex formula out of it.

Solver provides functions to query a solver over formulas.

Here is a short example where CafeSat is used to check the satisfiability of a simple formula:

import FormulaBuilder._
import Formulas._

val a: PropVar = propVar("a")
val b: PropVar = propVar("b")
val f: Formula = a && (!a || b)
Solver.solveForSatisfiability(f) match {
  case None => {
    println("There is no solution")
  }
  case Some(model) => {
    println("a is: " + model(a))
    println("b is: " + model(b))
  }
}

Linear Supertypes

AnyRef, Any

Type Members

trait Solver extends AnyRef

Value Members

object Extractors

Provides extractors to manipulate Formulas.Formula
object FormulaBuilder

Contains helper functions for building Formula.
Contains helper functions for building Formula.
The basic building blocks of formulas are true/false literals and propositional variables. You get a PropVar with propVar and bool2formula provides an implicit conversion from Boolean to True/False.
Once you have a Formula instance, you can combine it using its methods matching regular boolean operators. You can also use n-ary combinators or and and.
```
import Formulas._
import FormulaBuilder._

val a: PropVar = propVar("a")
val b: PropVar = propVar("b")
val f: Formula = and(a, (!a || b), (!b || false))
```
object Formulas

Contains type definitions for formulas.
Contains type definitions for formulas.
If you wish to instantiate a Formula or a PropVar, you need to use FormulaBuilder that will provide a generator function to create PropVar, and then build your formula from combinator methods in Formula.
Here is a simple example that shows how to build a formula:
```
import FormulaBuilder._
import Formulas._

val a: PropVar = propVar("a")
val b: PropVar = propVar("b")
val f: Formula = a && (!a || b)
```

object Solver

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 {
  case None => {
    println("There is no solution")
  }
  case Some(model) => {
    val valueA: Boolean = model(a)
    val valueB: Boolean = model(b)
    println("a is: " valueA)
    println("b is: " valueB)
  }
}

package api

Type Members

trait Solver extends AnyRef

Value Members

object Extractors

object FormulaBuilder

object Formulas

object Solver

Inherited from AnyRef

Inherited from Any

Ungrouped