### Install Bauhaus with pip

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_sources/getting_started.rst.txt

Use pip to install the bauhaus library. This is the first step to using the library.

```bash
pip install bauhaus
```

--------------------------------

### Import Bauhaus Library

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_sources/getting_started.rst.txt

Import the necessary components from the bauhaus library to start defining your logic model.

```python
from bauhaus import Encoding, proposition, constraint
```

--------------------------------

### Add Constraints with Helper Functions

Source: https://github.com/qumulab/bauhaus/blob/main/docs/getting_started.md

Add constraints using helper functions like add_at_most_one. This example enforces that at most one of the inputs is true.

```default
# At most one of the inputs is true.
constraint.add_at_most_one(e, A, A.method, Var('B'))

# Add arbitrary constraints on objects anotated with @proposition
x, y = A(1), A(2)
e.add_constraint(~x | y)
```

--------------------------------

### Define Constraints with @constraint Decorators

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_sources/getting_started.rst.txt

Use @constraint decorators on classes, methods, or directly invoke constraint methods to define rules for your propositional variables. This example shows 'implies_all' and 'at_most_k'.

```python
# Each instance of A implies the right side
@constraint.implies_all(e, right=['hello'])
# At most two of the A instances are true
@constraint.at_most_k(e, 2)
@proposition(e)
class A(object):

    def __init__(self, val):
        self.val = val

    def __repr__(self):
        return f"A.{self.val}"

    # Each instance of A implies the result of the method
    @constraint.implies_all(e)
    def method(self):
        return self.val
```

--------------------------------

### Initialize and Inspect Encoding

Source: https://context7.com/qumulab/bauhaus/llms.txt

Instantiate an Encoding object to collect propositions and constraints. Use `print(e)` to inspect its current state and `purge_propositions()` or `clear_constraints()` to reset it.

```python
from bauhaus import Encoding, proposition, constraint

e = Encoding()

# Inspect what the encoding currently holds
print(e)
# Encoding:
#   propositions::dict_keys([])
#   constraints::set()

# Manually clear propositions or constraints if reusing the encoding
e.purge_propositions()   # wipes all stored proposition instances
e.clear_constraints()    # wipes all stored constraint builders
```

--------------------------------

### Count Solutions and Likelihood Calculation

Source: https://context7.com/qumulab/bauhaus/llms.txt

Demonstrates how to count satisfying assignments and calculate the likelihood of a proposition being true within a compiled theory. Requires importing `Encoding`, `proposition`, `constraint`, `count_solutions`, and `likelihood`.

```python
from bauhaus import Encoding, proposition, constraint
from bauhaus.utils import count_solutions, likelihood

e = Encoding()

@constraint.at_most_one(e)
@proposition(e)
class Slot:
    def __init__(self, n):
        self.n = n
    def _prop_name(self):
        return f"Slot({self.n})"

slots = [Slot(i) for i in range(4)]
theory = e.compile()

total = count_solutions(theory)
print(f"Total models: {total}")           # 5 (none true, or exactly one of four)

prob = likelihood(theory, slots[0])
print(f"P(Slot(0)=True): {prob:.2f}")    # 0.20  (1 out of 5 models)

# Conditioned count: models where slots[0] AND slots[1] are both fixed
conditioned = count_solutions(theory, lits=[slots[0]])
print(f"Models with Slot(0)=True: {conditioned}")  # 1
```

--------------------------------

### Build and Add Constraint

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

This code snippet demonstrates how to build a constraint using a constraint builder and add it to an encoding. It handles cases with direct arguments (left/right) or a list of arguments.

```python
constraint = cbuilder(constraint_type, left=left, right=right)
encoding.constraints.add(constraint)
return
        elif args:
            args = tuple(flatten(args))
            constraint = cbuilder(constraint_type, args=args, k=k)
            encoding.constraints.add(constraint)
            return
        else:
            raise ValueError("Some or more of your provided" 
                             f" arguments for the {constraint_type.__name__}" 
                             " constraint were empty or invalid. Your" 
                             " provided arguments were: \n" 
                            f" args: {args}, " 
                            f" left: {left}, right: {right}")
```

--------------------------------

### Initialize Encoding Object in Python

Source: https://github.com/qumulab/bauhaus/blob/main/README.md

Create an Encoding object to store propositional variables and constraints. This is the first step in using the bauhaus library.

```python
from bauhaus import Encoding, proposition, constraint
e = Encoding()
```

--------------------------------

### Create an Encoding Object

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_sources/getting_started.rst.txt

Initialize an Encoding object to store propositional variables and constraints for your model.

```python
e = Encoding()
```

--------------------------------

### Encoding.introspect

Source: https://context7.com/qumulab/bauhaus/llms.txt

Debugs constraint origins by printing per-instance clauses. Optionally highlights variables based on a provided solution.

```APIDOC
## `Encoding.introspect` — Debug constraint origins

After `compile()`, `introspect()` prints the per-instance clauses that led to each final constraint. Optionally accepts a `solution` dict to colour-highlight true/false variables in the terminal output.

```python
from bauhaus import Encoding, proposition, constraint

e = Encoding()

@constraint.at_most_k(e, 2)
@proposition(e)
class Task:
    def __init__(self, name):
        self.name = name
    def _prop_name(self):
        return f"Task({self.name})"

