Testing out models

pumpkin-py/examples/testing.py

@@ -0,0 +1,15 @@
+from pumpkin_py import Model, constraints, Comparator
+
+model = Model()
+
+iv = model.new_integer_variable(0,1)
+a = model.new_boolean_variable(name="a")
+b = model.new_boolean_variable(name="b")
+c = model.new_boolean_variable(name="c")
+
+model.add_constraint(constraints.Clause([a, b]))          # a \/ b
+model.add_constraint(constraints.Clause([b.negate(),c]))  # b -> c
+model.add_constraint(constraints.Clause([model.predicate_as_boolean(iv, Comparator.Equal, 1)])) # iv == 1
+model.add_implication(constraints.Equals([iv], 0), c)  # c -> iv == 0
+
+model.satisfy(proof="test")

pumpkin-py/test

@@ -0,0 +1,10 @@
+i 1 -1
+n 2 1 0 1
+i 3 1 2
+n 4 -2 0 2 3
+i 5 -2 -3
+n 6 3 0 4 5
+i 7 3 -4
+n 8 4 0 6 7
+i 9 4 5
+n 10 -5 0 8 9

pumpkin-py/test.drcp

@@ -0,0 +1,24 @@
+i 1 1 2
+i 2 4 0 -3
+i 3 4 0 -5
+i 4 4 0 -6
+i 5 4 0 -7
+n 6 -8 0 5 4 3 2 1
+i 7 9 1
+i 8 1 0 -10
+n 9 11 0 8 6 7
+i 10 9 7
+i 11 9 0 -5
+n 12 -12 0 6 11 9 10
+i 13 10 3
+n 14 -3 0 12 13
+i 15 10 5
+n 16 -5 0 12 15
+i 17 10 6
+n 18 -6 0 12 17
+i 19 7 2
+i 20 10 0 -6
+i 21 10 0 -5
+i 22 10 0 -3
+n 23 0 9 12 22 21 20 19
+c UNSAT

pumpkin-py/test.lits

@@ -0,0 +1,12 @@
+8 [q0 <= 0]
+7 [q1 == 0]
+10 [q0 == 2]
+2 [q2 == 1]
+4 [q0 == 0]
+5 [q1 == 1]
+3 [q2 == 2]
+9 [q0 == 1]
+6 [q2 == 0]
+1 [q1 == 2]
+11 [q1 <= 1]
+12 [q0 <= 1]

pumpkin-solver/src/engine/constraint_satisfaction_solver.rs

@@ -1336,7 +1336,20 @@ impl ConstraintSatisfactionSolver {
                     continue;
                 }
 
-                if let Some(step_id) = self.unit_nogood_step_ids.get(&trail_entry.predicate) {
+                if let Some(step_id) = self
+                    .unit_nogood_step_ids
+                    .get(&trail_entry.predicate)
+                    .or_else(|| {
+                        // It could be the case that we attempt to get the reason for the predicate
+                        // [x >= v] but that the corresponding unit nogood idea is the one for the
+                        // predicate [x == v]
+                        let domain_id = trail_entry.predicate.get_domain();
+                        let right_hand_side = trail_entry.predicate.get_right_hand_side();
+
+                        self.unit_nogood_step_ids
+                            .get(&predicate!(domain_id == right_hand_side))
+                    })
+                {
                     self.internal_parameters.proof_log.add_propagation(*step_id);
                 } else {
                     panic!(