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.ParseFile(File as FolderItem, force as boolean = false) as String

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

Parses data file.

Returns empty text on success or error message from parser.

See also:

• ParseFile(File as FolderItem, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

LGLMBS.ParseFile(File as FolderItem, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

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

Parses data file.

Returns empty text on success or error message from parser.

See also:

• ParseFile(File as FolderItem, force as boolean = false) as String

LGLMBS.ParseFileMT(File as FolderItem, force as boolean = false) as String

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

Parses data file.

Returns empty text on success or error message from parser.

The work is performed on a preemptive thread, so this function does not block the application and can yield time to other Xojo threads. Must be called in a Xojo thread to enjoy benefits. If called in main thread will block, but keep other background threads running.

See also:

• ParseFileMT(File as FolderItem, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

LGLMBS.ParseFileMT(File as FolderItem, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

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

Parses data file.

Returns empty text on success or error message from parser.

The work is performed on a preemptive thread, so this function does not block the application and can yield time to other Xojo threads. Must be called in a Xojo thread to enjoy benefits. If called in main thread will block, but keep other background threads running.

See also:

• ParseFileMT(File as FolderItem, force as boolean = false) as String

LGLMBS.ParsePath(Path as String, force as boolean = false) as String

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

Parses data file given by path.

Returns empty text on success or error message from parser.

On MacOS and Linux, if file has the following extensions, the file will be decompressed with command line tool and then parsed:

.gz	gzip
.xz	xz
.bz2	bzip2
.zip	unzip
.7z	7x

See also:

• ParsePath(Path as String, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

LGLMBS.ParsePath(Path as String, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

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

Parses data file given by path.

Returns empty text on success or error message from parser.

On MacOS and Linux, if file has the following extensions, the file will be decompressed with command line tool and then parsed:

.gz	gzip
.xz	xz
.bz2	bzip2
.zip	unzip
.7z	7x

See also:

• ParsePath(Path as String, force as boolean = false) as String

LGLMBS.ParsePathMT(Path as String, force as boolean = false) as String

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

Parses data file given by path.

Returns empty text on success or error message from parser.

On MacOS and Linux, if file has the following extensions, the file will be decompressed with command line tool and then parsed:

.gz	gzip
.xz	xz
.bz2	bzip2
.zip	unzip
.7z	7x

The work is performed on a preemptive thread, so this function does not block the application and can yield time to other Xojo threads. Must be called in a Xojo thread to enjoy benefits. If called in main thread will block, but keep other background threads running.

See also:

• ParsePathMT(Path as String, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

LGLMBS.ParsePathMT(Path as String, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

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

Parses data file given by path.

Returns empty text on success or error message from parser.

On MacOS and Linux, if file has the following extensions, the file will be decompressed with command line tool and then parsed:

.gz	gzip
.xz	xz
.bz2	bzip2
.zip	unzip
.7z	7x

The work is performed on a preemptive thread, so this function does not block the application and can yield time to other Xojo threads. Must be called in a Xojo thread to enjoy benefits. If called in main thread will block, but keep other background threads running.

See also:

• ParsePathMT(Path as String, force as boolean = false) as String

LGLMBS.ParseString(Data as String, force as boolean = false) as String

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

Parses data file given it as text.

Returns empty text on success or error message from parser.
Please pass text with data separated with unix line endings (endofline.unix), so you may need to use ReplaceLineEndings function.

See also:

• ParseString(Data as String, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

LGLMBS.ParseString(Data as String, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

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

Parses data file given it as text.

Returns empty text on success or error message from parser.
Please pass text with data separated with unix line endings (endofline.unix), so you may need to use ReplaceLineEndings function.

See also:

• ParseString(Data as String, force as boolean = false) as String

LGLMBS.ParseStringMT(Data as String, force as boolean = false) as String

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

Parses data file given it as text.

Returns empty text on success or error message from parser.
Please pass text with data separated with unix line endings (endofline.unix), so you may need to use ReplaceLineEndings function.

The work is performed on a preemptive thread, so this function does not block the application and can yield time to other Xojo threads. Must be called in a Xojo thread to enjoy benefits. If called in main thread will block, but keep other background threads running.

See also:

• ParseStringMT(Data as String, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

LGLMBS.ParseStringMT(Data as String, force as boolean, byref LineNo as Integer, byref Max as Integer) as String

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

Parses data file given it as text.

Returns empty text on success or error message from parser.
Please pass text with data separated with unix line endings (endofline.unix), so you may need to use ReplaceLineEndings function.

The work is performed on a preemptive thread, so this function does not block the application and can yield time to other Xojo threads. Must be called in a Xojo thread to enjoy benefits. If called in main thread will block, but keep other background threads running.

See also:

• ParseStringMT(Data as String, force as boolean = false) as String

LGLMBS.Print(File as FolderItem = nil)

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

Print system to file or stdout.

Pass nil to use stdout.
Remaining in DIMACS format

LGLMBS.PrintAll(File as FolderItem = nil)

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

Prints all values.

Including units & equivs.
Pass nil to use stdout.

Some examples using this method:

• /Tools/SATSolver/Test LGL

LGLMBS.PrintOptions(prefix as string, IgnoreSome as boolean)

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

Print all options to stdout.

LGLMBS.PrintPCS(mixed as boolean)

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

Prints PCS file.

LGLMBS.PrintRangeOptions

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

Print range options to stdout.

LGLMBS.PrintSizes

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

Prints data structure sizes.

LGLMBS.PrintStats

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

Prints statistics to stdout.

LGLMBS.PrintUsage

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

Print usage "-h".

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.