formula

package
v0.4.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: May 11, 2024 License: MIT Imports: 9 Imported by: 2

Documentation

Overview

Package formula provides all the main data-structures for working with propositional formulas in LogicNG and generate them via a formula factory.

Usually the formula factory is the starting point of working with LogicNG. 

fac := formula.NewFactory()

From there on you can generate formulas on the factory or use a parser to parse them to the factory. All major algorithms which generate or manipulate formulas will need a formula factory as parameter. Usually within an application you only have one formula factory and keep working with it. Very seldom there should be the need to create more than one factory.

Formula factories are not thread-safe and you can not share formulas between formula factories since a formula in fact is only a unique ID (unit32) on the factory.

Index

Constants

View Source 
const (
	AuxCNF = "@RESERVED_CNF_"
	AuxCC  = "@RESERVED_CC_"
	AuxPBC = "@RESERVED_PBC_"
)

Variables

This section is empty.

Functions

func Comparator 

func Comparator(a, b interface{}) int

Comparator compares two formulas f1 and f2 with their integer value.

func DefaultFormulaGraphicalGenerator 

func DefaultFormulaGraphicalGenerator() *graphical.Generator[Formula]

DefaultFormulaGraphicalGenerator returns a graphical formula generator with sensible defaults.

func FormulaDepth added in v0.4.0 

func FormulaDepth(fac Factory, formula Formula) int

FormulaDepth returns the depth of the given formula. The depth of an atomic formula is defined as 0, all other operators increase the depth by 1.

func GenerateGraphicalFormulaAST added in v0.4.0 

func GenerateGraphicalFormulaAST(
	fac Factory,
	formula Formula,
	generator *graphical.Generator[Formula],
) *graphical.Representation

GenerateGraphicalFormulaAST generates a graphical representation of the formula with the configuration of the generator as an abstract syntax tree (AST). The resulting representation can then be exported as mermaid or graphviz graph.

func GenerateGraphicalFormulaDAG added in v0.4.0 

func GenerateGraphicalFormulaDAG(
	fac Factory,
	formula Formula,
	generator *graphical.Generator[Formula],
) *graphical.Representation

GenerateGraphicalFormulaDAG generates a graphical representation of the formula with the configuration of the generator as a graph (DAG). The resulting representation can then be exported as mermaid or graphviz graph.

func LiteralProfile added in v0.4.0 

func LiteralProfile(fac Factory, formula Formula) map[Literal]int

LiteralProfile returns the number of occurrences of each literal in the given formula.

func LookupFunctionCache 

func LookupFunctionCache(fac Factory, sort FunctionCacheSort, formula Formula) (any, bool)

LookupFunctionCache searches a cache entry for a given function sort and formula. It returns the optional result and a flag whether there was a cache entry.

func LookupPredicateCache 

func LookupPredicateCache(fac Factory, sort PredicateCacheSort, formula Formula) (bool, bool)

LookupPredicateCache searches a cache entry for a given predicate sort and formula. It returns the optional result and a flag whether there was a cache entry.

func NewTestData 

func NewTestData(fac Factory) testdata

func NumberOfAtoms added in v0.4.0 

func NumberOfAtoms(fac Factory, formula Formula) int

NumberOfAtoms returns the number of atomic formulas of the given formula. An atomic formula is a constant or a literal.

func NumberOfNodes added in v0.4.0 

func NumberOfNodes(fac Factory, formula Formula) int

NumberOfNodes returns the number of nodes (in the DAG) of the given formula.

func PropComparator added in v0.4.0 

func PropComparator(a, b Proposition) int

PropComparator compares two propositions p1 and p2.

func SetFunctionCache 

func SetFunctionCache(fac Factory, sort FunctionCacheSort, formula Formula, value any)

SetFunctionCache sets a cache entry for a given function sort, formula and value to cache.

func SetPredicateCache 

func SetPredicateCache(fac Factory, sort PredicateCacheSort, formula Formula, value bool)

SetPredicateCache sets a cache entry for a given predicate sort, formula and value to cache.

func SetTransformationCache 

func SetTransformationCache(fac Factory, sort TransformationCacheSort, formula, value Formula)

SetTransformationCache sets a cache entry for a given transformation sort, formula and value to cache.

func VariableProfile added in v0.4.0 

func VariableProfile(fac Factory, formula Formula) map[Variable]int

VariableProfile returns the number of occurrences of each variable in the given formula.

