From 53c45a620ef4aad18ed1a6b51b91de0a516c6525 Mon Sep 17 00:00:00 2001
From: Hannes Weichelt <hweichelt@uni-potsdam.de>
Date: Wed, 18 Sep 2024 16:49:16 +0200
Subject: [PATCH] Added two simple API examples to README

---
 README.md | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)

diff --git a/README.md b/README.md
index 5b0a470..dac396a 100644
--- a/README.md
+++ b/README.md
@@ -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)
+```