diff --git a/.appveyor.yml b/.appveyor.yml index 797eb36576..d5be0d5474 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -77,6 +77,10 @@ on_finish: echo "Compressing and uploading JUnit HTML report..." 7z a JUnit.html.zip JUnit.html Push-AppveyorArtifact JUnit.html.zip -DeploymentName "JUnit Report" + - ps: | + echo "Compressing and uploading trace files..." + 7z a traces.zip .\traces + Push-AppveyorArtifact traces.zip -DeploymentName "Traces" cache: - C:\ant diff --git a/.gitignore b/.gitignore index fe24e6c4b0..b8294fa20b 100644 --- a/.gitignore +++ b/.gitignore @@ -61,6 +61,8 @@ solvers_maven_conf/*.asc /Javadoc /Javadoc-z3 /gh-pages +/traces +/scripts/solver.log .idea/ diff --git a/build/gitlab-ci.yml b/build/gitlab-ci.yml index dbfee377d4..fb11798dec 100644 --- a/build/gitlab-ci.yml +++ b/build/gitlab-ci.yml @@ -132,6 +132,7 @@ spotbugs: - "JUnit.html" - "JUnit-coverage/" - "junit/coverage.xml" + - "traces/" when: always reports: junit: "junit/TESTS-TestSuites.xml" @@ -143,6 +144,7 @@ spotbugs: artifacts: paths: - "JUnit.html" # no coverage files available + - "traces/" unit-tests:x86_64:jdk-11: extends: .unit-tests diff --git a/scripts/requirements.txt b/scripts/requirements.txt new file mode 100644 index 0000000000..f3addd0514 --- /dev/null +++ b/scripts/requirements.txt @@ -0,0 +1,9 @@ +# This file is part of JavaSMT, +# an API wrapper for a collection of SMT solvers: +# https://github.com/sosy-lab/java-smt +# +# SPDX-FileCopyrightText: 2025 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +parsy~=2.2 diff --git a/scripts/traceToSmtlib.py b/scripts/traceToSmtlib.py new file mode 100755 index 0000000000..a2b79dfb65 --- /dev/null +++ b/scripts/traceToSmtlib.py @@ -0,0 +1,1518 @@ +#!/usr/bin/env python3 + +# This file is part of JavaSMT, +# an API wrapper for a collection of SMT solvers: +# https://github.com/sosy-lab/java-smt +# +# SPDX-FileCopyrightText: 2025 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +import argparse +import math +import sys +from dataclasses import dataclass +from enum import Enum +from fractions import Fraction +from pathlib import Path +from typing import List, Optional + +from parsy import regex, string, whitespace, eof, generate, alt, forward_declaration, from_enum + + +@dataclass +class Type: + def toSmtlib(self): + "Print type in SMTLIB format" + raise NotImplementedError() + + +@dataclass +class BooleanType(Type): + def toSmtlib(self): + return "Bool" + + +@dataclass +class IntegerType(Type): + def toSmtlib(self): + return "Int" + + +@dataclass +class RationalType(Type): + def toSmtlib(self): + return "Real" + + +@dataclass +class StringType(Type): + def toSmtlib(self): + return "String" + + +@dataclass +class BitvectorType(Type): + width: int + + def toSmtlib(self): + return f"(_ BitVec {self.width})" + + +@dataclass +class FloatType(Type): + exponent: int + significand: int + + def toSmtlib(self): + return f"(_ FloatingPoint {self.exponent} {self.significand})" + + +@dataclass +class ArrayType(Type): + index: Type + element: Type + + def toSmtlib(self): + return f"(Array {self.index.toSmtlib()} {self.element.toSmtlib()})" + + +@dataclass +class FunctionType(Type): + arguments: List[Type] + value: Type + + def toSmtlib(self): + return f"({' '.join([arg.toSmtlib() for arg in self.arguments])}) {self.value.toSmtlib()}" + + +# TODO Simplify grammar and make sure it matches the parser rules +""" +Grammar: + +program ::= line+ +line ::= ws* (definition | statement) ";\n" +definition ::= "var" ws* variable ws* "=" ws* statement +statement ::= variable ("." variable "(" ws* args ws* ")")+ +args ::= arg ws* ("," ws* arg)* +arg ::= variable | boolean | integer | float | string + +boolean ::= "true" | "false" +integer ::= -?[0-9]+L? | "new" ws* "BigInteger(\"" -?[0-9]+ "\")" +float ::= ... +string ::= "\"" .* "\"" +""" + +argument = forward_declaration() + +# Boolean constants +litBool = string("true").map(lambda str: True) | string("false").map(lambda str: False) + + +def test_bool(): + assert litBool.parse('true') == True + assert litBool.parse('false') == False + + +litNumeral = regex(r'0|-?[1-9][0-9]*').map(int) + + +@generate +def litDecimal(): + sign = yield string('-').optional() + integer = yield regex(r'0|[1-9][0-9]*') + yield string(".") + fraction = yield regex(r'[0-9]*') + shift = len(fraction) + num = int(integer) * 10 ** shift + int(fraction) + den = 10 ** shift + return Fraction(num if sign is None else -num, den) + + +@generate +def litFpConstant(): + sign = yield string('-').optional("") + integerPart = yield regex(r'[0-9]+') + yield string('.') + fractionPart = yield regex(r'[0-9]+') + exponentPart = "0" + hasExponent = yield string('E').optional() + if hasExponent is not None: + exponentPart = yield regex(r'-?[0-9]+') + return float(sign + integerPart + '.' + fractionPart + "e" + exponentPart) + + +# Integer constants +litInt = litNumeral << string("L").optional() + +# Double constants +litFloat = string("Double.NaN").map(lambda str: float('nan')) | \ + string("Double.POSITIVE_INFINITY").map(lambda str: float('inf')) | \ + string("Double.NEGATIVE_INFINITY").map(lambda str: float('-inf')) | \ + litFpConstant + + +# BigInteger constants +@generate +def litBigInteger(): + yield string('new') >> whitespace >> string('BigInteger(') >> whitespace.optional() + yield string('"') + integer = yield litNumeral + yield string('"') + yield whitespace.optional() << string(')') + return integer + + +# BigDecimal constants +@generate +def litBigDecimal(): + yield string('new') >> whitespace >> (string('BigDecimal(')) >> whitespace.optional() + yield string('"') + number = yield (litDecimal | litNumeral) + yield string('"') + yield whitespace.optional() << string(')') + return number + + +# Rational constants +@generate +def litRational(): + yield string('Rational.of("') + num = yield regex(r'-?[0-9]+').map(int) + isFraction = yield string("/").optional() + den = 1 + if isFraction is not None: + den = yield regex(r'[0-9]+').map(int) + yield string('")') + return Fraction(num, den) + + +litNumber = litBigInteger | litBigDecimal | litRational | litFloat | litInt + + +def test_number(): + assert litNumber.parse('123') == 123 + assert litNumber.parse('-123') == -123 + assert litNumber.parse('123L') == 123 + assert litNumber.parse('0.0') == 0.0 + assert litNumber.parse('1.23') == 1.23 + assert litNumber.parse('-1.23') == -1.23 + assert litNumber.parse('12.3E1') == 123.0 + assert litNumber.parse('12.3E-1') == 1.23 + assert litNumber.parse('Double.NEGATIVE_INFINITY') == float('-inf') + assert litNumber.parse('new BigInteger("123")') == 123 + assert litNumber.parse('new BigDecimal("123")') == Fraction(123) + assert litNumber.parse('new BigDecimal("123.4")') == Fraction(1234, 10) + assert litNumber.parse('new BigDecimal("0.0625")') == Fraction(625, 10000) + assert litNumber.parse('Rational.of("4")') == Fraction(4) + assert litNumber.parse('Rational.of("1/4")') == Fraction(1, 4) + + +# String constants +@generate +def litString(): + yield string('"') + lit = yield regex(r'(\\"|\\\'|\\n|\\\\|[^"])*') + yield string('"') + return lit.replace('\\"', '"').replace('\\\'', '\'').replace('\\n', '\n').replace('\\\\', '\\') + + +def test_string(): + assert litString.parse('"str"') == 'str' + assert litString.parse('"\\""') == '"' + assert litString.parse('"\\\\"') == '\\' + assert litString.parse('"\\\'"') == '\'' + assert litString.parse('"\\n"') == '\n' + + +class RoundingMode(Enum): + NEAREST_TIES_TO_EVEN = "FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN" + NEAREST_TIES_AWAY = "FloatingPointRoundingMode.NEAREST_TIES_AWAY" + TOWARD_POSITIVE = "FloatingPointRoundingMode.TOWARD_POSITIVE" + TOWARD_NEGATIVE = "FloatingPointRoundingMode.TOWARD_NEGATIVE" + TOWARD_ZERO = "FloatingPointRoundingMode.TOWARD_ZERO" + + def toSmtlib(self): + if self == RoundingMode.NEAREST_TIES_TO_EVEN: + return "RNE" + elif self == RoundingMode.NEAREST_TIES_AWAY: + return "RNA" + elif self == RoundingMode.TOWARD_POSITIVE: + return "RTP" + elif self == RoundingMode.TOWARD_NEGATIVE: + return "RTN" + elif self == RoundingMode.TOWARD_ZERO: + return "RTZ" + else: + raise Exception("Unknown rounding mode") + + +litRoundingMode = from_enum(RoundingMode) + + +class Sign(Enum): + POSITIVE = "FloatingPointNumber.Sign.POSITIVE" + NEGATIVE = "FloatingPointNumber.Sign.NEGATIVE" + + +litSign = from_enum(Sign) + +litType = forward_declaration() + +litBoolType = string("FormulaType.BooleanType").map(lambda str: BooleanType()) +litIntegerType = string("FormulaType.IntegerType").map(lambda str: IntegerType()) +litRationalType = string("FormulaType.RationalType").map(lambda str: RationalType()) +litStringType = string("FormulaType.StringType").map(lambda str: StringType()) + + +@generate +def litBitvectorType(): + yield string("FormulaType.getBitvectorTypeWithSize(") >> whitespace.optional() + width = yield regex(r'[0-9]+').map(int) + yield whitespace.optional() << string(")") + return BitvectorType(width) + + +@generate +def litFloatType(): + yield string("FormulaType.getFloatingPointType(") >> whitespace.optional() + exponent = yield regex(r'[0-9]+').map(int) + yield whitespace.optional() << string(",") << whitespace.optional() + significand = yield regex(r'[0-9]+').map(int) + yield whitespace.optional() << string(")") + return FloatType(exponent, 1 + significand) + + +@generate +def litArrayType(): + yield string("FormulaType.getArrayType(") + yield whitespace.optional() + index = yield litType + yield whitespace.optional() >> string(",") >> whitespace.optional() + elements = yield litType + yield whitespace.optional() >> string(")") + return ArrayType(index, elements) + + +litType.become( + alt(litBoolType, litIntegerType, litRationalType, litStringType, litBitvectorType, litFloatType, litArrayType)) + + +def test_sort(): + assert litType.parse("FormulaType.BooleanType") == BooleanType() + assert litType.parse("FormulaType.IntegerType") == IntegerType() + assert litType.parse("FormulaType.getBitvectorTypeWithSize(8)") == BitvectorType(8) + assert (litType.parse("FormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType)") + == ArrayType(IntegerType(), IntegerType())) + + +class Solvers(Enum): + OPENSMT = "SolverContextFactory.Solvers.OPENSMT" + MATHSAT5 = "SolverContextFactory.Solvers.MATHSAT5" + SMTINTERPOL = "SolverContextFactory.Solvers.SMTINTERPOL" + Z3 = "SolverContextFactory.Solvers.Z3" + PRINCESS = "SolverContextFactory.Solvers.PRINCESS" + BOOLECTOR = "SolverContextFactory.Solvers.BOOLECTOR" + CVC4 = "SolverContextFactory.Solvers.CVC4" + CVC5 = "SolverContextFactory.Solvers.CVC5" + YICES2 = "SolverContextFactory.Solvers.OPENSMT" + BITWUZLA = "SolverContextFactory.Solvers.BITWUZLA" + + +litSolvers = from_enum(Solvers) + + +class ProverOptions(Enum): + GENERATE_MODELS = "SolverContext.ProverOptions.GENERATE_MODELS" + GENERATE_ALL_SAT = "SolverContext.ProverOptions.GENERATE_ALL_SAT" + GENERATE_UNSAT_CORE = "SolverContext.ProverOptions.GENERATE_UNSAT_CORE" + GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS = "SolverContext.ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS" + ENABLE_SEPARATION_LOGIC = "SolverContext.ProverOptions.ENABLE_SEPARATION_LOGIC" + + +litProverOptions = from_enum(ProverOptions) + + +def test_proverOptions(): + assert litProverOptions.parse("SolverContext.ProverOptions.GENERATE_MODELS") == ProverOptions.GENERATE_MODELS + + +class Quantifier(Enum): + FORALL = "QuantifiedFormulaManager.Quantifier.FORALL" + EXISTS = "QuantifiedFormulaManager.Quantifier.EXISTS" + + +litQuantifier = from_enum(Quantifier) + + +@generate +def litList(): + yield (string("List.of(") | string("ImmutableList.of(") | string("Set.of(")) + yield whitespace.optional() + arg0 = yield argument.optional().map(lambda p: [p] if p is not None else []) + args = [] + if (arg0 is not []): + args = yield (whitespace.optional() >> string(",") >> whitespace.optional() >> argument).many() + yield whitespace.optional() + yield string(")") + return arg0 + args + + +def test_list(): + assert litList.parse("List.of(1, 2, var)") == [1, 2, "var"] + assert litList.parse("ImmutableList.of()") == [] + assert litList.parse("List.of(ImmutableList.of(1,2), ImmutableList.of(3,7))") == [[1, 2], [3, 7]] + assert litList.parse("Set.of(1,2)") == [1, 2] + + +variable = regex(r"[A-Za-z][A-Za-z0-9]*") + + +def test_variable(): + assert variable.parse("var1") == "var1" + assert variable.parse("mgr") == "mgr" + + +argument.become(alt( + litBool, + litNumber, + litRoundingMode, + litSign, + litString, + litType, + litSolvers, + litProverOptions, + litQuantifier, + litList, + variable)) + + +@dataclass +class Call: + fn: str + args: Optional[List] = None + + +@generate +def call(): + yield string(".") + fn = yield variable + yield string("(") + yield whitespace.optional() + arg0 = yield argument.optional().map(lambda p: [p] if p is not None else []) + args = [] + if (arg0 is not []): + args = yield (whitespace.optional() >> string(",") >> whitespace.optional() >> argument).many() + yield whitespace.optional() + yield string(")") + return Call(fn, arg0 + args) + + +@generate +def stmt(): + call0 = yield variable.map(lambda str: Call(str)) + calls = yield call.many() + return [call0] + calls + + +def test_stmt(): + assert stmt.parse("var1.method(123, false)") == [Call("var1"), Call("method", [123, False])] + assert (stmt.parse('mgr.getBitvectorFormulaManager().makeBitvector(8, new BigInteger("0"))') + == [Call("mgr"), Call("getBitvectorFormulaManager", []), Call("makeBitvector", [8, 0])]) + + +@dataclass +class Definition: + variable: Optional[str] + value: List[Call] + + def getCalls(self): + "Project the call chain on the right to just the method names" + return [call.fn for call in self.value] + + +@generate +def definition(): + yield string("var") + yield whitespace.optional() + var = yield variable + yield whitespace.optional() + yield string("=") + yield whitespace.optional() + value = yield stmt + return Definition(var, value) + + +line = whitespace.optional() >> (definition | stmt.map(lambda p: Definition(None, p))) << string(";\n") + + +def test_line(): + assert (line.parse( + 'var var5 = mgr.getBitvectorFormulaManager().makeBitvector(8, new BigInteger("0"));\n') + == Definition("var5", + [Call( + "mgr"), + Call( + "getBitvectorFormulaManager", + []), + Call( + "makeBitvector", + [8, + 0])])) + + +program = line.many() << whitespace.optional() << eof + + +def test_program(): + assert (program.parse( + """ + var var5 = mgr.getBitvectorFormulaManager().makeBitvector(8, new BigInteger("0")); + var var6 = mgr.getBitvectorFormulaManager().extend(var5, 24, false); + var var8 = mgr.getBitvectorFormulaManager().equal(var6, var6); + var var9 = mgr.getBitvectorFormulaManager().makeBitvector(32, 1L); + var2.push(); + var var21 = var2.addConstraint(var8); + var var22 = var2.isUnsat(); + var var23 = var2.getModel(); + var23.close(); + """) + == [Definition("var5", + [Call("mgr"), Call("getBitvectorFormulaManager", []), Call("makeBitvector", [8, 0])]), + Definition("var6", + [Call("mgr"), Call("getBitvectorFormulaManager", []), Call("extend", ["var5", 24, False])]), + Definition("var8", + [Call("mgr"), Call("getBitvectorFormulaManager", []), Call("equal", ["var6", "var6"])]), + Definition("var9", + [Call("mgr"), Call("getBitvectorFormulaManager", []), Call("makeBitvector", [32, 1])]), + Definition(None, [Call("var2"), Call("push", [])]), + Definition("var21", [Call("var2"), Call("addConstraint", ["var8"])]), + Definition("var22", [Call("var2"), Call("isUnsat", [])]), + Definition("var23", [Call("var2"), Call("getModel", [])]), + Definition(None, [Call("var23"), Call("close", [])])]) + + +def test_toSmtlib(): + assert (ArrayType(IntegerType(), ArrayType(BitvectorType(32), FloatType(8, 24))).toSmtlib() + == "(Array Int (Array (_ BitVec 32) (_ FloatingPoint 8 24)))") + + +def printBitvector(width, value): + "Print a bitvector literal in SMTLIB format" + digits = format(value, f'0{width}b') + if value < 0: + # Convert to 2s complement + digits = ''.join(['0' if l == '1' else '1' for l in digits]) + digits = format(int(digits, 2) + 1, f'0{width}b') + return '#b' + digits + + +def test_printBitvector(): + assert printBitvector(8, 5) == "#b00000101" + assert printBitvector(8, -5) == "#b11111011" + + +def parseNumber(repr): + "Parse a String as a number" + value = None + try: + value = int(repr) + except Exception: + pass + if value is not None: + return value + try: + value = Fraction(repr) + except Exception: + pass + if value is not None: + return value + try: + value = float(repr) + except Exception: + pass + if value is not None: + return value + else: + raise Exception(f'Could not parse "{repr}" as a number') + + +def flattenProvers(prog: List[Definition]): + "Push all assertions onto the same global prover" + # We assume that the provers are not used "in parallel" + # FIXME Reorder the instructions to avoid overlapping prover instances + active = "" + levels = 0 + trace = [] + for stmt in prog: + if (stmt.getCalls()[-1] == "newProverEnvironment" + or stmt.getCalls()[-1] == "newProverEnvironmentWithInterpolation"): + if levels > 0: + raise Exception("Can't open new prover before closing the last instance") + active = stmt.variable + levels = 1 + trace.append(Definition(None, [Call(active), Call("push", [])])) + elif stmt.getCalls()[-1] == "push": + levels += 1 + trace.append(stmt) + elif stmt.getCalls()[-1] == "pop": + levels -= 1 + trace.append(stmt) + elif stmt.getCalls() == [active, "close"]: + trace.extend([Definition(None, [Call(active), Call("pop", [])])] * levels) + levels = 0 + else: + trace.append(stmt) + return trace + + +@dataclass +class Expr: + fn: str + args: Optional[List] + + def toSmtlib(self): + if self.args == None or self.args == []: + return self.fn + else: + return f'({self.fn} {' '.join([arg.toSmtlib() for arg in self.args])})' + + +@dataclass +class Def: + symbol: str + sort: Type + value: Optional[Expr] + + def toSmtlib(self): + if self.value == None: + if isinstance(self.sort, FunctionType): + return f'(declare-fun {self.symbol} {self.sort.toSmtlib()})' + else: + return f'(declare-const {self.symbol} {self.sort.toSmtlib()})' + else: + return f'(define-fun {self.symbol} () {self.sort.toSmtlib()} {self.value.toSmtlib()})' + + +def const(value): + return Expr(value, []) + + +def var(name): + return Expr(str(name), None) + + +def app(fn, *args): + return Expr(fn, [p if isinstance(p, Expr) else var(p) for p in args]) + + +def toIntSmtlib(value): + "Print integer value as smtlib" + if isinstance(value, str): + return toIntSmtlib(parseNumber(value)) + if isinstance(value, float) and not math.isnan(value) and not math.isinf(value): + return toIntSmtlib(Fraction(value)) + if isinstance(value, int): + if value < 0: + return app('-', toIntSmtlib(-value)) + else: + return const(str(value)) + if isinstance(value, Fraction): + return app('div', toIntSmtlib(value.numerator), toIntSmtlib(value.numerator)) + else: + raise Exception(f'Can\'t convert "{value}" to Integer') + + +def toRealSmtlib(value): + "Print real value as smtlib" + if isinstance(value, str): + return toRealSmtlib(parseNumber(value)) + elif isinstance(value, int): + return toRealSmtlib(Fraction(value)) + elif isinstance(value, float): + return toRealSmtlib(Fraction.from_float(value)) + elif isinstance(value, Fraction): + return app('/', toIntSmtlib(value.numerator), toIntSmtlib(value.denominator)) + else: + raise Exception(f'Can\'t convert "{value}" to Real') + + +def toFpSmtlib(rm, fpType, value): + "Print float value as smtlib" + if isinstance(value, str): + return toFpSmtlib(rm, fpType, parseNumber(value)) + elif value == float('-inf'): + return const(f'(_ -oo {fpType.exponent} {fpType.significand})') + elif value == float('+inf'): + return const(f'(_ +oo {fpType.exponent} {fpType.significand})') + elif isinstance(value, float) and math.isnan(value): + return const(f'(_ NaN {fpType.exponent} {fpType.significand})') + else: + return app(f'(_ to_fp {fpType.exponent} {fpType.significand})', const(rm.toSmtlib()), toRealSmtlib(value)) + + +def translate(prog: List[Definition]): + "Convert a JavaSMT trace to a SMTLIB2 script" + # TODO Print error location + # TODO Use actual variable names in declarations + sortMap = {} + nameMap = {} # Stores UF names for function declarations + output: List[Def | Expr] = \ + [app('set-logic', const('ALL')), + app('set-option', const(':interactive-mode'), const('true')), + app('set-option', const(':produce-models'), const('true')), + app('set-option', const(':global-declarations'), const('true')) + ] + solver = prog[3].value[1].args[3] # Get solver name from createSolverContext call in the preamble + for stmt in prog[5:]: + def matchType(param, arg): + "Convert argument to match the given type" + if param == IntegerType() and sortMap[arg] == RationalType(): + return app('to_int', arg) + elif param == RationalType() and sortMap[arg] == IntegerType(): + return app('to_real', arg) + else: + return var(arg) + + if stmt.getCalls()[:-1] == ["mgr", "getBitvectorFormulaManager"]: + if stmt.getCalls()[-1] == "add": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvadd', arg1, arg2))) + + elif stmt.getCalls()[-1] == "and": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvand', arg1, arg2))) + + elif stmt.getCalls()[-1] == "concat": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BitvectorType(sortMap[arg1].width + sortMap[arg2].width) + output.append(Def(stmt.variable, sortMap[stmt.variable], app('concat', arg1, arg2))) + + elif stmt.getCalls()[-1] == "distinct": + args = stmt.value[-1].args[0] + sortMap[stmt.variable] = BooleanType() + if len(args) < 2: + output.append(Def(stmt.variable, sortMap[stmt.variable], const('true'))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('distinct', *args))) + + elif stmt.getCalls()[-1] == "divide": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = sortMap[arg1] + if arg3: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvsdiv', arg1, arg2))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvudiv', arg1, arg2))) + + elif stmt.getCalls()[-1] == "equal": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('=', arg1, arg2))) + + elif stmt.getCalls()[-1] == "extend": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = BitvectorType(sortMap[arg1].width + arg2) + if arg3: + output.append(Def(stmt.variable, sortMap[stmt.variable], app(f'(_ sign_extend {arg2})', arg1))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app(f'(_ zero_extend {arg2})', arg1))) + + elif stmt.getCalls()[-1] == "extract": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = BitvectorType(arg2 - arg3 + 1) + output.append(Def(stmt.variable, sortMap[stmt.variable], app(f'(_ extract {arg2} {arg3})', arg1))) + + elif stmt.getCalls()[-1] == "greaterOrEquals": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = BooleanType() + if arg3: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvsge', arg1, arg2))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvuge', arg1, arg2))) + + elif stmt.getCalls()[-1] == "greaterThan": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = BooleanType() + if arg3: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvsgt', arg1, arg2))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvugt', arg1, arg2))) + + elif stmt.getCalls()[-1] == "lessOrEquals": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = BooleanType() + if arg3: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvsle', arg1, arg2))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvule', arg1, arg2))) + + elif stmt.getCalls()[-1] == "lessThan": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = BooleanType() + if arg3: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvslt', arg1, arg2))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvult', arg1, arg2))) + + elif stmt.getCalls()[-1] == "makeBitvector": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BitvectorType(arg1) + if arg2 is int: + # Create bv constant + output.append(Def(stmt.variable, sortMap[stmt.variable], const(printBitvector(arg1, arg2)))) + else: + # Convert integer formula to bv formula + operation = "to_bv" if solver == Solvers.MATHSAT5 else "int_to_bv" + output.append(Def(stmt.variable, sortMap[stmt.variable], app(f'(_ {operation} {arg1})', arg2))) + + elif stmt.getCalls()[-1] == "makeVariable": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + if '|' in arg2: + continue # Skip illegal names + sortMap[stmt.variable] = arg1 + output.append(Def(stmt.variable, sortMap[stmt.variable], None)) + + elif stmt.getCalls()[-1] == "multiply": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvmul', arg1, arg2))) + + elif stmt.getCalls()[-1] == "negate": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvneg', arg1))) + + elif stmt.getCalls()[-1] == "not": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvnot', arg1))) + + elif stmt.getCalls()[-1] == "or": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvor', arg1, arg2))) + + elif stmt.getCalls()[-1] == "remainder": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = sortMap[arg1] + if arg3: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvsrem', arg1, arg2))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvurem', arg1, arg2))) + + elif stmt.getCalls()[-1] == "rotateLeft": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + if not isinstance(arg2, int): + raise Exception("rotateLeft is only supported for constant rotations") + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app(f'(_ rotate_left {arg2})', arg1))) + + elif stmt.getCalls()[-1] == "rotateRight": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + if not isinstance(arg2, int): + raise Exception("rotateRight is only supported for constant rotations") + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app(f'(_ rotate_right {arg2})', arg1))) + + elif stmt.getCalls()[-1] == "shiftLeft": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvshl', arg1, arg2))) + + elif stmt.getCalls()[-1] == "shiftRight": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = sortMap[arg1] + if arg3: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvashr', arg1, arg2))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvlshr', arg1, arg2))) + + elif stmt.getCalls()[-1] == "smodulo": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvsmod', arg1, arg2))) + + elif stmt.getCalls()[-1] == "subtract": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvsub', arg1, arg2))) + + elif stmt.getCalls()[-1] == "toIntegerFormula": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = IntegerType() + if arg2: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('sbv_to_int', arg1))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('ubv_to_int', arg1))) + + elif stmt.getCalls()[-1] == "xor": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('bvxor', arg1, arg2))) + + else: + raise Exception(f'Unsupported call: {stmt.getCalls()}') + + elif stmt.getCalls()[:-1] == ["mgr", "getBooleanFormulaManager"]: + if stmt.getCalls()[-1] == "and": + args = stmt.value[-1].args + sortMap[stmt.variable] = BooleanType() + if len(args) == 0: + output.append(Def(stmt.variable, sortMap[stmt.variable], const('true'))) + elif len(args) == 1: + output.append(Def(stmt.variable, sortMap[stmt.variable], var(args[0]))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('and', *args))) + + elif stmt.getCalls()[-1] == "equivalence": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('=', arg1, arg2))) + + elif stmt.getCalls()[-1] == "ifThenElse": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = sortMap[arg2] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('ite', arg1, arg2, arg3))) + + elif stmt.getCalls()[-1] == "implication": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('=>', arg1, arg2))) + + elif stmt.getCalls()[-1] == "makeFalse": + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], const('false'))) + + elif stmt.getCalls()[-1] == "makeTrue": + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], const('true'))) + + elif stmt.getCalls()[-1] == "makeBoolean": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = BooleanType() + if arg1: + output.append(Def(stmt.variable, sortMap[stmt.variable], const('true'))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], const('false'))) + + elif stmt.getCalls()[-1] == "makeVariable": + arg1 = stmt.value[-1].args[0] + if '|' in arg1: + continue # Skip illegal names + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], None)) + + elif stmt.getCalls()[-1] == "not": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('not', arg1))) + + elif stmt.getCalls()[-1] == "or": + args = stmt.value[-1].args + sortMap[stmt.variable] = BooleanType() + if len(args) == 0: + output.append(Def(stmt.variable, sortMap[stmt.variable], const('false'))) + elif len(args) == 1: + output.append(Def(stmt.variable, sortMap[stmt.variable], var(args[0]))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('or', *args))) + + elif stmt.getCalls()[-1] == "xor": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('xor', arg1, arg2))) + + else: + raise Exception(f'Unsupported call: {stmt.getCalls()}') + + elif stmt.getCalls()[1] == "getIntegerFormulaManager" or stmt.getCalls()[1] == "getRationalFormulaManager": + theoryType = IntegerType() if "Integer" in stmt.getCalls()[1] else RationalType() + + def conv(arg): + "Convert argument to match the type of the parameter" + return matchType(theoryType, arg) + + if stmt.getCalls()[-1] == "add": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = theoryType + output.append(Def(stmt.variable, sortMap[stmt.variable], app('+', conv(arg1), conv(arg2)))) + + elif stmt.getCalls()[-1] == "distinct": + args = stmt.value[-1].args + sortMap[stmt.variable] = BooleanType() + if len(args) < 2: + output.append(Def(stmt.variable, sortMap[stmt.variable], const('true'))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('distinct', *[conv(p) for p in args]))) + + elif stmt.getCalls()[-1] == "divide": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = theoryType + if theoryType == IntegerType(): + output.append(Def(stmt.variable, sortMap[stmt.variable], app('div', conv(arg1), conv(arg2)))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('/', conv(arg1), conv(arg2)))) + + elif stmt.getCalls()[-1] == "equal": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('=', conv(arg1), conv(arg2)))) + + elif stmt.getCalls()[-1] == "floor": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = IntegerType() + output.append(Def(stmt.variable, sortMap[stmt.variable], matchType(IntegerType(), arg1))) + + elif stmt.getCalls()[-1] == "greaterOrEquals": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('>=', conv(arg1), conv(arg2)))) + + elif stmt.getCalls()[-1] == "greaterThan": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('>', conv(arg1), conv(arg2)))) + + elif stmt.getCalls()[-1] == "lessOrEquals": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('<=', conv(arg1), conv(arg2)))) + + elif stmt.getCalls()[-1] == "lessThan": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('<', conv(arg1), conv(arg2)))) + + elif stmt.getCalls()[-1] == "makeNumber": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = theoryType + if theoryType == IntegerType(): + output.append(Def(stmt.variable, sortMap[stmt.variable], toIntSmtlib(arg1))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], toRealSmtlib(arg1))) + + elif stmt.getCalls()[-1] == "makeVariable": + arg1 = stmt.value[-1].args[0] + if '|' in arg1: + continue # Skip illegal names + sortMap[stmt.variable] = theoryType + output.append(Def(stmt.variable, sortMap[stmt.variable], None)) + + elif stmt.getCalls() == ["mgr", "getIntegerFormulaManager", "modularCongruence"]: + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], + app('=', app('mod', app('-', arg1, arg2), toIntSmtlib(arg3)), + toIntSmtlib(0)))) + + elif stmt.getCalls() == ["mgr", "getIntegerFormulaManager", "modulo"]: + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = IntegerType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('mod', arg1, arg2))) + + elif stmt.getCalls()[-1] == "multiply": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = theoryType + output.append(Def(stmt.variable, sortMap[stmt.variable], app('*', conv(arg1), conv(arg2)))) + + elif stmt.getCalls()[-1] == "negate": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = theoryType + output.append(Def(stmt.variable, sortMap[stmt.variable], app('-', conv(arg1)))) + + elif stmt.getCalls()[-1] == "subtract": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = theoryType + output.append(Def(stmt.variable, sortMap[stmt.variable], app('-', conv(arg1), conv(arg2)))) + + elif stmt.getCalls()[-1] == "sum": + args = stmt.value[-1].args + sortMap[stmt.variable] = theoryType + if len(args) == 0: + output.append(Def(stmt.variable, sortMap[stmt.variable], + const('0') if theoryType == IntegerType() else const('0.0'))) + elif len(args) == 1: + output.append(Def(stmt.variable, sortMap[stmt.variable], conv(args[0]))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app('+', *[conv(p) for p in args]))) + + else: + raise Exception(f'Unsupported call: {stmt.getCalls()}') + + elif stmt.getCalls()[:-1] == ["mgr", "getFloatingPointFormulaManager"]: + if stmt.getCalls()[-1] == "abs": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('fp.abs', arg1))) + + elif stmt.getCalls()[-1] == "add": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = sortMap[arg1] + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.add', const(arg3.toSmtlib()), arg1, arg2))) + + elif stmt.getCalls()[-1] == "assignment": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('=', arg1, arg2))) + + elif stmt.getCalls()[-1] == "castTo": + # Converts from float to bv/int, or convert between different fp precisions + arg1 = stmt.value[-1].args[0] # source (fp term) + arg2 = stmt.value[-1].args[1] # signed? + arg3 = stmt.value[-1].args[2] # target type (any type) + arg4 = stmt.value[-1].args[3] # rounding mode + sortMap[stmt.variable] = arg3 + if isinstance(arg3, FloatType): + output.append(Def(stmt.variable, sortMap[stmt.variable], + app(f'(_ to_fp {arg3.exponent} {arg3.significand})', const(arg4.toSmtlib()), + arg1))) + elif isinstance(arg3, IntegerType): + raise Exception("Converting from float to integer is not supported in SMTLIB") + elif isinstance(arg3, RationalType): + output.append(Def(stmt.variable, sortMap[stmt.variable], app('fp.to_real', arg1))) + elif isinstance(arg3, BitvectorType): + if arg2: + output.append(Def(stmt.variable, sortMap[stmt.variable], + app(f'(_ fp.to_sbv {arg3.width})', const(arg4.toSmtlib()), arg1))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], + app(f'(_ fp.to_ubv {arg3.width})', const(arg4.toSmtlib()), arg1))) + else: + raise Exception(f"Illegal cast from float to {arg3}") + + elif stmt.getCalls()[-1] == "castFrom": + # Converts from bv/int to float, or convert between different fp precisions + arg1 = stmt.value[-1].args[0] # source (any term) + arg2 = stmt.value[-1].args[1] # signed? + arg3 = stmt.value[-1].args[2] # target type (fp type) + arg4 = stmt.value[-1].args[3] # rounding mode + sortMap[stmt.variable] = arg3 + sourceType = sortMap[arg1] + if isinstance(sourceType, FloatType): + output.append(Def(stmt.variable, sortMap[stmt.variable], + app(f'(_ to_fp {arg3.exponent} {arg3.significand})', const(arg4.toSmtlib()), + arg1))) + elif isinstance(sourceType, IntegerType): + raise Exception("Converting from float to integer is not supported in SMTLIB") + elif isinstance(sourceType, RationalType): + output.append(Def(stmt.variable, sortMap[stmt.variable], + app(f'(_ to_fp {arg3.exponent} {arg3.significand})', const(arg4.toSmtlib()), + arg1))) + elif isinstance(sourceType, BitvectorType): + if arg2: + output.append(Def(stmt.variable, sortMap[stmt.variable], + app(f'(_ to_fp {arg3.exponent} {arg3.significand})', const(arg4.toSmtlib()), + arg1))) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], + app(f'(_ to_fp_unsigned {arg3.exponent} {arg3.significand})', + const(arg4.toSmtlib()), + arg1))) + else: + raise Exception(f"Illegal cast from {sourceType} to float") + + elif stmt.getCalls()[-1] == "divide": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = sortMap[arg1] + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.div', const(arg3.toSmtlib()), arg1, arg2))) + + elif stmt.getCalls()[-1] == "equalWithFPSemantics": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.eq', arg1, arg2))) + + elif stmt.getCalls()[-1] == "fromIeeeBitvector": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = arg2 + output.append( + Def(stmt.variable, sortMap[stmt.variable], + app(f'(_ to_fp {arg2.exponent} {arg2.significand})', arg1))) + + elif stmt.getCalls()[-1] == "greaterOrEquals": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.geq', arg1, arg2))) + + elif stmt.getCalls()[-1] == "greaterThan": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.gt', arg1, arg2))) + + elif stmt.getCalls()[-1] == "isInfinity": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = BooleanType() + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.isInfinite', arg1))) + + elif stmt.getCalls()[-1] == "isNaN": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = BooleanType() + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.isNaN', arg1))) + + elif stmt.getCalls()[-1] == "isNegative": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = BooleanType() + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.isNegative', arg1))) + + elif stmt.getCalls()[-1] == "isNormal": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = BooleanType() + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.isNormal', arg1))) + + elif stmt.getCalls()[-1] == "isSubnormal": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = BooleanType() + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.isSubnormal', arg1))) + + elif stmt.getCalls()[-1] == "isZero": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = BooleanType() + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.isZero', arg1))) + + elif stmt.getCalls()[-1] == "lessOrEquals": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('fp.leq', arg1, arg2))) + + elif stmt.getCalls()[-1] == "lessThan": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('fp.lt', arg1, arg2))) + + elif stmt.getCalls()[-1] == "makeMinusInfinity": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = arg1 + output.append( + Def(stmt.variable, sortMap[stmt.variable], const(f'(_ -oo {arg1.exponent} {arg1.significand})'))) + + elif stmt.getCalls()[-1] == "makeNaN": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = arg1 + output.append( + Def(stmt.variable, sortMap[stmt.variable], const(f'(_ NaN {arg1.exponent} {arg1.significand})'))) + + elif stmt.getCalls()[-1] == "makeNumber": + args = stmt.value[-1].args + if (len(args) == 3 + and (isinstance(args[0], float | int | Fraction | str)) + and isinstance(args[1], Type) + and isinstance(args[2], RoundingMode)): + rm = RoundingMode.NEAREST_TIES_TO_EVEN if len(args) == 2 else args[2] + sortMap[stmt.variable] = args[1] + output.append(Def(stmt.variable, sortMap[stmt.variable], toFpSmtlib(rm, args[1], args[0]))) + elif (len(args) == 4 + and isinstance(args[0], int) + and isinstance(args[1], int) + and isinstance(args[2], Sign) + and isinstance(args[3], FloatType)): + sortMap[stmt.variable] = args[3] + output.append(Def(stmt.variable, sortMap[stmt.variable], + app('fp', '#b1' if args[2] == Sign.NEGATIVE else '#b0', + printBitvector(args[3].exponent, args[0]), + printBitvector(args[3].significand - 1, args[1])))) + else: + raise Exception(f'Unsupported call: {stmt.getCalls()} ({type(args[0])} {args})') + + elif stmt.getCalls()[-1] == "makePlusInfinity": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = arg1 + output.append( + Def(stmt.variable, sortMap[stmt.variable], const(f'(_ +oo {arg1.exponent} {arg1.significand})'))) + + elif stmt.getCalls()[-1] == "makeRoundingMode": + pass + + elif stmt.getCalls()[-1] == "makeVariable": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + if '|' in arg1: + continue # Skip illegal names + sortMap[stmt.variable] = arg2 + output.append(Def(stmt.variable, sortMap[stmt.variable], None)) + + elif stmt.getCalls()[-1] == "max": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('fp.max', arg1, arg2))) + + elif stmt.getCalls()[-1] == "min": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('fp.min', arg1, arg2))) + + elif stmt.getCalls()[-1] == "multiply": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = sortMap[arg1] + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.mul', const(arg3.toSmtlib()), arg1, arg2))) + + elif stmt.getCalls()[-1] == "negate": + arg1 = stmt.value[-1].args[0] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('fp.neg', arg1))) + + elif stmt.getCalls()[-1] == "remainder": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('fp.rem', arg1, arg2))) + + elif stmt.getCalls()[-1] == "round": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.roundToIntegral', const(arg2.toSmtlib()), arg1))) + + elif stmt.getCalls()[-1] == "sqrt": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('fp.sqrt', const(arg2.toSmtlib()), arg1))) + + elif stmt.getCalls()[-1] == "subtract": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = sortMap[arg1] + output.append( + Def(stmt.variable, sortMap[stmt.variable], app('fp.sub', const(arg3.toSmtlib()), arg1, arg2))) + + elif stmt.getCalls()[-1] == "toIeeeBitvector": + raise Exception("Extracting the bits of a floating-point value is not supported in SMTLIB") + + else: + raise Exception(f'Unsupported call: {stmt.getCalls()}') + + elif stmt.getCalls()[:-1] == ["mgr", "getArrayFormulaManager"]: + if stmt.getCalls()[-1] == "equivalence": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = BooleanType() + output.append(Def(stmt.variable, sortMap[stmt.variable], app('=', arg1, arg2))) + + elif stmt.getCalls()[-1] == "makeArray": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + if isinstance(arg1, Type) and isinstance(arg2, Type): + # Build a const array + sortMap[stmt.variable] = ArrayType(arg1, arg2) + output.append(Def(stmt.variable, sortMap[stmt.variable], + app(f'(as const {sortMap[stmt.variable].toSmtlib()})', arg3))) + else: + # Declare a new variable + sortMap[stmt.variable] = ArrayType(arg2, arg3) + output.append(Def(stmt.variable, sortMap[stmt.variable], None)) + + elif stmt.getCalls()[-1] == "select": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + sortMap[stmt.variable] = sortMap[arg1].element + output.append(Def(stmt.variable, sortMap[stmt.variable], app('select', arg1, arg2))) + + elif stmt.getCalls()[-1] == "store": + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + arg3 = stmt.value[-1].args[2] + sortMap[stmt.variable] = sortMap[arg1] + output.append(Def(stmt.variable, sortMap[stmt.variable], app('store', arg1, arg2, arg3))) + + else: + raise Exception(f'Unsupported call: {stmt.getCalls()}') + + elif stmt.getCalls()[:-1] == ["mgr", "getQuantifiedFormulaManager"]: + # TODO + raise Exception(f'Quantifiers are not supported yet') + + elif stmt.getCalls()[:-1] == ["mgr", "getStringFormulaManager"]: + # TODO + raise Exception(f'Strings are not supported yet') + + elif stmt.getCalls()[:-1] == ["mgr", "getEnumerationFormulaManager"]: + # TODO + raise Exception(f'Enumerations are not supported yet') + + elif stmt.getCalls()[:-1] == ["mgr", "getSLFormulaManager"]: + # TODO + raise Exception(f'Separation logic is not supported yet') + + elif stmt.getCalls()[:-1] == ["mgr", "getUFManager"]: + if stmt.getCalls()[-1] == "callUF": + arg0 = stmt.value[-1].args[0] + args = stmt.value[-1].args[1] + name = nameMap[arg0] + values = [matchType(param, arg) for param, arg in zip(sortMap[arg0].arguments, args)] + sortMap[stmt.variable] = sortMap[arg0].value + if args == []: + output.append(Def(stmt.variable, sortMap[stmt.variable], None)) + else: + output.append(Def(stmt.variable, sortMap[stmt.variable], app(name, *values))) + + elif stmt.getCalls()[-1] == "declareUF": + arg0 = stmt.value[-1].args[0] + arg1 = stmt.value[-1].args[1] + args = stmt.value[-1].args[2] + if '|' in arg0: + continue # Skip illegal names + sortMap[stmt.variable] = FunctionType(args, arg1) + nameMap[stmt.variable] = f'|{arg0}|' + if args != []: + output.append(Def(nameMap[stmt.variable], sortMap[stmt.variable], None)) + + else: + raise Exception(f'Unsupported call: {stmt.getCalls()}') + + elif stmt.getCalls()[-1] == "addConstraint": + arg1 = stmt.value[-1].args[0] + output.append(app('assert', arg1)) + + elif stmt.getCalls()[-1] == "asList": + pass + + elif stmt.getCalls()[-1] == "close": + pass + + elif stmt.getCalls()[-1] == "evaluate": + arg1 = stmt.value[-1].args[0] + output.append(app('get-value', app('', arg1))) + + elif stmt.getCalls()[-1] == "getModel": + output.append(const('(get-model)')) + + elif stmt.getCalls()[-1] == "isUnsat": + output.append(const('(check-sat)')) + + elif stmt.getCalls() == ["mgr", "makeVariable"]: + arg1 = stmt.value[-1].args[0] + arg2 = stmt.value[-1].args[1] + if '|' in arg2: + continue # Skip illegal names + sortMap[stmt.variable] = arg1 + output.append(Def(stmt.variable, sortMap[stmt.variable], None)) + + elif stmt.getCalls()[-1] == "newProverEnvironment": + # TODO Apply options at the top of the file + pass + + elif stmt.getCalls()[-1] == "newProverEnvironmentWithInterpolation": + # TODO Apply options at the top of the file + pass + + elif stmt.getCalls()[-1] == "pop": + output.append(app('pop', const('1'))) + + elif stmt.getCalls()[-1] == "push": + output.append(app('push', const('1'))) + + else: + raise Exception(f'Unsupported call: {stmt.getCalls()}') + + return output + + +def printSmtlib(program): + "Convert intermediate representation to String" + return '\n'.join([line.toSmtlib() for line in program]) + '\n' + + +if __name__ == '__main__': + options = argparse.ArgumentParser(description='Convert JavaSMT traces to SMTLIB files') + + options.add_argument('file', type=Path, help='Input file') + options.add_argument('--save', action='store_true', + help='Save the output in a *.smt2 file. The path to the file is the same as for the input, but with a different extension') + + args = options.parse_args() + + if not args.file.is_file(): + print(f'Could not find input file "{args.file}"') + exit(-1) + + # Translate the trace + try: + output = printSmtlib(translate(flattenProvers(program.parse("\n" + open(args.file).read())))) + except Exception as exception: + print(f'In {args.file}: {exception}') + exit(-1) + + out = open(args.file.with_suffix('.smt2'), 'w') if args.save else sys.stdout + out.write(output) + out.close() diff --git a/scripts/tracingTest.sh b/scripts/tracingTest.sh new file mode 100755 index 0000000000..175a438d0c --- /dev/null +++ b/scripts/tracingTest.sh @@ -0,0 +1,36 @@ +#!/usr/bin/env bash + +# This file is part of JavaSMT, +# an API wrapper for a collection of SMT solvers: +# https://github.com/sosy-lab/java-smt +# +# SPDX-FileCopyrightText: 2025 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +set -e + +if [[ $# -eq 0 ]]; then + echo "No command line for the solver" + echo "Usage: ./tracingTest.sh " + echo "Where is the full command for the solver, including any options that need to be passed" + exit 1 +fi + +cmd=$* + +echo "Initializing venv" +python3 -m venv .venv +source .venv/bin/activate + +pip install -r requirements.txt + +echo -e "\nConverting JavaTraces to Smtlib" +find ../traces -name *.java -exec ./traceToSmtlib.py --save {} ';' + +echo -e "\nRunning the solver on the generated Smtlib files" +find ../traces -name *.smt2 -exec echo "path: {}" ';' -exec timeout 20s $* {} ';' 2>&1 | tee solver.log | grep -E "error|path" + +echo -e "\n(See solver.log for the entire solver output)" + +deactivate diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java index 34c547ae28..cda52a0f09 100644 --- a/src/org/sosy_lab/java_smt/SolverContextFactory.java +++ b/src/org/sosy_lab/java_smt/SolverContextFactory.java @@ -30,6 +30,7 @@ import org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext; import org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext; import org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext; +import org.sosy_lab.java_smt.delegate.trace.TraceSolverContext; import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaSolverContext; import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext; import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext; @@ -95,6 +96,11 @@ public enum Solvers { @Option(secure = true, description = "Apply additional checks to catch common user errors.") private boolean useDebugMode = false; + @Option( + secure = true, + description = "Enable API tracing to record all calls to the JavaSMT library") + private boolean trace = false; + @Option( secure = true, description = "Counts all operations and interactions towards the SMT solver.") @@ -230,6 +236,9 @@ public SolverContext generateContext(Solvers solverToCreate) if (useDebugMode) { context = new DebuggingSolverContext(solverToCreate, config, context); } + if (trace) { + context = new TraceSolverContext(solverToCreate, config, context); + } if (collectStatistics) { // statistics need to be the most outer wrapping layer. context = new StatisticsSolverContext(context); diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index 02f1b7281f..8eef4d99ad 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -298,6 +298,8 @@ public enum FunctionDeclarationKind { STR_TO_CODE, STR_LT, STR_LE, + + RE_NONE, RE_PLUS, RE_STAR, RE_OPTIONAL, @@ -308,6 +310,13 @@ public enum FunctionDeclarationKind { RE_COMPLEMENT, RE_DIFFERENCE, + // Separation logic + SEP_EMP, + SEP_NIL, + SEP_PTO, + SEP_STAR, + SEP_WAND, + // default case /** diff --git a/src/org/sosy_lab/java_smt/api/SLFormulaManager.java b/src/org/sosy_lab/java_smt/api/SLFormulaManager.java index 46cfcf7e01..15575fa119 100644 --- a/src/org/sosy_lab/java_smt/api/SLFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/SLFormulaManager.java @@ -80,8 +80,8 @@ public interface SLFormulaManager { * * @param the type of the address formula. * @param the type of the address formula type. - * @param pAdressType the type of the address formula. + * @param pAddressType the type of the address formula. * @return a formula representing the "nil" element for the given address type. */ - > AF makeNilElement(AT pAdressType); + > AF makeNilElement(AT pAddressType); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java index 72d3e65574..b3fc78f24f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java @@ -207,11 +207,15 @@ public ResultFormulaType sum(List operands) { } protected TFormulaInfo sumImpl(List operands) { - TFormulaInfo result = makeNumberImpl(0); - for (TFormulaInfo operand : operands) { - result = add(result, operand); + if (operands.isEmpty()) { + return makeNumberImpl(0); + } else { + TFormulaInfo result = operands.get(0); + for (TFormulaInfo operand : operands.subList(1, operands.size())) { + result = add(result, operand); + } + return result; } - return result; } @Override diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceArrayFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceArrayFormulaManager.java new file mode 100644 index 0000000000..d5d5714203 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceArrayFormulaManager.java @@ -0,0 +1,102 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import org.sosy_lab.java_smt.api.ArrayFormula; +import org.sosy_lab.java_smt.api.ArrayFormulaManager; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; + +@SuppressWarnings("MethodTypeParameterName") +public class TraceArrayFormulaManager implements ArrayFormulaManager { + private final ArrayFormulaManager delegate; + private final TraceLogger logger; + + TraceArrayFormulaManager(ArrayFormulaManager pDelegate, TraceLogger pLogger) { + delegate = pDelegate; + logger = pLogger; + } + + @Override + public TE select( + ArrayFormula pArray, TI pIndex) { + return logger.logDef( + "mgr.getArrayFormulaManager()", + String.format("select(%s, %s)", logger.toVariable(pArray), logger.toVariable(pIndex)), + () -> delegate.select(pArray, pIndex)); + } + + @Override + public ArrayFormula store( + ArrayFormula pArray, TI pIndex, TE pValue) { + return logger.logDef( + "mgr.getArrayFormulaManager()", + String.format( + "store(%s, %s, %s)", + logger.toVariable(pArray), logger.toVariable(pIndex), logger.toVariable(pValue)), + () -> delegate.store(pArray, pIndex, pValue)); + } + + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(String pName, FTI pIndexType, FTE pElementType) { + return logger.logDef( + "mgr.getArrayFormulaManager()", + String.format( + "makeArray(%s, %s, %s)", + logger.printString(pName), + logger.printFormulaType(pIndexType), + logger.printFormulaType(pElementType)), + () -> delegate.makeArray(pName, pIndexType, pElementType)); + } + + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(FTI pIndexType, FTE pElementType, TE defaultElement) { + return logger.logDef( + "mgr.getArrayFormulaManager()", + String.format( + "makeArray(%s, %s, %s)", + logger.printFormulaType(pIndexType), + logger.printFormulaType(pElementType), + logger.toVariable(defaultElement)), + () -> delegate.makeArray(pIndexType, pElementType, defaultElement)); + } + + @Override + public BooleanFormula equivalence( + ArrayFormula pArray1, ArrayFormula pArray2) { + return logger.logDef( + "mgr.getArrayFormulaManager()", + String.format( + "equivalence(%s, %s)", logger.toVariable(pArray1), logger.toVariable(pArray2)), + () -> delegate.equivalence(pArray1, pArray2)); + } + + @Override + public FormulaType getIndexType(ArrayFormula pArray) { + return delegate.getIndexType(pArray); + } + + @Override + public FormulaType getElementType(ArrayFormula pArray) { + return delegate.getElementType(pArray); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceBasicProverEnvironment.java new file mode 100644 index 0000000000..71983d6ce3 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceBasicProverEnvironment.java @@ -0,0 +1,135 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import java.util.Collection; +import java.util.List; +import java.util.Optional; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.java_smt.api.BasicProverEnvironment; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.SolverException; + +public class TraceBasicProverEnvironment implements BasicProverEnvironment { + private final BasicProverEnvironment delegate; + + private final TraceFormulaManager mgr; + private final TraceLogger logger; + + TraceBasicProverEnvironment( + BasicProverEnvironment pDelegate, + TraceFormulaManager pFormulaManager, + TraceLogger pLogger) { + delegate = pDelegate; + mgr = pFormulaManager; + logger = pLogger; + } + + @Override + public void pop() { + logger.logStmt(logger.toVariable(this), "pop()", delegate::pop); + } + + @Override + public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException { + return logger.logDefKeep( + logger.toVariable(this), + String.format("addConstraint(%s)", logger.toVariable(constraint)), + () -> delegate.addConstraint(constraint)); + } + + @Override + public void push() throws InterruptedException { + logger.logStmt(logger.toVariable(this), "push()", delegate::push); + } + + @Override + public int size() { + return delegate.size(); + } + + @Override + public boolean isUnsat() throws SolverException, InterruptedException { + return logger.logDefKeep(logger.toVariable(this), "isUnsat()", delegate::isUnsat); + } + + @Override + public boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + return logger.logDefKeep( + logger.toVariable(this), + String.format( + "isUnsatWithAssumptions(ImmutableList.of(%s))", logger.toVariables(assumptions)), + () -> delegate.isUnsatWithAssumptions(assumptions)); + } + + @SuppressWarnings("resource") + @Override + public Model getModel() throws SolverException { + return logger.logDefKeep( + logger.toVariable(this), + "getModel()", + () -> new TraceModel(delegate.getModel(), mgr, logger)); + } + + @Override + public List getUnsatCore() { + return mgr.rebuildAll( + logger.logDefDiscard(logger.toVariable(this), "getUnsatCore()", delegate::getUnsatCore)); + } + + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + return logger + .logDefKeep( + logger.toVariable(this), + String.format( + "getUnsatCoreOverAssumptions(ImmutableList.of(%s))", + logger.toVariables(assumptions)), + () -> delegate.unsatCoreOverAssumptions(assumptions)) + .map(mgr::rebuildAll); + } + + @Override + public void close() { + logger.logStmt(logger.toVariable(this), "close()", delegate::close); + } + + @Override + public R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + return logger.logDefDiscard( + logger.toVariable(this), + String.format( + "delegate.allSat(new AllSatCallback<>() {" + + " public void apply(List model) {}" + + " public R getResult() { throw new UnsupportedOperationException(); }" + + "}, ImmutableList.of(%s));", + logger.toVariables(important)), + () -> + delegate.allSat( + new AllSatCallback() { + @Override + public void apply(List model) { + var newModel = mgr.rebuildAll(model); + callback.apply(newModel); + } + + @Override + public R getResult() throws InterruptedException { + return callback.getResult(); + } + }, + important)); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceBitvectorFormulaManager.java new file mode 100644 index 0000000000..4db78c5804 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceBitvectorFormulaManager.java @@ -0,0 +1,312 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import java.math.BigInteger; +import java.util.List; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BitvectorFormulaManager; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; + +public class TraceBitvectorFormulaManager implements BitvectorFormulaManager { + private final BitvectorFormulaManager delegate; + private final TraceLogger logger; + + TraceBitvectorFormulaManager(BitvectorFormulaManager pDelegate, TraceLogger pLogger) { + delegate = pDelegate; + logger = pLogger; + } + + @Override + public BitvectorFormula makeBitvector(int length, long pI) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("makeBitvector(%s, %sL)", length, pI), + () -> delegate.makeBitvector(length, pI)); + } + + @Override + public BitvectorFormula makeBitvector(int length, BigInteger pI) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("makeBitvector(%s, new BigInteger(\"%s\"))", length, pI), + () -> delegate.makeBitvector(length, pI)); + } + + @Override + public BitvectorFormula makeBitvector(int length, IntegerFormula pI) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("makeBitvector(%s, %s)", length, logger.toVariable(pI)), + () -> delegate.makeBitvector(length, pI)); + } + + @Override + public IntegerFormula toIntegerFormula(BitvectorFormula pI, boolean signed) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("toIntegerFormula(%s, %s)", logger.toVariable(pI), signed), + () -> delegate.toIntegerFormula(pI, signed)); + } + + @Override + public BitvectorFormula makeVariable(int length, String pVar) { + return makeVariable(FormulaType.getBitvectorTypeWithSize(length), pVar); + } + + @Override + public BitvectorFormula makeVariable(BitvectorType type, String pVar) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format( + "makeVariable(%s, %s)", logger.printFormulaType(type), logger.printString(pVar)), + () -> delegate.makeVariable(type, pVar)); + } + + @Override + public int getLength(BitvectorFormula number) { + return logger.logDefDiscard( + "mgr.getBitvectorFormulaManager()", + String.format("getLength(%s)", logger.toVariable(number)), + () -> delegate.getLength(number)); + } + + @Override + public BitvectorFormula negate(BitvectorFormula number) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("negate(%s)", logger.toVariable(number)), + () -> delegate.negate(number)); + } + + @Override + public BitvectorFormula add(BitvectorFormula number1, BitvectorFormula number2) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("add(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.add(number1, number2)); + } + + @Override + public BitvectorFormula subtract(BitvectorFormula number1, BitvectorFormula number2) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("subtract(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.subtract(number1, number2)); + } + + @Override + public BitvectorFormula divide( + BitvectorFormula dividend, BitvectorFormula divisor, boolean signed) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format( + "divide(%s, %s, %s)", logger.toVariable(dividend), logger.toVariable(divisor), signed), + () -> delegate.divide(dividend, divisor, signed)); + } + + @Override + public BitvectorFormula smodulo(BitvectorFormula dividend, BitvectorFormula divisor) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("smodulo(%s, %s)", logger.toVariable(dividend), logger.toVariable(dividend)), + () -> delegate.smodulo(dividend, divisor)); + } + + @Override + public BitvectorFormula remainder( + BitvectorFormula dividend, BitvectorFormula divisor, boolean signed) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format( + "remainder(%s, %s, %s)", + logger.toVariable(dividend), logger.toVariable(divisor), signed), + () -> delegate.remainder(dividend, divisor, signed)); + } + + @Override + public BitvectorFormula multiply(BitvectorFormula number1, BitvectorFormula number2) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("multiply(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.multiply(number1, number2)); + } + + @Override + public BooleanFormula equal(BitvectorFormula number1, BitvectorFormula number2) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("equal(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.equal(number1, number2)); + } + + @Override + public BooleanFormula greaterThan( + BitvectorFormula number1, BitvectorFormula number2, boolean signed) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format( + "greaterThan(%s, %s, %s)", + logger.toVariable(number1), logger.toVariable(number2), signed), + () -> delegate.greaterThan(number1, number2, signed)); + } + + @Override + public BooleanFormula greaterOrEquals( + BitvectorFormula number1, BitvectorFormula number2, boolean signed) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format( + "greaterOrEquals(%s, %s, %s)", + logger.toVariable(number1), logger.toVariable(number2), signed), + () -> delegate.greaterOrEquals(number1, number2, signed)); + } + + @Override + public BooleanFormula lessThan( + BitvectorFormula number1, BitvectorFormula number2, boolean signed) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format( + "lessThan(%s, %s, %s)", logger.toVariable(number1), logger.toVariable(number2), signed), + () -> delegate.lessThan(number1, number2, signed)); + } + + @Override + public BooleanFormula lessOrEquals( + BitvectorFormula number1, BitvectorFormula number2, boolean signed) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format( + "lessOrEquals(%s, %s, %s)", + logger.toVariable(number1), logger.toVariable(number2), signed), + () -> delegate.lessOrEquals(number1, number2, signed)); + } + + @Override + public BitvectorFormula not(BitvectorFormula bits) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("not(%s)", logger.toVariable(bits)), + () -> delegate.not(bits)); + } + + @Override + public BitvectorFormula and(BitvectorFormula bits1, BitvectorFormula bits2) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("and(%s, %s)", logger.toVariable(bits1), logger.toVariable(bits2)), + () -> delegate.and(bits1, bits2)); + } + + @Override + public BitvectorFormula or(BitvectorFormula bits1, BitvectorFormula bits2) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("or(%s, %s)", logger.toVariable(bits1), logger.toVariable(bits2)), + () -> delegate.or(bits1, bits2)); + } + + @Override + public BitvectorFormula xor(BitvectorFormula bits1, BitvectorFormula bits2) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("xor(%s, %s)", logger.toVariable(bits1), logger.toVariable(bits2)), + () -> delegate.xor(bits1, bits2)); + } + + @Override + public BitvectorFormula shiftRight( + BitvectorFormula number, BitvectorFormula toShift, boolean signed) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format( + "shiftRight(%s, %s, %s)", + logger.toVariable(number), logger.toVariable(toShift), signed), + () -> delegate.shiftRight(number, toShift, signed)); + } + + @Override + public BitvectorFormula shiftLeft(BitvectorFormula number, BitvectorFormula toShift) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("shiftLeft(%s, %s)", logger.toVariable(number), logger.toVariable(toShift)), + () -> delegate.shiftLeft(number, toShift)); + } + + @Override + public BitvectorFormula rotateLeft(BitvectorFormula number, int toRotate) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("rotateLeft(%s, %s)", logger.toVariable(number), toRotate), + () -> delegate.rotateLeft(number, toRotate)); + } + + @Override + public BitvectorFormula rotateLeft(BitvectorFormula number, BitvectorFormula toRotate) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("rotateLeft(%s, %s)", logger.toVariable(number), logger.toVariable(toRotate)), + () -> delegate.rotateLeft(number, toRotate)); + } + + @Override + public BitvectorFormula rotateRight(BitvectorFormula number, int toRotate) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("rotateRight(%s, %s)", logger.toVariable(number), toRotate), + () -> delegate.rotateRight(number, toRotate)); + } + + @Override + public BitvectorFormula rotateRight(BitvectorFormula number, BitvectorFormula toRotate) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format( + "rotateRight(%s, %s)", logger.toVariable(number), logger.toVariable(toRotate)), + () -> delegate.rotateRight(number, toRotate)); + } + + @Override + public BitvectorFormula concat(BitvectorFormula prefix, BitvectorFormula suffix) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("concat(%s, %s)", logger.toVariable(prefix), logger.toVariable(prefix)), + () -> delegate.concat(prefix, suffix)); + } + + @Override + public BitvectorFormula extract(BitvectorFormula number, int msb, int lsb) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("extract(%s, %s, %s)", logger.toVariable(number), msb, lsb), + () -> delegate.extract(number, msb, lsb)); + } + + @Override + public BitvectorFormula extend(BitvectorFormula number, int extensionBits, boolean signed) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("extend(%s, %s, %s)", logger.toVariable(number), extensionBits, signed), + () -> delegate.extend(number, extensionBits, signed)); + } + + @Override + public BooleanFormula distinct(List pBits) { + return logger.logDef( + "mgr.getBitvectorFormulaManager()", + String.format("distinct(ImmutableList.of(%s))", logger.toVariables(pBits)), + () -> delegate.distinct(pBits)); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceBooleanFormulaManager.java new file mode 100644 index 0000000000..5d31d2e5c7 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceBooleanFormulaManager.java @@ -0,0 +1,207 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import com.google.common.collect.ImmutableList; +import java.util.Collection; +import java.util.Set; +import java.util.stream.Collector; +import java.util.stream.Collectors; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor; +import org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; + +public class TraceBooleanFormulaManager implements BooleanFormulaManager { + private final BooleanFormulaManager delegate; + + private final TraceFormulaManager mgr; + private final TraceLogger logger; + + TraceBooleanFormulaManager( + BooleanFormulaManager pDelegate, TraceFormulaManager pMgr, TraceLogger pLogger) { + delegate = pDelegate; + mgr = pMgr; + logger = pLogger; + } + + @Override + public BooleanFormula makeTrue() { + return logger.logDef("mgr.getBooleanFormulaManager()", "makeTrue()", delegate::makeTrue); + } + + @Override + public BooleanFormula makeFalse() { + return logger.logDef("mgr.getBooleanFormulaManager()", "makeFalse()", delegate::makeFalse); + } + + @Override + public BooleanFormula makeVariable(String pVar) { + return logger.logDef( + "mgr.getBooleanFormulaManager()", + String.format("makeVariable(%s)", logger.printString(pVar)), + () -> delegate.makeVariable(pVar)); + } + + @Override + public BooleanFormula equivalence(BooleanFormula formula1, BooleanFormula formula2) { + return logger.logDef( + "mgr.getBooleanFormulaManager()", + String.format( + "equivalence(%s, %s)", logger.toVariable(formula1), logger.toVariable(formula2)), + () -> delegate.equivalence(formula1, formula2)); + } + + @Override + public BooleanFormula implication(BooleanFormula formula1, BooleanFormula formula2) { + return logger.logDef( + "mgr.getBooleanFormulaManager()", + String.format( + "implication(%s, %s)", logger.toVariable(formula1), logger.toVariable(formula2)), + () -> delegate.implication(formula1, formula2)); + } + + @Override + public boolean isTrue(BooleanFormula formula) { + return logger.logDefDiscard( + "mgr.getBooleanFormulaManager()", + String.format("isTrue(%s)", logger.toVariable(formula)), + () -> delegate.isTrue(formula)); + } + + @Override + public boolean isFalse(BooleanFormula formula) { + return logger.logDefDiscard( + "mgr.getBooleanFormulaManager()", + String.format("isFalse(%s)", logger.toVariable(formula)), + () -> delegate.isFalse(formula)); + } + + @Override + public T ifThenElse(BooleanFormula cond, T f1, T f2) { + return logger.logDef( + "mgr.getBooleanFormulaManager()", + String.format( + "ifThenElse(%s, %s, %s)", + logger.toVariable(cond), logger.toVariable(f1), logger.toVariable(f2)), + () -> delegate.ifThenElse(cond, f1, f2)); + } + + @Override + public BooleanFormula not(BooleanFormula formula) { + return logger.logDef( + "mgr.getBooleanFormulaManager()", + String.format("not(%s)", logger.toVariable(formula)), + () -> delegate.not(formula)); + } + + @Override + public BooleanFormula and(BooleanFormula formula1, BooleanFormula formula2) { + return and(ImmutableList.of(formula1, formula2)); + } + + @Override + public BooleanFormula and(Collection bits) { + return logger.logDef( + "mgr.getBooleanFormulaManager()", + String.format("and(%s)", logger.toVariables(bits)), + () -> delegate.and(bits)); + } + + @Override + public Collector toConjunction() { + return Collectors.collectingAndThen(Collectors.toList(), this::and); + } + + @Override + public BooleanFormula or(BooleanFormula formula1, BooleanFormula formula2) { + return or(ImmutableList.of(formula1, formula2)); + } + + @Override + public BooleanFormula or(Collection bits) { + return logger.logDef( + "mgr.getBooleanFormulaManager()", + String.format("or(%s)", logger.toVariables(bits)), + () -> delegate.or(bits)); + } + + @Override + public Collector toDisjunction() { + return Collectors.collectingAndThen(Collectors.toList(), this::or); + } + + @Override + public BooleanFormula xor(BooleanFormula bits1, BooleanFormula bits2) { + return logger.logDef( + "mgr.getBooleanFormulaManager()", + String.format("xor(%s, %s)", logger.toVariable(bits1), logger.toVariable(bits2)), + () -> delegate.xor(bits1, bits2)); + } + + @Override + public R visit(BooleanFormula pFormula, BooleanFormulaVisitor visitor) { + return logger.logDefDiscard( + "mgr.getBooleanFormulaManager()", + String.format( + "visit(%s, new DefaultBooleanFormulaVisitor<>() {" + + "protected Formula visitDefault(Formula f) {" + + "return %s;" + + "}})", + logger.toVariable(pFormula), logger.toVariable(pFormula)), + () -> delegate.visit(pFormula, visitor)); + } + + @Override + public void visitRecursively( + BooleanFormula f, BooleanFormulaVisitor rFormulaVisitor) { + logger.logStmtDiscard( + "mgr.getBooleanFormulaManager()", + String.format( + "visitRecursively(%s, new DefaultBooleanFormulaVisitor<>() {" + + "protected TraversalProcess visitDefault(Formula f) {" + + "return TraversalProcess.CONTINUE;" + + "}})", + logger.toVariable(f)), + () -> delegate.visitRecursively(f, rFormulaVisitor)); + } + + @Override + public BooleanFormula transformRecursively( + BooleanFormula f, BooleanFormulaTransformationVisitor pVisitor) { + return logger.logDefDiscard( + "mgr.getBooleanFormulaManager()", + String.format( + "transformRecursively(%s, new BooleanFormulaTransformationVisitor(%s) {})", + logger.toVariable(f), "mgr"), + () -> delegate.transformRecursively(f, pVisitor)); + } + + @Override + public Set toConjunctionArgs(BooleanFormula f, boolean flatten) { + return mgr.rebuildAll( + logger.logDefDiscard( + "mgr.getBooleanFormulaManager()", + String.format("toConjunctionArgs(%s, %s)", logger.toVariable(f), flatten), + () -> delegate.toConjunctionArgs(f, flatten))); + } + + @Override + public Set toDisjunctionArgs(BooleanFormula f, boolean flatten) { + return mgr.rebuildAll( + logger.logDefDiscard( + "mgr.getBooleanFormulaManager()", + String.format("toDisjunctionArgs(%s, %s)", logger.toVariable(f), flatten), + () -> delegate.toDisjunctionArgs(f, flatten))); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceEnumerationFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceEnumerationFormulaManager.java new file mode 100644 index 0000000000..cd31bdec3d --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceEnumerationFormulaManager.java @@ -0,0 +1,68 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2025 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.delegate.trace; + +import static com.google.common.base.Preconditions.checkNotNull; + +import com.google.common.base.Joiner; +import com.google.common.collect.FluentIterable; +import java.util.Set; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.EnumerationFormula; +import org.sosy_lab.java_smt.api.EnumerationFormulaManager; +import org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType; + +public class TraceEnumerationFormulaManager implements EnumerationFormulaManager { + + private final EnumerationFormulaManager delegate; + private final TraceLogger logger; + + TraceEnumerationFormulaManager(EnumerationFormulaManager pDelegate, TraceLogger pLogger) { + delegate = checkNotNull(pDelegate); + logger = checkNotNull(pLogger); + } + + @Override + public EnumerationFormulaType declareEnumeration(String name, Set elementNames) { + return logger.logDefKeep( + "mgr.getEnumerationFormulaManager()", + String.format( + "declareEnumeration(%s, Set.of(%s))", + logger.printString(name), + FluentIterable.from(elementNames).transform(logger::printString).join(Joiner.on(", "))), + () -> delegate.declareEnumeration(name, elementNames)); + } + + @Override + public EnumerationFormula makeConstant(String pName, EnumerationFormulaType pType) { + return logger.logDef( + "mgr.getEnumerationFormulaManager()", + String.format("makeConstant(%s, %s)", logger.printString(pName), logger.toVariable(pType)), + () -> delegate.makeConstant(pName, pType)); + } + + @Override + public EnumerationFormula makeVariable(String pVar, EnumerationFormulaType pType) { + return logger.logDef( + "mgr.getEnumerationFormulaManager()", + String.format("makeVariable(%s, %s)", logger.printString(pVar), logger.toVariable(pType)), + () -> delegate.makeVariable(pVar, pType)); + } + + @Override + public BooleanFormula equivalence( + EnumerationFormula pEnumeration1, EnumerationFormula pEnumeration2) { + return logger.logDef( + "mgr.getEnumerationFormulaManager()", + String.format( + "equivalence(%s, %s)", + logger.toVariable(pEnumeration1), logger.toVariable(pEnumeration2)), + () -> delegate.equivalence(pEnumeration1, pEnumeration2)); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceFloatingPointFormulaManager.java new file mode 100644 index 0000000000..1c65a2cded --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceFloatingPointFormulaManager.java @@ -0,0 +1,495 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import java.math.BigDecimal; +import java.math.BigInteger; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormulaManager; +import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; +import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; + +public class TraceFloatingPointFormulaManager implements FloatingPointFormulaManager { + private final FloatingPointFormulaManager delegate; + private final TraceLogger logger; + + TraceFloatingPointFormulaManager(FloatingPointFormulaManager pDelegate, TraceLogger pLogger) { + delegate = pDelegate; + logger = pLogger; + } + + private String printRoundingMode(FloatingPointRoundingMode pRoundingMode) { + return "FloatingPointRoundingMode." + pRoundingMode.name(); + } + + private String printSign(Sign pSign) { + return "FloatingPointNumber.Sign." + pSign.name(); + } + + private String printDouble(double number) { + if (Double.isNaN(number)) { + return "Double.NaN"; + } else if (Double.isInfinite(number)) { + return number > 0 ? "Double.POSITIVE_INFINITY" : "Double.NEGATIVE_INFINITY"; + } else if (number == 0.0 + && Double.doubleToRawLongBits(number) == Double.doubleToRawLongBits(-0.0)) { + return "-0.0"; + } else { + return Double.toString(number); + } + } + + @Override + public FloatingPointRoundingModeFormula makeRoundingMode( + FloatingPointRoundingMode pRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("makeRoundingMode(%s)", "FloatingPointRoundingMode." + pRoundingMode.name()), + () -> delegate.makeRoundingMode(pRoundingMode)); + } + + @Override + public FloatingPointRoundingMode fromRoundingModeFormula( + FloatingPointRoundingModeFormula pRoundingModeFormula) { + return logger.logDefDiscard( + "mgr.getFloatingPointFormulaManager()", + String.format("fromRoundingModeFormula(%s)", logger.toVariable(pRoundingModeFormula)), + () -> delegate.fromRoundingModeFormula(pRoundingModeFormula)); + } + + @Override + public FloatingPointFormula makeNumber(double n, FloatingPointType type) { + return makeNumber(n, type, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula makeNumber( + double n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "makeNumber(%s, %s, %s)", + printDouble(n), + logger.printFormulaType(type), + printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.makeNumber(n, type, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula makeNumber(BigDecimal n, FloatingPointType type) { + return makeNumber(n, type, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula makeNumber( + BigDecimal n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "makeNumber(new BigDecimal(\"%s\"), %s, %s)", + n, logger.printFormulaType(type), printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.makeNumber(n, type, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula makeNumber(String n, FloatingPointType type) { + return makeNumber(n, type, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula makeNumber( + String n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "makeNumber(\"%s\", %s, %s)", + n, logger.printFormulaType(type), printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.makeNumber(n, type, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula makeNumber(Rational n, FloatingPointType type) { + return makeNumber(n, type, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula makeNumber( + Rational n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "makeNumber(Rational.of(\"%s\"), %s, %s)", + n, logger.printFormulaType(type), printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.makeNumber(n, type, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula makeNumber( + BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "makeNumber(new BigInteger(\"%s\"), new BigInteger(\"%s\"), %s, %s)", + exponent, mantissa, printSign(sign), logger.printFormulaType(type)), + () -> delegate.makeNumber(exponent, mantissa, sign, type)); + } + + @Override + public FloatingPointFormula makeVariable(String pVar, FloatingPointType type) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "makeVariable(%s, %s)", logger.printString(pVar), logger.printFormulaType(type)), + () -> delegate.makeVariable(pVar, type)); + } + + @Override + public FloatingPointFormula makePlusInfinity(FloatingPointType type) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("makePlusInfinity(%s)", logger.printFormulaType(type)), + () -> delegate.makePlusInfinity(type)); + } + + @Override + public FloatingPointFormula makeMinusInfinity(FloatingPointType type) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("makeMinusInfinity(%s)", logger.printFormulaType(type)), + () -> delegate.makeMinusInfinity(type)); + } + + @Override + public FloatingPointFormula makeNaN(FloatingPointType type) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("makeNaN(%s)", logger.printFormulaType(type)), + () -> delegate.makeNaN(type)); + } + + @Override + public T castTo( + FloatingPointFormula source, boolean signed, FormulaType targetType) { + return castTo(source, signed, targetType, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public T castTo( + FloatingPointFormula source, + boolean signed, + FormulaType targetType, + FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "castTo(%s, %s, %s, %s)", + logger.toVariable(source), + signed, + logger.printFormulaType(targetType), + printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.castTo(source, signed, targetType, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula castFrom( + Formula source, boolean signed, FloatingPointType targetType) { + return castFrom(source, signed, targetType, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula castFrom( + Formula source, + boolean signed, + FloatingPointType targetType, + FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "castFrom(%s, %s, %s, %s)", + logger.toVariable(source), + signed, + logger.printFormulaType(targetType), + printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.castFrom(source, signed, targetType, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula fromIeeeBitvector( + BitvectorFormula number, FloatingPointType pTargetType) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "fromIeeeBitvector(%s, %s)", + logger.toVariable(number), logger.printFormulaType(pTargetType)), + () -> delegate.fromIeeeBitvector(number, pTargetType)); + } + + @Override + public BitvectorFormula toIeeeBitvector(FloatingPointFormula number) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("toIeeeBitvector(%s)", logger.toVariable(number)), + () -> delegate.toIeeeBitvector(number)); + } + + @Override + public FloatingPointFormula round( + FloatingPointFormula formula, FloatingPointRoundingMode roundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("round(%s, %s)", logger.toVariable(formula), printRoundingMode(roundingMode)), + () -> delegate.round(formula, roundingMode)); + } + + @Override + public FloatingPointFormula negate(FloatingPointFormula number) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("negate(%s)", logger.toVariable(number)), + () -> delegate.negate(number)); + } + + @Override + public FloatingPointFormula abs(FloatingPointFormula number) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("abs(%s)", logger.toVariable(number)), + () -> delegate.abs(number)); + } + + @Override + public FloatingPointFormula max(FloatingPointFormula number1, FloatingPointFormula number2) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("max(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.max(number1, number2)); + } + + @Override + public FloatingPointFormula min(FloatingPointFormula number1, FloatingPointFormula number2) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("min(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.min(number1, number2)); + } + + @Override + public FloatingPointFormula sqrt(FloatingPointFormula number) { + return sqrt(number, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula sqrt( + FloatingPointFormula number, FloatingPointRoundingMode roundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("sqrt(%s, %s)", logger.toVariable(number), printRoundingMode(roundingMode)), + () -> delegate.sqrt(number, roundingMode)); + } + + @Override + public FloatingPointFormula add(FloatingPointFormula number1, FloatingPointFormula number2) { + return add(number1, number2, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula add( + FloatingPointFormula number1, + FloatingPointFormula number2, + FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "add(%s, %s, %s)", + logger.toVariable(number1), + logger.toVariable(number2), + printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.add(number1, number2, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula subtract(FloatingPointFormula number1, FloatingPointFormula number2) { + return subtract(number1, number2, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula subtract( + FloatingPointFormula number1, + FloatingPointFormula number2, + FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "subtract(%s, %s, %s)", + logger.toVariable(number1), + logger.toVariable(number2), + printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.subtract(number1, number2, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula divide(FloatingPointFormula number1, FloatingPointFormula number2) { + return divide(number1, number2, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula divide( + FloatingPointFormula number1, + FloatingPointFormula number2, + FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "divide(%s, %s, %s)", + logger.toVariable(number1), + logger.toVariable(number2), + printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.divide(number1, number2, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula multiply(FloatingPointFormula number1, FloatingPointFormula number2) { + return multiply(number1, number2, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public FloatingPointFormula multiply( + FloatingPointFormula number1, + FloatingPointFormula number2, + FloatingPointRoundingMode pFloatingPointRoundingMode) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "multiply(%s, %s, %s)", + logger.toVariable(number1), + logger.toVariable(number2), + printRoundingMode(pFloatingPointRoundingMode)), + () -> delegate.multiply(number1, number2, pFloatingPointRoundingMode)); + } + + @Override + public FloatingPointFormula remainder( + FloatingPointFormula dividend, FloatingPointFormula divisor) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("remainder(%s, %s)", logger.toVariable(dividend), logger.toVariable(divisor)), + () -> delegate.remainder(dividend, divisor)); + } + + @Override + public BooleanFormula assignment(FloatingPointFormula number1, FloatingPointFormula number2) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("assignment(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.assignment(number1, number2)); + } + + @Override + public BooleanFormula equalWithFPSemantics( + FloatingPointFormula number1, FloatingPointFormula number2) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "equalWithFPSemantics(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.equalWithFPSemantics(number1, number2)); + } + + @Override + public BooleanFormula greaterThan(FloatingPointFormula number1, FloatingPointFormula number2) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "greaterThan(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.greaterThan(number1, number2)); + } + + @Override + public BooleanFormula greaterOrEquals( + FloatingPointFormula number1, FloatingPointFormula number2) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "greaterOrEquals(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.greaterOrEquals(number1, number2)); + } + + @Override + public BooleanFormula lessThan(FloatingPointFormula number1, FloatingPointFormula number2) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("lessThan(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.lessThan(number1, number2)); + } + + @Override + public BooleanFormula lessOrEquals(FloatingPointFormula number1, FloatingPointFormula number2) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format( + "lessOrEquals(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.lessOrEquals(number1, number2)); + } + + @Override + public BooleanFormula isNaN(FloatingPointFormula number) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("isNaN(%s)", logger.toVariable(number)), + () -> delegate.isNaN(number)); + } + + @Override + public BooleanFormula isInfinity(FloatingPointFormula number) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("isInfinity(%s)", logger.toVariable(number)), + () -> delegate.isInfinity(number)); + } + + @Override + public BooleanFormula isZero(FloatingPointFormula number) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("isZero(%s)", logger.toVariable(number)), + () -> delegate.isZero(number)); + } + + @Override + public BooleanFormula isNormal(FloatingPointFormula number) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("isNormal(%s)", logger.toVariable(number)), + () -> delegate.isNormal(number)); + } + + @Override + public BooleanFormula isSubnormal(FloatingPointFormula number) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("isSubnormal(%s)", logger.toVariable(number)), + () -> delegate.isSubnormal(number)); + } + + @Override + public BooleanFormula isNegative(FloatingPointFormula number) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + String.format("isNegative(%s)", logger.toVariable(number)), + () -> delegate.isNegative(number)); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java new file mode 100644 index 0000000000..d921f10191 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java @@ -0,0 +1,1166 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import static org.sosy_lab.common.collect.Collections3.transformedImmutableListCopy; +import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy; + +import com.google.common.base.Joiner; +import com.google.common.base.Preconditions; +import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import java.math.BigInteger; +import java.util.List; +import java.util.Map; +import java.util.Set; +import org.sosy_lab.common.Appender; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.ArrayFormula; +import org.sosy_lab.java_smt.api.ArrayFormulaManager; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BitvectorFormulaManager; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.EnumerationFormulaManager; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormulaManager; +import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; +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.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; +import org.sosy_lab.java_smt.api.RationalFormulaManager; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.SLFormulaManager; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; +import org.sosy_lab.java_smt.api.Tactic; +import org.sosy_lab.java_smt.api.UFManager; +import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor; +import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; + +public class TraceFormulaManager implements FormulaManager { + private final FormulaManager delegate; + private TraceLogger logger; + + TraceFormulaManager(FormulaManager pDelegate) { + delegate = pDelegate; + } + + void setLogger(TraceLogger pLogger) { + logger = pLogger; + } + + @Override + public IntegerFormulaManager getIntegerFormulaManager() { + return new TraceIntegerFormulaManager(delegate.getIntegerFormulaManager(), logger); + } + + @Override + public RationalFormulaManager getRationalFormulaManager() { + return new TraceRationalFormulaManager(delegate.getRationalFormulaManager(), logger); + } + + @Override + public BooleanFormulaManager getBooleanFormulaManager() { + return new TraceBooleanFormulaManager(delegate.getBooleanFormulaManager(), this, logger); + } + + @Override + public ArrayFormulaManager getArrayFormulaManager() { + return new TraceArrayFormulaManager(delegate.getArrayFormulaManager(), logger); + } + + @Override + public BitvectorFormulaManager getBitvectorFormulaManager() { + return new TraceBitvectorFormulaManager(delegate.getBitvectorFormulaManager(), logger); + } + + @Override + public FloatingPointFormulaManager getFloatingPointFormulaManager() { + return new TraceFloatingPointFormulaManager(delegate.getFloatingPointFormulaManager(), logger); + } + + @Override + public UFManager getUFManager() { + return new TraceUFManager(delegate.getUFManager(), this, logger); + } + + @Override + public SLFormulaManager getSLFormulaManager() { + return new TraceSLFormulaManager(delegate.getSLFormulaManager(), logger); + } + + @Override + public QuantifiedFormulaManager getQuantifiedFormulaManager() { + return new TraceQuantifiedFormulaManager(delegate.getQuantifiedFormulaManager(), logger); + } + + @Override + public StringFormulaManager getStringFormulaManager() { + return new TraceStringFormulaManager(delegate.getStringFormulaManager(), logger); + } + + @Override + public EnumerationFormulaManager getEnumerationFormulaManager() { + return new TraceEnumerationFormulaManager(delegate.getEnumerationFormulaManager(), logger); + } + + private class Rebuilder extends FormulaTransformationVisitor { + Rebuilder(FormulaManager fmgr) { + super(fmgr); + } + + @Override + public Formula visitFreeVariable(Formula f, String name) { + if (!logger.isTracked(f)) { + var g = + logger.logDef( + "mgr", + String.format( + "makeVariable(%s, %s)", + logger.printFormulaType(delegate.getFormulaType(f)), logger.printString(name)), + () -> delegate.makeVariable(delegate.getFormulaType(f), name)); + Preconditions.checkArgument(g.equals(f), "%s (should be: %s)", g, f); + } + return f; + } + + @Override + public Formula visitConstant(Formula f, Object value) { + if (!logger.isTracked(f)) { + Formula g; + if (f instanceof BooleanFormula && value instanceof Boolean) { + g = getBooleanFormulaManager().makeBoolean((Boolean) value); + } else if (f instanceof BitvectorFormula && value instanceof BigInteger) { + var bvSize = delegate.getBitvectorFormulaManager().getLength((BitvectorFormula) f); + g = getBitvectorFormulaManager().makeBitvector(bvSize, (BigInteger) value); + } else if (f instanceof IntegerFormula && value instanceof BigInteger) { + g = getIntegerFormulaManager().makeNumber((BigInteger) value); + } else if (f instanceof RationalFormula && value instanceof BigInteger) { + g = getRationalFormulaManager().makeNumber((BigInteger) value); + } else if (f instanceof RationalFormula && value instanceof Rational) { + g = getRationalFormulaManager().makeNumber((Rational) value); + } else if (f instanceof FloatingPointRoundingModeFormula + && value instanceof FloatingPointRoundingMode) { + g = getFloatingPointFormulaManager().makeRoundingMode((FloatingPointRoundingMode) value); + } else if (f instanceof StringFormula && value instanceof String) { + g = getStringFormulaManager().makeString((String) value); + } else { + throw new IllegalArgumentException( + String.format( + "Unsupported value: Formula=%s, Value=%s", + delegate.getFormulaType(f), value.getClass().getName())); + } + Preconditions.checkArgument(g.equals(f)); + } + return f; + } + + @SuppressWarnings("CheckReturnValue") + @Override + public Formula visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + if (!logger.isTracked(f)) { + Formula g = makeApplication(functionDeclaration, args); + Preconditions.checkArgument(g.equals(f), "%s (should be: %s)", g, f); + } + return f; + } + + @SuppressWarnings("CheckReturnValue") + @Override + public BooleanFormula visitQuantifier( + BooleanFormula f, + Quantifier quantifier, + List boundVariables, + BooleanFormula body) { + if (!logger.isTracked(f)) { + var bound = rebuildAll(boundVariables); + final Formula g; + if (quantifier == Quantifier.EXISTS) { + g = getQuantifiedFormulaManager().exists(bound, body); + } else { + g = getQuantifiedFormulaManager().forall(bound, body); + } + Preconditions.checkArgument(g.equals(f), "%s (should be: %s)", g, f); + } + return f; + } + } + + public T rebuild(T f) { + return delegate.transformRecursively(f, new TraceFormulaManager.Rebuilder(this)); + } + + public List rebuildAll(List formulas) { + return transformedImmutableListCopy(formulas, this::rebuild); + } + + public Set rebuildAll(Set formulas) { + return transformedImmutableSetCopy(formulas, this::rebuild); + } + + @Override + public T makeVariable(FormulaType formulaType, String name) { + return logger.logDef( + "mgr", + String.format( + "makeVariable(%s, %s)", logger.printFormulaType(formulaType), logger.printString(name)), + () -> delegate.makeVariable(formulaType, name)); + } + + private int getArity(FunctionDeclaration pDeclaration) { + switch (pDeclaration.getKind()) { + case AND: + case OR: + case IFF: + case XOR: + case IMPLIES: + case DISTINCT: + case SUB: + case ADD: + case DIV: + case MUL: + case LT: + case LTE: + case GT: + case GTE: + case EQ: + case BV_CONCAT: + case BV_OR: + case BV_AND: + case BV_XOR: + case BV_SUB: + case BV_ADD: + case BV_MUL: + case STR_CONCAT: + case STR_LT: + case STR_LE: + case RE_CONCAT: + case RE_DIFFERENCE: + case RE_UNION: + case RE_INTERSECT: + return -1; + + case RE_NONE: + case SEP_NIL: + return 0; + + case INT_TO_BV: + case NOT: + case UMINUS: + case EQ_ZERO: + case GTE_ZERO: + case FLOOR: + case TO_REAL: + case CONST: + case BV_EXTRACT: + case BV_SIGN_EXTENSION: + case BV_ZERO_EXTENSION: + case BV_NOT: + case BV_NEG: + case BV_ROTATE_LEFT_BY_INT: + case BV_ROTATE_RIGHT_BY_INT: + case UBV_TO_INT: + case SBV_TO_INT: + case FP_NEG: + case FP_ABS: + case FP_IS_NAN: + case FP_IS_INF: + case FP_IS_ZERO: + case FP_IS_NEGATIVE: + case FP_IS_SUBNORMAL: + case FP_IS_NORMAL: + case FP_AS_IEEEBV: + case FP_FROM_IEEEBV: + case RE_PLUS: + case RE_STAR: + case INT_TO_STR: + case STR_FROM_CODE: + case STR_TO_CODE: + case STR_LENGTH: + case STR_TO_INT: + case STR_TO_RE: + case RE_COMPLEMENT: + case RE_OPTIONAL: + return 1; + + case SELECT: + case MODULO: + case BV_SDIV: + case BV_UDIV: + case BV_SREM: + case BV_UREM: + case BV_SMOD: + case BV_ULT: + case BV_SLT: + case BV_ULE: + case BV_SLE: + case BV_UGT: + case BV_SGT: + case BV_UGE: + case BV_SGE: + case BV_SHL: + case BV_LSHR: + case BV_ASHR: + case BV_ROTATE_LEFT: + case BV_ROTATE_RIGHT: + case BV_UCASTTO_FP: + case BV_SCASTTO_FP: + case FP_MAX: + case FP_MIN: + case FP_SQRT: + case FP_REM: + case FP_LT: + case FP_LE: + case FP_GE: + case FP_GT: + case FP_EQ: + case FP_ROUND_TO_INTEGRAL: + case FP_CASTTO_FP: + case FP_CASTTO_SBV: + case FP_CASTTO_UBV: + case STR_CHAR_AT: + case STR_CONTAINS: + case STR_IN_RE: + case STR_PREFIX: + case STR_SUFFIX: + case RE_RANGE: + case SEP_PTO: + case SEP_EMP: + case SEP_STAR: + case SEP_WAND: + return 2; + + case ITE: + case STORE: + case FP_SUB: + case FP_ADD: + case FP_DIV: + case FP_MUL: + case STR_INDEX_OF: + case STR_REPLACE: + case STR_REPLACE_ALL: + case STR_SUBSTRING: + return 3; + + default: + throw new IllegalArgumentException( + String.format( + "Unsupported kind: \"%s\" (%s)", pDeclaration.getName(), pDeclaration.getKind())); + } + } + + @SuppressWarnings({"unchecked", "rawtypes"}) + @Override + public T makeApplication( + FunctionDeclaration declaration, List args) { + if (declaration.getKind().equals(FunctionDeclarationKind.UF)) { + var uf = + getUFManager() + .declareUF( + declaration.getName(), declaration.getType(), declaration.getArgumentTypes()); + return getUFManager().callUF(uf, args); + } else { + // TODO Handle operations with a variable number of arguments + // TODO Figure out how to handle rounding mode for floats + // TODO Handle rational formulas + Preconditions.checkArgument( + getArity(declaration) == -1 ? args.size() > 1 : args.size() == getArity(declaration), + "Term \"%s\" (%s): expecting %s arguments, but found %s", + declaration.getName(), + declaration.getKind(), + getArity(declaration), + args.size()); + switch (declaration.getKind()) { + case AND: + return (T) getBooleanFormulaManager().and((List) args); + case NOT: + return (T) getBooleanFormulaManager().not((BooleanFormula) args.get(0)); + case OR: + return (T) getBooleanFormulaManager().or((List) args); + case IFF: + Preconditions.checkArgument(args.size() == 2); + return (T) + getBooleanFormulaManager() + .equivalence((BooleanFormula) args.get(0), (BooleanFormula) args.get(1)); + case ITE: + return getBooleanFormulaManager() + .ifThenElse((BooleanFormula) args.get(0), (T) args.get(1), (T) args.get(2)); + case XOR: + Preconditions.checkArgument(args.size() == 2); + + return (T) + getBooleanFormulaManager() + .xor((BooleanFormula) args.get(0), (BooleanFormula) args.get(1)); + case IMPLIES: + Preconditions.checkArgument(args.size() == 2); + return (T) + getBooleanFormulaManager() + .implication((BooleanFormula) args.get(0), (BooleanFormula) args.get(1)); + case DISTINCT: + if (declaration.getType().isIntegerType()) { + return (T) getIntegerFormulaManager().distinct((List) args); + } else if (declaration.getType().isRationalType()) { + return (T) getRationalFormulaManager().distinct((List) args); + } else if (declaration.getType().isBitvectorType()) { + return (T) getBitvectorFormulaManager().distinct((List) args); + } else { + // FIXME JavaSMT only supports 'distinct' for some of its theories + throw new UnsupportedOperationException( + String.format( + "Operator 'distinct' not " + "supported for %ss", declaration.getType())); + } + case STORE: + return (T) + getArrayFormulaManager().store((ArrayFormula) args.get(0), args.get(1), args.get(2)); + case SELECT: + return (T) getArrayFormulaManager().select((ArrayFormula) args.get(0), args.get(1)); + case CONST: + return (T) + getArrayFormulaManager() + .makeArray((ArrayFormulaType) declaration.getType(), args.get(0)); + case UMINUS: + if (declaration.getType().isIntegerType()) { + return (T) getIntegerFormulaManager().negate((IntegerFormula) args.get(0)); + } else { + return (T) getRationalFormulaManager().negate((NumeralFormula) args.get(0)); + } + case SUB: + Preconditions.checkArgument(args.size() == 2); + if (declaration.getType().isIntegerType()) { + return (T) + getIntegerFormulaManager() + .subtract((IntegerFormula) args.get(0), (IntegerFormula) args.get(1)); + } else { + return (T) + getRationalFormulaManager() + .subtract((NumeralFormula) args.get(0), (NumeralFormula) args.get(1)); + } + case ADD: + if (declaration.getType().isIntegerType()) { + return (T) getIntegerFormulaManager().sum((List) args); + } else { + return (T) getRationalFormulaManager().sum((List) args); + } + case DIV: + Preconditions.checkArgument(args.size() == 2); + if (declaration.getType().isIntegerType()) { + return (T) + getIntegerFormulaManager() + .divide((IntegerFormula) args.get(0), (IntegerFormula) args.get(1)); + } else { + return (T) + getRationalFormulaManager() + .divide((NumeralFormula) args.get(0), (NumeralFormula) args.get(1)); + } + case MUL: + Preconditions.checkArgument(args.size() == 2); + if (declaration.getType().isIntegerType()) { + return (T) + getIntegerFormulaManager() + .multiply((IntegerFormula) args.get(0), (IntegerFormula) args.get(1)); + } else { + return (T) + getRationalFormulaManager() + .multiply((NumeralFormula) args.get(0), (NumeralFormula) args.get(1)); + } + case MODULO: + return (T) + getIntegerFormulaManager() + .modulo((IntegerFormula) args.get(0), (IntegerFormula) args.get(1)); + case LT: + Preconditions.checkArgument(args.size() == 2); + return (T) + getRationalFormulaManager() + .lessThan((NumeralFormula) args.get(0), (NumeralFormula) args.get(1)); + case LTE: + Preconditions.checkArgument(args.size() == 2); + return (T) + getRationalFormulaManager() + .lessOrEquals((NumeralFormula) args.get(0), (NumeralFormula) args.get(1)); + case GT: + Preconditions.checkArgument(args.size() == 2); + return (T) + getRationalFormulaManager() + .greaterThan((NumeralFormula) args.get(0), (NumeralFormula) args.get(1)); + case GTE: + Preconditions.checkArgument(args.size() == 2); + return (T) + getRationalFormulaManager() + .greaterOrEquals((NumeralFormula) args.get(0), (NumeralFormula) args.get(1)); + case EQ: + Preconditions.checkArgument(args.size() == 2); + if (declaration.getArgumentTypes().get(0).isBooleanType()) { + return (T) + getBooleanFormulaManager() + .equivalence((BooleanFormula) args.get(0), (BooleanFormula) args.get(1)); + } else if (declaration.getArgumentTypes().get(1).isNumeralType()) { + if (declaration.getArgumentTypes().get(0).isRationalType() + || declaration.getArgumentTypes().get(1).isRationalType()) { + return (T) + getRationalFormulaManager() + .equal((NumeralFormula) args.get(0), (NumeralFormula) args.get(1)); + } else { + return (T) + getIntegerFormulaManager() + .equal((IntegerFormula) args.get(0), (IntegerFormula) args.get(1)); + } + } else if (declaration.getArgumentTypes().get(0).isStringType()) { + return (T) + getStringFormulaManager() + .equal((StringFormula) args.get(0), (StringFormula) args.get(1)); + + } else if (declaration.getArgumentTypes().get(0).isBitvectorType()) { + return (T) + getBitvectorFormulaManager() + .equal((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + } else if (declaration.getArgumentTypes().get(0).isArrayType()) { + return (T) + getArrayFormulaManager() + .equivalence((ArrayFormula) args.get(0), (ArrayFormula) args.get(1)); + } else { + throw new UnsupportedOperationException( + String.format( + "EQ not supported for theory " + "%s", declaration.getArgumentTypes().get(0))); + } + case EQ_ZERO: + if (args.get(0) instanceof IntegerFormula) { + return (T) + getIntegerFormulaManager() + .equal((IntegerFormula) args.get(0), getIntegerFormulaManager().makeNumber(0)); + } else { + return (T) + getRationalFormulaManager() + .equal((NumeralFormula) args.get(0), getRationalFormulaManager().makeNumber(0)); + } + case GTE_ZERO: + if (args.get(0) instanceof IntegerFormula) { + return (T) + getIntegerFormulaManager() + .greaterOrEquals( + (IntegerFormula) args.get(0), getIntegerFormulaManager().makeNumber(0)); + } else { + return (T) + getRationalFormulaManager() + .greaterOrEquals( + (NumeralFormula) args.get(0), getRationalFormulaManager().makeNumber(0)); + } + case TO_REAL: + return (T) + getRationalFormulaManager().sum(ImmutableList.of((NumeralFormula) args.get(0))); + case FLOOR: + if (args.get(0) instanceof IntegerFormula) { + return (T) getIntegerFormulaManager().floor((IntegerFormula) args.get(0)); + } else { + return (T) getRationalFormulaManager().floor((NumeralFormula) args.get(0)); + } + // FIXME Requires indexed functions + // case INT_TO_BV: + // case BV_EXTRACT: + case BV_CONCAT: + Preconditions.checkArgument(args.size() == 2); + return (T) + getBitvectorFormulaManager() + .concat((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + // FIXME Requires indexed functions + // case BV_SIGN_EXTENSION: + // case BV_ZERO_EXTENSION: + case BV_NOT: + return (T) getBitvectorFormulaManager().not((BitvectorFormula) args.get(0)); + case BV_NEG: + return (T) getBitvectorFormulaManager().negate((BitvectorFormula) args.get(0)); + case BV_OR: + Preconditions.checkArgument(args.size() == 2); + return (T) + getBitvectorFormulaManager() + .or((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_AND: + Preconditions.checkArgument(args.size() == 2); + return (T) + getBitvectorFormulaManager() + .and((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_XOR: + Preconditions.checkArgument(args.size() == 2); + return (T) + getBitvectorFormulaManager() + .xor((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_SUB: + Preconditions.checkArgument(args.size() == 2); + return (T) + getBitvectorFormulaManager() + .subtract((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_ADD: + Preconditions.checkArgument(args.size() == 2); + return (T) + getBitvectorFormulaManager() + .add((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_SDIV: + return (T) + getBitvectorFormulaManager() + .divide((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), true); + case BV_UDIV: + return (T) + getBitvectorFormulaManager() + .divide((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), false); + case BV_SREM: + return (T) + getBitvectorFormulaManager() + .remainder((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), true); + case BV_UREM: + return (T) + getBitvectorFormulaManager() + .remainder((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), false); + case BV_SMOD: + return (T) + getBitvectorFormulaManager() + .smodulo((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_MUL: + Preconditions.checkArgument(args.size() == 2); + return (T) + getBitvectorFormulaManager() + .multiply((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_ULT: + return (T) + getBitvectorFormulaManager() + .lessThan((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), false); + case BV_SLT: + return (T) + getBitvectorFormulaManager() + .lessThan((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), true); + case BV_ULE: + return (T) + getBitvectorFormulaManager() + .lessOrEquals( + (BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), false); + case BV_SLE: + return (T) + getBitvectorFormulaManager() + .lessOrEquals( + (BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), true); + case BV_UGT: + return (T) + getBitvectorFormulaManager() + .greaterThan( + (BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), false); + case BV_SGT: + return (T) + getBitvectorFormulaManager() + .greaterThan( + (BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), true); + case BV_UGE: + return (T) + getBitvectorFormulaManager() + .greaterOrEquals( + (BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), false); + case BV_SGE: + return (T) + getBitvectorFormulaManager() + .greaterOrEquals( + (BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), true); + case BV_EQ: // FIXME Why is this a separate symbol? + Preconditions.checkArgument(args.size() == 2); + return (T) + getBitvectorFormulaManager() + .equal((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_SHL: + return (T) + getBitvectorFormulaManager() + .shiftLeft((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_LSHR: + return (T) + getBitvectorFormulaManager() + .shiftRight( + (BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), false); + case BV_ASHR: + return (T) + getBitvectorFormulaManager() + .shiftRight((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1), true); + case BV_ROTATE_LEFT: + return (T) + getBitvectorFormulaManager() + .rotateLeft((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + case BV_ROTATE_RIGHT: + return (T) + getBitvectorFormulaManager() + .rotateRight((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); + // FIXME Requires indexed functions + // case BV_ROTATE_LEFT_BY_INT: + // case BV_ROTATE_RIGHT_BY_INT: + case BV_UCASTTO_FP: + return (T) + getFloatingPointFormulaManager() + .castFrom(args.get(0), false, (FloatingPointType) declaration.getType()); + case BV_SCASTTO_FP: + return (T) + getFloatingPointFormulaManager() + .castFrom(args.get(0), true, (FloatingPointType) declaration.getType()); + case UBV_TO_INT: + return (T) + getBitvectorFormulaManager().toIntegerFormula((BitvectorFormula) args.get(0), false); + case SBV_TO_INT: + return (T) + getBitvectorFormulaManager().toIntegerFormula((BitvectorFormula) args.get(0), true); + case FP_NEG: + return (T) getFloatingPointFormulaManager().negate((FloatingPointFormula) args.get(0)); + case FP_ABS: + return (T) getFloatingPointFormulaManager().abs((FloatingPointFormula) args.get(0)); + case FP_MAX: + return (T) + getFloatingPointFormulaManager() + .max((FloatingPointFormula) args.get(0), (FloatingPointFormula) args.get(1)); + case FP_MIN: + return (T) + getFloatingPointFormulaManager() + .min((FloatingPointFormula) args.get(0), (FloatingPointFormula) args.get(1)); + case FP_SQRT: + return (T) + getFloatingPointFormulaManager() + .sqrt( + (FloatingPointFormula) args.get(1), + getFloatingPointFormulaManager() + .fromRoundingModeFormula((FloatingPointRoundingModeFormula) args.get(0))); + case FP_SUB: + return (T) + getFloatingPointFormulaManager() + .subtract( + (FloatingPointFormula) args.get(1), + (FloatingPointFormula) args.get(2), + getFloatingPointFormulaManager() + .fromRoundingModeFormula((FloatingPointRoundingModeFormula) args.get(0))); + case FP_ADD: + return (T) + getFloatingPointFormulaManager() + .add( + (FloatingPointFormula) args.get(1), + (FloatingPointFormula) args.get(2), + getFloatingPointFormulaManager() + .fromRoundingModeFormula((FloatingPointRoundingModeFormula) args.get(0))); + case FP_DIV: + return (T) + getFloatingPointFormulaManager() + .divide( + (FloatingPointFormula) args.get(1), + (FloatingPointFormula) args.get(2), + getFloatingPointFormulaManager() + .fromRoundingModeFormula((FloatingPointRoundingModeFormula) args.get(0))); + case FP_REM: + return (T) + getFloatingPointFormulaManager() + .remainder( + (FloatingPointFormula) args.get(0), (FloatingPointFormula) args.get(1)); + case FP_MUL: + return (T) + getFloatingPointFormulaManager() + .multiply( + (FloatingPointFormula) args.get(1), + (FloatingPointFormula) args.get(2), + getFloatingPointFormulaManager() + .fromRoundingModeFormula((FloatingPointRoundingModeFormula) args.get(0))); + case FP_LT: + return (T) + getFloatingPointFormulaManager() + .lessThan((FloatingPointFormula) args.get(0), (FloatingPointFormula) args.get(1)); + case FP_LE: + return (T) + getFloatingPointFormulaManager() + .lessOrEquals( + (FloatingPointFormula) args.get(0), (FloatingPointFormula) args.get(1)); + case FP_GE: + return (T) + getFloatingPointFormulaManager() + .greaterOrEquals( + (FloatingPointFormula) args.get(0), (FloatingPointFormula) args.get(1)); + case FP_GT: + return (T) + getFloatingPointFormulaManager() + .greaterThan( + (FloatingPointFormula) args.get(0), (FloatingPointFormula) args.get(1)); + case FP_EQ: + return (T) + getFloatingPointFormulaManager() + .equalWithFPSemantics( + (FloatingPointFormula) args.get(0), (FloatingPointFormula) args.get(1)); + case FP_ROUND_TO_INTEGRAL: + return (T) + getFloatingPointFormulaManager() + .round( + (FloatingPointFormula) args.get(1), + getFloatingPointFormulaManager() + .fromRoundingModeFormula((FloatingPointRoundingModeFormula) args.get(0))); + case FP_IS_NAN: + return (T) getFloatingPointFormulaManager().isNaN((FloatingPointFormula) args.get(0)); + case FP_IS_INF: + return (T) + getFloatingPointFormulaManager().isInfinity((FloatingPointFormula) args.get(0)); + case FP_IS_ZERO: + return (T) getFloatingPointFormulaManager().isZero((FloatingPointFormula) args.get(0)); + case FP_IS_NEGATIVE: + return (T) + getFloatingPointFormulaManager().isNegative((FloatingPointFormula) args.get(0)); + case FP_IS_SUBNORMAL: + return (T) + getFloatingPointFormulaManager().isSubnormal((FloatingPointFormula) args.get(0)); + case FP_IS_NORMAL: + return (T) getFloatingPointFormulaManager().isNormal((FloatingPointFormula) args.get(0)); + case FP_CASTTO_FP: + return getFloatingPointFormulaManager() + .castTo((FloatingPointFormula) args.get(0), true, declaration.getType()); + case FP_CASTTO_SBV: + return getFloatingPointFormulaManager() + .castTo((FloatingPointFormula) args.get(0), true, declaration.getType()); + case FP_CASTTO_UBV: + return getFloatingPointFormulaManager() + .castTo((FloatingPointFormula) args.get(0), false, declaration.getType()); + case FP_AS_IEEEBV: + return (T) + getFloatingPointFormulaManager().toIeeeBitvector((FloatingPointFormula) args.get(0)); + case FP_FROM_IEEEBV: + return (T) + getFloatingPointFormulaManager() + .fromIeeeBitvector( + (BitvectorFormula) args.get(0), (FloatingPointType) declaration.getType()); + case STR_CONCAT: + Preconditions.checkArgument(args.size() >= 2); + return (T) getStringFormulaManager().concat((List) args); + case STR_PREFIX: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .prefix((StringFormula) args.get(0), (StringFormula) args.get(1)); + case STR_SUFFIX: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .suffix((StringFormula) args.get(0), (StringFormula) args.get(1)); + case STR_CONTAINS: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .contains((StringFormula) args.get(0), (StringFormula) args.get(1)); + case STR_SUBSTRING: + Preconditions.checkArgument(args.size() == 3); + return (T) + getStringFormulaManager() + .substring( + (StringFormula) args.get(0), + (IntegerFormula) args.get(1), + (IntegerFormula) args.get(2)); + case STR_REPLACE: + Preconditions.checkArgument(args.size() == 3); + return (T) + getStringFormulaManager() + .replace( + (StringFormula) args.get(0), + (StringFormula) args.get(1), + (StringFormula) args.get(2)); + case STR_REPLACE_ALL: + Preconditions.checkArgument(args.size() == 3); + return (T) + getStringFormulaManager() + .replaceAll( + (StringFormula) args.get(0), + (StringFormula) args.get(1), + (StringFormula) args.get(2)); + case STR_CHAR_AT: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .charAt((StringFormula) args.get(0), (IntegerFormula) args.get(1)); + case STR_LENGTH: + Preconditions.checkArgument(args.size() == 1); + return (T) getStringFormulaManager().length((StringFormula) args.get(0)); + case STR_INDEX_OF: + Preconditions.checkArgument(args.size() == 3); + return (T) + getStringFormulaManager() + .indexOf( + (StringFormula) args.get(0), + (StringFormula) args.get(1), + (IntegerFormula) args.get(2)); + case STR_TO_RE: + // String to RE injection + // We only support this for constant Strings + Preconditions.checkArgument(args.size() == 1); + String str = + delegate.visit( + args.get(0), + new DefaultFormulaVisitor<>() { + @Override + protected String visitDefault(Formula f) { + throw new IllegalArgumentException( + "We only support constant Strings for str.to_re"); + } + + @Override + public String visitConstant(Formula f, Object value) { + return (String) value; + } + }); + return (T) getStringFormulaManager().makeRegex(str); + case STR_IN_RE: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager().in((StringFormula) args.get(0), (RegexFormula) args.get(1)); + case STR_TO_INT: + Preconditions.checkArgument(args.size() == 1); + return (T) getStringFormulaManager().toIntegerFormula((StringFormula) args.get(0)); + case INT_TO_STR: + Preconditions.checkArgument(args.size() == 1); + return (T) getStringFormulaManager().toStringFormula((IntegerFormula) args.get(0)); + case STR_FROM_CODE: + Preconditions.checkArgument(args.size() == 1); + return (T) getStringFormulaManager().fromCodePoint((IntegerFormula) args.get(0)); + case STR_TO_CODE: + Preconditions.checkArgument(args.size() == 1); + return (T) getStringFormulaManager().toCodePoint((StringFormula) args.get(0)); + case STR_LT: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .lessThan((StringFormula) args.get(0), (StringFormula) args.get(1)); + case STR_LE: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .lessOrEquals((StringFormula) args.get(0), (StringFormula) args.get(1)); + case RE_NONE: + Preconditions.checkArgument(args.isEmpty()); + return (T) getStringFormulaManager().none(); + case RE_PLUS: + Preconditions.checkArgument(args.size() == 1); + return (T) getStringFormulaManager().cross((RegexFormula) args.get(0)); + case RE_STAR: + Preconditions.checkArgument(args.size() == 1); + return (T) getStringFormulaManager().closure((RegexFormula) args.get(0)); + case RE_OPTIONAL: + Preconditions.checkArgument(args.size() == 1); + return (T) getStringFormulaManager().optional((RegexFormula) args.get(0)); + case RE_CONCAT: + Preconditions.checkArgument(args.size() >= 2); + return (T) getStringFormulaManager().concatRegex((List) args); + case RE_UNION: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .union((RegexFormula) args.get(0), (RegexFormula) args.get(1)); + case RE_RANGE: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .range((StringFormula) args.get(0), (StringFormula) args.get(1)); + case RE_INTERSECT: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .intersection((RegexFormula) args.get(0), (RegexFormula) args.get(1)); + case RE_COMPLEMENT: + Preconditions.checkArgument(args.size() == 1); + return (T) getStringFormulaManager().complement((RegexFormula) args.get(0)); + case RE_DIFFERENCE: + Preconditions.checkArgument(args.size() == 2); + return (T) + getStringFormulaManager() + .difference((RegexFormula) args.get(0), (RegexFormula) args.get(1)); + case SEP_EMP: + Preconditions.checkArgument(args.size() == 2); + return (T) + getSLFormulaManager() + .makeEmptyHeap( + (FormulaType) args.get(0), + (FormulaType) args.get(1)); + case SEP_NIL: + Preconditions.checkArgument(args.size() == 1); + return (T) + getSLFormulaManager().makeNilElement((FormulaType) args.get(0)); + case SEP_PTO: + Preconditions.checkArgument(args.size() == 2); + return (T) + getSLFormulaManager().makePointsTo((Formula) args.get(0), (Formula) args.get(1)); + case SEP_STAR: + Preconditions.checkArgument(args.size() == 2); + return (T) + getSLFormulaManager() + .makeStar((BooleanFormula) args.get(0), (BooleanFormula) args.get(1)); + case SEP_WAND: + Preconditions.checkArgument(args.size() == 2); + return (T) + getSLFormulaManager() + .makeMagicWand((BooleanFormula) args.get(0), (BooleanFormula) args.get(1)); + // TODO + // case OTHER: + default: + throw new UnsupportedOperationException( + String.format( + "Operation not supported: %s, (%s)", + declaration.getKind(), declaration.getName())); + } + } + } + + @Override + public T makeApplication( + FunctionDeclaration declaration, Formula... args) { + return makeApplication(declaration, ImmutableList.copyOf(args)); + } + + @Override + public FormulaType getFormulaType(T formula) { + return logger.logDefDiscard( + "mgr", + String.format("getFormulaType(%s)", logger.toVariable(formula)), + () -> delegate.getFormulaType(formula)); + } + + @Override + public BooleanFormula parse(String s) throws IllegalArgumentException { + return rebuild( + logger.logDefDiscard( + "mgr", String.format("parse(%s)", logger.printString(s)), () -> delegate.parse(s))); + } + + @Override + public Appender dumpFormula(BooleanFormula pT) { + return logger.logDefDiscard( + "mgr", + String.format("dumpFormula(%s)", logger.toVariable(pT)), + () -> delegate.dumpFormula(pT)); + } + + @Override + public BooleanFormula applyTactic(BooleanFormula input, Tactic tactic) + throws InterruptedException, SolverException { + return rebuild( + logger.logDefDiscard( + "mgr", + String.format( + "applyTactic(%s, %s)", logger.toVariable(input), "Tactic." + tactic.name()), + () -> delegate.applyTactic(input, tactic))); + } + + @Override + public T simplify(T input) throws InterruptedException { + return rebuild( + logger.logDefDiscard( + "mgr", + String.format("simplify(%s)", logger.toVariable(input)), + () -> delegate.simplify(input))); + } + + @Override + public R visit(Formula f, FormulaVisitor rFormulaVisitor) { + return logger.logDefDiscard( + "mgr", + String.format( + "visit(%s, new DefaultFormulaVisitor<>() {" + + "protected Formula visitDefault(Formula f) {" + + "return f;" + + "}})", + logger.toVariable(f)), + () -> delegate.visit(f, rFormulaVisitor)); + } + + @Override + public void visitRecursively(Formula f, FormulaVisitor rFormulaVisitor) { + logger.logStmtDiscard( + "mgr", + String.format( + "visitRecursively(%s, new DefaultFormulaVisitor<>() {" + + "protected TraversalProcess visitDefault(Formula f) {" + + "return TraversalProcess.CONTINUE;" + + "}})", + logger.toVariable(f)), + () -> delegate.visitRecursively(f, rFormulaVisitor)); + } + + @Override + public T transformRecursively( + T f, FormulaTransformationVisitor pFormulaVisitor) { + return logger.logDefDiscard( + "mgr", + String.format( + "transformRecursively(%s, new FormulaTransformationVisitor(%s) {})", + logger.toVariable(f), "mgr"), + () -> delegate.transformRecursively(f, pFormulaVisitor)); + } + + @Override + public ImmutableMap extractVariables(Formula f) { + return logger.logDefDiscard( + "mgr", + String.format("extractVariables(%s)", logger.toVariable(f)), + () -> delegate.extractVariables(f)); + } + + @Override + public ImmutableMap extractVariablesAndUFs(Formula f) { + return logger.logDefDiscard( + "mgr", + String.format("extractVariablesAndUFs(%s)", logger.toVariable(f)), + () -> delegate.extractVariablesAndUFs(f)); + } + + @Override + public T substitute( + T f, Map fromToMapping) { + return rebuild( + logger.logDefDiscard( + "mgr", + String.format( + "substitute(%s, ImmutableMap.ofEntries(%s))", + logger.toVariable(f), + FluentIterable.from(fromToMapping.entrySet()) + .transform( + entry -> + String.format( + "Map.entry(%s, %s)", + logger.toVariable(entry.getKey()), + logger.toVariable(entry.getValue()))) + .join(Joiner.on(", "))), + () -> delegate.substitute(f, fromToMapping))); + } + + @Override + public BooleanFormula translateFrom(BooleanFormula formula, FormulaManager otherManager) { + // TODO Write API calls from all contexts into one file to allow us to support this method + throw new UnsupportedOperationException(); + } + + @Override + public boolean isValidName(String variableName) { + return delegate.isValidName(variableName); + } + + @Override + public String escape(String variableName) { + return delegate.escape(variableName); + } + + @Override + public String unescape(String variableName) { + return delegate.unescape(variableName); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceIntegerFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceIntegerFormulaManager.java new file mode 100644 index 0000000000..f7cf7b93bb --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceIntegerFormulaManager.java @@ -0,0 +1,59 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import java.math.BigInteger; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; + +public class TraceIntegerFormulaManager + extends TraceNumeralFormulaManager + implements IntegerFormulaManager { + private final IntegerFormulaManager delegate; + private final TraceLogger logger; + + TraceIntegerFormulaManager(IntegerFormulaManager pDelegate, TraceLogger pLogger) { + super(pDelegate, pLogger); + delegate = pDelegate; + logger = pLogger; + } + + @Override + public BooleanFormula modularCongruence( + IntegerFormula number1, IntegerFormula number2, BigInteger n) { + return logger.logDef( + "mgr.getIntegerFormulaManager()", + String.format( + "modularCongruence(%s, %s, new BigInteger(\"%s\"))", + logger.toVariable(number1), logger.toVariable(number2), n), + () -> delegate.modularCongruence(number1, number2, n)); + } + + @Override + public BooleanFormula modularCongruence(IntegerFormula number1, IntegerFormula number2, long n) { + return logger.logDef( + "mgr.getIntegerFormulaManager()", + String.format( + "modularCongruence(%s, %s, %s)", + logger.toVariable(number1), logger.toVariable(number2), n), + () -> delegate.modularCongruence(number1, number2, n)); + } + + @Override + public IntegerFormula modulo(IntegerFormula numerator, IntegerFormula denominator) { + return logger.logDef( + "mgr.getIntegerFormulaManager()", + String.format( + "modulo(%s, %s)", logger.toVariable(numerator), logger.toVariable(denominator)), + () -> delegate.modulo(numerator, denominator)); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceInterpolatingProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceInterpolatingProverEnvironment.java new file mode 100644 index 0000000000..e825aab60b --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceInterpolatingProverEnvironment.java @@ -0,0 +1,80 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import com.google.common.base.Joiner; +import com.google.common.collect.FluentIterable; +import java.util.Arrays; +import java.util.Collection; +import java.util.List; +import java.util.Objects; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.SolverException; + +public class TraceInterpolatingProverEnvironment extends TraceBasicProverEnvironment + implements InterpolatingProverEnvironment { + private final InterpolatingProverEnvironment delegate; + private final TraceFormulaManager mgr; + private final TraceLogger logger; + + TraceInterpolatingProverEnvironment( + InterpolatingProverEnvironment pDelegate, + TraceFormulaManager pFormulaManager, + TraceLogger pLogger) { + super(pDelegate, pFormulaManager, pLogger); + delegate = pDelegate; + mgr = pFormulaManager; + logger = pLogger; + } + + @Override + public List getSeqInterpolants(List> partitionedFormulas) + throws SolverException, InterruptedException { + return mgr.rebuildAll( + logger.logDefDiscard( + logger.toVariable(this), + String.format( + "getSeqInterpolant(ImmutableList.of(%s))", + FluentIterable.from(partitionedFormulas) + .transform(p -> String.format("ImmutableList.of(%s)", logger.toVariables(p))) + .join(Joiner.on(", "))), + () -> delegate.getSeqInterpolants(partitionedFormulas))); + } + + @Override + public BooleanFormula getInterpolant(Collection formulasOfA) + throws SolverException, InterruptedException { + return mgr.rebuild( + logger.logDefDiscard( + logger.toVariable(this), + String.format("getInterpolant(ImmutableList.of(%s))", logger.toVariables(formulasOfA)), + () -> delegate.getInterpolant(formulasOfA))); + } + + @Override + public List getTreeInterpolants( + List> partitionedFormulas, int[] startOfSubTree) + throws SolverException, InterruptedException { + return mgr.rebuildAll( + logger.logDefDiscard( + logger.toVariable(this), + String.format( + "getTreeInterpolant(ImmutableList.of(%s), new int[]{%s})", + FluentIterable.from(partitionedFormulas) + .transform(p -> String.format("ImmutableList.of(%s)", logger.toVariables(p))) + .join(Joiner.on(", ")), + FluentIterable.from(Arrays.stream(startOfSubTree).boxed().toArray()) + .transform(Objects::toString) + .join(Joiner.on(", "))), + () -> delegate.getTreeInterpolants(partitionedFormulas, startOfSubTree))); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceLogger.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceLogger.java new file mode 100644 index 0000000000..ce6a3d3f42 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceLogger.java @@ -0,0 +1,306 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import com.google.common.base.Joiner; +import com.google.common.base.Preconditions; +import com.google.common.collect.FluentIterable; +import java.io.File; +import java.io.IOException; +import java.io.RandomAccessFile; +import java.nio.charset.StandardCharsets; +import java.util.ArrayDeque; +import java.util.Deque; +import java.util.HashMap; +import java.util.Map; +import java.util.concurrent.Callable; +import org.sosy_lab.common.UniqueIdGenerator; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; +import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; + +class TraceLogger { + private final TraceFormulaManager mgr; + private final UniqueIdGenerator id = new UniqueIdGenerator(); + + private final Map valueMap = new HashMap<>(); + private final RandomAccessFile output; + + /** + * Contains lines that were recently added to the log. Entries on this list are preliminary and + * can still be removed from the final trace + */ + private final Deque lastLines = new ArrayDeque<>(); + + TraceLogger(TraceFormulaManager pMgr, File pFile) { + mgr = pMgr; + mgr.setLogger(this); + + // FIXME Check if the file already exists -> quite unlikely, lets ignore this case. + try { + output = new RandomAccessFile(pFile, "rw"); + } catch (IOException e) { + throw new IllegalArgumentException(e); + } + } + + /** Returns a fresh variable. */ + public String newVariable() { + return "var" + id.getFreshId(); + } + + /** + * Bind an object to a variable. + * + *

Use {@link #toVariable(Object)} to get the variable name for a tracked object + */ + public void mapVariable(String pVar, Object f) { + valueMap.putIfAbsent(f, pVar); + } + + /** Returns true if the object is tracked. */ + public boolean isTracked(Object f) { + return valueMap.containsKey(f); + } + + /** + * Returns the variable name of a tracked object. + * + *

Use {@link #mapVariable(String, Object)} to bind an object to a variable + */ + public String toVariable(Object f) { + String r = valueMap.get(f); + Preconditions.checkArgument(r != null, "Object not tracked: %s", f); + return r; + } + + /** Returns a comma-separated list of variable names for the given objects. */ + public String toVariables(Iterable objects) { + return FluentIterable.from(objects).transform(this::toVariable).join(Joiner.on(", ")); + } + + /** Add a definition of a new object to the log. */ + public void appendDef(String pVar, String pExpr) { + try { + lastLines.push(output.length()); + output.write(String.format("var %s = %s;%n", pVar, pExpr).getBytes(StandardCharsets.UTF_8)); + } catch (IOException e) { + throw new RuntimeException(e); + } + } + + /** Add a statement to the log. */ + public void appendStmt(String pStmt) { + try { + lastLines.push(output.length()); + output.write(String.format("%s;%n", pStmt).getBytes(StandardCharsets.UTF_8)); + } catch (IOException e) { + throw new RuntimeException(e); + } + } + + /** Undo the last line and remove it from the trace. */ + public void undoLast() { + Preconditions.checkArgument( + !lastLines.isEmpty(), "Cannot undo last trace, no undo points found"); + try { + var start = lastLines.pop(); + output.seek(start); + var line = output.readLine(); + if (start + line.length() + 1 == output.length()) { + // We need to remove the last line of the trace + // Just truncate the file + output.setLength(start); + } else { + // We need to remove a line somewhere in the middle + // Just overwrite it with whitespace to avoid having to move rest of the file around + output.seek(start); + output.write( + String.format("%s%n", " ".repeat(line.length())).getBytes(StandardCharsets.UTF_8)); + output.seek(output.length()); + } + } catch (IOException e) { + throw new RuntimeException(e); + } + } + + /** Remove an undo point and permanently commit the line to the trace. */ + public void keepLast() { + Preconditions.checkArgument( + !lastLines.isEmpty(), "Cannot remove undo point, list is already empty"); + lastLines.pop(); + } + + @SuppressWarnings("unchecked") + public static void sneakyThrow(Throwable e) throws E { + throw (E) e; + } + + /** Log an API call with return value. */ + public R logDef(String prefix, String method, Callable closure) { + String var = newVariable(); + try { + appendDef(var, prefix + "." + method); + R f = closure.call(); + if (isTracked(f)) { + undoLast(); + return f; + } else { + keepLast(); + mapVariable(var, f); + return mgr.rebuild(f); + } + } catch (Exception e) { + sneakyThrow(e); + throw new RuntimeException(e); + } + } + + /** + * Variant of {@link #logDef(String, String, Callable)} that will always keep the call in the log. + * + *

Use this version if the called function has side effects + */ + public R logDefKeep(String prefix, String method, Callable closure) { + String var = newVariable(); + try { + appendDef(var, prefix + "." + method); + R f = closure.call(); + keepLast(); + mapVariable(var, f); + return f; + } catch (Exception e) { + sneakyThrow(e); + throw new RuntimeException(e); + } + } + + /** + * Variant of {@link #logDef(String, String, Callable)} that will always remove the call from the + * log after it returned successfully. + */ + public R logDefDiscard(String prefix, String method, Callable closure) { + String var = newVariable(); + try { + appendDef(var, prefix + "." + method); + R f = closure.call(); + undoLast(); + return f; + } catch (Exception e) { + sneakyThrow(e); + throw new RuntimeException(e); + } + } + + /** Just like {@link Runnable}, but allows checked exceptions. */ + public interface CheckedRunnable { + void run() throws Exception; + } + + /** Log an API call without return value. */ + public void logStmt(String prefix, String method, CheckedRunnable closure) { + try { + appendStmt(prefix + "." + method); + closure.run(); + keepLast(); + } catch (Exception e) { + sneakyThrow(e); + } + } + + /** + * Variant of {@link #logStmt(String, String, CheckedRunnable)} that will remove the call from the + * log after it returned successfully. + */ + public void logStmtDiscard(String prefix, String method, CheckedRunnable closure) { + try { + appendStmt(prefix + "." + method); + closure.run(); + undoLast(); + } catch (Exception e) { + sneakyThrow(e); + } + } + + /** + * Print a String for the trace. + * + *

Adds quotes around the literal and escapes special characters. + */ + public String printString(String pString) { + StringBuilder builder = new StringBuilder(); + builder.append("\""); + for (var c : pString.codePoints().toArray()) { + switch (c) { + case '\'': + builder.append("\\'"); + break; + case '"': + builder.append("\\\""); + break; + case '\\': + builder.append("\\\\"); + break; + case '\n': + builder.append("\\n"); + break; + case '\t': + builder.append("\\t"); + break; + default: + builder.appendCodePoint(c); + } + } + builder.append("\""); + return builder.toString(); + } + + /** + * Print a {@link org.sosy_lab.java_smt.api.FormulaType} for the trace. + * + *

Returns a Java expression that will construct the type. + */ + public String printFormulaType(FormulaType pType) { + if (pType.isBooleanType()) { + return "FormulaType.BooleanType"; + } + if (pType.isIntegerType()) { + return "FormulaType.IntegerType"; + } + if (pType.isRationalType()) { + return "FormulaType.RationalType"; + } + if (pType.isArrayType()) { + ArrayFormulaType arrayType = (ArrayFormulaType) pType; + return String.format( + "FormulaType.getArrayType(%s, %s)", + printFormulaType(arrayType.getIndexType()), printFormulaType(arrayType.getElementType())); + } + if (pType.isBitvectorType()) { + BitvectorType bvType = (BitvectorType) pType; + return String.format("FormulaType.getBitvectorTypeWithSize(%s)", bvType.getSize()); + } + if (pType.isFloatingPointType()) { + FloatingPointType fpType = (FloatingPointType) pType; + return String.format( + "FormulaType.getFloatingPointType(%s, %s)", + fpType.getExponentSize(), fpType.getMantissaSize()); + } + if (pType.isStringType()) { + return "FormulaType.StringType"; + } + // FIXME Handle other cases + throw new IllegalArgumentException( + String.format("Unsupported formula type %s of class %s.", pType, pType.getClass())); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceModel.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceModel.java new file mode 100644 index 0000000000..f373625958 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceModel.java @@ -0,0 +1,142 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableList; +import java.math.BigInteger; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.EnumerationFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.StringFormula; + +public class TraceModel implements Model { + private final Model delegate; + + private final TraceFormulaManager mgr; + private final TraceLogger logger; + + TraceModel(Model pDelegate, TraceFormulaManager pMgr, TraceLogger pLogger) { + delegate = pDelegate; + mgr = pMgr; + logger = pLogger; + } + + @Override + public ImmutableList asList() { + logger.appendStmt(String.format("%s.asList()", logger.toVariable(this))); + ImmutableList result = delegate.asList(); + logger.undoLast(); + return FluentIterable.from(result) + // TODO Fix this in the Z3 model + .filter((ValueAssignment assignment) -> !assignment.getName().startsWith("#")) + .transform( + (ValueAssignment assigment) -> { + var key = mgr.rebuild(assigment.getKey()); + var val = mgr.rebuild(assigment.getValueAsFormula()); + var map = mgr.rebuild(assigment.getAssignmentAsFormula()); + return new ValueAssignment( + key, + val, + map, + assigment.getName(), + assigment.getValue(), + assigment.getArgumentsInterpretation()); + }) + .toList(); + } + + @Override + public @Nullable T eval(T formula) { + return mgr.rebuild( + logger.logDefDiscard( + logger.toVariable(this), + String.format("eval(%s)", logger.toVariable(formula)), + () -> delegate.eval(formula))); + } + + @Override + public @Nullable Object evaluate(Formula formula) { + return logger.logDefDiscard( + logger.toVariable(this), + String.format("evaluate(%s)", logger.toVariable(formula)), + () -> delegate.evaluate(formula)); + } + + @Override + public @Nullable BigInteger evaluate(IntegerFormula formula) { + return logger.logDefDiscard( + logger.toVariable(this), + String.format("evaluate(%s)", logger.toVariable(formula)), + () -> delegate.evaluate(formula)); + } + + @Override + public @Nullable Rational evaluate(RationalFormula formula) { + return logger.logDefDiscard( + logger.toVariable(this), + String.format("evaluate(%s)", logger.toVariable(formula)), + () -> delegate.evaluate(formula)); + } + + @Override + public @Nullable Boolean evaluate(BooleanFormula formula) { + return logger.logDefDiscard( + logger.toVariable(this), + String.format("evaluate(%s)", logger.toVariable(formula)), + () -> delegate.evaluate(formula)); + } + + @Override + public @Nullable BigInteger evaluate(BitvectorFormula formula) { + return logger.logDefDiscard( + logger.toVariable(this), + String.format("evaluate(%s)", logger.toVariable(formula)), + () -> delegate.evaluate(formula)); + } + + @Override + public @Nullable String evaluate(StringFormula formula) { + return logger.logDefDiscard( + logger.toVariable(this), + String.format("evaluate(%s)", logger.toVariable(formula)), + () -> delegate.evaluate(formula)); + } + + @Override + public @Nullable String evaluate(EnumerationFormula formula) { + return logger.logDefDiscard( + logger.toVariable(this), + String.format("evaluate(%s)", logger.toVariable(formula)), + () -> delegate.evaluate(formula)); + } + + @Override + public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) { + return logger.logDefDiscard( + logger.toVariable(this), + String.format("evaluate(%s)", logger.toVariable(formula)), + () -> delegate.evaluate(formula)); + } + + @Override + public void close() { + logger.logStmt(logger.toVariable(this), "close()", delegate::close); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceNumeralFormulaManager.java new file mode 100644 index 0000000000..7f85da6839 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceNumeralFormulaManager.java @@ -0,0 +1,199 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import java.math.BigDecimal; +import java.math.BigInteger; +import java.util.List; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.NumeralFormulaManager; + +@SuppressWarnings("ClassTypeParameterName") +public abstract class TraceNumeralFormulaManager< + ParamFormulaType extends NumeralFormula, ResultFormulaType extends NumeralFormula> + implements NumeralFormulaManager { + private final NumeralFormulaManager delegate; + private final TraceLogger logger; + + TraceNumeralFormulaManager( + NumeralFormulaManager pDelegate, TraceLogger pLogger) { + delegate = pDelegate; + logger = pLogger; + } + + private String getPrefix() { + return getFormulaType().equals(FormulaType.IntegerType) + ? "mgr.getIntegerFormulaManager()" + : "mgr.getRationalFormulaManager()"; + } + + @Override + public ResultFormulaType makeNumber(long number) { + return logger.logDef( + getPrefix(), String.format("makeNumber(%s)", number), () -> delegate.makeNumber(number)); + } + + @Override + public ResultFormulaType makeNumber(BigInteger number) { + return logger.logDef( + getPrefix(), + String.format("makeNumber(new BigInteger(\"%s\"))", number), + () -> delegate.makeNumber(number)); + } + + @Override + public ResultFormulaType makeNumber(double number) { + return logger.logDef( + getPrefix(), String.format("makeNumber(%s)", number), () -> delegate.makeNumber(number)); + } + + @Override + public ResultFormulaType makeNumber(BigDecimal number) { + return logger.logDef( + getPrefix(), + String.format("makeNumber(new BigInteger(\"%s\"))", number), + () -> delegate.makeNumber(number)); + } + + @Override + public ResultFormulaType makeNumber(String pI) { + return logger.logDef( + getPrefix(), String.format("makeNumber(\"%s\")", pI), () -> delegate.makeNumber(pI)); + } + + @Override + public ResultFormulaType makeNumber(Rational pRational) { + return logger.logDef( + getPrefix(), + String.format("makeNumber(Rational.of(\"%s\"))", pRational), + () -> delegate.makeNumber(pRational)); + } + + @Override + public ResultFormulaType makeVariable(String pVar) { + return logger.logDef( + getPrefix(), + String.format("makeVariable(%s)", logger.printString(pVar)), + () -> delegate.makeVariable(pVar)); + } + + @Override + public ResultFormulaType negate(ParamFormulaType number) { + return logger.logDef( + getPrefix(), + String.format("negate(%s)", logger.toVariable(number)), + () -> delegate.negate(number)); + } + + @Override + public ResultFormulaType add(ParamFormulaType number1, ParamFormulaType number2) { + return logger.logDef( + getPrefix(), + String.format("add(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.add(number1, number2)); + } + + @Override + public ResultFormulaType sum(List operands) { + return logger.logDef( + getPrefix(), + String.format("sum(%s)", logger.toVariables(operands)), + () -> delegate.sum(operands)); + } + + @Override + public ResultFormulaType subtract(ParamFormulaType number1, ParamFormulaType number2) { + return logger.logDef( + getPrefix(), + String.format("subtract(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.subtract(number1, number2)); + } + + @Override + public ResultFormulaType divide(ParamFormulaType numerator, ParamFormulaType denominator) { + return logger.logDef( + getPrefix(), + String.format( + "divide(%s, %s)", logger.toVariable(numerator), logger.toVariable(denominator)), + () -> delegate.divide(numerator, denominator)); + } + + @Override + public ResultFormulaType multiply(ParamFormulaType number1, ParamFormulaType number2) { + return logger.logDef( + getPrefix(), + String.format("multiply(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.multiply(number1, number2)); + } + + @Override + public BooleanFormula equal(ParamFormulaType number1, ParamFormulaType number2) { + return logger.logDef( + getPrefix(), + String.format("equal(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.equal(number1, number2)); + } + + @Override + public BooleanFormula distinct(List pNumbers) { + return logger.logDef( + getPrefix(), + String.format("distinct(%s)", logger.toVariables(pNumbers)), + () -> delegate.distinct(pNumbers)); + } + + @Override + public BooleanFormula greaterThan(ParamFormulaType number1, ParamFormulaType number2) { + return logger.logDef( + getPrefix(), + String.format( + "greaterThan(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.greaterThan(number1, number2)); + } + + @Override + public BooleanFormula greaterOrEquals(ParamFormulaType number1, ParamFormulaType number2) { + return logger.logDef( + getPrefix(), + String.format( + "greaterOrEquals(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.greaterOrEquals(number1, number2)); + } + + @Override + public BooleanFormula lessThan(ParamFormulaType number1, ParamFormulaType number2) { + return logger.logDef( + getPrefix(), + String.format("lessThan(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.lessThan(number1, number2)); + } + + @Override + public BooleanFormula lessOrEquals(ParamFormulaType number1, ParamFormulaType number2) { + return logger.logDef( + getPrefix(), + String.format( + "lessOrEquals(%s, %s)", logger.toVariable(number1), logger.toVariable(number2)), + () -> delegate.lessOrEquals(number1, number2)); + } + + @Override + public IntegerFormula floor(ParamFormulaType formula) { + return logger.logDef( + getPrefix(), + String.format("floor(%s)", logger.toVariable(formula)), + () -> delegate.floor(formula)); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceProverEnvironment.java new file mode 100644 index 0000000000..ec11ef5710 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceProverEnvironment.java @@ -0,0 +1,24 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import org.sosy_lab.java_smt.api.BasicProverEnvironment; +import org.sosy_lab.java_smt.api.ProverEnvironment; + +public class TraceProverEnvironment extends TraceBasicProverEnvironment + implements ProverEnvironment { + TraceProverEnvironment( + BasicProverEnvironment pDelegate, + TraceFormulaManager pFormulaManager, + TraceLogger pLogger) { + super(pDelegate, pFormulaManager, pLogger); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceQuantifiedFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceQuantifiedFormulaManager.java new file mode 100644 index 0000000000..d8df985975 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceQuantifiedFormulaManager.java @@ -0,0 +1,52 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2025 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.delegate.trace; + +import static com.google.common.base.Preconditions.checkNotNull; + +import java.util.List; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager; +import org.sosy_lab.java_smt.api.SolverException; + +public class TraceQuantifiedFormulaManager implements QuantifiedFormulaManager { + + private final QuantifiedFormulaManager delegate; + private final TraceLogger logger; + + TraceQuantifiedFormulaManager(QuantifiedFormulaManager pDelegate, TraceLogger pLogger) { + delegate = checkNotNull(pDelegate); + logger = checkNotNull(pLogger); + } + + private String printQuantifier(Quantifier pQuantifier) { + return "QuantifiedFormulaManager.Quantifier." + pQuantifier.name(); + } + + @Override + public BooleanFormula mkQuantifier( + Quantifier q, List pVariables, BooleanFormula pBody) { + return logger.logDef( + "mgr.getQuantifiedFormulaManager()", + String.format( + "mkQuantifier(%s, List.of(%s), %s)", + printQuantifier(q), logger.toVariables(pVariables), logger.toVariable(pBody)), + () -> delegate.mkQuantifier(q, pVariables, pBody)); + } + + @Override + public BooleanFormula eliminateQuantifiers(BooleanFormula pF) + throws InterruptedException, SolverException { + return logger.logDef( + "mgr.getQuantifiedFormulaManager()", + String.format("eliminateQuantifiers(%s)", logger.toVariable(pF)), + () -> delegate.eliminateQuantifiers(pF)); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceRationalFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceRationalFormulaManager.java new file mode 100644 index 0000000000..5883f2fb45 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceRationalFormulaManager.java @@ -0,0 +1,28 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.RationalFormulaManager; + +public class TraceRationalFormulaManager + extends TraceNumeralFormulaManager + implements RationalFormulaManager { + final RationalFormulaManager delegate; + final TraceLogger logger; + + TraceRationalFormulaManager(RationalFormulaManager pDelegate, TraceLogger pLogger) { + super(pDelegate, pLogger); + delegate = pDelegate; + logger = pLogger; + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceSLFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceSLFormulaManager.java new file mode 100644 index 0000000000..a458eb0815 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceSLFormulaManager.java @@ -0,0 +1,75 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2025 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.delegate.trace; + +import static com.google.common.base.Preconditions.checkNotNull; + +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.SLFormulaManager; + +@SuppressWarnings("MethodTypeParameterName") +public class TraceSLFormulaManager implements SLFormulaManager { + + private final SLFormulaManager delegate; + private final TraceLogger logger; + + TraceSLFormulaManager(SLFormulaManager pDelegate, TraceLogger pLogger) { + delegate = checkNotNull(pDelegate); + logger = checkNotNull(pLogger); + } + + @Override + public BooleanFormula makeStar(BooleanFormula f1, BooleanFormula f2) { + return logger.logDef( + "mgr.getSLFormulaManager()", + String.format("makeStar(%s, %s)", logger.toVariable(f1), logger.toVariable(f2)), + () -> delegate.makeStar(f1, f2)); + } + + @Override + public BooleanFormula makePointsTo(AF ptr, VF to) { + return logger.logDef( + "mgr.getSLFormulaManager()", + String.format("makePointsTo(%s, %s)", logger.toVariable(ptr), logger.toVariable(to)), + () -> delegate.makePointsTo(ptr, to)); + } + + @Override + public BooleanFormula makeMagicWand(BooleanFormula f1, BooleanFormula f2) { + return logger.logDef( + "mgr.getSLFormulaManager()", + String.format("makeMagicWand(%s, %s)", logger.toVariable(f1), logger.toVariable(f2)), + () -> delegate.makeMagicWand(f1, f2)); + } + + @Override + public < + AF extends Formula, + VF extends Formula, + AT extends FormulaType, + VT extends FormulaType> + BooleanFormula makeEmptyHeap(AT pAddressType, VT pValueType) { + return logger.logDef( + "mgr.getSLFormulaManager()", + String.format( + "makeEmptyHeap(%s, %s)", + logger.printFormulaType(pAddressType), logger.printFormulaType(pValueType)), + () -> delegate.makeEmptyHeap(pAddressType, pValueType)); + } + + @Override + public > AF makeNilElement(AT pAddressType) { + return logger.logDef( + "mgr.getSLFormulaManager()", + String.format("makeNilElement(%s)", logger.printFormulaType(pAddressType)), + () -> delegate.makeNilElement(pAddressType)); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceSolverContext.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceSolverContext.java new file mode 100644 index 0000000000..c86c614088 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceSolverContext.java @@ -0,0 +1,158 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import com.google.common.base.Joiner; +import com.google.common.base.Splitter; +import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableMap; +import com.google.common.io.MoreFiles; +import java.io.IOException; +import java.nio.file.Path; +import java.util.List; +import java.util.Map.Entry; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.FileOption; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.configuration.Option; +import org.sosy_lab.common.configuration.Options; +import org.sosy_lab.common.io.PathTemplate; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext; + +@Options +public class TraceSolverContext implements SolverContext { + private final SolverContext delegate; + private final TraceLogger logger; + private final TraceFormulaManager mgr; + + @Option( + secure = true, + name = "solver.tracefile", + description = "Export solver interaction as Java code into a file.") + @FileOption(FileOption.Type.OUTPUT_FILE) + private @Nullable PathTemplate tracefileTemplate = + PathTemplate.ofFormatString("traces/trace_%s.java"); + + public TraceSolverContext(Solvers pSolver, Configuration config, SolverContext pDelegate) + throws InvalidConfigurationException { + config.inject(this); + delegate = pDelegate; + mgr = new TraceFormulaManager(delegate.getFormulaManager()); + + // initialize the trace logger and create the trace file, + // nanotime is used to avoid collisions, and it is sorted by time. + final Path tracefile = tracefileTemplate.getPath(String.valueOf(System.nanoTime())); + try { + MoreFiles.createParentDirectories(tracefile); + } catch (IOException e) { + throw new InvalidConfigurationException("Could not create directory for trace files", e); + } + logger = new TraceLogger(mgr, tracefile.toFile()); + + this.initializeJavaSMT(config, pSolver); + } + + /** Write the header code for using JavaSMT, e.g., to initialize the context and solver. */ + private void initializeJavaSMT(Configuration config, Solvers pSolver) { + // Get relevant options from the configuration + String props = config.asPropertiesString(); + ImmutableMap.Builder options = ImmutableMap.builder(); + for (String s : props.lines().toArray(String[]::new)) { + List parts = Splitter.on(" = ").splitToList(s); + if (parts.get(0).startsWith("solver") + && !parts.get(0).equals("solver.trace") + && !parts.get(0).equals("solver.solver")) { + options.put(parts.get(0), parts.get(1)); + } + } + + // Write code for creating a solver context to the trace log + logger.appendDef( + "config", + "Configuration.builder()" + + FluentIterable.from(options.buildOrThrow().entrySet()) + .transform( + (Entry e) -> + String.format(".setOption(\"%s\", \"%s\")", e.getKey(), e.getValue())) + .join(Joiner.on("")) + + ".build()"); + logger.appendDef("logger", "LogManager.createNullLogManager()"); + logger.appendDef("notifier", "ShutdownNotifier.createDummy()"); + logger.appendDef( + "context", + "SolverContextFactory.createSolverContext(config, logger, notifier, " + + "SolverContextFactory.Solvers." + + pSolver.name() + + ")"); + logger.appendDef("mgr", "context.getFormulaManager()"); + } + + @Override + public FormulaManager getFormulaManager() { + return mgr; + } + + @SuppressWarnings("resource") + @Override + public ProverEnvironment newProverEnvironment(ProverOptions... options) { + return logger.logDefKeep( + "context", + String.format( + "newProverEnvironment(%s)", + FluentIterable.from(options) + .transform(v -> "SolverContext.ProverOptions." + v.name()) + .join(Joiner.on(", "))), + () -> new TraceProverEnvironment(delegate.newProverEnvironment(options), mgr, logger)); + } + + @SuppressWarnings("resource") + @Override + public InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( + ProverOptions... options) { + return logger.logDefKeep( + "context", + String.format( + "newProverEnvironmentWithInterpolation(%s)", + FluentIterable.from(options) + .transform(v -> "SolverContext.ProverOptions." + v.name()) + .join(Joiner.on(", "))), + () -> + new TraceInterpolatingProverEnvironment<>( + delegate.newProverEnvironmentWithInterpolation(options), mgr, logger)); + } + + @SuppressWarnings("resource") + @Override + public OptimizationProverEnvironment newOptimizationProverEnvironment(ProverOptions... options) { + throw new UnsupportedOperationException(); + } + + @Override + public String getVersion() { + return logger.logDefDiscard("context", "getVersion()", delegate::getVersion); + } + + @Override + public Solvers getSolverName() { + return delegate.getSolverName(); + } + + @Override + public void close() { + logger.logStmt("context", "close()", delegate::close); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceStringFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceStringFormulaManager.java new file mode 100644 index 0000000000..a8212da2c2 --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceStringFormulaManager.java @@ -0,0 +1,320 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2025 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.delegate.trace; + +import static com.google.common.base.Preconditions.checkNotNull; + +import java.util.List; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +public class TraceStringFormulaManager implements StringFormulaManager { + + private final StringFormulaManager delegate; + private final TraceLogger logger; + + TraceStringFormulaManager(StringFormulaManager pDelegate, TraceLogger pLogger) { + delegate = checkNotNull(pDelegate); + logger = checkNotNull(pLogger); + } + + @Override + public StringFormula makeString(String value) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("makeString(%s)", logger.printString(value)), + () -> delegate.makeString(value)); + } + + @Override + public StringFormula makeVariable(String pVar) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("makeVariable(%s)", logger.printString(pVar)), + () -> delegate.makeVariable(pVar)); + } + + @Override + public BooleanFormula equal(StringFormula str1, StringFormula str2) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("equal(%s, %s)", logger.toVariable(str1), logger.toVariable(str2)), + () -> delegate.equal(str1, str2)); + } + + @Override + public BooleanFormula greaterThan(StringFormula str1, StringFormula str2) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("greaterThan(%s, %s)", logger.toVariable(str1), logger.toVariable(str2)), + () -> delegate.greaterThan(str1, str2)); + } + + @Override + public BooleanFormula greaterOrEquals(StringFormula str1, StringFormula str2) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("greaterOrEquals(%s, %s)", logger.toVariable(str1), logger.toVariable(str2)), + () -> delegate.greaterOrEquals(str1, str2)); + } + + @Override + public BooleanFormula lessThan(StringFormula str1, StringFormula str2) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("lessThan(%s, %s)", logger.toVariable(str1), logger.toVariable(str2)), + () -> delegate.lessThan(str1, str2)); + } + + @Override + public BooleanFormula lessOrEquals(StringFormula str1, StringFormula str2) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("lessOrEquals(%s, %s)", logger.toVariable(str1), logger.toVariable(str2)), + () -> delegate.lessOrEquals(str1, str2)); + } + + @Override + public BooleanFormula prefix(StringFormula prefix, StringFormula str) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("prefix(%s, %s)", logger.toVariable(prefix), logger.toVariable(str)), + () -> delegate.prefix(prefix, str)); + } + + @Override + public BooleanFormula suffix(StringFormula suffix, StringFormula str) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("suffix(%s, %s)", logger.toVariable(suffix), logger.toVariable(str)), + () -> delegate.suffix(suffix, str)); + } + + @Override + public BooleanFormula contains(StringFormula str, StringFormula part) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("contains(%s, %s)", logger.toVariable(str), logger.toVariable(part)), + () -> delegate.contains(str, part)); + } + + @Override + public IntegerFormula indexOf(StringFormula str, StringFormula part, IntegerFormula startIndex) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format( + "indexOf(%s, %s, %s)", + logger.toVariable(str), logger.toVariable(part), logger.toVariable(startIndex)), + () -> delegate.indexOf(str, part, startIndex)); + } + + @Override + public StringFormula charAt(StringFormula str, IntegerFormula index) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("charAt(%s, %s)", logger.toVariable(str), logger.toVariable(index)), + () -> delegate.charAt(str, index)); + } + + @Override + public StringFormula substring(StringFormula str, IntegerFormula index, IntegerFormula length) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format( + "substring(%s, %s, %s)", + logger.toVariable(str), logger.toVariable(index), logger.toVariable(length)), + () -> delegate.substring(str, index, length)); + } + + @Override + public StringFormula replace( + StringFormula fullStr, StringFormula target, StringFormula replacement) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format( + "replace(%s, %s, %s)", + logger.toVariable(fullStr), logger.toVariable(target), logger.toVariable(replacement)), + () -> delegate.replace(fullStr, target, replacement)); + } + + @Override + public StringFormula replaceAll( + StringFormula fullStr, StringFormula target, StringFormula replacement) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format( + "replaceAll(%s, %s, %s)", + logger.toVariable(fullStr), logger.toVariable(target), logger.toVariable(replacement)), + () -> delegate.replaceAll(fullStr, target, replacement)); + } + + @Override + public IntegerFormula length(StringFormula str) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("length(%s)", logger.toVariable(str)), + () -> delegate.length(str)); + } + + @Override + public StringFormula concat(List parts) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format( + "concat(%s)", + parts.stream().map(logger::toVariable).reduce((a, b) -> a + ", " + b).orElse("")), + () -> delegate.concat(parts)); + } + + @Override + public BooleanFormula in(StringFormula str, RegexFormula regex) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("in(%s, %s)", logger.toVariable(str), logger.toVariable(regex)), + () -> delegate.in(str, regex)); + } + + @Override + public RegexFormula makeRegex(String value) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("makeRegex(%s)", logger.printString(value)), + () -> delegate.makeRegex(value)); + } + + @Override + public RegexFormula none() { + return logger.logDef("mgr.getStringFormulaManager()", "none()", delegate::none); + } + + @Override + public RegexFormula all() { + return logger.logDef("mgr.getStringFormulaManager()", "all()", delegate::all); + } + + @Override + public RegexFormula allChar() { + return logger.logDef("mgr.getStringFormulaManager()", "allChar()", delegate::allChar); + } + + @Override + public RegexFormula range(StringFormula start, StringFormula end) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("range(%s, %s)", logger.toVariable(start), logger.toVariable(end)), + () -> delegate.range(start, end)); + } + + @Override + public RegexFormula concatRegex(List parts) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("concatRegex(%s)", logger.toVariables(parts)), + () -> delegate.concatRegex(parts)); + } + + @Override + public RegexFormula union(RegexFormula regex1, RegexFormula regex2) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("union(%s, %s)", logger.toVariable(regex1), logger.toVariable(regex2)), + () -> delegate.union(regex1, regex2)); + } + + @Override + public RegexFormula intersection(RegexFormula regex1, RegexFormula regex2) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("intersection(%s, %s)", logger.toVariable(regex1), logger.toVariable(regex2)), + () -> delegate.intersection(regex1, regex2)); + } + + @Override + public RegexFormula complement(RegexFormula regex) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("complement(%s)", logger.toVariable(regex)), + () -> delegate.complement(regex)); + } + + @Override + public RegexFormula closure(RegexFormula regex) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("closure(%s)", logger.toVariable(regex)), + () -> delegate.closure(regex)); + } + + @Override + public RegexFormula difference(RegexFormula regex1, RegexFormula regex2) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("difference(%s, %s)", logger.toVariable(regex1), logger.toVariable(regex2)), + () -> delegate.difference(regex1, regex2)); + } + + @Override + public RegexFormula cross(RegexFormula regex) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("cross(%s)", logger.toVariable(regex)), + () -> delegate.cross(regex)); + } + + @Override + public RegexFormula optional(RegexFormula regex) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("optional(%s)", logger.toVariable(regex)), + () -> delegate.optional(regex)); + } + + @Override + public RegexFormula times(RegexFormula regex, int repetitions) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("times(%s, %d)", logger.toVariable(regex), repetitions), + () -> delegate.times(regex, repetitions)); + } + + @Override + public IntegerFormula toIntegerFormula(StringFormula str) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("toIntegerFormula(%s)", logger.toVariable(str)), + () -> delegate.toIntegerFormula(str)); + } + + @Override + public StringFormula toStringFormula(IntegerFormula number) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("toStringFormula(%s)", logger.toVariable(number)), + () -> delegate.toStringFormula(number)); + } + + @Override + public IntegerFormula toCodePoint(StringFormula str) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("toCodePoint(%s)", logger.toVariable(str)), + () -> delegate.toCodePoint(str)); + } + + @Override + public StringFormula fromCodePoint(IntegerFormula codePoint) { + return logger.logDef( + "mgr.getStringFormulaManager()", + String.format("fromCodePoint(%s)", logger.toVariable(codePoint)), + () -> delegate.fromCodePoint(codePoint)); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceUFManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceUFManager.java new file mode 100644 index 0000000000..8e295b87eb --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceUFManager.java @@ -0,0 +1,81 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.delegate.trace; + +import com.google.common.base.Joiner; +import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableList; +import java.util.List; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; +import org.sosy_lab.java_smt.api.UFManager; + +public class TraceUFManager implements UFManager { + private final UFManager delegate; + + private final FormulaManager mgr; + private final TraceLogger logger; + + TraceUFManager(UFManager pDelegate, FormulaManager pMgr, TraceLogger pLogger) { + delegate = pDelegate; + mgr = pMgr; + logger = pLogger; + } + + @Override + public FunctionDeclaration declareUF( + String name, FormulaType returnType, List> args) { + String var = logger.newVariable(); + logger.appendDef( + var, + String.format( + "mgr.getUFManager().declareUF(%s, %s, ImmutableList.of(%s))", + logger.printString(name), + logger.printFormulaType(returnType), + FluentIterable.from(args).transform(logger::printFormulaType).join(Joiner.on(", ")))); + FunctionDeclaration f = delegate.declareUF(name, returnType, args); + if (logger.isTracked(f)) { + logger.undoLast(); + } else { + logger.keepLast(); + logger.mapVariable(var, f); + } + return f; + } + + @Override + public T callUF( + FunctionDeclaration funcType, List args) { + if (funcType.getKind().equals(FunctionDeclarationKind.UF)) { + return logger.logDef( + "mgr.getUFManager()", + String.format( + "callUF(%s, ImmutableList.of(%s))", + logger.toVariable(funcType), logger.toVariables(args)), + () -> delegate.callUF(funcType, args)); + } else { + return mgr.makeApplication(funcType, args); + } + } + + @Override + public T declareAndCallUF( + String name, FormulaType pReturnType, List pArgs) { + ImmutableList.Builder> builder = ImmutableList.builder(); + for (Formula f : pArgs) { + builder.add(mgr.getFormulaType(f)); + } + return callUF(declareUF(name, pReturnType, builder.build()), pArgs); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/trace/package-info.java b/src/org/sosy_lab/java_smt/delegate/trace/package-info.java new file mode 100644 index 0000000000..1b69a33f5b --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/trace/package-info.java @@ -0,0 +1,15 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +@com.google.errorprone.annotations.CheckReturnValue +@javax.annotation.ParametersAreNonnullByDefault +@org.sosy_lab.common.annotations.FieldsAreNonnullByDefault +@org.sosy_lab.common.annotations.ReturnValuesAreNonnullByDefault +package org.sosy_lab.java_smt.delegate.trace; diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index aaaafe25d4..0d206eeb57 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -482,6 +482,7 @@ private Expr normalize(Expr operator) { .put(Kind.BITVECTOR_NEG, FunctionDeclarationKind.BV_NEG) .put(Kind.BITVECTOR_EXTRACT, FunctionDeclarationKind.BV_EXTRACT) .put(Kind.BITVECTOR_CONCAT, FunctionDeclarationKind.BV_CONCAT) + .put(Kind.BITVECTOR_TO_NAT, FunctionDeclarationKind.UBV_TO_INT) .put(Kind.BITVECTOR_SIGN_EXTEND, FunctionDeclarationKind.BV_SIGN_EXTENSION) .put(Kind.BITVECTOR_ZERO_EXTEND, FunctionDeclarationKind.BV_ZERO_EXTENSION) // Floating-point theory @@ -545,6 +546,12 @@ private Expr normalize(Expr operator) { .put(Kind.SELECT, FunctionDeclarationKind.SELECT) .put(Kind.STORE, FunctionDeclarationKind.STORE) .put(Kind.STORE_ALL, FunctionDeclarationKind.CONST) + // Separation logic + .put(Kind.SEP_EMP, FunctionDeclarationKind.SEP_EMP) + .put(Kind.SEP_NIL, FunctionDeclarationKind.SEP_NIL) + .put(Kind.SEP_PTO, FunctionDeclarationKind.SEP_PTO) + .put(Kind.SEP_STAR, FunctionDeclarationKind.SEP_STAR) + .put(Kind.SEP_WAND, FunctionDeclarationKind.SEP_WAND) .buildOrThrow(); private FunctionDeclarationKind getDeclarationKind(Expr f) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 8357c223b6..b951f3651c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -638,6 +638,7 @@ private Term normalize(Term operator) { .put(Kind.STRING_FROM_CODE, FunctionDeclarationKind.STR_FROM_CODE) .put(Kind.STRING_LT, FunctionDeclarationKind.STR_LT) .put(Kind.STRING_LEQ, FunctionDeclarationKind.STR_LE) + .put(Kind.REGEXP_NONE, FunctionDeclarationKind.RE_NONE) .put(Kind.REGEXP_PLUS, FunctionDeclarationKind.RE_PLUS) .put(Kind.REGEXP_STAR, FunctionDeclarationKind.RE_STAR) .put(Kind.REGEXP_OPT, FunctionDeclarationKind.RE_OPTIONAL) @@ -650,6 +651,12 @@ private Term normalize(Term operator) { .put(Kind.SELECT, FunctionDeclarationKind.SELECT) .put(Kind.STORE, FunctionDeclarationKind.STORE) .put(Kind.CONST_ARRAY, FunctionDeclarationKind.CONST) + // Separation logic + .put(Kind.SEP_EMP, FunctionDeclarationKind.SEP_EMP) + .put(Kind.SEP_NIL, FunctionDeclarationKind.SEP_NIL) + .put(Kind.SEP_PTO, FunctionDeclarationKind.SEP_PTO) + .put(Kind.SEP_STAR, FunctionDeclarationKind.SEP_STAR) + .put(Kind.SEP_WAND, FunctionDeclarationKind.SEP_WAND) .build(); private FunctionDeclarationKind getDeclarationKind(Term f) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index e77d109188..ff5618f730 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -109,6 +109,11 @@ assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType return out.toString(); } + @Override + protected Term simplify(Term f) throws InterruptedException { + return creator.getSolver().simplify(f); + } + @Override public T substitute( final T f, final Map fromToMapping) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java index f39e004ff7..a322f1f7ca 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java @@ -180,7 +180,8 @@ private Term getCVC5Interpolation(Collection formulasA, Collection f Term interpolant; try { itpSolver.assertFormula(phiPlus); - interpolant = itpSolver.getInterpolant(termManager.mkTerm(Kind.NOT, phiMinus)); + interpolant = + itpSolver.simplify(itpSolver.getInterpolant(termManager.mkTerm(Kind.NOT, phiMinus))); } finally { itpSolver.deletePointer(); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java index 6bb7c0f618..3f112c6296 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java @@ -140,17 +140,7 @@ protected Term allCharImpl() { @Override protected Term range(Term start, Term end) { - // Precondition: Both bounds must be single character Strings - // CVC5 already checks that the lower bound is smaller than the upper bound and returns the - // empty language otherwise. - Term one = termManager.mkInteger(1); - Term cond = - termManager.mkTerm( - Kind.AND, - termManager.mkTerm(Kind.EQUAL, length(start), one), - termManager.mkTerm(Kind.EQUAL, length(end), one)); - return termManager.mkTerm( - Kind.ITE, cond, termManager.mkTerm(Kind.REGEXP_RANGE, start, end), noneImpl()); + return termManager.mkTerm(Kind.REGEXP_RANGE, start, end); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 6f325cb173..9e4966cdad 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -602,6 +602,8 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) { return FunctionDeclarationKind.OTHER; } else if (fun == ModuloArithmetic.int_cast()) { return FunctionDeclarationKind.OTHER; + } else if (fun == PrincessEnvironment.stringTheory.re_none()) { + return FunctionDeclarationKind.RE_NONE; } else { return FunctionDeclarationKind.UF; } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java index 0ffa256696..656c3f55df 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java @@ -129,7 +129,13 @@ protected IFormula greaterThan(IExpression pNumber1, IExpression pNumber2) { @Override protected IFormula greaterOrEquals(IExpression pNumber1, IExpression pNumber2) { - return ((ITerm) pNumber1).$greater$eq((ITerm) pNumber2); + if (pNumber1.equals(IExpression.i(0))) { + return IExpression.geqZero((ITerm) pNumber2); + } else if (pNumber2.equals(IExpression.i(0))) { + return IExpression.geqZero((ITerm) pNumber1); + } else { + return ((ITerm) pNumber1).$greater$eq((ITerm) pNumber2); + } } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java index a73fbaee79..ca33ef7c76 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java @@ -37,7 +37,13 @@ abstract class PrincessNumeralFormulaManager< @Override protected IFormula equal(IExpression pNumber1, IExpression pNumber2) { - return ((ITerm) pNumber1).$eq$eq$eq((ITerm) pNumber2); + if (pNumber1.equals(IExpression.i(0))) { + return IExpression.eqZero((ITerm) pNumber2); + } else if (pNumber2.equals(IExpression.i(0))) { + return IExpression.eqZero((ITerm) pNumber1); + } else { + return ((ITerm) pNumber1).$eq$eq$eq((ITerm) pNumber2); + } } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java index 7c7657d1d1..09bd150d6d 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java @@ -174,4 +174,9 @@ public Term lessThan(Term pNumber1, Term pNumber2) { public Term lessOrEquals(Term pNumber1, Term pNumber2) { return env.term("<=", pNumber1, pNumber2); } + + @Override + protected Term sumImpl(List operands) { + return env.term("+", operands.toArray(new Term[0])); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index 0f9fdc558c..d5306417e8 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -9,7 +9,6 @@ package org.sosy_lab.java_smt.solvers.z3; import static com.google.common.base.Preconditions.checkArgument; -import static com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DISTINCT; import com.google.common.base.Preconditions; import com.google.common.collect.HashBasedTable; @@ -658,7 +657,7 @@ private FunctionDeclarationKind getDeclarationKind(long f) { Z3_decl_kind decl = Z3_decl_kind.fromInt(Native.getDeclKind(environment, Native.getAppDecl(environment, f))); - assert (arity > 0) || (arity == 0 && decl == Z3_OP_DISTINCT) + assert arity >= 0 : String.format( "Unexpected arity '%s' for formula '%s' for handling a function application.", arity, Native.astToString(environment, f)); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java index ea834fbdb1..2c380b8848 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java @@ -60,9 +60,7 @@ protected Long makeVariableImpl(String varName) { @Override protected Long negate(Long pNumber) { - long sort = Native.getSort(z3context, pNumber); - long minusOne = Native.mkInt(z3context, -1, sort); - return Native.mkMul(z3context, 2, new long[] {minusOne, pNumber}); + return Native.mkUnaryMinus(z3context, pNumber); } @Override @@ -74,6 +72,8 @@ protected Long add(Long pNumber1, Long pNumber2) { protected Long sumImpl(List operands) { if (operands.isEmpty()) { return makeNumberImpl(0); + } else if (operands.size() == 1) { + return operands.get(0); } else { return Native.mkAdd(z3context, operands.size(), Longs.toArray(operands)); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3QuantifiedFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3QuantifiedFormulaManager.java index 424f6bef9d..f6a9b043c3 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3QuantifiedFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3QuantifiedFormulaManager.java @@ -38,11 +38,11 @@ public Long mkQuantifier(Quantifier q, List pVariables, Long pBody) { return Native.mkQuantifierConst( z3context, q == Quantifier.FORALL, - 0, + 1, pVariables.size(), Longs.toArray(pVariables), 0, - new long[0], + null, pBody); } diff --git a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java index 178d4b73e8..40564d9150 100644 --- a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java @@ -88,9 +88,9 @@ public void testIntIndexStringValue() throws SolverException, InterruptedExcepti StringFormula stringTwo = smgr.makeString("two"); IntegerFormula intFour = imgr.makeNumber(4); ArrayFormula arr1 = - amgr.makeArray("arr1", FormulaType.IntegerType, StringType); + amgr.makeArray("arr1", IntegerType, StringType); ArrayFormula arr2 = - amgr.makeArray("arr2", FormulaType.IntegerType, StringType); + amgr.makeArray("arr2", IntegerType, StringType); BooleanFormula query = bmgr.and( amgr.equivalence(arr2, amgr.store(arr1, intFour, stringTwo)), diff --git a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java index 8974490f3d..50730295c7 100644 --- a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java @@ -17,6 +17,7 @@ import org.checkerframework.checker.nullness.qual.NonNull; import org.junit.Test; import org.sosy_lab.common.configuration.ConfigurationBuilder; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -51,7 +52,7 @@ public class ModelEvaluationTest extends SolverBasedTest0.ParameterizedSolverBas private static int problemSize; @Override - protected ConfigurationBuilder createTestConfigBuilder() { + protected ConfigurationBuilder createTestConfigBuilder() throws InvalidConfigurationException { problemSize = solverToUse() == Solvers.PRINCESS ? 10 : 50; // Princess is too slow. ConfigurationBuilder builder = super.createTestConfigBuilder(); if (solverToUse() == Solvers.MATHSAT5) { diff --git a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java index e5650b8ba0..471bd682bb 100644 --- a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java +++ b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java @@ -24,6 +24,7 @@ import org.junit.runners.Parameterized.Parameter; import org.junit.runners.Parameterized.Parameters; import org.sosy_lab.common.configuration.ConfigurationBuilder; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.FormulaType; @@ -90,7 +91,7 @@ public void chooseNumeralFormulaManager() { public NonLinearArithmetic nonLinearArithmetic; @Override - protected ConfigurationBuilder createTestConfigBuilder() { + protected ConfigurationBuilder createTestConfigBuilder() throws InvalidConfigurationException { return super.createTestConfigBuilder() .setOption("solver.nonLinearArithmetic", nonLinearArithmetic.name()); } diff --git a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java index 3b80ce644e..3d436c0567 100644 --- a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java +++ b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java @@ -22,6 +22,7 @@ import org.junit.runners.Parameterized.Parameter; import org.junit.runners.Parameterized.Parameters; import org.sosy_lab.common.configuration.ConfigurationBuilder; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; @@ -53,7 +54,7 @@ protected Solvers solverToUse() { public NonLinearArithmetic nonLinearArithmetic; @Override - protected ConfigurationBuilder createTestConfigBuilder() { + protected ConfigurationBuilder createTestConfigBuilder() throws InvalidConfigurationException { return super.createTestConfigBuilder() .setOption("solver.nonLinearArithmetic", nonLinearArithmetic.name()); } diff --git a/src/org/sosy_lab/java_smt/test/OptimizationTest.java b/src/org/sosy_lab/java_smt/test/OptimizationTest.java index ca2beefc6d..efc7646b6e 100644 --- a/src/org/sosy_lab/java_smt/test/OptimizationTest.java +++ b/src/org/sosy_lab/java_smt/test/OptimizationTest.java @@ -16,6 +16,7 @@ import org.junit.Before; import org.junit.Test; import org.sosy_lab.common.configuration.ConfigurationBuilder; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.Model; @@ -29,7 +30,7 @@ public class OptimizationTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @Override - protected ConfigurationBuilder createTestConfigBuilder() { + protected ConfigurationBuilder createTestConfigBuilder() throws InvalidConfigurationException { return super.createTestConfigBuilder().setOption("solver.mathsat5.loadOptimathsat5", "true"); } diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 901452e8d7..0b39a9e6f0 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -18,6 +18,8 @@ import org.checkerframework.checker.nullness.qual.Nullable; import org.junit.After; import org.junit.Before; +import org.junit.Rule; +import org.junit.rules.TestName; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; import org.junit.runners.Parameterized.Parameter; @@ -26,7 +28,10 @@ import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.ConfigurationBuilder; +import org.sosy_lab.common.configuration.FileOption; import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.configuration.converters.FileTypeConverter; +import org.sosy_lab.common.io.PathTemplate; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; @@ -87,6 +92,8 @@ */ public abstract class SolverBasedTest0 { + @Rule public TestName testName = new TestName(); + protected Configuration config; protected final LogManager logger = LogManager.createTestLogManager(); @@ -123,12 +130,25 @@ protected Logics logicToUse() { return Logics.QF_AUFLIRA; } - protected ConfigurationBuilder createTestConfigBuilder() { + protected ConfigurationBuilder createTestConfigBuilder() throws InvalidConfigurationException { ConfigurationBuilder newConfig = Configuration.builder().setOption("solver.solver", solverToUse().toString()); + + if (solverToUse() != Solvers.BOOLECTOR) { // Boolector has no formula visitation. + String tracefile = + String.format( + "traces/%s/trace_%s_%s.java", + this.getClass().getSimpleName(), testName.getMethodName(), System.nanoTime()); + newConfig.setOption("solver.trace", "true").setOption("solver.tracefile", tracefile); + Configuration configForFiles = Configuration.builder().setOption("output.path", "./").build(); + FileTypeConverter fileTypeConverter = FileTypeConverter.create(configForFiles); + Configuration.getDefaultConverters().put(FileOption.class, fileTypeConverter); + newConfig.addConverter(PathTemplate.class, fileTypeConverter); + } if (solverToUse() == Solvers.OPENSMT) { newConfig.setOption("solver.opensmt.logic", logicToUse().toString()); } + return newConfig; }