Types

type AbortableTransformation added in v0.4.0 

type AbortableTransformation func(Factory, Formula, handler.Handler) (Formula, bool)

An AbortableTransformation is a function which maps a formula to another formula. It takes an handler which can be used to abort the computation. If the computation is aborted by the handler, the ok flag in the response is false.

type AuxVarSort added in v0.3.0 

type AuxVarSort string

AuxVarSort encodes the auxiliary variable sort.

type CSort 

type CSort byte

CSort encodes the sort of an integer comparator 

const (
	EQ CSort = iota // equal
	LE              // less or equal
	LT              // less than
	GE              // greater or equal
	GT              // greater than
)

func (CSort) Evaluate 

func (c CSort) Evaluate(lhs, rhs int) bool

Evaluate evaluates an integer comparison given its left- and right-hand side.

func (CSort) String 

func (i CSort) String() string

type CachingFactory 

type CachingFactory struct {
	// contains filtered or unexported fields
}

A CachingFactory is the default (and currently only) implementation of the formula factory in LogicNG.

In this implementation, the container function is 'smart': A formula factory guarantees that syntactically equivalent formulas are created only once. This mechanism also extends to variants of the formula in terms of associativity and commutativity. Therefore, if the user creates formulas for 

A & B
B & A
(B & A)

all of them are represented by only one formula in memory. This approach is only possible, because formulas in LogicNG are immutable data structures. So once created, a formula can never be altered again.

func (*CachingFactory) AMO 

func (fac *CachingFactory) AMO(variables ...Variable) Formula

AMO returns an at-most-one (<= 1) constraint over the given variables.

func (*CachingFactory) And 

func (fac *CachingFactory) And(operands ...Formula) Formula

And returns a conjunction of the given operands. If the result is an And formula, it is guaranteed to have at least two operands. An empty conjunction is treated as true, a conjunction with one operand, is treated as this operand.

func (*CachingFactory) BinaryLeftRight 

func (fac *CachingFactory) BinaryLeftRight(formula Formula) (left, right Formula, ok bool)

BinaryLeftRight returns the left and right operand of a given formula interpreted as a binary operator. The ok flag indicates whether the binary operator was found on the factory or not.

func (*CachingFactory) BinaryOperator 

func (fac *CachingFactory) BinaryOperator(sort FSort, left, right Formula) (Formula, error)

BinaryOperator returns a new binary operator with the given sort and the two operands left and right. Returns an error if the given sort is not a binary operator (implication or equivalence).

func (*CachingFactory) CC 

func (fac *CachingFactory) CC(comparator CSort, rhs uint32, variables ...Variable) Formula

CC returns a new cardinality constraint with the given comparator and right-hand-side representing a constraint v_1 + ... + v_n C rhs with C in [<, >, <=, >=, =].

func (*CachingFactory) Clause 

func (fac *CachingFactory) Clause(operands ...Literal) Formula

Clause returns a disjunction between the given literals. In contrast to the [Or] Method, the operands are not condensed. Meaning, if the operands contain duplicate literals, the result will also contain these duplicates and therefore lead to potential problems down the road.

func (*CachingFactory) ConfigurationFor 

func (fac *CachingFactory) ConfigurationFor(
	sort configuration.Sort,
) (config configuration.Config, ok bool)

ConfigurationFor returns the configuration for a given configuration sort. The ok flag indicates whether a config for the given sort was found in the factory.

func (*CachingFactory) Constant 

func (fac *CachingFactory) Constant(value bool) Formula

Constant returns the Boolean constant represented by the given value.

func (*CachingFactory) EXO 

func (fac *CachingFactory) EXO(variables ...Variable) Formula

EXO returns an exactly-one (= 1) constraint over the given variables.

func (*CachingFactory) Equivalence 

func (fac *CachingFactory) Equivalence(left, right Formula) Formula

Equivalence returns an equivalence left <=> right.

func (*CachingFactory) Falsum 

func (fac *CachingFactory) Falsum() Formula

Falsum returns the Boolean false constant.

func (*CachingFactory) Implication 

func (fac *CachingFactory) Implication(left, right Formula) Formula

Implication returns an implication left => right.

func (*CachingFactory) Lit 

func (fac *CachingFactory) Lit(name string, phase bool) Literal

Lit returns a Boolean literal with the given name and phase. For a name "A" the positive phase returns the variable "A" whereas the negative phase returns the negated variable "~A". In contrast to the Literal function, a literal type is returned.

