Evaluate arithmetic terms before storing ground atoms

Fixes #159

src/main/java/at/ac/tuwien/kr/alpha/Alpha.java

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2017-2018, the Alpha Team.
+ * Copyright (c) 2017-2019, the Alpha Team.
  * All rights reserved.
  * 
  * Additional changes made by Siemens.
@@ -219,7 +219,7 @@ private Stream<AnswerSet> solve(CharStream program) throws IOException {
 	}
 
 	public Stream<AnswerSet> solve() {
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(debug);
 		Grounder grounder = GrounderFactory.getInstance(grounderName, program, atomStore);
 		Solver solver = SolverFactory.getInstance(solverName, storeName, atomStore, grounder, new Random(seed), BranchingHeuristicFactory.Heuristic.NAIVE, debug, false);
 		return solver.stream();

src/main/java/at/ac/tuwien/kr/alpha/Main.java

@@ -226,7 +226,7 @@ public static void main(String[] args) {
 			bailOut("Failed to parse program.", e);
 		}
 
-		final AtomStore atomStore = new AtomStoreImpl();
+		final AtomStore atomStore = new AtomStoreImpl(debugInternalChecks);
 		final Grounder grounder = GrounderFactory.getInstance(
 			commandLine.getOptionValue(OPT_GROUNDER, DEFAULT_GROUNDER), program, atomStore, filter, normalizationUseGrid
 		);

src/main/java/at/ac/tuwien/kr/alpha/common/AtomStore.java

@@ -1,6 +1,34 @@
+/**
+ * Copyright (c) 2016-2019, the Alpha Team.
+ * All rights reserved.
+ *
+ * Additional changes made by Siemens.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ *
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
 package at.ac.tuwien.kr.alpha.common;
 
 import at.ac.tuwien.kr.alpha.common.atoms.Atom;
+import at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm;
 
 import java.util.Iterator;
 
@@ -38,6 +66,14 @@ public interface AtomStore {
 	 * @return the int representing the Atom object.
 	 */
 	int get(Atom atom);
+
+	/**
+	 * Evaluates all {@link ArithmeticTerm}s in {@code groundAtom} before calling {@link #putIfAbsent(Atom)}.
+	 * The terms inside the atom are modified directly (TODO: change this, cf. issue #150)
+	 * @param groundAtom
+	 * @return the integer ID of the ground atom, possibly newly assigned
+	 */
+	int evaluateArithmeticTermsAndPutIfAbsent(Atom groundAtom);
 
 	/**
 	 * If the given ground atom is not already stored, associates it with a new integer (ID) and stores it, else

src/main/java/at/ac/tuwien/kr/alpha/common/AtomStoreImpl.java

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2016-2017, the Alpha Team.
+ * Copyright (c) 2016-2019, the Alpha Team.
  * All rights reserved.
  * 
  * Additional changes made by Siemens.
@@ -28,34 +28,65 @@
 package at.ac.tuwien.kr.alpha.common;
 
 import at.ac.tuwien.kr.alpha.common.atoms.Atom;
+import at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm;
+import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm;
+import at.ac.tuwien.kr.alpha.common.terms.FunctionTerm;
+import at.ac.tuwien.kr.alpha.common.terms.Term;
 import at.ac.tuwien.kr.alpha.grounder.IntIdGenerator;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
 
-import java.util.*;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
 
 import static at.ac.tuwien.kr.alpha.Util.oops;
 
 /**
  * This class stores ground atoms and provides the translation from an (integer) atomId to a (structured) predicate instance.
- * Copyright (c) 2016-2017, the Alpha Team.
+ * Copyright (c) 2016-2019, the Alpha Team.
  */
 public class AtomStoreImpl implements AtomStore {
 	private List<Atom> atomIdsToInternalBasicAtoms = new ArrayList<>();
 	private Map<Atom, Integer> predicateInstancesToAtomIds = new HashMap<>();
 	private IntIdGenerator atomIdGenerator = new IntIdGenerator(1);
+	private boolean debugInternalChecks;
 
 	private List<Integer> releasedAtomIds = new ArrayList<>();	// contains atomIds ready to be garbage collected if necessary.
-
-	public AtomStoreImpl() {
+
+	public AtomStoreImpl(boolean debugInternalChecks) {
+		this.debugInternalChecks = debugInternalChecks;
 		// Create atomId for falsum (currently not needed, but it gets atomId 0, which cannot represent a negated literal).
 		atomIdsToInternalBasicAtoms.add(null);
 	}
+
+	@Override
+	public int evaluateArithmeticTermsAndPutIfAbsent(Atom groundAtom) {
+		evaluateArithmeticTerms(groundAtom.getTerms());
+		return putIfAbsent(groundAtom);
+	}
+
+	private void evaluateArithmeticTerms(List<Term> terms) {
+		for (int i = 0; i < terms.size(); i++) {
+			Term term = terms.get(i);
+			if (term instanceof ArithmeticTerm) {
+				terms.set(i, ConstantTerm.getInstance(ArithmeticTerm.evaluateGroundTerm((ArithmeticTerm)term)));
+			}
+			if (term instanceof FunctionTerm) {
+				evaluateArithmeticTerms(((FunctionTerm)term).getTerms());
+			}
+		}
+	}
 
 	@Override
 	public int putIfAbsent(Atom groundAtom) {
 		if (!groundAtom.isGround()) {
 			throw new IllegalArgumentException("atom must be ground");
 		}
+
+		if (debugInternalChecks) {
+			checkNoArithmeticTerms(groundAtom.getTerms());
+		}
 
 		Integer id = predicateInstancesToAtomIds.get(groundAtom);
 
@@ -68,6 +99,17 @@ public int putIfAbsent(Atom groundAtom) {
 		return id;
 	}
 
+	private void checkNoArithmeticTerms(List<Term> terms) {
+		for (Term term : terms) {
+			if (term instanceof ArithmeticTerm) {
+				throw new IllegalArgumentException("ArithmeticTerm has not been evaluated: " + term);
+			}
+			if (term instanceof FunctionTerm) {
+				checkNoArithmeticTerms(((FunctionTerm)term).getTerms());
+			}
+		}
+	}
+
 	@Override
 	public boolean contains(Atom groundAtom) {
 		return predicateInstancesToAtomIds.containsKey(groundAtom);

src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2017-2018, the Alpha Team.
+ * Copyright (c) 2017-2019, the Alpha Team.
  * All rights reserved.
  * 
  * Additional changes made by Siemens.
@@ -45,7 +45,7 @@
 
 /**
  * Class to generate ground NoGoods out of non-ground rules and grounding substitutions.
- * Copyright (c) 2017-2018, the Alpha Team.
+ * Copyright (c) 2017-2019, the Alpha Team.
  */
 public class NoGoodGenerator {
 	private final AtomStore atomStore;
@@ -94,7 +94,7 @@ List<NoGood> generateNoGoodsFromGroundSubstitution(final NonGroundRule nonGround
 		}
 
 		final int bodyRepresentingLiteral = atomToLiteral(atomStore.putIfAbsent(bodyAtom));
-		final int headLiteral = atomToLiteral(atomStore.putIfAbsent(nonGroundRule.getHeadAtom().substitute(substitution)));
+		final int headLiteral = atomToLiteral(atomStore.evaluateArithmeticTermsAndPutIfAbsent(nonGroundRule.getHeadAtom().substitute(substitution)));
 
 		final List<NoGood> result = new ArrayList<>();
 
@@ -139,7 +139,7 @@ List<Integer> collectNegLiterals(final NonGroundRule nonGroundRule, final Substi
 				continue;
 			}
 
-			bodyLiteralsNegative.add(atomToLiteral(atomStore.putIfAbsent(groundAtom)));
+			bodyLiteralsNegative.add(atomToLiteral(atomStore.evaluateArithmeticTermsAndPutIfAbsent(groundAtom)));
 		}
 		return bodyLiteralsNegative;
 	}
@@ -174,7 +174,7 @@ private List<Integer> collectPosLiterals(final NonGroundRule nonGroundRule, fina
 				return null;
 			}
 
-			bodyLiteralsPositive.add(atomToLiteral(atomStore.putIfAbsent(groundAtom)));
+			bodyLiteralsPositive.add(atomToLiteral(atomStore.evaluateArithmeticTermsAndPutIfAbsent(groundAtom)));
 		}
 		return bodyLiteralsPositive;
 	}

src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java

@@ -55,7 +55,7 @@ public void groundRuleAlreadyGround() {
 				+ "b :- not a. "
 				+ "c :- b.");
 
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(true);
 		Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore);
 		Map<Integer, NoGood> noGoods = grounder.getNoGoods(new TrailAssignment(atomStore));
 		int litCNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("c", 0))), false);