tasks = [Task(n) for n in ["write", "review", "deploy", "monitor"]]
theory = e.compile()
solution = theory.solve()

# Print constraint origin traces
e.introspect(solution=solution)
# {Encoding Introspection}
#
# constraint.at_most_k:  function = Task  k = 2:
#
# (~Var(Task(write)), ~Var(Task(review))) =>
# Or({~Var(Task(write)), ~Var(Task(review)), ~Var(Task(deploy))})
# ...
# Final at_most_k: And({Or({...})})
```
```

--------------------------------

### Encoding.compile

Source: https://context7.com/qumulab/bauhaus/llms.txt

Builds the theory by iterating over stored constraints and builders, producing NNF clauses. Optionally converts to CNF.

```APIDOC
## `Encoding.compile` — Build the theory

Iterates over all stored `_ConstraintBuilder` objects and custom constraints, calls each builder's `.build()` method to produce NNF clauses, and returns a top-level `nnf.And` node. By default it converts to CNF (`CNF=True`); pass `CNF=False` for simpler NNF output.

```python
from bauhaus import Encoding, proposition, constraint

e = Encoding()

@constraint.exactly_one(e)
@proposition(e)
class Option:
    def __init__(self, label):
        self.label = label
    def _prop_name(self):
        return f"Opt({self.label})"

opts = [Option(x) for x in ["A", "B", "C"]]

# CNF form (default) — suitable for DPLL-based SAT solvers
cnf_theory = e.compile(CNF=True)

# NNF form — simpler but not in clause form
e.clear_constraints()
# re-add constraints ...
# nnf_theory = e.compile(CNF=False)

# Solve with python-nnf
solution = cnf_theory.solve()
print(solution)
# {Opt(A): False, Opt(B): True, Opt(C): False}  (one valid model)
```
```

--------------------------------

### Encoding Class Initialization

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Initializes an Encoding object to store propositions and constraints. It sets up attributes for propositions, constraints, and debugging information.

```python
def __init__(self):
        """
        Creates an Encoding object. This will store propositions
        and constraints that you can compile into a theory.

        Attributes
        ----------
        propositions : defaultdict(weakref.WeakValueDictionary)
            Stores decorated classes/functions pointing to
            their associated instances.These are later used
            to build the theory's constraints.

        constraints : set
            A set of unique _ConstraintBuilder objects
            that hold relevant information to build an NNF
            constraint.
            They are added to the Encoding object whenever the
            constraint decorator is used or when it is called
            as a function.
        debug_constraints : dictionary
            Maps ConstraintBuilder objects to their compiled
            constraints for debugging purposes.

        """
        self.propositions = defaultdict(weakref.WeakValueDictionary)
        self.constraints = set()
        self.debug_constraints = dict()
```

--------------------------------

### Encoding Propositions with Weak References

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_sources/architecture.rst.txt

Illustrates how the Encoding object uses WeakValueDictionaries to store propositions, allowing instances to be garbage collected if no longer referenced elsewhere.

```python
encoding.propositions = {classname -> WeakValueDictionary(id -> obj,
                                                              id -> obj,
                                                              …
                                                              id -> obj)
```

--------------------------------

### Debug Constraint Origins with Encoding.introspect

Source: https://context7.com/qumulab/bauhaus/llms.txt

Prints per-instance clauses after `compile()`. Optionally accepts a `solution` dict to highlight true/false variables in terminal output, aiding in debugging constraint origins.

```python
from bauhaus import Encoding, proposition, constraint

e = Encoding()

@constraint.at_most_k(e, 2)
@proposition(e)
class Task:
    def __init__(self, name):
        self.name = name
    def _prop_name(self):
        return f"Task({self.name})"

tasks = [Task(n) for n in ["write", "review", "deploy", "monitor"]]
theory = e.compile()
solution = theory.solve()

# Print constraint origin traces
e.introspect(solution=solution)
# {Encoding Introspection}
#
# constraint.at_most_k:  function = Task  k = 2:
#
# (~Var(Task(write)), ~Var(Task(review))) =>
# Or({~Var(Task(write)), ~Var(Task(review)), ~Var(Task(deploy))})
# ...
# Final at_most_k: And({Or({...})})
```

--------------------------------

### Pretty-Print NNF Formulas with Encoding.pprint

Source: https://context7.com/qumulab/bauhaus/llms.txt

Renders any `nnf.NNF` formula using logical symbols (∧, ∨, ¬). Supports optional ANSI color-coding when a solution dict is provided for highlighting.

```python
from bauhaus import Encoding, proposition, constraint

e = Encoding()

@constraint.at_least_one(e)
@proposition(e)
class Flag:
    def __init__(self, name):
        self.name = name
    def _prop_name(self):
        return f"Flag({self.name})"

flags = [Flag("x"), Flag("y"), Flag("z")]
theory = e.compile()
solution = theory.solve()

# Pretty-print the compiled theory with solution highlighting
for clause in theory:
    e.pprint(clause, solution=solution)
# (Flag(x) ∨ Flag(y) ∨ Flag(z))   — green if true, red if false
```

--------------------------------

### Encoding Propositions in Bauhaus

Source: https://github.com/qumulab/bauhaus/blob/main/docs/architecture.md

Illustrates how the 'propositions' attribute of an Encoding object stores propositions using a WeakValueDictionary to manage object references and enable garbage collection.