func (*CachingFactory) LitNamePhase 

func (fac *CachingFactory) LitNamePhase(literal Literal) (name string, phase, ok bool)

LitNamePhase returns the name and phase of the given literal. The ok flag indicates whether the literal was found on the factory or not.

func (*CachingFactory) Literal 

func (fac *CachingFactory) Literal(name string, phase bool) Formula

Literal returns a Boolean literal with the given name and phase. For a name "A" the positive phase returns the variable "A" whereas the negative phase returns the negated variable "~A".

func (*CachingFactory) LiteralNamePhase 

func (fac *CachingFactory) LiteralNamePhase(formula Formula) (name string, phase, ok bool)

LiteralNamePhase returns the name and phase of a given formula interpreted as literal. The ok flag is false when the given formula was not a literal, or it was not found on the factory.

func (*CachingFactory) Minterm 

func (fac *CachingFactory) Minterm(operands ...Literal) Formula

Minterm returns a conjunction between the given literals. In contrast to the [And] Method, the operands are not condensed. Meaning, if the operands contain duplicate literals, the result will also contain these duplicates and therefore lead to potential problems down the road.

func (*CachingFactory) NaryOperands 

func (fac *CachingFactory) NaryOperands(formula Formula) (ops []Formula, ok bool)

NaryOperands returns the operands of a given formula interpreted as an n-ary operator. The ok flag indicates whether the n-ary operator was found on the factory or not.

func (*CachingFactory) NaryOperator 

func (fac *CachingFactory) NaryOperator(sort FSort, operands ...Formula) (Formula, error)

NaryOperator returns a new n-ary operator with the given sort and the list of operands. Returns an error if the given sort is not a binary operator (conjunction or disjunction).

func (*CachingFactory) NewAuxVar added in v0.3.0 

func (fac *CachingFactory) NewAuxVar(sort AuxVarSort) Variable

NewAuxVariable generates and returns a new auxiliary variable of the given sort.

func (*CachingFactory) Not 

func (fac *CachingFactory) Not(operand Formula) Formula

Not returns the negation of the given formula. Constants, literals and negations are negated directly and returned. For all other formulas a new Not formula is returned.

func (*CachingFactory) NotOperand 

func (fac *CachingFactory) NotOperand(formula Formula) (op Formula, ok bool)

NotOperand returns the operand of a given formula interpreted as negation. The ok flag indicates whether the negation was found on the factory or not.

func (*CachingFactory) Operands 

func (fac *CachingFactory) Operands(formula Formula) []Formula

Operands returns the operands of a given formula. For a negation this is its operand, for an implication and equivalence its left and right operand (in this order), for n-ary operators their operands. All other formulas have no operands.

func (*CachingFactory) Or 

func (fac *CachingFactory) Or(operands ...Formula) Formula

Or returns a disjunction of the given operands. If the result is an Or formula, it is guaranteed to have at least two operands. An empty disjunction is treated as false, a disjunction with one operand, is treated as this operand.

func (*CachingFactory) PBC 

func (fac *CachingFactory) PBC(comparator CSort, rhs int, literals []Literal, coefficients []int) Formula

PBC returns a pseudo-Boolean constraint with the given comparator and right-hand-side. The single operands are represented by multiplications x_i * l_i with x_i from the coefficients and l_i from the literals. The constraint represented is therefore x_1 * l_1 + ... + x_n * x_n C rhs with C in [<, >, <=, >=, =].

func (*CachingFactory) PBCOps 

func (fac *CachingFactory) PBCOps(
	formula Formula,
) (comparator CSort, rhs int, literals []Literal, coefficients []int, found bool)

PBCOps returns the comparator, right-hand-side, literals, and coefficients of a given formula interpreted as a pseudo-Boolean constraint. The ok flag indicates whether the constraint was found on the factory or not.

func (*CachingFactory) PutConfiguration 

func (fac *CachingFactory) PutConfiguration(config configuration.Config) error

PutConfiguration adds a configuration to the factory.

func (*CachingFactory) SetPrintSymbols 

func (fac *CachingFactory) SetPrintSymbols(symbols *PrintSymbols)

SetPrintSymbols sets the symbols for printing formulas with Sprint.

func (*CachingFactory) Statistics 

func (fac *CachingFactory) Statistics() string

Statistics returns a statistic of the factory as a multi-line string.

