Documentation
¶
Overview ¶
Package enum provides algorithms to perform model enumeration on formulas in LogicNG.
An enumeration can be performed on a formula:
assert := assert.New(t)
fac := f.NewFactory()
p := parser.New(fac)
formula := p.ParseUnsafe("A & (B | C)")
models := enum.OnFormula(fac, formula, fac.Vars("A", "B", "C")) // will produce 3 models
or directly on a SAT solver
solver := sat.NewMiniSatSolver(fac)
models = enum.OnSolver(solver, fac.Vars("A", "B", "C")) // will produce 3 models
Model enumeration is one use case of the model iteration in the iter package and can be configured as described there.
Index ¶
- func CanonicalCNF(fac f.Factory, formula f.Formula) f.Formula
- func CanonicalCNFWithHandler(fac f.Factory, formula f.Formula, iterHandler iter.Handler) (cnf f.Formula, ok bool)
- func CanonicalDNF(fac f.Factory, formula f.Formula) f.Formula
- func CanonicalDNFWithHandler(fac f.Factory, formula f.Formula, iterHandler iter.Handler) (cnf f.Formula, ok bool)
- func OnFormula(fac f.Factory, formula f.Formula, variables []f.Variable, ...) []*model.Model
- func OnFormulaWithConfig(fac f.Factory, formula f.Formula, variables []f.Variable, config *iter.Config, ...) ([]*model.Model, bool)
- func OnSolver(solver *sat.Solver, variables []f.Variable, additionalVariables ...f.Variable) []*model.Model
- func OnSolverWithConfig(solver *sat.Solver, variables []f.Variable, config *iter.Config, ...) ([]*model.Model, bool)
- func ToBDDOnFormula(fac f.Factory, formula f.Formula, variables []f.Variable) *bdd.BDD
- func ToBDDOnFormulaWithConfig(fac f.Factory, formula f.Formula, variables []f.Variable, config *iter.Config) (*bdd.BDD, bool)
- func ToBDDOnSolver(solver *sat.Solver, variables []f.Variable) *bdd.BDD
- func ToBDDOnSolverWithConfig(solver *sat.Solver, variables []f.Variable, config *iter.Config) (*bdd.BDD, bool)
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func CanonicalCNF ¶
CanonicalCNF returns a canonical CNF of the given formula.
func CanonicalCNFWithHandler ¶ added in v0.4.0
func CanonicalCNFWithHandler(fac f.Factory, formula f.Formula, iterHandler iter.Handler) (cnf f.Formula, ok bool)
CanonicalCNF returns a canonical CNF of the given formula. The given iterHandler can be used to abort the computation. If the enumeration was aborted, the ok flag is false.
func CanonicalDNF ¶
CanonicalDNF returns a canonical DNF of the given formula.
func CanonicalDNFWithHandler ¶ added in v0.4.0
func CanonicalDNFWithHandler(fac f.Factory, formula f.Formula, iterHandler iter.Handler) (cnf f.Formula, ok bool)
CanonicalDNF returns a canonical DNF of the given formula. The given iterHandler can be used to abort the computation. If the enumeration was aborted, the ok flag is false.
func OnFormula ¶
func OnFormula( fac f.Factory, formula f.Formula, variables []f.Variable, additionalVariables ...f.Variable, ) []*model.Model
OnFormula enumerates all models of a formula over the given variables. The additionalVariables will be included in each model, but are not iterated over.
func OnFormulaWithConfig ¶
func OnFormulaWithConfig( fac f.Factory, formula f.Formula, variables []f.Variable, config *iter.Config, additionalVariables ...f.Variable, ) ([]*model.Model, bool)
OnFormulaWithConfig enumerates all models of a formula over the given variables. The additionalVariables will be included in each model, but are not iterated over. The config can be used to influence the model iteration process by setting a handler and/or an iteration strategy.
func OnSolver ¶
func OnSolver(solver *sat.Solver, variables []f.Variable, additionalVariables ...f.Variable) []*model.Model
OnSolver enumerates all models on the given SAT solver over the given variables. The additionalVariables will be included in each model, but are not iterated over.
func OnSolverWithConfig ¶
func OnSolverWithConfig( solver *sat.Solver, variables []f.Variable, config *iter.Config, additionalVariables ...f.Variable, ) ([]*model.Model, bool)
OnSolverWithConfig enumerates all models on the given SAT solver over the given variables. The additionalVariables will be included in each model, but are not iterated over. The config can be used to influence the model iteration process by setting a handler and/or an iteration strategy.
func ToBDDOnFormula ¶
ToBDDOnFormula enumerates all models of a formula over the given variables and tathers the result in a BDD.
func ToBDDOnFormulaWithConfig ¶
func ToBDDOnFormulaWithConfig( fac f.Factory, formula f.Formula, variables []f.Variable, config *iter.Config, ) (*bdd.BDD, bool)
ToBDDOnFormulaWithConfig enumerates all models of a formula over the given variables and gathers the result in a BDD. The config can be used to influence the model iteration process by setting a handler and/or an iteration strategy.
func ToBDDOnSolver ¶
ToBDDOnSolver enumerates all models on the given SAT solver over the given variables and gathers the result in a BDD.
func ToBDDOnSolverWithConfig ¶
func ToBDDOnSolverWithConfig( solver *sat.Solver, variables []f.Variable, config *iter.Config, ) (*bdd.BDD, bool)
ToBDDOnSolverWithConfig enumerates all models on the given SAT solver over the given variables and gathers the result in a BDD. The config can be used to influence the model iteration process by setting a handler and/or an iteration strategy.
Types ¶
This section is empty.
Source Files