```default
encoding.propositions = {classname -> WeakValueDictionary(id -> obj,
                                                          id -> obj,
                                                          …
                                                          id -> obj)
```

--------------------------------

### Compile Constraints to NNF

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

Converts the stored constraints into a theory in Negation Normal Form (NNF).

```python
theory = e.compile(CNF=False)
```

--------------------------------

### Human-Readable Solution Display with print_theory

Source: https://context7.com/qumulab/bauhaus/llms.txt

Formats a solved theory dict into a table, grouped by truth value, object type, or both. Useful for presenting SAT solver results clearly.

```python
from bauhaus import Encoding, proposition, constraint, print_theory

e = Encoding()

@constraint.exactly_one(e)
@proposition(e)
class Candidate:
    def __init__(self, name):
        self.name = name
    def _prop_name(self):
        return f"Candidate({self.name})"

candidates = [Candidate(n) for n in ["Alice", "Bob", "Carol"]]
theory = e.compile()
solution = theory.solve()

print_theory(solution, format="truth")
# Solved theory:
#   Candidate(Alice):   True
#   Candidate(Bob):    False
#   Candidate(Carol):  False

print_theory(solution, format="objects")
# (grouped by type)

print_theory(solution, format="both")
# (grouped by truth value, then type)
```

--------------------------------

### Encoding.pprint

Source: https://context7.com/qumulab/bauhaus/llms.txt

Pretty-prints NNF formulas using logical symbols and optional ANSI color-coding when a solution is provided.

```APIDOC
## `Encoding.pprint` — Pretty-print NNF formulas

Renders any `nnf.NNF` formula with logical symbols (∧, ∨, ¬) and optional ANSI colour-coding when a solution dict is provided.

```python
from bauhaus import Encoding, proposition, constraint

e = Encoding()

@constraint.at_least_one(e)
@proposition(e)
class Flag:
    def __init__(self, name):
        self.name = name
    def _prop_name(self):
        return f"Flag({self.name})"

flags = [Flag("x"), Flag("y"), Flag("z")]
theory = e.compile()
solution = theory.solve()

# Pretty-print the compiled theory with solution highlighting
for clause in theory:
    e.pprint(clause, solution=solution)
# (Flag(x) ∨ Flag(y) ∨ Flag(z))   — green if true, red if false
```
```

--------------------------------

### Build Theory with Encoding.compile (CNF and NNF)

Source: https://context7.com/qumulab/bauhaus/llms.txt

Compiles stored constraints into NNF clauses. By default, it converts to CNF (`CNF=True`); set `CNF=False` for simpler NNF output. Suitable for DPLL-based SAT solvers.

```python
from bauhaus import Encoding, proposition, constraint

e = Encoding()

@constraint.exactly_one(e)
@proposition(e)
class Option:
    def __init__(self, label):
        self.label = label
    def _prop_name(self):
        return f"Opt({self.label})"

opts = [Option(x) for x in ["A", "B", "C"]]

# CNF form (default) — suitable for DPLL-based SAT solvers
cnf_theory = e.compile(CNF=True)

# NNF form — simpler but not in clause form
e.clear_constraints()
# re-add constraints ...
# nnf_theory = e.compile(CNF=False)

# Solve with python-nnf
solution = cnf_theory.solve()
print(solution)
# {Opt(A): False, Opt(B): True, Opt(C): False}  (one valid model)
```

--------------------------------

### Compile theory and view introspection

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/getting_started.html

Compile the encoding into a theory and use `e.introspect()` to view the origin of each constraint. Note that output may be truncated.

```python
objects = [A(val) for val in range(1,4)]
theory = e.compile()
# >> And({And({Or({Var(3), ~Var(A.3)}), Or({Var(1), ~Var(A.1)}),
# ...
#         And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})})})

e.introspect()
# >> constraint.at_most_k:  function = A  k = 2:

# (~Var(A.3), ~Var(A.1)) =>
# Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})

# (~Var(A.3), ~Var(A.2)) =>
# Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})

# (~Var(A.1), ~Var(A.2)) =>
# Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})

# Final at_most_k: And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})})
# ...
```

--------------------------------

### Compile Constraints to CNF

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

Converts the stored constraints into a theory in Conjunctive Normal Form (CNF). Set CNF to False to obtain Negation Normal Form (NNF).

```python
theory = e.compile()
```

--------------------------------

### Compile Constraints to Theory

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Compiles the stored constraints into a logical theory in Conjunctive Normal Form (CNF) or Negation Normal Form (NNF). Raises ValueError if constraints or propositions are empty.

```python
def compile(self, CNF=True) -> 'NNF':
        """ Convert constraints into a theory in
        conjunctive normal form, or if specified,
        the simpler negation-normal form.
        
        Arguments
        ---------
        CNF : bool
            Default is True. Converts a theory to CNF.
        
        Returns
        -------
        theory : NNF
            Conjunctive or Negation normal form of constraints.

        """
        if not self.constraints:
            raise ValueError(f"Constraints in {self} are empty."
                             " This can happen if no objects from"
                             " decorated classes are instantiated,"
                             " if no classes/methods are decorated"
                             " with @constraint or no function"
                             " calls of the form constraint.add_method")
        if not self.propositions.values():
            raise ValueError(f"Constraints in {self} are empty."
                             " This can happen if no objects from"
                             " decorated classes are instantiated.")

        theory = []
        self.clear_debug()

        for constraint in self.constraints:
            clause = constraint.build(self.propositions)
            if CNF:
                clause = clause.to_CNF()
            if clause:
                theory.append(clause)
                try:
                    self.debug_constraints[constraint] = clause
                except Exception as e:
                    raise(e)
            else:
                warnings.warn(f"The {constraint} was not built and"
                            "will not be added to the theory.")
        return And(theory)
```

