# Getting Started#

## Installing#

bauhaus can be installed with pip:

```
pip install bauhaus
```

## Using Bauhaus#

First things first, import the bauhaus library:

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

Create Encoding objects that you intend to transform into a theory. Encoding objects will store your modelâ€™s propositional variables and constraints on the fly.

```
e = Encoding()
```

Create propositional variables by decorating class definitions with `@proposition`

.

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

Create constraints by decorating classes, methods, or invoking the constraint methods.

```
# 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
# 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)
```

Compile your theory into conjunctive or negation normal form (note: the theory is truncated),

```
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)})})})
```

And view the origin of each constraint, from the propositional object to the final constraint. (Note: the introspection is truncated)

```
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)})})
...
...
```