Crate sat_toasty_helper

Structs

AtMostOne

ConditionalClauseBuilder

a ConditionalClauseBuilder struct has a reference to another ClauseBuilder; it will implicitly add the given constraint as a hypothesis to any clauses added.

Defined

PropMap

Solver

A Solver is used to build and (and later solve) SAT constraints.

Var

A Var is an opaque identifier used for variables.

Enums

Lit

VarOrProp

VarOrProp is just a convenient type to mix your Prop types with Vars that you’ve already converted.

Traits

ClauseBuilder

A ClauseBuilder allows clauses to be added.

ClauseBuilderHelper

This trait defines all of the helper functions used to build complex clauses. This methods are defined here instead of on ClauseBuilder directly so that ClauseBuilder remains object-safe.

DefinedProp

A DefinedProp is a prop that comes along with a definition, which is just a set of clauses that are added as soon as it’s mentioned.

InternalProp

A Prop represents a variable that can be assigned a value in a SAT constraint.

Prop

Implement this trait for your types to allow them as propositions in your SAT constraints.