func (*CachingFactory) Symbols 

func (fac *CachingFactory) Symbols() *PrintSymbols

Symbols returns the print symbols for the factory. These symbols are used when calling Sprint on a formula.

func (*CachingFactory) Var 

func (fac *CachingFactory) Var(name string) Variable

Var returns a Boolean variable with the given name. In contrast to the Variable method, a variable type is returned.

func (*CachingFactory) VarName 

func (fac *CachingFactory) VarName(variable Variable) (name string, ok bool)

VarName returns the name of the given variable. The ok flag indicates whether the variable was found on the factory or not.

func (*CachingFactory) Variable 

func (fac *CachingFactory) Variable(name string) Formula

Variable returns a Boolean variable with the given name as a Formula.

func (*CachingFactory) Vars 

func (fac *CachingFactory) Vars(name ...string) []Variable

Vars returns a list of Boolean variable with the given names.

func (*CachingFactory) Verum 

func (fac *CachingFactory) Verum() Formula

Verum returns the Boolean true constant.

type ExtendedProposition 

type ExtendedProposition[T fmt.Stringer] struct {
	Backpack T
	// contains filtered or unexported fields
}

An ExtendedProposition is a proposition implementation with a formula and a user provided generic backpack.

func NewExtendedProposition 

func NewExtendedProposition[T fmt.Stringer](formula Formula, backpack T) *ExtendedProposition[T]

NewExtendedProposition returns a new extended proposition with the formula and the given backpack.

func (*ExtendedProposition[T]) Formula 

func (p *ExtendedProposition[T]) Formula() Formula

Formula returns the formula of the proposition.

func (*ExtendedProposition[T]) Sprint 

func (p *ExtendedProposition[T]) Sprint(fac Factory) string

Sprint takes a formula factory and pretty-prints the proposition.

func (*ExtendedProposition[T]) String 

func (p *ExtendedProposition[T]) String() string

type FSort 

type FSort uint32

FSort encodes the different formula sorts. 

const (
	SortFalse   FSort = iota // constant false
	SortTrue                 // constant true
	SortLiteral              // literal (variable + phase)
	SortNot                  // negation
	SortAnd                  // conjunction
	SortOr                   // disjunction
	SortImpl                 // implication
	SortEquiv                // equivalence
	SortCC                   // cardinality constraint
	SortPBC                  // pseudo-Boolean constraint
)

func DualSort 

func DualSort(fsort FSort) (FSort, error)

DualSort returns the dual sort for AND and OR. For all other formula types it returns an error.

func (FSort) String 

func (i FSort) String() string

type Factory 

type Factory interface {
	Verum() Formula
	Falsum() Formula
	Constant(value bool) Formula
	Var(name string) Variable
	Variable(name string) Formula
	Vars(name ...string) []Variable
	Lit(name string, phase bool) Literal
	Literal(name string, phase bool) Formula
	Not(operand Formula) Formula
	BinaryOperator(sort FSort, left, right Formula) (Formula, error)
	Implication(left, right Formula) Formula
	Equivalence(left Formula, right Formula) Formula
	NaryOperator(sort FSort, operands ...Formula) (Formula, error)
	And(operands ...Formula) Formula
	Minterm(operands ...Literal) Formula
	Or(operands ...Formula) Formula
	Clause(operands ...Literal) Formula
	CC(comparator CSort, rhs uint32, variables ...Variable) Formula
	AMO(variables ...Variable) Formula
	EXO(variables ...Variable) Formula
	PBC(comparator CSort, rhs int, literals []Literal, coefficients []int) Formula

	VarName(variable Variable) (name string, found bool)
	LitNamePhase(literal Literal) (name string, phase, found bool)
	LiteralNamePhase(formula Formula) (name string, phase, found bool)
	NotOperand(formula Formula) (op Formula, found bool)
	BinaryLeftRight(formula Formula) (left, right Formula, found bool)
	NaryOperands(formula Formula) (ops []Formula, found bool)
	PBCOps(formula Formula) (comparator CSort, rhs int, literals []Literal, coefficients []int, found bool)
	Operands(formula Formula) []Formula

	NewAuxVar(sort AuxVarSort) Variable

	ConfigurationFor(sort configuration.Sort) (configuration.Config, bool)
	PutConfiguration(configuration configuration.Config) error
	Symbols() *PrintSymbols
	SetPrintSymbols(symbols *PrintSymbols)

	Statistics() string
	// contains filtered or unexported methods
}

