();
- }
-
- public abstract Sort getResultSort(
- String[] indices, Sort[] paramSorts, Sort resultSort);
-
- public int getFlags(String[] indices, Sort[] paramSorts, Sort result) {
- return FunctionSymbol.INTERNAL;
- }
-
- private static boolean isReal(Sort[] sorts) {
- for (final Sort s : sorts) {
- if (s.getRealSort() != s) {
- return false;
- }
- }
- return true;
- }
-
- public Term getDefinition(TermVariable[] tvs, Sort resultSort) { // NOPMD
- return null;
- }
-
- public FunctionSymbol getFunctionWithResult(
- Theory theory, String[] indices, Sort[] paramSorts,
- Sort resultSort) {
- assert isReal(paramSorts);
- final int flags = getFlags(indices, paramSorts, resultSort);
- if ((flags & (FunctionSymbol.ASSOCMASK)) != 0) {
- if (paramSorts.length < 2) {
- return null;
- }
- final Sort[] realParams = new Sort[] {
- paramSorts[0], paramSorts[paramSorts.length - 1]
- };
- final Sort otherSort =
- (flags & (FunctionSymbol.ASSOCMASK)) == FunctionSymbol.LEFTASSOC
- ? realParams[1] : realParams[0];
- for (int i = 1; i < paramSorts.length - 1; i++) {
- if (paramSorts[i] != otherSort) {
- return null;
- }
- }
- paramSorts = realParams;
- }
- if (((flags & (FunctionSymbol.RETURNOVERLOAD)) == 0)
- != (resultSort == null)) {
- /* According to standard the return type must be given
- * if and only if the function is overloaded on the return type.
- */
- return null;
- }
- final int hash = Arrays.hashCode(indices)
- ^ Arrays.hashCode(paramSorts)
- ^ (resultSort == null ? 0 : resultSort.hashCode());
- for (final FunctionSymbol func : mInstances.iterateHashCode(hash)) {
- if (Arrays.equals(func.mIndices, indices)
- && Arrays.equals(func.mParamSort, paramSorts)
- && (resultSort == null
- || func.mReturnSort == resultSort)) {
- return func;
- }
- }
-
- resultSort = getResultSort(indices, paramSorts, resultSort);
- if (resultSort == null) {
- return null;
- }
-
- TermVariable[] defVars = new TermVariable[paramSorts.length];
- for (int i = 0; i < paramSorts.length; i++) {
- defVars[i] = theory.createTermVariable("x" + i, paramSorts[i]);
- }
- Term definition;
- if (((flags & (FunctionSymbol.RETURNOVERLOAD)) != 0)// NOPMD
- && resultSort != resultSort.getRealSort()) {
- final FunctionSymbol realFunc =
- getFunctionWithResult(theory, indices, paramSorts,
- resultSort.getRealSort());
- definition = theory.term(realFunc, defVars);
- } else {
- definition = getDefinition(defVars, resultSort);
- }
- if (definition == null) {
- defVars = null;
- }
- final FunctionSymbol func = new FunctionSymbol(
- mFuncName, indices, paramSorts, resultSort,
- defVars, definition, flags);
- mInstances.put(hash, func);
- return func;
- }
-
- @Override
- public String toString() {
- return mFuncName;
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/INonSolverScript.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/INonSolverScript.java
deleted file mode 100644
index 2bdff8aa98d..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/INonSolverScript.java
+++ /dev/null
@@ -1,16 +0,0 @@
-package de.uni_freiburg.informatik.ultimate.logic;
-
-/**
- * Empty interface that can be used to mark subclasses of {@link Script} that cannot answer check-sat queries. (E.g.
- * classes that are only used for building {@link Term}s during parsing.)
- *
- * Note that this class is a symptom of an architectural problem: Some subclasses of Script are used as an interface to
- * an actual SMT solver ({@link SMTInterpol}, {@link Scriptor}), other subclasses are used only for parsing and
- * building {@link Term}s).
- * Once the Script class is split according to these functionalities, this interface should become obsolete.
- *
- * @author Alexander Nutz (nutz@informatik.uni-freiburg.de)
- */
-public interface INonSolverScript {
-
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/IRAConstantFormatter.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/IRAConstantFormatter.java
deleted file mode 100644
index 7fe6e8415e1..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/IRAConstantFormatter.java
+++ /dev/null
@@ -1,52 +0,0 @@
-/*
- * Copyright (C) 2013 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see mInstances = new UnifyHash<>();
-
- /**
- * Create an IRA wrapper function for name for the given parameter sorts. This is a new function symbol whose
- * definition casts all integer parameters to real parameters using the {@code to_real} function. If the parameter
- * count does not match, or if not all parameters are real or integer this returns null.
- *
- * For associative functions this creates a wrapper for every used sequence of sorts. E.g., it may create the
- * function {@code (define-fun + ((Real a) (Int b) (Real c)) (+ a (to_real b) c))}.
- *
- * @param theory
- * the underlying theory.
- * @param name
- * the unwrapped function symbol. It is assumed that it takes two real parameters except for "ite".
- * @param indices
- * optional indices, null for no indices.
- * @param paramSorts
- * the parameter sorts for the wrapper function.
- * @param resultType
- * the result type specified by SMTLIB {@code (as ..)}; null if no result type specified.
- * @return null if an error occured, otherwise the wrapping function symbol.
- */
- public FunctionSymbol createWrapper(Theory theory, String name, final String[] indices, Sort[] paramSorts,
- final Sort resultType) {
- final Sort realSort = theory.getRealSort();
- final Sort intSort = theory.getNumericSort();
- final FunctionSymbol fsym;
- /*
- * First check that paramSorts is correct.
- */
- if (name.equals(SMTLIBConstants.ITE) && indices == null) {
- /* ite expects a bool and two int/real mixed arguments. */
- if (paramSorts[0] != theory.getBooleanSort()) {
- return null;
- }
- if ((paramSorts[1] != intSort || paramSorts[2] != realSort)
- && (paramSorts[1] != realSort || paramSorts[2] != intSort)) {
- return null;
- }
- /* Create the base function symbol. */
- fsym = theory.getFunctionWithResult(name, indices, resultType,
- new Sort[] { theory.getBooleanSort(), realSort, realSort });
- } else {
- /* Else all arguments must be Int or Real. */
- boolean hasInt = false;
- boolean hasReal = false;
- for (int i = 0; i < paramSorts.length; i++) {
- if (paramSorts[i] == intSort) {
- hasInt = true;
- } else if (paramSorts[i] == realSort) {
- hasReal = true;
- } else {
- return null;
- }
- }
- /* At least one must be Int and -- except for division -- one must be Real. */
- if (!hasInt || (!hasReal && !name.equals(SMTLIBConstants.DIVIDE))) {
- return null;
- }
- /* Create the base function symbol. */
- fsym = theory.getFunctionWithResult(name, indices, resultType, realSort, realSort);
- /* Check if the number of parameters is two or the symbol is associative. */
- if (paramSorts.length != 2 && (fsym.mFlags & FunctionSymbol.ASSOCMASK) == 0) {
- throw new SMTLIBException("Function " + name + " is not associative.");
- }
- }
-
- /* Check if we already created a wrapper and return it. */
- final int hash = fsym.hashCode() ^ Arrays.hashCode(paramSorts);
- for (final FunctionSymbol func : mInstances.iterateHashCode(hash)) {
- if (((ApplicationTerm) func.getDefinition()).getFunction() == fsym
- && Arrays.equals(func.mParamSort, paramSorts)) {
- return func;
- }
- }
-
- /* Create the wrapping definition */
- final TermVariable[] defVars = new TermVariable[paramSorts.length];
- final Term[] wrappedArgs = new Term[paramSorts.length];
- for (int i = 0; i < paramSorts.length; i++) {
- defVars[i] = theory.createTermVariable("x" + i, paramSorts[i]);
- wrappedArgs[i] = paramSorts[i] == intSort ? theory.term("to_real", defVars[i]) : defVars[i];
- }
- final Term definition = theory.term(fsym, wrappedArgs);
- assert definition != null;
-
- /* Create the function symbol */
- final FunctionSymbol wrapper = new FunctionSymbol(fsym.getName(), fsym.getIndices(), paramSorts, fsym.getReturnSort(),
- defVars, definition, (fsym.mFlags & ~FunctionSymbol.ASSOCMASK));
- mInstances.put(hash, wrapper);
- return wrapper;
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/IsConstructorFactory.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/IsConstructorFactory.java
deleted file mode 100644
index a1232b064fa..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/IsConstructorFactory.java
+++ /dev/null
@@ -1,28 +0,0 @@
-package de.uni_freiburg.informatik.ultimate.logic;
-
-public class IsConstructorFactory extends FunctionSymbolFactory {
-
- public IsConstructorFactory() {
- super(SMTLIBConstants.IS);
- }
-
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices.length != 1 || paramSorts.length != 1) {
- return null;
- }
-
- if (!paramSorts[0].getSortSymbol().isDatatype()) {
- return null;
- }
-
- final DataType datatype = (DataType) paramSorts[0].getSortSymbol();
- for (int i = 0; i < datatype.getConstructors().length; i++) {
- if (indices[0].equals(datatype.getConstructors()[i].getName())) {
- return paramSorts[0].getTheory().getBooleanSort();
- }
- }
- return null;
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/LambdaTerm.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/LambdaTerm.java
deleted file mode 100644
index 65bf231543c..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/LambdaTerm.java
+++ /dev/null
@@ -1,95 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see
- * (lambda ((var_1 sort_1) ... (var_n sort_n)) term)
- *
- *
- * @author hoenicke
- */
-public class LambdaTerm extends Term {
- private final TermVariable[] mVariables;
- private final Term mSubTerm;
- private final Sort mSort;
-
- LambdaTerm(final TermVariable[] vars, final Term subterm, final int hash) {
- super(hash);
- mVariables = vars;
- mSubTerm = subterm;
- Sort mySort = subterm.getSort();
- for (int i = vars.length - 1; i >= 0; i--) {
- mySort = mySort.getTheory().getSort(SMTLIBConstants.FUNC, vars[i].getSort(), mySort);
- }
- mSort = mySort;
- }
-
- /**
- * Get the quantified variables.
- * @return the variables
- */
- public TermVariable[] getVariables() {
- return mVariables;
- }
-
- /**
- * Get the formula under the quantifier.
- * @return the sub-formula.
- */
- public Term getSubterm() {
- return mSubTerm;
- }
-
- @Override
- public Sort getSort() {
- return mSort;
- }
-
- public static final int hashLambda(final TermVariable[] vars, final Term f) {
- return HashUtils.hashJenkins(f.hashCode(), (Object[]) vars);
- }
-
- @Override
- public void toStringHelper(final ArrayDeque mTodo) {
- // Add subterm to stack.
- mTodo.addLast(")");
- mTodo.addLast(getSubterm());
- mTodo.addLast(")) ");
-
- // Add variables
- final TermVariable[] vars = getVariables();
- for (int i = vars.length - 1; i > 0; i--) {
- mTodo.addLast(vars[i].getSort());
- mTodo.addLast(") (" + vars[i] + " ");
- }
- mTodo.addLast(vars[0].getSort());
-
- // Print out the quantifier.
- mTodo.addLast("(lambda ((" + vars[0] + " ");
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/LetTerm.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/LetTerm.java
deleted file mode 100644
index 64a4157065a..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/LetTerm.java
+++ /dev/null
@@ -1,101 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see
- * (let ((var_0 val_0) ... (var_n val_n)) ...)
- *
- *
- * A let term is created by {@link Script#let(TermVariable[], Term[], Term)}.
- *
- * @author hoenicke
- */
-public class LetTerm extends Term {
- private final TermVariable[] mVariables;
- private final Term[] mValues;
- private final Term mSubterm;
- private final Sort mSort;
-
- /**
- * @return The variables
- */
- public TermVariable[] getVariables() {
- return mVariables;
- }
-
- /**
- * @return The values
- */
- public Term[] getValues() {
- return mValues;
- }
-
- /**
- * @return The subformula
- */
- public Term getSubTerm() {
- return mSubterm;
- }
-
- LetTerm(TermVariable[] vars, Term[] vals, Term t, int hash) {
- super(hash);
- mVariables = vars;
- mValues = vals;
- mSubterm = t;
- mSort = t.getSort();
- }
-
- @Override
- public Sort getSort() {
- return mSort;
- }
-
- public static final int hashLet(
- TermVariable[] vars, Term[] values, Term subform) {
-// return Arrays.hashCode(vars) ^ Arrays.hashCode(values) ^
-// subform.hashCode();
- return HashUtils.hashJenkins(
- HashUtils.hashJenkins(subform.hashCode(), (Object[]) values),
- (Object[]) vars);
- }
-
- @Override
- public void toStringHelper(ArrayDeque mTodo) {
- // Add subterm to stack.
- mTodo.addLast(")");
- mTodo.addLast(getSubTerm());
- mTodo.addLast(")) ");
- // Add assigned values to stack
- final TermVariable[] vars = getVariables();
- final Term[] values = getValues();
- for (int i = values.length - 1; i > 0; i--) {
- mTodo.addLast(values[i]);
- mTodo.addLast(") (" + vars[i].toString() + " ");
- }
- mTodo.addLast(values[0]);
- mTodo.addLast("(let ((" + vars[0].toString() + " ");
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/LoggingScript.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/LoggingScript.java
deleted file mode 100644
index b8ec0a4b926..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/LoggingScript.java
+++ /dev/null
@@ -1,562 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see null if cse should not be
- * performed.
- */
- private final FormulaLet mLetter;
-
- /**
- * Create a new script logging the commands by the user. Most commands are not supported, e.g., checkSat always
- * returns unknown. Furthermore, common subexpression elimination is not used in the output.
- *
- * @param file
- * The name of the logging file (should end in .smt2).
- * @param autoFlush
- * Automatically flush the output stream after every command.
- * @throws IOException
- * IOException If an I/O error has occurred.
- */
- public LoggingScript(final String file, final boolean autoFlush) throws IOException {
- this(new NoopScript(), file, autoFlush);
- }
-
- /**
- * Create a new script logging the commands by the user. Most commands are not supported, e.g., checkSat always
- * returns unknown. This constructor can be used to set up logging using common subexpression elimination.
- *
- * @param file
- * The name of the logging file (should end in .smt2).
- * @param autoFlush
- * Automatically flush the output stream after every command.
- * @param useCSE
- * Use common subexpression elimination in output (introduces let terms)
- * @throws IOException
- * IOException If an I/O error has occurred.
- */
- public LoggingScript(final String file, final boolean autoFlush, final boolean useCSE) throws IOException {
- this(new NoopScript(), file, autoFlush, useCSE);
- }
-
- /**
- * Create a new script logging the interaction between the user and the wrapped script into a file. This constructor
- * sets up logging to not use common subexpression elimination.
- *
- * @param script
- * The wrapped script.
- * @param file
- * The name of the logging file (should end in .smt2).
- * @param autoFlush
- * Automatically flush the output stream after every command.
- * @throws IOException
- * IOException If an I/O error has occurred.
- */
- public LoggingScript(final Script script, final String file, final boolean autoFlush) throws IOException {
- this(script, file, autoFlush, false);
- }
-
- /**
- * Create a new script logging the interaction between the user and the wrapped script into a file. This constructor
- * can be used to set up logging using common subexpression elimination.
- *
- * @param script
- * The wrapped script.
- * @param file
- * The name of the logging file (should end in .smt2).
- * @param autoFlush
- * Automatically flush the output stream after every command.
- * @param useCSE
- * Use common subexpression elimination in output (introduces let terms)
- * @throws IOException
- * IOException If an I/O error has occurred.
- */
- public LoggingScript(final Script script, final String file, final boolean autoFlush, final boolean useCSE)
- throws IOException {
- super(script);
- OutputStream out;
- if (file.equals("")) {
- out = System.out;
- } else if (file.equals("")) {
- out = System.err;
- } else {
- out = new FileOutputStream(file);
- if (file.endsWith(".gz")) {
- out = new GZIPOutputStream(out);
- }
- }
- mPw = new PrintWriter(new BufferedWriter(new OutputStreamWriter(out)), autoFlush);
- mLetter = useCSE ? new FormulaLet() : null;
- }
-
- private final Term formatTerm(final Term input) {
- return mLetter == null ? input : new FormulaLet().let(input);
- }
-
- @Override
- public void setLogic(final String logic) throws UnsupportedOperationException, SMTLIBException {
- mPw.println("(set-logic " + logic + ")");
- super.setLogic(logic);
- }
-
- @Override
- public void setLogic(final Logics logic) throws UnsupportedOperationException, SMTLIBException {
- mPw.println("(set-logic " + logic.name() + ")");
- super.setLogic(logic);
- }
-
- @Override
- public void setOption(final String opt, final Object value) throws UnsupportedOperationException, SMTLIBException {
- mPw.print("(set-option ");
- mPw.print(opt);
- mPw.print(' ');
- mPw.print(PrintTerm.quoteObjectIfString(value));
- mPw.println(")");
- super.setOption(opt, value);
- }
-
- @Override
- public void setInfo(final String info, final Object value) {
- mPw.print("(set-info ");
- mPw.print(info);
- mPw.print(' ');
- mPw.print(PrintTerm.quoteObjectIfString(value));
- mPw.println(")");
- super.setInfo(info, value);
- }
-
- @Override
- public FunctionSymbol getFunctionSymbol(final String constructor) {
- return mScript.getFunctionSymbol(constructor);
- }
-
- @Override
- public void declareSort(final String sort, final int arity) throws SMTLIBException {
- mPw.print("(declare-sort ");
- mPw.print(PrintTerm.quoteIdentifier(sort));
- mPw.print(' ');
- mPw.print(arity);
- mPw.println(")");
- super.declareSort(sort, arity);
- }
-
- @Override
- public void defineSort(final String sort, final Sort[] sortParams, final Sort definition) throws SMTLIBException {
- mPw.print("(define-sort ");
- mPw.print(PrintTerm.quoteIdentifier(sort));
- mPw.print(" (");
- String sep = "";
- for (final Sort p : sortParams) {
- mPw.print(sep);
- mTermPrinter.append(mPw, p);
- sep = " ";
- }
- mPw.print(") ");
- mTermPrinter.append(mPw, definition);
- mPw.println(")");
- super.defineSort(sort, sortParams, definition);
- }
-
- @Override
- public void declareDatatype(final DataType datatype, final DataType.Constructor[] constrs) throws SMTLIBException {
- assert datatype.mNumParams == 0;
- mPw.print("(declare-datatype ");
- mPw.print(PrintTerm.quoteIdentifier(datatype.getName()));
- mPw.print(" (");
- for (int j = 0; j < constrs.length; j++) {
- mPw.print("(");
- mPw.print(PrintTerm.quoteIdentifier(constrs[j].getName()));
- for (int k = 0; k < constrs[j].getArgumentSorts().length; k++) {
- mPw.print(" ");
- mPw.print("(");
- mPw.print(PrintTerm.quoteIdentifier(constrs[j].getSelectors()[k]));
- mPw.print(" ");
- mPw.print(constrs[j].getArgumentSorts()[k]);
- mPw.print(")");
- }
- mPw.print(j != constrs.length - 1 ? ") " : ")");
- }
- mPw.println("))");
- super.declareDatatype(datatype, constrs);
- }
-
- @Override
- public void declareDatatypes(final DataType[] datatypes, final DataType.Constructor[][] constrs,
- final Sort[][] sortParams) throws SMTLIBException {
- assert datatypes.length == constrs.length && datatypes.length == sortParams.length;
- mPw.print("(declare-datatypes (");
- String sep1 = "";
- for (final DataType datatype : datatypes) {
- mPw.print(sep1);
- sep1 = " ";
- mPw.print("(");
- mPw.print(PrintTerm.quoteIdentifier(datatype.getName()));
- mPw.print(" ");
- mPw.print(datatype.mNumParams);
- mPw.print(")");
- }
- mPw.print(") (");
- String sep2 = "";
- for (int i = 0; i < constrs.length; i++) {
- mPw.print(sep2);
- sep2 = " ";
- if (sortParams[i] != null) {
- mPw.print("(par (");
- String sep3 = "";
- for (final Sort param : sortParams[i]) {
- mPw.print(sep3);
- sep3 = " ";
- mPw.print(param);
- }
- mPw.print(") ");
- }
- mPw.print("(");
- String sep4 = "";
- for (final DataType.Constructor constructor : constrs[i]) {
- mPw.print(sep4);
- sep4 = " ";
- mPw.print("(");
- mPw.print(PrintTerm.quoteIdentifier(constructor.getName()));
- for (int j = 0; j < constructor.getArgumentSorts().length; j++) {
- mPw.print(" ");
- mPw.print("(");
- mPw.print(PrintTerm.quoteIdentifier(constructor.getSelectors()[j]));
- mPw.print(" ");
- mPw.print(constructor.getArgumentSorts()[j]);
- mPw.print(")");
- }
- mPw.print(")");
- }
- mPw.print(")");
- if (sortParams[i] != null) {
- mPw.print(")");
- }
- }
- mPw.println("))");
- super.declareDatatypes(datatypes, constrs, sortParams);
- }
-
- @Override
- public void declareFun(final String fun, final Sort[] paramSorts, final Sort resultSort) throws SMTLIBException {
- mPw.print("(declare-fun ");
- mPw.print(PrintTerm.quoteIdentifier(fun));
- mPw.print(" (");
- String sep = "";
- for (final Sort p : paramSorts) {
- mPw.print(sep);
- mTermPrinter.append(mPw, p);
- sep = " ";
- }
- mPw.print(") ");
- mTermPrinter.append(mPw, resultSort);
- mPw.println(")");
- super.declareFun(fun, paramSorts, resultSort);
- }
-
- @Override
- public void defineFun(final String fun, final TermVariable[] params, final Sort resultSort, final Term definition)
- throws SMTLIBException {
- mPw.print("(define-fun ");
- mPw.print(PrintTerm.quoteIdentifier(fun));
- mPw.print(" (");
- String sep = "(";
- for (final TermVariable t : params) {
- mPw.print(sep);
- mPw.print(t);
- mPw.print(' ');
- mTermPrinter.append(mPw, t.getSort());
- mPw.print(')');
- sep = " (";
- }
- mPw.print(") ");
- mTermPrinter.append(mPw, resultSort);
- mPw.print(' ');
- mTermPrinter.append(mPw, formatTerm(definition));
- mPw.println(")");
- super.defineFun(fun, params, resultSort, definition);
- }
-
- @Override
- public void push(final int levels) throws SMTLIBException {
- mPw.println("(push " + levels + ")");
- super.push(levels);
- }
-
- @Override
- public void pop(final int levels) throws SMTLIBException {
- mPw.println("(pop " + levels + ")");
- super.pop(levels);
- }
-
- @Override
- public LBool assertTerm(final Term term) throws SMTLIBException {
- mPw.print("(assert ");
- mTermPrinter.append(mPw, formatTerm(term));
- mPw.println(")");
- return super.assertTerm(term);
- }
-
- @Override
- public LBool checkSat() throws SMTLIBException {
- mPw.println("(check-sat)");
- return super.checkSat();
- }
-
- @Override
- public LBool checkSatAssuming(final Term... assumptions) throws SMTLIBException {
- mPw.print("(check-sat-assuming (");
- String sep = "";
- for (final Term t : assumptions) {
- mPw.print(sep);
- mTermPrinter.append(mPw, formatTerm(t));
- sep = " ";
- }
- mPw.println("))");
- return super.checkSatAssuming(assumptions);
- }
-
- @Override
- public Term[] getAssertions() throws SMTLIBException {
- mPw.println("(get-assertions)");
- return super.getAssertions();
- }
-
- @Override
- public Term getProof() throws SMTLIBException, UnsupportedOperationException {
- mPw.println("(get-proof)");
- return super.getProof();
- }
-
- @Override
- public Term[] getUnsatCore() throws SMTLIBException, UnsupportedOperationException {
- mPw.println("(get-unsat-core)");
- return super.getUnsatCore();
- }
-
- @Override
- public Map getValue(final Term[] terms) throws SMTLIBException, UnsupportedOperationException {
- mPw.print("(get-value (");
- String sep = "";
- for (final Term t : terms) {
- mPw.print(sep);
- mTermPrinter.append(mPw, formatTerm(t));
- sep = " ";
- }
- mPw.println("))");
- return super.getValue(terms);
- }
-
- @Override
- public Assignments getAssignment() throws SMTLIBException, UnsupportedOperationException {
- mPw.println("(get-assignment)");
- return super.getAssignment();
- }
-
- @Override
- public Object getOption(final String opt) throws UnsupportedOperationException {
- mPw.println("(get-option " + opt + ")");
- return super.getOption(opt);
- }
-
- @Override
- public Object getInfo(final String info) throws UnsupportedOperationException {
- mPw.println("(get-info " + info + ")");
- return super.getInfo(info);
- }
-
- @Override
- public Term simplify(final Term term) throws SMTLIBException {
- mPw.print("(simplify ");
- mTermPrinter.append(mPw, term);
- mPw.println(")");
- return super.simplify(term);
- }
-
- @Override
- public void reset() {
- mPw.println("(reset)");
- super.reset();
- }
-
- @Override
- public Term[] getInterpolants(final Term[] partition) throws SMTLIBException, UnsupportedOperationException {
- mPw.print("(get-interpolants");
- for (final Term t : partition) {
- mPw.print(' ');
- mTermPrinter.append(mPw, t);
- }
- mPw.println(')');
- return super.getInterpolants(partition);
- }
-
- private void printInterpolantQuery(final Term[] partition, final int[] startOfSubtree) {
- // Grammar for tree interpolation:
- // tree ::= children term
- // children ::= tree ('(' tree ')')*
- //
- // So the an open parenthesis marks the beginning of a new sibling.
- // example: parent c, children a, b.
- // partitions: [a,b,c]
- // startofSubtree: [0,1,0]
- // textual representation: a (b) c
- mTermPrinter.append(mPw, partition[0]);
- for (int i = 1; i < partition.length; ++i) {
- int prevStart = startOfSubtree[i - 1];
- while (startOfSubtree[i] < prevStart) {
- mPw.print(')');
- prevStart = startOfSubtree[prevStart - 1];
- }
- mPw.print(' ');
- if (startOfSubtree[i] == i) {
- mPw.print('(');
- }
- mTermPrinter.append(mPw, partition[i]);
- }
- }
-
- @Override
- public Term[] getInterpolants(final Term[] partition, final int[] startOfSubtree)
- throws SMTLIBException, UnsupportedOperationException {
- mPw.print("(get-interpolants ");
- printInterpolantQuery(partition, startOfSubtree);
- mPw.println(')');
- return super.getInterpolants(partition, startOfSubtree);
- }
-
- @Override
- public Term[] getInterpolants(final Term[] partition, final int[] startOfSubtree, final Term proofTree)
- throws SMTLIBException, UnsupportedOperationException {
- mPw.print("(get-interpolants ");
- printInterpolantQuery(partition, startOfSubtree);
- mPw.print(" :proof ");
- mTermPrinter.append(mPw, proofTree);
- mPw.println(')');
- return super.getInterpolants(partition, startOfSubtree);
- }
-
- @Override
- public void exit() {
- mPw.println("(exit)");
- mPw.flush();
- mPw.close();
- super.exit();
- }
-
- @Override
- public Model getModel() throws SMTLIBException, UnsupportedOperationException {
- mPw.println("(get-model)");
- return super.getModel();
- }
-
- @Override
- public Iterable checkAllsat(final Term[] predicates) throws SMTLIBException, UnsupportedOperationException {
- final PrintTerm pt = new PrintTerm();
- mPw.print("(check-allsat (");
- String spacer = "";
- for (final Term p : predicates) {
- mPw.print(spacer);
- pt.append(mPw, p);
- spacer = " ";
- }
- mPw.println("))");
- return super.checkAllsat(predicates);
- }
-
- @Override
- public Term[] findImpliedEquality(final Term[] x, final Term[] y) {
- final PrintTerm pt = new PrintTerm();
- mPw.print("(find-implied-equality (");
- String spacer = "";
- for (final Term p : x) {
- mPw.print(spacer);
- pt.append(mPw, p);
- spacer = " ";
- }
- mPw.print(") (");
- spacer = "";
- for (final Term p : x) {
- mPw.print(spacer);
- pt.append(mPw, p);
- spacer = " ";
- }
- mPw.println("))");
- return super.findImpliedEquality(x, y);
- }
-
- @Override
- public QuotedObject echo(final QuotedObject msg) {
- mPw.print("(echo ");
- mPw.print(msg);
- mPw.println(')');
- return super.echo(msg);
- }
-
- /**
- * Write a comment to the generated SMTLIB dump file. Note that this function is only available in the LoggingScript
- * and not in the interface {@link Script} since it only makes sense for logging and not for solving.
- *
- * @param comment
- * The comment to write to the dump file.
- */
- public void comment(final String comment) {
- mPw.print("; ");
- mPw.println(comment);
- }
-
- @Override
- public void resetAssertions() {
- mPw.println("(reset-assertions)");
- super.resetAssertions();
- }
-
- @Override
- public Term[] getUnsatAssumptions() throws SMTLIBException, UnsupportedOperationException {
- mPw.println("(get-unsat-assumptions)");
- return super.getUnsatAssumptions();
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Logics.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Logics.java
deleted file mode 100644
index 3686f27e8a2..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Logics.java
+++ /dev/null
@@ -1,275 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see true if and only if mixed arithmetic can be used in
- * this logic.
- */
- public boolean isIRA() {
- return (mFeatures & (Features.IA + Features.RA))
- == (Features.IA + Features.RA);
- }
- /**
- * Does this logic support uninterpreted functions and sorts?
- * @return true if and only if the logic supports uninterpreted
- * functions and sorts.
- */
- public boolean isUF() {
- return (mFeatures & Features.UF) != 0;
- }
- /**
- * Does this logic support arrays?
- * @return true if and only if this logic supports arrays.
- */
- public boolean isArray() {
- return (mFeatures & Features.AX) != 0;
- }
- /**
- * Does this logic support bit vectors?
- * @return true if and only if this logic supports bit vectors.
- */
- public boolean isBitVector() {
- return (mFeatures & Features.BV) != 0;
- }
- /**
- * Does this logic support quantifiers?
- * @return true if and only if quantified formulas can be build
- * in this logic.
- */
- public boolean isQuantified() {
- return (mFeatures & Features.QU) != 0;
- }
-
- /**
- * Does this logic support arithmetic operators?
- * @return true if and only if this logic supports arithmetic
- */
- public boolean isArithmetic() {
- return (mFeatures & (Features.NA + Features.LA + Features.DL)) != 0;
- }
-
- /**
- * Does this logic support difference logic?
- * @return true if and only if this logic support difference
- * logic;
- * it returns false for linear arithmetic and non-linear arithmetic logics.
- */
- public boolean isDifferenceLogic() {
- return (mFeatures & Features.DL) != 0;
- }
- /**
- * Is this logic restricted to linear arithmetic?
- * @return true if and only if this logic is restricted to linear arithmetic.
- */
- public boolean isLinearArithmetic() {
- return (mFeatures & (Features.LA | Features.DL)) != 0;
- }
- /**
- * Does this logic support non-linear arithmetic?
- * @return true if and only if this logic support non-linear
- * logic.
- */
- public boolean isNonLinearArithmetic() {
- return (mFeatures & Features.NA) != 0;
- }
- /**
- * Does this logic have integers?
- * @return true if and only if this logic has integers.
- */
- public boolean hasIntegers() {
- return (mFeatures & Features.IA) != 0;
- }
- /**
- * Does this logic have real numbers?
- * @return true if and only if this logic has reals.
- */
- public boolean hasReals() {
- return (mFeatures & Features.RA) != 0;
- }
- /**
- * Does this logic support floating point arithmetic?
- * @return true if and only if this logic supports floating
- * point arithmetic.
- */
- public boolean isFloatingPoint() {
- return (mFeatures & Features.FP) != 0;
- }
- /**
- * Does this logic support datatypes?
- * @return true if and only if this logic supports datatypes.
- */
- public boolean isDatatype() {
- return (mFeatures & Features.DT) != 0;
- }
- /**
- * Does this logic support strings?
- * @return true if and only if this logic supports strings.
- */
- public boolean isString() {
- return (mFeatures & Features.S) != 0;
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/MatchTerm.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/MatchTerm.java
deleted file mode 100644
index a89997a826b..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/MatchTerm.java
+++ /dev/null
@@ -1,102 +0,0 @@
-/*
- * Copyright (C) 2018 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see
- * (match t (((c_1 v_11.. v1m) t_1) ... ((c_n v_n1.. vnm) t_m)))
- *
- *
- * @author Jochen Hoenicke
- */
-public class MatchTerm extends Term {
- private final Term mDataTerm;
- private final TermVariable[][] mVariables;
- private final Term mCases[];
- private final DataType.Constructor[] mConstructors;
-
- MatchTerm(final int hash, final Term dataArg, final TermVariable[][] vars, final Term[] cases,
- final DataType.Constructor[] constructors) {
- super(hash);
- mDataTerm = dataArg;
- mVariables = vars;
- mCases = cases;
- mConstructors = constructors;
- }
-
- @Override
- public Sort getSort() {
- return mCases[0].getSort();
- }
-
- public Term getDataTerm() {
- return mDataTerm;
- }
-
- public DataType.Constructor[] getConstructors() {
- return mConstructors;
- }
-
- public TermVariable[][] getVariables() {
- return mVariables;
- }
-
- public Term[] getCases() {
- return mCases;
- }
-
- public static final int hashMatch(final Term dataArg, final TermVariable[][] vars, final Term[] cases) {
- return HashUtils.hashJenkins(dataArg.hashCode(), (Object[]) cases);
- }
-
- @Override
- public void toStringHelper(final ArrayDeque mTodo) {
- // Add subterm to stack.
- mTodo.addLast("))");
- for (int i = mCases.length - 1; i >= 0; i--) {
- mTodo.addLast(")");
- mTodo.addLast(mCases[i]);
- if (mConstructors[i] == null) {
- mTodo.addLast(" ");
- mTodo.addLast(mVariables[i][0]);
- } else if (mVariables[i].length > 0) {
- mTodo.addLast(") ");
- for (int j = mVariables[i].length - 1; j >= 0; j--) {
- mTodo.addLast(mVariables[i][j]);
- mTodo.addLast(" ");
- }
- mTodo.addLast(mConstructors[i].getName());
- mTodo.addLast("(");
- } else {
- mTodo.addLast(" ");
- mTodo.addLast(mConstructors[i].getName());
- }
- mTodo.addLast(i > 0 ? " (" : "(");
- }
- mTodo.addLast(" (");
- mTodo.addLast(mDataTerm);
- mTodo.addLast("(match ");
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Model.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Model.java
deleted file mode 100644
index 3c70328a22c..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Model.java
+++ /dev/null
@@ -1,81 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see evaluate(Term[] input);
-
- /**
- * Get the set of function symbols for which the model defines the value. These is the set of uninterpreted function
- * symbols.
- *
- * @return The set of function symbols.
- */
- public Set getDefinedFunctions();
-
- /**
- * Get the definition of a function. This is a term that can be used as last parameter in a
- *
- *
- * (define-fun ...)
- *
- *
- * command.
- *
- * @param func
- * the name of the function
- * @param args
- * the variables that should be used in the returned term to refer to the arguments. Their sort must
- * match the function arguments of the function.
- * @return The defining term.
- */
- public Term getFunctionDefinition(String func, TermVariable[] args);
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/MutableRational.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/MutableRational.java
deleted file mode 100644
index 20a1ac1d961..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/MutableRational.java
+++ /dev/null
@@ -1,532 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see {
- int mNum;
- int mDenom;
- BigInteger mBignum;
- BigInteger mBigdenom;
-
- /**
- * Create a new rational representing num/denom.
- * @param num the numerator.
- * @param denom the denominator.
- */
- public MutableRational(int num, int denom) {
- setValue(num, denom);
- }
-
- /**
- * Create a new rational representing num/denom.
- * @param num the numerator.
- * @param denom the denominator.
- */
- public MutableRational(BigInteger num, BigInteger denom) {
- mBignum = num;
- mBigdenom = denom;
- normalize();
- }
-
- /**
- * Create a new mutable rational from a rational.
- * @param r the rational.
- */
- public MutableRational(Rational r) {
- mNum = r.mNum;
- mDenom = r.mDenom;
- if (r instanceof Rational.BigRational) {
- mBignum = r.numerator();
- mBigdenom = r.denominator();
- }
- }
-
- /**
- * Create a new copy of a mutable rational.
- * @param r the original rational.
- */
- public MutableRational(MutableRational r) {
- mNum = r.mNum;
- mDenom = r.mDenom;
- mBignum = r.mBignum;
- mBigdenom = r.mBigdenom;
- }
-
- /**
- * Set the value of this rational to value.
- * @param value the value to set to.
- */
- public void setValue(Rational value) {
- mNum = value.mNum;
- mDenom = value.mDenom;
- if (value instanceof Rational.BigRational) {
- mBignum = value.numerator();
- mBigdenom = value.denominator();
- } else {
- mBignum = mBigdenom = null;
- }
- }
-
- /**
- * Set the value of this rational to newnum/newdenom.
- * @param newnum the new numerator.
- * @param newdenom the new denominator.
- */
- public void setValue(long newnum, long newdenom) {
- long gcd2 = Rational.gcd(Math.abs(newnum), Math.abs(newdenom));
- if (newdenom < 0) {
- gcd2 = -gcd2;
- }
- if (gcd2 != 0) {
- newnum /= gcd2;
- newdenom /= gcd2;
- }
-
- if (Integer.MIN_VALUE <= newnum && newnum <= Integer.MAX_VALUE
- && newdenom <= Integer.MAX_VALUE) {
- mNum = (int) newnum;
- mDenom = (int) newdenom;
- mBignum = mBigdenom = null;
- } else {
- mBignum = BigInteger.valueOf(newnum);
- mBigdenom = BigInteger.valueOf(newdenom);
- }
- }
-
- /**
- * Normalize the rational by dividing through the gcd. This is
- * called after every operation.
- */
- private void normalize() {
- if (mBignum == null) {
- final int norm = Rational.gcd(mNum, mDenom);
- if (norm != 0 && norm != 1) {
- mNum /= norm;
- mDenom /= norm;
- }
- if (mDenom < 0) {
- mNum = -mNum;
- mDenom = -mDenom;
- }
- } else {
- if (!mBigdenom.equals(BigInteger.ONE)) {
- BigInteger norm = Rational.gcd(mBignum, mBigdenom).abs();
- if (mBigdenom.signum() < 0) {
- norm = norm.negate();
- }
- if (!norm.equals(BigInteger.ZERO)
- && !norm.equals(BigInteger.ONE)) {
- mBignum = mBignum.divide(norm);
- mBigdenom = mBigdenom.divide(norm);
- }
- }
- if (mBigdenom.bitLength() < 32 && mBignum.bitLength() < 32) { // NOCHECKSTYLE
- mNum = mBignum.intValue();
- mDenom = mBigdenom.intValue();
- mBignum = mBigdenom = null;
- }
- }
- }
-
- /**
- * Add the rational other to this rational.
- * @param other the rational to add.
- * @return this mutable rational.
- */
- public MutableRational add(Rational other) {
- /* fast path */
- if (other == Rational.ZERO) {
- return this;
- }
- if (mBignum == null && !(other instanceof Rational.BigRational)) {
- if (mDenom == other.mDenom) {
- /* handle gcd = 0 correctly
- * two INFINITYs with same sign give INFINITY,
- * otherwise it gives NAN.
- */
- if (mDenom == 0) {
- if (mNum != other.mNum) {
- mNum = 0;
- }
- } else {
- /* a common, very simple case, e.g. for integers */
- setValue((long) mNum + other.mNum, mDenom);
- }
- } else {
- final int gcd = Rational.gcd(mDenom, other.mDenom);
- final long denomgcd = mDenom / gcd;
- final long otherdenomgcd = other.mDenom / gcd;
- final long newdenom = denomgcd * other.mDenom;
- final long newnum = otherdenomgcd * mNum + denomgcd * other.mNum;
- setValue(newnum, newdenom);
- }
- return this;
- }
-
- if (mBignum == null && mNum == 0 && mDenom == 1) {
- /* This is zero; set result to other */
- mBignum = other.numerator();
- mBigdenom = other.denominator();
- return this;
- }
-
- final BigInteger tdenom = denominator();
- final BigInteger odenom = other.denominator();
- if (tdenom.equals(odenom)) {
- mBignum = numerator().add(other.numerator());
- mBigdenom = tdenom;
- } else {
- final BigInteger gcd = Rational.gcd(tdenom, odenom);
- final BigInteger tdenomgcd = tdenom.divide(gcd);
- final BigInteger odenomgcd = odenom.divide(gcd);
- mBignum = numerator().multiply(odenomgcd)
- .add(other.numerator().multiply(tdenomgcd));
- mBigdenom = tdenom.multiply(odenomgcd);
- }
- normalize();
- return this;
- }
-
- /**
- * Negate this rational, i.e., this = -this.
- * @return this mutable rational.
- */
- public MutableRational negate() {
- if (mBignum == null) {
- if (mNum == Integer.MIN_VALUE) {
- setValue(-(long)Integer.MIN_VALUE, mDenom);
- } else {
- mNum = -mNum;
- }
- } else {
- mBignum = mBignum.negate();
- }
- return this;
- }
-
- /**
- * Subtract the other rational from this.
- * @param other the rational to subtract.
- * @return this mutable rational.
- */
- public MutableRational sub(Rational other) {
- return add(other.negate());
- }
-
- /**
- * Multiply this rational with other and store the result in this.
- * @param other the rational to multiply with.
- * @return this mutable rational.
- */
- public MutableRational mul(Rational other) {
- /* fast path */
- if (other == Rational.ONE) {
- return this;
- }
- if (other == Rational.MONE) {
- return negate();
- }
- if (mBignum == null && !(other instanceof Rational.BigRational)) {
- final long newnum = (long)mNum * other.mNum;
- final long newdenom = (long)mDenom * other.mDenom;
- setValue(newnum, newdenom);
- return this;
- }
-
- mBignum = numerator().multiply(other.numerator());
- mBigdenom = denominator().multiply(other.denominator());
- normalize();
- return this;
- }
-
- /**
- * Divide this rational by the other and store the result in this.
- * @param other the divisor.
- * @return this mutable rational.
- */
- public MutableRational div(Rational other) {
- /* fast path */
- if (other == Rational.ZERO) {
- throw new ArithmeticException("Division by ZERO");
- }
- if (mBignum == null && mNum == 0) {
- return this;
- }
- if (other == Rational.ONE) {
- return this;
- }
- if (other == Rational.MONE) {
- return negate();
- }
- if (mBignum == null && !(other instanceof Rational.BigRational)) {
- long newnum = (long)mNum * other.mDenom;
- final long newdenom = (long)mDenom * other.mNum;
- // +-inf : -c = -+inf
- if (newdenom == 0 && other.mNum < 0) {
- newnum = -newnum;
- }
- setValue(newnum, newdenom);
- return this;
- }
- mBignum = numerator().multiply(other.denominator());
- mBigdenom = denominator().multiply(other.numerator());
- // +-inf : -c = -+inf
- if (mBigdenom.equals(BigInteger.ZERO)
- && other.numerator().signum() == -1) {
- mBignum = mBignum.negate();
- }
- normalize();
- return this;
- }
-
- /**
- * Compute the multiplicative inverse of this rational and store
- * it in this.
- * @return this mutable rational.
- */
- public MutableRational inverse() {
- if (mBignum == null) {
- setValue(mDenom, mNum);
- } else {
- final BigInteger tmp = mBigdenom;
- if (mBignum.signum() < 0) {
- mBigdenom = mBignum.negate();
- mBignum = tmp.negate();
- } else {
- mBigdenom = mBignum;
- mBignum = tmp;
- }
- }
- return this;
- }
-
- /**
- * Check if this rational is negative.
- * @return true iff {@code this < 0}.
- */
- public boolean isNegative() {
- return numerator().signum() < 0;
- }
-
- /**
- * Computes {@code this += (fac1*fac2)}.
- * @param fac1 one of the factors.
- * @param fac2 the other factor.
- * @return this mutable rational.
- */
- public MutableRational addmul(Rational fac1,Rational fac2) {
- return add(fac1.mul(fac2));
- }
-
- /**
- * Computes {@code this += (fac1*fac2)}.
- * @param fac1 one of the factors.
- * @param fac2 the other factor.
- * @return this mutable rational.
- */
- public MutableRational addmul(Rational fac1,BigInteger fac2) {
- return add(fac1.mul(fac2));
- }
-
- /**
- * Computes {@code this = (this - s) / d}.
- * @param s the rational to subtract.
- * @param d the divisor.
- * @return this mutable rational.
- */
- public MutableRational subdiv(Rational s,Rational d) {
- return sub(s).div(d);
- }
-
- @Override
- /**
- * Compares this mutable rational with the other.
- * @param o the other mutable rational.
- * @return -1, if this < o; 1, if this > o; 0 if they are equal.
- */
- public int compareTo(MutableRational o) {
- /* fast path */
- if (mBignum == null && o.mBignum == null) {
- /* handle infinities and nan */
- if (o.mDenom == mDenom) {
- return mNum < o.mNum ? -1 : mNum == o.mNum ? 0 : 1;
- }
- final long valt = (long)mNum * o.mDenom;
- final long valo = (long)o.mNum * mDenom;
- return valt < valo ? -1 : valt == valo ? 0 : 1;
- }
- final BigInteger valthis = numerator().multiply(o.denominator());
- final BigInteger valo = o.numerator().multiply(denominator());
- return valthis.compareTo(valo);
- }
-
- /**
- * Compares this mutable rational with the other.
- * @param o the other rational.
- * @return -1, if this < o; 1, if this > o; 0 if they are equal.
- */
- public int compareTo(Rational o) {
- /* fast path */
- if (mBignum == null && !(o instanceof BigRational)) {
- /* handle infinities and nan */
- if (o.mDenom == mDenom) {
- return mNum < o.mNum ? -1 : mNum == o.mNum ? 0 : 1;
- }
- final long valt = (long)mNum * o.mDenom;
- final long valo = (long)o.mNum * mDenom;
- return valt < valo ? -1 : valt == valo ? 0 : 1;
- }
- final BigInteger valthis = numerator().multiply(o.denominator());
- final BigInteger valo = o.numerator().multiply(denominator());
- return valthis.compareTo(valo);
- }
-
- /**
- * Compares this mutable rational with the other. This works with
- * MutableRational and Rational.
- * @param o the other rational.
- * @return true if this equals o, false otherwise.
- */
- @Override
- public boolean equals(Object o) {
- if (o instanceof Rational) {
- final Rational r = (Rational) o;
- // Works thanks to normalization!!!
- return mBignum == null
- ? !(r instanceof Rational.BigRational)
- && mNum == r.mNum && mDenom == r.mDenom
- : mBignum.equals(r.numerator())
- && mBigdenom.equals(r.denominator());
- }
- if (o instanceof MutableRational) {
- final MutableRational r = (MutableRational) o;
- // Works thanks to normalization!!!
- return mBignum == null
- ? r.mBignum == null && mNum == r.mNum && mDenom == r.mDenom
- : mBignum.equals(r.mBignum) && mBigdenom.equals(r.mBigdenom);
- }
- return false;
- }
-
- /**
- * Get the numerator of this rational.
- * @return the numerator.
- */
- public BigInteger numerator() {
- return mBignum == null ? BigInteger.valueOf(mNum) : mBignum;
- }
-
- /**
- * Get the denominator of this rational.
- * @return the denominator.
- */
- public BigInteger denominator() {
- return mBigdenom == null ? BigInteger.valueOf(mDenom) : mBigdenom;
- }
-
- /**
- * Computes a hashcode. The hashcode is computed as
- * {@code 257 * numerator + denominator} if both fit into an integer and
- * {@code 257 * numerator().hashCode() + denominator().hashCode()} if big
- * integers are necessary.
- * @return the hashcode.
- */
- @Override
- public int hashCode() {
- if (mBignum == null) {
- return mNum * 257 + mDenom;
- } else {
- return mBignum.hashCode() * 257 + mBigdenom.hashCode();
- }
- }
-
- /**
- * Get a string representation of this number. This is
- * {@code numerator()+ "/" + denominator()} except for
- * infinity ({@code "inf"}), nan ({@code "nan"}), or minus
- * infinity ({@code "-inf"}).
- * @return the string representation.
- */
- @Override
- public String toString() {
- /* fast path */
- if (mBignum == null) {
- if (mDenom == 0) {
- return mNum > 0 ? "inf" : mNum == 0 ? "nan" : "-inf";
- }
- if (mDenom == 1) {
- return String.valueOf(mNum);
- }
- return mNum + "/" + mDenom;
- } else {
- if (mBigdenom.equals(BigInteger.ONE)) {
- return mBignum.toString();
- }
- return mBignum + "/" + mBigdenom;
- }
- }
-
- /**
- * Check whether this rational represents an integral value. Both infinity
- * values are treated as integral.
- * @return {@code true} iff value is integral.
- */
- public boolean isIntegral() {
- return (mBignum == null)
- ? mDenom <= 1 : mBigdenom.equals(BigInteger.ONE);
- }
-
- /**
- * Convert this mutable rational into a immutable rational.
- * @return the rational.
- */
- public Rational toRational() {
- if (mBignum == null) {
- return Rational.valueOf(mNum, mDenom);
- }
- return Rational.valueOf(numerator(), denominator());
- }
-
- /**
- * Compute sign of this rational. This is equivalent to
- * {@code compare(Rational.ZERO)}.
- * @return the sign of the rational, +1 for positive, 0 for 0 and
- * -1 for negative.
- */
- public int signum() {
- if (mBignum == null) {
- return mNum < 0 ? -1 : mNum == 0 ? 0 : 1;
- }
- return mBignum.signum();
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/NonRecursive.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/NonRecursive.java
deleted file mode 100644
index 22e4ad263fc..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/NonRecursive.java
+++ /dev/null
@@ -1,175 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see
- * class MyWalker extends TermWalker {
- * MyWalker(Term term) { super(term) }
- * walk(NonRecursiveWalker walker, final ApplicationTerm appTerm) {
- * walker.addWorkItem(new NonRecursive.Walker() {
- * public void walk(NonRecursiveWalker walker) {
- * // ... code that should run after parameters are processed
- * }
- * }
- * for (Term param : appTerm.getParameters()) {
- * walker.enqueueWalker(new MyWalker(param));
- * }
- * }
- * walk(... // handle other term classes...
- *
- *
- * For stateful walker you need to extend the class NonRecursive. In
- * addition you still need a Walker class that does the job. It can
- * access the state by casting NonRecursive.
- *
- * Results can be added in a stateful walker to an additional result
- * stack. See FormulaUnLet as an example.
- *
- * @see ComputeFreeVariables
- * @see FormulaUnLet
- * @author Jochen Hoenicke
- */
-public class NonRecursive {
- /**
- * The todo stack. It contains the terms to convert and some info how much
- * was already processed of this term.
- */
- private final ArrayDeque mTodo = new ArrayDeque<>();
-
- /**
- * Walker that does some piece of work. This can be added to
- * the todo stack to be executed later.
- *
- * @author hoenicke
- */
- protected interface Walker {
- /**
- * Do one step of the recursive algorithm. This may enqueue new
- * walkers that do the remaining steps.
- * @param engine The non recursive engine where new walkers
- * can be enqueued.
- */
- public void walk(NonRecursive engine);
- }
- /**
- * Manually reset this walker. This function can be used to clear the
- * todo stack when an exception is raised by a walker. This exception will
- * terminate the non-recursive walk but will leave some walker in the todo
- * stack.
- */
- protected void reset() {
- mTodo.clear();
- }
-
- /**
- * Enqueues a walker on the todo stack.
- * @param item the walker to enqueue.
- */
- public void enqueueWalker(final Walker item) {
- mTodo.addLast(item);
- }
-
- /**
- * The main work horse. This will repeat doing work items until the
- * todo stack is empty.
- * @param item the walker to execute initially.
- */
- public void run(final Walker item) {
- mTodo.addLast(item);
- run();
- }
- /**
- * The main work horse. This will repeat doing work items until the
- * todo stack is empty. This method expects that some Walker are on
- * the todo stack.
- */
- public void run() {
- while (!mTodo.isEmpty()) {
- mTodo.removeLast().walk(this);
- }
- }
-
- @Override
- public String toString() {
- return mTodo.toString();
- }
-
- /**
- * Walker that walks non-recursively over terms.
- * This dispatches the walk function. You still have to provide
- * the code that chooses which sub terms to walk.
- *
- * @author hoenicke
- */
- public static abstract class TermWalker implements Walker {
- protected Term mTerm;
- public TermWalker(final Term term) {
- mTerm = term;
- }
- @Override
- public void walk(final NonRecursive walker) {
- if (mTerm instanceof ApplicationTerm) {
- walk(walker, (ApplicationTerm) mTerm);
- } else if (mTerm instanceof LetTerm) {
- walk(walker, (LetTerm) mTerm);
- } else if (mTerm instanceof AnnotatedTerm) {
- walk(walker, (AnnotatedTerm) mTerm);
- } else if (mTerm instanceof LambdaTerm) {
- walk(walker, (LambdaTerm) mTerm);
- } else if (mTerm instanceof QuantifiedFormula) {
- walk(walker, (QuantifiedFormula) mTerm);
- } else if (mTerm instanceof ConstantTerm) {
- walk(walker, (ConstantTerm) mTerm);
- } else if (mTerm instanceof TermVariable) {
- walk(walker, (TermVariable) mTerm);
- } else if (mTerm instanceof MatchTerm) {
- walk(walker, (MatchTerm) mTerm);
- }
- }
-
- public abstract void walk(NonRecursive walker, ConstantTerm term);
- public abstract void walk(NonRecursive walker, AnnotatedTerm term);
- public abstract void walk(NonRecursive walker, ApplicationTerm term);
- public abstract void walk(NonRecursive walker, LetTerm term);
- public abstract void walk(NonRecursive walker, LambdaTerm term);
- public abstract void walk(NonRecursive walker, QuantifiedFormula term);
- public abstract void walk(NonRecursive walker, TermVariable term);
- public abstract void walk(NonRecursive walker, MatchTerm term);
-
- public Term getTerm() {
- return mTerm;
- }
-
- @Override
- public String toString() {
- return getClass().getSimpleName() + ":" + mTerm;
- }
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/NoopScript.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/NoopScript.java
deleted file mode 100644
index 8fc635b8476..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/NoopScript.java
+++ /dev/null
@@ -1,617 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see getValue(final Term[] terms) throws SMTLIBException,
- UnsupportedOperationException {
- throw new UnsupportedOperationException();
- }
-
- @Override
- public Assignments getAssignment() throws SMTLIBException,
- UnsupportedOperationException {
- throw new UnsupportedOperationException();
- }
-
- @Override
- public Object getOption(final String opt)
- throws UnsupportedOperationException {
- throw new UnsupportedOperationException();
- }
-
- @Override
- public Object getInfo(final String info)
- throws UnsupportedOperationException {
- throw new UnsupportedOperationException();
- }
-
- @Override
- public Term simplify(final Term term) throws SMTLIBException {
- throw new UnsupportedOperationException();
- }
-
- @Override
- public void reset() {
- mTheory = null;
- mStackLevel = 0;
- }
-
- @Override
- public Term[] getInterpolants(final Term[] partition) throws SMTLIBException,
- UnsupportedOperationException {
- // The default startOfSubtrees is an array with 0's.
- final int[] startOfSubtrees = new int[partition.length];
- return getInterpolants(partition, startOfSubtrees);
- }
-
- @Override
- public Term[] getInterpolants(final Term[] partition, final int[] startOfSubtree)
- throws SMTLIBException, UnsupportedOperationException {
- return getInterpolants(partition, startOfSubtree, getProof());
- }
-
- @Override
- public Term[] getInterpolants(final Term[] partition, final int[] startOfSubtree, final Term proofTree)
- throws SMTLIBException, UnsupportedOperationException {
- throw new UnsupportedOperationException();
- }
-
- @Override
- public void exit() {
- // Nothing to do
- }
-
- @Override
- public Sort sort(final String sortname, final Sort... params) throws SMTLIBException {
- return sort(sortname, null, params);
- }
-
- @Override
- public Sort sort(final String sortname, final String[] indices, final Sort... params)
- throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- final Sort res = mTheory.getSort(sortname, indices, params);
- if (res == null) {
- throw new SMTLIBException("Sort " + sortname + " not declared");
- }
- return res;
- }
-
- @Override
- public Term term(final String funcname, final Term... params) throws SMTLIBException {
- return term(funcname, null, null, params);
- }
-
- @Override
- public Term term(final String funcname, final String[] indices,
- final Sort returnSort, final Term... params) throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- return mTheory.term(funcname, indices, returnSort, params);
- }
-
- @Override
- public TermVariable variable(final String varname, final Sort sort)
- throws SMTLIBException {
- if (sort == null || varname == null) {
- throw new SMTLIBException(
- "Invalid input to create a term variable");
- }
- checkSymbol(varname);
- return mTheory.createTermVariable(varname, sort);
- }
-
- @Override
- public Term quantifier(final int quantor, final TermVariable[] vars, Term body,
- final Term[]... patterns) throws SMTLIBException {
- if (vars.length == 0) {
- throw new SMTLIBException("No quantified variables given");
- }
- if (body == null) {
- throw new SMTLIBException("Empty quantifier body");
- }
- if (patterns != null && patterns.length > 0) {
- final Annotation[] annots = new Annotation[patterns.length];
- int i = 0;
- for (final Term[] p : patterns) {
- annots[i++] = new Annotation(":pattern", p);
- }
- body = mTheory.annotatedTerm(annots, body);
- }
- if (quantor == Script.EXISTS) {
- return mTheory.exists(vars, body);
- }
- if (quantor == Script.FORALL) {
- return mTheory.forall(vars, body);
- }
- throw new SMTLIBException("Unknown Quantifier");
- }
-
- @Override
- public Term let(final TermVariable[] vars, final Term[] values, final Term body)
- throws SMTLIBException {
- if (vars.length != values.length) {
- throw new SMTLIBException(
- "Need exactly one value for every variable");
- }
- return mTheory.let(vars, values, body);
- }
-
- @Override
- public Term match(final Term dataArg, final TermVariable[][] vars, final Term[] cases,
- final DataType.Constructor[] constructors) throws SMTLIBException {
- return mTheory.match(dataArg, vars, cases, constructors);
- }
-
-
-
- @Override
- public Term annotate(final Term t, final Annotation... annotations)
- throws SMTLIBException {
- if (annotations.length > 0) {
- for (final Annotation a : annotations) {
- if (a.getKey().equals(":named")) {
- if (!(a.getValue() instanceof String)) {
- throw new SMTLIBException(
- "Need a string value for :named");
- }
- checkSymbol((String) a.getValue());
- if (t.getFreeVars().length != 0) {
- throw new SMTLIBException("Cannot name open terms");
- } else {
- defineFunInternal((String) a.getValue(),
- Theory.EMPTY_TERM_VARIABLE_ARRAY, t.getSort(), t);
- }
- }
- }
- return mTheory.annotatedTerm(annotations, t);
- } else {
- return t;
- }
- }
-
- @Override
- public Term numeral(final String num) throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- if (mTheory.getNumericSort() == null) {
- throw new SMTLIBException("Logic does not allow numerals");
- }
- try {
- return mTheory.numeral(num);
- } catch (final NumberFormatException enfe) {
- throw new SMTLIBException("Not a numeral: " + num);
- }
- }
-
- @Override
- public Term numeral(final BigInteger num) throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- if (mTheory.getNumericSort() == null) {
- throw new SMTLIBException("Logic does not allow numerals");
- }
- return mTheory.numeral(num);
- }
-
- @Override
- public Term decimal(final String decimal) throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- if (mTheory.getRealSort() == null) {
- throw new SMTLIBException("Logic does not allow reals");
- }
- try {
- return mTheory.decimal(decimal);
- } catch (final NumberFormatException enfe) {
- throw new SMTLIBException("Not a decimal: " + decimal);
- }
- }
-
- @Override
- public Term decimal(final BigDecimal decimal) throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- if (mTheory.getRealSort() == null) {
- throw new SMTLIBException("Logic does not allow reals");
- }
- return mTheory.decimal(decimal);
- }
-
- @Override
- public Term string(final QuotedObject str) throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- if (mTheory.getStringSort() == null) {
- throw new SMTLIBException("Logic does not allow strings");
- }
- return mTheory.string(str);
- }
-
- @Override
- public Term hexadecimal(final String hex) throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- final Term res = mTheory.hexadecimal(hex);
- if (res == null) {
- throw new SMTLIBException("No bitvector logic");
- }
- return res;
- }
-
- @Override
- public Term binary(final String bin) throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- final Term res = mTheory.binary(bin);
- if (res == null) {
- throw new SMTLIBException("No bitvector logic");
- }
- return res;
- }
-
- @Override
- public Sort[] sortVariables(final String... names) throws SMTLIBException {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- return mTheory.createSortVariables(names);
- }
-
- @Override
- public Model getModel() throws SMTLIBException,
- UnsupportedOperationException {
- throw new UnsupportedOperationException();
- }
-
- @Override
- public Iterable checkAllsat(final Term[] predicates)
- throws SMTLIBException, UnsupportedOperationException {
- throw new UnsupportedOperationException();
- }
-
- @Override
- public Term[] findImpliedEquality(final Term[] x, final Term[] y)
- throws SMTLIBException, UnsupportedOperationException {
- throw new UnsupportedOperationException();
- }
-
- @Override
- public QuotedObject echo(final QuotedObject msg) {
- return msg;
- }
-
- @Override
- public void resetAssertions() {
- if (mTheory == null) {
- throw new SMTLIBException("No logic set!");
- }
- mTheory.resetAssertions();
- mStackLevel = 0;
- }
-
- @Override
- public Term[] getUnsatAssumptions() throws SMTLIBException,
- UnsupportedOperationException {
- throw new UnsupportedOperationException();
- }
-
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/OccurrenceCounter.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/OccurrenceCounter.java
deleted file mode 100644
index 449d80150d5..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/OccurrenceCounter.java
+++ /dev/null
@@ -1,174 +0,0 @@
-/*
- * Copyright (C) 2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see unifier = new HashMap();
- for (int i = 0; i < paramSorts.length; i++) {
- if (!mParamSorts[i].unifySort(unifier, paramSorts[i])) {
- return null;
- }
- }
- if (result != null) { // NOPMD
- if (!mResultSort.unifySort(unifier, result.getRealSort())) {
- return null;
- }
- return result;
- } else {
- final Sort[] mapping = new Sort[mTypeParams.length];
- for (int i = 0; i < mTypeParams.length; i++) {
- mapping[i] = unifier.get(mTypeParams[i]);
- // check if there are still unresolved type parameters.
- if (mapping[i] == null) {
- return null;
- }
- }
- return mResultSort.mapSort(mapping);
- }
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/PrintTerm.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/PrintTerm.java
deleted file mode 100644
index ed6d042cc4f..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/PrintTerm.java
+++ /dev/null
@@ -1,162 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see mTodo = new ArrayDeque<>();
- /**
- * Convert a term into an appendable.
- * @param appender The appendable.
- * @param term The term.
- */
- public void append(final Appendable appender, final Term term) {
- try {
- mTodo.add(term);
- run(appender);
- } catch (final IOException ex) {
- throw new RuntimeException("Appender throws IOException", ex);
- }
- }
- /**
- * Convert a sort into an appendable. Note that sorts can get pretty long,
- * too. Hence we do this non-recursively to prevent stack overflows.
- * @param appender The appendable.
- * @param sort The sort.
- */
- public void append(final Appendable appender, final Sort sort) {
- try {
- mTodo.add(sort);
- run(appender);
- } catch (final IOException ex) {
- throw new RuntimeException("Appender throws IOException", ex);
- }
- }
-
- /**
- * Append an s-expression. The s-expression might contain terms.
- * @param appender The appendable.
- * @param sexpr The s-expression.
- */
- public void append(final Appendable appender, final Object[] sexpr) {
- try {
- mTodo.add(sexpr);
- run(appender);
- } catch (final IOException ex) {
- throw new RuntimeException("Appender throws IOException", ex);
- }
- }
-
- /**
- * Ensure the identifier is SMTLIB 2 compliant. If a symbol that is not
- * allowed due to the SMTLIB 2 standard is encountered, the whole identifier
- * will be quoted.
- * @param id An unquoted identifier.
- * @return SMTLIB 2 compliant identifier.
- */
- public static String quoteIdentifier(final String id) {
- assert id.indexOf('|') < 0 && id.indexOf('\\') < 0;
- for (int idx = 0; idx < id.length(); idx++) {
- final char c = id.charAt(idx);
- if (!(c >= 'A' && c <= 'Z')
- && !(c >= 'a' && c <= 'z')
- && !(c >= '0' && c <= '9' && idx > 0)
- && "~!@$%^&*_+-=<>.?/".indexOf(c) < 0) {
- return "|" + id + "|";
- }
- }
- return id;
- }
-
- /**
- * Ensure that object can be used as SMT-LIB 2 compliant identifier.
- * otherwise the input is returned.
- * @param value some object.
- * @return quoted identifier if value is String, otherwise value
- * (the input) is returned.
- */
- public static Object quoteObjectIfString(final Object value) {
- if (value instanceof String) {
- final String valueAsString = String.valueOf(value);
- if (valueAsString.charAt(0) == '|' && valueAsString.charAt(valueAsString.length() - 1) == '|') {
- return value;
- } else {
- return quoteIdentifier(valueAsString);
- }
- } else {
- return value;
- }
- }
-
- /**
- * Walk over a term and add its components to the todo queue.
- *
- * @param term the term.
- */
- protected void walkTerm(final Term term) {
- term.toStringHelper(mTodo);
- }
-
- /**
- * Walk over a sort and add its components to the todo queue.
- *
- * @param sort the sort.
- */
- protected void walkSort(final Sort sort) {
- sort.toStringHelper(mTodo);
- }
-
- private void run(final Appendable appender) throws IOException {
- while (!mTodo.isEmpty()) {
- final Object next = mTodo.removeLast();
- if (next instanceof Term) {
- walkTerm((Term) next);
- } else if (next instanceof Sort) {
- walkSort((Sort) next);
- } else if (next instanceof Object[]) {
- final Object[] arr = (Object[]) 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());
- }
- }
- }
-
- @Override
- public String toString() {
- return "[PrintTerm: " + mTodo + "]";
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/QuantifiedFormula.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/QuantifiedFormula.java
deleted file mode 100644
index 724e8824ea5..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/QuantifiedFormula.java
+++ /dev/null
@@ -1,109 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see
- * (forall ((var_1 sort_1) ... (var_n sort_n)) ...)
- * or
- *
- * (exists ((var_1 sort_1) ... (var_n sort_n)) ...)
- * .
- *
- * A quantified formula is created by
- * {@link Script#quantifier(int, TermVariable[], Term, Term[][])}.
- *
- * @author hoenicke
- */
-public class QuantifiedFormula extends Term {
- public static final int EXISTS = 0;
- public static final int FORALL = 1;
-
- private final int mQuantifier;
- private final TermVariable[] mVariables;
- private final Term mSubFormula;
-
- QuantifiedFormula(final int quant, final TermVariable[] vars, final Term f, final int hash) {
- super(hash);
- mQuantifier = quant;
- mVariables = vars;
- mSubFormula = f;
- }
-
- /**
- * @return the quantifier
- */
- public int getQuantifier() {
- return mQuantifier;
- }
-
- /**
- * Get the quantified variables.
- * @return the variables
- */
- public TermVariable[] getVariables() {
- return mVariables;
- }
-
- /**
- * Get the formula under the quantifier.
- * @return the sub-formula.
- */
- public Term getSubformula() {
- return mSubFormula;
- }
-
- @Override
- public Sort getSort() {
- return mSubFormula.getSort();
- }
-
- public static final int hashQuantifier(
- final int quant, final TermVariable[] vars, final Term f) {
- return //Arrays.hashCode(vars) ^ f.hashCode() ^ quant;
- HashUtils.hashJenkins(f.hashCode() ^ quant, (Object[]) vars);
- }
-
- @Override
- public void toStringHelper(final ArrayDeque mTodo) {
- // Add subterm to stack.
- mTodo.addLast(")");
- mTodo.addLast(getSubformula());
- mTodo.addLast(")) ");
-
- // Add variables
- final TermVariable[] vars = getVariables();
- for (int i = vars.length - 1; i > 0; i--) {
- mTodo.addLast(vars[i].getSort());
- mTodo.addLast(") (" + vars[i] + " ");
- }
- mTodo.addLast(vars[0].getSort());
-
- // Print out the quantifier.
- mTodo.addLast("(" + (getQuantifier() == EXISTS ? "exists" : "forall")
- + " ((" + vars[0] + " ");
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/QuotedObject.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/QuotedObject.java
deleted file mode 100644
index a28b1c4dcfb..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/QuotedObject.java
+++ /dev/null
@@ -1,117 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see "..."
- * is represented by a ConstantTerm whose value is a quoted object. The
- * underlying value is the string in parsed form, i.e., escape sequences using
- * backslash are removed and the surrounding quotes are removed.
- *
- * A QuotedObject can also be used to quote arbitrary java objects. These can
- * be used in annotations and will produce syntactically correct SMTLIB
- * scripts if they are dumped.
- *
- * @author hoenicke
- */
-public class QuotedObject {
- /**
- * The underlying Object.
- */
- private final String mValue;
-
- /**
- * True, if this needs to be quoted using the smt-lib 2.5 syntax.
- */
- private boolean mIsSMTLIB25;
-
- /**
- * Create a quoted object.
- * @param value the value that is quoted. Usually this is a string
- * without the quotes.
- */
- public QuotedObject(String value) {
- this(value, true);
- assert value.indexOf('\\') < 0 && value.indexOf('\"') < 0;
- }
-
- /**
- * Create a quoted object.
- * @param value the value that is quoted. Usually this is a string
- * without the quotes.
- */
- public QuotedObject(String value, boolean isSMTLIB25) {
- mValue = value;
- mIsSMTLIB25 = isSMTLIB25;
- }
-
- /**
- * Get the underlying object.
- * @return the underlying object.
- */
- public String getValue() {
- return mValue;
- }
-
- private static String quoteString20(String str) {
- final StringBuilder sb = new StringBuilder();
- sb.append('\"');
- for (int i = 0; i < str.length(); i++) {
- final char c = str.charAt(i);
- switch(c) {
- case '\\':
- sb.append("\\\\");
- break;
- case '\"':
- sb.append("\\\"");
- break;
- default:
- sb.append(c);
- break;
- }
- }
- return sb.append('\"').toString();
- }
-
- private static String quoteString25(String str) {
- final StringBuilder sb = new StringBuilder();
- sb.append('\"');
- for (int i = 0; i < str.length(); i++) {
- final char c = str.charAt(i);
- if (c == '\"') {
- sb.append("\"\"");
- } else {
- sb.append(c);
- }
- }
- return sb.append('\"').toString();
- }
-
- /**
- * Returns the representation of the string. This adds the
- * quotes and converts escape sequences appropriately.
- * @return the SMTLIB compatible string representation.
- */
- @Override
- public String toString() {
- return mIsSMTLIB25 ? quoteString25(mValue) : quoteString20(mValue);
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Rational.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Rational.java
deleted file mode 100644
index 1a928890021..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Rational.java
+++ /dev/null
@@ -1,931 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see
- * ONE.div(NEGATIVE_INFINITY).isNegative() = false (no negative ZERO)
- * ZERO.inverse() = POSITIVE_INFINITY
- * POSITIVE_INFINITY.add(finite number) = POSITIVE_INFINITY.
- * POSITIVE_INFINITY.add(NEGATIVE_INFINITY) = NAN
- * ZERO.mul(POSITIVE_INFINITY) = ZERO.mul(NEGATIVE_INFINITY) = NAN
- * number.div(ZERO) = POSITIVE_INFINITY.mul(number.signum())
- * NAN.isIntegral = POSITIVE_INFINITY.isIntegral = true
- * NAN.floor() = NAN;
- * POSITIVE_INFINITY.floor() = POSITIVE_INFINITY;
- * NAN.frac() = POSITIVE_INFINITY.frac() = ZERO;
- *
- *
- * This class only uses bigintegers if either numerator or
- * denominator does not fit into an int.
- * @author Juergen Christ, Jochen Hoenicke
- */
-public class Rational implements Comparable {
- /**
- * The numerator if num and denom are in int range.
- */
- int mNum;
- /**
- * The denominator if num and denom are in int range.
- */
- int mDenom;
-
- static class BigRational extends Rational {
- /**
- * The numerator if num or denom is outside int range.
- */
- BigInteger mBignum;
- /**
- * The denominator if num or denom is outside int range.
- */
- BigInteger mBigdenom;
-
- /**
- * Construct a rational from two bigints. The constructor
- * is private and does not normalize. Use the static
- * constructor valueOf instead.
- * @param nom Numerator
- * @param denom Denominator
- */
- private BigRational(final BigInteger nom,final BigInteger denom) {
- super(nom.signum(),1);
- mBignum = nom;
- mBigdenom = denom;
- }
-
- /**
- * Return a new rational representing this + other.
- * @param other Rational to add.
- * @return Sum of this and other.
- */
- @Override
- public Rational add(final Rational other) {
- /* fast path */
- if (other == Rational.ZERO) {
- return this;
- }
-
- final BigInteger tdenom = denominator();
- final BigInteger odenom = other.denominator();
- if (tdenom.equals(odenom)) {
- /* another very simple case */
- return valueOf(numerator().add(other.numerator()), tdenom);
- }
- final BigInteger gcd = tdenom.gcd(odenom);
- final BigInteger tdenomgcd = tdenom.divide(gcd);
- final BigInteger odenomgcd = odenom.divide(gcd);
- final BigInteger newnum = numerator().multiply(odenomgcd)
- .add(other.numerator().multiply(tdenomgcd));
- final BigInteger newdenom = tdenom.multiply(odenomgcd);
- return valueOf(newnum, newdenom);
- }
-
- /**
- * Returns a new rational equal to -this.
- * @return -this
- */
- @Override
- public Rational negate() {
- return Rational.valueOf(mBignum.negate(), mBigdenom);
- }
-
- /**
- * Return a new rational representing this * other.
- * @param other Rational to multiply.
- * @return Product of this and other.
- */
- @Override
- public Rational mul(final Rational other) {
- /* fast path */
- if (other == Rational.ONE) {
- return this;
- }
- if (other == Rational.ZERO) {
- return other;
- }
- if (other == Rational.MONE) {
- return negate();
- }
-
- final BigInteger newnum = numerator().multiply(other.numerator());
- final BigInteger newdenom = denominator().multiply(other.denominator());
- return valueOf(newnum, newdenom);
- }
-
- /**
- * Return a new rational representing this * other.
- * @param other big integer to multiply.
- * @return Product of this and other.
- */
- @Override
- public Rational mul(final BigInteger other) {
- if (other.bitLength() < 2) {
- /* fast path */
- final int oint = other.intValue();
- if (oint == 1) {
- return this;
- }
- if (oint == -1) {
- return negate();
- }
- if (oint == 0) {
- return Rational.ZERO;
- }
- }
- return valueOf(numerator().multiply(other), denominator());
- }
-
- /**
- * Return a new rational representing this / other.
- * @param other Rational to divide.
- * @return Quotient of this and other.
- */
- @Override
- public Rational div(final Rational other) {
- if (other == Rational.ONE) {
- return this;
- }
- if (other == Rational.MONE) {
- return negate();
- }
- final BigInteger denom = denominator().multiply(other.numerator());
- BigInteger nom = numerator().multiply(other.denominator());
- // +-inf : -c = -+inf
- if (denom.equals(BigInteger.ZERO)
- && other.numerator().signum() == -1) {
- nom = nom.negate();
- }
- return valueOf(nom,denom);
- }
-
- /**
- * Return a new rational representing this / other.
- * @param other Rational to divide.
- * @return Quotient of this and other.
- */
- public Rational idiv(final Rational other) {
- BigInteger num = denominator().multiply(other.numerator());
- final BigInteger denom = numerator().multiply(other.denominator());
- // +-inf : -c = -+inf
- if (denom.equals(BigInteger.ZERO) && numerator().signum() == -1) {
- num = num.negate();
- }
- return valueOf(num,denom);
- }
-
- /**
- * Returns a new rational representing the inverse of this.
- * @return Inverse of this.
- */
- @Override
- public Rational inverse() {
- return valueOf(mBigdenom, mBignum);
- }
-
- /**
- * Compute the gcd of two rationals (this and other). The gcd
- * is the rational number, such that dividing this and other with
- * the gcd will yield two co-prime integers.
- * @param other the second rational argument.
- * @return the gcd of this and other.
- */
- @Override
- public Rational gcd(final Rational other) {
- if (other == Rational.ZERO) {
- return this.abs();
- }
- final BigInteger tdenom = denominator();
- final BigInteger odenom = other.denominator();
- final BigInteger gcddenom = tdenom.gcd(odenom);
- final BigInteger denom = tdenom.divide(gcddenom).multiply(odenom);
- final BigInteger num = numerator().gcd(other.numerator());
- return Rational.valueOf(num, denom);
- }
-
- @Override
- public int compareTo(final Rational o) {
- final BigInteger valthis = numerator().multiply(o.denominator());
- final BigInteger valo = o.numerator().multiply(denominator());
- return valthis.compareTo(valo);
- }
-
- @Override
- public boolean equals(final Object o) {
- if (o instanceof BigRational) {
- final BigRational r = (BigRational) o;
- // Works thanks to normalization!!!
- return mBignum.equals(r.mBignum)
- && mBigdenom.equals(r.mBigdenom);
- }
- if (o instanceof MutableRational) {
- return ((MutableRational) o).equals(this);
- }
- return false;
- }
-
- @Override
- public BigInteger numerator() {
- return mBignum;
- }
- @Override
- public BigInteger denominator() {
- return mBigdenom;
- }
-
- @Override
- public int hashCode() {
- final int hashNum = HashUtils.hashJenkins(0, mBignum.toByteArray());
- return HashUtils.hashJenkins(hashNum, mBigdenom.toByteArray());
- }
-
- @Override
- public String toString() {
- if (mBigdenom.equals(BigInteger.ONE)) {
- return mBignum.toString();
- }
- return mBignum.toString() + "/" + mBigdenom.toString();
- }
-
- /**
- * Check whether this rational represents an integral value. Both
- * infinity values are treated as integral.
- * @return true iff value is integral.
- */
- @Override
- public boolean isIntegral() {
- return mBigdenom.equals(BigInteger.ONE);
- }
- /**
- * Return a new rational representing the biggest integral rational not
- * bigger than this.
- * @return Next smaller integer of this.
- */
- @Override
- public Rational floor() {
- if (denominator().equals(BigInteger.ONE)) {
- return this;
- }
- BigInteger div = numerator().divide(denominator());
- if (numerator().signum() < 0) {
- div = div.subtract(BigInteger.ONE);
- }
- return Rational.valueOf(div,BigInteger.ONE);
- }
- /**
- * Returns the fractional part of the rational, i.e. the
- * number this.sub(this.floor()).
- * @return Next smaller integer of this.
- */
- @Override
- public Rational frac() {
- if (mBigdenom.equals(BigInteger.ONE)) {
- return Rational.ZERO;
- }
- BigInteger newnum = mBignum.mod(mBigdenom);
- if (newnum.signum() < 0) {
- newnum = newnum.add(mBigdenom);
- }
- return Rational.valueOf(newnum, mBigdenom);
- }
- /**
- * Return a new rational representing the smallest integral rational not
- * smaller than this.
- * @return Next bigger integer of this.
- */
- @Override
- public Rational ceil() {
- if (denominator().equals(BigInteger.ONE)) {
- return this;
- }
- BigInteger div = numerator().divide(denominator());
- if (numerator().signum() > 0) {
- div = div.add(BigInteger.ONE);
- }
- return Rational.valueOf(div,BigInteger.ONE);
- }
- @Override
- public Rational abs() {
- return valueOf(mBignum.abs(), mBigdenom);
- }
- }
-
- /**
- * Construct a rational from two ints. The constructor
- * is private and does not normalize. Use the static
- * constructor valueOf instead.
- * @param num The numerator.
- * @param denom The denominator.
- */
- private Rational(final int num, final int denom) {
- mNum = num;
- mDenom = denom;
- }
-
- /**
- * Construct a rational from two bigints. Use this method
- * to create a rational number if the numerator or denominator
- * may be to big to fit in an int. This method normalizes
- * the rational number and does partial unification.
- *
- * @param bignum The numerator.
- * @param bigdenom The denominator.
- * @return a rational representing numerator/denominator.
- */
- public static Rational valueOf(BigInteger bignum, BigInteger bigdenom) {
- final int cp = bigdenom.signum();
- if (cp < 0) {
- bignum = bignum.negate();
- bigdenom = bigdenom.negate();
- } else if (cp == 0) {
- return valueOf(bignum.signum(), 0);
- }
- if (!bigdenom.equals(BigInteger.ONE)) {
- final BigInteger norm = gcd(bignum, bigdenom).abs();
- if (!norm.equals(BigInteger.ONE)) {
- bignum = bignum.divide(norm);
- bigdenom = bigdenom.divide(norm);
- }
- }
- if (bigdenom.bitLength() < 32 && bignum.bitLength() < 32) {
- return valueOf(bignum.intValue(), bigdenom.intValue());
- } else {
- return new BigRational(bignum, bigdenom);
- }
- }
-
- /**
- * Construct a rational from two longs. Use this method
- * to create a rational number. This method normalizes
- * the rational number and may return a previously created
- * one.
- * This method does not work if called with value
- * Long.MIN_VALUE.
- *
- * @param newnum The numerator.
- * @param newdenom The denominator.
- * @return a rational representing numerator/denominator.
- */
- public static Rational valueOf(long newnum, long newdenom) {
- if (newdenom != 1) {
- long gcd2 = Math.abs(gcd(newnum, newdenom));
- if (gcd2 == 0) {
- return NAN;
- }
- if (newdenom < 0) {
- gcd2 = -gcd2;
- }
- newnum /= gcd2;
- newdenom /= gcd2;
- }
-
- if (newdenom == 1) {
- if (newnum == 0) {
- return ZERO;
- }
- if (newnum == 1) {
- return ONE;
- }
- if (newnum == -1) {
- return MONE;
- }
- } else if (newdenom == 0) {
- if (newnum == 1) {
- return POSITIVE_INFINITY;
- } else {
- return NEGATIVE_INFINITY;
- }
- }
-
- if (Integer.MIN_VALUE <= newnum && newnum <= Integer.MAX_VALUE
- && newdenom <= Integer.MAX_VALUE) {
- return new Rational((int) newnum, (int) newdenom);
- }
- return new BigRational(BigInteger.valueOf(newnum),
- BigInteger.valueOf(newdenom));
- }
-
- /**
- * Calculates the greatest common divisor of two numbers. Expects two
- * nonnegative values.
- * @param a First number
- * @param b Second Number
- * @return Greatest common divisor
- */
- public static int gcd(int a, int b) {
- /* This is faster for integer */
- //assert(a >= 0 && b >= 0);
- while (b != 0) {
- final int t = a % b;
- a = b;
- b = t;
- }
- return a;
- }
-
- /**
- * Calculates the greatest common divisor of two numbers.
- * @param a First number
- * @param b Second Number
- * @return Greatest common divisor
- */
- public static long gcd(long a, long b) {
- /* This is faster for longs on 32-bit architectures */
- if (a < 0) {
- a = -a;
- }
- if (b < 0) {
- b = -b;
- }
- if (a == 0 || b == 1) {
- return b;
- }
- if (b == 0 || a == 1) {
- return a;
- }
- final int ashift = Long.numberOfTrailingZeros(a);
- final int bshift = Long.numberOfTrailingZeros(b);
- a >>= ashift;
- b >>= bshift;
- while (a != b) {
- long t;
- if (a < b) {
- t = b - a;
- b = a;
- } else {
- if (b == 1) {
- a = b;
- break;
- }
- t = a - b;
- }
- do {
- t >>= 1;
- } while (((int) t & 1) == 0);
- a = t;
- }
- return a << Math.min(ashift, bshift);
- }
-
- /**
- * Compute the gcd of two BigInteger. This is the same
- * as {@code i1.gcd(i2)}, but it is more efficient for small numbers.
- * @param i1 the first big integer.
- * @param i2 the second big integer.
- * @return the gcd of i1 and i2.
- */
- public static BigInteger gcd(final BigInteger i1, final BigInteger i2) {
- if (i1 == BigInteger.ONE || i2 == BigInteger.ONE) {
- return BigInteger.ONE;
- }
- final int l1 = i1.bitLength();
- final int l2 = i2.bitLength();
- if (l1 < 31 && l2 < 31) {
- return BigInteger.valueOf(gcd(i1.intValue(), i2.intValue()));
- } else if (l1 < 63 && l2 < 63) {
- return BigInteger.valueOf(gcd(i1.longValue(), i2.longValue()));
- } else {
- return i1.gcd(i2);
- }
- }
-
- /**
- * Return a new rational representing this + other.
- * @param other Rational to add.
- * @return Sum of this and other.
- */
- public Rational add(final Rational other) {
- /* fast path */
- if (other == Rational.ZERO) {
- return this;
- }
- if (this == Rational.ZERO) {
- return other;
- }
- if (other instanceof BigRational) {
- return other.add(this);
- } else {
- if (mDenom == other.mDenom) {
- /* handle gcd = 0 correctly
- * two INFINITYs with same sign give INFINITY,
- * otherwise it gives NAN.
- */
- if (mDenom == 0) {
- return mNum == other.mNum ? this : NAN;
- }
- /* a common, very simple case, e.g. for integers */
- return valueOf((long) mNum + other.mNum, mDenom);
- }
- /* This also handles infinity/NAN + normal correctly. */
- final int gcd = gcd(mDenom, other.mDenom);
- final long denomgcd = mDenom / gcd;
- final long otherdenomgcd = other.mDenom / gcd;
- final long newdenom = denomgcd * other.mDenom;
- final long newnum = otherdenomgcd * mNum + denomgcd * other.mNum;
- return valueOf(newnum, newdenom);
- }
- }
-
- /**
- * Computes {@code this + (fac1*fac2)}.
- * @param fac1 one of the factors.
- * @param fac2 the other factor.
- * @return the result of the computation.
- */
- public Rational addmul(final Rational fac1,final Rational fac2) {
- return add(fac1.mul(fac2));
- }
-
- /**
- * Computes {@code (this - s) / d}.
- * @param s the rational to subtract.
- * @param d the divisor.
- * @return the result of the computation.
- */
- public Rational subdiv(final Rational s,final Rational d) {
- return sub(s).div(d);
- }
- /**
- * Returns a new rational equal to -this.
- * @return -this.
- */
- public Rational negate() {
- return Rational.valueOf(-(long)mNum, mDenom);
- }
- /**
- * Return a new rational representing this - other.
- * @param other Rational to subtract.
- * @return Difference of this and other.
- */
- public Rational sub(final Rational other) {
- return add(other.negate());
- }
- /**
- * Return a new rational representing this * other.
- * @param other Rational to multiply.
- * @return Product of this and other.
- */
- public Rational mul(final Rational other) {
- /* fast path */
- if (other == Rational.ONE) {
- return this;
- }
- if (this == Rational.ONE) {
- return other;
- }
- if (other == Rational.MONE) {
- return negate();
- }
- if (this == Rational.MONE) {
- return other.negate();
- }
- if (other instanceof BigRational) {
- return other.mul(this);
- }
-
- final long newnum = (long)mNum * other.mNum;
- final long newdenom = (long)mDenom * other.mDenom;
- return valueOf(newnum, newdenom);
- }
-
- /**
- * Return a new rational representing this * other.
- * @param other big integer to multiply.
- * @return Product of this and other.
- */
- public Rational mul(final BigInteger other) {
- if (other.bitLength() < 32) { // NOCHECKSTYLE
- /* fast path */
- final int oint = other.intValue();
- if (oint == 1) {
- return this;
- }
- if (oint == -1) {
- return negate();
- }
- final long newnum = (long)mNum * oint;
- return valueOf(newnum, mDenom);
- }
-
- if (this == Rational.ONE) {
- return valueOf(other, BigInteger.ONE);
- }
- if (this == Rational.MONE) {
- return valueOf(other.negate(), BigInteger.ONE);
- }
-
- return valueOf(numerator().multiply(other), denominator());
- }
- /**
- * Return a new rational representing this / other.
- * @param other Rational to divide.
- * @return Quotient of this and other.
- */
- public Rational div(final Rational other) {
- if (other == Rational.ONE) {
- return this;
- }
- if (other == Rational.MONE) {
- return negate();
- }
-
- if (other instanceof BigRational) {
- return ((BigRational)other).idiv(this);
- }
-
- /* fast path */
- long newnum = (long)mNum * other.mDenom;
- final long newdenom = (long)mDenom * other.mNum;
- // +-inf : -c = -+inf
- if (newdenom == 0 && other.mNum < 0) {
- newnum = -newnum;
- }
- return valueOf(newnum, newdenom);
- }
-
- /**
- * Compute the gcd of two rationals (this and other). The gcd is the rational
- * number, such that dividing this and other with the gcd will yield two
- * co-prime integers. The gcd is always non-negative.
- *
- * @param other the second rational argument.
- * @return the gcd of this and other.
- */
- public Rational gcd(final Rational other) {
- if (this == Rational.ZERO) {
- return other.abs();
- }
- if (other == Rational.ZERO) {
- return this.abs();
- }
- if (other instanceof BigRational) {
- return other.gcd(this);
- }
- /* new numerator = gcd(num, other.num) */
- /* new denominator = lcm(denom, other.denom) */
- final int gcddenom = gcd(mDenom, other.mDenom);
- final long denom = ((long) (mDenom / gcddenom)) * other.mDenom;
- final long num = gcd(mNum < 0 ? -(long) mNum : mNum, other.mNum < 0 ? -(long) other.mNum : other.mNum);
- return valueOf(num, denom);
- }
- /**
- * Returns a new rational representing the inverse of this.
- * @return Inverse of this.
- */
- public Rational inverse() {
- return valueOf(mDenom, mNum);
- }
-
- /**
- * Check whether this rational is negative.
- * @return true iff this rational is negative.
- */
- public boolean isNegative() {
- return mNum < 0;
- }
- /**
- * Return the sign of this rational. The sign will be -1, 0, or 1 if this
- * rational is negative, zero, or positive.
- * @return The sign of this rational.
- */
- public int signum() {
- return mNum < 0 ? -1 : mNum == 0 ? 0 : 1;
- }
-
- @Override
- /**
- * Compares this rational with the other.
- * @param o the other rational.
- * @return -1, if this < o; 1, if this > o; 0 if they are equal.
- */
- public int compareTo(final Rational o) {
- if (o instanceof BigRational) {
- return -o.compareTo(this);
- }
-
- /* handle infinities and nan */
- if (o.mDenom == mDenom) {
- return mNum < o.mNum ? -1 : mNum == o.mNum ? 0 : 1;
- }
- final long valt = (long)mNum * o.mDenom;
- final long valo = (long)o.mNum * mDenom;
- return valt < valo ? -1 : valt == valo ? 0 : 1;
- }
- @Override
- /**
- * Compares this rational with the other. This works with
- * Rational and MutableRational.
- * @param o the other rational.
- * @return true if this equals o, false otherwise.
- */
- public boolean equals(final Object o) {
- if (o instanceof Rational) {
- if (o instanceof BigRational) {
- return false;
- }
- final Rational r = (Rational) o;
- // Works thanks to normalization!!!
- return mNum == r.mNum && mDenom == r.mDenom;
- }
- if (o instanceof MutableRational) {
- return ((MutableRational) o).equals(this);
- }
- return false;
- }
-
- /**
- * Get the numerator of this rational.
- * @return the numerator.
- */
- public BigInteger numerator() {
- return BigInteger.valueOf(mNum);
- }
-
- /**
- * Get the denominator of this rational.
- * @return the denominator.
- */
- public BigInteger denominator() {
- return BigInteger.valueOf(mDenom);
- }
-
- /**
- * Computes a hashcode. The hashcode is computed as
- * {@code 257 * numerator + denominator} if both fit into an integer and
- * {@code 257 * numerator().hashCode() + denominator().hashCode()} if big
- * integers are necessary.
- * @return the hashcode.
- */
- @Override
- public int hashCode() {
- return HashUtils.hashJenkins(mNum, mDenom);
- }
- /**
- * Get a string representation of this number. This is
- * {@code numerator()+ "/" + denominator()} except for
- * infinity ({@code "inf"}), nan ({@code "nan"}), or minus
- * infinity ({@code "-inf"}).
- * @return the string representation.
- */
- @Override
- public String toString() {
- if (mDenom == 0) {
- return mNum > 0 ? "inf" : mNum == 0 ? "nan" : "-inf";
- }
- if (mDenom == 1) {
- return String.valueOf(mNum);
- }
- return mNum + "/" + mDenom;
- }
- /**
- * Check whether this rational represents an integral value. Both infinity
- * values are treated as integral.
- * @return true iff value is integral.
- */
- public boolean isIntegral() {
- return mDenom <= 1;
- }
- /**
- * Return a new rational representing the biggest integral rational not
- * bigger than this.
- * @return Next smaller integer of this.
- */
- public Rational floor() {
- if (mDenom <= 1) {
- return this;
- }
- int div = mNum / mDenom;
- // Java rounds the wrong way for negative numbers.
- // We know that the division is not exact due to
- // normalization and mdenom != 1, so subtracting
- // one fixes the result for negative numbers.
- if (mNum < 0) {
- div--;
- }
- return valueOf(div, 1);
- }
- /**
- * Returns the fractional part of the rational, i.e. the
- * number this.sub(this.floor()).
- * @return Next smaller integer of this.
- */
- public Rational frac() {
- if (mDenom <= 1) {
- return Rational.ZERO;
- }
- int newnum = mNum % mDenom;
- // Java rounds the wrong way for negative numbers.
- // We know that the division is not exact due to
- // normalization and mdenom != 1, so subtracting
- // one fixes the result for negative numbers.
- if (newnum < 0) {
- newnum += mDenom;
- }
- return valueOf(newnum, mDenom);
- }
- /**
- * Return a new rational representing the smallest integral rational not
- * smaller than this.
- * @return Next bigger integer of this.
- */
- public Rational ceil() {
- if (mDenom <= 1) {
- return this;
- }
- int div = mNum / mDenom;
- // Java rounds the wrong way for positive numbers.
- // We know that the division is not exact due to
- // normalization and mdenom != 1, so adding
- // one fixes the result for positive numbers.
- if (mNum > 0) {
- div++;
- }
- return valueOf(div, 1);
- }
- /**
- * Compute the absolute of this rational.
- * @return Rational that is equal to the absolute value of this rational.
- */
- public Rational abs() {
- return valueOf(Math.abs((long) mNum), mDenom);
- }
-
- /**
- * Positive infinity. Used to represent the result of 1/0.
- */
- public final static Rational POSITIVE_INFINITY = new Rational(1,0);
- /**
- * Not a number. Used to represent the result of 0/0.
- */
- public final static Rational NAN = new Rational(0,0);
- /**
- * Negative infinity. Used to represent the result of -1/0.
- */
- public final static Rational NEGATIVE_INFINITY = new Rational(-1,0);
- /**
- * The number 0.
- */
- public final static Rational ZERO = new Rational(0,1);
- /**
- * The number 1.
- */
- public final static Rational ONE = new Rational(1,1);
- /**
- * The number -1.
- */
- public final static Rational MONE = new Rational(-1,1);
- /**
- * The number 2.
- */
- public static final Rational TWO = new Rational(2,1);
-
- /**
- * Creates a constant term containing this rational.
- * @param sort the sort of the constant term that should be created.
- * @return a constant term with this rational value.
- * @throws SMTLIBException if term is infinite or NaN, if the
- * sort is not numeric, or if the term is not integral and the sort
- * is Int.
- */
- public Term toTerm(final Sort sort) {
- return sort.getTheory().constant(this, sort);
- }
- /**
- * Check whether this rational corresponds to a (finite) rational value.
- * This function can be used to test for infinites and NaNs.
- * @return true if and only if this rational is not infinite or NaN.
- */
- public boolean isRational() {
- return mDenom != 0;
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/ReasonUnknown.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/ReasonUnknown.java
deleted file mode 100644
index 95c9e41608b..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/ReasonUnknown.java
+++ /dev/null
@@ -1,64 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see (error "msg")
- * For the result unsupported, the standard java exception
- * UnsupportedOperationException is used.
- *
- * This class extends RuntimeException since it should never be thrown if
- * the script interface is used correctly. It therefore corresponds to
- * other runtime exceptions like IllegalArgumentException.
- *
- * @author hoenicke
- */
-@SuppressWarnings("serial")
-public class SMTLIBException extends RuntimeException {
- public SMTLIBException(String message) {
- super(message);
- }
-
- public SMTLIBException(Throwable cause) {
- super(cause);
- }
-
- public SMTLIBException(String message, Throwable cause) {
- super(message, cause);
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java
deleted file mode 100644
index 7ab6d02c507..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Script.java
+++ /dev/null
@@ -1,680 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see
- * Option Type :print-success Boolean :produce-proofs Boolean :produce-assignments Boolean :produce-models Boolean :regular-output-channel String :diagnostic-output-channel String :verbosity Integer :interactive-mode Boolean :random-seed BigInteger :timeout BigInteger
- *
- * @author Jochen Hoenicke, Juergen Christ
- */
-public interface Script {
- public static final Sort[] EMPTY_SORT_ARRAY = new Sort[0];
- public static final Term[] EMPTY_TERM_ARRAY = new Term[0];
- /**
- * A lifted three valued Boolean datatype. Convenience operators for the
- * interaction with SMT-solvers written in C are given.
- * @author Juergen Christ
- */
- public enum LBool {
- UNSAT {
- @Override
- public String toString() {
- return "unsat";
- }
- },
- UNKNOWN {
- @Override
- public String toString() {
- return "unknown";
- }
- },
- SAT {
- @Override
- public String toString() {
- return "sat";
- }
- };
- }
- /**
- * Set the logic for the solver. The logic should be the name of one of the
- * elements in the {@link Logics} enumeration.
- * @param logic Name of the logic to set.
- * @throws UnsupportedOperationException If the logic is not supported by
- * the solver.
- * @throws SMTLIBException If a logic is already set.
- */
- public void setLogic(String logic)
- throws UnsupportedOperationException, SMTLIBException;
- /**
- * Set the logic for the solver.
- * @param logic Name of the logic to set.
- * @throws UnsupportedOperationException If the logic is not supported by
- * the solver.
- * @throws SMTLIBException If a logic is already set.
- */
- public void setLogic(Logics logic)
- throws UnsupportedOperationException, SMTLIBException;
-
- /**
- * Set an option for the solver. At least the options described in the standard should be valid options.
- *
- * @param opt
- * Name of the option. Note that it has to start with a colon ({@code :}).
- * @param value
- * Value for this option.
- * @throws UnsupportedOperationException
- * If the option is unsupported.
- * @throws SMTLIBException
- * In case of type errors.
- */
- public void setOption(String opt, Object value)
- throws UnsupportedOperationException, SMTLIBException;
-
- /**
- * Set some information for the solver. Note that according to the standard a solver has to return success, but
- * ignore the info.
- *
- * @param info
- * Name of the info. Note that it has to start with a colon ({@code :}).
- * @param value
- * Value for this info.
- */
- public void setInfo(String info, Object value);
-
- /**
- * Check if constructor is the Constructor of a Datatype within the Theory.
- *
- * @param constructor
- * The Name of the constructor.
- * @return The Constructor or null if it does not exist.
- */
- public FunctionSymbol getFunctionSymbol(String constructor);
-
- /**
- * Declare constructors of a datatype.
- *
- * @param name
- * Name of the Constructor.
- * @param selectors
- * The selectors of the Constructor.
- * @param argumentSorts
- * The argumentSorts of the Constructor.
- * @return The array of constructors.
- * @throws SMTLIBException
- * if name or selectors contain invalid characters.
- */
- public DataType.Constructor constructor(String name, String[] selectors, Sort[] argumentSorts)
- throws SMTLIBException;
-
- /**
- * Create a new datatype.
- *
- * @param typename
- * Name of the datatypes.
- * @param numParams
- * The number of generic arguments for generic datatypes.
- * @return The datatype object.
- * @throws SMTLIBException
- * if typename contains invalid characters.
- */
- public DataType datatype(String typename, int numParams)
- throws SMTLIBException;
-
- /**
- * Declare new datatypes by setting their constructors.
- *
- * @param datatype
- * @param constrs
- * The constructors.
- * @throws SMTLIBException
- * if any problem occurs, e.g. symbols with same name already declared.
- */
- public void declareDatatype(DataType datatype, DataType.Constructor[] constrs)
- throws SMTLIBException;
-
- /**
- * Declare new datatypes by setting their constructors.
- *
- * @param datatypes
- * the datatypes to declare.
- * @param constrs
- * The constructors for each datatype (with {@code constrs.length == datatypes.length}).
- * @param sortParams
- * The sort parameters for each datatype, the outer array contains null if the datatype is not generic
- * ({@code sortParams.length == datatypes.length}).
- * @throws SMTLIBException
- * if any problem occurs, e.g, symbols with same name already declared, wrong array lengths.
- */
- public void declareDatatypes(DataType[] datatypes, DataType.Constructor[][] constrs, Sort[][] sortParams)
- throws SMTLIBException;
-
- /**
- * Declare a user-defined sort.
- * @param sort The name of the new sort.
- * @param arity The arity of the new sort.
- * @throws SMTLIBException If no logic is set, the logic does not allow
- * user-defined sorts, or a sort with this
- * name already exists.
- */
- public void declareSort(String sort, int arity) throws SMTLIBException;
- /**
- * Define an alias of a sort.
- * @param sort Name of the alias.
- * @param sortParams Sort parameters.
- * @param definition Original sort.
- * @throws SMTLIBException If no logic is set, the logic does not allow
- * user-defined sorts, or a sort with this
- * name already exists.
- */
- public void defineSort(String sort, Sort[] sortParams, Sort definition)
- throws SMTLIBException;
- /**
- * Declare a function symbol.
- * @param fun Name of the function symbol.
- * @param paramSorts Sorts of the parameters.
- * @param resultSort Sort of the result of an application of this function.
- * @throws SMTLIBException If the logic is not set, the logic is not an UF
- * logic but the function takes parameters, or a
- * function with this name already exists.
- */
- public void declareFun(String fun, Sort[] paramSorts, Sort resultSort)
- throws SMTLIBException;
- /**
- * Define an alias of a function symbol.
- * @param fun Name of the alias.
- * @param params Parameters of the alias.
- * @param resultSort Return sort of the alias.
- * @param definition Definition of the function alias.
- * @throws SMTLIBException If the logic is not set, the logic is not an UF
- * logic but the function takes parameters, or a
- * function with this name already exists.
- */
- public void defineFun(String fun, TermVariable[] params, Sort resultSort,
- Term definition) throws SMTLIBException;
- /**
- * Push some levels onto the assertion stack.
- * @param levels The number of levels to push.
- * @throws SMTLIBException If logic is not set.
- */
- public void push(int levels) throws SMTLIBException;
- /**
- * Pop some levels from the assertion stack.
- * @param levels The number of levels to pop.
- * @throws SMTLIBException If not enough stack levels are available.
- */
- public void pop(int levels) throws SMTLIBException;
- /**
- * Assert a Boolean term into the solver. The solver might return a change
- * in the state of the logical context. Compliant solvers do not have to do
- * a full check here but return {@link LBool#UNKNOWN}.
- * @param term The Boolean term to assert.
- * @return Possibly an unsatisfiability detected by the solver.
- * @throws SMTLIBException If the term is not Boolean or a named term
- * matches an already defined function.
- */
- public LBool assertTerm(Term term) throws SMTLIBException;
- /**
- * Check for satisfiability of the current context.
- *
- * Note that this function should return {@link LBool#UNKNOWN} in case of
- * errors.
- * @return The result of the check as a lifted Boolean.
- * @throws SMTLIBException If the logic is not set.
- */
- public LBool checkSat() throws SMTLIBException;
- /**
- * Check for satisfiability of the current context under additional
- * assumptions.
- *
- * Note that this function should return {@link LBool#UNKNOWN} in case of
- * errors.
- * @param assumptions Additional assumptions as Boolean constants (nullary
- * ApplicationTerms of sort Bool or their negations).
- * @return The result of the check as a lifted Boolean.
- * @throws SMTLIBException If the logic is not set.
- */
- public LBool checkSatAssuming(Term... assumptions) throws SMTLIBException;
- /**
- * Get all assertions contained in the assertion stack. Note that this
- * command is only available in interactive mode. To enable interactive
- * mode, call
- * {@link #setOption(String, Object) setOption}(":interactive-mode", true).
- * @return An array of all asserted terms.
- * @throws SMTLIBException If interactive mode is not enabled.
- */
- public Term[] getAssertions() throws SMTLIBException;
- /**
- * Trigger a call to a proof processor. Note that this command is only
- * available if proof production is enabled and the last {@link #checkSat()}
- * returned {@link LBool#UNSAT}. To enable proof production, call
- * {@link #setOption(String, Object) setOption}(":produce-proofs", true).
- * @return the proof. This is given as a big smtlib term of the internal
- * type {@literal @proof}.
- * @throws SMTLIBException If proof production is not enabled or the solver
- * did not detect unsatisfiability.
- * @throws UnsupportedOperationException If proof generation is unsupported.
- */
- public Term getProof()
- throws SMTLIBException, UnsupportedOperationException;
- /**
- * Get the unsat core. Note that this command is only available if unsat
- * core production is enabled and the last {@link #checkSat()} returned
- * {@link LBool#UNSAT}. To enable unsat core production, call
- * {@link #setOption(String, Object) setOption}(":produce-unsat-cores",
- * true).
- * @return An array of terms forming an unsat core.
- * @throws SMTLIBException If proof production is not enabled or the solver
- * did not detect unsatisfiability.
- * @throws UnsupportedOperationException If unsat core computation is
- * unsupported.
- */
- public Term[] getUnsatCore()
- throws SMTLIBException, UnsupportedOperationException;
- /**
- * Get the unsatisfiable assumptions. Note that this command is only
- * available if unsat assumption production is enabled and the last
- * {@link #checkSatAssuming(Term...)} returned
- * {@link LBool#UNSAT}. To enable unsat assumption production, call
- * {@link #setOption(String, Object) setOption}
- * (":produce-unsat-assumptions", true).
- * @return An array of terms that correspond to an unsatisfiable subset of
- * last assumptions.
- * @throws SMTLIBException If unsat assumption production is not enabled or
- * the solver did not detect unsatisfiability.
- * @throws UnsupportedOperationException If unsat assumption computation is
- * unsupported.
- */
- public Term[] getUnsatAssumptions()
- throws SMTLIBException, UnsupportedOperationException;
- /**
- * Get values for some terms in the model. Note that this command is only
- * available if model production is enabled and the last {@link #checkSat()}
- * did not return {@link LBool#UNSAT}. To enable model production, call
- * {@link #setOption(String, Object) setOption}(":produce-models", true).
- * @param terms an array of terms whose value should be computed.
- * @return A valuation (mapping from term to value (which is again
- * represented by a term) where the keys are the given terms.
- * @throws SMTLIBException If model production is not enabled or the solver
- * detected unsatisfiability.
- * @throws UnsupportedOperationException If model computation is
- * unsupported
- */
- public Map getValue(Term[] terms)
- throws SMTLIBException, UnsupportedOperationException;
- /**
- * Get values for all named boolean terms in the model. Note that this
- * command is only available if assignment production is enabled and the
- * last {@link #checkSat()} did not return {@link LBool#UNSAT}. To
- * enable assignment production, call
- * {@link #setOption(String, Object) setOption}(":produce-assignments",
- * true).
- * @return An {@link Assignments}.
- * @throws SMTLIBException If assignment production is not enabled, or the
- * solver did not detect unsatisfiability.
- * @throws UnsupportedOperationException If model computation is
- * unsupported
- */
- public Assignments getAssignment()
- throws SMTLIBException, UnsupportedOperationException;
- /**
- * Get the value of an option.
- * @param opt Name of an option.
- * @return The value of this option.
- * @throws UnsupportedOperationException If option is unsupported.
- */
- public Object getOption(String opt) throws UnsupportedOperationException;
-
- /**
- * Get information from the solver. Note that the solver only has to implement the info values described in the
- * standard.
- *
- * @param info
- * Name of the info. Note that it has to start with a colon ({@code :}).
- * @return Value of the option.
- * @throws UnsupportedOperationException
- * If the info is unsupported.
- * @throws SMTLIBException
- * If info is :reason-unknown but last check did not return unknown.
- */
- public Object getInfo(String info)
- throws UnsupportedOperationException, SMTLIBException;
- /**
- * Exit the solver.
- */
- public void exit();
-
- /* Term creation */
- /**
- * Constant representing universal quantification.
- */
- public static final int FORALL = QuantifiedFormula.FORALL;
- /**
- * Constant representing existential quantification.
- */
- public static final int EXISTS = QuantifiedFormula.EXISTS;
-
- /**
- * Get the theory that is used to maintain the term database and list of
- * declared and defined functions.
- *
- * @return the theory.
- */
- public Theory getTheory();
-
- /**
- * Instantiate an n-ary sort with parameters.
- * @param sortname Name of the sort.
- * @param params Sort parameters.
- * @return The corresponding sort.
- * @throws SMTLIBException If and only if the sort does not exist.
- */
- public Sort sort(String sortname, Sort... params) throws SMTLIBException;
- /**
- * Instantiate an indexed n-ary sort with parameters.
- * @param sortname Name of the sort.
- * @param indices Sort indices.
- * @param params Sort parameters.
- * @return The corresponding sort.
- * @throws SMTLIBException If and only if the sort does not exist.
- */
- public Sort sort(String sortname, String[] indices, Sort... params)
- throws SMTLIBException;
- /**
- * Create an array of sort parameters. These parameters can be used when
- * defining a sort. Note that these names cannot be used in the sort
- * functions since the result does not contain any real sort. Users have
- * to save the array and use its components. The result contains the
- * variables in the order in which the names are specified in the input.
- * @param names The names of the variables
- * @return An array corresponding to sort variables with the given names.
- * @throws SMTLIBException If an error occured.
- */
- public Sort[] sortVariables(String... names) throws SMTLIBException;
- /**
- * Create an n-ary term by name. This function should also be used to
- * construct Boolean terms. I.e., the function names "and", "or", "=>",
- * "ite", "=", "distinct", or "not" might be used to create formulas.
- * @param funcname Name of the function.
- * @param params The parameters of the function application.
- * @return The constructed term.
- * @throws SMTLIBException If an error occurred.
- */
- public Term term(String funcname, Term... params) throws SMTLIBException;
- /**
- * Create an n-ary term by name, indices and return sort. This term
- * constructor can be used to resolve overloaded function symbols, or create
- * applications of the "as" function.
- * @param funcname Name of the function.
- * @param indices Indices for the function.
- * @param returnSort Return sort of the function.
- * @param params The parameters of the function application.
- * @return The constructed term.
- * @throws SMTLIBException If an error occurred.
- */
- public Term term(String funcname, String[] indices,
- Sort returnSort, Term... params) throws SMTLIBException;
- /**
- * Create a term variable.
- * @param varname Name of the variable.
- * @param sort Sort of the variable.
- * @return The term variable.
- * @throws SMTLIBException If no name or an invalid sort is given.
- */
- public TermVariable variable(String varname, Sort sort)
- throws SMTLIBException;
- /**
- * Create a quantified formula.
- * @param quantor The quantor flag (one of {@link #EXISTS}, or
- * {@link #FORALL})
- * @param vars The quantified variables.
- * @param body The body of the quantified formula.
- * @param patterns Possible patterns for e-matching (may be
- * null).
- * @return The quantified formula.
- * @throws SMTLIBException If an error occurred.
- */
- public Term quantifier(int quantor, TermVariable[] vars, Term body,
- Term[]... patterns) throws SMTLIBException;
- /**
- * Create a let term. Note that you have to provide exactly as many
- * variables as you provide values.
- * @param vars Variables bound by a let.
- * @param values Values for these variables.
- * @param body Body of the let term.
- * @return The let term.
- * @throws SMTLIBException If an error occurred.
- */
- public Term let(TermVariable[] vars, Term[] values, Term body)
- throws SMTLIBException;
-
- /**
- * Create a match term.
- *
- * @param dataArg
- * The term that is to be matched.
- * @param vars
- * The variables of each pattern.
- * @param cases
- * The match cases.
- * @return The match term.
- * @throws SMTLIBException
- * if a problem occurs (with a human readable description).
- */
- public Term match(final Term dataArg, final TermVariable[][] vars, final Term[] cases,
- DataType.Constructor[] constructors) throws SMTLIBException;
- /**
- * Annotate a term. This can be used to create named terms.
- * @param t Term to annotate.
- * @param annotations Annotations for this term.
- * @return The annotated term.
- * @throws SMTLIBException If the annotation is invalid, or the evaluation
- * of :named produces an error.
- */
- public Term annotate(Term t, Annotation... annotations)
- throws SMTLIBException;
- /**
- * Create a numeral term.
- * @param num String representation of the numeral.
- * @return A numeral term.
- * @throws SMTLIBException If an error occurred.
- */
- public Term numeral(String num) throws SMTLIBException;
- /**
- * Create a numeral term.
- * @param num the numeral as a big integer.
- * @return A numeral term.
- * @throws SMTLIBException If an error occurred.
- */
- public Term numeral(BigInteger num) throws SMTLIBException;
- /**
- * Create a decimal term.
- * @param decimal String representation of the decimal.
- * @return A decimal term.
- */
- public Term decimal(String decimal) throws SMTLIBException;
- /**
- * Create a decimal term.
- * @param decimal the decimal as a big decimal.
- * @return A decimal term.
- */
- public Term decimal(BigDecimal decimal) throws SMTLIBException;
- /**
- * Create a hexadecimal term.
- * @param hex String representation of the hexadecimal.
- * @return A hexadecimal term.
- * @throws SMTLIBException If an error occurred.
- */
- public Term hexadecimal(String hex) throws SMTLIBException;
- /**
- * Create a binary term.
- * @param bin String representation of the binary.
- * @return A binary term.
- * @throws SMTLIBException If an error occurred.
- */
- public Term binary(String bin) throws SMTLIBException;
- /**
- * Create a string term.
- * @param str The string constant (as quoted object).
- * @return A string term.
- * @throws SMTLIBException If an error occurred.
- */
- public Term string(QuotedObject str) throws SMTLIBException;
-
- /* Non-SMTLIB extensions */
- /**
- * Return the underlying theory. This theory is only valid after a call to
- * setLogic and before a call to restart.
- * @return The underlying theory
- */
-// public Theory getTheory();
- /**
- * Simplify a term. This returns a term that is under the current
- * assertions equivalent to the input term.
- * @param term A (usually Boolean) term to simplify.
- * @return The simplified term.
- * @throws SMTLIBException If an error occurred or unsupported.
- */
- public Term simplify(Term term) throws SMTLIBException;
- /**
- * Reset the solver completely. Note that this invalidates all objects
- * previously returned and unsets the logic.
- */
- public void reset();
- /**
- * Resets the assertion stack. This option will keep the logic and all
- * globally defined symbols.
- */
- public void resetAssertions();
- /**
- * Get interpolants for the partitions. Note that the arguments to this
- * call must either be the names of Boolean top-level assertions, or the
- * conjunction of such names.
- * @param partition Partitioning of the assertion stack.
- * @return Interpolants.
- * @throws SMTLIBException An error occurred.
- * @throws UnsupportedOperationException If interpolant computation is
- * unsupported.
- */
- public Term[] getInterpolants(Term[] partition)
- throws SMTLIBException, UnsupportedOperationException;
-
- /**
- * Compute a sequence of interpolants. The nesting array describes the start of
- * the subtree for tree interpolants. For inductive sequences of interpolants
- * use a nesting array completely filled with 0.
- *
- * @param partition The array of formulas. This should contain either
- * top-level names or conjunction of top-level names.
- * @param startOfSubtree The start of the subtree containing the formula at this
- * index as root.
- * @return Tree interpolants respecting the nesting relation.
- * @throws SMTLIBException An error occurred.
- * @throws UnsupportedOperationException If interpolant computation is
- * unsupported.
- */
- public Term[] getInterpolants(Term[] partition, int[] startOfSubtree)
- throws SMTLIBException, UnsupportedOperationException;
-
- /**
- * Compute a sequence of interpolants. The nesting array describes the start of
- * the subtree for tree interpolants. For inductive sequences of interpolants
- * use a nesting array completely filled with 0. This computes the interpolants
- * from the given proof. It can be called at any time, even if the assertion
- * stack has been modified since computing the proof.
- *
- * @param partition The array of formulas. This should contain either
- * top-level names or conjunction of top-level names.
- * @param startOfSubtree The start of the subtree containing the formula at this
- * index as root.
- * @param proofTree The proof tree that used to compute interpolants.
- * @return Tree interpolants respecting the nesting relation.
- * @throws SMTLIBException An error occurred.
- * @throws UnsupportedOperationException If interpolant computation is
- * unsupported.
- */
- public Term[] getInterpolants(Term[] partition, int[] startOfSubtree, Term proofTree)
- throws SMTLIBException, UnsupportedOperationException;
- /**
- * Retrieve a complete model from the solver. This is an optional (non-
- * SMTLIB compliant) operation. This function can only be called when the
- * previous {@link #checkSat()} returned {@link LBool#SAT} or (optionally)
- * {@link LBool#UNKNOWN} and no assertion stack command was issued after
- * this check.
- * @return A model for the current formula.
- * @throws SMTLIBException
- * Model production was not enabled.
- * @throws UnsupportedOperationException
- * The solver does not support this operation.
- */
- public Model getModel()
- throws SMTLIBException, UnsupportedOperationException;
- /**
- * Perform an AllSAT computation over some important predicates.
- * @param predicates The important predicates. Must be Boolean.
- * @return Iterator over minterms found during iteration.
- * @throws SMTLIBException If a predicate is non-Boolean.
- * @throws UnsupportedOperationException If the operation is unsupported.
- */
- public Iterable checkAllsat(Term[] predicates)
- throws SMTLIBException, UnsupportedOperationException;
- /**
- * Try to find an equality between x and y that
- * is implied in the current satisfiable context. If successful, this
- * method returns an array of parameters a,b,c such that the
- * equality a*x = b*y + c is implied by the current context.
- * Note that the x array and the y array must be
- * of equal length and of length at least 2.
- * @param x The different incarnations of the lhs variable.
- * @param y The different incarnations of the rhs variable.
- * @return Array of length 3 or array of length 0 if no equality is implied.
- */
- public Term[] findImpliedEquality(Term[] x, Term[] y);
- /**
- * Echo a message on the regular output channel of the solver. Although
- * this function is not specified in the SMTLIB standard, we do not expect
- * implementations to throw any exceptions. Instead, if the command is
- * unsupported, it should simply be implemented as the identity function.
- * @param msg The message to print.
- * @return The message.
- */
- public QuotedObject echo(QuotedObject msg);
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Sort.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Sort.java
deleted file mode 100644
index 5a535915197..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Sort.java
+++ /dev/null
@@ -1,360 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see getRealSort() == this holds.
- *
- * A sort has a sort symbol and as many sort arguments as the sort symbol
- * specifies. There are also parametric sorts used for declaring polymorphic
- * function symbols. A parametric sort (or sort variable) has a position
- * (used for substitution) and a name, both stored in the SortSymbol.
- *
- * Every term has a closed real sort, which can be obtained by term.getSort().
- * Defined sorts may occur only in function symbols and the declared sort of
- * a term variable. Sorts that are not closed may only occur in polymorphic
- * function symbols and in sort definitions in SortSymbol.
- *
- * @author Jochen Hoenicke
- */
-public final class Sort {
- /**
- * The sort symbol.
- */
- final SortSymbol mSymbol;
- /**
- * The arguments of the sort symbol. This is null if the sort symbol
- * has no arguments, otherwise it is an array with mSymbol.mnumParams
- * elements.
- */
- final Sort[] mArgs;
- /**
- * The indices of the sort symbol. For the sort BitVec this is an
- * array with one element containing the bit length. This field is
- * null (instead of the empty array) if there are no indices.
- */
- final String[] mIndices;
- /**
- * The cached real sort. This is null if real sort was not yet computed.
- * Otherwise it is this for a real sort and the real sort as which the
- * sort is defined in all other cases.
- */
- //@ invariant mRealSort == null || mRealSort.getRealSort() == mRealSort
- Sort mRealSort;
-
- private int mHash;
-
- Sort(final SortSymbol sym, final String[] indices, final Sort[] args) {
- assert args != null;
- assert args.length == (sym.isSortVariable() ? 0 : sym.mNumParams)
- : "Sort created with wrong number of args";
- mSymbol = sym;
- mIndices = indices;
- mArgs = args;
- mHash = HashUtils.hashJenkins(mSymbol.hashCode(), (Object[]) mArgs);
- if (mIndices != null) {
- mHash = HashUtils.hashJenkins(mHash, (Object[]) mIndices);
- }
- }
-
- /**
- * Get the name of this sort.
- * @return the name.
- */
- public String getName() {
- return mSymbol.getName();
- }
-
- /**
- * Get the indexed name of this sort in smtlib representation.
- * @return the name.
- */
- public String getIndexedName() {
- final String name = PrintTerm.quoteIdentifier(mSymbol.getName());
- if (mIndices == null) {
- return name;
- }
- final StringBuilder sb = new StringBuilder();
- sb.append("(_ ").append(name);
- for (final String i : mIndices) {
- sb.append(' ').append(i);
- }
- sb.append(')');
- return sb.toString();
- }
-
- /**
- * Get the symbol for the sort constructor.
- *
- * @return the sort symbol
- */
- public SortSymbol getSortSymbol() {
- return mSymbol;
- }
-
- /**
- * Get the indices, if this is an indexed sort like (_ bv 5).
- * @return the indices, null if this sort is not indexed.
- */
- public String[] getIndices() {
- return mIndices;
- }
-
- /**
- * Get the sort arguments for a sort. This is used for a sort, whose
- * sort symbol was declared with
- * {@link Script#declareSort(String, int) declare-sort(name, int)}
- * where the second parameter is not zero. In that case the sort is created
- * with sort arguments and these arguments are returned by this method.
- * @return An array containing the sort arguments for this sort.
- * You must never write to this array.
- */
- public Sort[] getArguments() {
- return mArgs;
- }
-
- /**
- * Get the real sort. This is used for sorts that are defined with
- * {@link Script#defineSort(String, Sort[], Sort) define-sort}.
- * For other sorts this just returns this.
- * @return the sort representation where all sort definitions are expanded.
- */
- public Sort getRealSort() {
- if (mRealSort == null) {
- if (mSymbol.mSortDefinition == null) {
- if (mArgs.length == 0) {
- mRealSort = this;
- } else {
- Sort[] newArgs = mArgs;
- for (int i = 0; i < newArgs.length; i++) {
- final Sort realArg = mArgs[i].getRealSort();
- if (realArg != mArgs[i]) {
- if (newArgs == mArgs) {
- newArgs = mArgs.clone();
- }
- newArgs[i] = realArg;
- }
- }
- if (newArgs == mArgs) {
- mRealSort = this;
- } else {
- mRealSort =
- mSymbol.getSort(mIndices, newArgs).getRealSort();
- }
- }
- } else {
- mRealSort =
- mSymbol.mSortDefinition.mapSort(mArgs).getRealSort();
- }
- }
- return mRealSort;
- }
-
- boolean equalsSort(final Sort other) {
- if (this == other) {
- return true;
- }
- return getRealSort() == other.getRealSort();
- }
-
- /**
- * Unify this sort with a concrete sort.
- *
- * @param unifier The unifier map. It serves as map from sort parameters
- * to substituted sorts, and also as cache for all open sorts. It should
- * contain all previously computed substitutions.
- * @param concrete the concrete sort to unify this sort with.
- * It must be closed and real.
- * @return true if the sorts unify (in which case the unifier is extended)
- * or false otherwise.
- */
- boolean unifySort(final HashMap unifier, final Sort concrete) {
- assert concrete.getRealSort() == concrete;
- final Sort last = unifier.get(this);
- if (last != null) {
- return last == concrete;
- }
-
- if (!mSymbol.isSortVariable()) {
- final Sort me = getRealSort();
- if (me.mSymbol != concrete.mSymbol) {
- return false;
- }
-
- for (int i = 0; i < me.mArgs.length; i++) {
- if (!me.mArgs[i].unifySort(unifier, concrete.mArgs[i])) {
- return false;
- }
- }
- }
- unifier.put(this, concrete);
- return true;
- }
-
- /**
- * Substitute this sort.
- *
- * @param substitution The substitution. Note that every sort variable has
- * a unique position which is used as index in the substitution array.
- * @return The substituted sort.
- */
- public Sort mapSort(final Sort[] substitution) {
- if (mSymbol.isSortVariable()) {
- return substitution[mSymbol.mNumParams];
- }
- if (mArgs.length == 0) {
- return this;
- }
- if (mArgs.length == 1) {
- final Sort arg = mArgs[0].mapSort(substitution);
- return mSymbol.getSort(mIndices, new Sort[] { arg });
- }
-
- // For more than two arguments create a cache to avoid exponential blow
- final HashMap cachedMappings = new HashMap();
- return mapSort(substitution, cachedMappings);
- }
-
- /**
- * Substitute this sort.
- *
- * @param substitution The substitution. Note that every sort variable has
- * a unique position which is used as index in the substitution array.
- * @param cachedMappings A cache storing for each visited sort the
- * corresponding substituted sort.
- * @return The substituted sort.
- */
- Sort mapSort(final Sort[] substitution, final HashMap cachedMappings) {
- if (mSymbol.isSortVariable()) {
- return substitution[mSymbol.mNumParams];
- }
- Sort result = cachedMappings.get(this);
- if (result != null) {
- return result;
- }
- if (mArgs.length == 0) {
- result = this;
- } else {
- final Sort[] newArgs = new Sort[mArgs.length];
- for (int i = 0; i < mArgs.length; i++) {
- newArgs[i] = mArgs[i].mapSort(substitution, cachedMappings);
- }
- result = mSymbol.getSort(mIndices, newArgs);
- }
- cachedMappings.put(this, result);
- return result;
- }
-
- /**
- * This returns true if and only if the sort was created with
- * {@link Script#sortVariables(String...)}. These are only used for a
- * later {@link Script#defineSort(String, Sort[], Sort) define-sort}
- * command.
- * @return true iff this is a sort variable.
- */
- public boolean isSortVariable() {
- return mSymbol.isSortVariable();
- }
-
- /**
- * This returns the SMTLIB string represenation of this sort.
- * @return the SMTLIB string representation.
- */
- @Override
- public String toString() {
- if (mArgs.length == 0) {
- return getIndexedName();
- }
- final StringBuilder sb = new StringBuilder();
- new PrintTerm().append(sb, this);
- return sb.toString();
- }
-
- /**
- * Convert a sort to a string in a stack based fashion.
- * @param mTodo The stack where to put the strings and sub sorts.
- * @see PrintTerm
- */
- void toStringHelper(final ArrayDeque mTodo) {
- final String name = getIndexedName();
- final Sort[] args = getArguments();
- if (args.length == 0) {
- mTodo.addLast(name);
- } else {
- mTodo.addLast(")");
- for (int i = args.length - 1; i >= 0; i--) {
- mTodo.addLast(args[i]);
- mTodo.addLast(" ");
- }
- mTodo.addLast(name);
- mTodo.addLast("(");
- }
- }
-
- public Theory getTheory() {
- return mSymbol.mTheory;
- }
-
- /**
- * Returns true if this is an array sort. This is any instantiation
- * of the parametric sort Array defined by the SMTLIB array theory.
- * @return true if this is an array sort.
- */
- public boolean isArraySort() {
- return getRealSort().mSymbol.isArray();
- }
-
- /**
- * @return true if this is a bit-vector sort.
- */
- public boolean isBitVecSort() {
- return getName().equals("BitVec");
- }
-
- /**
- * Returns true if this is a numeric sort. Numeric sorts are only the
- * sorts Int and Real defined by the corresponding SMTLIB theories.
- * @return true if this is a numeric sort.
- */
- public boolean isNumericSort() {
- return getRealSort().mSymbol.isNumeric();
- }
-
- /**
- * Returns true if this sort is internal, i.e., defined by an SMTLIB
- * theory.
- * @return true if the sort is internal, false if it is user defined.
- */
- public boolean isInternal() {
- return mSymbol.isIntern();
- }
-
- @Override
- public int hashCode() {
- return mHash;
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/SortSymbol.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/SortSymbol.java
deleted file mode 100644
index ab629328e8e..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/SortSymbol.java
+++ /dev/null
@@ -1,247 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see Array IndexSort ElemSort is parametric over the index and
- * element sort. The sort symbol represents only the name, i.e., Array and
- * stores the number of sort parameters. Then several objects of type Sort
- * can be instantiated with different sort parameters.
- *
- * @author Jochen Hoenicke
- */
-public class SortSymbol {
- /**
- * Flag to indicate that this is an internal sort symbol. An internal
- * sort is one, that is defined by the theory, i.e., Bool, Int, Real,
- * BitVec, Array.
- */
- static final int INTERNAL = 1;
- /**
- * Flag to indicate that this sort is really a sort variable. Sort
- * variables are only used in sort definitions. Outside of these every
- * sort should not contain any sort variable.
- */
- static final int TYPEPARAM = 2;
- /**
- * Flag to indicate that this sort expects index parameter. The only
- * such sort is currently BitVec.
- */
- static final int INDEXED = 4;
- /**
- * Flag to indicate numeric types.
- */
- static final int NUMERIC = 8;
- /**
- * Flag to indicate array types.
- */
- static final int ARRAY = 0x10;
- /**
- * Flag to indicate data types.
- */
- static final int DATATYPE = 0x20;
- /**
- * Flag to indicate the function types.
- */
- static final int FUNCTION = 0x40;
-
- final Theory mTheory;
- final String mName;
- /**
- * The number of parameters this sort symbol expects. If the TYPEPARAM
- * flag is set, this sort is a sort variable and takes no parameters; in
- * that case this gives the de-Bruijn-index of the sort variable.
- */
- final int mNumParams;
- /**
- * The flags. This is the bitwise or of INTERNAL, TYPEPARAM and
- * INDEXED.
- */
- final int mFlags;
- /**
- * The sorts already created from this SortSymbol.
- * If mNumParams is 0, this is the single sort corresponding to
- * this SortSymbol. Otherwise this is a UnifyHash containing all
- * created sorts.
- */
- final Object mSorts;
-
- /**
- * The primitive sort if this is a sort definition.
- */
- final Sort mSortDefinition;
-
- /**
- * The constructor for sort symbols.
- * @param theory The theory this sort belongs to.
- * @param name The name of the sort (without enclosing | for quoting).
- * @param numParams The number of sort parameters this sort expects.
- * E.g., Array expects two sort parameters for index and
- * element sort. For sort variables this gives the
- * de-Bruijn index of the variable instead.
- * @param definition The sort definition, or null if this is a fresh sort.
- * @param flags The flags; bitwise or of INTERNAL, TYPEPARAM and INDEXED.
- */
- SortSymbol(Theory theory, String name, int numParams,
- Sort definition, int flags) {
- mTheory = theory;
- mName = name;
- mFlags = flags;
- mNumParams = numParams;
- mSortDefinition = definition;
- if ((mFlags & TYPEPARAM) != 0
- || ((mFlags & INDEXED) == 0 && mNumParams == 0)) {
- mSorts = new Sort(this, null, new Sort[0]);
- } else {
- mSorts = new UnifyHash();
- }
- }
-
- /**
- * Checks if the sort is internal, i.e., defined by the logic.
- * @return true, if the sort is an internal sort.
- */
- public boolean isIntern() {
- return (mFlags & INTERNAL) != 0;
- }
-
- /**
- * Returns the name of this sort. The | symbols used for quoting are
- * not part of the name.
- * @return the name of the sort.
- */
- public String getName() {
- return mName;
- }
-
- /**
- * Returns a string representation of the sort symbol, as it would be
- * used for declare-sort command.
- * @return the string representation.
- */
- @Override
- public String toString() {
- return "(" + PrintTerm.quoteIdentifier(mName) + " " + mNumParams + ")";
- }
-
- /**
- * Checks whether the indices and the arity match and the sort can be
- * created. This function is called when a sort expression is parsed.
- * Override this function if your sort expects indices.
- * @param indices The indices.
- * @param arity The number of sort parameters.
- * @throws IllegalArgumentException if the sort parameters or the index
- * do not match.
- */
- public void checkArity(String[] indices, int arity) {
- if (indices != null) {
- throw new IllegalArgumentException(
- "Indexed Sort " + mName + " undefined");
- }
- if (arity != ((mFlags & TYPEPARAM) == 0 ? mNumParams : 0)) {
- throw new IllegalArgumentException(
- "Wrong number of arguments for sort " + mName);
- }
- }
-
- @SuppressWarnings("unchecked")
- /**
- * Create the sort with the given indices and sort parameters. Sorts are
- * unified, so this will return an instance of a previously created sort
- * if it already exists.
- * @param indices The indices of the sort, which are given by
- * (_ sortname indices). This is null if no indices were
- * used.
- * @param args The sort parameters; the empty array if no parameters were
- * used.
- * @return the created sort.
- * @throws IllegalArgumentException if the indices or number of sort
- * parameters do not match.
- */
- public Sort getSort(String[] indices, Sort... args) {
- checkArity(indices, args.length);
- if ((mFlags & INDEXED) == 0 && args.length == 0) {
- return (Sort) mSorts;
- }
- final UnifyHash sortCache = (UnifyHash) mSorts;
- final int hash = Arrays.hashCode(indices) ^ Arrays.hashCode(args);
- for (final Sort sort : sortCache.iterateHashCode(hash)) {
- if (Arrays.equals(sort.getArguments(), args)
- && Arrays.equals(sort.getIndices(), indices)) {
- return sort;
- }
- }
- final Sort sort = new Sort(this, indices, args);
- sortCache.put(hash, sort);
- return sort;
- }
-
- /**
- * Checks if this is a sort variable.
- * @return true if this is a sort variable.
- */
- public boolean isSortVariable() {
- return (mFlags & TYPEPARAM) != 0;
- }
- /**
- * Check if this sort symbol corresponds to a numeric sort.
- * @return true if this sort is numeric.
- */
- public boolean isNumeric() {
- return (mFlags & NUMERIC) != 0;
- }
-
- /**
- * Check if this sort symbol corresponds to an array sort.
- * @return true if this sort is an array sort.
- */
- public boolean isArray() {
- return (mFlags & ARRAY) != 0;
- }
-
- /**
- * Check if this sort symbol is a datatype.
- *
- * @return true if this sort symbol is a datatype.
- */
- public boolean isDatatype() {
- return (mFlags & DATATYPE) != 0;
- }
-
- /**
- * Check if this sort symbol is a function type, i.e. the sort symbol
- * {@code ->}.
- *
- * @return true if this sort symbol is a function type.
- */
- public boolean isFunction() {
- return (mFlags & FUNCTION) != 0;
- }
-
- @Override
- public int hashCode() {
- return mName.hashCode();
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Term.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Term.java
deleted file mode 100644
index d70b696a450..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Term.java
+++ /dev/null
@@ -1,130 +0,0 @@
-/*
- * Copyright (C) 2009-2022 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see
- * {@link ApplicationTerm} represents a function application
- * (name ...).
- * {@link AnnotatedTerm} represents an annotated term
- * (! term ...).
- * {@link ConstantTerm} represents a numeral, decimal, bit vector, or string
- * literal.
- * {@link LambdaTerm} represents a lambda term
- * (lambda ((var sort)...) term).
- * {@link LetTerm} represents a let term
- * (let ((var term)...) term).
- * {@link MatchTerm} represents a datatype match term
- * (match d (cases...)).
- * {@link TermVariable} represents a term variable var used in
- * quantifier or let term. Note that constants are represented by
- * ApplicationTerm.
- * {@link QuantifiedFormula} represents a quantified formula
- * (exists/forall ...).
- *
- *
- * In principle it is possible to write your own sub-classes, but that is
- * dangerous and only recommend for the advanced SMTInterpol hacker.
- *
- * @author Juergen Christ, Jochen Hoenicke
- */
-public abstract class Term {
- private final int mHash;
-
- /**
- * A temporary counter used e.g. to count the number of occurrences of this
- * term in a bigger term.
- * Don't use this!!!!
- */
- public int mTmpCtr;
-
- TermVariable[] mFreeVars;
-
- /**
- * Create a term.
- * @param hash the hash code of the term. This should be stable.
- */
- protected Term(final int hash) {
- mHash = hash;
- }
-
- /**
- * Returns the SMTLIB sort of this term.
- * @return the sort of the term.
- */
- public abstract Sort getSort();
-
- /**
- * Computes and returns the free variables occurring in this term.
- * @return the free variables.
- */
- public TermVariable[] getFreeVars() {
- if (mFreeVars == null) {
- new ComputeFreeVariables().transform(this);
- }
- return mFreeVars;
- }
-
- public Theory getTheory() {
- return getSort().mSymbol.mTheory;
- }
-
- /**
- * Prints an SMTLIB representation of this term. This
- * {@link FormulaLet introduces lets for common subexpressions}
- * to prevent exponential blow-up when printing
- * a term with lots of sharing.
- * @return an SMTLIB representation.
- */
- @Override
- public String toString() {
- final Term letted = new FormulaLet().let(this);
- return letted.toStringDirect();
- }
-
- /**
- * Prints the canonical SMTLIB representation of this term.
- * This does not eliminate common sub-expressions and can cause
- * exponential blow-up.
- * @return the canonical SMTLIB representation.
- */
- public String toStringDirect() {
- final StringBuilder sb = new StringBuilder();
- new PrintTerm().append(sb, this);
- return sb.toString();
- }
-
- @Override
- public int hashCode() {
- return mHash;
- }
-
- /**
- * Convert a term to a string in a stack based fashion. This is used
- * for internal purposes. External users can just use toString()
- * or toStringDirect().
- * @param mTodo The stack where to put the strings and sub terms.
- * @see PrintTerm
- */
- protected abstract void toStringHelper(ArrayDeque mTodo);
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/TermEquivalence.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/TermEquivalence.java
deleted file mode 100644
index 521405fbf2c..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/TermEquivalence.java
+++ /dev/null
@@ -1,248 +0,0 @@
-/*
- * Copyright (C) 2013 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see (let ((x 0)) x) is equivalent to (let ((y 0)) y), but not to 0 or
- * (let ((y 0)) 0).
- *
- * @author Juergen Christ, Jochen Hoenicke
- */
-public class TermEquivalence extends NonRecursive {
-
- private final ScopedHashMap mRenaming =
- new ScopedHashMap();
-
- private void beginScope() {
- mRenaming.beginScope();
- }
-
- private void endScope() {
- mRenaming.endScope();
- }
-
- private void addRenaming(TermVariable lvar, TermVariable rvar) {
- mRenaming.put(lvar, rvar);
- }
-
- private boolean checkRenaming(TermVariable lvar, TermVariable rvar) {
- return mRenaming.get(lvar) == rvar;
- }
-
- @SuppressWarnings("serial")
- private static final class NotEq extends RuntimeException {
- // Empty control flow exception
- }
-
- private final static class EndScope implements Walker {
- public final static EndScope INSTANCE = new EndScope();
- @Override
- public void walk(NonRecursive engine) {
- final TermEquivalence te = (TermEquivalence) engine;
- te.endScope();
- }
- }
-
- private final static class AddRenaming implements Walker {
- private final TermVariable mLvar, mRvar;
- public AddRenaming(TermVariable lvar, TermVariable rvar) {
- mLvar = lvar;
- mRvar = rvar;
- }
- @Override
- public void walk(NonRecursive engine) {
- final TermEquivalence te = (TermEquivalence) engine;
- te.addRenaming(mLvar, mRvar);
- }
- }
-
- private final static class TermEq implements Walker {
-
- private final Term mLhs, mRhs;
-
- public TermEq(Term lhs, Term rhs) {
- mLhs = lhs;
- mRhs = rhs;
- }
-
- private final void notEqual() {
- throw new NotEq();
- }
-
- @Override
- public void walk(NonRecursive engine) {
- final TermEquivalence te = (TermEquivalence) engine;
- if (mLhs != mRhs) {
- if (mLhs.getClass() != mRhs.getClass()) {
- // Cannot be equal
- notEqual();
- }
- if (mLhs instanceof ApplicationTerm) {
- final ApplicationTerm l = (ApplicationTerm) mLhs;
- final ApplicationTerm r = (ApplicationTerm) mRhs;
- if (l.getFunction() != r.getFunction()) {
- notEqual();
- }
- final Term[] lparams = l.getParameters();
- final Term[] rparams = r.getParameters();
- if (lparams.length != rparams.length) {
- notEqual();
- }
- for (int i = 0; i < lparams.length; ++i) {
- te.enqueueWalker(new TermEq(lparams[i], rparams[i]));
- }
- } else if (mLhs instanceof AnnotatedTerm) {
- final AnnotatedTerm l = (AnnotatedTerm) mLhs;
- final AnnotatedTerm r = (AnnotatedTerm) mRhs;
- final Annotation[] lannot = l.getAnnotations();
- final Annotation[] rannot = r.getAnnotations();
- if (rannot.length != lannot.length) {
- notEqual();
- }
- for (int i = 0; i < lannot.length; ++i) {
- if (!lannot[i].getKey().equals(rannot[i].getKey())) {
- notEqual();
- }
- if (lannot[i].getValue() instanceof Term
- && rannot[i].getValue() instanceof Term) {
- te.enqueueWalker(new TermEq(
- (Term) lannot[i].getValue(),
- (Term) rannot[i].getValue()));
- } else if (lannot[i].getValue() instanceof Object[]
- && rannot[i].getValue() instanceof Object[]) {
- te.enqueueWalker(
- new ArrayEq((Object[]) lannot[i].getValue(), (Object[]) rannot[i].getValue()));
- } else if (lannot[i].getValue() != rannot[i].getValue() && (lannot[i].getValue() == null
- || !lannot[i].getValue().equals(rannot[i].getValue()))) {
- notEqual();
- }
- }
- } else if (mLhs instanceof LetTerm) {
- final LetTerm llet = (LetTerm) mLhs;
- final LetTerm rlet = (LetTerm) mRhs;
- final TermVariable[] lvars = llet.getVariables();
- final TermVariable[] rvars = rlet.getVariables();
- if (lvars.length != rvars.length) {
- notEqual();
- }
- te.enqueueWalker(EndScope.INSTANCE);
- te.enqueueWalker(new TermEq(llet.getSubTerm(), rlet.getSubTerm()));
- final Term[] lvals = llet.getValues();
- final Term[] rvals = rlet.getValues();
- for (int i = 0; i < lvars.length; ++i) {
- te.enqueueWalker(new AddRenaming(lvars[i], rvars[i]));
- te.enqueueWalker(new TermEq(lvals[i], rvals[i]));
- }
- // te.enqueueWalker(BeginScope.INSTANCE);
- te.beginScope();
- } else if (mLhs instanceof QuantifiedFormula) {
- final QuantifiedFormula lq = (QuantifiedFormula) mLhs;
- final QuantifiedFormula rq = (QuantifiedFormula) mRhs;
- if (lq.getQuantifier() != rq.getQuantifier()) {
- notEqual();
- }
- final TermVariable[] lv = lq.getVariables();
- final TermVariable[] rv = rq.getVariables();
- if (lv.length != rv.length) {
- notEqual();
- }
- te.enqueueWalker(EndScope.INSTANCE);
- te.beginScope();
- for (int i = 0; i < lv.length; ++i) {
- if (lv[i] != rv[i]) {
- if (lv[i].getSort() != rv[i].getSort()) {
- notEqual();
- }
- te.addRenaming(lv[i], rv[i]);
- }
- }
- te.enqueueWalker(new TermEq(lq.getSubformula(), rq.getSubformula()));
- } else if (mLhs instanceof TermVariable) {
- final TermVariable lv = (TermVariable) mLhs;
- final TermVariable rv = (TermVariable) mRhs;
- if (!te.checkRenaming(lv, rv)) {
- notEqual();
- }
- } // Term case switch
- }
- }
- }
-
- private final static class ArrayEq implements Walker {
-
- private final Object[] mLhs, mRhs;
-
- public ArrayEq(Object[] lhs, Object[] rhs) {
- mLhs = lhs;
- mRhs = rhs;
- }
-
- private final void notEqual() {
- throw new NotEq();
- }
-
- @Override
- public void walk(NonRecursive engine) {
- final TermEquivalence te = (TermEquivalence) engine;
- if (mLhs != mRhs) {
- if (mLhs.getClass() != mRhs.getClass()) {
- // Cannot be equal
- notEqual();
- }
- if (mLhs.length != mRhs.length) {
- notEqual();
- }
- for (int i = 0; i < mLhs.length; ++i) {
- if (mLhs[i] == mRhs[i]) {
- continue;
- }
- if (mLhs[i] instanceof Term && mRhs[i] instanceof Term) {
- te.enqueueWalker(new TermEq((Term) mLhs[i], (Term) mRhs[i]));
- } else if (mLhs[i] instanceof Object[] && mRhs[i] instanceof Object[]) {
- te.enqueueWalker(new ArrayEq((Object[]) mLhs[i], (Object[]) mRhs[i]));
- } else {
- if (mLhs[i] != mRhs[i] && (mLhs[i] == null || !mLhs[i].equals(mRhs[i]))) {
- notEqual();
- }
- }
- }
- }
- }
- }
-
- /**
- * Returns true if the terms are equivalent.
- * @param lhs the left hand side term.
- * @param rhs the right hand side term.
- * @return true if the terms are equivalent modulo variable renaming.
- */
- public boolean equal(Term lhs, Term rhs) {
- try {
- run(new TermEq(lhs, rhs));
- return true;
- } catch (final NotEq ignored) {
- reset();
- return false;
- }
- }
-
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/TermTransformer.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/TermTransformer.java
deleted file mode 100644
index c97dbda7820..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/TermTransformer.java
+++ /dev/null
@@ -1,638 +0,0 @@
-/*
- * Copyright (C) 2009-2021 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see > mCache = new ArrayList<>();
- private final ScopedHashMap mScopeMap = new ScopedHashMap<>();
-
- /**
- * The converted terms. This is used for example to store the arguments of an
- * application term, before the application term is evaluated.
- */
- private final ArrayDeque mConverted = new ArrayDeque<>();
-
- /**
- * The converted object arrays. This is used to store the arguments of an array
- * valued annotation, before the annotation's subterm is processed.
- */
- private final ArrayDeque mConvertedArrays = new ArrayDeque<>();
-
- /**
- * This class represents one item of work. It consists of a term and some task
- * that still needs to be performed on the term.
- */
- private static class Convert implements Walker {
- private final Term mTerm;
-
- public Convert(final Term term) {
- mTerm = term;
- }
-
- @Override
- public String toString() {
- return "Convert " + mTerm.toStringDirect();
- }
-
- @Override
- public void walk(final NonRecursive walker) {
- ((TermTransformer) walker).cacheConvert(mTerm);
- }
- }
-
- /**
- * Push all terms in the array on the todo stack as CONVERT work item.
- *
- * @param terms
- * the array of terms.
- */
- protected final void pushTerms(final Term[] terms) {
- for (int i = terms.length - 1; i >= 0; i--) {
- pushTerm(terms[i]);
- }
- }
-
- /**
- * Push a term on the todo stack as CONVERT work item.
- *
- * @param term
- * the term to convert.
- */
- protected final void pushTerm(final Term term) {
- enqueueWalker(new Convert(term));
- }
-
- /**
- * Set the conversion result to term.
- *
- * @param term
- * the converted term.
- */
- protected final void setResult(final Term term) {
- mConverted.addLast(term);
- }
-
- private int findScope(final TermVariable[] tvs) {
- int maxScopeNr = 0;
- for (final TermVariable tv : tvs) {
- final Integer scopeNr = mScopeMap.get(tv);
- if (scopeNr != null && scopeNr > maxScopeNr) {
- maxScopeNr = scopeNr;
- }
- }
- return maxScopeNr;
- }
-
- private static class AddCache implements Walker {
- Term mOldTerm;
-
- public AddCache(final Term term) {
- mOldTerm = term;
- }
-
- @Override
- public void walk(final NonRecursive engine) {
- final TermTransformer transformer = (TermTransformer) engine;
- final int scopeNr = transformer.findScope(mOldTerm.getFreeVars());
- transformer.mCache.get(scopeNr).put(mOldTerm, transformer.mConverted.getLast());
- }
-
- @Override
- public String toString() {
- return "AddCache[" + mOldTerm.toStringDirect() + "]";
- }
- }
-
- private void cacheConvert(final Term term) {
- final int scopeNr = findScope(term.getFreeVars());
- final Term result = mCache.get(scopeNr).get(term);
- if (result == null) {
- enqueueWalker(new AddCache(term));
- convert(term);
- } else {
- setResult(result);
- }
- }
-
- protected void beginScope(final TermVariable[] vars) {
- final Integer scopeNumber = mCache.size();
- mCache.add(new HashMap());
- mScopeMap.beginScope();
- for (final TermVariable var : vars) {
- mScopeMap.put(var, scopeNumber);
- }
- }
-
- protected void endScope() {
- final int scopeNr = mCache.size() - 1;
- mCache.remove(scopeNr);
- mScopeMap.endScope();
- }
-
- /**
- * The function that does the transformation. Override this function if you
- * build your own term transformer. It does not return the result but instead it
- * puts it on the converted stack using setResult(). Instead it can also enqueue
- * some Builders that will in the end put the result on the converted stack.
- *
- * You can always call super.convert() if you do not need to convert the term.
- * It will still convert the sub-terms. If you do not want to convert the sub
- * terms, call setResult(term) instead.
- *
- * @param term
- * The term to convert.
- */
- protected void convert(final Term term) {
- if (term instanceof ConstantTerm || term instanceof TermVariable) {
- mConverted.addLast(term);
- } else if (term instanceof ApplicationTerm) {
- enqueueWalker(new BuildApplicationTerm((ApplicationTerm) term));
- pushTerms(((ApplicationTerm) term).getParameters());
- } else if (term instanceof LetTerm) {
- enqueueWalker(new StartLetTerm((LetTerm) term));
- pushTerms(((LetTerm) term).getValues());
- } else if (term instanceof QuantifiedFormula) {
- final QuantifiedFormula qf = (QuantifiedFormula) term;
- enqueueWalker(new BuildQuantifier(qf));
- pushTerm(qf.getSubformula());
- beginScope(qf.getVariables());
- } else if (term instanceof LambdaTerm) {
- final LambdaTerm lambda = (LambdaTerm) term;
- enqueueWalker(new BuildLambda(lambda));
- pushTerm(lambda.getSubterm());
- beginScope(lambda.getVariables());
- } else if (term instanceof AnnotatedTerm) {
- final AnnotatedTerm annterm = (AnnotatedTerm) term;
- enqueueWalker(new BuildAnnotation(annterm));
- final ArrayDeque todo = new ArrayDeque<>();
- for (final Annotation annot : annterm.getAnnotations()) {
- if (annot.getValue() != null) {
- todo.add(annot.getValue());
- }
- }
- while (!todo.isEmpty()) {
- final Object value = todo.removeLast();
- if (value instanceof Term) {
- pushTerm((Term) value);
- } else if (value instanceof Object[]) {
- enqueueWalker(new BuildObjectArray((Object[]) value));
- for (final Object elem : (Object[]) value) {
- todo.add(elem);
- }
- }
- }
- pushTerm(annterm.getSubterm());
- return;
- } else if (term instanceof MatchTerm) {
- final MatchTerm matchTerm = (MatchTerm) term;
- enqueueWalker(new WalkMatchTerm(matchTerm));
- pushTerm(matchTerm.getDataTerm());
- } else {
- throw new AssertionError("Unknown Term: " + term.toStringDirect());
- }
- }
-
- public void convertApplicationTerm(final ApplicationTerm appTerm, final Term[] newArgs) {
- Term newTerm = appTerm;
- if (newArgs != appTerm.getParameters()) {
- final FunctionSymbol fun = appTerm.getFunction();
- final Theory theory = fun.getTheory();
- newTerm = theory.term(fun, newArgs);
- }
- setResult(newTerm);
- }
-
- public void preConvertLet(final LetTerm oldLet, final Term[] newValues) {
- beginScope(oldLet.getVariables());
- enqueueWalker(new BuildLetTerm(oldLet, newValues));
- pushTerm(oldLet.getSubTerm());
- }
-
- public void postConvertLet(final LetTerm oldLet, final Term[] newValues, final Term newBody) {
- Term result = oldLet;
- if (oldLet.getValues() != newValues || oldLet.getSubTerm() != newBody) {
- result = oldLet.getTheory().let(oldLet.getVariables(), newValues, newBody);
- }
- setResult(result);
- }
-
- public void postConvertLambda(final LambdaTerm old, final Term newBody) {
- Term newFormula = old;
- if (newBody != old.getSubterm()) {
- final Theory theory = old.getTheory();
- final TermVariable[] vars = old.getVariables();
- newFormula = theory.lambda(vars, newBody);
- }
- setResult(newFormula);
- }
-
- public void postConvertQuantifier(final QuantifiedFormula old, final Term newBody) {
- Term newFormula = old;
- if (newBody != old.getSubformula()) {
- final Theory theory = old.getTheory();
- final TermVariable[] vars = old.getVariables();
- newFormula = old.getQuantifier() == QuantifiedFormula.EXISTS ? theory.exists(vars, newBody)
- : theory.forall(vars, newBody);
- }
- setResult(newFormula);
- }
-
- public void postConvertAnnotation(final AnnotatedTerm old, final Annotation[] newAnnots, final Term newBody) {
- final Annotation[] annots = old.getAnnotations();
- Term result = old;
- if (newBody != old.getSubterm() || newAnnots != annots) {
- result = old.getTheory().annotatedTerm(newAnnots, newBody);
- }
- setResult(result);
- }
-
- public void preConvertMatchCase(final MatchTerm oldMatch, final int caseNr) {
- beginScope(oldMatch.getVariables()[caseNr]);
- pushTerm(oldMatch.getCases()[caseNr]);
- }
-
- public void postConvertMatch(final MatchTerm oldMatch, final Term newDataTerm, final Term[] newCases) {
- Term result = oldMatch;
- if (newDataTerm != oldMatch.getDataTerm() || newCases != oldMatch.getCases()) {
- final Theory theory = oldMatch.getTheory();
- result = theory.match(newDataTerm, oldMatch.getVariables(), newCases, oldMatch.getConstructors());
- }
- setResult(result);
- }
-
- /**
- * Transform a term.
- *
- * @param term
- * the term to transform.
- * @return the resulting transformed term.
- */
- public final Term transform(final Term term) {
- beginScope(new TermVariable[0]);
- run(new Convert(term));
- endScope();
- return mConverted.removeLast();
- }
-
- /**
- * Get a single converted term from the converted stack. This is the dual of
- * pushTerm() that is called after the term were removed from the todo stack and
- * pushed to the converted stack.
- *
- * @return the new converted term.
- */
- protected final Term getConverted() {
- return mConverted.removeLast();
- }
-
- /**
- * Get a single converted object array from the converted stack.
- *
- * @return the new converted object array.
- */
- protected final Object[] getConvertedObjectArray() {
- return mConvertedArrays.removeLast();
- }
-
- /**
- * Get the converted terms from the converted stack. This is the dual of
- * pushTerms() that is called after the term were removed from the todo stack
- * and pushed to the converted stack. It takes the old terms as argument and
- * checks for changes.
- *
- * @param oldArgs
- * the original arguments.
- * @return the new converted arguments. It will return the same array oldArgs if
- * there were no changes.
- */
- protected final Term[] getConverted(final Term[] oldArgs) {
- Term[] newArgs = oldArgs;
- for (int i = oldArgs.length - 1; i >= 0; i--) {
- final Term newTerm = getConverted();
- if (newTerm != oldArgs[i]) {
- if (newArgs == oldArgs) {
- newArgs = oldArgs.clone();
- }
- newArgs[i] = newTerm;
- }
- }
- return newArgs;
- }
-
- /**
- * Collect the arguments of an application term from the converted stack and
- * finish the conversion of appTerm. This is called after the arguments of
- * appTerm have been converted. It will put the converted term on the converted
- * stack and store it in the cache.
- */
- protected static class BuildApplicationTerm implements Walker {
- /** the application term to convert. */
- private final ApplicationTerm mAppTerm;
-
- public BuildApplicationTerm(final ApplicationTerm term) {
- mAppTerm = term;
- }
-
- @Override
- public void walk(final NonRecursive engine) {
- final TermTransformer transformer = (TermTransformer) engine;
- /* collect args and check if they have been changed */
- final Term[] oldArgs = mAppTerm.getParameters();
- final Term[] newArgs = transformer.getConverted(oldArgs);
- transformer.convertApplicationTerm(mAppTerm, newArgs);
- }
-
- @Override
- public String toString() {
- return mAppTerm.getFunction().getApplicationString();
- }
- }
-
- /**
- * Walker that is called after the variable values are transformed and before
- * the let body starts.
- */
- protected static class StartLetTerm implements Walker {
- /** the let term to convert. */
- private final LetTerm mLetTerm;
-
- public StartLetTerm(final LetTerm term) {
- mLetTerm = term;
- }
-
- @Override
- public void walk(final NonRecursive engine) {
- final TermTransformer transformer = (TermTransformer) engine;
- final Term[] values = transformer.getConverted(mLetTerm.getValues());
- transformer.preConvertLet(mLetTerm, values);
- }
-
- @Override
- public String toString() {
- return "let" + Arrays.toString(mLetTerm.getVariables());
- }
- }
-
- /**
- * Collect the sub term and the values of a let term from the converted stack
- * and finish the conversion of let term.
- */
- protected static class BuildLetTerm implements Walker {
- /** the let term to convert. */
- private final LetTerm mLetTerm;
- /** the converted values that are letted to the variables. */
- private final Term[] mNewValues;
-
- public BuildLetTerm(final LetTerm term, final Term[] newValues) {
- mLetTerm = term;
- mNewValues = newValues;
- }
-
- @Override
- public void walk(final NonRecursive engine) {
- final TermTransformer transformer = (TermTransformer) engine;
- final Term newBody = transformer.getConverted();
- transformer.postConvertLet(mLetTerm, mNewValues, newBody);
- transformer.endScope();
- }
-
- @Override
- public String toString() {
- return "let" + Arrays.toString(mLetTerm.getVariables());
- }
- }
-
- /**
- * Collect the sub term of a lambda term and build the converted formula. The
- * converted sub formula is expected to be on the converted stack. It stores the
- * converted quantifier on the converted stack and in the cache.
- */
- protected static class BuildLambda implements Walker {
- /** the quantifier to convert. */
- private final LambdaTerm mLambda;
-
- public BuildLambda(final LambdaTerm term) {
- mLambda = term;
- }
-
- @Override
- public void walk(final NonRecursive engine) {
- final TermTransformer transformer = (TermTransformer) engine;
- final Term sub = transformer.getConverted();
- transformer.postConvertLambda(mLambda, sub);
- transformer.endScope();
- }
-
- @Override
- public String toString() {
- return "lambda";
- }
- }
-
- /**
- * Collect the sub term of a quantified formula and build the converted formula.
- * The converted sub formula is expected to be on the converted stack. It stores
- * the converted quantifier on the converted stack and in the cache.
- */
- protected static class BuildQuantifier implements Walker {
- /** the quantifier to convert. */
- private final QuantifiedFormula mQuant;
-
- public BuildQuantifier(final QuantifiedFormula term) {
- mQuant = term;
- }
-
- @Override
- public void walk(final NonRecursive engine) {
- final TermTransformer transformer = (TermTransformer) engine;
- final Term sub = transformer.getConverted();
- transformer.postConvertQuantifier(mQuant, sub);
- transformer.endScope();
- }
-
- @Override
- public String toString() {
- return mQuant.getQuantifier() == QuantifiedFormula.EXISTS ? "exists" : "forall";
- }
- }
-
- /**
- * Collect the sub term and annotations of an annotated formula from the
- * converted stack. It converts the annotation and stores the result in the
- * cache and on the converted stack. Note that only Annotations that are of type
- * Term or Term[] are converted.
- */
- protected static class BuildAnnotation implements Walker {
- /** the annotated term. */
- private final AnnotatedTerm mAnnotatedTerm;
-
- public BuildAnnotation(final AnnotatedTerm term) {
- mAnnotatedTerm = term;
- }
-
- @Override
- public void walk(final NonRecursive engine) {
- final TermTransformer transformer = (TermTransformer) engine;
- final Annotation[] annots = mAnnotatedTerm.getAnnotations();
- Annotation[] newAnnots = annots;
- for (int i = annots.length - 1; i >= 0; i--) {
- final Object value = annots[i].getValue();
- Object newValue;
- if (value instanceof Term) {
- newValue = transformer.getConverted();
- } else if (value instanceof Object[]) {
- newValue = transformer.getConvertedObjectArray();
- } else {
- newValue = value;
- }
- if (newValue != value) {
- if (annots == newAnnots) {
- newAnnots = annots.clone();
- }
- newAnnots[i] = new Annotation(annots[i].getKey(), newValue);
- }
- }
- final Term sub = transformer.getConverted();
- transformer.postConvertAnnotation(mAnnotatedTerm, newAnnots, sub);
- }
-
- @Override
- public String toString() {
- return "annotate";
- }
- }
-
- /**
- * Collect the sub terms and sub arrays of an array (part of an annotated
- * formula).
- */
- protected static class BuildObjectArray implements Walker {
- private final Object[] mArray;
-
- public BuildObjectArray(final Object[] array) {
- mArray = array;
- }
-
- @Override
- public void walk(final NonRecursive engine) {
- final TermTransformer transformer = (TermTransformer) engine;
- Object[] newArray = mArray;
- for (int i = newArray.length - 1; i >= 0; i--) {
- final Object value = newArray[i];
- Object newValue;
- if (value instanceof Term) {
- newValue = transformer.getConverted();
- } else if (value instanceof Object[]) {
- newValue = transformer.getConvertedObjectArray();
- } else {
- newValue = value;
- }
- if (newValue != value) {
- if (mArray == newArray) {
- newArray = mArray.clone();
- }
- newArray[i] = newValue;
- }
- }
- transformer.mConvertedArrays.addLast(newArray);
- }
-
- @Override
- public String toString() {
- return "annotate";
- }
- }
-
- /**
- * Walk over each case of a match term, one after another.
- */
- protected static class WalkMatchTerm implements Walker {
- /** the match term. */
- private final MatchTerm mMatchTerm;
- /** the next case nr to walk through */
- private int mCaseNr;
-
- public WalkMatchTerm(final MatchTerm term) {
- mMatchTerm = term;
- mCaseNr = 0;
- }
-
- @Override
- public void walk(final NonRecursive engine) {
- final TermTransformer transformer = (TermTransformer) engine;
- final Term[] cases = mMatchTerm.getCases();
- if (mCaseNr > 0) {
- transformer.endScope();
- }
- if (mCaseNr < cases.length) {
- transformer.enqueueWalker(this);
- transformer.preConvertMatchCase(mMatchTerm, mCaseNr);
- mCaseNr++;
- } else {
- final Term[] newCases = transformer.getConverted(cases);
- final Term newDataTerm = transformer.getConverted();
- transformer.postConvertMatch(mMatchTerm, newDataTerm, newCases);
- }
- }
-
- @Override
- public String toString() {
- return "annotate";
- }
- }
-
- @Override
- public void reset() {
- super.reset();
- mConverted.clear();
- mCache.clear();
- mScopeMap.clear();
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/TermVariable.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/TermVariable.java
deleted file mode 100644
index 7dd0c69829d..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/TermVariable.java
+++ /dev/null
@@ -1,87 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see mTodo) {
- mTodo.add(toString());
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Theory.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Theory.java
deleted file mode 100644
index 3dcdf3cdb5d..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Theory.java
+++ /dev/null
@@ -1,1886 +0,0 @@
-/*
- * Copyright (C) 2009-2014 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see mFunFactory = new ScopedHashMap<>();
- private final UnifyHash mModelValueCache = new UnifyHash<>();
-
- private final ScopedHashMap mDeclaredSorts = new ScopedHashMap<>();
- private final ScopedHashMap mDeclaredFuns = new ScopedHashMap<>();
-
- private final UnifyHash mLetCache = new UnifyHash<>();
- private final UnifyHash mTermCache = new UnifyHash<>();
- private final UnifyHash mTvUnify = new UnifyHash<>();
- /**
- * Factory for to_real wrapper function symbol, if IRA logic is used.
- */
- private IRAWrapperFactory mIRAWrappers;
-
- public final ApplicationTerm mTrue, mFalse;
- public final FunctionSymbol mAnd, mOr, mNot, mImplies, mXor;
- public final PolymorphicFunctionSymbol mEquals, mDistinct;
-
- final static Sort[] EMPTY_SORT_ARRAY = Script.EMPTY_SORT_ARRAY;
- final static TermVariable[] EMPTY_TERM_VARIABLE_ARRAY = {};
- final static Term[] EMPTY_TERM_ARRAY = Script.EMPTY_TERM_ARRAY;
- /**
- * Pattern for model value variables '{@literal @}digits'.
- */
- private final static String MODEL_VALUE_PATTERN = "@\\d+";
- public final static String BITVEC_CONST_PATTERN = "bv\\d+";
-
- private int mTvarCtr = 0;
-
- private int mAuxCounter = 0;
-
- private boolean mGlobalDecls;
-
- public Theory() {
- mTrue = mFalse = null;
- mAnd = mOr = mNot = mImplies = mXor = null;
- mEquals = mDistinct = null;
- }
-
- public Theory(final Logics logic) {
- this(logic, null);
- }
-
- /**
- * Create the term factory. The solver setup should be used to create internal function symbols, e.g., to represent
- * proof objects.
- *
- * @param logic
- * The logic to use.
- * @param solverSetup
- * The solver-specific setup delegate.
- */
- public Theory(final Logics logic, final SolverSetup solverSetup) {
- mSolverSetup = solverSetup;
- final Sort[] noarg = new Sort[0];
- mBooleanSort = declareInternalSort("Bool", 0, 0).getSort(null, noarg);
- final Sort[] generic1 = createSortVariables("A");
- final Sort[] bool1 = new Sort[] { mBooleanSort };
- final Sort[] bool2 = new Sort[] { mBooleanSort, mBooleanSort };
- final Sort[] generic2 = new Sort[] { generic1[0], generic1[0] };
- final int leftassoc = FunctionSymbol.LEFTASSOC;
- mNot = declareInternalFunction("not", bool1, mBooleanSort, 0);
- mAnd = declareInternalFunction("and", bool2, mBooleanSort, leftassoc);
- mOr = declareInternalFunction("or", bool2, mBooleanSort, leftassoc);
- mImplies = declareInternalFunction("=>", bool2, mBooleanSort, FunctionSymbol.RIGHTASSOC);
- mEquals = declareInternalPolymorphicFunction("=", generic1, generic2, mBooleanSort, FunctionSymbol.CHAINABLE);
- mDistinct = declareInternalPolymorphicFunction("distinct", generic1, generic2, mBooleanSort,
- FunctionSymbol.PAIRWISE);
- mXor = declareInternalFunction("xor", bool2, mBooleanSort, leftassoc);
- declareInternalPolymorphicFunction("ite", generic1, new Sort[] { mBooleanSort, generic1[0], generic1[0] },
- generic1[0], 0);
- mTrue = (ApplicationTerm) term(declareInternalFunction("true", noarg, mBooleanSort, 0));
- mFalse = (ApplicationTerm) term(declareInternalFunction("false", noarg, mBooleanSort, 0));
- declareInternalSort(SMTLIBConstants.FUNC, 2, SortSymbol.FUNCTION);
-
- // Finally, declare logic specific functions
- setLogic(logic);
- }
-
- /**
- * Method to check if indices is a numeral or symbol. If numeral return as BigInteger, if symbol return null
- */
- public BigInteger toNumeral(final String index) {
- try {
- return new BigInteger(index);
- } catch (final NumberFormatException e) {
- throw new SMTLIBException("not a numeral: " + index, e);
- }
- }
-
- /**
- * Method to check if the parameter is the name of a constructor. If so, return the constructor.
- */
- public FunctionSymbol getFunctionSymbol(final String constructor) {
- return mDeclaredFuns.get(constructor);
- }
-
- /******************** LOGICAL OPERATORS *******************************/
-
- private Term simplifyAndOr(final FunctionSymbol connector, final Term... subforms) {
- final Term neutral = (connector == mAnd ? mTrue : mFalse);
- final LinkedHashSet formulas = new LinkedHashSet<>();
-
- for (final Term f : subforms) {
- if (f == mTrue || f == mFalse) {
- if (f == neutral) {
- continue;
- }
- return f;
- }
-
- /* Normalize nested and/ors */
- if (f instanceof ApplicationTerm && ((ApplicationTerm) f).getFunction() == connector) {
- for (final Term subf : ((ApplicationTerm) f).getParameters()) {
- formulas.add(subf);
- }
- } else {
- formulas.add(f);
- }
- }
- if (formulas.size() <= 1) { // NOPMD
- if (formulas.isEmpty()) {
- return neutral;
- }
- return formulas.iterator().next();
- }
- final Term[] arrforms = formulas.toArray(new Term[formulas.size()]);
- return term(connector, arrforms);
- }
-
- public Term not(final Term f) {
- if (f == mTrue) {
- return mFalse;
- }
- if (f == mFalse) {
- return mTrue;
- }
- if (f instanceof ApplicationTerm && ((ApplicationTerm) f).getFunction() == mNot) {
- return ((ApplicationTerm) f).getParameters()[0];
- }
- return term(mNot, f);
- }
-
- public Term and(final Term... subforms) {
- return simplifyAndOr(mAnd, subforms);
- }
-
- public Term or(final Term... subforms) {
- return simplifyAndOr(mOr, subforms);
- }
-
- public Term implies(final Term f, final Term g) {
- if (g == mTrue || f == mTrue) {
- return g;
- }
- if (f == mFalse) {
- return mTrue;
- }
- if (g == mFalse) {
- return not(f);
- }
- if (f == g) {
- return mTrue;
- }
- return term(mImplies, f, g);
- }
-
- public Term xor(final Term f, final Term g) {
- if (f == mTrue) {
- return not(g);
- }
- if (g == mTrue) {
- return not(f);
- }
- if (f == mFalse) {
- return g;
- }
- if (g == mFalse) {
- return f;
- }
- if (f == g) {
- return mFalse;
- }
- return term(mXor, f, g);
- }
-
- public Term ifthenelse(final Term c, final Term t, final Term e) {
- if (c == mTrue) {
- return t;
- }
- if (c == mFalse) {
- return e;
- }
- if (t == e) {
- return t;
- }
- if (t == mTrue && e == mFalse) {
- return c;
- }
- if (t == mFalse && e == mTrue) {
- return not(c);
- }
- if (t == mTrue) {
- return term(mOr, c, e);
- }
- if (t == mFalse) {
- return term(mAnd, term(mNot, c), e);
- }
- if (e == mTrue) {
- return term(mImplies, c, t);
- }
- if (e == mFalse) {
- return term(mAnd, c, t);
- }
- return term("ite", c, t, e);
- }
-
- public Term lambda(final TermVariable[] vars, final Term subterm) {
- final int hash = LambdaTerm.hashLambda(vars, subterm);
- for (final Term term : mTermCache.iterateHashCode(hash)) {
- if (term instanceof LambdaTerm) {
- final LambdaTerm lambda = (LambdaTerm) term;
- if (lambda.getSubterm() == subterm && Arrays.equals(lambda.getVariables(), vars)) {
- return lambda;
- }
- }
- }
- final LambdaTerm lambda = new LambdaTerm(vars, subterm, hash);
- mTermCache.put(hash, lambda);
- return lambda;
- }
-
- private Term quantify(final int quant, final TermVariable[] vars, final Term f) {
- final int hash = QuantifiedFormula.hashQuantifier(quant, vars, f);
- for (final Term term : mTermCache.iterateHashCode(hash)) {
- if (term instanceof QuantifiedFormula) {
- final QuantifiedFormula qf = (QuantifiedFormula) term;
- if (qf.getQuantifier() == quant && qf.getSubformula() == f && Arrays.equals(vars, qf.getVariables())) {
- return qf;
- }
- }
- }
- final QuantifiedFormula qf = new QuantifiedFormula(quant, vars, f, hash);
- mTermCache.put(hash, qf);
- return qf;
- }
-
- public Term exists(final TermVariable[] vars, final Term f) {
- return quantify(QuantifiedFormula.EXISTS, vars, f);
- }
-
- public Term forall(final TermVariable[] vars, final Term f) {
- return quantify(QuantifiedFormula.FORALL, vars, f);
- }
-
- public Term match(final Term dataArg, final TermVariable[][] vars, final Term[] cases,
- final DataType.Constructor[] constructors) {
-
- final int hash = MatchTerm.hashMatch(dataArg, vars, cases);
- for (final Term t : mTermCache.iterateHashCode(hash)) {
- if (t instanceof MatchTerm) {
- final MatchTerm mt = (MatchTerm) t;
- if (mt.getDataTerm() == dataArg && Arrays.equals(mt.getCases(), cases)
- && Arrays.deepEquals(mt.getVariables(), vars)
- && Arrays.equals(mt.getConstructors(), constructors)) {
- return mt;
- }
- }
- }
- final MatchTerm mt = new MatchTerm(hash, dataArg, vars, cases, constructors);
- mTermCache.put(hash, mt);
- return mt;
- }
-
- public Term let(final TermVariable[] vars, final Term[] values, final Term subform) {
- assert (vars.length == values.length);
- if (vars.length == 0) {
- return subform;
- }
- final int hash = LetTerm.hashLet(vars, values, subform);
- for (final LetTerm lt : mLetCache.iterateHashCode(hash)) {
- if (lt.getSubTerm() == subform && Arrays.equals(lt.getVariables(), vars)
- && Arrays.equals(lt.getValues(), values)) {
- return lt;
- }
- }
- final LetTerm lf = new LetTerm(vars, values, subform, hash);
- mLetCache.put(hash, lf);
- return lf;
- }
-
- public Term let(final TermVariable var, final Term value, final Term subform) {
- return let(new TermVariable[] { var }, new Term[] { value }, subform);
- }
-
- public Term distinct(final Term... terms) {
- if (terms.length < 2) {
- return null;
- }
- if (terms.length == 2) {
- if (terms[0] == terms[1]) {
- return mFalse;
- }
- if (terms[0].getSort() == mBooleanSort) {
- if (terms[0] == mFalse) {
- return terms[1];
- }
- if (terms[1] == mFalse) {
- return terms[0];
- }
- if (terms[0] == mTrue) {
- return not(terms[1]);
- }
- if (terms[1] == mTrue) {
- return not(terms[0]);
- }
- }
- return term(mDistinct, terms);
- }
- final HashSet params = new HashSet<>(Arrays.asList(terms));
- if (params.size() != terms.length) {
- // We had something like (distinct ... a ... a ...)
- return mFalse;
- }
- return term(mDistinct, terms);
- }
-
- public Term equals(final Term... terms) {
- if (terms.length < 2) {
- return null;
- }
- if (terms.length == 2) {
- if (terms[0] == terms[1]) {
- return mTrue;
- }
- if (terms[0].getSort() == mBooleanSort) {
- if (terms[0] == mTrue) {
- return terms[1];
- }
- if (terms[1] == mTrue) {
- return terms[0];
- }
- if (terms[0] == mFalse) {
- return not(terms[1]);
- }
- if (terms[1] == mFalse) {
- return not(terms[0]);
- }
- }
- return term(mEquals, terms);
- }
- final HashSet params = new HashSet<>(Arrays.asList(terms));
- if (params.size() == 1) {
- // We had (= a a ... a)
- return mTrue;
- }
- return term(mEquals, terms);
- }
-
- /******************** CONSTANTS *************************************/
-
- public Term constant(final Object value, final Sort sort) {
- if (value instanceof Rational) {
- if (!sort.isNumericSort()) {
- throw new SMTLIBException("Not a numeric sort");
- }
- final Rational v = (Rational) value;
- if (!v.isRational()) {
- throw new SMTLIBException("Infinite/NaN value");
- }
- if (sort.getName().equals("Int") && !v.isIntegral()) {
- throw new SMTLIBException("Non-integral value with integer sort");
- }
- }
- if (sort.isBitVecSort()) {
- if (value instanceof BigInteger) {
- final BigInteger intValue = (BigInteger) value;
- if (intValue.signum() < 0 || intValue.bitLength() > Integer.valueOf(sort.getIndices()[0])) {
- throw new SMTLIBException("Bitvector constant out of range");
- }
- }
- }
- final int hash = ConstantTerm.hashConstant(value, sort);
- for (final Term t : mTermCache.iterateHashCode(hash)) {
- if (t instanceof ConstantTerm) {
- final ConstantTerm nt = (ConstantTerm) t;
- if (nt.getSort() == sort && value.equals(nt.getValue())) {
- return nt;
- }
- }
- }
- final ConstantTerm nt = new ConstantTerm(value, sort, hash);
- mTermCache.put(hash, nt);
- return nt;
- }
-
- public Term numeral(final BigInteger num) {
- if (mNumericSort != mRealSort) {
- // For integer sort, always use Rational constants for numerals.
- return constant(Rational.valueOf(num, BigInteger.ONE), mNumericSort);
- }
- // For real arithmetic using Rational would convert to decimal, which we want to avoid.
- // positive and negated numerals are represented as constants of BigInteger type
- // instead.
- return constant(num, mNumericSort);
- }
-
- public Term numeral(final String num) {
- return numeral(toNumeral(num));
- }
-
- public Term decimal(final BigDecimal value) {
- // Check if this is uses the default scale and no fractional part.
- // In this case we create a rational constant instead.
- // Also handle BigDecimal without scale to distinguish them from numerals.
- if (value.scale() <= 0 || (value.scale() == 1 && value.remainder(BigDecimal.ONE).signum() == 0)) {
- return constant(Rational.valueOf(value.toBigIntegerExact(), BigInteger.ONE), mRealSort);
- }
- // If the input contains something like 0.1, don't automatically convert to (/ 1.0 10.0), to avoid
- // changing the input.
- Term result = constant(value.abs(), mRealSort);
- // positive non-normalized decimals are represented as BigDecimal constants
- // negative BigDecimals like -0.1 are normalized to the SMT term (- 0.1)
- if (value.signum() < 0) {
- final FunctionSymbol neg = getFunction("-", mRealSort);
- result = term(neg, result);
- }
- return result;
- }
-
- public Term decimal(final String value) {
- return decimal(new BigDecimal(value));
- }
-
- /**
- * Convert a rational constant to a term of the correct sort. The constant must be integral if the sort is integer.
- *
- * @param c
- * the constant to convert.
- * @param sort
- * the sort; either Real or Int.
- * @return an smt term representing constant c.
- */
- public Term rational(final Rational c, final Sort sort) {
- return constant(c, sort);
- }
-
- public Term binary(final String value) {
- assert value.startsWith("#b");
- if (mBitVecSort == null) {
- return null;
- }
- final String bsize = String.valueOf(value.length() - 2);
- final Sort sort = mBitVecSort.getSort(new String[] { bsize }, new Sort[0]);
- return new ConstantTerm(value, sort, ConstantTerm.hashConstant(value, sort));
- }
-
- public Term hexadecimal(final String value) {
- assert value.startsWith("#x");
- if (mBitVecSort == null) {
- return null;
- }
- final String bsize = String.valueOf(4 * (value.length() - 2));// NOCHECKSTYLE
- final Sort sort = mBitVecSort.getSort(new String[] { bsize }, new Sort[0]);
- return new ConstantTerm(value, sort, ConstantTerm.hashConstant(value, sort));
- }
-
- public Term modelRational(final Rational rat, final Sort sort) {
- final BigInteger num = rat.numerator();
- final BigInteger denom = rat.denominator();
-
- if (sort == mRealSort) {
- if (mLogic.isIRA()) {
- final FunctionSymbol div = getFunction("/", mRealSort, mRealSort);
- final FunctionSymbol toreal = getFunction("to_real", mNumericSort);
- Term numeralTerm = term(toreal, numeral(num.abs()));
- if (num.signum() < 0) {
- numeralTerm = term("-", numeralTerm);
- }
- return term(div, numeralTerm, term(toreal, numeral(denom)));
- } else {
- if (denom.equals(BigInteger.ONE)) {
- return decimal(new BigDecimal(num));
- }
- final FunctionSymbol div = getFunction("/", mNumericSort, mNumericSort);
- return term(div, numeral(num), numeral(denom));
- }
- } else {
- assert denom.equals(BigInteger.ONE);
- return numeral(rat.numerator());
- }
- }
-
- public Term string(final QuotedObject value) {
- return constant(value, mStringSort);
- }
-
- /******************** LOGICS AND THEORIES ********************************/
- public Logics getLogic() {
- return mLogic;
- }
-
- public FunctionSymbol declareInternalFunction(final String name, final Sort[] paramTypes, final Sort resultType,
- final int flags) {
- return defineFunction(name, paramTypes, resultType, null, null, flags | FunctionSymbol.INTERNAL);
- }
-
- public FunctionSymbol declareInternalFunction(final String name, final Sort[] paramTypes,
- final TermVariable[] defVars, final Term definition, final int flags) {
- return defineFunction(name, paramTypes, definition.getSort(), defVars, definition,
- flags | FunctionSymbol.INTERNAL);
- }
-
- public PolymorphicFunctionSymbol declareInternalPolymorphicFunction(final String name, final Sort[] sortParams,
- final Sort[] paramTypes, final Sort resultType, final int flags) {
- assert !mFunFactory.containsKey(name);
- final PolymorphicFunctionSymbol f = new PolymorphicFunctionSymbol(name, sortParams, paramTypes, resultType,
- flags | FunctionSymbol.INTERNAL);
- declareInternalFunctionFactory(f);
- return f;
- }
-
- class MinusFunctionFactory extends FunctionSymbolFactory {
- Sort mSort1, mSort2;
-
- public MinusFunctionFactory(final Sort sort1, final Sort sort2) {
- super(SMTLIBConstants.MINUS);
- mSort1 = sort1;
- mSort2 = sort2;
- }
-
- @Override
- public int getFlags(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- return paramSorts.length == 1 ? FunctionSymbol.INTERNAL
- : FunctionSymbol.LEFTASSOC | FunctionSymbol.INTERNAL;
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices != null || paramSorts.length == 0 || paramSorts.length > 2 || resultSort != null
- || (paramSorts[0] != mSort1 && paramSorts[0] != mSort2)) {
- return null;
- }
-
- if (paramSorts.length == 2 && paramSorts[0] != paramSorts[1]) {
- return null;
- }
-
- return paramSorts[0];
- }
- }
-
- class DivisibleFunctionFactory extends FunctionSymbolFactory {
- public DivisibleFunctionFactory() {
- super("divisible");
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- return indices != null && indices.length == 1 && toNumeral(indices[0]).signum() > 0
- && paramSorts.length == 1 && paramSorts[0] == mNumericSort && resultSort == null ? mBooleanSort
- : null;
- }
- }
-
- private Term absDefinition(final TermVariable x) {
- final Term zero = Rational.ZERO.toTerm(x.getSort());
- return term(SMTLIBConstants.ITE, term(SMTLIBConstants.LT, x, zero), term(SMTLIBConstants.MINUS, x), x);
- }
-
- private void createNumericOperators(final Sort sort, final boolean isRealArith) {
- final Sort[] sort1 = new Sort[] { sort };
- final Sort[] sort2 = new Sort[] { sort, sort };
- declareInternalFunction(SMTLIBConstants.PLUS, sort2, sort, FunctionSymbol.LEFTASSOC);
- declareInternalFunctionFactory(new MinusFunctionFactory(sort, sort));
- declareInternalFunction(SMTLIBConstants.MUL, sort2, sort, FunctionSymbol.LEFTASSOC);
- /* the functions /, div and mod are partial (for division by 0) and thus partially uninterpreted */
- if (isRealArith) {
- declareInternalFunction(SMTLIBConstants.DIVIDE, sort2, sort,
- FunctionSymbol.LEFTASSOC | FunctionSymbol.UNINTERPRETEDINTERNAL);
- } else {
- declareInternalFunction(SMTLIBConstants.DIV, sort2, sort,
- FunctionSymbol.LEFTASSOC | FunctionSymbol.UNINTERPRETEDINTERNAL);
- declareInternalFunction(SMTLIBConstants.MOD, sort2, sort, FunctionSymbol.UNINTERPRETEDINTERNAL);
- declareInternalFunctionFactory(new DivisibleFunctionFactory());
- }
- final Sort sBool = mBooleanSort;
- declareInternalFunction(SMTLIBConstants.GT, sort2, sBool, FunctionSymbol.CHAINABLE);
- declareInternalFunction(SMTLIBConstants.GEQ, sort2, sBool, FunctionSymbol.CHAINABLE);
- declareInternalFunction(SMTLIBConstants.LT, sort2, sBool, FunctionSymbol.CHAINABLE);
- declareInternalFunction(SMTLIBConstants.LEQ, sort2, sBool, FunctionSymbol.CHAINABLE);
-
- final TermVariable x = createTermVariable("x", sort);
- declareInternalFunction(SMTLIBConstants.ABS, sort1, new TermVariable[] { x }, absDefinition(x), 0);
- }
-
- private void createIRAOperators() {
- mIRAWrappers = new IRAWrapperFactory();
- class BinArithFactory extends FunctionSymbolFactory {
- Sort mReturnSort;
- int mFlags;
-
- BinArithFactory(final String name, final Sort returnSort, final int flags) {
- super(name);
- mReturnSort = returnSort;
- mFlags = flags | FunctionSymbol.INTERNAL;
- }
-
- @Override
- public int getFlags(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- return mFlags;
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null && paramSorts.length == 2 && paramSorts[0] == paramSorts[1]
- && (paramSorts[0] == mNumericSort || paramSorts[0] == mRealSort) && resultSort == null) {
- return mReturnSort == null ? paramSorts[0] : mReturnSort;
- }
- return null;
- }
- }
-
- declareInternalFunctionFactory(new BinArithFactory("+", null, FunctionSymbol.LEFTASSOC));
- declareInternalFunctionFactory(new MinusFunctionFactory(mNumericSort, mRealSort));
- declareInternalFunctionFactory(new BinArithFactory("*", null, FunctionSymbol.LEFTASSOC));
- declareInternalFunctionFactory(new BinArithFactory(">", mBooleanSort, FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new BinArithFactory(">=", mBooleanSort, FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new BinArithFactory("<", mBooleanSort, FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new BinArithFactory("<=", mBooleanSort, FunctionSymbol.CHAINABLE));
-
- final Sort[] int1 = new Sort[] { mNumericSort };
- final Sort[] int2 = new Sort[] { mNumericSort, mNumericSort };
- final Sort[] real1 = new Sort[] { mRealSort };
- final Sort[] real2 = new Sort[] { mRealSort, mRealSort };
- declareInternalFunction("/", real2, mRealSort, FunctionSymbol.LEFTASSOC);
- declareInternalFunction("div", int2, mNumericSort, FunctionSymbol.LEFTASSOC);
- declareInternalFunctionFactory(new DivisibleFunctionFactory());
- declareInternalFunction("to_real", int1, mRealSort, 0);
- declareInternalFunction("to_int", real1, mNumericSort, 0);
-
- declareInternalFunction("mod", int2, mNumericSort, 0);
- final TermVariable xr = createTermVariable("x1", mRealSort);
- // isint x: (= x (to_real (to_int x)))
- final Term isintx = term("=", xr, term("to_real", term("to_int", xr)));
- declareInternalFunction("is_int", real1, new TermVariable[] { xr }, isintx, 0);
-
- declareInternalFunctionFactory(new FunctionSymbolFactory("abs") {
- @Override
- public Term getDefinition(final TermVariable[] tvs, final Sort resultSort) {
- return absDefinition(tvs[0]);
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null && paramSorts.length == 1
- && (paramSorts[0] == mNumericSort || paramSorts[0] == mRealSort) && resultSort == null) {
- return paramSorts[0];
- }
- return null;
- }
- });
-
- }
-
- private void createArrayOperators() {
- final Sort[] generic2 = createSortVariables("X", "Y");
- final SortSymbol arraySort = declareInternalSort("Array", 2, SortSymbol.ARRAY);
-
- // (Array X Y)
- final Sort array = arraySort.getSort(null, generic2);
- // select : ((Array X Y) X) -> Y
- declareInternalPolymorphicFunction("select", generic2, new Sort[] { array, generic2[0] }, generic2[1], 0);
- // store : ((Array X Y) X Y) -> (Array X Y)
- declareInternalPolymorphicFunction("store", generic2, new Sort[] { array, generic2[0], generic2[1] }, array, 0);
- // const : (Y) -> (Array X Y)
- declareInternalPolymorphicFunction(SMTLIBConstants.CONST, generic2, new Sort[] { generic2[1] }, array,
- FunctionSymbol.INTERNAL | FunctionSymbol.RETURNOVERLOAD);
- final Sort lambdaSort = getSort(SMTLIBConstants.FUNC, generic2);
- // arrayof : (-> X Y) -> (Array X Y)
- declareInternalPolymorphicFunction(SMTLIBConstants.ARRAYOF, generic2, new Sort[] { lambdaSort }, array,
- FunctionSymbol.INTERNAL | FunctionSymbol.RETURNOVERLOAD);
- }
-
- private void createBitVecSort() {
- mBitVecSort = new SortSymbol(this, "BitVec", 0, null, SortSymbol.INTERNAL | SortSymbol.INDEXED) {
- @Override
- public void checkArity(final String[] indices, final int arity) {
- if (indices == null || indices.length != 1) {
- throw new IllegalArgumentException("BitVec needs one index");
- }
- if (toNumeral(indices[0]).signum() <= 0) {
- throw new IllegalArgumentException("BitVec index must be positive");
- }
- if (arity != 0) {
- throw new IllegalArgumentException("BitVec has no parameters");
- }
- }
- };
- mDeclaredSorts.put("BitVec", mBitVecSort);
- }
-
- private void createBitVecOperators() {
- class RegularBitVecFunction extends FunctionSymbolFactory {
- int mNumArgs;
- int mFlags;
- Sort mResult;
-
- public RegularBitVecFunction(final String name, final int numArgs, final Sort result, final int flags) {
- super(name);
- mNumArgs = numArgs;
- mResult = result;
- mFlags = flags;
- }
-
- public RegularBitVecFunction(final String name, final int numArgs, final Sort result) {
- this(name, numArgs, result, FunctionSymbol.INTERNAL);
- }
-
- @Override
- public int getFlags(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- return mFlags;
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices != null || paramSorts.length != mNumArgs || resultSort != null
- || paramSorts[0].getName() != "BitVec") {
- return null;
- }
- for (int i = 1; i < mNumArgs; i++) {
- if (paramSorts[i] != paramSorts[0]) {
- return null;
- }
- }
- return mResult == null ? paramSorts[0] : mResult;
- }
- }
- class ExtendBitVecFunction extends FunctionSymbolFactory {
- public ExtendBitVecFunction(final String name) {
- super(name);
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 1 || paramSorts.length != 1 || resultSort != null
- || paramSorts[0].getName() != "BitVec") {
- return null;
- }
- final BigInteger size = toNumeral(indices[0]).add(toNumeral(paramSorts[0].getIndices()[0]));
- return mBitVecSort.getSort(new String[] { size.toString() }, new Sort[0]);
- }
- }
- class RotateBitVecFunction extends FunctionSymbolFactory {
- public RotateBitVecFunction(final String name) {
- super(name);
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 1 || paramSorts.length != 1 || resultSort != null
- || paramSorts[0].getName() != "BitVec") {
- return null;
- }
- return paramSorts[0];
- }
- }
- class Bv2NatFunction extends FunctionSymbolFactory {
- public Bv2NatFunction(final String name) {
- super(name);
- assert name.equals("bv2nat") : "Wrong name: " + name;
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices != null || paramSorts.length != 1 || paramSorts[0].getName() != "BitVec"
- || resultSort != null) {
- return null;
- }
- return mNumericSort;
- }
- }
- class Nat2BvFunction extends FunctionSymbolFactory {
- public Nat2BvFunction(final String name) {
- super(name);
- assert name.equals("nat2bv") : "Wrong name: " + name;
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 1 || paramSorts.length != 1
- || !paramSorts[0].getName().equals("Int") || resultSort != null) {
- return null;
- }
- return mBitVecSort.getSort(indices);
- }
- }
- declareInternalFunctionFactory(new FunctionSymbolFactory("concat") {
- @Override
- public int getFlags(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- return FunctionSymbol.INTERNAL;
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices != null || paramSorts.length != 2 || resultSort != null
- || paramSorts[0].getName() != "BitVec" || paramSorts[1].getName() != "BitVec") {
- return null;
- }
-
- final BigInteger paramSortAsInt0 = toNumeral(paramSorts[0].getIndices()[0]);
- final BigInteger paramSortAsInt1 = toNumeral(paramSorts[1].getIndices()[0]);
-
- final BigInteger size = paramSortAsInt0.add(paramSortAsInt1);
- // before: final BigInteger size = paramSorts[0].getIndices()[0].add(paramSorts[1].getIndices()[0]);
- return mBitVecSort.getSort(new String[] { size.toString() }, new Sort[0]);
- // what does { size } ?
- }
- });
- declareInternalFunctionFactory(new FunctionSymbolFactory("extract") {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length < 2 || paramSorts.length != 1 || resultSort != null
- || paramSorts[0].getName() != "BitVec") {
- return null;
- }
- final BigInteger idxFirst = toNumeral(indices[0]);
- final BigInteger idxScnd = toNumeral(indices[1]);
- final BigInteger paramLength = toNumeral(paramSorts[0].getIndices()[0]);
- if (idxFirst.compareTo(idxScnd) < 0 || paramLength.compareTo(idxFirst) < 0) {
- return null;
- }
- final BigInteger size = idxFirst.subtract(idxScnd).add(BigInteger.ONE);
- return mBitVecSort.getSort(new String[] { size.toString() }, new Sort[0]);
- }
- });
- final Sort bitvec1 = mBitVecSort.getSort(new String[] { BigInteger.ONE.toString() }, new Sort[0]);
-
- declareInternalFunctionFactory(new RegularBitVecFunction("bvnot", 1, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvand", 2, null, FunctionSymbol.INTERNAL | FunctionSymbol.LEFTASSOC));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvor", 2, null, FunctionSymbol.INTERNAL | FunctionSymbol.LEFTASSOC));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvneg", 1, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvadd", 2, null, FunctionSymbol.INTERNAL | FunctionSymbol.LEFTASSOC));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvmul", 2, null, FunctionSymbol.INTERNAL | FunctionSymbol.LEFTASSOC));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvudiv", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvurem", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvshl", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvlshr", 2, null));
-
- declareInternalFunctionFactory(new RegularBitVecFunction("bvnand", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvnor", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvxor", 2, null, FunctionSymbol.INTERNAL | FunctionSymbol.LEFTASSOC));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvxnor", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvcomp", 2, bitvec1));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvsub", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvsdiv", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvsrem", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvsmod", 2, null));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvashr", 2, null));
-
- declareInternalFunctionFactory(new FunctionSymbolFactory("repeat") {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 1 || paramSorts.length != 1 || resultSort != null
- || paramSorts[0].getName() != "BitVec") {
- return null;
- }
- final BigInteger size = toNumeral(indices[0]).multiply(toNumeral(paramSorts[0].getIndices()[0]));
- return mBitVecSort.getSort(new String[] { size.toString() }, new Sort[0]);
- }
- });
- declareInternalFunctionFactory(new ExtendBitVecFunction("zero_extend"));
- declareInternalFunctionFactory(new ExtendBitVecFunction("sign_extend"));
- declareInternalFunctionFactory(new RotateBitVecFunction("rotate_left"));
- declareInternalFunctionFactory(new RotateBitVecFunction("rotate_right"));
-
- declareInternalFunctionFactory(new RegularBitVecFunction("bvult", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvule", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvugt", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvuge", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvslt", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvsle", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvsgt", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularBitVecFunction("bvsge", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
-
- declareInternalFunctionFactory(new Bv2NatFunction("bv2nat"));
- declareInternalFunctionFactory(new Nat2BvFunction("nat2bv"));
-
-
-
- }
-
- private void createFloatingPointOperators() {
-
- mFloatingPointSort = new SortSymbol(this, "FloatingPoint", 0, null, SortSymbol.INTERNAL | SortSymbol.INDEXED) {
- @Override
- public void checkArity(final String[] indices, final int arity) {
- if (indices == null || indices.length != 2) {
- throw new IllegalArgumentException("Floating Point needs two indices");
- }
-
- if (toNumeral(indices[0]).signum() <= 0 || toNumeral(indices[1]).signum() <= 0) {
- throw new IllegalArgumentException("FloatingPoint indices must be greater 0");
- }
-
- if (arity != 0) {
- throw new IllegalArgumentException("FloatingPoint has no parameters");
- }
- }
- };
-
- mDeclaredSorts.put("FloatingPoint", mFloatingPointSort);
- mRoundingModeSort = declareInternalSort("RoundingMode", 0, 0).getSort(null, new Sort[0]);
-
- /*
- * Used to create Functions of the Floating Point theory
- */
- class RegularFloatingPointFunction extends FunctionSymbolFactory {
- int mNumArgs;
- Sort mResult;
- int mFlags;
- int mFirstFloat;
-
- public RegularFloatingPointFunction(final String name, final int numArgs, final Sort result,
- final int flags) {
- super(name);
- mNumArgs = numArgs;
- mResult = result;
- mFlags = flags;
- }
-
- @Override
- public int getFlags(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- return mFlags;
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices != null || paramSorts.length != mNumArgs || resultSort != null) {
- return null;
- }
- if (paramSorts[0].getName() == ("RoundingMode")) {
- mFirstFloat = 1;
- } else {
- mFirstFloat = 0;
- }
- for (int i = mFirstFloat; i < mNumArgs; i++) {
- if (paramSorts[i].getName() != "FloatingPoint") {
- return null;
- }
- }
- return mResult == null ? paramSorts[mFirstFloat] : mResult;
- }
- }
-
- declareInternalFunctionFactory(new FunctionSymbolFactory("fp") {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices != null || paramSorts.length != 3 || resultSort != null
- || paramSorts[0].getName() != "BitVec" || paramSorts[1].getName() != "BitVec"
- || paramSorts[2].getName() != "BitVec") {
- return null;
- }
- final BigInteger fpSignIndex = toNumeral(paramSorts[0].getIndices()[0]);
- if (!fpSignIndex.equals(BigInteger.ONE)) {
- return null;
- }
- final String[] fpIndices = new String[2];
- fpIndices[0] = toNumeral(paramSorts[1].getIndices()[0]).toString();
- fpIndices[1] = toNumeral(paramSorts[2].getIndices()[0]).add(BigInteger.ONE).toString();
- return mFloatingPointSort.getSort(fpIndices, new Sort[0]);
- }
- });
-
- // from BitVec to FP
- declareInternalFunctionFactory(new FunctionSymbolFactory("to_fp") {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 2 || paramSorts == null) {
- return null;
- }
- // from BitVec to FP
- if (paramSorts.length == 1 && paramSorts[0].getName() == "BitVec") {
- if (!((toNumeral(indices[0]).add(toNumeral(indices[1]))
- .equals(toNumeral(paramSorts[0].getIndices()[0]))))) {
- return null;
- }
- return mFloatingPointSort.getSort(indices, new Sort[0]);
- }
-
- // from FP to FP
- if (paramSorts.length == 2 && paramSorts[0].getName() == "RoundingMode"
- && (paramSorts[1].getName() == "FloatingPoint")) {
- return mFloatingPointSort.getSort(indices, new Sort[0]);
- }
-
- // from real to FP
- if (paramSorts.length == 2 && paramSorts[0].getName() == "RoundingMode"
- && paramSorts[1].getName() == "Real") {
- return mFloatingPointSort.getSort(indices, new Sort[0]);
- }
-
- // from signed machine integer, represented as a 2's complement bit vector to FP
- if (paramSorts.length == 2 && paramSorts[0].getName() == "RoundingMode"
- && paramSorts[1].getName() == "BitVec") {
- return mFloatingPointSort.getSort(indices, new Sort[0]);
- }
- return null;
- }
- });
-
- declareInternalFunctionFactory(new FunctionSymbolFactory("to_fp_unsigned") {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 2 || paramSorts.length != 2 || resultSort != null
- || paramSorts[0].getName() != "RoundingMode" || paramSorts[1].getName() != "BitVec") {
- return null;
- }
- return mFloatingPointSort.getSort(indices, new Sort[0]);
- }
- });
-
- declareInternalFunctionFactory(new FunctionSymbolFactory("fp.to_ubv") {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 1 || paramSorts.length != 2 || resultSort != null
- || paramSorts[0].getName() != "RoundingMode" || paramSorts[1].getName() != "FloatingPoint") {
- return null;
- }
- return mBitVecSort.getSort(new String[] { indices[0] }, new Sort[0]);
- }
- });
-
- declareInternalFunctionFactory(new FunctionSymbolFactory("fp.to_sbv") {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 1 || paramSorts.length != 2 || resultSort != null
- || paramSorts[0].getName() != "RoundingMode" || paramSorts[1].getName() != "FloatingPoint") {
- return null;
- }
- return mBitVecSort.getSort(new String[] { indices[0] }, new Sort[0]);
- }
- });
-
- /*
- * Used to create Constants of the Floating Point theory
- */
- class FloatingPointConstant extends FunctionSymbolFactory {
- public FloatingPointConstant(final String name) {
- super(name);
- }
-
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices.length != 2 || paramSorts.length != 0 || resultSort != null) {
- return null;
- }
- return mFloatingPointSort.getSort(indices, new Sort[0]);
- }
- }
- // +/- infinity
- declareInternalFunctionFactory(new FloatingPointConstant("+oo"));
- declareInternalFunctionFactory(new FloatingPointConstant("-oo"));
- // +/- zero
- declareInternalFunctionFactory(new FloatingPointConstant("+zero"));
- declareInternalFunctionFactory(new FloatingPointConstant("-zero"));
-
- declareInternalFunctionFactory(new FloatingPointConstant("NaN"));
-
- // short forms of common floats
- defineSort("Float16", 0, mFloatingPointSort.getSort(new String[] { new String("5"), new String("11") }));
- defineSort("Float32", 0, mFloatingPointSort.getSort(new String[] { new String("8"), new String("24") }));
- defineSort("Float64", 0, mFloatingPointSort.getSort(new String[] { new String("11"), new String("53") }));
- defineSort("Float128", 0, mFloatingPointSort.getSort(new String[] { new String("15"), new String("113") }));
-
- // RoundingModes
- declareInternalFunction("roundNearestTiesToEven", new Sort[0], mRoundingModeSort, 0);
- declareInternalFunction("roundNearestTiesToAway", new Sort[0], mRoundingModeSort, 0);
- declareInternalFunction("roundTowardPositive", new Sort[0], mRoundingModeSort, 0);
- declareInternalFunction("roundTowardNegative", new Sort[0], mRoundingModeSort, 0);
- declareInternalFunction("roundTowardZero", new Sort[0], mRoundingModeSort, 0);
- defineFunction("RNE", new Sort[0], mRoundingModeSort, new TermVariable[0], term("roundNearestTiesToEven"),
- FunctionSymbol.INTERNAL);
- defineFunction("RNA", new Sort[0], mRoundingModeSort, new TermVariable[0], term("roundNearestTiesToAway"),
- FunctionSymbol.INTERNAL);
- defineFunction("RTP", new Sort[0], mRoundingModeSort, new TermVariable[0], term("roundTowardPositive"),
- FunctionSymbol.INTERNAL);
- defineFunction("RTN", new Sort[0], mRoundingModeSort, new TermVariable[0], term("roundTowardNegative"),
- FunctionSymbol.INTERNAL);
- defineFunction("RTZ", new Sort[0], mRoundingModeSort, new TermVariable[0], term("roundTowardZero"),
- FunctionSymbol.INTERNAL);
-
- // Operators
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.abs", 1, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.neg", 1, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.min", 2, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.max", 2, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.rem", 2, null, FunctionSymbol.INTERNAL));
- // rounded operators
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.add", 3, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.sub", 3, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.mul", 3, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.div", 3, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.fma", 4, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.sqrt", 2, null, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.roundToIntegral", 2, null, FunctionSymbol.INTERNAL));
-
- // Comparison Operators
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.leq", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.lt", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.geq", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.gt", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.eq", 2, mBooleanSort,
- FunctionSymbol.INTERNAL | FunctionSymbol.CHAINABLE));
-
- // Classification of numbers
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.isNormal", 1, mBooleanSort, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.isSubnormal", 1, mBooleanSort, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.isZero", 1, mBooleanSort, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.isInfinite", 1, mBooleanSort, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.isNaN", 1, mBooleanSort, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.isNegative", 1, mBooleanSort, FunctionSymbol.INTERNAL));
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.isPositive", 1, mBooleanSort, FunctionSymbol.INTERNAL));
-
- // Conversion from FP
- declareInternalFunctionFactory(new RegularFloatingPointFunction("fp.to_real", 1, mRealSort, FunctionSymbol.INTERNAL));
- }
-
- private void createStringOperators() {
- final Sort str = declareInternalSort(SMTLIBConstants.STRING, 0, 0).getSort(null);
- final Sort re = declareInternalSort(SMTLIBConstants.REGLAN, 0, 0).getSort(null);
- mStringSort = str;
- final Sort[] str1 = new Sort[] { str };
- final Sort[] str2 = new Sort[] { str, str };
- final Sort[] str3 = new Sort[] { str, str, str };
- final Sort[] str_re = new Sort[] { str, re };
- final Sort[] str_re_str = new Sort[] { str, re, str };
- final Sort[] re1 = new Sort[] { re };
- final Sort[] re2 = new Sort[] { re, re };
- declareInternalFunctionFactory(new FunctionSymbolFactory(SMTLIBConstants.CHAR) {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 1 || paramSorts.length != 0 || resultSort != null) {
- return null;
- }
- final String index = indices[0];
- if (!index.startsWith("#x") || index.length() <= 2 || index.length() > 7
- || (index.length() == 7 && index.charAt(2) > '2')) {
- return null;
- }
- return str;
- }
- });
- declareInternalFunction(SMTLIBConstants.STR_CONCAT, str2, str, FunctionSymbol.LEFTASSOC);
- declareInternalFunction(SMTLIBConstants.STR_LT, str2, mBooleanSort, FunctionSymbol.CHAINABLE);
- declareInternalFunction(SMTLIBConstants.STR_TO_RE, str1, re, 0);
- declareInternalFunction(SMTLIBConstants.STR_IN_RE, str_re, mBooleanSort, 0);
- declareInternalFunction(SMTLIBConstants.RE_NONE, EMPTY_SORT_ARRAY, re, 0);
- declareInternalFunction(SMTLIBConstants.RE_ALL, EMPTY_SORT_ARRAY, re, 0);
- declareInternalFunction(SMTLIBConstants.RE_ALLCHAR, EMPTY_SORT_ARRAY, re, 0);
- declareInternalFunction(SMTLIBConstants.RE_CONCAT, re2, re, FunctionSymbol.LEFTASSOC);
- declareInternalFunction(SMTLIBConstants.RE_UNION, re2, re, FunctionSymbol.LEFTASSOC);
- declareInternalFunction(SMTLIBConstants.RE_INTER, re2, re, FunctionSymbol.LEFTASSOC);
- declareInternalFunction(SMTLIBConstants.RE_STAR, re1, re, 0);
-
- declareInternalFunction(SMTLIBConstants.STR_LE, str2, mBooleanSort, FunctionSymbol.CHAINABLE);
- declareInternalFunction(SMTLIBConstants.STR_PREFIXOF, str2, mBooleanSort, 0);
- declareInternalFunction(SMTLIBConstants.STR_SUFFIXOF, str2, mBooleanSort, 0);
- declareInternalFunction(SMTLIBConstants.STR_CONTAINS, str2, mBooleanSort, 0);
- declareInternalFunction(SMTLIBConstants.STR_REPLACE, str3, str, 0);
- declareInternalFunction(SMTLIBConstants.STR_REPLACE_ALL, str3, str, 0);
- declareInternalFunction(SMTLIBConstants.STR_REPLACE_RE, str_re_str, str, 0);
- declareInternalFunction(SMTLIBConstants.STR_REPLACE_RE_ALL, str_re_str, str, 0);
-
- declareInternalFunction(SMTLIBConstants.RE_COMP, re1, re, 0);
- declareInternalFunction(SMTLIBConstants.RE_DIFF, re2, re, FunctionSymbol.LEFTASSOC);
- declareInternalFunction(SMTLIBConstants.RE_PLUS, re1, re, 0);
- declareInternalFunction(SMTLIBConstants.RE_OPT, re1, re, 0);
- declareInternalFunction(SMTLIBConstants.RE_RANGE, str2, re, 0);
-
- declareInternalFunction(SMTLIBConstants.STR_IS_DIGIT, str1, mBooleanSort, 0);
-
- declareInternalFunctionFactory(new FunctionSymbolFactory(SMTLIBConstants.RE_ITER) {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 1 || paramSorts.length != 1 || resultSort != null
- || paramSorts[0] != re) {
- return null;
- }
- toNumeral(indices[0]);
- return re;
- }
- });
- declareInternalFunctionFactory(new FunctionSymbolFactory(SMTLIBConstants.RE_LOOP) {
- @Override
- public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
- if (indices == null || indices.length != 2 || paramSorts.length != 1 || resultSort != null
- || paramSorts[0] != re) {
- return null;
- }
- toNumeral(indices[0]);
- toNumeral(indices[1]);
- return re;
- }
- });
- if (mLogic.hasIntegers()) {
- final Sort[] int1 = new Sort[] { mNumericSort };
- final Sort[] str_int = new Sort[] { str, mNumericSort };
- final Sort[] str2_int = new Sort[] { str, str, mNumericSort };
- final Sort[] str_int2 = new Sort[] { str, mNumericSort, mNumericSort };
- declareInternalFunction(SMTLIBConstants.STR_LEN, str1, mNumericSort, 0);
- declareInternalFunction(SMTLIBConstants.STR_AT, str_int, str, 0);
- declareInternalFunction(SMTLIBConstants.STR_SUBSTR, str_int2, str, 0);
- declareInternalFunction(SMTLIBConstants.STR_INDEXOF, str2_int, mNumericSort, 0);
- declareInternalFunction(SMTLIBConstants.STR_TO_CODE, str1, mNumericSort, 0);
- declareInternalFunction(SMTLIBConstants.STR_FROM_CODE, int1, str, 0);
- declareInternalFunction(SMTLIBConstants.STR_TO_INT, str1, mNumericSort, 0);
- declareInternalFunction(SMTLIBConstants.STR_FROM_INT, int1, str, 0);
- }
- }
-
- private void setLogic(final Logics logic) {
- mLogic = logic;
-
- if (logic.isArray()) {
- createArrayOperators();
- }
-
- if (logic.hasReals() || logic.isFloatingPoint()) {
- mRealSort = declareInternalSort("Real", 0, SortSymbol.NUMERIC).getSort(null, new Sort[0]);
- }
-
- if (logic.isArithmetic() || logic.isBitVector()) {
-
- if (logic.hasIntegers() || logic.isBitVector()) {
- mNumericSort = declareInternalSort("Int", 0, SortSymbol.NUMERIC).getSort(null, new Sort[0]);
- } else {
- mNumericSort = mRealSort;
- }
-
- if (logic.isIRA() || (logic.isBitVector() && logic.hasReals())) {
- createIRAOperators();
- } else {
- createNumericOperators(mNumericSort, logic.hasReals());
- }
- }
-
- if (logic.isBitVector() || logic.isFloatingPoint()) {
- createBitVecSort();
- }
-
- if (logic.isBitVector()) {
- createBitVecOperators();
- }
-
- if (logic.isFloatingPoint()) {
- createFloatingPointOperators();
- }
-
- if (logic.isString()) {
- createStringOperators();
- }
- if (mSolverSetup != null) {
- mSolverSetup.setLogic(this, logic);
- }
- if (logic.isDatatype()) {
- declareInternalFunctionFactory(new IsConstructorFactory());
- }
- }
-
- /******************** SORTS ********************************************/
-
- private SortSymbol defineSort(final String name, final int paramCount, final Sort definition, final int flags) {
- if ((flags & FunctionSymbol.INTERNAL) == 0 && definition == null && !mLogic.isUF() && !mLogic.isArray()) {
- throw new IllegalArgumentException("Free sorts are not allowed in this logic");
- }
- SortSymbol sortsym = mDeclaredSorts.get(name);
- if (sortsym != null) {
- throw new IllegalArgumentException("Sort " + name + " already exists.");
- }
- sortsym = new SortSymbol(this, name, paramCount, definition, flags);
- mDeclaredSorts.put(name, sortsym);
- return sortsym;
- }
-
- public SortSymbol declareSort(final String name, final int paramCount) {
- return defineSort(name, paramCount, null, 0);
- }
-
- public SortSymbol defineSort(final String name, final int paramCount, final Sort definition) {
- return defineSort(name, paramCount, definition, 0);
- }
-
- public Sort[] createSortVariables(final String... names) {
- final Sort[] sorts = new Sort[names.length];
- for (int i = 0; i < names.length; i++) {
- sorts[i] = new SortSymbol(this, names[i], i, null, SortSymbol.TYPEPARAM).getSort(null, new Sort[0]);
- }
- return sorts;
- }
-
- public SortSymbol declareInternalSort(final String name, final int paramCount, final int flags) {
- return defineSort(name, paramCount, null, flags | SortSymbol.INTERNAL);
- }
-
- /**
- * Returns the sort object for a previously declared or defined sort with sort arguments.
- *
- * @param id
- * The name of the sort.
- * @param args
- * The sort arguments.
- * @return the sort object.
- */
- public Sort getSort(final String id, final Sort... args) {
- return getSort(id, null, args);
- }
-
- /**
- * Returns the sort object for a previously declared or defined sort with sort arguments.
- *
- * @param id
- * The name of the sort.
- * @param args
- * The sort arguments.
- * @return the sort object.
- */
- public Sort getSort(final String id, final String[] indices, final Sort... args) {
- SortSymbol symbol;
- symbol = mDeclaredSorts.get(id);
- if (symbol == null) {
- return null;
- }
- return symbol.getSort(indices, args);
- }
-
- /**
- * Returns the Boolean sort. This is more efficient but has the same effect as calling getSort("Bool").
- *
- * @return the Boolean sort.
- */
- public Sort getBooleanSort() {
- return mBooleanSort;
- }
-
- /**
- * Get the sort used to construct integers. Note that this returns null if the logic does not support
- * integers.
- *
- * @return Sort used for integers.
- */
- public Sort getNumericSort() {
- return mNumericSort;
- }
-
- /**
- * Get the sort used to construct reals. Note that this returns null if the logic does not support
- * reals.
- *
- * @return Sort used for reals.
- */
- public Sort getRealSort() {
- return mRealSort;
- }
-
- /**
- * Get the sort used to construct strings. Note that this returns null if the logic does not support
- * strings.
- *
- * @return Sort used for strings.
- */
- public Sort getStringSort() {
- return mStringSort;
- }
-
- /******************** FUNCTIONS SYMBOLS AND FUNCTION TERMS ************/
-
- public void declareInternalFunctionFactory(final FunctionSymbolFactory factory) {
- if (mFunFactory.put(factory.mFuncName, factory) != null) {
- throw new AssertionError();
- }
- }
-
- private FunctionSymbol defineFunction(final String name, Sort[] paramTypes, final Sort resultType,
- TermVariable[] definitionVars, final Term definition, final int flags) {
- if ((flags & FunctionSymbol.INTERNAL) == 0) {
- if (mLogic == null) {
- throw new IllegalArgumentException("Call set-logic first!");
- }
- if (!mLogic.isUF() && paramTypes.length > 0 && definition == null) {
- throw new IllegalArgumentException("Free functions are not allowed in this logic!");
- }
- }
- if (name.charAt(0) == '@' && name.matches(MODEL_VALUE_PATTERN)) {
- throw new IllegalArgumentException("Function " + name + " is reserved for internal purposes.");
- }
- if (mFunFactory.get(name) != null || mDeclaredFuns.get(name) != null) {
- throw new IllegalArgumentException("Function " + name + " is already defined.");
- }
- if (paramTypes.length == 0) {
- paramTypes = EMPTY_SORT_ARRAY;
- }
- if (definitionVars != null && definitionVars.length == 0) {
- definitionVars = EMPTY_TERM_VARIABLE_ARRAY;
- }
- final FunctionSymbol f =
- new FunctionSymbol(name, null, paramTypes, resultType, definitionVars, definition, flags);
- mDeclaredFuns.put(name, f);
- return f;
- }
-
- /**
- * Declare a new function symbol. This corresponds to declare-fun in SMTLIB.
- *
- * @param name
- * name of the function.
- * @param paramTypes
- * the sorts of the parameters of the function.
- * @param resultType
- * the sort of the result type of the function.
- * @throws IllegalArgumentException
- * if a function with that name is already defined or if the sorts are not visible in this scope.
- * @return the created function symbol.
- */
- public FunctionSymbol declareFunction(final String name, final Sort[] paramTypes, final Sort resultType) {
- return defineFunction(name, paramTypes, resultType, null, null, 0);
- }
-
- /**
- * Defines a new function symbol. This corresponds to define-fun in SMTLIB.
- *
- * @param name
- * name of the function.
- * @param definitionVars
- * the variables of the function.
- * @param definition
- * the definition of the function.
- * @throws IllegalArgumentException
- * if a function with that name is already defined or if the sorts are not visible in this scope.
- * @return the created function symbol.
- */
- public FunctionSymbol defineFunction(final String name, final TermVariable[] definitionVars,
- final Term definition) {
- final Sort[] paramTypes = definitionVars.length == 0 ? EMPTY_SORT_ARRAY : new Sort[definitionVars.length];
- for (int i = 0; i < paramTypes.length; i++) {
- paramTypes[i] = definitionVars[i].getSort();
- }
- final Sort resultType = definition.getSort();
- return defineFunction(name, paramTypes, resultType, definitionVars, definition, 0);
- }
-
- public FunctionSymbol getFunction(final String name, final Sort... paramTypes) {
- return getFunctionWithResult(name, null, null, paramTypes);
- }
-
- public Map getDeclaredFunctions() {
- return mDeclaredFuns;
- }
-
- public Map getDeclaredSorts() {
- return mDeclaredSorts;
- }
-
- public Map getFunctionFactories() {
- return mFunFactory;
- }
-
- private FunctionSymbol getModelValueSymbol(final String name, final Sort sort) {
- final int hash = HashUtils.hashJenkins(name.hashCode(), sort);
- for (final FunctionSymbol symb : mModelValueCache.iterateHashCode(hash)) {
- if (symb.getName().equals(name) && symb.getReturnSort() == sort) {
- return symb;
- }
- }
- final FunctionSymbol symb = new FunctionSymbol(name, null, EMPTY_SORT_ARRAY, sort, null, null,
- FunctionSymbol.RETURNOVERLOAD | FunctionSymbol.INTERNAL | FunctionSymbol.MODELVALUE);
- mModelValueCache.put(hash, symb);
- return symb;
- }
-
- public FunctionSymbol getFunctionWithResult(final String name, final String[] indices, final Sort resultType,
- final Sort... paramTypes) {
- final FunctionSymbolFactory factory = mFunFactory.get(name);
- if (factory != null) {
- FunctionSymbol fsym = factory.getFunctionWithResult(this, indices, paramTypes, resultType);
- if (fsym == null && mIRAWrappers != null) {
- fsym = mIRAWrappers.createWrapper(this, name, indices, paramTypes, resultType);
- }
- if (fsym == null) {
- final StringBuilder sb = new StringBuilder();
- final PrintTerm pt = new PrintTerm();
- sb.append("Builtin function ");
- if (indices != null) {
- sb.append("(_ ").append(name);
- for (final String i : indices) {
- sb.append(" ").append(i);
- }
- sb.append(") does not support indices or argument sorts (");
- } else {
- sb.append(name);
- sb.append(" does not support argument sorts (");
- }
- String sep = "";
- for (final Sort s : paramTypes) {
- sb.append(sep);
- pt.append(sb, s);
- sep = " ";
- }
- sb.append(")");
- throw new SMTLIBException(sb.toString());
- }
- return fsym;
- }
- FunctionSymbol fsym = mDeclaredFuns.get(name);
- if (fsym != null) {
- if (indices != null) {
- throw new SMTLIBException("Function " + name + " take no index.");
- }
- if (resultType != null || !fsym.typecheck(paramTypes)) {
- if (mIRAWrappers != null) {
- fsym = mIRAWrappers.createWrapper(this, name, indices, paramTypes, resultType);
- if (fsym != null) {
- return fsym;
- }
- }
- throw new SMTLIBException(
- "Application of function " + fsym + " does not type check.");
- }
- return fsym;
- }
- if (resultType != null && indices == null && paramTypes.length == 0 && name.matches(MODEL_VALUE_PATTERN)) {
- return getModelValueSymbol(name, resultType);
- }
- throw new SMTLIBException("Unknown function symbol " + name + ".");
- }
-
- public Term term(final FunctionSymbolFactory factory, final Term... parameters) {
- final Sort[] sorts = parameters.length == 0 ? EMPTY_SORT_ARRAY : new Sort[parameters.length];
- for (int i = 0; i < parameters.length; i++) {
- sorts[i] = parameters[i].getSort();
- }
- final FunctionSymbol fsym = factory.getFunctionWithResult(this, null, sorts, null);
- if (fsym == null) {
- throw new IllegalArgumentException("Did not find overload for function " + factory);
- }
- return term(fsym, parameters);
- }
-
- public Term term(final String funcname, final String[] indices,
- final Sort returnSort, final Term... params) throws SMTLIBException {
- if (mBitVecSort != null && indices != null && indices.length == 1 && returnSort == null && params.length == 0
- && funcname.matches(BITVEC_CONST_PATTERN) && indices[0].matches("\\d+")) {
- final BigInteger value = new BigInteger(funcname.substring(2));
- if (value.bitLength() > Integer.parseInt(indices[0])) {
- throw new SMTLIBException("Constant out of range: (_ " + funcname + " " + indices[0] + ")");
- }
- return constant(value, mBitVecSort.getSort(indices));
- }
-
- final Sort[] sorts = params.length == 0 ? Script.EMPTY_SORT_ARRAY : new Sort[params.length];
- for (int i = 0; i < sorts.length; i++) {
- sorts[i] = params[i].getSort();
- }
- final FunctionSymbol fsym = getFunctionWithResult(funcname, indices, returnSort, sorts);
- return term(fsym, params);
- }
-
- public Term term(final String func, final Term... parameters) {
- return term(func, null, null, parameters);
- }
-
- public Term term(final FunctionSymbol func, Term... parameters) {
- // Special case for normalizing rationals: we want to use ConstantValue with Rational, for things
- // like (/ 1.0 2.0), to avoid the overhead of parsing them again. To avoid two terms that look identical but are
- // not equal, we don't create an ApplicationTerm when parsing rational constants.
- if (func.isIntern() && func.getName().equals(SMTLIBConstants.DIVIDE) && parameters.length == 2
- && parameters[0] instanceof ConstantTerm && parameters[1] instanceof ConstantTerm
- && parameters[0].getSort() == getRealSort() && parameters[1].getSort() == getRealSort()) {
- final ConstantTerm numTerm = (ConstantTerm) parameters[0];
- final ConstantTerm denomTerm = (ConstantTerm) parameters[1];
- BigInteger num = null, denom = null;
- if (numTerm.getValue() instanceof Rational && denomTerm.getValue() instanceof Rational) {
- final Rational numRat = (Rational) numTerm.getValue();
- final Rational denomRat = (Rational) denomTerm.getValue();
- if (numRat.isIntegral() && denomRat.isIntegral()) {
- num = numRat.numerator();
- denom = denomRat.numerator();
- }
- }
- // make sure that num and denom have the right form such that the created
- // rational term would be completely identical
- if (num != null && denom.compareTo(BigInteger.ONE) > 0 && num.gcd(denom).equals(BigInteger.ONE)) {
- final Rational value = Rational.valueOf(num, denom);
- return constant(value, getRealSort());
- }
- }
- if (func.isIntern() && func.getName().equals(SMTLIBConstants.MINUS) && parameters.length == 1
- && parameters[0] instanceof ConstantTerm
- && (parameters[0].getSort() == getNumericSort() || parameters[0].getSort() == getRealSort())) {
- final ConstantTerm numTerm = (ConstantTerm) parameters[0];
- if (numTerm.getValue() instanceof Rational) {
- final Rational num = (Rational) numTerm.getValue();
- // make sure that num has the right form. In particular we only allow negating integrals, as the
- // normal form of -.5 is (/ (- 1.0) 2.0).
- if (num.isIntegral() && num.signum() > 0) {
- return constant(num.negate(), numTerm.getSort());
- }
- } else if (numTerm.getValue() instanceof BigInteger) {
- final BigInteger num = (BigInteger) numTerm.getValue();
- // make sure that num is positive.
- if (num.signum() > 0) {
- return constant(num.negate(), numTerm.getSort());
- }
- }
- }
-
- // Not a rational term to normalize
- if (parameters.length == 0) {
- parameters = EMPTY_TERM_ARRAY;
- }
- final int hash = ApplicationTerm.hashApplication(func, parameters);
- for (final Term t : mTermCache.iterateHashCode(hash)) {
- if (t instanceof ApplicationTerm) {
- final ApplicationTerm app = (ApplicationTerm) t;
- if (func == app.getFunction() && Arrays.equals(app.getParameters(), parameters)) {
- return app;
- }
- }
- }
- final ApplicationTerm app = new ApplicationTerm(func, parameters, hash);
- mTermCache.put(hash, app);
- return app;
- }
-
- /******************** TERM VARIABLES AND VARIABLE TERMS *****************/
-
- /**
- * Create a fresh term variable that does not clash with any existing one.
- *
- * @param prefix
- * the prefix of the variable name (without the leading ?).
- * @param sort
- * the sort of the variable.
- * @return a fresh term variable.
- */
- public TermVariable createFreshTermVariable(final String prefix, final Sort sort) {
- final String name = "." + prefix + "." + mTvarCtr++;
- return new TermVariable(name, sort, TermVariable.hashVariable(name, sort));
- }
-
- /**
- * Create a term variable with the given name and sort.
- *
- * @param name
- * the variable name.
- * @param sort
- * the sort of the variable.
- * @return a term variable.
- */
- public TermVariable createTermVariable(final String name, final Sort sort) {
- final int hash = TermVariable.hashVariable(name, sort);
- for (final TermVariable tv : mTvUnify.iterateHashCode(hash)) {
- if (tv.getSort().equals(sort) && tv.getName().equals(name)) {
- return tv;
- }
- }
- final TermVariable tv = new TermVariable(name, sort, hash);
- mTvUnify.put(hash, tv);
- return tv;
- }
-
- public DataType.Constructor createConstructor(final String name, final String[] selectors,
- final Sort[] argumentSorts) {
- final DataType.Constructor constructor = new DataType.Constructor(name, selectors, argumentSorts);
- return constructor;
-
- }
-
- /**
- * Create a new data type with the given name and number of parameters.
- *
- * @param name
- * the variable name.
- * @param numParams
- * the number of parameters of the data type.
- * @return a data type.
- */
- public DataType createDatatypes(final String name, final int numParams) {
- if (mDeclaredSorts.containsKey(name)) {
- throw new SMTLIBException("Datatype " + name + " already exists.");
- }
- final DataType datatype = new DataType(this, name, numParams);
- mDeclaredSorts.put(name, datatype);
- return datatype;
- }
-
- public Term term(final TermVariable var) {
- return var;
- }
-
- /******************** ANNOTATED TERMS *********************************/
-
- public Term annotatedTerm(final Annotation[] annots, final Term sub) {
- final int hash = AnnotatedTerm.hashAnnotations(annots, sub);
- for (final Term t : mTermCache.iterateHashCode(hash)) {
- if (t instanceof AnnotatedTerm) {
- final AnnotatedTerm annot = (AnnotatedTerm) t;
- if (sub == annot.getSubterm() && Arrays.equals(annot.getAnnotations(), annots)) {
- return annot;
- }
- }
- }
- final AnnotatedTerm annot = new AnnotatedTerm(annots, sub, hash);
- mTermCache.put(hash, annot);
- return annot;
- }
-
- /******************** ASSERTION STACK *********************************/
-
- public void push() {
- if (!mGlobalDecls) {
- mFunFactory.beginScope();
- mDeclaredFuns.beginScope();
- mDeclaredSorts.beginScope();
- }
- }
-
- public void pop() {
- if (!mGlobalDecls) {
- mFunFactory.endScope();
- mDeclaredFuns.endScope();
- mDeclaredSorts.endScope();
- }
- }
-
- /**
- * Create a fresh auxiliary function that stands for the given term and takes the given variables as arguments.
- */
- public FunctionSymbol createFreshAuxFunction(final TermVariable[] vars, final Term term) {
- final Sort[] paramSorts = new Sort[vars.length];
- for (int i = 0; i < vars.length; i++) {
- paramSorts[i] = vars[i].getSort();
- }
- return declareInternalFunction("@AUX" + (mAuxCounter++), paramSorts, vars, term,
- FunctionSymbol.UNINTERPRETEDINTERNAL); // TODO Change flag?
- }
-
- public void resetAssertions() {
- if (mGlobalDecls) {
- return;
- }
- while (mDeclaredFuns.getActiveScopeNum() > 1) {
- mDeclaredFuns.endScope();
- }
- for (final Iterator> it = mDeclaredFuns.entrySet().iterator(); it
- .hasNext();) {
- final Map.Entry next = it.next();
- if (!next.getValue().isIntern()) {
- it.remove();
- }
- }
- while (mFunFactory.getActiveScopeNum() > 1) {
- mFunFactory.endScope();
- }
- while (mDeclaredSorts.getActiveScopeNum() > 1) {
- mDeclaredSorts.endScope();
- }
- for (final Iterator> it = mDeclaredSorts.entrySet().iterator(); it.hasNext();) {
- final Map.Entry next = it.next();
- if (!next.getValue().isIntern()) {
- it.remove();
- }
- }
- }
-
- public void setGlobalSymbols(final boolean globalDecls) {
- mGlobalDecls = globalDecls;
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Util.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Util.java
deleted file mode 100644
index 3571d83b585..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Util.java
+++ /dev/null
@@ -1,256 +0,0 @@
-/*
- * Copyright (C) 2009-2012 University of Freiburg
- *
- * This file is part of SMTInterpol.
- *
- * SMTInterpol is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * SMTInterpol is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with SMTInterpol. If not, see formulas = new LinkedHashSet<>();
-
- for (final Term f : subforms) {
- if (f == neutral) {
- continue;
- }
- if (f == absorbing) {
- return f;
- }
-
- /* Normalize nested and/ors */
- if (f instanceof ApplicationTerm && ((ApplicationTerm) f).getFunction().getName().equals(connector)) {
- for (final Term subf : ((ApplicationTerm) f).getParameters()) {
- formulas.add(subf);
- }
- } else {
- formulas.add(f);
- }
- }
- if (formulas.size() <= 1) { // NOPMD
- if (formulas.isEmpty()) {
- return neutral;
- }
- return formulas.iterator().next();
- }
- final Term[] arrforms = formulas.toArray(new Term[formulas.size()]);
- return script.term(connector, arrforms);
- }
-
- /**
- * Create a slightly simplified if-then-else term. This mainly optimizes the special cases where one of the
- * parameters is true or false.
- *
- * @param script
- * the script where the term is created.
- * @param cond
- * the if condition.
- * @param thenPart
- * the then part.
- * @param elsePart
- * the else part.
- * @return the simplified if-then-else term.
- */
- public static Term ite(final Script script, final Term cond, final Term thenPart, final Term elsePart) {
- final Term trueTerm = script.term("true");
- final Term falseTerm = script.term("false");
- if (cond == trueTerm || thenPart == elsePart) {
- return thenPart;
- } else if (cond == falseTerm) {
- return elsePart;
- } else if (thenPart == trueTerm) {
- return Util.or(script, cond, elsePart);
- } else if (elsePart == falseTerm) {
- return Util.and(script, cond, thenPart);
- } else if (thenPart == falseTerm) {
- return Util.and(script, Util.not(script, cond), elsePart);
- } else if (elsePart == trueTerm) {
- return Util.or(script, Util.not(script, cond), thenPart);
- }
- return script.term("ite", cond, thenPart, elsePart);
- }
-
- /**
- * Create a slightly simplified implies term. This mainly optimizes the special cases where one of the parameters is
- * true or false or if a left-hand-side term occurs more than once. It also handles the case where only one
- * subformula is given.
- *
- * @param script
- * the script where the term is created.
- * @param subforms
- * the sub formulas.
- * @return A simplified version of (=> subforms...).
- */
- public static Term implies(final Script script, final Term... subforms) {
- final Term trueTerm = script.term("true");
- final Term lastFormula = subforms[subforms.length - 1];
- if (lastFormula == trueTerm) {
- return trueTerm;
- }
- final Term falseTerm = script.term("false");
- if (lastFormula == falseTerm) {
- final Term[] allButLast = new Term[subforms.length - 1];
- System.arraycopy(subforms, 0, allButLast, 0, subforms.length - 1);
- return Util.not(script, Util.and(script, allButLast));
- }
- final LinkedHashSet newSubforms = new LinkedHashSet<>();
- for (int i = 0; i < subforms.length - 1; i++) {
- if (subforms[i] == falseTerm) {
- return trueTerm;
- }
- if (subforms[i] != trueTerm) {
- newSubforms.add(subforms[i]);
- }
- }
- if (newSubforms.isEmpty()) {
- return lastFormula;
- }
- final Term[] newParams = newSubforms.toArray(new Term[newSubforms.size() + 1]);
- newParams[newParams.length - 1] = lastFormula;
- return script.term("=>", newParams);
- }
-}
diff --git a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/WrapperScript.java b/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/WrapperScript.java
deleted file mode 100644
index 19555bc30f8..00000000000
--- a/trunk/source/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/WrapperScript.java
+++ /dev/null
@@ -1,377 +0,0 @@
-/*
- * Copyright (C) 2018 Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
- * Copyright (C) 2018 University of Freiburg
- *
- * This file is part of the ULTIMATE ModelCheckerUtils Library.
- *
- * The ULTIMATE ModelCheckerUtils Library is free software: you can redistribute it and/or modify
- * it under the terms of the GNU Lesser General Public License as published
- * by the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * The ULTIMATE ModelCheckerUtils Library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public License
- * along with the ULTIMATE ModelCheckerUtils Library. If not, see
- * The type of {@link Script} to search for.
- * @param clazz
- * The {@link Class} instance representing the type.
- * @return A {@link Script} instance if one can be found or null.
- */
- @SuppressWarnings("unchecked")
- public T findBacking(final Class clazz) {
- final Iterator