@@ -75,7 +75,7 @@ public void groundRuleWithLongerBodyAlreadyGround() {
 				+ "c :- b. "
 				+ "d :- b, c. ");
 
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(true);
 		Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore);
 		Map<Integer, NoGood> noGoods = grounder.getNoGoods(new TrailAssignment(atomStore));
 		int litANeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("a", 0))), false);
@@ -98,7 +98,7 @@ public void groundConstraintAlreadyGround() {
 				+ "b :- not a. "
 				+ ":- b.");
 
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(true);
 		Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore);
 		Map<Integer, NoGood> noGoods = grounder.getNoGoods(new TrailAssignment(atomStore));
 		int litB = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0))));

src/test/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGeneratorTest.java

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2018 Siemens AG
+ * Copyright (c) 2018-2019 Siemens AG
  * All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
@@ -63,7 +63,7 @@ public void collectNeg_ContainsOnlyPositiveLiterals() {
 				+ "nq(a,b) :- not q(a,b).");
 
 		Rule rule = program.getRules().get(1);
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(true);
 		Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore);
 		NoGoodGenerator noGoodGenerator = ((NaiveGrounder)grounder).noGoodGenerator;
 		NonGroundRule nonGroundRule = NonGroundRule.constructNonGroundRule(rule);

src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java

