Package org.mcp.core

Class MCPBitVector

java.lang.Object
org.mcp.core.MCPBitVector
public class MCPBitVector extends Object
Represents a symbolic bit vector for sets of constraints, supporting both BDD and SAT backends.

Provides logical operations (and, or, not, implication, etc.) and conversion between BDD and SAT representations. Each instance is associated with a backend type and the corresponding factory.

Since:
2025-02-28
Author:

  • Constructor Details

    • MCPBitVector

      public MCPBitVector(Object value, MCPFactory.MCPType type)
      Constructs a new MCPBitVector with the given value and backend type.
      Parameters:
      value - the underlying value (BDD or Formula)
      type - the backend type (BDD or SAT)

    • MCPBitVector

      public MCPBitVector(MCPBitVector other)
      Copy constructor. Creates a deep copy of the given MCPBitVector.
      Parameters:
      other - the MCPBitVector to copy

  • Method Details

    • setFactory

      public void setFactory(Object factory)
      Sets the factory (BDDFactory or FormulaFactory) for this bit vector.
      Parameters:
      factory - the factory object

    • getFactory

      public Object getFactory()
      Returns the factory (BDDFactory or FormulaFactory) associated with this bit vector.
      Returns:
      the factory object

    • or

      public MCPBitVector or(MCPBitVector other)
      Performs a logical OR with another MCPBitVector.
      Parameters:
      other - the other bit vector
      Returns:
      a new MCPBitVector representing the OR result

    • and

      public MCPBitVector and(MCPBitVector other)
      Performs a logical AND with another MCPBitVector.
      Parameters:
      other - the other bit vector
      Returns:
      a new MCPBitVector representing the AND result

    • andWith

      public MCPBitVector andWith(MCPBitVector other)
      Performs an in-place logical AND with another MCPBitVector (modifies this instance for SAT).
      Parameters:
      other - the other bit vector
      Returns:
      a new MCPBitVector representing the AND result

    • diff

      public MCPBitVector diff(MCPBitVector other)
      Computes the difference (this AND NOT other) with another MCPBitVector.
      Parameters:
      other - the other bit vector
      Returns:
      a new MCPBitVector representing the difference

    • diffWith

      public MCPBitVector diffWith(MCPBitVector other)
      Computes the in-place difference (this AND NOT other) with another MCPBitVector (modifies this instance for SAT).
      Parameters:
      other - the other bit vector
      Returns:
      a new MCPBitVector representing the difference

    • withFactory

      public MCPBitVector withFactory(Object factory)
      Returns a new MCPBitVector with the same value and the given factory set.
      Parameters:
      factory - the factory to set
      Returns:
      a new MCPBitVector with the factory set

    • getValue

      public Object getValue()
      Returns the underlying value (BDD or Formula) of this bit vector.
      Returns:
      the underlying value

    • 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 bit vector.
      Overrides:
      hashCode in class Object
      Returns:
      the hash code

    • toString

      public String toString()
      Returns a string representation of this bit vector.
      Overrides:
      toString in class Object
      Returns:
      a string representation

    • isZero

      public boolean isZero()
      Checks if this bit vector represents logical false (contradiction).
      Returns:
      true if contradiction, false otherwise

    • isOne

      public boolean isOne()
      Checks if this bit vector represents logical true (tautology).
      Returns:
      true if tautology, false otherwise

    • satCount

      public double satCount()
      Returns the number of satisfying assignments for this bit vector. For SAT, returns 1 if satisfiable, 0 otherwise.
      Returns:
      the number of satisfying assignments

    • imp

      public MCPBitVector imp(MCPBitVector other)
      Performs logical implication (this => other).
      Parameters:
      other - the other bit vector
      Returns:
      a new MCPBitVector representing the implication

    • impWith

      public MCPBitVector impWith(MCPBitVector other)
      Performs in-place logical implication (this => other) (modifies this instance for SAT).
      Parameters:
      other - the other bit vector
      Returns:
      a new MCPBitVector representing the implication

    • not

      public MCPBitVector not()
      Performs logical NOT on this bit vector.
      Returns:
      a new MCPBitVector representing the negation

    • biimp

      public MCPBitVector biimp(MCPBitVector other)
      Performs logical bi-implication (equivalence) with another MCPBitVector.
      Parameters:
      other - the other bit vector
      Returns:
      a new MCPBitVector representing the equivalence

    • id

      public MCPBitVector id()
      Returns a copy of this bit vector (for BDD, returns a new reference).
      Returns:
      a new MCPBitVector copy

    • getType

      public MCPFactory.MCPType getType()
      Returns the backend type of this bit vector.
      Returns:
      the MCPType (BDD or SAT)

    • isBDD

      public boolean isBDD()
      Checks if this bit vector uses the BDD backend.
      Returns:
      true if BDD, false otherwise

    • isSAT

      public boolean isSAT()
      Checks if this bit vector uses the SAT backend.
      Returns:
      true if SAT, false otherwise

    • copy

      public MCPBitVector copy()
      Returns a deep copy of this MCPBitVector.
      Returns:
      a new MCPBitVector copy