Add LogicProgram::project() query function.

potassco · Sep 2, 2024 · f9bbe9b · f9bbe9b
1 parent 69e8c3d
commit f9bbe9b
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 0 deletions.
diff --git a/clasp/logic_program.h b/clasp/logic_program.h
@@ -424,6 +424,8 @@ class LogicProgram : public ProgramBuilder {
 	 */
 	bool    extractCondition(Id_t cId, Potassco::LitVec& lits) const;
 
+	//! Returns the projection variables added in the current step.
+	Potassco::AtomSpan project() const;
 
 	//! Maps the given unsat core of solver literals to original program assumptions.
 	/*!

diff --git a/src/logic_program.cpp b/src/logic_program.cpp
@@ -2157,6 +2157,9 @@ Atom_t LogicProgram::falseAtom() {
 	return aFalse;
 }
 
+Potassco::AtomSpan LogicProgram::project() const {
+	return Potassco::toSpan(auxData_->project);
+}
 bool LogicProgram::extractCondition(Id_t id, Potassco::LitVec& out) const {
 	out.clear();
 	if (id == Clasp::Asp::falseId || (frozen() && getLiteral(id) == lit_false())) { return false; }

diff --git a/tests/parser_test.cpp b/tests/parser_test.cpp
@@ -527,6 +527,9 @@ TEST_CASE("Aspif parser", "[parser][asp]") {
 			"#project{x1, x3}.");
 		REQUIRE(parse(api, in));
 		REQUIRE(api.endProgram());
+		REQUIRE(api.project().size == 2);
+		REQUIRE(api.project()[0] == 1);
+		REQUIRE(api.project()[1] == 3);
 		REQUIRE(ctx.output.size() == 4);
 		Literal a = api.getLiteral(1);
 		Literal b = api.getLiteral(2);