--------------------------------

### constraint

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

A class that creates constraints on the fly, supporting various SAT constraints like 'at least one', 'at most one', 'exactly one', 'at most K', and 'implies all'. Constraints can be used as decorators or function invocations.

```APIDOC
## constraint

### Description
The `constraint` class facilitates the creation of various Satisfiability (SAT) constraints. It can be used as a decorator for classes or methods, or as a function to add constraints directly to an `Encoding` object. It supports multiple constraint types including 'at least one', 'at most one', 'exactly one', 'at most K', and 'implies all'.

### Usage
As a decorator:
```python
from bauhaus import Encoding, constraint, proposition

e = Encoding()

@constraint.at_most_one(e)
@proposition
class MyClass:
    pass

class MyOtherClass:
    @constraint.implies_all(e)
    def my_method(self):
        pass
```

As a function call:
```python
# Example for adding 'at least one' constraint
constraint.add_at_least_one(e, var1, var2, var3)
```

### Supported Constraints
- At least one
- At most one
- Exactly one
- At most K
- Implies all
```

--------------------------------

### Introspect Encoding Constraints

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Observes the origin of a theory from each propositional object to the final constraint. Use this to debug and understand constraint generation. Ensure the theory is compiled before calling.

```python
def introspect(self):
        """Observing the origin of a theory from each
        propositional object to the final constraint.

        Details
        -------
        The mapping is structured like so,

        Encoding.debug_constraints : dictionary

            key -> ConstraintBuilder object

            value -> Clause built in Encoding.compile()
        
        Each ConstraintBuilder object has the attribute
        instance_constraints : defaultdict with,

            key -> Object (from annotated class or method)

            value -> List of constraint clauses created per object
        
        This allows you to view the constraints created
        for annotated classes or methods and the per-instance
        object constraints, along with the final (succinct) 
        constraint.

        """
        if not self.debug_constraints:
            warnings.warn("Your theory has not been compiled yet,"
                          "so we cannot provide a representation of it."
                          "Try running compile() on your encoding.")
            return self.debug_constraints

        for constraint, clause in self.debug_constraints.items():
            print(f"{constraint}: \n")
            if constraint.instance_constraints:
                for instance, values in constraint.instance_constraints.items():
                        print(f"{instance} =>")
                        for v in values:
                            print(f"{v}")
                        print("\n")
            print(f"Final {constraint._constraint.__name__}: {clause} \n")
```

--------------------------------

### Decorate Function with Constraint

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

This method allows decorating a function with a constraint. It creates a constraint builder object and adds it to the encoding, then returns a wrapper for the original function.

```python
@classmethod
def _decorate(cls, 
                  encoding: Encoding,
                  constraint_type,
                  k=None,
                  left=None,
                  right=None):
        """
        `Private Method`:
        Create _ConstraintBuilder objects from constraint.method
        function calls

        Arguments
        ---------
        constraint : function
            Reference to the function for building an SAT encoding
            constraint in _ConstraintBuilder
        func : function
            Decorated class or bound method. Default = None.
        k : int
            Used for constraint "At most K".
        left : tuple
            Used for constraint "implies all".
            User-given arguments for the left implication.
        right : tuple
            Used for constraint "implies all".
            User-given arguments for the right implication.

        Returns
        -------
        Wrapper: Returns the function it decorated

        """
        def wrapper(func):
            constraint = cbuilder(constraint_type,
                                  func=func,
                                  k=k,
                                  left=left,
                                  right=right)
            encoding.constraints.add(constraint)

            @wraps(func)
            def wrapped(*args, **kwargs):
                ret = func(*args, **kwargs)
                return ret
            return wrapped
        return wrapper
```

--------------------------------

### Constraint Class Methods

Source: https://github.com/qumulab/bauhaus/blob/main/docs/bauhaus.md

Methods for creating and adding constraints to an Encoding object.

```APIDOC
## Constraint Class

### Description
Creates constraints on the fly when used as a decorator or as a function invocation. Supports various SAT constraints like 'At least one', 'At most one', 'Exactly one', 'At most K', and 'Implies all'.

### Methods

#### `add_at_least_one(*args)`
At least one of the propositional variables are True. Constraint is added directly with this function.
* **Parameters:**
  **encoding** ([*Encoding*](#bauhaus.Encoding)) – Given encoding.

### Example
`@constraint.add_at_least_one(encoding, [Obj, Class, Class.method])`

#### `add_at_most_k(k: int, *args)`
At most K of the propositional variables are True. Constraint is added directly with this function.
* **Parameters:**
  * **encoding** ([*Encoding*](#bauhaus.Encoding)) – Given encoding.
  * **k** (*int*) – The number of variables that are true at one time. Must be less than the number of total variables for the constraint.
```

--------------------------------

### Partition-based Constraints with `groupby`

Source: https://context7.com/qumulab/bauhaus/llms.txt

Utilize the `groupby` parameter in constraint decorators to apply constraints independently to sub-groups of propositions. `groupby` can accept an attribute name or a callable for defining these sub-groups.

