diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java index 69fe6fb906..abd38bc6ea 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java @@ -86,6 +86,10 @@ public Interpolant getInterpolant(ItpPattern pattern) { try (final var itpSolverBinary = itpSolverBinaryFactory.get()) { itpSolverBinary.issueCommand("(set-option :produce-interpolants true)"); itpSolverBinary.issueCommand("(set-logic ALL)"); + typeStack.forEach(enumType -> { + Collection literals = enumType.getLongValues().stream().map(name -> String.format("(%s)", name)).toList(); + itpSolverBinary.issueCommand(String.format("(declare-datatypes ((%s 0)) ((%s)))", enumType.getName(), String.join(" ", literals))); + }); declarationStack.forEach( constDecl -> itpSolverBinary.issueCommand(symbolTable.getDeclaration(constDecl))); @@ -108,6 +112,8 @@ public Interpolant getInterpolant(ItpPattern pattern) { itpSolverBinary.issueCommand( String.format("(assert (and %s))", aTerm.collect(Collectors.joining(" ")))); + itpSolverBinary.issueCommand("(check-sat)"); + itpSolverBinary.readResponse(); itpSolverBinary.issueCommand( String.format("(get-interpolant _cvc5_interpolant%d (not (and %s)))", interpolantCount++, bTerm.collect(Collectors.joining(" ")))); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java index 48f793ed09..85f5f9a80f 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java @@ -145,6 +145,7 @@ import hu.bme.mit.theta.core.type.rattype.RatToIntExpr; import hu.bme.mit.theta.core.utils.BvUtils; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibExprTransformer; +import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibSymbolTable; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTransformationManager; import java.math.BigInteger; @@ -156,13 +157,15 @@ public class GenericSmtLibExprTransformer implements SmtLibExprTransformer { private static final int CACHE_SIZE = 1000; private final SmtLibTransformationManager transformer; + private final SmtLibSymbolTable symbolTable; private final Cache, String> exprToTerm; private final DispatchTable table; private final Env env; - public GenericSmtLibExprTransformer(final SmtLibTransformationManager transformer) { + public GenericSmtLibExprTransformer(final SmtLibTransformationManager transformer, final SmtLibSymbolTable symbolTable) { this.transformer = transformer; + this.symbolTable = symbolTable; this.env = new Env(); this.exprToTerm = CacheBuilder.newBuilder().maximumSize(CACHE_SIZE).build(); @@ -739,7 +742,9 @@ protected String transformEnumNeq(final EnumNeqExpr expr) { } protected String transformEnumLit(final EnumLitExpr expr) { - return EnumType.makeLongName(expr.getType(), expr.getValue()); + String longName = EnumType.makeLongName(expr.getType(), expr.getValue()); + symbolTable.putEnumLiteral(longName, expr); + return longName; } /* diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java index 267ee7e210..2e551f0985 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java @@ -19,8 +19,12 @@ import com.google.common.collect.HashBiMap; import com.google.common.collect.Maps; import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibSymbolTable; +import java.util.HashMap; +import java.util.Map; + import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; @@ -32,10 +36,12 @@ public class GenericSmtLibSymbolTable implements SmtLibSymbolTable { private final BiMap, String> constToSymbol; private final BiMap, String> constToDeclaration; + private final Map symbolToEnumLiteral; public GenericSmtLibSymbolTable() { constToSymbol = Maps.synchronizedBiMap(HashBiMap.create()); constToDeclaration = Maps.synchronizedBiMap(HashBiMap.create()); + symbolToEnumLiteral = new HashMap<>(); } public GenericSmtLibSymbolTable(GenericSmtLibSymbolTable table) { @@ -43,6 +49,8 @@ public GenericSmtLibSymbolTable(GenericSmtLibSymbolTable table) { constToSymbol.putAll(table.constToSymbol); constToDeclaration = Maps.synchronizedBiMap(HashBiMap.create()); constToDeclaration.putAll(table.constToDeclaration); + symbolToEnumLiteral = new HashMap<>(); + symbolToEnumLiteral.putAll(table.symbolToEnumLiteral); } @Override @@ -56,6 +64,11 @@ public boolean definesSymbol(final String symbol) { symbol.replaceAll(problematicCharactersRegex, problematicCharactersReplacement)); } + @Override + public boolean definesEnumLiteral(String literal) { + return symbolToEnumLiteral.containsKey(literal); + } + @Override public String getSymbol(final ConstDecl constDecl) { checkArgument(definesConst(constDecl)); @@ -74,6 +87,11 @@ public ConstDecl getConst(final String symbol) { return constToSymbol.inverse().get(symbol); } + @Override + public EnumLitExpr getEnumLiteral(String literal) { + return symbolToEnumLiteral.get(literal); + } + @Override public void put(final ConstDecl constDecl, final String symbol, final String declaration) { checkNotNull(constDecl); @@ -85,4 +103,9 @@ public void put(final ConstDecl constDecl, final String symbol, final String constToDeclaration.put(constDecl, declaration.replaceAll(problematicCharactersRegex, problematicCharactersReplacement)); } + + @Override + public void putEnumLiteral(String symbol, EnumLitExpr litExpr) { + symbolToEnumLiteral.put(symbol, litExpr); + } } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java index b4d45a9313..ffc65010db 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java @@ -28,16 +28,79 @@ import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.abstracttype.*; +import hu.bme.mit.theta.core.type.abstracttype.AddExpr; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.type.abstracttype.GeqExpr; +import hu.bme.mit.theta.core.type.abstracttype.GtExpr; +import hu.bme.mit.theta.core.type.abstracttype.LeqExpr; +import hu.bme.mit.theta.core.type.abstracttype.LtExpr; +import hu.bme.mit.theta.core.type.abstracttype.ModExpr; +import hu.bme.mit.theta.core.type.abstracttype.MulExpr; +import hu.bme.mit.theta.core.type.abstracttype.NegExpr; +import hu.bme.mit.theta.core.type.abstracttype.RemExpr; +import hu.bme.mit.theta.core.type.abstracttype.SubExpr; import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; -import hu.bme.mit.theta.core.type.booltype.*; -import hu.bme.mit.theta.core.type.bvtype.*; +import hu.bme.mit.theta.core.type.booltype.AndExpr; +import hu.bme.mit.theta.core.type.booltype.BoolExprs; +import hu.bme.mit.theta.core.type.booltype.IffExpr; +import hu.bme.mit.theta.core.type.booltype.ImplyExpr; +import hu.bme.mit.theta.core.type.booltype.NotExpr; +import hu.bme.mit.theta.core.type.booltype.OrExpr; +import hu.bme.mit.theta.core.type.booltype.XorExpr; +import hu.bme.mit.theta.core.type.bvtype.BvAddExpr; +import hu.bme.mit.theta.core.type.bvtype.BvAndExpr; +import hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvConcatExpr; +import hu.bme.mit.theta.core.type.bvtype.BvExprs; +import hu.bme.mit.theta.core.type.bvtype.BvExtractExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNegExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNotExpr; +import hu.bme.mit.theta.core.type.bvtype.BvOrExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSDivExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSExtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSGeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSGtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSLeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSLtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSModExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr; +import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; +import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr; +import hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvUGtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvULeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvULtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvURemExpr; +import hu.bme.mit.theta.core.type.bvtype.BvXorExpr; +import hu.bme.mit.theta.core.type.bvtype.BvZExtExpr; import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; import hu.bme.mit.theta.core.type.enumtype.EnumType; -import hu.bme.mit.theta.core.type.fptype.*; +import hu.bme.mit.theta.core.type.fptype.FpAbsExpr; +import hu.bme.mit.theta.core.type.fptype.FpAddExpr; +import hu.bme.mit.theta.core.type.fptype.FpDivExpr; +import hu.bme.mit.theta.core.type.fptype.FpEqExpr; +import hu.bme.mit.theta.core.type.fptype.FpExprs; +import hu.bme.mit.theta.core.type.fptype.FpGeqExpr; +import hu.bme.mit.theta.core.type.fptype.FpGtExpr; +import hu.bme.mit.theta.core.type.fptype.FpIsNanExpr; +import hu.bme.mit.theta.core.type.fptype.FpLeqExpr; +import hu.bme.mit.theta.core.type.fptype.FpLtExpr; +import hu.bme.mit.theta.core.type.fptype.FpMaxExpr; +import hu.bme.mit.theta.core.type.fptype.FpMinExpr; +import hu.bme.mit.theta.core.type.fptype.FpMulExpr; +import hu.bme.mit.theta.core.type.fptype.FpNegExpr; +import hu.bme.mit.theta.core.type.fptype.FpRemExpr; +import hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr; +import hu.bme.mit.theta.core.type.fptype.FpRoundingMode; +import hu.bme.mit.theta.core.type.fptype.FpSqrtExpr; +import hu.bme.mit.theta.core.type.fptype.FpSubExpr; import hu.bme.mit.theta.core.type.functype.FuncExprs; import hu.bme.mit.theta.core.type.functype.FuncLitExpr; import hu.bme.mit.theta.core.type.functype.FuncType; @@ -49,7 +112,6 @@ import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Lexer; import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser; -import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.*; import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolverException; import hu.bme.mit.theta.solver.smtlib.solver.model.SmtLibModel; import hu.bme.mit.theta.solver.smtlib.solver.parser.ThrowExceptionErrorListener; @@ -60,25 +122,47 @@ import java.math.BigDecimal; import java.math.BigInteger; -import java.util.*; -import java.util.function.*; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.function.BiFunction; +import java.util.function.BinaryOperator; +import java.util.function.Function; +import java.util.function.Supplier; +import java.util.function.UnaryOperator; import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.core.decl.Decls.Param; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall; import static hu.bme.mit.theta.core.type.functype.FuncExprs.Func; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; import static hu.bme.mit.theta.core.utils.TypeUtils.castBv; -import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.*; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.BinaryContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.DecimalContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Exists_termContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Forall_termContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Generic_termContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.HexadecimalContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.IdentifierContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.IndexContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Let_termContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.NumeralContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Qual_identifierContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.SortContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Spec_constantContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.SymbolContext; +import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.TermContext; import static java.util.stream.Collectors.toList; -import java.lang.String; - public class GenericSmtLibTermTransformer implements SmtLibTermTransformer { protected final SmtLibSymbolTable symbolTable; @@ -551,6 +635,8 @@ protected Expr transformSymbol(final SymbolContext ctx, final SmtLibModel mod return decl.getRef(); } else if (symbolTable.definesSymbol(value)) { return symbolTable.getConst(value).getRef(); + } else if(symbolTable.definesEnumLiteral(value)) { + return symbolTable.getEnumLiteral(value); } else { throw new SmtLibSolverException("Transforation of symbol not supported: " + value); } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTransformationManager.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTransformationManager.java index 8d6bc2f811..24fefdfcae 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTransformationManager.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTransformationManager.java @@ -33,7 +33,7 @@ public class GenericSmtLibTransformationManager implements SmtLibTransformationM public GenericSmtLibTransformationManager(final SmtLibSymbolTable symbolTable) { this.typeTransformer = instantiateTypeTransformer(this); this.declTransformer = instantiateDeclTransformer(this, symbolTable); - this.exprTransformer = instantiateExprTransformer(this); + this.exprTransformer = instantiateExprTransformer(this, symbolTable); } @Override @@ -63,7 +63,8 @@ protected SmtLibDeclTransformer instantiateDeclTransformer( } protected SmtLibExprTransformer instantiateExprTransformer( - final SmtLibTransformationManager transformer) { - return new GenericSmtLibExprTransformer(transformer); + final SmtLibTransformationManager transformer, final SmtLibSymbolTable symbolTable + ) { + return new GenericSmtLibExprTransformer(transformer, symbolTable); } } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibExprTransformer.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibExprTransformer.java index 4ec99b63d2..5a7dbd33b4 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibExprTransformer.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibExprTransformer.java @@ -17,12 +17,13 @@ import hu.bme.mit.theta.core.type.inttype.IntRemExpr; import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibExprTransformer; +import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibSymbolTable; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTransformationManager; public class MathSATSmtLibExprTransformer extends GenericSmtLibExprTransformer { - public MathSATSmtLibExprTransformer(final SmtLibTransformationManager transformer) { - super(transformer); + public MathSATSmtLibExprTransformer(final SmtLibTransformationManager transformer, final SmtLibSymbolTable symbolTable) { + super(transformer, symbolTable); } @Override diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibTransformationManager.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibTransformationManager.java index 7c148969ca..12dd71c7bb 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibTransformationManager.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibTransformationManager.java @@ -28,7 +28,8 @@ public MathSATSmtLibTransformationManager(final SmtLibSymbolTable symbolTable) { @Override protected SmtLibExprTransformer instantiateExprTransformer( - final SmtLibTransformationManager transformer) { - return new MathSATSmtLibExprTransformer(transformer); + final SmtLibTransformationManager transformer, final SmtLibSymbolTable symbolTable + ) { + return new MathSATSmtLibExprTransformer(transformer, symbolTable); } } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/transformer/SmtLibSymbolTable.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/transformer/SmtLibSymbolTable.java index ba506f5a51..32d122c6a0 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/transformer/SmtLibSymbolTable.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/transformer/SmtLibSymbolTable.java @@ -16,6 +16,7 @@ package hu.bme.mit.theta.solver.smtlib.solver.transformer; import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; public interface SmtLibSymbolTable { @@ -23,11 +24,17 @@ public interface SmtLibSymbolTable { boolean definesSymbol(String symbol); + boolean definesEnumLiteral(String literal); + String getSymbol(ConstDecl constDecl); String getDeclaration(ConstDecl constDecl); ConstDecl getConst(String symbol); + EnumLitExpr getEnumLiteral(String literal); + void put(ConstDecl constDecl, String symbol, String declaration); + + void putEnumLiteral(String symbol, EnumLitExpr litExpr); } diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java index 6e61059f45..af3c6e7b3d 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java @@ -19,7 +19,7 @@ import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; -import hu.bme.mit.theta.solver.smtlib.impl.z3.Z3SmtLibSolverFactory; +import hu.bme.mit.theta.solver.smtlib.impl.smtinterpol.SMTInterpolSmtLibSolverFactory; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.config.XstsConfig; import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder; @@ -355,10 +355,12 @@ public void test() throws IOException { new FileInputStream(propPath))) { xsts = XstsDslManager.createXsts(inputStream); } -// String[] args = {"-q"}; + String[] args = {"-q"}; // final var smtSolver = SMTInterpolSmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\smtinterpol-2.5-1256-g55d6ba76.jar"), args); + final var smtSolver = SMTInterpolSmtLibSolverFactory.create(Path.of("E:\\smt\\SMTInterpol-releases\\smtinterpol-2.5-1301-g2c871e40_datatype_interpolation.jar"), args); // final var smtSolver = CVC5SmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\cvc5-Win64.exe"), new String[]{"--incremental"}); - final var smtSolver = Z3SmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\z3-4.12.4-x64-win\\bin\\z3.exe"), new String[]{"-smt2", "-in"}); +// final var smtSolver = CVC5SmtLibSolverFactory.create(Path.of("E:\\smt\\cvc5\\cvc5-2024-01-13-x86_64-win64-production.exe"), new String[]{"--incremental"}); +// final var smtSolver = Z3SmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\z3-4.12.4-x64-win\\bin\\z3.exe"), new String[]{"-smt2", "-in"}); final XstsConfig configuration = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, smtSolver, smtSolver).initPrec(XstsConfigBuilder.InitPrec.CTRL)