Fix issue #33

Simplification of sums correctly replaced eq atoms with their roots
but then searched for the original atoms when merging duplicates.
E.g. given 2 {x1, x2, x3} with x1 == x3, simplifySum() first replaced
'x3' with 'x1' but then unsuccessfully searched for 'x3' when trying
to merge the equivalent atoms into 'x1=2'.

CHANGES

@@ -2,6 +2,8 @@ clasp 3.3.4:
   * fixed: https://github.com/potassco/clasp/pull/22
   * fixed: https://github.com/potassco/clasp/issues/16
   * fixed: https://github.com/potassco/clasp/issues/18
+  * fixed: https://github.com/potassco/clasp/issues/33
+  * fixed: https://github.com/potassco/clasp/issues/34
   * fixed: possible infinite loop in detection of problem type from input.
   * fixed: Atoms of incremental programs not always marked as frozen.
   * added internal interface for user-defined statistics

src/logic_program.cpp

@@ -1680,7 +1680,9 @@ bool LogicProgram::simplifySum(Head_t ht, const Potassco::AtomSpan& head, const
 				meta.hash += hashLit(p);
 			}
 			else { // Merge duplicate lits
-				w = (std::find_if(out.wlits_begin(), out.wlits_end(), IsLit(Potassco::lit(*it)))->weight += w);
+				Potassco::WeightLit_t* pos = std::find_if(out.wlits_begin(), out.wlits_end(), IsLit(toInt(p)));
+				POTASSCO_ASSERT(pos != out.wlits_end());
+				w = (pos->weight += w);
 				++dirty;
 			}
 			if (w > maxW) { maxW = w; }

tests/program_builder_test.cpp

@@ -1512,6 +1512,37 @@ TEST_CASE("Incremental logic program", "[asp]") {
 		REQUIRE(findSmodels(exp, lp));
 	}
 
+	SECTION("testSimplifyRuleEq") {
+		lp.start(ctx);
+		lp.updateProgram();
+		lpAdd(lp,
+			"{x3}.\n"
+			"x1 :- x3.\n"
+			"x2 :- x3.\n");
+
+		// x1 == x2
+		REQUIRE((lp.endProgram() && ctx.endInit()));
+		uint32 x1 = lp.getAtom(1)->id();
+		uint32 x2 = lp.getAtom(2)->id();
+		REQUIRE(x1 == x2);
+
+		lp.updateProgram();
+
+		lpAdd(lp,
+			"{x4}.\n"
+			"x5 :- 2{x1, x2, x4}.");
+		REQUIRE(lp.endProgram());
+		REQUIRE(lp.getAtom(5)->supports() == 1);
+		PrgBody* body = lp.getBody(lp.getAtom(5)->supps_begin()->node());
+		REQUIRE(body->type() == Potassco::Body_t::Sum);
+		REQUIRE(body->bound() == 2);
+		REQUIRE(body->size() == 2);
+
+		uint32 eqIdx = body->goal(0).var() == 4;
+		REQUIRE(body->weight(eqIdx) == 2);
+		REQUIRE(body->weight(1 - eqIdx) == 1);
+	}
+
 	SECTION("testEqUnfreeze") {
 		lp.start(ctx);
 		lp.updateProgram();