```python
from bauhaus import Encoding, proposition, constraint

e = Encoding()

@constraint.exactly_one(e, groupby="row")   # exactly one True per row
@proposition(e)
class Cell:
    def __init__(self, row, col):
        self.row = row
        self.col = col
    def _prop_name(self):
        return f"C({self.row},{self.col})"

cells = [Cell(r, c) for r in range(3) for c in range(3)]
# Produces three independent "exactly one" constraints — one per row
theory = e.compile()
sol = theory.solve()
true_cells = [k for k, v in sol.items() if v]
print(true_cells)  # Exactly one cell per row is True, e.g. [C(0,1), C(1,0), C(2,2)]
```

--------------------------------

### Introspect Constraints in Bauhaus

Source: https://github.com/qumulab/bauhaus/blob/main/README.md

Use the introspect() method to view the origin and structure of constraints within the encoding. This helps in understanding how propositional objects map to the final compiled constraints.

```python
e.introspect()
>>
constraint.at_most_k:  function = A  k = 2:

(~Var(A.3), ~Var(A.1)) =>
Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})


(~Var(A.3), ~Var(A.2)) =>
Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})


(~Var(A.1), ~Var(A.2)) =>
Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})


Final at_most_k: And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})})
...
...

```

--------------------------------

### proposition

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Creates a propositional variable from a decorated class or function and adds it to the provided Encoding object. It returns the original object instance.

```APIDOC
## proposition(encoding: Encoding)

### Description
Creates a propositional variable from the decorated class or function and adds it to the `Encoding` object. Each instance of the decorated class will be added to the propositions in the given `Encoding` object. The original object instance is returned.

### Method
`@proposition(encoding)` decorator applied to a class.

### Parameters
- **encoding** (Encoding): The `Encoding` object to which the propositional variable will be added.

### Returns
- The decorated function or class.

### Example
```python
from bauhaus import Encoding, proposition

e = Encoding()

@proposition(e)
class MyClass(object):
    pass

# Now, instances of MyClass will be added to e.propositions
instance = MyClass()
# e.propositions will contain {'MyClass': {id(instance): instance}}
```
```

--------------------------------

### Encoding.introspect

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Observes the origin of a theory from each propositional object to the final constraint. It provides a detailed mapping of constraints, including constraints per object instance and the final compiled constraint.

```APIDOC
## introspect()

### Description
Observes the origin of a theory from each propositional object to the final constraint. This method provides a detailed mapping of constraints, including constraints per object instance and the final compiled constraint. If the theory has not been compiled, a warning is issued.

### Method
`self.introspect()`

### Parameters
None

### Response
- `debug_constraints` (dict): A dictionary where keys are `ConstraintBuilder` objects and values are the compiled `Clause` objects. Returns an empty dictionary if the theory has not been compiled.
```

--------------------------------

### Define Propositional Variables with @proposition

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_sources/getting_started.rst.txt

Decorate class definitions with @proposition to register instances as propositional variables within the Encoding object.

```python
@proposition(e) # Each instance of A is stored as a proposition
class A(object):
    pass
```

--------------------------------

### Introspect Constraints

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_sources/getting_started.rst.txt

Examine the origin and structure of the generated constraints, mapping propositional objects to their final form in the theory. The output is truncated.

```python
e.introspect()
>> 
constraint.at_most_k:  function = A  k = 2:

(~Var(A.3), ~Var(A.1)) =>
Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})


(~Var(A.3), ~Var(A.2)) =>
Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})


(~Var(A.1), ~Var(A.2)) =>
Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})


Final at_most_k: And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})}) 
...
```

--------------------------------

### Add At Most K Constraint

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

Use this function to add a constraint where at most K of the specified propositional variables can be true. Ensure K is less than the total number of variables.

```python
@constraint.add_at_most_k(encoding, k, [Obj, Class, Class.method])
```

--------------------------------

### constraint Decorator and Functions

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

The `constraint` decorator and functions are used to create constraints on propositions. It supports various constraint types like 'at least one', 'at most one', 'exactly one', 'at most K', and 'implies all'.

```APIDOC
## Class: bauhaus.constraint

### Description
Creates constraints on the fly when used as a decorator or function invocation. It supports several types of SAT constraints including 'At least one', 'At most one', 'Exactly one', 'At most K', and 'Implies all'.

### Methods
- `add_at_least_one(*args)`: Adds an 'at least one' constraint.

### Decorators
- `@constraint.method`: Used for decorating methods.
- `@constraint.at_most_one(e)`: Decorator for 'at most one' constraint.
- `@constraint.implies_all(e)`: Decorator for 'implies all' constraint.

### Usage Examples
```python
# Decorator for class or method
@constraint.at_most_one(e)
@proposition
class A:
    @constraint.implies_all(e)
    def do_something(self):
        pass

# Constraint creation by function call
constraint.add_at_least_one(e, *args)
```
```

--------------------------------

### Print Theory

Source: https://github.com/qumulab/bauhaus/blob/main/docs/bauhaus.md

Prints a solved theory in a human-readable format. Supports 'truth', 'objects', or 'both' formats.

```python
bauhaus.print_theory(theory: dict | None, format: str = 'truth')
```

--------------------------------

### Encoding Class

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

The `Encoding` object stores propositions and constraints, allowing them to be compiled into a logical theory. It supports introspection for debugging.

