Support for Offset Equalities

Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/PrintTerm.java

@@ -144,6 +144,16 @@ private void run(final Appendable appender) throws IOException {
 					}
 				}
 				appender.append('(');
+			} else if (next instanceof int[]) {
+				final int[] arr = (int[]) next;
+				mTodo.addLast(")");
+				for (int i = arr.length - 1; i >= 0; i--) {
+					mTodo.addLast(arr[i]);
+					if (i > 0) {
+						mTodo.addLast(" ");
+					}
+				}
+				appender.append('(');
 			} else {
 				appender.append(next.toString());
 			}

SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/convert/CCTermBuilder.java

@@ -22,8 +22,10 @@
 
 import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
 import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol;
+import de.uni_freiburg.informatik.ultimate.logic.Rational;
 import de.uni_freiburg.informatik.ultimate.logic.Term;
 import de.uni_freiburg.informatik.ultimate.smtinterpol.proof.SourceAnnotation;
+import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCParameter;
 import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm;
 import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CClosure;
 
@@ -35,19 +37,29 @@ public class CCTermBuilder {
 	private final SourceAnnotation mSource;
 
 	private final ArrayDeque<Operation> mOps = new ArrayDeque<>();
-	private final ArrayDeque<CCTerm> mConverted = new ArrayDeque<>();
+	/**
+	 * The converted results as {@link CCParameter}s: the term that produced {@code mConverted.peek()} has value
+	 * {@code peek().getCCTerm() + peek().getOffset()}. The offset carries the {@code +5} of an offset-free term like
+	 * {@code x+5} up to the enclosing application, where it ends up in that argument's {@link CCParameter}. Offsets are
+	 * {@link Rational#ZERO} (i.e. a bare {@link CCTerm}) unless offset equalities are enabled.
+	 */
+	private final ArrayDeque<CCParameter> mConverted = new ArrayDeque<>();
 
 	public CCTermBuilder(Clausifier clausifier, final SourceAnnotation source) {
 		mClausifier = clausifier;
 		mSource = source;
 	}
 
-	public CCTerm convert(final Term t) {
+	private void pushResult(final CCParameter ccParam) {
+		mConverted.push(ccParam);
+	}
+
+	public CCParameter convert(final Term t) {
 		mOps.push(new BuildCCTerm(t));
 		while (!mOps.isEmpty()) {
 			mOps.pop().perform();
 		}
-		final CCTerm res = mConverted.pop();
+		final CCParameter res = mConverted.pop();
 		assert mConverted.isEmpty();
 		return res;
 	}
@@ -61,12 +73,19 @@ public BuildCCTerm(final Term term) {
 
 		@Override
 		public void perform() {
-			CCTerm ccTerm = mClausifier.getCCTerm(mTerm);
+			// mCCTerms is keyed by offset-free terms; probe (and below build) the offset-free part, then re-apply the
+			// constant as the CCParameter's offset (zero when the term is already offset-free).
+			final Term offsetFree = mClausifier.getOffsetFreeTerm(mTerm);
+			final CCTerm ccTerm = mClausifier.getCCTerm(offsetFree);
 			if (ccTerm != null) {
-				mConverted.push(ccTerm);
+				pushResult(CCParameter.of(ccTerm, mClausifier.getTermConstant(mTerm)));
 			} else {
 				final CClosure cclosure = mClausifier.getCClosure();
-				if (Clausifier.needCCTerm(mTerm) && ((ApplicationTerm) mTerm).getParameters().length > 0) {
+				if (offsetFree != mTerm) {
+					// Numeric term with a non-zero constant: build the offset-free CCTerm and remember the constant.
+					mOps.push(new AddOffsetToTerm(mClausifier.getTermConstant(mTerm)));
+					mOps.push(new BuildCCTerm(offsetFree));
+				} else if (Clausifier.needCCTerm(mTerm) && ((ApplicationTerm) mTerm).getParameters().length > 0) {
 					final FunctionSymbol fs = ((ApplicationTerm) mTerm).getFunction();
 					if (fs.isIntern() && fs.getName() == "select") {
 						mClausifier.getArrayTheory().cleanCaches();
@@ -79,16 +98,34 @@ public void perform() {
 					}
 				} else {
 					// We have an intern function symbol
-					ccTerm = cclosure.createAnonTerm(mTerm);
-					cclosure.addTerm(ccTerm, mTerm);
-					mClausifier.shareCCTerm(mTerm, ccTerm);
+					final CCTerm anonTerm = cclosure.createAnonTerm(mTerm);
+					cclosure.addTerm(anonTerm, mTerm);
+					mClausifier.shareCCTerm(mTerm, anonTerm);
 					mClausifier.addTermAxioms(mTerm, mSource);
-					mConverted.push(ccTerm);
+					pushResult(anonTerm);
 				}
 			}
 		}
 	}
 
+	/**
+	 * Adds an offset to the (already built) numeric CCTerm of its offset-free part,
+	 * and pushes the CCParameter with the offset.
+	 */
+	private class AddOffsetToTerm implements Operation {
+		private final Rational mOffset;
+
+		public AddOffsetToTerm(final Rational offset) {
+			mOffset = offset;
+		}
+
+		@Override
+		public void perform() {
+			final CCTerm offsetFreeParam = (CCTerm) mConverted.pop();
+			pushResult(CCParameter.of(offsetFreeParam, mOffset));
+		}
+	}
+
 	/**
 	 * Helper class to build the intermediate CCAppTerms. Note that all these terms will be func terms.
 	 *
@@ -103,16 +140,18 @@ public BuildCCAppTerm(ApplicationTerm appTerm) {
 
 		@Override
 		public void perform() {
-			final CCTerm[] args = new CCTerm[mAppTerm.getParameters().length];
+			final CCParameter[] args = new CCParameter[mAppTerm.getParameters().length];
 			for (int i = args.length - 1; i >= 0; i--) {
 				args[i] = mConverted.pop();
 			}
 			assert mClausifier.getCCTerm(mAppTerm) == null;
-			final CCTerm ccTerm = mClausifier.getCClosure().createAppTerm(mAppTerm.getFunction(), args, mSource);
+			final CCTerm ccTerm =
+					mClausifier.getCClosure().createAppTerm(mAppTerm.getFunction(), args, mSource);
 			mClausifier.getCClosure().addTerm(ccTerm, mAppTerm);
 			mClausifier.shareCCTerm(mAppTerm, ccTerm);
 			mClausifier.addTermAxioms(mAppTerm, mSource);
-			mConverted.push(ccTerm);
+			// the application term itself is not numeric-offset; its value is the application
+			pushResult(ccTerm);
 		}
 	}
 }

SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/convert/Clausifier.java

@@ -71,6 +71,7 @@
 import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.bitvector.BvToIntUtils;
 import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ArrayTheory;
 import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCAppTerm;
+import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCParameter;
 import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm;
 import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CClosure;
 import de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.DTReverseTrigger;
@@ -221,10 +222,10 @@ public Clausifier(final Theory theory, final DPLLEngine engine, final ProofMode
 	 *            The source annotation that is used for auxiliary axioms.
 	 * @return the ccterm.
 	 */
-	public CCTerm createCCTerm(final Term term, final SourceAnnotation source) {
+	public CCParameter createCCTerm(final Term term, final SourceAnnotation source) {
 		final boolean wasRunning = mIsRunning;
 		mIsRunning = true;
-		final CCTerm ccterm = new CCTermBuilder(this, source).convert(term);
+		final CCParameter ccterm = new CCTermBuilder(this, source).convert(term);
 		mIsRunning = wasRunning;
 		if (!wasRunning) {
 			run();
@@ -261,8 +262,13 @@ public void setTermFlags(final Term term, final int newFlags) {
 	}
 
 	public void share(final CCTerm ccTerm, final LASharedTerm laTerm) {
+		// With offset equalities several terms (e.g. 2x+4y, 2x+4y+1, 2x+4y+5) map to the same offset-free CCTerm. Each
+		// of them is a distinct value, so each full-value LASharedTerm must be registered with linear arithmetic (so
+		// mbtc sees every value); but the offset-free CCTerm is shared with congruence closure only once.
 		getLASolver().addSharedTerm(laTerm);
-		getCClosure().addSharedTerm(ccTerm);
+		if (ccTerm.getSharedTerm() != ccTerm) {
+			getCClosure().addSharedTerm(ccTerm);
+		}
 	}
 
 	public void shareLATerm(final Term term, final LASharedTerm laTerm) {
@@ -284,6 +290,10 @@ public void shareCCTerm(final Term term, final CCTerm ccTerm) {
 	}
 
 	public void addTermAxioms(final Term term, final SourceAnnotation source) {
+		// Axioms are added for offset-free terms only; an offseted term (x+5) carries its constant structurally and its
+		// offset-free part (x) gets the axioms. The only callers with user terms (EqualityProxy, createEqualityProxy)
+		// normalize via getOffsetFreeTerm before calling.
+		assert getTermConstant(term).equals(Rational.ZERO) : "addTermAxioms on offseted term " + term;
 		final int termFlags = getTermFlags(term);
 		if ((termFlags & Clausifier.AUX_AXIOM_ADDED) == 0) {
 			final boolean wasRunning = mIsRunning;
@@ -293,7 +303,7 @@ public void addTermAxioms(final Term term, final SourceAnnotation source) {
 				CCTerm ccTerm = getCCTerm(term);
 				if (ccTerm == null && (needCCTerm(term) || term.getSort().isArraySort())) {
 					final CCTermBuilder cc = new CCTermBuilder(this, source);
-					ccTerm = cc.convert(term);
+					ccTerm = (CCTerm) cc.convert(term);
 				}
 
 				final ApplicationTerm at = (ApplicationTerm) term;
@@ -329,7 +339,7 @@ public void addTermAxioms(final Term term, final SourceAnnotation source) {
 					final String funcName = at.getFunction().getName();
 					final boolean isStore = funcName.equals("store");
 					final boolean isConst = funcName.equals(SMTLIBConstants.CONST);
-					mArrayTheory.notifyArray(getCCTerm(term), isStore, isConst);
+					mArrayTheory.notifyArray(ccTerm, isStore, isConst);
 				}
 
 				if (fs.isConstructor()) {
@@ -353,6 +363,15 @@ public void addTermAxioms(final Term term, final SourceAnnotation source) {
 
 			}
 			if (term.getSort().isNumericSort()) {
+				// With offset equalities the CCTerm is offset-free (value 2x+4y for a term 2x+4y+1) and the
+				// constant is carried structurally at the use sites. The LASharedTerm must then be offset-free
+				// too, so it stays value-consistent with the offset-free CCTerm: clash-slot MBTC values a member
+				// as value(rep) + offsetToRep and must not double-count the constant. Terms differing only by a
+				// constant share one offset-free CCTerm; each still registers its own offset-free LASharedTerm
+				// (same value), which is harmless and recognized as already-known by the offset-aware guards.
+				//
+				// Without offset equalities the LASharedTerm carries the full value (its constant), as before,
+				// so whole-term mbtc groups shared terms by their true value.
 				boolean needsLA = term instanceof ConstantTerm;
 				if (term instanceof ApplicationTerm) {
 					final String func = ((ApplicationTerm) term).getFunction().getName();
@@ -364,6 +383,9 @@ public void addTermAxioms(final Term term, final SourceAnnotation source) {
 					final MutableAffineTerm mat = createMutableAffinTerm(new Polynomial(term), source);
 					assert mat.getConstant().mEps == 0;
 					if (!mLATerms.containsKey(term)) {
+						// The LASharedTerm shares the term's value with linear arithmetic. The term is offset-free (see
+						// the precondition), so this stays consistent with getCCTerm and the endScope unshare loop, which
+						// look up CC nodes by the (offset-free) key.
 						shareLATerm(term, new LASharedTerm(term, mat.getSummands(), mat.getConstant().mReal));
 					}
 				}
@@ -570,13 +592,77 @@ public MutableAffineTerm toMutableAffineTerm(final Polynomial poly) {
 	}
 
 	public CCTerm getCCTerm(final Term term) {
+		// mCCTerms is keyed by offset-free terms only; an offseted term has no entry of its own (its CCParameter, with
+		// the constant as offset, is produced at build time by createCCTerm). Callers must normalize via
+		// getOffsetFreeTerm first, or use getCCParameter for a possibly offseted term.
+		assert getTermConstant(term).equals(Rational.ZERO) : "getCCTerm on offseted term " + term;
 		return mCCTerms.get(term);
 	}
 
+	/**
+	 * Get the {@link CCParameter} denoting the value of the given term: the CCTerm of the term's offset-free part plus
+	 * the term's constant. Unlike {@link #getCCTerm} this accepts terms with a constant summand. This function does not
+	 * create new terms.
+	 *
+	 * @return the value of the term, or null if no CCTerm exists for the term's offset-free part.
+	 */
+	public CCParameter getCCParameter(final Term term) {
+		final Rational constant = getTermConstant(term);
+		final CCTerm ccTerm = getCCTerm(constant.equals(Rational.ZERO) ? term : getOffsetFreeTerm(term));
+		return ccTerm == null ? null : CCParameter.of(ccTerm, constant);
+	}
+
 	public LASharedTerm getLATerm(final Term term) {
 		return mLATerms.get(term);
 	}
 
+	/**
+	 * Whether offset equalities are enabled in the congruence closure. When enabled, numeric terms are represented by
+	 * offset-free CCTerms with the constant carried as an offset.
+	 */
+	public boolean createOffsetEqualities() {
+		return getCClosure() != null && getCClosure().createOffsetEqualities();
+	}
+
+	/**
+	 * The constant offset of a numeric term, i.e. the value such that {@code term == offsetFreeTerm + constant}. Returns
+	 * {@link Rational#ZERO} when offset equalities are disabled or the term is not numeric.
+	 */
+	public Rational getTermConstant(final Term term) {
+		if (!createOffsetEqualities() || !term.getSort().isNumericSort()) {
+			return Rational.ZERO;
+		}
+		return new Polynomial(term).getConstant();
+	}
+
+	/**
+	 * Build the normalized term for {@code term + constant}. The result is a single flattened polynomial term (not a
+	 * nested {@code (+ term constant)}), so that re-parsing it as a Polynomial recovers all summands.
+	 */
+	public Term addConstantToTerm(final Term term, final Rational constant) {
+		return CCParameter.addConstant(term, constant);
+	}
+
+	/**
+	 * The offset-free part of a numeric term, i.e. the term with its constant
+	 * summand removed. Two terms that differ only by a constant (e.g.
+	 * {@code 2x+4y+1} and {@code 2x+4y+5}) yield the same canonical offset-free
+	 * term, so they share a single CCTerm. Returns the term itself when it has no
+	 * constant or offset equalities are disabled.
+	 */
+	public Term getOffsetFreeTerm(final Term term) {
+		if (!createOffsetEqualities() || !term.getSort().isNumericSort()) {
+			return term;
+		}
+		final Polynomial poly = new Polynomial(term);
+		final Rational constant = poly.getConstant();
+		if (constant.equals(Rational.ZERO)) {
+			return term;
+		}
+		poly.add(constant.negate());
+		return mCompiler.unifyPolynomial(poly, term.getSort());
+	}
+
 	public ILiteral getILiteral(final Term term) {
 		return mLiterals.get(term);
 	}
@@ -1296,8 +1382,13 @@ public EqualityProxy createEqualityProxy(final Term lhs, final Term rhs, final S
 		if (sort.getName().equals("Int") && !diff.getConstant().isIntegral()) {
 			return EqualityProxy.getFalseProxy();
 		}
-		addTermAxioms(lhs, source);
-		addTermAxioms(rhs, source);
+		// The proxy works on the offset-free sides plus the offset (value(offLhs) == value(offRhs) + offset). The
+		// offset is the difference of the two sides' constants.
+		final Term offLhs = getOffsetFreeTerm(lhs);
+		final Term offRhs = getOffsetFreeTerm(rhs);
+		final Rational offset = getTermConstant(rhs).sub(getTermConstant(lhs));
+		addTermAxioms(offLhs, source);
+		addTermAxioms(offRhs, source);
 		// we cannot really normalize the sign of the term. Try both signs.
 		EqualityProxy eqForm = mEqualities.get(diff);
 		if (eqForm != null) {
@@ -1308,7 +1399,7 @@ public EqualityProxy createEqualityProxy(final Term lhs, final Term rhs, final S
 		if (eqForm != null) {
 			return eqForm;
 		}
-		eqForm = new EqualityProxy(this, lhs, rhs);
+		eqForm = new EqualityProxy(this, offLhs, offRhs, offset);
 		mEqualities.put(diff, eqForm);
 		return eqForm;
 	}