From 0f04e87b9abd705be6dc0c55cc002430705032e9 Mon Sep 17 00:00:00 2001 From: RipplB Date: Tue, 18 Jun 2024 10:15:38 +0200 Subject: [PATCH] Introduce datatypes for smtlib --- .../smtlib/impl/cvc5/CVC5SmtLibItpSolver.java | 6 + .../generic/GenericSmtLibExprTransformer.java | 36 ++++- .../generic/GenericSmtLibSolverBinary.java | 2 + .../generic/GenericSmtLibSolverFactory.java | 19 +++ .../generic/GenericSmtLibSymbolTable.java | 23 ++++ .../generic/GenericSmtLibTermTransformer.java | 130 +++++------------- .../GenericSmtLibTransformationManager.java | 7 +- .../generic/GenericSmtLibTypeTransformer.java | 6 + .../mathsat/MathSATSmtLibExprTransformer.java | 5 +- .../MathSATSmtLibTransformationManager.java | 5 +- .../princess/PrincessSmtLibItpSolver.java | 16 +-- .../princess/PrincessSmtLibSolverFactory.java | 21 ++- .../PrincessSmtLibSolverInstaller.java | 5 +- .../SMTInterpolSmtLibItpSolver.java | 27 ++-- .../SMTInterpolSmtLibSolverFactory.java | 26 ++-- .../SMTInterpolSmtLibSolverInstaller.java | 11 +- .../solver/smtlib/solver/EnumStrategy.java | 125 +++++++++++++++++ .../solver/smtlib/solver/SmtLibItpSolver.java | 42 +++--- .../solver/smtlib/solver/SmtLibSolver.java | 91 ++++++------ .../smtlib/solver/model/SmtLibValuation.java | 6 +- .../solver/transformer/SmtLibSymbolTable.java | 7 + 21 files changed, 388 insertions(+), 228 deletions(-) create mode 100644 subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/EnumStrategy.java 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 707a80735c..5ca7759404 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 @@ -90,6 +90,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))); @@ -115,6 +119,8 @@ public Interpolant getInterpolant(ItpPattern pattern) { itpSolverBinary.issueCommand("(assert (= shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh 0))"); 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 1233550ba0..bed493ea87 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 @@ -82,6 +82,10 @@ 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.EnumEqExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumNeqExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumType; 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.FpAssignExpr; @@ -142,6 +146,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; @@ -155,13 +160,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(); @@ -262,6 +269,14 @@ protected DispatchTable.Builder buildDispatchTable(DispatchTable.Builder .addCase(IntToRatExpr.class, this::transformIntToRat) + // Enums + + .addCase(EnumLitExpr.class, this::transformEnumLit) + + .addCase(EnumNeqExpr.class, this::transformEnumNeq) + + .addCase(EnumEqExpr.class, this::transformEnumEq) + // Bitvectors .addCase(BvLitExpr.class, this::transformBvLit) @@ -722,6 +737,25 @@ protected String transformIntToRat(final IntToRatExpr expr) { return String.format("(to_real %s)", toTerm(expr.getOp())); } + /* + * Enums + */ + + protected String transformEnumEq(final EnumEqExpr expr) { + return String.format("(= %s %s)", toTerm(expr.getLeftOp()), toTerm(expr.getRightOp())); + } + + protected String transformEnumNeq(final EnumNeqExpr expr) { + return String.format("(not (= %s %s))", toTerm(expr.getLeftOp()), + toTerm(expr.getRightOp())); + } + + protected String transformEnumLit(final EnumLitExpr expr) { + String longName = EnumType.makeLongName(expr.getType(), expr.getValue()); + symbolTable.putEnumLiteral(longName, expr); + return longName; + } + /* * Bitvectors */ diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverBinary.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverBinary.java index 32eeb689a6..582cc70252 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverBinary.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverBinary.java @@ -34,6 +34,7 @@ public final class GenericSmtLibSolverBinary implements SmtLibSolverBinary { private final NuProcess solverProcess; private final ProcessHandler processHandler; + private final List issuedCommands = new ArrayList<>(); public GenericSmtLibSolverBinary(final Path solverPath, final String[] args) { this(solverPath, args, EnumSet.noneOf(Solver.class)); @@ -61,6 +62,7 @@ public GenericSmtLibSolverBinary(final Path solverPath, final String[] args, @Override public void issueCommand(final String command) { + issuedCommands.add(command); checkState(solverProcess.isRunning()); processHandler.write(command); solverProcess.wantWrite(); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverFactory.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverFactory.java index a544b9eb7c..3b37da0786 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverFactory.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverFactory.java @@ -20,6 +20,7 @@ import hu.bme.mit.theta.solver.Solver; import hu.bme.mit.theta.solver.SolverFactory; import hu.bme.mit.theta.solver.UCSolver; +import hu.bme.mit.theta.solver.smtlib.solver.EnumStrategy; import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolver; import java.nio.file.Path; @@ -27,6 +28,8 @@ public class GenericSmtLibSolverFactory implements SolverFactory { + protected final EnumStrategy enumStrategy; + protected final Path solverPath; protected final String[] args; private final EnumSet solverOverride; @@ -37,15 +40,31 @@ protected GenericSmtLibSolverFactory(Path solverPath, String[] args) { protected GenericSmtLibSolverFactory(Path solverPath, String[] args, EnumSet solverOverride) { + this(solverPath, args, solverOverride, EnumStrategy.SORTS); + } + + protected GenericSmtLibSolverFactory(Path solverPath, String[] args, + EnumStrategy enumStrategy) { + this(solverPath, args, EnumSet.noneOf(GenericSmtLibSolverBinary.Solver.class), enumStrategy); + } + + protected GenericSmtLibSolverFactory(Path solverPath, String[] args, + EnumSet solverOverride, + EnumStrategy enumStrategy) { this.solverPath = solverPath; this.args = args; this.solverOverride = solverOverride; + this.enumStrategy = enumStrategy; } public static GenericSmtLibSolverFactory create(Path solverPath, String[] args) { return new GenericSmtLibSolverFactory(solverPath, args); } + public static GenericSmtLibSolverFactory create(Path solverPath, String[] args, EnumStrategy enumStrategy) { + return new GenericSmtLibSolverFactory(solverPath, args, enumStrategy); + } + @Override public Solver createSolver() { final var symbolTable = new GenericSmtLibSymbolTable(); 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 f003780f0f..d4a9665ef9 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 b7192786ef..42df64c3b6 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,77 +28,16 @@ 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.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.abstracttype.*; 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.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.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.booltype.*; +import hu.bme.mit.theta.core.type.bvtype.*; +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.functype.FuncExprs; import hu.bme.mit.theta.core.type.functype.FuncLitExpr; import hu.bme.mit.theta.core.type.functype.FuncType; @@ -110,7 +49,7 @@ 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.Let_termContext; +import hu.bme.mit.theta.solver.smtlib.solver.EnumStrategy; 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; @@ -121,53 +60,36 @@ import java.math.BigDecimal; import java.math.BigInteger; -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.*; +import java.util.function.*; 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.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.booltype.BoolExprs.*; 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.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.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 hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.*; import static java.util.stream.Collectors.toList; public class GenericSmtLibTermTransformer implements SmtLibTermTransformer { protected final SmtLibSymbolTable symbolTable; protected final Map funAppTransformer; + protected final EnumStrategy enumStrategy; public GenericSmtLibTermTransformer(final SmtLibSymbolTable symbolTable) { + this(symbolTable, EnumStrategy.getDefaultStrategy()); + } + + public GenericSmtLibTermTransformer(final SmtLibSymbolTable symbolTable, final EnumStrategy enumStrategy) { this.symbolTable = symbolTable; + this.enumStrategy = enumStrategy; this.funAppTransformer = new HashMap<>() {{ // Generic put("ite", exprIteOperator()); @@ -304,6 +226,8 @@ private Expr toExpr(final String term, final SmtLibModel model) { @Override public LitExpr toLitExpr(final String litImpl, final T type, final SmtLibModel model) { + if (type instanceof EnumType enumType) + return (LitExpr) cast(toEnumLitExpr(litImpl, enumType, model), type); final var litExpr = toLitExpr(litImpl, model); if (litExpr == null) { @@ -336,6 +260,18 @@ private Expr toLitExpr(final String litImpl, final SmtLibModel model) { return expr; } + private EnumLitExpr toEnumLitExpr(final String litImpl, final EnumType type, final SmtLibModel model) { + final var lexer = new SMTLIBv2Lexer(CharStreams.fromString(litImpl)); + final var parser = new SMTLIBv2Parser(new CommonTokenStream(lexer)); + lexer.removeErrorListeners(); + lexer.addErrorListener(new ThrowExceptionErrorListener()); + parser.removeErrorListeners(); + parser.addErrorListener(new ThrowExceptionErrorListener()); + + final var funcDef = parser.function_def(); + return enumStrategy.transformEnumTerm(funcDef, type, model); + } + @Override @SuppressWarnings("unchecked") public LitExpr> toArrayLitExpr( @@ -621,8 +557,10 @@ 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); + throw new SmtLibSolverException("Transformation 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/generic/GenericSmtLibTypeTransformer.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTypeTransformer.java index ff6c8061d6..c0442f7ab7 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTypeTransformer.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTypeTransformer.java @@ -22,6 +22,7 @@ import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.type.fptype.FpType; import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.core.type.rattype.RatType; @@ -55,6 +56,7 @@ protected DispatchTable.Builder buildDispatchTable(DispatchTable.Builder .addCase(RatType.class, this::ratType) .addCase(BvType.class, this::bvType) .addCase(FpType.class, this::fpType) + .addCase(EnumType.class, this::enumType) .addCase(ArrayType.class, this::arrayType); return builder; } @@ -92,4 +94,8 @@ protected String arrayType(final ArrayType type) { return String.format("(Array %s %s)", toSort(type.getIndexType()), toSort(type.getElemType())); } + + protected String enumType(final EnumType type) { + return type.getName(); + } } 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/impl/princess/PrincessSmtLibItpSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibItpSolver.java index 8ab0bc7590..24f20adf58 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibItpSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibItpSolver.java @@ -19,13 +19,10 @@ import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolExprs; import hu.bme.mit.theta.core.type.booltype.BoolType; -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.SolverStatus; +import hu.bme.mit.theta.solver.*; 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.solver.EnumStrategy; import hu.bme.mit.theta.solver.smtlib.solver.SmtLibItpSolver; import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolverException; import hu.bme.mit.theta.solver.smtlib.solver.binary.SmtLibSolverBinary; @@ -44,9 +41,7 @@ import java.util.*; import java.util.stream.Collectors; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; -import static com.google.common.base.Preconditions.checkState; +import static com.google.common.base.Preconditions.*; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; public final class PrincessSmtLibItpSolver extends SmtLibItpSolver { @@ -58,9 +53,10 @@ public final class PrincessSmtLibItpSolver extends SmtLibItpSolver { @@ -65,9 +53,10 @@ public final class SMTInterpolSmtLibItpSolver extends SmtLibItpSolver final var name = String.format(assertionNamePattern, assertionCount++); assertionNames.put(assertion, name); - issueGeneralCommand(String.format("(assert (! %s :named %s))", term, name)); + issueGeneralCommand(String.format("(assert (! %s :named %s))", enumStrategy.wrapAssertionExpression(term, consts.stream().collect(Collectors.toMap(c -> c, symbolTable::getSymbol))), name)); } @Override diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverFactory.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverFactory.java index 4068d72f02..06d1ac81b1 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverFactory.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverFactory.java @@ -23,55 +23,59 @@ import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibSymbolTable; import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibTermTransformer; import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibTransformationManager; +import hu.bme.mit.theta.solver.smtlib.solver.EnumStrategy; import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolver; import java.nio.file.Path; public class SMTInterpolSmtLibSolverFactory implements SolverFactory { + private final EnumStrategy enumStrategy; + private final Path solverPath; private final String[] args; - private SMTInterpolSmtLibSolverFactory(Path solverPath, String[] args) { + private SMTInterpolSmtLibSolverFactory(Path solverPath, String[] args, final EnumStrategy enumStrategy) { this.solverPath = solverPath; this.args = args; + this.enumStrategy = enumStrategy; } - public static SMTInterpolSmtLibSolverFactory create(Path solverPath, String[] args) { - return new SMTInterpolSmtLibSolverFactory(solverPath, args); + public static SMTInterpolSmtLibSolverFactory create(Path solverPath, String[] args, final EnumStrategy enumStrategy) { + return new SMTInterpolSmtLibSolverFactory(solverPath, args, enumStrategy); } @Override public Solver createSolver() { final var symbolTable = new GenericSmtLibSymbolTable(); final var transformationManager = new GenericSmtLibTransformationManager(symbolTable); - final var termTransformer = new GenericSmtLibTermTransformer(symbolTable); + final var termTransformer = new GenericSmtLibTermTransformer(symbolTable, enumStrategy); final var solverBinary = new GenericSmtLibSolverBinary(getJavaBinary(), getSolverArgs()); return new SmtLibSolver(symbolTable, transformationManager, termTransformer, solverBinary, - false); + false, enumStrategy); } @Override public UCSolver createUCSolver() { final var symbolTable = new GenericSmtLibSymbolTable(); final var transformationManager = new GenericSmtLibTransformationManager(symbolTable); - final var termTransformer = new GenericSmtLibTermTransformer(symbolTable); + final var termTransformer = new GenericSmtLibTermTransformer(symbolTable, enumStrategy); final var solverBinary = new GenericSmtLibSolverBinary(getJavaBinary(), getSolverArgs()); return new SmtLibSolver(symbolTable, transformationManager, termTransformer, solverBinary, - true); + true, enumStrategy); } @Override public ItpSolver createItpSolver() { final var symbolTable = new GenericSmtLibSymbolTable(); final var transformationManager = new GenericSmtLibTransformationManager(symbolTable); - final var termTransformer = new GenericSmtLibTermTransformer(symbolTable); + final var termTransformer = new GenericSmtLibTermTransformer(symbolTable, enumStrategy); final var solverBinary = new GenericSmtLibSolverBinary(getJavaBinary(), getSolverArgs()); return new SMTInterpolSmtLibItpSolver(symbolTable, transformationManager, termTransformer, - solverBinary); + solverBinary, enumStrategy); } private Path getJavaBinary() { @@ -82,9 +86,7 @@ private String[] getSolverArgs() { final var solverArgs = new String[args.length + 2]; solverArgs[0] = "-jar"; solverArgs[1] = solverPath.toAbsolutePath().toString(); - for (var i = 0; i < args.length; i++) { - solverArgs[i + 2] = args[i]; - } + System.arraycopy(args, 0, solverArgs, 2, args.length); return solverArgs; } } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java index d8985637b1..a28ca58b3f 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java @@ -17,6 +17,7 @@ import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.solver.SolverFactory; +import hu.bme.mit.theta.solver.smtlib.solver.EnumStrategy; import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstaller; import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstallerException; @@ -76,7 +77,7 @@ public SolverFactory getSolverFactory(final Path installDir, final String versio final Path solverPath, final String[] solverArgs) throws SmtLibSolverInstallerException { final var solverFilePath = solverPath != null ? solverPath : installDir.resolve(getSolverBinaryName(version)); - return SMTInterpolSmtLibSolverFactory.create(solverFilePath, solverArgs); + return SMTInterpolSmtLibSolverFactory.create(solverFilePath, solverArgs, getEnumStrategyForVersion(version)); } @Override @@ -108,4 +109,12 @@ private URL getDownloadUrl(final String version) private String getSolverBinaryName(final String version) { return String.format("smtinterpol-%s.jar", version); } + + private EnumStrategy getEnumStrategyForVersion(final String version) { + // pre-release version 2.5-1301-g2c871e40 already suppoprted datatype interpolation + if (Integer.valueOf(version.split("-")[1]) > 1256) { + return EnumStrategy.DATATYPES; + } + return EnumStrategy.SORTS; + } } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/EnumStrategy.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/EnumStrategy.java new file mode 100644 index 0000000000..8c53e2a427 --- /dev/null +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/EnumStrategy.java @@ -0,0 +1,125 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.solver.smtlib.solver; + +import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumType; +import hu.bme.mit.theta.solver.Stack; +import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser; +import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Function_defContext; +import hu.bme.mit.theta.solver.smtlib.solver.model.SmtLibModel; + +import java.util.*; +import java.util.function.Consumer; + +/** + * EnumTypes need to be handled on SMT solvers too. SmtLib standard contains datatypes, and the + * behaviour for that is implemented in the DATATYPES strategy. However, most solvers don't support + * interpolation with datatypes. For this, a workaround is implemented in the SORTS strategy. + */ +public enum EnumStrategy { + + DATATYPES { + @Override + public void declareDatatypes(final Collection allTypes, final Stack typeStack, final Consumer issueGeneralCommand) { + List types = new ArrayList<>(allTypes); + types.removeAll(typeStack.toCollection()); + Set typeSet = new HashSet<>(types); + for (Type t : + typeSet) { + if (t instanceof EnumType enumType) { + typeStack.add(enumType); + Collection literals = enumType.getLongValues().stream().map(name -> String.format("(%s)", name)).toList(); + issueGeneralCommand.accept(String.format("(declare-datatypes ((%s 0)) ((%s)))", enumType.getName(), String.join(" ", literals))); + } + } + } + + @Override + public EnumLitExpr transformEnumTerm(Function_defContext funcDef, EnumType type, SmtLibModel model) { + final String longName = funcDef.term().qual_identifier().identifier().symbol().getText(); + return type.litFromLongName(longName); + } + }, + + SORTS { + @Override + public void declareDatatypes(Collection allTypes, Stack typeStack, Consumer issueGeneralCommand) { + List types = new ArrayList<>(allTypes); + types.removeAll(typeStack.toCollection()); + Set typeSet = new HashSet<>(types); + for (Type t : + typeSet) { + if (t instanceof EnumType enumType) { + typeStack.add(enumType); + issueGeneralCommand.accept(String.format("(declare-sort %s 0)", enumType.getName())); + enumType.getLongValues().forEach(literal -> issueGeneralCommand.accept(String.format("(declare-const %s %s)", literal, enumType.getName()))); + issueGeneralCommand.accept(String.format("(assert (distinct %s))", String.join(" ", enumType.getLongValues()))); + } + } + } + + @Override + public String wrapAssertionExpression(String assertion, Map, String> consts) { + boolean needsWrap = false; + StringBuilder sb = new StringBuilder("(and ").append(assertion); + for (var constDeclEntry : consts.entrySet()) { + var constDecl = constDeclEntry.getKey(); + var nameOnSolver = constDeclEntry.getValue(); + if (constDecl.getType() instanceof EnumType enumType) { + sb.append(" (or"); + enumType.getLongValues().forEach(val -> sb.append(String.format(" (= %s %s)", nameOnSolver, val))); + sb.append(")"); + needsWrap = true; + } + } + sb.append(")"); + return needsWrap ? sb.toString() : assertion; + } + + @Override + public EnumLitExpr transformEnumTerm(Function_defContext funcDef, EnumType type, SmtLibModel model) { + final String id = funcDef.term().qual_identifier().identifier().symbol().getText(); + for (var lit : type.getLongValues()) { + if (model.getTerm(lit).contains(id)) + return type.litFromLongName(lit); + } + throw new RuntimeException(); + } + }; + + + public abstract void declareDatatypes(final Collection allTypes, final Stack typeStack, final Consumer issueGeneralCommand); + + /** + * Wraps an expression with additional ones if needed. + * + * @param assertion the expression part that was going to be asserted. (e.g. "(= x 1)") + * @param consts all variables part of the expression + */ + public String wrapAssertionExpression(final String assertion, final Map, String> consts) { + return assertion; + } + + public abstract EnumLitExpr transformEnumTerm(final SMTLIBv2Parser.Function_defContext funcDef, final EnumType type, final SmtLibModel model); + + public static EnumStrategy getDefaultStrategy() { + return EnumStrategy.SORTS; + } + +} 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 6fe9ce060c..44342a5561 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 @@ -18,16 +18,11 @@ import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; 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.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.*; 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; @@ -46,10 +41,9 @@ import java.util.Collection; import java.util.Set; +import java.util.stream.Collectors; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; -import static com.google.common.base.Preconditions.checkState; +import static com.google.common.base.Preconditions.*; public abstract class SmtLibItpSolver implements ItpSolver { @@ -62,6 +56,8 @@ public abstract class SmtLibItpSolver implements ItpS protected final Stack> assertions; protected final Stack markers; protected final Stack> declarationStack; + protected final Stack typeStack; + protected final EnumStrategy enumStrategy; private Valuation model; private SolverStatus status; @@ -71,22 +67,31 @@ public SmtLibItpSolver( final SmtLibSymbolTable symbolTable, final SmtLibTransformationManager transformationManager, final SmtLibTermTransformer termTransformer, final SmtLibSolverBinary solverBinary + ) { + this(symbolTable, transformationManager, termTransformer, solverBinary, EnumStrategy.getDefaultStrategy()); + } + + public SmtLibItpSolver( + final SmtLibSymbolTable symbolTable, + final SmtLibTransformationManager transformationManager, + final SmtLibTermTransformer termTransformer, final SmtLibSolverBinary solverBinary, + final EnumStrategy enumStrategy ) { this.symbolTable = symbolTable; this.transformationManager = transformationManager; this.termTransformer = termTransformer; + this.enumStrategy = enumStrategy; this.solverBinary = solverBinary; this.assertions = new StackImpl<>(); this.markers = new StackImpl<>(); this.declarationStack = new StackImpl<>(); + typeStack = new StackImpl<>(); init(); } - @Override - public abstract ItpPattern createTreePattern(ItpMarkerTree root); @Override public abstract T createMarker(); @@ -107,13 +112,15 @@ public void add(final ItpMarker marker, final Expr assertion) { final var consts = ExprUtils.getConstants(assertion); consts.removeAll(declarationStack.toCollection()); declarationStack.add(consts); + enumStrategy.declareDatatypes((Collection) consts.stream().map(ConstDecl::getType).toList(), typeStack, this::issueGeneralCommand); final var itpMarker = (T) marker; final var term = transformationManager.toTerm(assertion); - itpMarker.add(assertion, term); + + itpMarker.add(assertion, enumStrategy.wrapAssertionExpression(term, ExprUtils.getConstants(assertion).stream().collect(Collectors.toMap(c -> c, symbolTable::getSymbol)))); assertions.add(assertion); - add(itpMarker, assertion, consts, term); + add(itpMarker, assertion, consts, enumStrategy.wrapAssertionExpression(term, ExprUtils.getConstants(assertion).stream().collect(Collectors.toMap(c -> c, symbolTable::getSymbol)))); clearState(); } @@ -151,6 +158,7 @@ public void push() { } assertions.push(); declarationStack.push(); + typeStack.push(); issueGeneralCommand("(push 1)"); } @@ -162,6 +170,7 @@ public void pop(final int n) { } assertions.pop(n); declarationStack.pop(n); + typeStack.pop(n); issueGeneralCommand(String.format("(pop %d)", n)); clearState(); } @@ -207,9 +216,6 @@ private Valuation extractModel() { } } - @Override - public abstract Interpolant getInterpolant(ItpPattern pattern); - @Override public Collection> getAssertions() { return assertions.toCollection(); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java index 9cbd53991b..0183b7a015 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java @@ -18,51 +18,42 @@ import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; 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.Solver; -import hu.bme.mit.theta.solver.SolverStatus; import hu.bme.mit.theta.solver.Stack; -import hu.bme.mit.theta.solver.UCSolver; -import hu.bme.mit.theta.solver.UnknownSolverStatusException; +import hu.bme.mit.theta.solver.*; 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; import hu.bme.mit.theta.solver.smtlib.solver.binary.SmtLibSolverBinary; import hu.bme.mit.theta.solver.smtlib.solver.model.SmtLibValuation; -import hu.bme.mit.theta.solver.smtlib.solver.parser.CheckSatResponse; -import hu.bme.mit.theta.solver.smtlib.solver.parser.GeneralResponse; -import hu.bme.mit.theta.solver.smtlib.solver.parser.GetModelResponse; -import hu.bme.mit.theta.solver.smtlib.solver.parser.GetUnsatCoreResponse; -import hu.bme.mit.theta.solver.smtlib.solver.parser.ThrowExceptionErrorListener; +import hu.bme.mit.theta.solver.smtlib.solver.parser.*; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibSymbolTable; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTermTransformer; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTransformationManager; import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.CommonTokenStream; -import java.util.Collection; -import java.util.Collections; -import java.util.HashMap; -import java.util.LinkedList; -import java.util.Map; +import java.util.*; +import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkState; public class SmtLibSolver implements UCSolver, Solver { + private static final String ASSUMPTION_LABEL = "_LABEL_%d"; protected final SmtLibSymbolTable symbolTable; protected final SmtLibTransformationManager transformationManager; protected final SmtLibTermTransformer termTransformer; - protected final SmtLibSolverBinary solverBinary; - private final boolean unsatCoreEnabled; - protected final Stack> assertions; protected final Map> assumptions; protected final Stack> declarationStack; - - private static final String ASSUMPTION_LABEL = "_LABEL_%d"; + protected final Stack typeStack; + protected final EnumStrategy enumStrategy; + private final boolean unsatCoreEnabled; private int labelNum = 0; private Valuation model; @@ -74,34 +65,38 @@ public SmtLibSolver( final SmtLibTransformationManager transformationManager, final SmtLibTermTransformer termTransformer, final SmtLibSolverBinary solverBinary, boolean unsatCoreEnabled + ) { + this(symbolTable, transformationManager, termTransformer, solverBinary, unsatCoreEnabled, EnumStrategy.getDefaultStrategy()); + } + + public SmtLibSolver( + final SmtLibSymbolTable symbolTable, + final SmtLibTransformationManager transformationManager, + final SmtLibTermTransformer termTransformer, final SmtLibSolverBinary solverBinary, + boolean unsatCoreEnabled, + final EnumStrategy enumStrategy ) { this.solverBinary = solverBinary; this.symbolTable = symbolTable; this.transformationManager = transformationManager; this.termTransformer = termTransformer; + this.enumStrategy = enumStrategy; this.unsatCoreEnabled = unsatCoreEnabled; assertions = new StackImpl<>(); assumptions = new HashMap<>(); declarationStack = new StackImpl<>(); + typeStack = new StackImpl<>(); init(); } @Override public void add(Expr assertion) { - final var consts = ExprUtils.getConstants(assertion); - consts.removeAll(declarationStack.toCollection()); - declarationStack.add(consts); - - final var term = transformationManager.toTerm(assertion); - - assertions.add(assertion); - consts.stream().map(symbolTable::getDeclaration).forEach(this::issueGeneralCommand); - issueGeneralCommand(String.format("(assert %s)", term)); - - clearState(); + final var simplifiedAssertion = ExprUtils.simplify(assertion); + final var term = transformationManager.toTerm(simplifiedAssertion); + add(simplifiedAssertion, term); } public void add(final Expr assertion, final String term) { @@ -110,8 +105,9 @@ public void add(final Expr assertion, final String term) { declarationStack.add(consts); assertions.add(assertion); + enumStrategy.declareDatatypes((Collection) consts.stream().map(ConstDecl::getType).toList(), typeStack, this::issueGeneralCommand); consts.stream().map(symbolTable::getDeclaration).forEach(this::issueGeneralCommand); - issueGeneralCommand(String.format("(assert %s)", term)); + issueGeneralCommand(String.format("(assert %s)", enumStrategy.wrapAssertionExpression(term, ExprUtils.getConstants(assertion).stream().collect(Collectors.toMap(c -> c, symbolTable::getSymbol))))); clearState(); } @@ -128,7 +124,8 @@ public void track(Expr assertion) { assertions.add(assertion); consts.stream().map(symbolTable::getDeclaration).forEach(this::issueGeneralCommand); - issueGeneralCommand(String.format("(assert (! %s :named %s))", term, label)); + enumStrategy.declareDatatypes((Collection) consts.stream().map(ConstDecl::getType).toList(), typeStack, this::issueGeneralCommand); + issueGeneralCommand(String.format("(assert (! %s :named %s))", enumStrategy.wrapAssertionExpression(term, ExprUtils.getConstants(assertion).stream().collect(Collectors.toMap(c -> c, symbolTable::getSymbol))), label)); clearState(); } @@ -136,29 +133,32 @@ public void track(Expr assertion) { @Override public SolverStatus check() { solverBinary.issueCommand("(check-sat)"); - var res = parseResponse(solverBinary.readResponse()); + + final String rp = solverBinary.readResponse(); + final var res = parseResponse(rp); if (res.isError()) { throw new SmtLibSolverException(res.getReason()); - } else if (res.isSpecific()) { - final CheckSatResponse checkSatResponse = res.asSpecific().asCheckSatResponse(); - if (checkSatResponse.isSat()) { - status = SolverStatus.SAT; - } else if (checkSatResponse.isUnsat()) { - status = SolverStatus.UNSAT; - } else { - throw new UnknownSolverStatusException(); - } - } else { + } + if (!res.isSpecific()) { throw new AssertionError(); } - - return status; + final CheckSatResponse checkSatResponse = res.asSpecific().asCheckSatResponse(); + if (checkSatResponse.isSat()) { + status = SolverStatus.SAT; + return status; + } + if (checkSatResponse.isUnsat()) { + status = SolverStatus.UNSAT; + return status; + } + throw new UnknownSolverStatusException(); } @Override public void push() { assertions.push(); declarationStack.push(); + typeStack.push(); issueGeneralCommand("(push 1)"); } @@ -166,6 +166,7 @@ public void push() { public void pop(int n) { assertions.pop(n); declarationStack.pop(n); + typeStack.pop(n); issueGeneralCommand("(pop 1)"); clearState(); } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/model/SmtLibValuation.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/model/SmtLibValuation.java index 37ed606968..0f88e2d4ff 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/model/SmtLibValuation.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/model/SmtLibValuation.java @@ -28,11 +28,7 @@ import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTermTransformer; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTransformationManager; -import java.util.Collection; -import java.util.Collections; -import java.util.HashMap; -import java.util.Map; -import java.util.Optional; +import java.util.*; import static com.google.common.base.Preconditions.checkNotNull; 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); }