```APIDOC
## Class: bauhaus.Encoding

### Description
An `Encoding` object stores propositions and constraints created on the fly using `@proposition` and `@constraint` decorators and functions. These can be compiled into a logical theory in conjunctive or negation normal form for submission to a SAT solver. The `introspect()` function can be used for debugging the theory's origin.

### Attributes
- `propositions`: Stores decorated classes/functions pointing to their associated instances. Type: `defaultdict(weakref.WeakValueDictionary)`
- `constraints`: A set of unique `_ConstraintBuilder` objects holding information to build NNF constraints. Type: `set`
- `debug_constraints`: Maps `ConstraintBuilder` objects to their compiled constraints for debugging. Type: `dictionary`

### Methods
- `__init__()`: Creates an `Encoding` object.
- `clear_debug()`: Clears the `debug_constraints` attribute.
- `compile(_CNF=True)`: Compiles constraints into a theory in conjunctive normal form (CNF) or negation normal form (NNF). Returns an `NNF` object.
- `introspect()`: Provides a detailed view of the theory's origin, mapping `ConstraintBuilder` objects to their compiled constraints and showing per-object constraints.
```

--------------------------------

### bauhaus.proposition

Source: https://github.com/qumulab/bauhaus/blob/main/docs/bauhaus.md

Creates a propositional variable from a decorated class or function and adds it to the provided Encoding object. Returns the original object instance.

```APIDOC
## bauhaus.proposition(encoding: [Encoding](#bauhaus.Encoding))

### Description
Create a propositional variable from the decorated
class or function. Adds propositional variable to Encoding.
Return original object instance.

### Parameters
#### Path Parameters
- **encoding** ([*Encoding*](#bauhaus.Encoding)) – Given encoding object.

### Request Example
```python
e = Encoding()
@proposition(e)
class A(object):
    pass
```

### Response
#### Success Response (200)
- **The decorated function** (function) - Returns the original object instance.
```

--------------------------------

### Using @proposition Decorator

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

Decorate a class or function with @proposition to create a propositional variable and add it to the given Encoding object. Each instance of the decorated class becomes a proposition.

```python
e = Encoding()
@proposition(e)
class A(object):
    pass
>> e.propositions = {'A': {id: object}}
```

```python
@proposition(e)
class A(object):

    def __init__(self, data):
        self.data = data

    @constraint.implies_all(encoding)
    def foo(self):
        return self.data
```

--------------------------------

### Encoding Class Representation

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Provides a string representation of the Encoding object, showing its propositions and constraints.

```python
def __repr__(self) -> str:
        return (
                f"Encoding: \n"
                f"  propositions::{self.propositions.keys()} \n"
                f"  constraints::{self.constraints}")
```

--------------------------------

### At Most K Constraint Decorator

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Provides a decorator to enforce that at most K of the propositional variables in the encoding are True. It includes type and value checks for K and issues a warning if K is 1.

```python
if not isinstance(k, int):
            raise TypeError(f"The provided k={k} is not an integer.")
        if k < 1:
            raise ValueError(f"The provided k={k} is less than 1.")
        if k == 1:
            warnings.warn(f"Warning: The provided k={k} will" 
                           " result in an 'at most one' constraint,"
                           " but we'll proceed anyway.")
        return constraint._decorate(encoding,
                                    cbuilder.at_most_k,
                                    k=k)
```

--------------------------------

### print_theory

Source: https://github.com/qumulab/bauhaus/blob/main/docs/bauhaus.md

Prints a solved theory in a human-readable format. Propositions are printed according to their str or repr functions.

```APIDOC
## bauhaus.print_theory(theory: dict | None, format: str = 'truth')

### Description
Prints a solved theory in a human readable format. Propositions are printed according to their str or repr functions.

### Parameters
* **theory** (*dict*) – The theory to print.
* **format** (*str*) – The format to print the theory in. One of “truth”, “objects”, or “both”. Defaults to truth. truth: group output by truth values. objects: group output by object types. both: group output primarily by truth values, and secondarily by object type.
```

--------------------------------

### At Most K Decorator

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

Use this decorator to enforce that at most K of the propositional variables are true. Requires an encoding object and the value of K. K must be less than the total number of variables.

```python
@constraint.at_most_k(encoding, k)
```

--------------------------------

### print_theory

Source: https://context7.com/qumulab/bauhaus/llms.txt

Formats a solved theory dict into a human-readable table, grouped by truth value, object type, or both.

```APIDOC
## `print_theory` — Human-readable solution display

Formats a solved theory dict (from `nnf.And.solve()`) as a table grouped by truth value, by object type, or both.

```python
from bauhaus import Encoding, proposition, constraint, print_theory

e = Encoding()

@constraint.exactly_one(e)
@proposition(e)
class Candidate:
    def __init__(self, name):
        self.name = name
    def _prop_name(self):
        return f"Candidate({self.name})"

candidates = [Candidate(n) for n in ["Alice", "Bob", "Carol"]]
theory = e.compile()
solution = theory.solve()

print_theory(solution, format="truth")
# Solved theory:
#   Candidate(Alice):   True
#   Candidate(Bob):    False
#   Candidate(Carol):  False

print_theory(solution, format="objects")
# (grouped by type)

print_theory(solution, format="both")
# (grouped by truth value, then type)
```
```

--------------------------------

### Implies All Constraint (Decorator) - Method

