From baf643ab00478e7284d388b63986340c2081de22 Mon Sep 17 00:00:00 2001
From: Benjamin Kaufmann <kaufmann@cs.uni-potsdam.de>
Date: Wed, 4 Dec 2024 09:44:31 +0100
Subject: [PATCH] Update clasp.

* Fix issue in clingo propagator when adding asserting clauses.
---
 clasp                                       |  2 +-
 libpyclingo/clingo/tests/test_propagator.py | 50 +++++++++++++++++++++
 2 files changed, 51 insertions(+), 1 deletion(-)

diff --git a/clasp b/clasp
index 005bcf5ad..2207c3ab9 160000
--- a/clasp
+++ b/clasp
@@ -1 +1 @@
-Subproject commit 005bcf5ad301df5afc1784f31c9ef5083c943e57
+Subproject commit 2207c3ab9116652c3478428676bf44a912b43060
diff --git a/libpyclingo/clingo/tests/test_propagator.py b/libpyclingo/clingo/tests/test_propagator.py
index 7adcc36e1..7c672702a 100644
--- a/libpyclingo/clingo/tests/test_propagator.py
+++ b/libpyclingo/clingo/tests/test_propagator.py
@@ -262,3 +262,53 @@ def test_heurisitc(self):
         self.ctl.register_propagator(TestHeuristic(self))
         self.ctl.solve(on_model=self.mcb.on_model)
         self.assertEqual(self.mcb.models, _p(["a"]))
+
+
+class TestAddAssertingClause(TestCase):
+    class Prop(Propagator):
+        def __init__(self, tc, lock=False):
+            self._start_lit = 0
+            self._end_lit = 0
+            self._value_lit = 0
+            self._test = tc
+            self._lock = lock
+
+        def init(self, init: PropagateInit) -> None:
+            for atom in init.symbolic_atoms.by_signature("start", 0):
+                self._start_lit = init.solver_literal(atom.literal)
+            for atom in init.symbolic_atoms.by_signature("end", 0):
+                self._end_lit = init.solver_literal(atom.literal)
+            for atom in init.symbolic_atoms.by_signature("value", 0):
+                self._value_lit = init.solver_literal(atom.literal)
+            for lit in sorted([self._start_lit, self._end_lit, self._value_lit]):
+                init.add_watch(lit)
+                init.add_watch(-lit)
+
+        def propagate(self, control: PropagateControl, changes):
+            ass = control.assignment
+            if ass.is_false(self._value_lit) and ass.is_false(self._end_lit):
+                nogood = [self._start_lit, -self._end_lit, -self._value_lit]
+                dl = ass.decision_level
+                result = control.add_nogood(nogood, tag=False, lock=self._lock)
+                self._test.assertEqual(dl, ass.decision_level)
+                self._test.assertFalse(result)
+
+        def decide(self, thread_id: int, assignment: Assignment, fallback: int) -> int:
+            if assignment.is_free(self._end_lit): return -self._end_lit
+            if assignment.is_free(self._value_lit): return -self._value_lit
+            return fallback
+
+    def setUp(self):
+        self.ctl = Control(["0"])
+        self.ctl.add("base", [], "start. {value}. {end}.")
+        self.ctl.ground([("base", [])])
+
+    def test_default(self):
+        prop = TestAddAssertingClause.Prop(self, lock=False)
+        self.ctl.register_propagator(prop)
+        self.ctl.solve()
+
+    def test_locked(self):
+        prop = TestAddAssertingClause.Prop(self, lock=True)
+        self.ctl.register_propagator(prop)
+        self.ctl.solve()