A Factory is the central concept of LogicNG and is always required when working with the library. A formula factory is an object consisting of two major components:

  1. a factory, which creates formulas
  2. a container, which stores created formulas.

Formula factories are not thread safe!

func NewFactory 

func NewFactory(conserveVars ...bool) Factory

NewFactory returns a new caching formula factory. If the optional conserveVars flag is set to true, trivial contradictions and tautologies are not simplified in formulas. E. g. a formula like A & ~A, A | ~A, or A => A can be generated on the formula factory. Therefore it is guaranteed that all variables of the original formula are still present on the formula factory. If set to false, the formulas will be simplified to false or true and therefore variables of the original formula can not be present on the formula factory. The default behaviour is that the flag is set to false.

type Formula 

type Formula uint32

Formula represents a Boolean (or pseudo-Boolean) formula in LogicNG. The datatype itself is just an alias to an uint32. The first four bits encode the formula sort whereas the remaining 28 bit are a unique identifier for the formula on the factory. Therefore, a formula is only valid and useful in the context of the factory which was used to generate it.

func EncodeFormula 

func EncodeFormula(fsort FSort, id uint32) Formula

EncodeFormula takes a formula sort and a unique ID an returns its encoding.

func LiteralsAsFormulas 

func LiteralsAsFormulas(literals []Literal) []Formula

LiteralsAsFormulas returns a list of literals as a list of formulas.

func LookupTransformationCache 

func LookupTransformationCache(fac Factory, sort TransformationCacheSort, formula Formula) (Formula, bool)

LookupTransformationCache searches a cache entry for a given transformation sort and formula. It returns the optional result and a flag whether there was a cache entry.

func NewCornerCases 

func NewCornerCases(fac Factory) []Formula

func SubNodes added in v0.4.0 

func SubNodes(fac Factory, formula Formula) []Formula

SubNodes returns all sub-nodes of the given formula. The order of the sub-nodes is bottom-up, i.e. a sub-node only appears in the result when all of its sub-nodes are already listed.

func VariablesAsFormulas 

func VariablesAsFormulas(variables []Variable) []Formula

VariablesAsFormulas returns a list of variables as a list of formulas.

func (Formula) AsLiteral 

func (f Formula) AsLiteral() (Literal, error)

AsLiteral returns the current formula as a literal type or returns an error if the formula is not a literal.

func (Formula) AsVariable 

func (f Formula) AsVariable() (Variable, error)

AsVariable returns the current formula as a variable type or returns an error if the formula is not a variable.

func (Formula) ID 

func (f Formula) ID() uint32

ID returns the extracted ID of a formula.

func (Formula) IsAtomic 

func (f Formula) IsAtomic() bool

IsAtomic reports whether the formula is an atomic formula, i.e. a constant, a literal, or a pseudo-Boolean constraint including cardinality constraints.

func (Formula) IsConstant 

func (f Formula) IsConstant() bool

IsConstant reports whether the formula is a constant.

func (Formula) IsNeg 

func (f Formula) IsNeg() bool

IsNeg reports whether the formula is negative, i.e. the false constant, a negative literal, or a negation.

func (Formula) IsPos 

func (f Formula) IsPos() bool

IsPos reports whether the formula is positive, i.e. the true constant, a positive literal, or any formula which is not a negation.

func (Formula) Negate 

func (f Formula) Negate(fac Factory) Formula

Negate returns the negation of the formula.

func (Formula) Sort 

func (f Formula) Sort() FSort

Sort returns the extracted sort of a formula.

func (Formula) Sprint 

func (f Formula) Sprint(fac Factory) string

Sprint prints a formula in human-readable form. In order to this, the generating formula factor must be passed as a parameter.

This method panics if the formula cannot be found on the factory.

func (Formula) String 

func (f Formula) String() string

String returns a simple string representation of a formula. Since the default string method does not know the constructing factory, only the formula sort and ID can be printed. If you want a human-readable string output, use the Sprint function which takes the factory as parameter.

type FormulaSet 

type FormulaSet = fset[Formula] // Immutable set of formulas

func NewFormulaSet 

func NewFormulaSet(formula ...Formula) *FormulaSet

NewFormulaSet generates a new formula set with the given formulas as content.

type Function added in v0.4.0 

type Function[T any] func(Factory, Formula) T

A Function is a function which maps a formula to an arbitrary value.

type FunctionCacheSort 

type FunctionCacheSort byte

FunctionCacheSort encodes a formula function sort for which the result can be cached. 

const (
	FuncVariables FunctionCacheSort = iota
	FuncLiterals
	FuncDepth
	FuncSubnodes
	FuncNumberOfAtoms
	FuncNumberOfNodes
	FuncDNNFModelCount
)

func (FunctionCacheSort) String 

func (i FunctionCacheSort) String() string

type LitSet 

type LitSet = fset[Literal] // Immutable set of literals

func Literals 

func Literals(fac Factory, formula ...Formula) *LitSet

Literals returns all literals of the given formula as a literal set.

func NewLitSet 

func NewLitSet(literal ...Literal) *LitSet

NewLitSet generates a new literal set with the given literal as content.

type Literal 

type Literal uint32

Literal represents a Boolean literal in LogicNG. This is just a type alias for the uint32 wrapped by the Formula type. But for type-safety reasons it is often desirable to explicitly know that something is a literal. You can convert between literal and formula with the AsFormula and AsLiteral methods.

func EncodeLiteral 

func EncodeLiteral(id uint32) Literal

EncodeLiteral takes a unique ID an returns its encoding as a literal.

func VariablesAsLiterals 

func VariablesAsLiterals(variables []Variable) []Literal

VariablesAsLiterals returns a list of variables as a list of literals.

func (Literal) AsFormula 

func (l Literal) AsFormula() Formula

AsFormula returns the literal as a formula type.

func (Literal) ID 

func (l Literal) ID() uint32

ID returns the extracted ID of the literal.

func (Literal) IsNeg 

func (l Literal) IsNeg() bool

IsNeg reports whether the literal is negative.

func (Literal) IsPos 

func (l Literal) IsPos() bool

IsPos reports whether the literal is positive.

func (Literal) Negate 

func (l Literal) Negate(fac Factory) Literal

Negate returns the negation of the literal.

func (Literal) Sprint 

func (l Literal) Sprint(fac Factory) string

Sprint prints a literal in human-readable form. In order to this, the generating formula factor must be passed as a parameter.

This method panics if the literal cannot be found on the factory.

func (Literal) Variable 

func (l Literal) Variable() Variable

Variable extracts the variable from a literal.

type MutableFormulaSet added in v0.3.0 

type MutableFormulaSet = mutableFset[Formula] // Mutable set of formulas

func NewMutableFormulaSet added in v0.3.0 

func NewMutableFormulaSet(formula ...Formula) *MutableFormulaSet

NewMutableFormulaSet generates a new mutable formula set with the given formulas as content.

type MutableLitSet added in v0.3.0 

type MutableLitSet = mutableFset[Literal] // Mutable set of literals

func NewMutableLitSet added in v0.3.0 

func NewMutableLitSet(literal ...Literal) *MutableLitSet

NewMutableLitSet generates a new mutable literal set with the given literal as content.

type MutableVarSet added in v0.3.0 

type MutableVarSet = mutableFset[Variable] // Mutable set of variables

func NewMutableVarSet added in v0.3.0 

func NewMutableVarSet(variable ...Variable) *MutableVarSet

NewMutableVarSet generates a new mutable variable set with the given variables as content.

func NewMutableVarSetCopy added in v0.3.0 

func NewMutableVarSetCopy(variableSet ...*VarSet) *MutableVarSet

NewMutableVarSetCopy returns a new mutable variable set with the content of all the given variable sets as content.

type Predicate added in v0.4.0 

type Predicate func(Factory, Formula) bool

A Predicate is a function which maps a formula to a boolean value.

type PredicateCacheSort 

type PredicateCacheSort byte

PredicateCacheSort encodes a formula predicate sort for which the result can be cached. 

const (
	PredNNF PredicateCacheSort = iota
	PredCNF
	PredDNF
	PredAIG
)

func (PredicateCacheSort) String 

func (i PredicateCacheSort) String() string

type PrintSymbols 

type PrintSymbols struct {
	Verum          string // default: $true
	Falsum         string // default: $false
	Not            string // default: ~
	Implication    string // default: =>
	Equivalence    string // default: <=>
	And            string // default: &
	Or             string // default: |
	LeftBracket    string // default: (
	RightBracket   string // default: )
	Plus           string // default: +
	Minus          string // default: -
	Multiplication string // default: *
	Equal          string // default: =
	Less           string // default: <
	LessOrEqual    string // default: <=
	Greater        string // default: >
	GreaterOrEqual string // default: >=
}