Source: https://github.com/qumulab/bauhaus/blob/main/docs/bauhaus.md

Adds a constraint where propositions on the left imply propositions on the right. When decorating a method, instances are on the left, and return values are on the right. Additional variables can be specified for either side.

```python
@proposition(e)
class A(object):

    def __init__(self, data):
        self.data = data

    @constraint.implies_all(encoding)
    def foo(self):
        return self.data
```

--------------------------------

### Encoding Class Methods

Source: https://github.com/qumulab/bauhaus/blob/main/docs/bauhaus.md

Methods available on the Encoding class for managing propositions and constraints, compiling theories, and introspection.

```APIDOC
## Encoding Class

### Description
An Encoding object stores propositions and constraints created using decorators and functions. It can compile these into a logical theory in conjunctive or negation normal form.

### Methods

#### `__init__()`
Creates an Encoding object.

#### `propositions`
Stores decorated classes/functions pointing to their associated instances.
* **Type:** defaultdict(weakref.WeakValueDictionary)

#### `constraints`
A set of unique `_ConstraintBuilder` objects that hold relevant information to build an NNF constraint.
* **Type:** set

#### `debug_constraints`
Maps `ConstraintBuilder` objects to their compiled constraints for debugging purposes.
* **Type:** dictionary

#### `add_constraint(constraint: NNF)`
Add an NNF constraint to the encoding.
* **Parameters:**
  **cons** (*NNF*) – Constraint to be added.

#### `clear_constraints()`
Clears the constraints of an Encoding object.

#### `clear_debug_constraints()`
Clear `debug_constraints` attribute in Encoding.

#### `compile(CNF=True) → NNF`
Convert constraints into a theory in conjunctive normal form, or if specified, the simpler negation-normal form.
* **Parameters:**
  **CNF** (*bool*) – Default is True. Converts a theory to CNF.
* **Returns:**
  **theory** – Conjunctive or Negation normal form of constraints.
* **Return type:** NNF

#### `disable_custom_constraints()`
Disable the functionality for using custom_constraints.

#### `introspect(solution: dict | None = None, var_level=False)`
Observing the origin of a theory from each propositional object to the final constraint.
* **param solution:**
  Optional; A solution to use to highlight output.
* **type solution:** dictionary
* **param var_level:**
  Defaults to False; If True, output coloring will be based on the variable instead of the literal.
* **type var_level:** boolean

#### `pprint(formula, solution: dict | None = None, var_level=False)`
Pretty print an NNF formula.
* **Parameters:**
  * **formula** (*NNF*) – Formula to be displayed.
  * **solution** (*dictionary*) – Optional; A solution to use to highlight output.
  * **var_level** (*boolean*) – Defaults to False; If True, output coloring will be based on the variable instead of the literal.

#### `purge_propositions()`
Purges the propositional variables of an Encoding object.
```

--------------------------------

### At Least One Decorator

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

Use this decorator to enforce that at least one of the propositional variables is true. Requires an encoding object.

```python
@constraint.at_least_one(encoding)
```

--------------------------------

### Introspect Theory Origin

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

Allows observation of the theory's origin, mapping ConstraintBuilder objects to their compiled clauses and detailing per-instance constraints.

```python
e.introspect()
```

--------------------------------

### Create Propositional Variable with Bauhaus

Source: https://github.com/qumulab/bauhaus/blob/main/docs/bauhaus.md

Use the `@proposition` decorator to add class instances to an Encoding object's propositions. Ensure an Encoding object is initialized before decorating.

```python
e = Encoding()
@proposition(e)
class A(object):
    pass
>> e.propositions = {'A': {id: object}}
```

--------------------------------

### Define Propositional Variables with @proposition Decorator

Source: https://github.com/qumulab/bauhaus/blob/main/README.md

Decorate Python classes with @proposition to create propositional variables. Each instance of the decorated class will represent a unique proposition.

```python
@proposition(e) # Each instance of A is stored as a proposition
class A(object): pass
```

--------------------------------

### Create Propositional Variable Decorator

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Creates a propositional variable from a decorated class or function and adds it to the given Encoding object. Returns the original object instance.

```python
def proposition(encoding: Encoding):
    """Create a propositional variable from the decorated
    class or function. 
    
    Adds propositional variable to Encoding.

    Return original object instance.

    Arguments
    ---------
    encoding : Encoding
        Given encoding object.
    
    Returns
    -------
    The decorated function : function

    Examples
    --------

    Each instance of class A is added to propositions
    in the given Encoding object::

        e = Encoding()
        @proposition(e)
        class A(object):
            pass
        >> e.propositions = {'A': {id: object}}

    """
    def wrapper(cls):
        @wraps(cls)
        def wrapped(*args, **kwargs):
            ret = cls(*args, **kwargs)
            ret._var = Var(ret)
            class_name = ret.__class__.__qualname__
            encoding.propositions[class_name][id(ret)] = ret
            return ret
        return wrapped
    return wrapper
```

--------------------------------

### Add Custom NNF Constraints with Encoding.add_constraint

Source: https://context7.com/qumulab/bauhaus/llms.txt

Register custom formulas using `e.add_constraint()` to be included during compilation. Supports standard logical operators like &, |, ~, and >>.

