Package org.mcp.sat

Class MutableSATInteger

java.lang.Object

org.mcp.sat.SATInteger

org.mcp.sat.MutableSATInteger

All Implemented Interfaces:

Serializable

public final class MutableSATInteger
extends SATInteger

MutableSATInteger represents a mutable bit-vector for SAT-based integer encoding.

Provides methods for constructing, copying, and manipulating SAT integer variables, as well as converting SAT assignments to integer values.

Since:

2025-02-28

Author:

See Also:

• Serialized Form

Field Summary

Fields inherited from class org.mcp.sat.SATInteger

_bitvec, _factory, _maxVal

Constructor Summary

Constructors

Constructor	Description
MutableSATInteger(org.logicng.formulas.FormulaFactory factory, int length)	Constructs a MutableSATInteger with the given length, initializing all bits as free variables.
MutableSATInteger(org.logicng.formulas.FormulaFactory factory, org.logicng.formulas.Variable[] bitvec)	Constructs a MutableSATInteger from a bit vector.
MutableSATInteger(MutableSATInteger other)	Copy constructor.

Method Summary

Modifier and Type	Method	Description
boolean	equals(Object o)	Checks equality with another object.
protected org.logicng.formulas.Formula	firstBitsEqual(long value, int length)	Returns a formula representing the first length bits equal to the given value.
int	hashCode()	Returns the hash code for this MutableSATInteger.
static MutableSATInteger	makeFromIndex(org.logicng.formulas.FormulaFactory factory, int length, int start, boolean reverse)	Creates a MutableSATInteger from a bitvector index.
long	satAssignmentToLong(org.logicng.datastructures.Assignment assignment)	Converts a SAT assignment to a long value.

Methods inherited from class org.mcp.sat.SATInteger

getBitvec, getFactory, getValueSatisfying, getValueSatisfyingToInt, getValuesSatisfying, size, value

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait

Constructor Details

MutableSATInteger

public MutableSATInteger(org.logicng.formulas.FormulaFactory factory,
 org.logicng.formulas.Variable[] bitvec)

Constructs a MutableSATInteger from a bit vector.

Parameters:

factory - the formula factory

bitvec - the bit vector

MutableSATInteger

public MutableSATInteger(org.logicng.formulas.FormulaFactory factory,
 int length)

Constructs a MutableSATInteger with the given length, initializing all bits as free variables.

Parameters:

factory - the formula factory

length - the number of bits

MutableSATInteger

public MutableSATInteger(MutableSATInteger other)

Copy constructor.

Parameters:

other - the MutableSATInteger to copy

Method Details

makeFromIndex

public static MutableSATInteger makeFromIndex(org.logicng.formulas.FormulaFactory factory,
 int length,
 int start,
 boolean reverse)

Creates a MutableSATInteger from a bitvector index.

Parameters:

factory - the formula factory

length - the number of bits

start - the starting index

reverse - whether to reverse the bit order

Returns:

a new MutableSATInteger

satAssignmentToLong

public long satAssignmentToLong(org.logicng.datastructures.Assignment assignment)

Converts a SAT assignment to a long value.

Specified by:

satAssignmentToLong in class SATInteger

Parameters:

assignment - the SAT assignment

Returns:

the corresponding long value

firstBitsEqual

protected org.logicng.formulas.Formula firstBitsEqual(long value,
 int length)

Returns a formula representing the first length bits equal to the given value.

Specified by:

firstBitsEqual in class SATInteger

Parameters:

value - the value to compare

length - the number of bits to check

Returns:

the formula representing the equality

equals

public boolean equals(Object o)

Checks equality with another object.

Overrides:

equals in class Object

Parameters:

o - the object to compare

Returns:

true if equal, false otherwise

hashCode

public int hashCode()

Returns the hash code for this MutableSATInteger.

Overrides:

hashCode in class Object

Returns:

the hash code