Fix handling of "sticky" logic program options.

* Enabling distinct true variables for incremental steps should be a
  "sticky" operation that must be independent of changes to other
  preprocessor options.

clasp/logic_program.h

@@ -143,25 +143,25 @@ class LogicProgram : public ProgramBuilder {
 		mode_transform_scc    = 5, //!< Transform recursive cardinality- and weight rules to normal rules.
 		mode_transform_nhcf   = 6, //!< Transform cardinality- and weight rules in non-hcf components to normal rules.
 		mode_transform_integ  = 7, //!< Transform cardinality-based integrity constraints.
-		mode_transform_dynamic= 8  //!< Heuristically decide whether or not to transform a particular extended rule.
+		mode_transform_dynamic= 8  //!< Heuristically decide whether to transform a particular extended rule.
 	};
 
 	//! Options for the Asp-Preprocessor.
 	struct AspOptions {
-		static const uint32 MAX_EQ_ITERS = static_cast<uint32>( (1u<<25)-1 );
+		static const uint32 MAX_EQ_ITERS = static_cast<uint32>( (1u<<26)-1 );
 		typedef ExtendedRuleMode TrMode;
 		AspOptions() {
+			static_assert(sizeof(*this) == sizeof(TrMode) + sizeof(uint32), "unexpected alignment");
 			std::memset(this, 0, sizeof(AspOptions));
 			iters = 5;
 		}
-		AspOptions& iterations(uint32 it)   { iters   = it;return *this;}
+		AspOptions& iterations(uint32 it)   { iters   = it <= MAX_EQ_ITERS ? it : MAX_EQ_ITERS; return *this;}
 		AspOptions& depthFirst()            { dfOrder = 1; return *this;}
 		AspOptions& backpropagate()         { backprop= 1; return *this;}
 		AspOptions& noScc()                 { noSCC   = 1; return *this;}
 		AspOptions& noEq()                  { iters   = 0; return *this;}
 		AspOptions& disableGamma()          { noGamma = 1; return *this;}
 		AspOptions& ext(ExtendedRuleMode m) { erMode  = m; return *this;}
-		AspOptions& distinctTrue()          { distTrue= 1; return *this;}
 		TrMode erMode;       //!< How to handle extended rules?
 		uint32 iters    : 26;//!< Number of iterations in eq-preprocessing or 0 to disable.
 		uint32 noSCC    :  1;//!< Disable scc checking?
@@ -170,7 +170,6 @@ class LogicProgram : public ProgramBuilder {
 		uint32 backprop :  1;//!< Enable backpropagation during preprocessing?
 		uint32 oldMap   :  1;//!< Use old and larger mapping for disjunctive programs.
 		uint32 noGamma  :  1;//!< Disable creation of (shifted) gamma rules for non-hcf disjunctions?
-		uint32 distTrue :  1;//!< Add distinct true var for each step instead of one for all steps.
 	};
 
 	/*!
@@ -227,7 +226,7 @@ class LogicProgram : public ProgramBuilder {
 	 */
 	bool end() { return endProgram(); }
 
-	//! Visits the the simplified program by notifying out on its elements.
+	//! Visits the simplified program by notifying out on its elements.
 	void accept(Potassco::AbstractProgram& out);
 
 	//! Disposes (parts of) the internal representation of the logic program.
@@ -315,7 +314,7 @@ class LogicProgram : public ProgramBuilder {
 
 	//! Adds the given rule (or integrity constraint) to the program.
 	/*!
-	 * \pre The the rule does not define an atom from a previous incremental step.
+	 * \pre The rule does not define an atom from a previous incremental step.
 	 *
 	 * Simplifies the given rule and adds it to the program if it
 	 * is neither tautological (e.g. a :- a) nor contradictory (e.g. a :- b, not b).
@@ -428,7 +427,7 @@ class LogicProgram : public ProgramBuilder {
 
 	//! Maps the given unsat core of solver literals to original program assumptions.
 	/*!
-	 * \param solverCore An unsat core found when solving under ProgramBuilder::getAssumptions().
+	 * \param unsatCore An unsat core found when solving under ProgramBuilder::getAssumptions().
 	 * \param prgLits The given unsat core expressed in terms of program literals.
 	 * \return Whether unsatCore was successfully mapped.
 	 */

src/logic_program.cpp

@@ -214,9 +214,11 @@ struct LogicProgram::Aux {
 };
 
 struct LogicProgram::IndexData {
+	IndexData() : distTrue(false) {}
 	IndexMap body;  // hash -> body id
 	IndexMap disj;  // hash -> disjunction id
 	IndexMap domEq; // maps eq atoms modified by dom heuristic to aux vars
+	bool  distTrue;
 };
 
 LogicProgram::LogicProgram() : theory_(0), input_(1, UINT32_MAX), auxData_(0), incData_(0) {
@@ -256,6 +258,7 @@ void LogicProgram::dispose(bool force) {
 		theory_  = 0;
 		input_   = AtomRange(1, UINT32_MAX);
 		statsId_ = 0;
+		*index_  = IndexData();
 	}
 	rule_.clear();
 }
@@ -286,7 +289,7 @@ void LogicProgram::setOptions(const AspOptions& opts) {
 	}
 }
 void LogicProgram::enableDistinctTrue() {
-	opts_.distinctTrue();
+	index_->distTrue = true;
 }
 ProgramParser* LogicProgram::doCreateParser() {
 	return new AspParser(*this);
@@ -1221,7 +1224,7 @@ void LogicProgram::prepareProgram(bool checkSccs) {
 	prepareComponents();
 	prepareOutputTable();
 	freezeAssumptions();
-	if (incData_ && options().distTrue) {
+	if (incData_ && index_->distTrue) {
 		for (Var a = startAtom(), end = startAuxAtom(); a != end; ++a) {
 			if (isSentinel(getRootAtom(a)->literal())) {
 				Incremental::StepTrue t(end - 1, 0);
@@ -1489,9 +1492,10 @@ void LogicProgram::prepareOutputTable() {
 	std::stable_sort(show_.begin(), show_.end(), compose22(std::less<Id_t>(), select1st<ShowPair>(), select1st<ShowPair>()));
 	for (ShowVec::iterator it = show_.begin(), end = show_.end(); it != end; ++it) {
 		Literal lit = getLiteral(it->first);
-		bool isAtom = it->first < startAuxAtom();
-		if      (!isSentinel(lit))  { out.add(it->second, lit, it->first); if (isAtom) ctx()->setOutput(lit.var(), true); }
+		if      (!isSentinel(lit))  { out.add(it->second, lit, it->first); }
 		else if (lit == lit_true()) { out.add(it->second); }
+		bool isAtom = it->first < startAuxAtom();
+		if (isAtom) { ctx()->setOutput(lit.var(), true); }
 	}
 	if (!auxData_->project.empty()) {
 		for (VarVec::const_iterator it = auxData_->project.begin(), end = auxData_->project.end(); it != end; ++it) {

tests/parser_test.cpp

@@ -498,10 +498,11 @@ TEST_CASE("Aspif parser", "[parser][asp]") {
 	SECTION("testOutputDirective") {
 		in.toAspif("{x1;x2}."
 			"#output fact.\n"
-			"#output conj : x1, x2.");
+			"#output conj : x1, x2."
+			"#output lit : not x1.");
 		REQUIRE(parse(api, in));
 		REQUIRE((api.endProgram() && ctx.endInit()));
-		REQUIRE(ctx.output.size() == 2);
+		REQUIRE(ctx.output.size() == 3);
 		REQUIRE(ctx.output.numFacts() == 1);
 		REQUIRE(sameProgram(api, in));
 	}