```python
from bauhaus import Encoding, proposition

e = Encoding()

@proposition(e)
class Switch:
    def __init__(self, name):
        self.name = name
    def _prop_name(self):
        return f"Switch({self.name})"

a, b, c = Switch("A"), Switch("B"), Switch("C")

# A implies B, and either B or C must hold, and not both A and C
e.add_constraint(a >> b)
e.add_constraint(b | c)
e.add_constraint(~(a & c))

theory = e.compile()
sol = theory.solve()
print({str(k): v for k, v in sol.items()})
# e.g., {'Switch(A)': False, 'Switch(B)': True, 'Switch(C)': False}
```

--------------------------------

### Encoding.add_constraint

Source: https://context7.com/qumulab/bauhaus/llms.txt

Registers custom constraints with the encoding. These constraints are then included during the compilation process.

```APIDOC
## `Encoding.add_constraint` — Custom NNF constraints

After annotating classes with `@proposition`, individual instances support `&`, `|`, `~`, and `>>` directly to build arbitrary custom formulas. These are registered with `e.add_constraint()` and included during `compile()`.

```python
from bauhaus import Encoding, proposition

e = Encoding()

@proposition(e)
class Switch:
    def __init__(self, name):
        self.name = name
    def _prop_name(self):
        return f"Switch({self.name})"

a, b, c = Switch("A"), Switch("B"), Switch("C")

# A implies B, and either B or C must hold, and not both A and C
e.add_constraint(a >> b)
e.add_constraint(b | c)
e.add_constraint(~(a & c))

theory = e.compile()
sol = theory.solve()
print({str(k): v for k, v in sol.items()})
# e.g., {'Switch(A)': False, 'Switch(B)': True, 'Switch(C)': False}
```
```

--------------------------------

### Compile Theory

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_sources/getting_started.rst.txt

Compile the defined encoding into a theory, typically in conjunctive or negation normal form. The output is truncated for brevity.

```python
objects = [A(val) for val in range(1,4)]
theory = e.compile()
>> And({And({Or({Var(3), ~Var(A.3)}), Or({Var(1), ~Var(A.1)}),
        ...
        And({Or({~Var(A.1), ~Var(A.2), ~Var(A.3)})})})
```

--------------------------------

### none_of

Source: https://github.com/qumulab/bauhaus/blob/main/docs/bauhaus.md

Adds a constraint that ensures none of the propositional variables are true. This constraint is added using the @constraint decorator.

```APIDOC
## none_of(**kwargs)

### Description
None of the propositional variables are True. Constraint is added with the @constraint decorator.

### Parameters
* **encoding** ([*Encoding*](#bauhaus.Encoding)) – Given encoding.
```

--------------------------------

### None True Constraint for Propositions

Source: https://context7.com/qumulab/bauhaus/llms.txt

Apply `@constraint.none_of` to assert that no proposition within the specified group can be true simultaneously. This is encoded as the negation of an OR, equivalent to an AND of negated variables.

```python
from bauhaus import Encoding, proposition, constraint

e = Encoding()

@constraint.none_of(e)
@proposition(e)
class BannedMove:
    def __init__(self, move):
        self.move = move
    def _prop_name(self):
        return f"Banned({self.move})"

banned = [BannedMove(m) for m in ["e4", "d4", "Nf3"]]
theory = e.compile()
sol = theory.solve()
# All banned moves are False in every solution
print(all(not sol[k] for k in sol))  # True
```

--------------------------------

### Exactly One Constraint Decorator

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Provides a decorator to enforce that exactly one of the propositional variables in the encoding is True. The constraint is automatically added to the given encoding.

```python
@constraint._decorate(encoding, cbuilder.exactly_one)
```

--------------------------------

### bauhaus.proposition

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

Decorator to create a propositional variable from a decorated class or function and add it to an Encoding object.

```APIDOC
## bauhaus.proposition(encoding: bauhaus.core.Encoding)

### Description
Create a propositional variable from the decorated class or function. Adds propositional variable to Encoding. Return original object instance.

### Parameters
#### Path Parameters
- **encoding** (Encoding) - Required - Given encoding object.

### Returns
- **function** - The decorated function

### Example
```python
e = Encoding()
@proposition(e)
class A(object):
    pass
# e.propositions will contain {'A': {id: object}}
```
```

--------------------------------

### add_at_most_k

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/_modules/bauhaus/core.html

Adds a constraint that at most K of the provided propositional variables can be True. This is used directly as a function call.

```APIDOC
## add_at_most_k

### Description
At most K of the propositional variables are True

Constraint is added directly with this function.

### Arguments
* `encoding` (Encoding): Given encoding.
* `k` (int): The number of variables that are true at one time. Must be less than the number of total variables for the constraint.
* `*args`: Variable number of propositional variables.

### Example
```python
@constraint.add_at_most_k(encoding, k, [Obj, Class, Class.method])
```
```

--------------------------------

### Exactly One Decorator

Source: https://github.com/qumulab/bauhaus/blob/main/docs/_build/html/bauhaus.html

Use this decorator to enforce that exactly one of the propositional variables is true. Requires an encoding object.

```python
@constraint.exactly_one(encoding)
```

--------------------------------

### Add At Most K Constraint by Function Call

Source: https://github.com/qumulab/bauhaus/blob/main/docs/bauhaus.md

Directly add an 'at most K' constraint to an encoding using the add_at_most_k function. Specify the maximum number of true variables (k) and the propositional variables involved.

```python
constraint.add_at_most_k(encoding, k, *args)
```