From cfbc083862dedc509df2b2f8e57586ad0e4b4ca7 Mon Sep 17 00:00:00 2001 From: RipplB Date: Sun, 23 Jun 2024 13:04:46 +0200 Subject: [PATCH] Use FunctionDeclarationKind instead of function name to match Theta expressions --- .../javasmt/JavaSMTTermTransformer.java | 230 +++++++++--------- 1 file changed, 115 insertions(+), 115 deletions(-) diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java index c14d63856c..8abf5606e4 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java @@ -57,6 +57,7 @@ import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; import org.sosy_lab.java_smt.api.SolverContext; @@ -97,118 +98,119 @@ final class JavaSMTTermTransformer { private final JavaSMTSymbolTable symbolTable; private final SolverContext context; - private final Map, QuadFunction, Model, List>, Expr>> environment; + private final Map, QuadFunction, Model, List>, Expr>> environment; public JavaSMTTermTransformer(final JavaSMTSymbolTable symbolTable, SolverContext context) { this.symbolTable = symbolTable; this.context = context; environment = Containers.createMap(); - addFunc("and", exprMultiaryOperator(hu.bme.mit.theta.core.type.booltype.AndExpr::create)); - addFunc("false", exprNullaryOperator(hu.bme.mit.theta.core.type.booltype.FalseExpr::getInstance)); - addFunc("true", exprNullaryOperator(hu.bme.mit.theta.core.type.booltype.TrueExpr::getInstance)); - addFunc("iff", exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.IffExpr::create)); - addFunc("not", exprUnaryOperator(hu.bme.mit.theta.core.type.booltype.NotExpr::create)); - addFunc("=>", exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.ImplyExpr::create)); - addFunc("xor", exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.XorExpr::create)); - addFunc("or", exprMultiaryOperator(hu.bme.mit.theta.core.type.booltype.OrExpr::create)); - addFunc("ite", exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create)); - addFunc("if", exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create)); - addFunc("prime", exprUnaryOperator(hu.bme.mit.theta.core.type.anytype.PrimeExpr::of)); - addFunc("=", exprBinaryOperator((expr, expr2) -> expr.getType() instanceof FpType ? FpAssign((Expr) expr, (Expr) expr2) : Eq(expr, expr2))); - addFunc(">=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Geq)); - addFunc(">", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Gt)); - addFunc("<=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Leq)); - addFunc("<", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Lt)); - addFunc("+", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Add)); - addFunc("-", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Sub)); - addFunc("+", exprUnaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Pos)); - addFunc("-", exprUnaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Neg)); - addFunc("*", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Mul)); - addFunc("/", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Div)); - addFunc("to_int", exprUnaryOperator(hu.bme.mit.theta.core.type.rattype.RatToIntExpr::create)); - addFunc("div", exprBinaryOperator(hu.bme.mit.theta.core.type.inttype.IntDivExpr::create)); - addFunc("to_rat", exprUnaryOperator(hu.bme.mit.theta.core.type.inttype.IntToRatExpr::create)); - addFunc("mod", exprBinaryOperator(hu.bme.mit.theta.core.type.inttype.IntModExpr::create)); - addFunc("rem", exprBinaryOperator(hu.bme.mit.theta.core.type.inttype.IntRemExpr::create)); - addFunc("fp.add", exprFpMultiaryOperator(hu.bme.mit.theta.core.type.fptype.FpAddExpr::create)); - addFunc("fp.sub", exprFpBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpSubExpr::create)); - addFunc("fp.pos", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpPosExpr::create)); - addFunc("fp.neg", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpNegExpr::create)); - addFunc("fp.mul", exprFpMultiaryOperator(hu.bme.mit.theta.core.type.fptype.FpMulExpr::create)); - addFunc("fp.div", exprFpBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpDivExpr::create)); - addFunc("fp.rem", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpRemExpr::create)); - addFunc("fprem", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpRemExpr::create)); - addFunc("fp.abs", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpAbsExpr::create)); - addFunc("fp.leq", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpLeqExpr::create)); - addFunc("fp.lt", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpLtExpr::create)); - addFunc("fp.geq", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpGeqExpr::create)); - addFunc("fp.gt", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpGtExpr::create)); - addFunc("fp.eq", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpEqExpr::create)); - addFunc("fp.isnan", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsNanExpr::create)); - addFunc("fp.isNaN", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsNanExpr::create)); - addFunc("isinfinite", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr::create)); - addFunc("fp.isInfinite", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr::create)); - addFunc("fp.roundtoint", exprFpUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr::create)); - addFunc("fp.roundToIntegral", exprFpUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr::create)); - addFunc("fp.sqrt", exprFpUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpSqrtExpr::create)); - addFunc("fp.max", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpMaxExpr::create)); - addFunc("fp.min", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpMinExpr::create)); - addFunc("++", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvConcatExpr::create)); - addFunc("concat", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvConcatExpr::create)); - addFunc("bvadd", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvAddExpr::create)); - addFunc("bvsub", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSubExpr::create)); - addFunc("bvpos", exprUnaryOperator(hu.bme.mit.theta.core.type.bvtype.BvPosExpr::create)); - addFunc("bvneg", exprUnaryOperator(hu.bme.mit.theta.core.type.bvtype.BvNegExpr::create)); - addFunc("bvmul", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvMulExpr::create)); - addFunc("bvudiv", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUDivExpr::create)); - addFunc("bvsdiv", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSDivExpr::create)); - addFunc("bvsmod", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSModExpr::create)); - addFunc("bvurem", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvURemExpr::create)); - addFunc("bvsrem", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSRemExpr::create)); - addFunc("bvor", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvOrExpr::create)); - addFunc("bvand", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvAndExpr::create)); - addFunc("bvxor", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvXorExpr::create)); - addFunc("bvnot", exprUnaryOperator(hu.bme.mit.theta.core.type.bvtype.BvNotExpr::create)); - addFunc("bvshl", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr::create)); - addFunc("bvashr", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr::create)); - addFunc("bvlshr", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr::create)); - addFunc("bvrol", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr::create)); - addFunc("ext_rotate_left", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr::create)); - addFunc("bvror", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr::create)); - addFunc("ext_rotate_right", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr::create)); - addFunc("bvult", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvULtExpr::create)); - addFunc("bvule", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvULeqExpr::create)); - addFunc("bvugt", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUGtExpr::create)); - addFunc("bvuge", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr::create)); - addFunc("bvslt", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSLtExpr::create)); - addFunc("bvsle", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSLeqExpr::create)); - addFunc("bvsgt", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSGtExpr::create)); - addFunc("bvsge", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSGeqExpr::create)); - addFunc("read", exprBinaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr::create)); - addFunc("write", exprTernaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr::create)); - addFunc("select", exprBinaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr::create)); - addFunc("store", exprTernaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr::create)); - - environment.put(Tuple2.of("fp.frombv", 1), (term, args, model, vars) -> { + addFunc(FunctionDeclarationKind.AND, exprMultiaryOperator(hu.bme.mit.theta.core.type.booltype.AndExpr::create)); +// addFunc("false", exprNullaryOperator(hu.bme.mit.theta.core.type.booltype.FalseExpr::getInstance)); +// addFunc("true", exprNullaryOperator(hu.bme.mit.theta.core.type.booltype.TrueExpr::getInstance)); + addFunc(FunctionDeclarationKind.IFF, exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.IffExpr::create)); + addFunc(FunctionDeclarationKind.NOT, exprUnaryOperator(hu.bme.mit.theta.core.type.booltype.NotExpr::create)); + addFunc(FunctionDeclarationKind.IMPLIES, exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.ImplyExpr::create)); + addFunc(FunctionDeclarationKind.XOR, exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.XorExpr::create)); + addFunc(FunctionDeclarationKind.OR, exprMultiaryOperator(hu.bme.mit.theta.core.type.booltype.OrExpr::create)); + addFunc(FunctionDeclarationKind.ITE, exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create)); +// addFunc("if", exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create)); +// addFunc("prime", exprUnaryOperator(hu.bme.mit.theta.core.type.anytype.PrimeExpr::of)); + addFunc(FunctionDeclarationKind.EQ, exprBinaryOperator((expr, expr2) -> expr.getType() instanceof FpType ? FpAssign((Expr) expr, (Expr) expr2) : Eq(expr, expr2))); + addFunc(FunctionDeclarationKind.GTE, exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Geq)); + addFunc(FunctionDeclarationKind.GT, exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Gt)); + addFunc(FunctionDeclarationKind.LTE, exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Leq)); + addFunc(FunctionDeclarationKind.LT, exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Lt)); + addFunc(FunctionDeclarationKind.ADD, exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Add)); + addFunc(FunctionDeclarationKind.SUB, exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Sub)); +// addFunc("+", exprUnaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Pos)); + addFunc(FunctionDeclarationKind.UMINUS, exprUnaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Neg)); + addFunc(FunctionDeclarationKind.MUL, exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Mul)); + addFunc(FunctionDeclarationKind.DIV, exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Div)); + addFunc(FunctionDeclarationKind.FLOOR, exprUnaryOperator(hu.bme.mit.theta.core.type.rattype.RatToIntExpr::create)); + addFunc(FunctionDeclarationKind.FP_ROUND_TO_INTEGRAL, exprUnaryOperator(hu.bme.mit.theta.core.type.rattype.RatToIntExpr::create)); +// addFunc("div", exprBinaryOperator(hu.bme.mit.theta.core.type.inttype.IntDivExpr::create)); + addFunc(FunctionDeclarationKind.TO_REAL, exprUnaryOperator(hu.bme.mit.theta.core.type.inttype.IntToRatExpr::create)); + addFunc(FunctionDeclarationKind.MODULO, exprBinaryOperator(hu.bme.mit.theta.core.type.inttype.IntModExpr::create)); +// addFunc("rem", exprBinaryOperator(hu.bme.mit.theta.core.type.inttype.IntRemExpr::create)); + addFunc(FunctionDeclarationKind.FP_ADD, exprFpMultiaryOperator(hu.bme.mit.theta.core.type.fptype.FpAddExpr::create)); + addFunc(FunctionDeclarationKind.FP_SUB, exprFpBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpSubExpr::create)); +// addFunc("fp.pos", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpPosExpr::create)); + addFunc(FunctionDeclarationKind.FP_NEG, exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpNegExpr::create)); + addFunc(FunctionDeclarationKind.FP_MUL, exprFpMultiaryOperator(hu.bme.mit.theta.core.type.fptype.FpMulExpr::create)); + addFunc(FunctionDeclarationKind.FP_DIV, exprFpBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpDivExpr::create)); +// addFunc("fp.rem", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpRemExpr::create)); +// addFunc("fprem", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpRemExpr::create)); + addFunc(FunctionDeclarationKind.FP_ABS, exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpAbsExpr::create)); + addFunc(FunctionDeclarationKind.FP_LE, exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpLeqExpr::create)); + addFunc(FunctionDeclarationKind.FP_LT, exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpLtExpr::create)); + addFunc(FunctionDeclarationKind.FP_GE, exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpGeqExpr::create)); + addFunc(FunctionDeclarationKind.FP_GT, exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpGtExpr::create)); + addFunc(FunctionDeclarationKind.FP_EQ, exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpEqExpr::create)); + addFunc(FunctionDeclarationKind.FP_IS_NAN, exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsNanExpr::create)); +// addFunc("fp.isNaN", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsNanExpr::create)); + addFunc(FunctionDeclarationKind.FP_IS_INF, exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr::create)); +// addFunc("fp.isInfinite", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr::create)); + addFunc(FunctionDeclarationKind.FP_ROUND_TO_INTEGRAL, exprFpUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr::create)); +// addFunc("fp.roundToIntegral", exprFpUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr::create)); + addFunc(FunctionDeclarationKind.FP_SQRT, exprFpUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpSqrtExpr::create)); + addFunc(FunctionDeclarationKind.FP_MAX, exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpMaxExpr::create)); + addFunc(FunctionDeclarationKind.FP_MIN, exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpMinExpr::create)); + addFunc(FunctionDeclarationKind.BV_CONCAT, exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvConcatExpr::create)); +// addFunc("concat", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvConcatExpr::create)); + addFunc(FunctionDeclarationKind.BV_ADD, exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvAddExpr::create)); + addFunc(FunctionDeclarationKind.BV_SUB, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSubExpr::create)); +// addFunc("bvpos", exprUnaryOperator(hu.bme.mit.theta.core.type.bvtype.BvPosExpr::create)); + addFunc(FunctionDeclarationKind.BV_NEG, exprUnaryOperator(hu.bme.mit.theta.core.type.bvtype.BvNegExpr::create)); + addFunc(FunctionDeclarationKind.BV_MUL, exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvMulExpr::create)); + addFunc(FunctionDeclarationKind.BV_UDIV, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUDivExpr::create)); + addFunc(FunctionDeclarationKind.BV_SDIV, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSDivExpr::create)); +// addFunc("bvsmod", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSModExpr::create)); +// addFunc("bvurem", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvURemExpr::create)); +// addFunc("bvsrem", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSRemExpr::create)); + addFunc(FunctionDeclarationKind.BV_OR, exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvOrExpr::create)); + addFunc(FunctionDeclarationKind.BV_AND, exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvAndExpr::create)); + addFunc(FunctionDeclarationKind.BV_XOR, exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvXorExpr::create)); + addFunc(FunctionDeclarationKind.BV_NOT, exprUnaryOperator(hu.bme.mit.theta.core.type.bvtype.BvNotExpr::create)); + addFunc(FunctionDeclarationKind.BV_SHL, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr::create)); + addFunc(FunctionDeclarationKind.BV_ASHR, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr::create)); + addFunc(FunctionDeclarationKind.BV_LSHR, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr::create)); +// addFunc("bvrol", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr::create)); +// addFunc("ext_rotate_left", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr::create)); +// addFunc("bvror", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr::create)); +// addFunc("ext_rotate_right", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr::create)); + addFunc(FunctionDeclarationKind.BV_ULT, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvULtExpr::create)); + addFunc(FunctionDeclarationKind.BV_ULE, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvULeqExpr::create)); + addFunc(FunctionDeclarationKind.BV_UGT, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUGtExpr::create)); + addFunc(FunctionDeclarationKind.BV_UGE, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr::create)); + addFunc(FunctionDeclarationKind.BV_SLT, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSLtExpr::create)); + addFunc(FunctionDeclarationKind.BV_SLE, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSLeqExpr::create)); + addFunc(FunctionDeclarationKind.BV_SGT, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSGtExpr::create)); + addFunc(FunctionDeclarationKind.BV_SGE, exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSGeqExpr::create)); +// addFunc("read", exprBinaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr::create)); +// addFunc("write", exprTernaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr::create)); + addFunc(FunctionDeclarationKind.SELECT, exprBinaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr::create)); + addFunc(FunctionDeclarationKind.STORE, exprTernaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr::create)); + + environment.put(Tuple2.of(FunctionDeclarationKind.FP_FROM_IEEEBV, 1), (term, args, model, vars) -> { FloatingPointType type = (FloatingPointType) context.getFormulaManager().getFormulaType((FloatingPointFormula) term); final var roundingmode = getRoundingMode(args.get(0).toString()); final Expr op = (Expr) transform(args.get(1), model, vars); return FpFromBvExpr.of(roundingmode, op, FpType.of(type.getExponentSize(), type.getMantissaSize() + 1), true); }); - environment.put(Tuple2.of("fp.to_sbv", 2), (term, args, model, vars) -> { + environment.put(Tuple2.of(FunctionDeclarationKind.FP_CASTTO_SBV, 2), (term, args, model, vars) -> { BitvectorType type = (BitvectorType) context.getFormulaManager().getFormulaType((BitvectorFormula) term); final var roundingmode = getRoundingMode(args.get(0).toString()); final Expr op = (Expr) transform(args.get(1), model, vars); return FpToBvExpr.of(roundingmode, op, type.getSize(), true); }); - environment.put(Tuple2.of("fp.to_ubv", 2), (term, args, model, vars) -> { + environment.put(Tuple2.of(FunctionDeclarationKind.FP_CASTTO_SBV, 2), (term, args, model, vars) -> { BitvectorType type = (BitvectorType) context.getFormulaManager().getFormulaType((BitvectorFormula) term); final var roundingmode = getRoundingMode(args.get(0).toString()); final Expr op = (Expr) transform(args.get(1), model, vars); return FpToBvExpr.of(roundingmode, op, type.getSize(), false); }); - environment.put(Tuple2.of("to_fp", 2), (term, args, model, vars) -> { + environment.put(Tuple2.of(FunctionDeclarationKind.FP_CASTTO_FP, 2), (term, args, model, vars) -> { FloatingPointType type = (FloatingPointType) context.getFormulaManager().getFormulaType((FloatingPointFormula) term); final var roundingmode = getRoundingMode(args.get(0).toString()); final Expr op = transform(args.get(1), model, vars); @@ -220,13 +222,13 @@ public JavaSMTTermTransformer(final JavaSMTSymbolTable symbolTable, SolverContex throw new JavaSMTSolverException("Unsupported:" + op.getType()); } }); - environment.put(Tuple2.of("to_fp", 1), (term, args, model, vars) -> { - FloatingPointType type = (FloatingPointType) context.getFormulaManager().getFormulaType((FloatingPointFormula) term); - final Expr op = (Expr) transform(args.get(0), model, vars); - return FpFromBvExpr.of(FpRoundingMode.getDefaultRoundingMode(), op, FpType.of(type.getExponentSize(), type.getMantissaSize() + 1), true); - }); +// environment.put(Tuple2.of("to_fp", 1), (term, args, model, vars) -> { +// FloatingPointType type = (FloatingPointType) context.getFormulaManager().getFormulaType((FloatingPointFormula) term); +// final Expr op = (Expr) transform(args.get(0), model, vars); +// return FpFromBvExpr.of(FpRoundingMode.getDefaultRoundingMode(), op, FpType.of(type.getExponentSize(), type.getMantissaSize() + 1), true); +// }); - environment.put(Tuple2.of("extract", 1), (term, args, model, vars) -> { + environment.put(Tuple2.of(FunctionDeclarationKind.BV_EXTRACT, 1), (term, args, model, vars) -> { final Pattern pattern = Pattern.compile("extract ([0-9]+) ([0-9]+)"); final String termStr = term.toString(); final Matcher match = pattern.matcher(termStr); @@ -238,34 +240,32 @@ public JavaSMTTermTransformer(final JavaSMTSymbolTable symbolTable, SolverContex } throw new JavaSMTSolverException("Not supported: " + term); }); - environment.put(Tuple2.of("zero_extend", 1), (term, args, model, vars) -> { + environment.put(Tuple2.of(FunctionDeclarationKind.BV_ZERO_EXTENSION, 1), (term, args, model, vars) -> { BitvectorType type = (BitvectorType) context.getFormulaManager().getFormulaType((BitvectorFormula) term); final Expr op = (Expr) transform(args.get(0), model, vars); return BvZExtExpr.of(op, BvType.of(type.getSize())); }); - environment.put(Tuple2.of("sign_extend", 1), (term, args, model, vars) -> { + environment.put(Tuple2.of(FunctionDeclarationKind.BV_SIGN_EXTENSION, 1), (term, args, model, vars) -> { BitvectorType type = (BitvectorType) context.getFormulaManager().getFormulaType((BitvectorFormula) term); final Expr op = (Expr) transform(args.get(0), model, vars); return BvSExtExpr.of(op, BvType.of(type.getSize())); }); - environment.put(Tuple2.of("EqZero", 1), (term, args, model, vars) -> { + environment.put(Tuple2.of(FunctionDeclarationKind.EQ_ZERO, 1), (term, args, model, vars) -> { final Expr op = transform(args.get(0), model, vars); return Eq(op, TypeUtils.getDefaultValue(op.getType())); }); - environment.put(Tuple2.of("fp", 3), (term, args, model, vars) -> { - final Expr op1 = (Expr) transform(args.get(0), model, vars); - final Expr op2 = (Expr) transform(args.get(1), model, vars); - final Expr op3 = (Expr) transform(args.get(2), model, vars); - return FpLitExpr.of((BvLitExpr) op1, (BvLitExpr) op2, (BvLitExpr) op3); - }); - environment.put(Tuple2.of("const", 1), (term, args, model, vars) -> { - return transformLit(term, transform(args.get(0), model, vars)); - }); +// environment.put(Tuple2.of("fp", 3), (term, args, model, vars) -> { +// final Expr op1 = (Expr) transform(args.get(0), model, vars); +// final Expr op2 = (Expr) transform(args.get(1), model, vars); +// final Expr op3 = (Expr) transform(args.get(2), model, vars); +// return FpLitExpr.of((BvLitExpr) op1, (BvLitExpr) op2, (BvLitExpr) op3); +// }); +// environment.put(Tuple2.of("const", 1), (term, args, model, vars) -> transformLit(term, transform(args.get(0), model, vars))); } - private void addFunc(String name, Tuple2, Model, List>, Expr>> func) { - checkArgument(!environment.containsKey(Tuple2.of(name, func.get1())), "Duplicate key: " + Tuple2.of(name, func.get1())); - environment.put(Tuple2.of(name, func.get1()), func.get2()); + private void addFunc(FunctionDeclarationKind declarationKind, Tuple2, Model, List>, Expr>> func) { + checkArgument(!environment.containsKey(Tuple2.of(declarationKind, func.get1())), "Duplicate key: " + Tuple2.of(declarationKind, func.get1())); + environment.put(Tuple2.of(declarationKind, func.get1()), func.get2()); } public Expr toExpr(final Formula term) { @@ -278,7 +278,7 @@ private Expr transform(final Formula term, final Model model, final List> vars) { try { - return context.getFormulaManager().visit(term, new FormulaVisitor>() { + return context.getFormulaManager().visit(term, new FormulaVisitor<>() { @Override public Expr visitFreeVariable(Formula f, String name) { return transformVar(f, name, vars); @@ -382,8 +382,8 @@ private Expr transformApp(Formula f, final FunctionDeclaration funcDecl, final Model model, final List> vars) { - final var key1 = Tuple2.of(funcDecl.getName(), args.size()); - final var key2 = Tuple2.of(funcDecl.getName(), -1); + final var key1 = Tuple2.of(funcDecl.getKind(), args.size()); + final var key2 = Tuple2.of(funcDecl.getKind(), -1); if (environment.containsKey(key1)) { return environment.get(key1).apply(f, args, model, vars); } else if (environment.containsKey(key2)) {