diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java index 98667ad383..07bd23df1d 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java @@ -22,7 +22,14 @@ import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.utils.ExprUtils; -import hu.bme.mit.theta.solver.*; +import hu.bme.mit.theta.solver.Interpolant; +import hu.bme.mit.theta.solver.ItpMarker; +import hu.bme.mit.theta.solver.ItpMarkerTree; +import hu.bme.mit.theta.solver.ItpPattern; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.SolverStatus; +import hu.bme.mit.theta.solver.Stack; +import hu.bme.mit.theta.solver.UnknownSolverStatusException; import hu.bme.mit.theta.solver.impl.StackImpl; import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Lexer; import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser; @@ -39,12 +46,13 @@ import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.CommonTokenStream; -import java.util.ArrayList; import java.util.Collection; -import java.util.List; +import java.util.HashSet; import java.util.Set; -import static com.google.common.base.Preconditions.*; +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; public abstract class SmtLibItpSolver implements ItpSolver { @@ -254,7 +262,7 @@ protected final GeneralResponse parseResponse(final String response) { } private void declareDatatypes(final Collection allTypes) { - List types = new ArrayList<>(allTypes); + Set types = new HashSet<>(allTypes); types.removeAll(typeStack.toCollection()); for (Type t : types) {