Uses of Class
eu.bandm.tools.dpll.Formula

Packages that use Formula

Package	Description
eu.bandm.tools.dpll	Model and solver for propositional logic in conjunctive normal form.

Uses of Formula in eu.bandm.tools.dpll

Fields in eu.bandm.tools.dpll declared as Formula

Modifier and Type	Field	Description
protected Formula<P>	SATSolver.State.form	The remaining formula to be solved.
protected Formula<P>	SATSolver.State.solution	The solution candidate that records all committed steps.

Methods in eu.bandm.tools.dpll that return Formula

Modifier and Type	Method	Description
Formula<P>	Formula.and(Formula<P> other)	Returns the conjunction of this and another formula.
static <P> Formula<P>	Formula.bottom()	Returns a bottom formula.
static <P> Formula<P>	Formula.empty()	Returns an empty formula.
abstract Formula<P>	Formula.given(Literal<P> literal)	Returns a formula that abstracts from the given literal in this formula.
static <P> Formula<P>	Formula.horn(P consequent, Collection<? extends P> antecedents)	Returns a Horn formula with the given consequent and antecedents.
static <P> Formula<P>	Formula.horn(P consequent, P... antecedents)	Returns a Horn formula with the given consequent and antecedents.
static <P> Formula<P>	Formula.of(Clause<P>... clauses)	Returns a formula containing the given clauses.
static <P> Formula<P>	Formula.of(List<? extends Clause<P>> clauses)	Returns a formula containing the given clauses.
protected Formula<P>	SATSolver.State.sequential(SATSolver.State<P> s1, SATSolver.State<P> s2)	Finds a solution from either of two split states by sequential exploration.
Formula<P>	SATSolver.solve(Formula<P> form)	Solves a formula.
Formula<P>	SATSolver.State.solve()	Returns a solution for this state.
protected Formula<P>	SATSolver.State.split()	Finds a solution by splitting this state.
protected Formula<P>	SATSolver.State.split(SATSolver.State<P> s1, SATSolver.State<P> s2)	Finds a solution from either of two split states.
Formula<P>	Formula.with(Clause<P> first)	Returns a formula that prepends a clause to this formula.
Formula<P>	Formula.with(Literal<P> first)	Returns a formula that prepends a unit clause to this formula.

Methods in eu.bandm.tools.dpll with parameters of type Formula

Modifier and Type	Method	Description
Formula<P>	Formula.and(Formula<P> other)	Returns the conjunction of this and another formula.
Optional<Set<Literal<P>>>	SATSolver.findSolution(Formula<P> form)	Solves a formula.
protected SATSolver.State<P>	SATSolver.initialState(Formula<P> form)	Creates a new initial state for solving the given formula.
Formula<P>	SATSolver.solve(Formula<P> form)	Solves a formula.

Constructors in eu.bandm.tools.dpll with parameters of type Formula

Modifier	Constructor	Description
protected	State(Formula<P> form)	Creates a new state with the given formula and the empty solution candidate.
protected	State(Formula<P> form, Formula<P> solution)	Creates a new state with the given formula empty solution candidate.