LGLMBS.Add(lit as Integer)

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Adds a value.

LGLMBS.Assume(lit as Integer)

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Assume single units.

LGLMBS.CAssume(lit as Integer)

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Assume clause (at most one)

LGLMBS.Clone as LGLMBS

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Clones the object.

Both 'Cloning' and 'Forking' can be used to implement 'Push & Pop', but the asymmetric forking is more similar to the classical way of implementing it, needs less resources since for instance eliminated variables do not occupy any memory in the children, but requires lifting back satisfying assignments explicitly (through the whole parent chain). If these full satisfying assignments are really needed actually cloning could be more space efficient too. Assume you want to split the solver into two instances, one with a literal set to false, the other one to true. Then cloning allows you to produce two independent branches, while for forking you need three, since the root / top solver still has to be kept for lifting back a potential assignment.

LGLMBS.Constructor

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

The constructor.

Creates new empty object.

LGLMBS.DefaultOption(Name as String) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Queries default value for an option.

LGLMBS.Deref(lit as Integer) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Queries value.

neg=false, pos=true
Returns -1 if lit is bigger then MaxVar.

LGLMBS.Failed(lit as Integer) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Checks failed flag for given item.

neg=false, pos=true
for assumptions.

LGLMBS.Fixate

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Add assumptions as units

LGLMBS.Fixed(lit as Integer) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Checks fixed flag.

neg=false, pos=true
Toplevel

LGLMBS.FlushCache

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Flush all learned clauses.

LGLMBS.FlushTimers

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Flush timers.

LGLMBS.Fork as LGLMBS

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Forks the object.

'Forking' copies only irredundant clauses and also uses internal variable indices of the parent as external variable indices. Thus 'parent' and the forked off 'child' do neither exactly work the same way, nor do they use from the API point of view the same set of variables. They are satisfiability equivalent. If the child becomes unsatisfiable the parent can be assumed to be unsatisfiable too and thus 'join' would just add the empty clause to the parent. If the child produces a satisfying assignment, this assignment is turned into an assignment of the parent by 'join'. Parents can be forked multiple times. A child has exactly one parent. Parents and children can be released independently. Between 'Fork' and 'Join' no other operations but further 'Fork' are allowed. The effect ot multiple 'Join' with the same parent is unclear at this point. The same memory manager is use for the child and the parent. Options, prefix, output file and the callbacks for 'getime' and 'Abort' are copied too (if set).

Both 'Cloning' and 'Forking' can be used to implement 'Push & Pop', but the asymmetric forking is more similar to the classical way of implementing it, needs less resources since for instance eliminated variables do not occupy any memory in the children, but requires lifting back satisfying assignments explicitly (through the whole parent chain). If these full satisfying assignments are really needed actually cloning could be more space efficient too. Assume you want to split the solver into two instances, one with a literal set to false, the other one to true. Then cloning allows you to produce two independent branches, while for forking you need three, since the root / top solver still has to be kept for lifting back a potential assignment.

LGLMBS.Freeze(lit as Integer)

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Freezes the given item.

LGLMBS.Frozen(lit as Integer) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Queries frozen state.

LGLMBS.GetOptionMinMax(Name as String, byref min as Integer, byref max as Integer) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Queries current value, minimum and maximum values.

LGLMBS.HasOption(Name as String) as Boolean

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Checks if the given option is set.

LGLMBS.IncVar as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Increases variables by one.

LGLMBS.Join(Child as LGLMBS) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Joins back forked child.

LGLMBS.Lookahead as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Returns a good look ahead literal or zero if all potential literals have been eliminated or have been used as blocking literals in blocked clause elimination.

Zero is also returned if the formula is already inconsistent. The lookahead literal is made usable again, for instance if it was not frozen during a previous SAT call and thus implicitly became melted. Therefore it can be added in a unit clause.

LGLMBS.Melt(lit as Integer)

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Melts a literal.

LGLMBS.MeltAll

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Melt all literals.

LGLMBS.Option(Name as String) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
property	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Queries or sets option value.

(Read and Write computed property)

LGLMBS.ReadOptionFile(File as FolderItem) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Reads the option file.

LGLMBS.Reconstk(byref Start as Ptr, byref Top as Ptr)

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Set Start and Top to the 'start' and 'top' of the reconstruction stack, which is used in BCE, BVE and CCE for reconstructing a solution after eliminating variables or clauses.

These pointers are only valid until the next Sat or Simp call.

LGLMBS.ReduceCache

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Reset cache size.

LGLMBS.Representative(lit as Integer) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Return representative from equivalence class if literal is not top-level assigned nor eliminated.

LGLMBS.ResetPhase(lit as integer)

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Set default phase of a literal.

Stop forcing phase in decisions.

LGLMBS.Reusable(lit as Integer) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Checks if item can be reused.

If a literal was not frozen at the last call to Sat (or Simp) it becomes 'unusable' after the next call even though it might not have been used as blocking literal etc.

LGLMBS.Reuse(lit as Integer)

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Reuses an item.

If a literal was not frozen at the last call to Sat (or Simp) it becomes 'unusable' after the next call even though it might not have been used as blocking literal etc.

LGLMBS.TraverseAllClauses

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Loops over all clauses and calls TraverseAllClauses event for each.

Internally calls TraverseUnits, TraverseEquivalences and TraverseRemainingClauses.

See also:

• TraverseAllClauses(Lit as Integer)

LGLMBS.TraverseEquivalences

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Loops over equivalences and calls TraverseEquivalences event for each.

See also:

• TraverseEquivalences(Lit as Integer, Representation as Integer)

LGLMBS.TraverseRemainingClauses

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Loops over remaining clauses and calls TraverseRemainingClauses event for each.

See also:

• TraverseRemainingClauses(Lit as Integer)

LGLMBS.TraverseUnits

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Loops over units and calls TraverseUnits event for each.

See also:

• TraverseUnits(Unit as Integer)

LGLMBS.Unclone(Child as LGLMBS) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Unclones the object.

LGLMBS.Usable(lit as Integer) as Integer

Type	Topic	Plugin	Version	macOS	Windows	Linux	iOS	Targets
method	SATSolver	MBS Tools Plugin	20.0	✅ Yes	✅ Yes	✅ Yes	✅ Yes	All

Checks whether an item is usable.

If a literal was not frozen at the last call to Sat (or Simp) it becomes 'unusable' after the next call even though it might not have been used as blocking literal etc.