Skip to content

Commit

Permalink
Introduce datatypes for smtlib
Browse files Browse the repository at this point in the history
  • Loading branch information
@RipplB
RipplB authored and RipplB committed Jun 29, 2024
1 parent 0ae875a commit 0f04e87
Show file tree
Hide file tree
Showing 21 changed files with 388 additions and 228 deletions.
6 changes: 6 additions & 0 deletions ...er-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<String> 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)));

Expand All @@ -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(" "))));
Expand Down
36 changes: 35 additions & 1 deletion ...c/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand All @@ -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<Expr<?>, String> exprToTerm;
private final DispatchTable<String> 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();
Expand Down Expand Up @@ -262,6 +269,14 @@ protected DispatchTable.Builder<String> 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)
Expand Down Expand Up @@ -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
*/
Expand Down
2 changes: 2 additions & 0 deletions .../src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverBinary.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ public final class GenericSmtLibSolverBinary implements SmtLibSolverBinary {

private final NuProcess solverProcess;
private final ProcessHandler processHandler;
private final List<String> issuedCommands = new ArrayList<>();

public GenericSmtLibSolverBinary(final Path solverPath, final String[] args) {
this(solverPath, args, EnumSet.noneOf(Solver.class));
Expand Down Expand Up @@ -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();
Expand Down
19 changes: 19 additions & 0 deletions ...src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,16 @@
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;
import java.util.EnumSet;

public class GenericSmtLibSolverFactory implements SolverFactory {

protected final EnumStrategy enumStrategy;

protected final Path solverPath;
protected final String[] args;
private final EnumSet<GenericSmtLibSolverBinary.Solver> solverOverride;
Expand All @@ -37,15 +40,31 @@ protected GenericSmtLibSolverFactory(Path solverPath, String[] args) {

protected GenericSmtLibSolverFactory(Path solverPath, String[] args,
EnumSet<GenericSmtLibSolverBinary.Solver> 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<GenericSmtLibSolverBinary.Solver> 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();
Expand Down
23 changes: 23 additions & 0 deletions ...b/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -32,17 +36,21 @@ public class GenericSmtLibSymbolTable implements SmtLibSymbolTable {

private final BiMap<ConstDecl<?>, String> constToSymbol;
private final BiMap<ConstDecl<?>, String> constToDeclaration;
private final Map<String, EnumLitExpr> symbolToEnumLiteral;

public GenericSmtLibSymbolTable() {
constToSymbol = Maps.synchronizedBiMap(HashBiMap.create());
constToDeclaration = Maps.synchronizedBiMap(HashBiMap.create());
symbolToEnumLiteral = new HashMap<>();
}

public GenericSmtLibSymbolTable(GenericSmtLibSymbolTable table) {
constToSymbol = Maps.synchronizedBiMap(HashBiMap.create());
constToSymbol.putAll(table.constToSymbol);
constToDeclaration = Maps.synchronizedBiMap(HashBiMap.create());
constToDeclaration.putAll(table.constToDeclaration);
symbolToEnumLiteral = new HashMap<>();
symbolToEnumLiteral.putAll(table.symbolToEnumLiteral);
}

@Override
Expand All @@ -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));
Expand All @@ -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);
Expand All @@ -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);
}
}
Loading

0 comments on commit 0f04e87

Please sign in to comment.