@@ -1,3 +1,30 @@
+/**
+ * Copyright (c) 2018-2019, the Alpha Team.
+ * All rights reserved.
+ * 
+ * Additional changes made by Siemens.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * 
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ * 
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
 package at.ac.tuwien.kr.alpha.grounder.structure;
 
 import at.ac.tuwien.kr.alpha.common.AtomStore;
@@ -36,7 +63,7 @@ public void justifySimpleRules() {
 			"nr :- not r." +
 			":- not p(5).";
 		Program parsedProgram = parser.parse(program);
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(true);
 		NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore);
 		grounder.getNoGoods(null);
 		TrailAssignment assignment = new TrailAssignment(atomStore);
@@ -61,7 +88,7 @@ public void justifyLargerRules() {
 			"{s(1,2)}." +
 			":- not p(1).";
 		Program parsedProgram = parser.parse(program);
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(true);
 		NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore);
 		grounder.getNoGoods(null);
 		TrailAssignment assignment = new TrailAssignment(atomStore);
@@ -98,7 +125,7 @@ public void justifyMultipleReasons() {
 			"p(X) :- p(Y), s(Y,X)." +
 			":- not p(c).";
 		Program parsedProgram = parser.parse(program);
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(true);
 		NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore);
 		grounder.getNoGoods(null);
 		TrailAssignment assignment = new TrailAssignment(atomStore);
@@ -144,4 +171,4 @@ public void justifyMultipleReasons() {
 		assertFalse(reasons.isEmpty());
 	}
 
-}
+}

src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2017, the Alpha Team.
+ * Copyright (c) 2017-2019, the Alpha Team.
  * All rights reserved.
  *
  * Additional changes made by Siemens.
@@ -152,7 +152,7 @@ protected Solver getInstance(AtomStore atomStore, Grounder grounder) {
 	}
 
 	protected Solver getInstance(Program program) {
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(true);
 		return getInstance(atomStore, GrounderFactory.getInstance(grounderName, program, atomStore));
 	}
 

src/test/java/at/ac/tuwien/kr/alpha/solver/AggregatesTest.java

@@ -164,7 +164,7 @@ public void testAggregate_Sum_GlobalVariable() throws IOException {
 
 	@Override
 	protected Solver getInstance(Program program) {
-		AtomStore atomStore = new AtomStoreImpl();
+		AtomStore atomStore = new AtomStoreImpl(true);
 		return getInstance(atomStore, GrounderFactory.getInstance(grounderName, program, atomStore, p->true, useCountingGridNormalization()));
 	}
 

src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2017 Siemens AG
+ * Copyright (c) 2017-2019 Siemens AG
  * All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
@@ -51,7 +51,7 @@ public class ChoiceManagerTests extends AbstractSolverTests {
 	public void setUp() throws IOException {
 		String testProgram = "h :- b1, b2, not b3, not b4.";
 		Program parsedProgram = new ProgramParser().parse(testProgram);
-		this.atomStore = new AtomStoreImpl();
+		this.atomStore = new AtomStoreImpl(true);
 		this.grounder = new NaiveGrounder(parsedProgram, atomStore);
 		WritableAssignment assignment = new TrailAssignment(atomStore);
 		NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment);