Documentation
¶
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type UnsatCore ¶
type UnsatCore struct {
Propositions []f.Proposition // propositions of the unsat core
IsGuaranteedMUS bool // flag whether the core is guaranteed to be a MUS
}
UnsatCore represents an unsatisfiable core of a formula. If the core is guaranteed to be a MUS, the flag IsGuaranteedMus is set to true. If it is set to false, the core could be a MUS, but for efficiency reasons this is not computed.
func NewUnsatCore ¶
func NewUnsatCore(propositions []f.Proposition, isMus bool) *UnsatCore
NewUnsatCore creates a new UnsatCore with the given propositions and the given flag whether the core is guaranteed to be a MUS.
Source Files
Directories
¶
| Path | Synopsis |
|---|---|
|
Package mus provides data structures and algorithms for minimal unsatisfiable sets (MUS) in LogicNG.
|
Package mus provides data structures and algorithms for minimal unsatisfiable sets (MUS) in LogicNG. |
|
Package smus provides an algorithm to compute a smallest minimal unsatisfiable set (SMUS) of a set of propositions or formulas in LogicNG.
|
Package smus provides an algorithm to compute a smallest minimal unsatisfiable set (SMUS) of a set of propositions or formulas in LogicNG. |
Click to show internal directories.
Click to hide internal directories.