Skip to content

Commit

Permalink
Added two simple API examples to README
Browse files Browse the repository at this point in the history
  • Loading branch information
hweichelt committed Sep 18, 2024
1 parent a93a642 commit 53c45a6
Showing 1 changed file with 63 additions and 0 deletions.
63 changes: 63 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -109,3 +109,66 @@ b(5) a(5)
```

A selection of more examples can be found [here](examples)

## API

Here are two example for using `clingexplaid`'s API.

### Minimal Unsatisfiable Subsets (MUS)

```python
import clingo
from clingexplaid.transformers import AssumptionTransformer
from clingexplaid.mus import CoreComputer

PROGRAM = """
a(1..3).
{b(4..6)}.
a(X) :- b(X).
:- a(X), X>=3.
"""

control = clingo.Control()
at = AssumptionTransformer(signatures={("a", 1)})

transformed_program = at.parse_string(PROGRAM)

control.add("base", [], transformed_program)
control.ground([("base", [])])

assumptions = at.get_assumption_literals(control)

cc = CoreComputer(control, assumptions)


def shrink_on_core(core) -> None:
mus_literals = cc.shrink(core)
print("MUS:", cc.mus_to_string(mus_literals))


control.solve(assumptions=list(assumptions), on_core=shrink_on_core)
```

### Unsatisfiable Constraints

```python
from clingexplaid.unsat_constraints import UnsatConstraintComputer

PROGRAM = """
a(1..3).
{b(4..6)}.
a(X) :- b(X).
:- a(X), X>=3.
"""

ucc = UnsatConstraintComputer()
ucc.parse_string(PROGRAM)
unsat_constraints = ucc.get_unsat_constraints()

for uc_id, unsat_constraint in unsat_constraints.items():
print(f"Unsat Constraint {uc_id}:", unsat_constraint)
```

0 comments on commit 53c45a6

Please sign in to comment.