PrintSymbols gathers all symbols for Boolean and pseudo-Boolean formulas for printing formulas. You can use the DefaultSymbols method to use exactly these symbols which can be parsed again be the default parser, or you can define your own symbols.

func DefaultSymbols 

func DefaultSymbols() *PrintSymbols

DefaultSymbols returns the standard symbols for printing formulas.

type Proposition 

type Proposition interface {
	Formula() Formula
	String() string
	Sprint(fac Factory) string
}

A Proposition is a formula with additional information like a textual description or a user-provided object.

type StandardProposition 

type StandardProposition struct {
	Description string
	// contains filtered or unexported fields
}

A StandardProposition is a simple proposition implementation with a formula and a textual description.

func NewStandardProposition 

func NewStandardProposition(formula Formula, description ...string) *StandardProposition

NewStandardProposition returns a new standard proposition with the formula and an optional textual description.

func (*StandardProposition) Formula 

func (p *StandardProposition) Formula() Formula

Formula returns the formula of the proposition.

func (*StandardProposition) Sprint 

func (p *StandardProposition) Sprint(fac Factory) string

Sprint takes a formula factory and pretty-prints the proposition.

func (*StandardProposition) String 

func (p *StandardProposition) String() string

type Transformation added in v0.4.0 

type Transformation func(Factory, Formula) Formula

A Transformation is a function which maps a formula to another formula

type TransformationCacheSort 

type TransformationCacheSort byte

TransformationCacheSort encodes a formula transformation sort for which the result can be cached. 

const (
	TransNNF TransformationCacheSort = iota
	TransCNFFactorization
	TransDNFFactorization
	TransAIG
	TransDistrSimpl
	TransUnitPropagation
	TransBDDCNF
	TransBDDNF
)

func (TransformationCacheSort) String 

func (i TransformationCacheSort) String() string

type Tristate 

type Tristate byte

Tristate represents a Boolean value with the possibility of a third UNDEF value. 

const (
	TristateTrue Tristate = iota
	TristateFalse
	TristateUndef
)

func TristateFromBool 

func TristateFromBool(b bool) Tristate

TristateFromBool returns the tristate for the given Boolean value.

func (Tristate) Negate 

func (t Tristate) Negate() Tristate

Negate returns the negation of the tristate TRUE turns FALSE, FALSE turns TRUE, and UNDEF stays UNDEF.

func (Tristate) String 

func (i Tristate) String() string

type VarSet 

type VarSet = fset[Variable] // Immutable set of variables

func NewVarSet 

func NewVarSet(variable ...Variable) *VarSet

NewVarSet generates a new variable set with the given variables as content.

func NewVarSetCopy added in v0.3.0 

func NewVarSetCopy(variableSet ...*VarSet) *VarSet

NewVarSetCopy returns a new variable set with the content of all the given variable sets as content.

func Variables 

func Variables(fac Factory, formula ...Formula) *VarSet

Variables returns all variables of the given formula as a variable set.

type Variable 

type Variable uint32

Variable represents a Boolean variable in LogicNG. This is just a type alias for the uint32 wrapped by the Formula type. But for type-safety reasons it is often desirable to explicitly know that something is a variable. You can convert between variable and formula with the AsFormula and AsVariable methods.

func EncodeVariable 

func EncodeVariable(id uint32) Variable

EncodeVariable takes a unique ID an returns its encoding as a variable.

func LiteralsAsVariables 

func LiteralsAsVariables(literals []Literal) ([]Variable, error)

LiteralsAsVariables returns a list of literals as a list of variables or returns an error if there is a negative literal in the list.

func (Variable) AsFormula 

func (v Variable) AsFormula() Formula

AsFormula returns the variable as a formula type.

func (Variable) AsLiteral 

func (v Variable) AsLiteral() Literal

AsLiteral returns the variable as a literal type.

func (Variable) ID 

func (v Variable) ID() uint32

ID returns the extracted ID of the variable.

func (Variable) Negate 

func (v Variable) Negate(fac Factory) Literal

Negate returns the negation of the variable.

func (Variable) Sprint 

func (v Variable) Sprint(fac Factory) string

Sprint prints a variable in human-readable form. In order to this, the generating formula factor must be passed as a parameter.

This method panics if the variable cannot be found on the factory.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.