diff --git a/.gitignore b/.gitignore index e0a8342b77..7427e9a9db 100644 --- a/.gitignore +++ b/.gitignore @@ -38,3 +38,4 @@ test-semantics/*.llvm *.olean lakefile.olean .lake/ +docker-results \ No newline at end of file diff --git a/SSA/Projects/InstCombine/HackersDelight/ch2_1DeMorgan.lean b/SSA/Projects/InstCombine/HackersDelight/ch2_1DeMorgan.lean index 201b185d44..55e6c9ad35 100644 --- a/SSA/Projects/InstCombine/HackersDelight/ch2_1DeMorgan.lean +++ b/SSA/Projects/InstCombine/HackersDelight/ch2_1DeMorgan.lean @@ -14,39 +14,39 @@ variable {x y z : BitVec WIDTH} theorem not_and_eq_not_or_not : ~~~ (x &&& y) = ~~~ x ||| ~~~ y := by - all_goals sorry + all_goals bv_compare' theorem not_or_eq_not_and_not : ~~~ (x ||| y) = ~~~ x &&& ~~~ y := by - all_goals sorry + all_goals bv_compare' theorem not_add_one_eq_not_sub_one : ~~~ (x + 1) = ~~~ x - 1 := by - all_goals sorry + all_goals bv_compare' theorem not_sub_one_eq_not_add_one : ~~~ (x - 1) = ~~~ x + 1 := by - all_goals sorry + all_goals bv_compare' theorem not_neg_eq_sub_one : ~~~ (- x) = x - 1 := by - all_goals sorry + all_goals bv_compare' theorem not_xor_eq_not_xor : ~~~ (x ^^^ y) = ~~~ x ^^^ y := by - all_goals sorry + all_goals bv_compare' theorem q_not_xor : ~~~ (x ^^^ y) = ~~~ x ^^^ y := by - all_goals sorry + all_goals bv_compare' theorem not_add_eq_not_sub : ~~~ (x + y) = ~~~ x - y := by - all_goals sorry + all_goals bv_compare' theorem not_sub_eq_not_add : ~~~ (x - y) = ~~~ x + y := by - all_goals sorry + all_goals bv_compare' end DeMorgansLawsExtended diff --git a/SSA/Projects/InstCombine/HackersDelight/ch2_2AdditionAndLogicalOps.lean b/SSA/Projects/InstCombine/HackersDelight/ch2_2AdditionAndLogicalOps.lean index 951a85dd26..ea9de583f3 100644 --- a/SSA/Projects/InstCombine/HackersDelight/ch2_2AdditionAndLogicalOps.lean +++ b/SSA/Projects/InstCombine/HackersDelight/ch2_2AdditionAndLogicalOps.lean @@ -12,91 +12,91 @@ variable {x y z : BitVec WIDTH} theorem neg_eq_not_add_one : -x = ~~~ x + 1 := by - all_goals sorry + all_goals bv_compare' theorem neg_eq_neg_not_one : -x = ~~~ (x - 1) := by - all_goals sorry + all_goals bv_compare' theorem not_eq_neg_sub_one : ~~~ x = - x - 1:= by - all_goals sorry + all_goals bv_compare' theorem neg_not_eq_add_one : - ~~~ x = x + 1 := by - all_goals sorry + all_goals bv_compare' theorem not_neg_eq_sub_one : ~~~ (-x) = x - 1 := by - all_goals sorry + all_goals bv_compare' theorem add_eq_sub_not_sub_one : x + y = x - ~~~ y - 1 := by - all_goals sorry + all_goals bv_compare' theorem add_eq_xor_add_mul_and : x + y = (x ^^^ y) + 2 * (x &&& y) := by - all_goals sorry + all_goals bv_compare' theorem add_eq_or_add_and : x + y = (x ||| y) + (x &&& y) := by - all_goals sorry + all_goals bv_compare' theorem add_eq_mul_or_neg_xor : x + y = 2 * (x ||| y) - (x ^^^ y) := by - all_goals sorry + all_goals bv_compare' theorem sub_eq_add_not_add_one : x - y = x + ~~~ y + 1 := by - all_goals sorry + all_goals bv_compare' theorem sub_eq_xor_sub_mul_not_and : x - y = (x ^^^ y) - 2 * (~~~ x &&& y) := by - all_goals sorry + all_goals bv_compare' theorem sub_eq_and_not_sub_not_and : x - y = (x &&& ~~~ y) - (~~~ x &&& y) := by - all_goals sorry + all_goals bv_compare' theorem sub_eq_mul_and_not_sub_xor : x - y = 2 * (x &&& ~~~ y) - (x ^^^ y) := by - all_goals sorry + all_goals bv_compare' theorem xor_eq_or_sub_and : x ^^^ y = (x ||| y) - (x &&& y) := by - all_goals sorry + all_goals bv_compare' theorem and_not_eq_or_sub: x &&& ~~~ y = (x ||| y) - y := by - all_goals sorry + all_goals bv_compare' theorem and_not_eq_sub_add : x &&& ~~~ y = x - (x &&& y) := by - all_goals sorry + all_goals bv_compare' theorem not_sub_eq_sub_sub_one : ~~~ (x - y) = y - x - 1 := by - all_goals sorry + all_goals bv_compare' theorem not_sub_eq_not_add : ~~~ (x - y) = ~~~x + y := by - all_goals sorry + all_goals bv_compare' theorem not_xor_eq_and_sub_or_sub_one : ~~~ (x ^^^ y) = (x &&& y) - (x ||| y) - 1 := by - all_goals sorry + all_goals bv_compare' theorem not_xor_eq_and_add_not_or : ~~~ (x ^^^ y) = (x &&& y) + ~~~ (x ||| y) := by - all_goals sorry + all_goals bv_compare' theorem or_eq_and_not_add : x ||| y = (x &&& ~~~ y) + y := by - all_goals sorry + all_goals bv_compare' theorem and_eq_not_or_sub_not : x &&& y = (~~~ x ||| y) - ~~~ x := by - all_goals sorry + all_goals bv_compare' end AdditionCombinedWithLogicalOperations diff --git a/artifact-evaluation/Dockerfile b/artifact-evaluation/Dockerfile index a4d65cc16f..c885d93782 100644 --- a/artifact-evaluation/Dockerfile +++ b/artifact-evaluation/Dockerfile @@ -6,15 +6,17 @@ WORKDIR /code RUN apt-get update -y \ && DEBIAN_FRONTEND="noninteractive" apt-get install --yes \ tzdata \ + pip \ + python3-venv \ build-essential \ cmake \ git \ - ripgrep \ - vim \ - neovim \ - emacs \ ninja-build \ - gdb curl wget + gdb curl wget \ + # dependencies for experiment scripts + python3-matplotlib python3-pandas python3-num2words \ + # bitwuzla dependencies + meson libgmp-dev libcadical-dev libsymfpu-dev pkg-config # Install Lean RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > /code/elan.sh \ @@ -22,11 +24,36 @@ RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh - ENV PATH /root/.elan/bin:$PATH ENV LIBRARY_PATH /root/.elan/lib:$LIBRARY_PATH -# Download & build lean-mlir -RUN curl -L https://github.com/opencompl/ssa/archive/refs/tags/v0.1.3.tar.gz > /code/ssa.tar.gz # SSA tar file -RUN tar xf ssa.tar.gz && ls /code/ && mv ssa-0.1.3 ssa # untar -WORKDIR /code/ssa -RUN lake -R exe cache get -RUN lake build SSA mlirnatural +# Install Bitwuzla +RUN git clone https://github.com/bitwuzla/bitwuzla +WORKDIR /code/bitwuzla +RUN ./configure.py && cd build && ninja install -USER root +# Install Lean-MLIR +RUN git clone https://github.com/opencompl/lean-mlir +WORKDIR /code/lean-mlir + +# Install plotting script dependencies + +# WORKDIR /code/lean-mlir/bv-evaluation/ +# RUN bash -c "\ +# python3 -m venv venv \ +# && source venv/bin/activate \ +# && python3 -m pip install -r /code/lean-mlir/bv-evaluation/requirements.txt " + +# First, get cached dependencies +WORKDIR /code/lean-mlir +COPY . . + +# COPY lean-toolchain lakefile.toml lake-manifest.json ./ +# RUN lake exe cache get! + +# Then, copy & build lean-mlir +RUN lake exe cache get +RUN lake build + +# Set the evaluation script directory as working dir +WORKDIR /code/lean-mlir/bv-evaluation/ +RUN python3 compare-leansat-vs-bitwuzla-hdel.py + +USER root \ No newline at end of file diff --git a/artifact-evaluation/README.md b/artifact-evaluation/README.md index 0f8f7df7a2..2ca39dea5b 100644 --- a/artifact-evaluation/README.md +++ b/artifact-evaluation/README.md @@ -7,5 +7,10 @@ $ docker login $ make docker-build-and-push ``` -#### Steps to use docker image +#### Build docker image and extract results +from folder lean-mlir: +- docker build -f artifact-evaluation/Dockerfile -t lean-image . +- docker create --name temp-container lean-image +- docker cp temp-container:/code/lean-mlir/bv-evaluation/raw-data ./docker-results +- docker rm temp-container \ No newline at end of file diff --git a/artifact-evaluation/artifact.pdf b/artifact-evaluation/artifact.pdf index 148cfb1ba7..faafe01cb3 100644 Binary files a/artifact-evaluation/artifact.pdf and b/artifact-evaluation/artifact.pdf differ diff --git a/artifact-evaluation/artifact.tex b/artifact-evaluation/artifact.tex index da7ec1fef1..9d7f5567e4 100644 --- a/artifact-evaluation/artifact.tex +++ b/artifact-evaluation/artifact.tex @@ -116,10 +116,15 @@ \subsubsection{Software dependencies} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Experiment workflow} -Access the docker image \texttt{opencompl-ssa} from -\url{https://zenodo.org/records/11519739}. +Access the docker image \texttt{lean-mlir} from +\textcolor{red}{Zenodo link}. \begin{minted}[fontsize=\scriptsize]{text} + from folder lean-mlir: +- docker build -f artifact-evaluation/Dockerfile -t lean-image . +- docker create --name temp-container lean-image +- docker cp temp-container:/code/lean-mlir/bv-evaluation/raw-data ./docker-results +- docker rm temp-container $ docker load -i opencompl-ssa.tar $ docker run -it siddudruid/opencompl-ssa # | This clears the build cache, diff --git a/artifact-evaluation/makefile b/artifact-evaluation/makefile deleted file mode 100644 index fbcb53c841..0000000000 --- a/artifact-evaluation/makefile +++ /dev/null @@ -1,11 +0,0 @@ -.PHONY: docker-build docker-build-debug clean -artifact.pdf: artifact.tex sigplanconf.cls - latexmk -pdf -shell-escape artifact.tex - -docker-build-and-push: - docker build -t opencompl-ssa --progress plain . - docker save -o ./opencompl-ssa.tar opencompl-ssa - docker push siddudruid/opencompl-ssa - -clean: - latexmk -C diff --git a/bv-evaluation/Makefile b/bv-evaluation/Makefile new file mode 100644 index 0000000000..07f509aee9 --- /dev/null +++ b/bv-evaluation/Makefile @@ -0,0 +1,17 @@ + +DOCKER=podman +DOCKER_IMAGE_TAG=opencompl/lean-mlir-bv-evaluate + +docker-image: + ${DOCKER} build -f Dockerfile ../ -t "${DOCKER_IMAGE_TAG}" + +.PHONY: + +*.py: .PHONY + ./run-script.sh python3 $@ + +clean: + docker rmi ${DOCKER_IMAGE_TAG} + +all: + ./run-script.sh ./run-tests.sh diff --git a/bv-evaluation/collect-data-alive.py b/bv-evaluation/collect-data-alive.py index 7b753059e1..3d0e919ea0 100644 --- a/bv-evaluation/collect-data-alive.py +++ b/bv-evaluation/collect-data-alive.py @@ -4,7 +4,7 @@ import os import re -paper_directory = 'for-paper/' +paper_directory = '' benchmark_dir = "../SSA/Projects/InstCombine/" res_dir = "results/AliveSymbolic/" raw_data_dir = paper_directory + 'raw-data/AliveSymbolic/' @@ -19,6 +19,16 @@ "#fb9a99", "#e31a1c"] +def clear_folder(): + for file in os.listdir(RESULTS_DIR): + file_path = os.path.join(RESULTS_DIR, file) + try: + if os.path.isfile(file_path) or os.path.islink(file_path): + os.unlink(file_path) + elif os.path.isdir(file_path): + shutil.rmtree(file_path) + except Exception as e: + print('Failed to delete %s. Reason: %s' % (file_path, e)) def parse_tacbenches(file_name, raw): diff --git a/bv-evaluation/collect-data-hdel-symbolic.py b/bv-evaluation/collect-data-hdel-symbolic.py index 4cdeccfee7..228b16949e 100644 --- a/bv-evaluation/collect-data-hdel-symbolic.py +++ b/bv-evaluation/collect-data-hdel-symbolic.py @@ -4,7 +4,7 @@ import os import re -paper_directory = 'for-paper/' +paper_directory = '' benchmark_dir = "../SSA/Projects/InstCombine/HackersDelight/" res_dir = "results/HackersDelightSymbolic/" raw_data_dir = paper_directory + 'raw-data/HackersDelightSymbolic/' diff --git a/bv-evaluation/collect-data-hdel.py b/bv-evaluation/collect-data-hdel.py index 5bb5bc1593..a22e669634 100644 --- a/bv-evaluation/collect-data-hdel.py +++ b/bv-evaluation/collect-data-hdel.py @@ -3,7 +3,7 @@ import pandas as pd import os -paper_directory = 'for-paper/' +paper_directory = '' benchmark_dir = "../SSA/Projects/InstCombine/HackersDelight/" res_dir = "results/HackersDelight/" raw_data_dir = paper_directory + 'raw-data/HackersDelight/' @@ -80,7 +80,9 @@ while l: if "Bitwuzla " in l: cegb = False - if "counter" in l : + if "failed" in l : + print(l) + elif "counter" in l : cegb = True tot = float(l.split("after ")[1].split("ms")[0]) if r == 0: diff --git a/bv-evaluation/collect-data-llvm-symbolic.py b/bv-evaluation/collect-data-llvm-symbolic.py index d7541801c2..5ce57e8961 100644 --- a/bv-evaluation/collect-data-llvm-symbolic.py +++ b/bv-evaluation/collect-data-llvm-symbolic.py @@ -4,7 +4,7 @@ import os import re -paper_directory = 'for-paper/' +paper_directory = '' benchmark_dir = "../SSA/Projects/InstCombine/tests/proofs/" res_dir = "results/InstCombineSymbolic/" raw_data_dir = paper_directory + 'raw-data/InstCombineSymbolic/' diff --git a/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py b/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py index a69d3b79fb..253dea2448 100644 --- a/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py +++ b/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py @@ -74,4 +74,4 @@ def process(jobs: int): parser = argparse.ArgumentParser(prog='compare-leansat-vs-bitwuzla-llvm') parser.add_argument('-j', '--jobs', type=int, default=1) args = parser.parse_args() -process(args.jobs) \ No newline at end of file +process(args.jobs) diff --git a/bv-evaluation/compare-leansat-vs-bitwuzla-llvm.py b/bv-evaluation/compare-leansat-vs-bitwuzla-llvm.py index 8328e9f1cc..74bc8d60ec 100644 --- a/bv-evaluation/compare-leansat-vs-bitwuzla-llvm.py +++ b/bv-evaluation/compare-leansat-vs-bitwuzla-llvm.py @@ -14,17 +14,6 @@ TIMEOUT = 1800 -def clear_folder(): - for file in os.listdir(RESULTS_DIR): - file_path = os.path.join(RESULTS_DIR, file) - try: - if os.path.isfile(file_path) or os.path.islink(file_path): - os.unlink(file_path) - elif os.path.isdir(file_path): - shutil.rmtree(file_path) - except Exception as e: - print('Failed to delete %s. Reason: %s' % (file_path, e)) - def run_file(file: str): file_path = BENCHMARK_DIR + file file_title = file.split('.')[0] @@ -48,7 +37,7 @@ def process(jobs: int): with concurrent.futures.ThreadPoolExecutor(max_workers=jobs) as executor: futures = {} for file in os.listdir(BENCHMARK_DIR): - if "_proof" in file: # currently discard broken chapter + if "_proof" in file: future = executor.submit(run_file, file) futures[future] = file @@ -62,5 +51,4 @@ def process(jobs: int): parser = argparse.ArgumentParser(prog='compare-leansat-vs-bitwuzla-llvm') parser.add_argument('-j', '--jobs', type=int, default=1) args = parser.parse_args() -clear_folder() process(args.jobs) diff --git a/bv-evaluation/plots/Makefile b/bv-evaluation/plots/Makefile new file mode 100644 index 0000000000..fda22e102f --- /dev/null +++ b/bv-evaluation/plots/Makefile @@ -0,0 +1,22 @@ +.PHONY: lint + + +all : + python3 plot.py all + +lint: + ruff format *.py + ruff check *.py + +instcombine : + python3 plot.py instcombine + +hackersdelight : + python3 plot.py hackersdelight + +smtlib : + python3 plot.py smtlib + + +clean: + rm *.pdf diff --git a/bv-evaluation/plots/bitwuzla_ch2_1DeMorgan.pdf b/bv-evaluation/plots/bitwuzla_ch2_1DeMorgan.pdf deleted file mode 100644 index ff980c56e1..0000000000 Binary files a/bv-evaluation/plots/bitwuzla_ch2_1DeMorgan.pdf and /dev/null differ diff --git a/bv-evaluation/plots/bitwuzla_ch2_2AdditionAndLogicalOps.pdf b/bv-evaluation/plots/bitwuzla_ch2_2AdditionAndLogicalOps.pdf deleted file mode 100644 index 55d3dd9617..0000000000 Binary files a/bv-evaluation/plots/bitwuzla_ch2_2AdditionAndLogicalOps.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv16_ch2_1DeMorgan.pdf b/bv-evaluation/plots/cumul_problems_bv16_ch2_1DeMorgan.pdf deleted file mode 100644 index dc76536132..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv16_ch2_1DeMorgan.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv16_ch2_2AdditionAndLogicalOps.pdf b/bv-evaluation/plots/cumul_problems_bv16_ch2_2AdditionAndLogicalOps.pdf deleted file mode 100644 index 9e3d78d060..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv16_ch2_2AdditionAndLogicalOps.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv32_ch2_1DeMorgan.pdf b/bv-evaluation/plots/cumul_problems_bv32_ch2_1DeMorgan.pdf deleted file mode 100644 index 83eb8e6599..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv32_ch2_1DeMorgan.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv32_ch2_2AdditionAndLogicalOps.pdf b/bv-evaluation/plots/cumul_problems_bv32_ch2_2AdditionAndLogicalOps.pdf deleted file mode 100644 index c6bcf81da5..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv32_ch2_2AdditionAndLogicalOps.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv4_ch2_1DeMorgan.pdf b/bv-evaluation/plots/cumul_problems_bv4_ch2_1DeMorgan.pdf deleted file mode 100644 index f804feb457..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv4_ch2_1DeMorgan.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv4_ch2_2AdditionAndLogicalOps.pdf b/bv-evaluation/plots/cumul_problems_bv4_ch2_2AdditionAndLogicalOps.pdf deleted file mode 100644 index ef2b11cc54..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv4_ch2_2AdditionAndLogicalOps.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv64_ch2_1DeMorgan.pdf b/bv-evaluation/plots/cumul_problems_bv64_ch2_1DeMorgan.pdf deleted file mode 100644 index 013f9f49b8..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv64_ch2_1DeMorgan.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv64_ch2_2AdditionAndLogicalOps.pdf b/bv-evaluation/plots/cumul_problems_bv64_ch2_2AdditionAndLogicalOps.pdf deleted file mode 100644 index 08b0cff50a..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv64_ch2_2AdditionAndLogicalOps.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv8_ch2_1DeMorgan.pdf b/bv-evaluation/plots/cumul_problems_bv8_ch2_1DeMorgan.pdf deleted file mode 100644 index 97307a02a8..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv8_ch2_1DeMorgan.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_bv8_ch2_2AdditionAndLogicalOps.pdf b/bv-evaluation/plots/cumul_problems_bv8_ch2_2AdditionAndLogicalOps.pdf deleted file mode 100644 index 7925de013b..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_bv8_ch2_2AdditionAndLogicalOps.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_llvm_llvm-ceg-cumul.pdf b/bv-evaluation/plots/cumul_problems_llvm_llvm-ceg-cumul.pdf deleted file mode 100644 index cec7343d53..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_llvm_llvm-ceg-cumul.pdf and /dev/null differ diff --git a/bv-evaluation/plots/cumul_problems_llvm_llvm-cumul.pdf b/bv-evaluation/plots/cumul_problems_llvm_llvm-cumul.pdf deleted file mode 100644 index 762a11beea..0000000000 Binary files a/bv-evaluation/plots/cumul_problems_llvm_llvm-cumul.pdf and /dev/null differ diff --git a/bv-evaluation/plots/leanSAT_stacked_ch2_1DeMorgan.pdf b/bv-evaluation/plots/leanSAT_stacked_ch2_1DeMorgan.pdf deleted file mode 100644 index f4f2e47d08..0000000000 Binary files a/bv-evaluation/plots/leanSAT_stacked_ch2_1DeMorgan.pdf and /dev/null differ diff --git a/bv-evaluation/plots/leanSAT_stacked_ch2_2AdditionAndLogicalOps.pdf b/bv-evaluation/plots/leanSAT_stacked_ch2_2AdditionAndLogicalOps.pdf deleted file mode 100644 index 9a1f7255d3..0000000000 Binary files a/bv-evaluation/plots/leanSAT_stacked_ch2_2AdditionAndLogicalOps.pdf and /dev/null differ diff --git a/bv-evaluation/plots/llvm-ceg-cumul.pdf b/bv-evaluation/plots/llvm-ceg-cumul.pdf deleted file mode 100644 index 3cfdadbf46..0000000000 Binary files a/bv-evaluation/plots/llvm-ceg-cumul.pdf and /dev/null differ diff --git a/bv-evaluation/plots/llvm-cumul.pdf b/bv-evaluation/plots/llvm-cumul.pdf deleted file mode 100644 index 5e85ced502..0000000000 Binary files a/bv-evaluation/plots/llvm-cumul.pdf and /dev/null differ diff --git a/bv-evaluation/plots/plot.py b/bv-evaluation/plots/plot.py new file mode 100644 index 0000000000..a57b5e8aac --- /dev/null +++ b/bv-evaluation/plots/plot.py @@ -0,0 +1,898 @@ +#!/usr/bin/env python3 + +import argparse +import os +import pandas as pd +import matplotlib +import matplotlib.pyplot as plt +import numpy as np +import pudb +import math + +from typing import Callable + +instCombineDataDir = "../raw-data/InstCombine/" +hackersDelightDataDir = "../raw-data/HackersDelight/" +SMTLIBDataDir = "../raw-data/SMTLIB/" + + +def setGlobalDefaults(): + ## Use TrueType fonts instead of Type 3 fonts + # + # Type 3 fonts embed bitmaps and are not allowed in camera-ready submissions + # for many conferences. TrueType fonts look better and are accepted. + # This follows: https://www.conference-publishing.com/Help.php + matplotlib.rcParams["pdf.fonttype"] = 42 + matplotlib.rcParams["ps.fonttype"] = 42 + + ## Enable tight_layout by default + # + # This ensures the plot has always sufficient space for legends, ... + # Without this sometimes parts of the figure would be cut off. + matplotlib.rcParams["figure.autolayout"] = True + + ## Legend defaults + matplotlib.rcParams["legend.frameon"] = False + + # Hide the right and top spines + # + # This reduces the number of lines in the plot. Lines typically catch + # a readers attention and distract the reader from the actual content. + # By removing unnecessary spines, we help the reader to focus on + # the figures in the graph. + matplotlib.rcParams["axes.spines.right"] = False + matplotlib.rcParams["axes.spines.top"] = False + + +matplotlib.rcParams["figure.figsize"] = 14, 7 +matplotlib.rcParams.update({"font.size": 16}) + + +# Color palette +light_gray = "#cacaca" +dark_gray = "#827b7b" +light_blue = "#a6cee3" +dark_blue = "#1f78b4" +light_green = "#b2df8a" +dark_green = "#33a02c" +light_red = "#fb9a99" +dark_red = "#e31a1c" +black = "#000000" +white = "#ffffff" + +col = [ + "#a6cee3", + "#1f78b4", + "#b2df8a", + "#33a02c", + "#fb9a99", + "#e31a1c", + "#000000", + "#ffffff", +] + + +def save(figure, name): + # Do not emit a creation date, creator name, or producer. This will make the + # content of the pdfs we generate more deterministic. + metadata = {"CreationDate": None, "Creator": None, "Producer": None} + # plt.tight_layout() + plt.tight_layout() + + figure.savefig(name, metadata=metadata) + + # Close figure to avoid warning about too many open figures. + plt.close(figure) + + print(f"written to {name}") + + +# helper for str_from_float. +# format float in scientific with at most *digits* digits. +# +# precision of the mantissa will be reduced as necessary, +# as much as possible to get it within *digits*, but this +# can't be guaranteed for very large numbers. +def get_scientific(x: float, digits: int): + # get scientific without leading zeros or + in exp + def get(x: float, prec: int) -> str: + result = f"{x:.{prec}e}" + result = result.replace("e+", "e") + while "e0" in result: + result = result.replace("e0", "e") + while "e-0" in result: + result = result.replace("e-0", "e-") + return result + + result = get(x, digits) + len_after_e = len(result.split("e")[1]) + prec = max(0, digits - len_after_e - 2) + return get(x, prec) + + +# format float with at most *digits* digits. +# if the number is too small or too big, +# it will be formatted in scientific notation, +# optionally a suffix can be passed for the unit. +# +# note: this displays different numbers with different +# precision depending on their length, as much as can fit. +def str_from_float(x: float, digits: int = 3, suffix: str = "") -> str: + result = f"{x:.{digits}f}" + before_decimal = result.split(".")[0] + if len(before_decimal) == digits: + return before_decimal + if len(before_decimal) > digits: + # we can't even fit the integral part + return get_scientific(x, digits) + + result = result[: digits + 1] # plus 1 for the decimal point + if float(result) == 0: + # we can't even get one significant figure + return get_scientific(x, digits) + + return result[: digits + 1] + + +# Attach a text label above each bar in *rects*, displaying its height +def autolabel( + ax, + rects, + label_from_height: Callable[[float], str] = str_from_float, + xoffset=0, + yoffset=1, + **kwargs, +): + # kwargs is directly passed to ax.annotate and overrides defaults below + assert "xytext" not in kwargs, "use xoffset and yoffset instead of xytext" + default_kwargs = dict( + xytext=(xoffset, yoffset), + fontsize="smaller", + rotation=0, + ha="center", + va="bottom", + textcoords="offset points", + ) + + for rect in rects: + height = rect.get_height() + ax.annotate( + label_from_height(height), + xy=(rect.get_x() + rect.get_width() / 2, height), + **(default_kwargs | kwargs), + ) + + +# utility to print times as 1h4m, 1d15h, 143.2ms, 10.3s etc. +def str_from_ms(ms): + def maybe_val_with_unit(val, unit): + return f"{val}{unit}" if val != 0 else "" + + if ms < 1000: + return f"{ms:.3g}ms" + + s = ms / 1000 + ms = 0 + if s < 60: + return f"{s:.3g}s" + + m = int(s // 60) + s -= 60 * m + if m < 60: + return f'{m}m{maybe_val_with_unit(math.floor(s), "s")}' + + h = int(m // 60) + m -= 60 * h + if h < 24: + return f'{h}h{maybe_val_with_unit(m, "m")}' + + d = int(h // 24) + h -= 24 * d + return f'{d}d{maybe_val_with_unit(h, "h")}' + + +def autolabel_ms(ax, rects, **kwargs): + autolabel(ax, rects, label_from_height=str_from_ms, **kwargs) + + +# Plot an example speedup plot +def plot_speedup(): + labels = ["G1", "G2", "G3", "G4", "G5"] + men_means = [1.5, 1.2, 1.3, 1.1, 1.0] + women_means = [1.8, 1.5, 1.1, 1.3, 0.9] + + x = np.arange(len(labels)) # the label locations + width = 0.35 # the width of the bars + + fig, ax = plt.subplots() + rects1 = ax.bar(x - width / 2, men_means, width, label="Men", color=light_blue) + rects2 = ax.bar(x + width / 2, women_means, width, label="Women", color=dark_blue) + + # Y-Axis Label + # + # Use a horizontal label for improved readability. + ax.set_ylabel( + "Speedup", + rotation="horizontal", + position=(1, 1.05), + horizontalalignment="left", + verticalalignment="bottom", + ) + + # Add some text for labels, title and custom x-axis tick labels, etc. + ax.set_xticks(x) + ax.set_xticklabels(labels) + + ax.legend(ncol=100, loc="lower right", bbox_to_anchor=(0, 1, 1, 0)) + + autolabel(ax, rects1) + autolabel(ax, rects2) + + save(fig, "speedup.pdf") + + +def bar_bw_impact(dfs, bm, tool, bv_width): + i = 0 + fig, ax = plt.subplots() + width = 0.15 + items = [] + max = 0 + for i, bvw in enumerate(bv_width): + df = dfs[dfs["bvw"] == str(bvw)] + a = ax.bar( + np.arange(df.shape[0]) - width + (i - 1) * width, + df[tool], + width, + color=col[i], + label=bv_width[i], + ) + items.append(a) + if np.max(df[tool]) > max: + max = np.max(df[tool]) + ax.set_xlabel("Theorems") + ax.set_ylabel("Time [ms]", rotation="horizontal", horizontalalignment="left", y=1) + ax.set_yscale("log") + ax.set_xticks(np.arange(df.shape[0])) + ax.legend(loc="center right", ncols=1, frameon=False, bbox_to_anchor=(1.2, 0.5)) + # enable autolabel if necessary + # for a in items: + # autolabel(ax, a) + save(fig, tool + "_" + bm.split(".")[0] + ".pdf") + + +def compare_tools_same_bw(df, bm, tool1, tool2): + max = np.max(df[tool1]) + fig, ax = plt.subplots() + df_sorted = df.sort_values(by="leanSAT") + ax.plot( + np.arange(len(df_sorted[tool1])), df_sorted[tool1], color=col[0], label=tool1 + ) + ax.plot( + np.arange(len(df_sorted[tool2])), df_sorted[tool2], color=col[3], label=tool2 + ) + if np.max(df_sorted[tool2]) > max: + max = np.max(df_sorted[tool2]) + ax.set_xlabel("Theorems") + ax.set_ylabel("Time [ms]", rotation="horizontal", horizontalalignment="left", y=1) + ax.set_xticks(np.arange(len(df[tool1]))) + ax.legend(loc="center right", ncols=1, frameon=False, bbox_to_anchor=(1.2, 0.5)) + ax.set_yscale("log") + save(fig, tool1 + "_" + tool2 + "_" + bm.split(".")[0] + ".pdf") + + +def compare_tools_diff_bw(dfs, bm, tool1, tool2, bv_width): + fig, ax = plt.subplots() + width = 0.15 + max = 0.0 + for i, bvw in enumerate(bv_width): + df = dfs[dfs["bvw"] == str(bvw)] + ax.bar( + np.arange(len(df[tool1])) - width + (i - 1) * width, + np.subtract(df[tool1], df[tool2]), + width, + color=col[i], + label=bv_width[i], + ) + i = i + 1 + if np.max(np.subtract(df[tool1], df[tool2])) > max: + max = np.max(np.subtract(df[tool1], df[tool2])) + ax.set_xlabel("Theorems") + ax.set_ylabel("Time [ms]", rotation="horizontal", horizontalalignment="left", y=1) + ax.set_xticks(np.arange(len(df[tool1]))) + ax.legend(loc="center right", ncols=1, frameon=False, bbox_to_anchor=(1.2, 0.5)) + save(fig, tool1 + "_" + tool2 + "_diff_" + bm.split(".")[0] + ".pdf") + +def leanSAT_tot_stacked_perc(df, bm, type): + if type == 'h_tot': + matplotlib.rcParams["figure.figsize"] = 14, 3 + x = np.arange(len(df["leanSAT"])) + width = 1.0 + fig, ax = plt.subplots(figsize=(14, 3.5)) + # df_sorted = df.sort_values(by="leanSAT") + # print(df_sorted) + tot_sum = (df["leanSAT-rw"] + df["leanSAT-bb"]+ df["leanSAT-sat"]+ df["leanSAT-lrat-t"]+ df["leanSAT-lrat-c"]) + df['tot-sum'] = tot_sum + df_sorted = df.sort_values(by="tot-sum") + # print(df_sorted) + ax_right = ax.twinx() + + ax.bar( + x, + np.divide(df_sorted["leanSAT-rw"],df_sorted['tot-sum'])*100, + width, + label="rewriting", + bottom=np.zeros_like(df_sorted["leanSAT-rw"]), + color=dark_blue, + edgecolor = dark_blue + ) + ax.bar( + x, + np.divide(df_sorted["leanSAT-bb"]+df_sorted["leanSAT-sat"], df_sorted['tot-sum'])*100, + width, + label="bit-blasting and SAT solving", + bottom=np.divide(df_sorted["leanSAT-rw"],df_sorted['tot-sum'])*100, + color=light_gray, + edgecolor=light_gray + ) + ax.bar( + x, + np.divide(df_sorted["leanSAT-lrat-t"] +df_sorted["leanSAT-lrat-c"], df_sorted['tot-sum'])*100, + width, + label="LRAT", + bottom=np.divide(df_sorted["leanSAT-rw"],df_sorted['tot-sum'])*100 + + np.divide(df_sorted["leanSAT-bb"]+df_sorted["leanSAT-sat"], df_sorted['tot-sum'])*100, + color=dark_green, + edgecolor=dark_green + ) + ax_right.plot( + x, + df_sorted['tot-sum'], + width, + label="total time", + color=black, + ) + ax_right.set_yscale("log") + ax.set_xticks(np.arange(0,len(df_sorted), 10**np.floor(np.log10(len(df_sorted))))) + # ax.set_title("Time to solve theorems from "+bm, pad=20) + ax.set_ylabel("Distribution [%]", rotation="horizontal", horizontalalignment="left", y=1.05) + ax_right.set_ylabel("Time [ms]", rotation="horizontal", horizontalalignment="right", y=1.08) + ax.legend(ncols=4, frameon=False, bbox_to_anchor= [0.5, 1], loc='lower center') + plt.gca().spines['right'].set_visible(True) + save(fig, "leanSAT_stacked_perc_" + bm.split(".")[0] + ".pdf") + + +def leanSAT_smtlib_unsat_stacked_perc(df: pd.DataFrame, bm, type): + if type == 'h_tot': + matplotlib.rcParams["figure.figsize"] = 14, 5 + x = np.arange(len(df["benchmark"])) + width = 1.0 + fig, ax = plt.subplots() + # df_sorted = df.sort_values(by="leanSAT") + # print(df_sorted) + df = df.apply(lambda x: x / 10**6 if x.name in + ['leanSAT-ld', 'leanSAT-rr', 'leanSAT-ac', + 'leanSAT-af', 'leanSAT-ecs', 'leanSAT-bb', + 'leanSAT-sat', 'leanSAT-lrat', 'leanSAT-kc'] else x) + tot_sum = (df["leanSAT-ld"] + df["leanSAT-rr"] + df["leanSAT-ac"] + + df["leanSAT-af"] + df["leanSAT-ecs"] + df["leanSAT-bb"] + + df["leanSAT-sat"] + df["leanSAT-lrat"] + df["leanSAT-kc"]) + df['tot-sum'] = tot_sum + df_sorted = df.sort_values(by="tot-sum") + # print(df_sorted) + ax_right = ax.twinx() + + bottom = np.zeros_like(df_sorted["leanSAT-ld"]) + ax.bar( + x, + np.divide(df_sorted["leanSAT-ld"] + df_sorted["leanSAT-rr"] + + df_sorted["leanSAT-ac"] + df_sorted["leanSAT-af"] + + df_sorted["leanSAT-ecs"] + df_sorted["leanSAT-kc"], df_sorted['tot-sum'])*100, + width, + label="rewriting + kernel checking", + bottom=bottom, + color=dark_blue, + edgecolor = dark_blue + ) + bottom += np.divide(df_sorted["leanSAT-ld"] + df_sorted["leanSAT-rr"] + + df_sorted["leanSAT-ac"] + df_sorted["leanSAT-af"] + + df_sorted["leanSAT-ecs"] + df_sorted["leanSAT-kc"], df_sorted['tot-sum'])*100 + ax.bar( + x, + np.divide(df_sorted["leanSAT-bb"] + df_sorted["leanSAT-sat"], + df_sorted['tot-sum'])*100, + width, + label="bit-blasting and SAT solving", + bottom=bottom, + color=light_gray, + edgecolor=light_gray + ) + bottom += np.divide(df_sorted["leanSAT-bb"] + df_sorted["leanSAT-sat"], df_sorted['tot-sum'])*100 + ax.bar( + x, + np.divide(df_sorted["leanSAT-lrat"], df_sorted['tot-sum'])*100, + width, + label="LRAT", + bottom=bottom, + color=dark_green, + edgecolor=dark_green + ) + ax_right.plot( + x, + df_sorted['tot-sum'], + width, + label="total time", + color=black, + ) + ax_right.set_yscale("log") + ax.set_xticks(np.arange(0,len(df_sorted), 10**np.floor(np.log10(len(df_sorted))))) + # ax.set_title("Time to solve theorems from "+bm, pad=20) + ax.set_ylabel("Distribution [%]", rotation="horizontal", horizontalalignment="left", y=1.05) + ax_right.set_ylabel("Time [ms]", rotation="horizontal", horizontalalignment="right", y=1.08) + ax.legend(ncols=4, frameon=False, bbox_to_anchor= [0.5, 1], loc='lower center') + plt.gca().spines['right'].set_visible(True) + save(fig, "leanSAT_stacked_smtlib_" + bm.split(".")[0] + ".pdf") + + +def leanSAT_smtlib_sat_stacked_perc(df: pd.DataFrame, bm, type): + if type == 'h_tot': + matplotlib.rcParams["figure.figsize"] = 14, 5 + x = np.arange(len(df["benchmark"])) + width = 1.0 + fig, ax = plt.subplots() + # df_sorted = df.sort_values(by="leanSAT") + # print(df_sorted) + df = df.apply(lambda x: x / 10**6 if x.name in + ['leanSAT-ld', 'leanSAT-rr', 'leanSAT-ac', + 'leanSAT-af', 'leanSAT-ecs', 'leanSAT-bb', + 'leanSAT-sat', 'leanSAT-lrat'] else x) + tot_sum = (df["leanSAT-ld"] + df["leanSAT-rr"] + df["leanSAT-ac"] + + df["leanSAT-af"] + df["leanSAT-ecs"] + df["leanSAT-bb"] + + df["leanSAT-sat"] + df["leanSAT-lrat"]) + df['tot-sum'] = tot_sum + df_sorted = df.sort_values(by="tot-sum") + # print(df_sorted) + ax_right = ax.twinx() + + bottom = np.zeros_like(df_sorted["leanSAT-ld"]) + ax.bar( + x, + np.divide(df_sorted["leanSAT-ld"] + df_sorted["leanSAT-rr"] + + df_sorted["leanSAT-ac"] + df_sorted["leanSAT-af"] + + df_sorted["leanSAT-ecs"], df_sorted['tot-sum'])*100, + width, + label="rewriting", + bottom=bottom, + color=dark_blue, + edgecolor = dark_blue + ) + bottom += np.divide(df_sorted["leanSAT-ld"] + df_sorted["leanSAT-rr"] + + df_sorted["leanSAT-ac"] + df_sorted["leanSAT-af"] + + df_sorted["leanSAT-ecs"], df_sorted['tot-sum'])*100 + ax.bar( + x, + np.divide(df_sorted["leanSAT-bb"] + df_sorted["leanSAT-sat"], + df_sorted['tot-sum'])*100, + width, + label="bit-blasting and SAT solving", + bottom=bottom, + color=light_gray, + edgecolor=light_gray + ) + ax_right.plot( + x, + df_sorted['tot-sum'], + width, + label="total time", + color=black, + ) + ax_right.set_yscale("log") + ax.set_xticks(np.arange(0,len(df_sorted), 10**np.floor(np.log10(len(df_sorted))))) + # ax.set_title("Time to solve theorems from "+bm, pad=20) + ax.set_ylabel("Distribution [%]", rotation="horizontal", horizontalalignment="left", y=1.05) + ax_right.set_ylabel("Time [ms]", rotation="horizontal", horizontalalignment="right", y=1.08) + ax.legend(ncols=4, frameon=False, bbox_to_anchor= [0.5, 1], loc='lower center') + plt.gca().spines['right'].set_visible(True) + save(fig, "leanSAT_stacked_smtlib_" + bm.split(".")[0] + ".pdf") + + +def leanSAT_tot_stacked(df, bm): + x = np.arange(len(df["leanSAT"])) + width = 0.45 + fig, ax = plt.subplots() + df_sorted = df.sort_values(by="leanSAT") + # print(df_sorted) + colors_in_order = [ + "#e31a1c", + "#9ecae1", + "#deebf7", + "#74c476", + "#bae4b3" + ] + ax.bar( + x, + df_sorted["leanSAT-rw"], + width, + label="rewriting", + bottom=np.zeros_like(df_sorted["leanSAT-rw"]), + color=colors_in_order[0], + ) + ax.bar( + x, + df_sorted["leanSAT-bb"], + width, + label="bit-blasting", + bottom=df_sorted["leanSAT-rw"], + color=colors_in_order[1], + ) + ax.bar( + x, + df_sorted["leanSAT-sat"], + width, + label="sat solving", + bottom=np.array(df_sorted["leanSAT-rw"]) + np.array(df_sorted["leanSAT-bb"]), + color=colors_in_order[2], + ) + ax.bar( + x, + df_sorted["leanSAT-lrat-t"], + width, + label="lrat-trimming", + bottom=np.array(df_sorted["leanSAT-rw"]) + + np.array(df_sorted["leanSAT-bb"]) + + np.array(df_sorted["leanSAT-sat"]), + color=colors_in_order[3], + ) + ax.bar( + x, + df_sorted["leanSAT-lrat-c"], + width, + label="lrat-checking", + bottom=np.array(df_sorted["leanSAT-rw"]) + + np.array(df_sorted["leanSAT-bb"]) + + np.array(df_sorted["leanSAT-sat"]) + + np.array(df_sorted["leanSAT-lrat-t"]), + color=colors_in_order[4], + ) + # ax.set_yscale("log") + ax.set_xticks(np.arange(0,len(df_sorted),len(df_sorted)-1)) + ax.set_title("Time to solve theorems from "+bm, pad=20) + ax.set_ylabel("Time [ms]", rotation="horizontal", horizontalalignment="left", y=1) + ax.legend(loc="best", ncols=1, frameon=False) + save(fig, "leanSAT_stacked_" + bm.split(".")[0] + ".pdf") + +def leanSAT_tot_stacked_area(df, bm): + x = np.arange(len(df["leanSAT"])) + fig, ax = plt.subplots() + df_sorted = df.sort_values(by="leanSAT") + x = np.arange(len(df["leanSAT"])) + fig, ax = plt.subplots() + colors_in_order = [ + "#bdd7e7", + "#6baed6", + "#3182bd", + "#bae4b3", + "#74c476" + ] + ax.stackplot( + x, + df_sorted["leanSAT-rw"], + df_sorted["leanSAT-bb"], + df_sorted["leanSAT-sat"], + df_sorted["leanSAT-lrat-t"], + df_sorted["leanSAT-lrat-c"], + labels=["rw","bb","sat","lrat-t","lrats"], + colors=colors_in_order + ) + + ax.set_yscale("log") + ax.set_xticks(np.arange(0,51,50)) + ax.set_xlabel("Theorems") + ax.set_ylabel("Time [ms]", rotation="horizontal", horizontalalignment="left", y=1) + ax.legend(loc="center right", ncols=1, frameon=False, bbox_to_anchor=(1.2, 0.5)) + save(fig, "leanSAT_stacked_area_" + bm.split(".")[0] + ".pdf") + +# for hackers delight we want to consider bitwidth in the plotting +def cumul_solving_time_hackers_delight(df, tool1, tool2, bm, bv_width): + matplotlib.rcParams["figure.figsize"] = 14, 5 + + + fig, ax = plt.subplots(1,3) + for i, bvw in enumerate([4, 16, 64]): + dfs = [] + df_tmp = df.loc[df["bvw"] == str(bvw)] + df_sorted = df_tmp.sort_values(by="leanSAT") + + sorted1 = np.sort(df_sorted[tool1]) + sorted2 = np.sort(df_sorted[tool2]) + cumtime1 = [0] + cumtime1.extend(np.cumsum(sorted1)) + cumtime2 = [0] + cumtime2.extend(np.cumsum(sorted2)) + + ax[i].plot( + cumtime1, + np.arange(0, len(df_sorted[tool1]) + 1), + marker="o", + color=col[0], + label='bv_decide', + ) + ax[i].plot( + cumtime2, + np.arange(0, len(df_sorted[tool2]) + 1), + marker="x", + color=col[3], + label=tool2, + ) + ax[i].set_xlabel('bitwidth: '+str(bvw)) + ax[i].set_xscale('log') + ax[0].set_ylabel("Problems solved", rotation="vertical", ha="center") + # ax.set_yscale("log") + ax[1].set_title("bv_decide vs. Bitwuzla Scaling Solving Hackers' Delight Theorems") + ax[0].legend(loc="upper left", ncols=1, frameon=False) + ax[1].text(0.5, -0.28, "Cumulative Time [ms]", transform=ax[1].transAxes, ha="center") + save(fig, "cumul_problems_bv_4_16_64_" + bm.split(".")[0] + ".pdf") + +def cumul_solving_time(df, tool1, tool2, bm): + fig, ax = plt.subplots(figsize=(14, 3)) + sorted1 = np.sort(df[tool1]) + sorted2 = np.sort(df[tool2]) + cumtime1 = [0] + cumtime1.extend(np.cumsum(sorted1)) + cumtime2 = [0] + cumtime2.extend(np.cumsum(sorted2)) + ax.plot( + cumtime1, + np.arange(0, len(df[tool1]) + 1), + marker="o", + color=col[0], + label='bv_decide', + ) + ax.plot( + cumtime2, + np.arange(0, len(df[tool2]) + 1), + marker="x", + color=col[3], + label=tool2, + ) + ax.set_xlabel("Time [ms]") + ax.set_xscale('log') + ax.set_ylabel("Problems solved", rotation="horizontal", ha="left", y=1) + # ax.set_xscale("log") + # ax.set_yscale("log") + ax.legend(loc="upper left", ncols=1, frameon=False) + # ax.legend(loc="center right", ncols=1, frameon=False, bbox_to_anchor=(1.2, 0.5)) + save(fig, "cumul_problems_llvm_" + bm.split(".")[0] + ".pdf") + +def cumul_solving_time_smtlib(df, name): + fig, ax = plt.subplots(figsize=(14, 3)) + plt.rcParams["path.simplify_threshold"] = 1 + # only consider rows where the problem was actually sat/unsat + sorted1 = np.sort(df['time_cpu_bw']) + sorted2 = np.sort(df['time_cpu_lw']) + sorted3 = np.sort(df['time_cpu_coq']) + cumtime1 = [0] + cumtime1.extend(np.cumsum(sorted1)) + cumtime2 = [0] + cumtime2.extend(np.cumsum(sorted2)) + cumtime3 = [0] + cumtime3.extend(np.cumsum(sorted3)) + ax.plot( + cumtime1, + np.arange(0, len(df['time_cpu_bw']) + 1), + marker="o", + color=dark_green, + label='bitwuzla', + ) + ax.plot( + cumtime2, + np.arange(0, len(df['time_cpu_lw']) + 1), + marker="x", + color=light_blue, + label='bv_decide', + ) + ax.plot( + cumtime3, + np.arange(0, len(df['time_cpu_coq']) + 1), + marker="*", + color=dark_red, + label='CoqQFBV', + ) + ax.set_xscale('log') + ax.set_xlabel("Time [s] - "+name.upper()+" results") + ax.set_ylabel("Problems solved", rotation="horizontal", ha="left", y=1) + # add a line to highlight the difference in #solved problems between the tools + # x_start = cumtime1[len([x for x in np.array(df['time_cpu_lw']) if x > 0])-10] + # x_end = np.sum(df['time_cpu_lw']) + # y_value = len([x for x in np.array(df['time_cpu_lw']) if x > 0]) + # ax.plot([x_start, x_end], [len([x for x in np.array(df['time_cpu_lw']) if x > 0]), len([x for x in np.array(df['time_cpu_lw']) if x > 0])], color='black', linestyle='--', linewidth=1) + # ax.annotate(f"10^{int(np.round(np.log10(x_end - x_start)))} s", + # xy=(x_start+(x_end-x_start)/2, y_value), + # xytext=((x_end-x_start)/2, y_value * 1.01), + # fontsize=12, color='black') + + # x_start_c = cumtime1[len([x for x in np.array(df['time_cpu_coq']) if x > 0])-10] + # x_end_c = np.sum(df['time_cpu_coq']) + # y_value_c = len([x for x in np.array(df['time_cpu_coq']) if x > 0]) + # ax.plot([x_start_c, x_end_c], [len([x for x in np.array(df['time_cpu_coq']) if x > 0]), len([x for x in np.array(df['time_cpu_coq']) if x > 0])], color='black', linestyle='--', linewidth=1) + # ax.annotate(f"10^{int(np.round(np.log10(x_end_c - x_start_c)))} s", + # xy=(x_start_c, y_value_c), + # xytext=((x_end_c-x_start_c)/2, y_value_c * 1.01), + # fontsize=12, color='black') + + # y_start = next((i for i, x in enumerate(cumtime2) if x > np.sum(df['time_cpu_bw'])), -1) + # y_end = len(df['time_cpu_bw']) + # print(cumtime1[-1]) + # x_value = np.sum(df['time_cpu_bw']) + # ax.plot([x_value, x_value], [y_start, y_end], color='black', linestyle='dashed', linewidth=1) + # y_end = next((i for i, x in enumerate(cumtime2) if x > np.sum(df['time_cpu_bw'])), -1) + # y_start = 0 + # print(cumtime1[-1]) + # x_value = np.sum(df['time_cpu_bw']) + # ax.plot([x_value, x_value], [y_start, y_end], color='black', linestyle='solid', linewidth=2) + # ax.annotate(f"{int(y_end)} problems", + # xy=(x_start, y_value), + # xytext=(x_value*1.1, y_end * 0.95), + # fontsize=12, color='black') + + # x_start_c = cumtime1[len([x for x in np.array(df['time_cpu_coq']) if x > 0])-10] + # x_end_c = np.sum(df['time_cpu_coq']) + # y_value_c = len([x for x in np.array(df['time_cpu_coq']) if x > 0]) + # ax.plot([x_start_c, x_end_c], [len([x for x in np.array(df['time_cpu_coq']) if x > 0]), len([x for x in np.array(df['time_cpu_coq']) if x > 0])], color='black', linestyle='--', linewidth=1) + # ax.annotate(f"10^{int(np.round(np.log10(x_end_c - x_start_c)))} s", + # xy=(x_start_c, y_value_c), + # xytext=((x_end_c-x_start_c)/2, y_value_c * 1.01), + # fontsize=12, color='black') + + # ax.axvline(np.sum(df['time_cpu_bw']), color = black, linestyle = '--') + # ax.set_xscale("log") + # ax.set_yscale("log") + # ax.legend(loc="center right", ncols=1, frameon=False, bbox_to_anchor=(1.2, 0.5)) + ax.legend(loc="upper left", ncols=1, frameon=False) + save(fig, "cumul_problems_smtlib_"+name+".pdf") + +def scatter_solving_time_smtlib(df_sat, df_unsat): + fig, ax = plt.subplots(1, 2, figsize=(14, 4), sharey=True) + + ax[0].scatter(df_sat['time_cpu_bw'], df_sat['time_cpu_lw'], c = "#beaed4", label = 'SAT results', marker = ".") + ax[1].scatter(df_unsat['time_cpu_bw'], df_unsat['time_cpu_lw'], c = "#fdc086", label = 'UNSAT results', marker=".") + + ax[0].set_xlabel("SAT") + ax[1].set_xlabel("UNSAT") + + time_sat_min = min(df_sat["time_cpu_bw"].min(), df_sat["time_cpu_lw"].min()) + time_sat_max = max(df_sat["time_cpu_bw"].max(), df_sat["time_cpu_lw"].max()) + + time_unsat_min = min(df_unsat["time_cpu_bw"].min(), df_unsat["time_cpu_lw"].min()) + time_unsat_max = max(df_unsat["time_cpu_bw"].max(), df_unsat["time_cpu_lw"].max()) + + time_min = min(time_sat_min, time_sat_max) + time_max = max(time_sat_max, time_unsat_max) + + ax[0].set_ylim(10**(np.floor(np.log10(time_min))), 10**(np.floor(np.log10(time_max)))) + ax[1].set_ylim(10**(np.floor(np.log10(time_min))), 10**(np.floor(np.log10(time_max)))) + ax[0].plot([df_sat["time_cpu_bw"].min(), df_sat["time_cpu_bw"].max()], [df_sat["time_cpu_bw"].min(), df_sat["time_cpu_bw"].max()], c = black) + ax[1].plot([df_unsat["time_cpu_bw"].min(), df_unsat["time_cpu_lw"].max()], [df_unsat["time_cpu_bw"].min(), df_unsat["time_cpu_lw"].max()], c = black) + ax[0].set_xscale('log') + ax[0].set_yscale('log') + ax[1].set_xscale('log') + ax[1].set_yscale('log') + # ax[1].text(1.2, 0, "Time [ms]\nbitwuzla", transform=ax[1].transAxes, ha="right") + fig.text(0.5, 0.04, "Time [ms] - bitwuzla", ha="center", va="center") + ax[0].set_ylabel("Time [s] - bv_decide", rotation="horizontal", ha="left", y=1.05) + # ax.legend(loc="lower center", ncols=2, frameon=False) + save(fig, "scatter_smtlib.pdf") + +def scatter_solving_time_instcombine(df): + fig, ax = plt.subplots(figsize=(14, 3), sharey=True) + tot_sum = (df["leanSAT-rw"] + df["leanSAT-bb"]+ df["leanSAT-sat"]+ df["leanSAT-lrat-t"]+ df["leanSAT-lrat-c"]) + ax.scatter(df['bitwuzla'], tot_sum, c = "#beaed4", marker = ".") + + ax.set_xlabel("T") + + time_min = min(df["bitwuzla"].min(), tot_sum.min()) + time_max = min(df["bitwuzla"].max(), tot_sum.max()) + + ax.set_ylim(10**(np.floor(np.log10(time_min))), 10**(np.ceil(np.log10(time_max)))) + ax.plot([df["bitwuzla"].min(), tot_sum.max()], [df["bitwuzla"].min(), tot_sum.max()], c = black) + ax.set_xscale('log') + ax.set_yscale('log') + # ax[1].text(1.2, 0, "Time [ms]\nbitwuzla", transform=ax[1].transAxes, ha="right") + ax.set_xlabel("Time [ms] - bitwuzla", ha="center", va="center", y = -0.2) + ax.set_ylabel("Time [ms] - bv_decide", rotation="horizontal", ha="left", y=1.05) + # ax.legend(loc="lower center", ncols=2, frameon=False) + save(fig, "scatter_smtlib_instcombine.pdf") + + +def plot_hackersdelight(): + dfs = [] + for file in os.listdir(hackersDelightDataDir): + if 'err' not in file and 'ceg' not in file and 'sym' not in file: + bvw = file.split('_')[0].split('w')[1] + df_bw = pd.read_csv(hackersDelightDataDir + file) + df_sorted = df_bw.sort_values(by="leanSAT") + if len(df_sorted > 0): + compare_tools_same_bw(df_bw, file, "leanSAT", "bitwuzla") + leanSAT_tot_stacked(df_bw, file) + leanSAT_tot_stacked_perc(df_bw, file, 'h') + leanSAT_tot_stacked_area(df_bw, file) + df_sorted.insert(1, 'bvw', [bvw] * len(df_sorted), True) + df_sorted.insert(1, 'filename', file.split('_')[1]+'_'+file.split('_')[2], True) + dfs.append(df_sorted) + + + df = pd.concat(dfs, axis = 0) + + df.to_csv('gigantic-df.csv') + + bv_width = df["bvw"].unique() + + file = "HackersDelight" + df_new = df[df["bvw"] == str(64)] + leanSAT_tot_stacked(df_new, file+'_bvw64') + leanSAT_tot_stacked_perc(df_new, file+'_bvw64', 'h_tot') + + cumul_solving_time_hackers_delight(df, "leanSAT", "bitwuzla", file, bv_width) + + bar_bw_impact(df, file, "bitwuzla", bv_width) + bar_bw_impact(df, file, "leanSAT", bv_width) + compare_tools_diff_bw(df, file, "leanSAT", "bitwuzla", bv_width) + +def plot_instcombine(): + for file in os.listdir(instCombineDataDir): + if 'err' not in file and 'ceg' not in file: + df = pd.read_csv(instCombineDataDir + file) + cumul_solving_time(df, "leanSAT", "bitwuzla", file) + leanSAT_tot_stacked(df, 'instCombine') + leanSAT_tot_stacked_perc(df, 'instCombine', 'i') + leanSAT_tot_stacked_area(df, 'instCombine') + scatter_solving_time_instcombine(df) + +def plot_smtlib(): + # filter out results that are unknown for both solvers + df_bitwuzla_46k = pd.read_csv(SMTLIBDataDir + 'bitwuzla_46k.csv') + df_leanwuzla_46k = pd.read_csv(SMTLIBDataDir + 'leanwuzla_46k.csv') + df_coq_46k = pd.read_csv(SMTLIBDataDir + 'coq_46k.csv') + df_bitwuzla_46k_no_unknowns = df_bitwuzla_46k[df_bitwuzla_46k['result'] != 'unknown'] + df_leanwuzla_46k_no_unknowns = df_leanwuzla_46k[df_leanwuzla_46k['result'] != 'unknown'] + df_coq_46k_no_unknowns = df_coq_46k[df_coq_46k['result'] != 'unknown'] + df_coq_46k_no_unknowns = df_coq_46k_no_unknowns.rename(columns = lambda x : x + '_coq' if x != 'benchmark' else x) + merged_df = pd.merge(df_bitwuzla_46k_no_unknowns, df_leanwuzla_46k_no_unknowns, how = 'outer', on = 'benchmark', suffixes = ('_bw', '_lw')) + merged_df_tot = pd.merge(merged_df, df_coq_46k_no_unknowns, how = 'outer', on = 'benchmark') + df_sat = merged_df_tot.loc[lambda x: (x['result_bw'] == 'sat') | (x['result_lw'] == 'sat') | (x['result_coq'] == 'sat')] + df_unsat = merged_df_tot.loc[lambda x: (x['result_bw'] == 'unsat') | (x['result_lw'] == 'unsat') | (x['result_coq'] == 'unsat')] + # separate sat from unsat + cumul_solving_time_smtlib(df_sat, 'sat') + cumul_solving_time_smtlib(df_unsat, 'unsat') + scatter_solving_time_smtlib(df_sat, df_unsat) + # plot stacked area plot + df_leanwuzla_46k_stats = pd.read_csv(SMTLIBDataDir + 'leanwuzla_46k_stats.csv') + df_sat_stats = df_leanwuzla_46k_stats[df_leanwuzla_46k_stats['leanSAT-res'] == 'sat'] + df_unsat_stats = df_leanwuzla_46k_stats[df_leanwuzla_46k_stats['leanSAT-res'] == 'unsat'] + leanSAT_smtlib_sat_stacked_perc(df_sat_stats, 'sat', 'i') + leanSAT_smtlib_unsat_stacked_perc(df_unsat_stats, 'unsat', 'i') + + +def main(): + parser = argparse.ArgumentParser( + prog="plot", + description="Plot the figures for this paper", + ) + parser.add_argument( + "names", nargs="+", choices=["all", "hackersdelight", "instcombine", "smtlib"] + ) + args = parser.parse_args() + + setGlobalDefaults() + + if "all" in args.names or "hackersdelight" in args.names: + plot_hackersdelight() + + if "all" in args.names or "instcombine" in args.names: + plot_instcombine() + + if "all" in args.names or "smtlib" in args.names: + plot_smtlib() + + +if __name__ == "__main__": + main() \ No newline at end of file diff --git a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_16_r0.txt b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_16_r0.txt index c105f64750..34ca15734d 100644 --- a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_16_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_16_r0.txt @@ -1,18 +1,18 @@ -Bitwuzla proved the goal after 70.395738ms, solving context: 0.000000ms -LeanSAT proved the goal after 73.426402ms: rewriting 10.212120ms, bitblasting 0.000000ms, SAT solving 59.297662ms, LRAT trimming 0.000000ms, LRAT checking 1.583640ms -Bitwuzla proved the goal after 70.577480ms, solving context: 0.000000ms -LeanSAT proved the goal after 73.895859ms: rewriting 10.834020ms, bitblasting 0.000000ms, SAT solving 59.350389ms, LRAT trimming 0.000000ms, LRAT checking 1.412380ms -Bitwuzla proved the goal after 7.571740ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.620960ms: rewriting 7.605910ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 73.845570ms, solving context: 0.000000ms -LeanSAT proved the goal after 79.697419ms: rewriting 14.503850ms, bitblasting 0.000000ms, SAT solving 59.228619ms, LRAT trimming 1.123160ms, LRAT checking 3.552650ms -Bitwuzla proved the goal after 7.236630ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.189910ms: rewriting 7.176410ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 68.681271ms, solving context: 0.000000ms -LeanSAT proved the goal after 72.363430ms: rewriting 9.216790ms, bitblasting 0.000000ms, SAT solving 59.256370ms, LRAT trimming 0.000000ms, LRAT checking 1.391460ms -Bitwuzla proved the goal after 68.808100ms, solving context: 0.000000ms -LeanSAT proved the goal after 72.109000ms: rewriting 9.270100ms, bitblasting 0.000000ms, SAT solving 59.269240ms, LRAT trimming 0.000000ms, LRAT checking 1.000130ms -Bitwuzla proved the goal after 75.912630ms, solving context: 0.000000ms -LeanSAT proved the goal after 86.227989ms: rewriting 16.287970ms, bitblasting 0.000000ms, SAT solving 59.217289ms, LRAT trimming 3.063990ms, LRAT checking 5.969070ms -Bitwuzla proved the goal after 75.689599ms, solving context: 1.000000ms -LeanSAT proved the goal after 89.330811ms: rewriting 16.239951ms, bitblasting 0.000000ms, SAT solving 59.372361ms, LRAT trimming 4.609639ms, LRAT checking 7.475820ms +Bitwuzla proved the goal after 13.445142ms, solving context: 0.000000ms +LeanSAT proved the goal after 13.024632ms: rewriting 13.008442ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 12.794033ms, solving context: 0.000000ms +LeanSAT proved the goal after 12.713904ms: rewriting 12.708594ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.861705ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.722857ms: rewriting 14.717758ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.082400ms, solving context: 0.000000ms +LeanSAT proved the goal after 61.999764ms: rewriting 5.768749ms, bitblasting 0.062717ms, SAT solving 52.642146ms, LRAT trimming 0.397057ms, LRAT checking 2.712099ms +Bitwuzla proved the goal after 15.713367ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.214741ms: rewriting 15.207046ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 57.399659ms, solving context: 0.000000ms +LeanSAT proved the goal after 60.104428ms: rewriting 3.814137ms, bitblasting 0.038853ms, SAT solving 53.051693ms, LRAT trimming 0.319945ms, LRAT checking 2.435827ms +Bitwuzla proved the goal after 57.955839ms, solving context: 0.000000ms +LeanSAT proved the goal after 59.684952ms: rewriting 4.060605ms, bitblasting 0.040144ms, SAT solving 52.843299ms, LRAT trimming 0.321107ms, LRAT checking 1.985369ms +Bitwuzla proved the goal after 60.649515ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.287152ms: rewriting 6.876057ms, bitblasting 0.063397ms, SAT solving 52.821771ms, LRAT trimming 1.733411ms, LRAT checking 4.282397ms +Bitwuzla proved the goal after 59.742076ms, solving context: 1.000000ms +LeanSAT proved the goal after 67.074382ms: rewriting 6.501401ms, bitblasting 0.079417ms, SAT solving 53.071041ms, LRAT trimming 1.842845ms, LRAT checking 5.019107ms diff --git a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_32_r0.txt b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_32_r0.txt index 149522881a..10671dfd26 100644 --- a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_32_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_32_r0.txt @@ -1,18 +1,18 @@ -Bitwuzla proved the goal after 70.680310ms, solving context: 0.000000ms -LeanSAT proved the goal after 74.436730ms: rewriting 10.242250ms, bitblasting 0.000000ms, SAT solving 59.244820ms, LRAT trimming 0.000000ms, LRAT checking 3.040370ms -Bitwuzla proved the goal after 70.168432ms, solving context: 0.000000ms -LeanSAT proved the goal after 74.845588ms: rewriting 10.804620ms, bitblasting 0.000000ms, SAT solving 59.282818ms, LRAT trimming 0.000000ms, LRAT checking 2.849240ms -Bitwuzla proved the goal after 7.608389ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.510090ms: rewriting 7.497310ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 73.440149ms, solving context: 1.000000ms -LeanSAT proved the goal after 83.055341ms: rewriting 14.328861ms, bitblasting 0.000000ms, SAT solving 59.158321ms, LRAT trimming 2.420630ms, LRAT checking 5.280859ms -Bitwuzla proved the goal after 7.164650ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.141680ms: rewriting 7.128370ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 68.602529ms, solving context: 1.000000ms -LeanSAT proved the goal after 73.691121ms: rewriting 9.132620ms, bitblasting 0.000000ms, SAT solving 59.416571ms, LRAT trimming 0.000000ms, LRAT checking 2.979060ms -Bitwuzla proved the goal after 68.842899ms, solving context: 1.000000ms -LeanSAT proved the goal after 73.289520ms: rewriting 9.186900ms, bitblasting 0.000000ms, SAT solving 59.369150ms, LRAT trimming 0.000000ms, LRAT checking 1.661820ms -Bitwuzla proved the goal after 75.850279ms, solving context: 0.000000ms -LeanSAT proved the goal after 96.313090ms: rewriting 16.203730ms, bitblasting 0.000000ms, SAT solving 59.399350ms, LRAT trimming 7.197830ms, LRAT checking 10.965020ms -Bitwuzla proved the goal after 75.504969ms, solving context: 2.000000ms -LeanSAT proved the goal after 96.813070ms: rewriting 16.052260ms, bitblasting 0.000000ms, SAT solving 59.332770ms, LRAT trimming 7.446400ms, LRAT checking 11.509130ms +Bitwuzla proved the goal after 13.532786ms, solving context: 0.000000ms +LeanSAT proved the goal after 13.126972ms: rewriting 13.111914ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 12.927852ms, solving context: 0.000000ms +LeanSAT proved the goal after 12.864213ms: rewriting 12.858764ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.824706ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.786485ms: rewriting 14.781466ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.022411ms, solving context: 0.000000ms +LeanSAT proved the goal after 64.106487ms: rewriting 5.755143ms, bitblasting 0.101759ms, SAT solving 52.952401ms, LRAT trimming 1.048589ms, LRAT checking 3.723346ms +Bitwuzla proved the goal after 16.513304ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.752620ms: rewriting 15.745527ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 57.222227ms, solving context: 1.000000ms +LeanSAT proved the goal after 60.883482ms: rewriting 3.872716ms, bitblasting 0.057056ms, SAT solving 52.986217ms, LRAT trimming 0.447071ms, LRAT checking 2.936916ms +Bitwuzla proved the goal after 57.657223ms, solving context: 1.000000ms +LeanSAT proved the goal after 60.719917ms: rewriting 4.098216ms, bitblasting 0.065091ms, SAT solving 53.049023ms, LRAT trimming 0.462008ms, LRAT checking 2.458218ms +Bitwuzla proved the goal after 60.448209ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.950371ms: rewriting 6.864926ms, bitblasting 0.109824ms, SAT solving 52.930212ms, LRAT trimming 2.311194ms, LRAT checking 5.067456ms +Bitwuzla proved the goal after 60.442750ms, solving context: 3.000000ms +LeanSAT proved the goal after 72.418613ms: rewriting 6.682406ms, bitblasting 0.133358ms, SAT solving 53.099307ms, LRAT trimming 3.887883ms, LRAT checking 7.824789ms diff --git a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_4_r0.txt b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_4_r0.txt index 283e84d0d3..cb148c5f21 100644 --- a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_4_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_4_r0.txt @@ -1,18 +1,18 @@ -Bitwuzla proved the goal after 69.424261ms, solving context: 0.000000ms -LeanSAT proved the goal after 71.264829ms: rewriting 9.868970ms, bitblasting 0.000000ms, SAT solving 58.338140ms, LRAT trimming 0.000000ms, LRAT checking 1.546079ms -Bitwuzla proved the goal after 69.285661ms, solving context: 0.000000ms -LeanSAT proved the goal after 71.650610ms: rewriting 10.526530ms, bitblasting 0.000000ms, SAT solving 58.346520ms, LRAT trimming 0.000000ms, LRAT checking 1.367450ms -Bitwuzla proved the goal after 7.521210ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.476680ms: rewriting 7.465660ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 72.636630ms, solving context: 0.000000ms -LeanSAT proved the goal after 75.842670ms: rewriting 14.028830ms, bitblasting 0.000000ms, SAT solving 58.298780ms, LRAT trimming 0.000000ms, LRAT checking 1.649410ms -Bitwuzla proved the goal after 6.979160ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.047410ms: rewriting 7.035910ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 67.665520ms, solving context: 0.000000ms -LeanSAT proved the goal after 69.995550ms: rewriting 8.868450ms, bitblasting 0.000000ms, SAT solving 58.371080ms, LRAT trimming 0.000000ms, LRAT checking 1.271080ms -Bitwuzla proved the goal after 68.047422ms, solving context: 0.000000ms -LeanSAT proved the goal after 69.704557ms: rewriting 8.865409ms, bitblasting 0.000000ms, SAT solving 58.459298ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 74.829330ms, solving context: 0.000000ms -LeanSAT proved the goal after 79.120669ms: rewriting 15.975740ms, bitblasting 0.000000ms, SAT solving 58.438609ms, LRAT trimming 0.000000ms, LRAT checking 2.805790ms -Bitwuzla proved the goal after 74.460690ms, solving context: 0.000000ms -LeanSAT proved the goal after 78.781331ms: rewriting 15.691260ms, bitblasting 0.000000ms, SAT solving 58.501911ms, LRAT trimming 0.000000ms, LRAT checking 2.728630ms +Bitwuzla proved the goal after 14.114667ms, solving context: 0.000000ms +LeanSAT proved the goal after 13.244911ms: rewriting 13.229562ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 12.772633ms, solving context: 0.000000ms +LeanSAT proved the goal after 12.881025ms: rewriting 12.875554ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.849332ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.769804ms: rewriting 14.764704ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.024794ms, solving context: 0.000000ms +LeanSAT proved the goal after 61.017468ms: rewriting 5.772225ms, bitblasting 0.031609ms, SAT solving 52.595610ms, LRAT trimming 0.172771ms, LRAT checking 2.167427ms +Bitwuzla proved the goal after 15.647426ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.215593ms: rewriting 15.208278ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 57.101612ms, solving context: 0.000000ms +LeanSAT proved the goal after 59.450086ms: rewriting 3.746762ms, bitblasting 0.019536ms, SAT solving 52.790582ms, LRAT trimming 0.207195ms, LRAT checking 2.278484ms +Bitwuzla proved the goal after 57.665853ms, solving context: 0.000000ms +LeanSAT proved the goal after 58.830452ms: rewriting 3.779122ms, bitblasting 0.020238ms, SAT solving 52.673012ms, LRAT trimming 0.171829ms, LRAT checking 1.833808ms +Bitwuzla proved the goal after 60.588371ms, solving context: 0.000000ms +LeanSAT proved the goal after 63.316781ms: rewriting 6.935196ms, bitblasting 0.029014ms, SAT solving 53.042961ms, LRAT trimming 0.506601ms, LRAT checking 2.461864ms +Bitwuzla proved the goal after 59.624841ms, solving context: 0.000000ms +LeanSAT proved the goal after 63.304639ms: rewriting 6.357944ms, bitblasting 0.034223ms, SAT solving 53.038093ms, LRAT trimming 0.683600ms, LRAT checking 2.846017ms diff --git a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_64_r0.txt b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_64_r0.txt index e6cfc19975..1bc4142ff1 100644 --- a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_64_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_64_r0.txt @@ -1,18 +1,18 @@ -Bitwuzla proved the goal after 70.332659ms, solving context: 0.000000ms -LeanSAT proved the goal after 76.237470ms: rewriting 10.212521ms, bitblasting 0.000000ms, SAT solving 59.150559ms, LRAT trimming 0.000000ms, LRAT checking 4.017130ms -Bitwuzla proved the goal after 70.196810ms, solving context: 0.000000ms -LeanSAT proved the goal after 76.861159ms: rewriting 10.778170ms, bitblasting 0.000000ms, SAT solving 59.221059ms, LRAT trimming 1.013370ms, LRAT checking 3.891000ms -Bitwuzla proved the goal after 7.560260ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.488710ms: rewriting 7.475250ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 73.622859ms, solving context: 1.000000ms -LeanSAT proved the goal after 94.435701ms: rewriting 14.388301ms, bitblasting 0.000000ms, SAT solving 59.316171ms, LRAT trimming 6.938919ms, LRAT checking 10.866830ms -Bitwuzla proved the goal after 7.174720ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.100390ms: rewriting 7.086910ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 68.595939ms, solving context: 2.000000ms -LeanSAT proved the goal after 76.114110ms: rewriting 9.133700ms, bitblasting 0.000000ms, SAT solving 59.297709ms, LRAT trimming 1.112530ms, LRAT checking 4.345551ms -Bitwuzla proved the goal after 68.826699ms, solving context: 2.000000ms -LeanSAT proved the goal after 75.915220ms: rewriting 9.136770ms, bitblasting 0.000000ms, SAT solving 59.348930ms, LRAT trimming 1.105120ms, LRAT checking 4.040900ms -Bitwuzla proved the goal after 75.754420ms, solving context: 0.000000ms -LeanSAT proved the goal after 116.713799ms: rewriting 16.197209ms, bitblasting 0.000000ms, SAT solving 59.368020ms, LRAT trimming 15.507860ms, LRAT checking 21.176920ms -Bitwuzla proved the goal after 75.749129ms, solving context: 5.000000ms -LeanSAT proved the goal after 194.553399ms: rewriting 16.085470ms, bitblasting 0.000000ms, SAT solving 109.619779ms, LRAT trimming 30.782530ms, LRAT checking 33.625670ms +Bitwuzla proved the goal after 13.440935ms, solving context: 0.000000ms +LeanSAT proved the goal after 13.037836ms: rewriting 13.020313ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 12.680062ms, solving context: 0.000000ms +LeanSAT proved the goal after 12.590745ms: rewriting 12.585846ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.780424ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.699684ms: rewriting 14.693001ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.114580ms, solving context: 1.000000ms +LeanSAT proved the goal after 64.905654ms: rewriting 5.740306ms, bitblasting 0.190313ms, SAT solving 52.602544ms, LRAT trimming 1.421161ms, LRAT checking 4.254224ms +Bitwuzla proved the goal after 15.517063ms, solving context: 0.000000ms +LeanSAT proved the goal after 16.323030ms: rewriting 16.312981ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 57.672552ms, solving context: 1.000000ms +LeanSAT proved the goal after 62.176222ms: rewriting 3.746352ms, bitblasting 0.106088ms, SAT solving 53.081361ms, LRAT trimming 0.675415ms, LRAT checking 3.729741ms +Bitwuzla proved the goal after 57.523196ms, solving context: 1.000000ms +LeanSAT proved the goal after 61.586307ms: rewriting 3.911728ms, bitblasting 0.113831ms, SAT solving 52.997719ms, LRAT trimming 0.610374ms, LRAT checking 3.174619ms +Bitwuzla proved the goal after 60.272242ms, solving context: 0.000000ms +LeanSAT proved the goal after 74.038212ms: rewriting 6.376348ms, bitblasting 0.225960ms, SAT solving 52.842357ms, LRAT trimming 4.733506ms, LRAT checking 8.815049ms +Bitwuzla proved the goal after 60.272285ms, solving context: 8.000000ms +LeanSAT proved the goal after 78.344422ms: rewriting 6.451136ms, bitblasting 0.255094ms, SAT solving 53.051375ms, LRAT trimming 6.367031ms, LRAT checking 10.846403ms diff --git a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_8_r0.txt b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_8_r0.txt index 1184256882..74281dda54 100644 --- a/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_8_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_1DeMorgan_8_r0.txt @@ -1,18 +1,18 @@ -Bitwuzla proved the goal after 69.354480ms, solving context: 0.000000ms -LeanSAT proved the goal after 71.478670ms: rewriting 9.890210ms, bitblasting 0.000000ms, SAT solving 58.298410ms, LRAT trimming 0.000000ms, LRAT checking 1.551500ms -Bitwuzla proved the goal after 69.140540ms, solving context: 0.000000ms -LeanSAT proved the goal after 71.838520ms: rewriting 10.491230ms, bitblasting 0.000000ms, SAT solving 58.316830ms, LRAT trimming 0.000000ms, LRAT checking 1.323820ms -Bitwuzla proved the goal after 7.501030ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.560180ms: rewriting 7.548960ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 72.749852ms, solving context: 0.000000ms -LeanSAT proved the goal after 76.678938ms: rewriting 14.072620ms, bitblasting 0.000000ms, SAT solving 58.339557ms, LRAT trimming 0.000000ms, LRAT checking 2.682760ms -Bitwuzla proved the goal after 7.063190ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.146520ms: rewriting 7.134180ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 67.544431ms, solving context: 0.000000ms -LeanSAT proved the goal after 70.228378ms: rewriting 8.884250ms, bitblasting 0.000000ms, SAT solving 58.281488ms, LRAT trimming 0.000000ms, LRAT checking 1.269370ms -Bitwuzla proved the goal after 67.940700ms, solving context: 0.000000ms -LeanSAT proved the goal after 69.917399ms: rewriting 8.842210ms, bitblasting 0.000000ms, SAT solving 58.387818ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 74.657420ms, solving context: 0.000000ms -LeanSAT proved the goal after 80.796040ms: rewriting 15.972070ms, bitblasting 0.000000ms, SAT solving 58.232211ms, LRAT trimming 1.693700ms, LRAT checking 3.703799ms -Bitwuzla proved the goal after 74.639229ms, solving context: 1.000000ms -LeanSAT proved the goal after 83.178130ms: rewriting 15.888520ms, bitblasting 0.000000ms, SAT solving 58.302089ms, LRAT trimming 2.825120ms, LRAT checking 5.000470ms +Bitwuzla proved the goal after 13.677805ms, solving context: 0.000000ms +LeanSAT proved the goal after 13.108367ms: rewriting 13.093299ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 12.917021ms, solving context: 0.000000ms +LeanSAT proved the goal after 13.025654ms: rewriting 13.020824ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.841638ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.748795ms: rewriting 14.743455ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.024152ms, solving context: 0.000000ms +LeanSAT proved the goal after 62.145243ms: rewriting 5.757508ms, bitblasting 0.041568ms, SAT solving 52.966477ms, LRAT trimming 0.325254ms, LRAT checking 2.685580ms +Bitwuzla proved the goal after 15.659237ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.207437ms: rewriting 15.200174ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 57.467494ms, solving context: 0.000000ms +LeanSAT proved the goal after 60.064365ms: rewriting 3.992207ms, bitblasting 0.025167ms, SAT solving 53.119261ms, LRAT trimming 0.261756ms, LRAT checking 2.295035ms +Bitwuzla proved the goal after 57.724928ms, solving context: 0.000000ms +LeanSAT proved the goal after 59.361191ms: rewriting 3.822513ms, bitblasting 0.025277ms, SAT solving 53.056655ms, LRAT trimming 0.213316ms, LRAT checking 1.867591ms +Bitwuzla proved the goal after 60.545401ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.197024ms: rewriting 6.905621ms, bitblasting 0.041187ms, SAT solving 53.068900ms, LRAT trimming 1.130611ms, LRAT checking 3.656955ms +Bitwuzla proved the goal after 60.421612ms, solving context: 0.000000ms +LeanSAT proved the goal after 64.263070ms: rewriting 6.312669ms, bitblasting 0.048420ms, SAT solving 52.757762ms, LRAT trimming 1.066341ms, LRAT checking 3.676621ms diff --git a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_16_r0.txt b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_16_r0.txt index dbbed64ddb..7eb7d9fffb 100644 --- a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_16_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_16_r0.txt @@ -1,44 +1,44 @@ -Bitwuzla proved the goal after 5.743560ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.472170ms: rewriting 5.439600ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 74.316120ms, solving context: 0.000000ms -LeanSAT proved the goal after 79.452419ms: rewriting 14.611389ms, bitblasting 0.000000ms, SAT solving 58.935369ms, LRAT trimming 1.128990ms, LRAT checking 3.531271ms -Bitwuzla proved the goal after 7.209810ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.180030ms: rewriting 7.167090ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 5.147560ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.332579ms: rewriting 5.322039ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 6.886410ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.054090ms: rewriting 7.042820ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 76.303660ms, solving context: 0.000000ms -LeanSAT proved the goal after 93.417980ms: rewriting 17.396030ms, bitblasting 0.000000ms, SAT solving 58.825700ms, LRAT trimming 6.071050ms, LRAT checking 9.535220ms -Bitwuzla proved the goal after 74.460810ms, solving context: 1.000000ms -LeanSAT proved the goal after 86.938460ms: rewriting 15.293030ms, bitblasting 0.000000ms, SAT solving 59.049060ms, LRAT trimming 2.800260ms, LRAT checking 6.866760ms -Bitwuzla proved the goal after 71.334109ms, solving context: 0.000000ms -LeanSAT proved the goal after 78.440701ms: rewriting 12.536921ms, bitblasting 0.000000ms, SAT solving 58.995851ms, LRAT trimming 1.664960ms, LRAT checking 3.875209ms -Bitwuzla proved the goal after 78.516941ms, solving context: 1.000000ms -LeanSAT proved the goal after 103.318918ms: rewriting 19.911249ms, bitblasting 0.000000ms, SAT solving 58.778029ms, LRAT trimming 8.542920ms, LRAT checking 12.795320ms -Bitwuzla proved the goal after 77.827950ms, solving context: 0.000000ms -LeanSAT proved the goal after 95.975989ms: rewriting 18.510940ms, bitblasting 0.000000ms, SAT solving 59.044699ms, LRAT trimming 6.360120ms, LRAT checking 10.230710ms -Bitwuzla proved the goal after 83.960138ms, solving context: 4.000000ms -LeanSAT proved the goal after 124.290770ms: rewriting 24.798460ms, bitblasting 0.000000ms, SAT solving 58.446690ms, LRAT trimming 16.160380ms, LRAT checking 21.219520ms -Bitwuzla proved the goal after 82.238350ms, solving context: 2.000000ms -LeanSAT proved the goal after 104.086869ms: rewriting 22.800030ms, bitblasting 0.000000ms, SAT solving 58.908280ms, LRAT trimming 8.086200ms, LRAT checking 12.341180ms -Bitwuzla proved the goal after 83.953141ms, solving context: 5.000000ms -LeanSAT proved the goal after 123.892028ms: rewriting 24.722368ms, bitblasting 0.000000ms, SAT solving 58.576070ms, LRAT trimming 16.083050ms, LRAT checking 20.797550ms -Bitwuzla proved the goal after 76.422800ms, solving context: 0.000000ms -LeanSAT proved the goal after 85.248200ms: rewriting 17.288350ms, bitblasting 0.000000ms, SAT solving 59.106270ms, LRAT trimming 2.452250ms, LRAT checking 4.827590ms -Bitwuzla proved the goal after 76.536310ms, solving context: 0.000000ms -LeanSAT proved the goal after 82.436979ms: rewriting 16.632109ms, bitblasting 0.000000ms, SAT solving 59.123799ms, LRAT trimming 1.588490ms, LRAT checking 3.584931ms -Bitwuzla proved the goal after 75.856979ms, solving context: 0.000000ms -LeanSAT proved the goal after 82.757771ms: rewriting 16.511140ms, bitblasting 0.000000ms, SAT solving 59.249802ms, LRAT trimming 1.788640ms, LRAT checking 3.718439ms -Bitwuzla proved the goal after 81.777779ms, solving context: 1.000000ms -LeanSAT proved the goal after 117.246460ms: rewriting 22.343870ms, bitblasting 0.000000ms, SAT solving 58.920520ms, LRAT trimming 14.843100ms, LRAT checking 18.988570ms -Bitwuzla proved the goal after 75.335043ms, solving context: 1.000000ms -LeanSAT proved the goal after 88.845448ms: rewriting 15.974599ms, bitblasting 0.000000ms, SAT solving 59.082598ms, LRAT trimming 4.617921ms, LRAT checking 7.458100ms -Bitwuzla proved the goal after 79.654030ms, solving context: 0.000000ms -LeanSAT proved the goal after 88.935990ms: rewriting 20.691710ms, bitblasting 0.000000ms, SAT solving 59.017101ms, LRAT trimming 2.311739ms, LRAT checking 5.181480ms -Bitwuzla proved the goal after 72.067920ms, solving context: 0.000000ms -LeanSAT proved the goal after 77.317449ms: rewriting 13.306100ms, bitblasting 0.000000ms, SAT solving 59.275620ms, LRAT trimming 0.000000ms, LRAT checking 2.756760ms -Bitwuzla proved the goal after 70.681300ms, solving context: 0.000000ms -LeanSAT proved the goal after 75.918700ms: rewriting 11.604270ms, bitblasting 0.000000ms, SAT solving 59.260371ms, LRAT trimming 0.000000ms, LRAT checking 2.895059ms -Bitwuzla proved the goal after 74.670631ms, solving context: 0.000000ms -LeanSAT proved the goal after 83.622250ms: rewriting 15.546350ms, bitblasting 0.000000ms, SAT solving 59.182111ms, LRAT trimming 2.326140ms, LRAT checking 5.019839ms +Bitwuzla proved the goal after 14.863688ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.307325ms: rewriting 14.291796ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.324229ms, solving context: 0.000000ms +LeanSAT proved the goal after 63.255965ms: rewriting 6.231239ms, bitblasting 0.060633ms, SAT solving 52.964803ms, LRAT trimming 0.509156ms, LRAT checking 3.064785ms +Bitwuzla proved the goal after 14.913672ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.419313ms: rewriting 14.411519ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.601391ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.502958ms: rewriting 14.498160ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 15.260405ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.249255ms: rewriting 15.244887ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 62.768322ms, solving context: 0.000000ms +LeanSAT proved the goal after 72.584661ms: rewriting 9.332511ms, bitblasting 0.096780ms, SAT solving 53.051578ms, LRAT trimming 3.044367ms, LRAT checking 6.475032ms +Bitwuzla proved the goal after 65.042007ms, solving context: 1.000000ms +LeanSAT proved the goal after 70.837655ms: rewriting 11.905702ms, bitblasting 0.069819ms, SAT solving 53.041838ms, LRAT trimming 1.188328ms, LRAT checking 4.115145ms +Bitwuzla proved the goal after 62.250383ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.571125ms: rewriting 8.303868ms, bitblasting 0.065571ms, SAT solving 53.011471ms, LRAT trimming 1.084454ms, LRAT checking 3.572949ms +Bitwuzla proved the goal after 67.600580ms, solving context: 1.000000ms +LeanSAT proved the goal after 74.042548ms: rewriting 14.401850ms, bitblasting 0.074389ms, SAT solving 53.053467ms, LRAT trimming 1.450706ms, LRAT checking 4.530489ms +Bitwuzla proved the goal after 63.121660ms, solving context: 0.000000ms +LeanSAT proved the goal after 70.352903ms: rewriting 9.001504ms, bitblasting 0.080519ms, SAT solving 52.867593ms, LRAT trimming 2.409848ms, LRAT checking 5.457130ms +Bitwuzla proved the goal after 67.273723ms, solving context: 3.000000ms +LeanSAT proved the goal after 76.399149ms: rewriting 13.565045ms, bitblasting 0.094686ms, SAT solving 52.743403ms, LRAT trimming 2.815041ms, LRAT checking 6.524662ms +Bitwuzla proved the goal after 62.971338ms, solving context: 1.000000ms +LeanSAT proved the goal after 69.881269ms: rewriting 8.827052ms, bitblasting 0.084457ms, SAT solving 53.039907ms, LRAT trimming 2.732117ms, LRAT checking 4.651662ms +Bitwuzla proved the goal after 67.515652ms, solving context: 1.000000ms +LeanSAT proved the goal after 75.197275ms: rewriting 13.762973ms, bitblasting 0.101508ms, SAT solving 53.093061ms, LRAT trimming 2.517969ms, LRAT checking 5.152636ms +Bitwuzla proved the goal after 61.881265ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.400840ms: rewriting 8.403062ms, bitblasting 0.054742ms, SAT solving 53.177529ms, LRAT trimming 0.455026ms, LRAT checking 2.831523ms +Bitwuzla proved the goal after 61.390542ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.239191ms: rewriting 8.511895ms, bitblasting 0.054462ms, SAT solving 53.140052ms, LRAT trimming 0.497705ms, LRAT checking 3.547811ms +Bitwuzla proved the goal after 62.650185ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.350503ms: rewriting 8.720102ms, bitblasting 0.059120ms, SAT solving 53.260991ms, LRAT trimming 0.508635ms, LRAT checking 3.260420ms +Bitwuzla proved the goal after 62.800111ms, solving context: 1.000000ms +LeanSAT proved the goal after 78.847658ms: rewriting 8.830719ms, bitblasting 0.142124ms, SAT solving 53.341435ms, LRAT trimming 5.315377ms, LRAT checking 10.428467ms +Bitwuzla proved the goal after 61.200879ms, solving context: 1.000000ms +LeanSAT proved the goal after 69.284260ms: rewriting 7.612455ms, bitblasting 0.086611ms, SAT solving 53.335476ms, LRAT trimming 2.066409ms, LRAT checking 5.580879ms +Bitwuzla proved the goal after 64.245576ms, solving context: 0.000000ms +LeanSAT proved the goal after 70.003004ms: rewriting 10.025769ms, bitblasting 0.095988ms, SAT solving 53.346265ms, LRAT trimming 1.227551ms, LRAT checking 4.702727ms +Bitwuzla proved the goal after 61.751271ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.143333ms: rewriting 7.728480ms, bitblasting 0.063508ms, SAT solving 53.331124ms, LRAT trimming 0.251708ms, LRAT checking 3.242966ms +Bitwuzla proved the goal after 60.963429ms, solving context: 0.000000ms +LeanSAT proved the goal after 64.445467ms: rewriting 6.748308ms, bitblasting 0.073286ms, SAT solving 53.353358ms, LRAT trimming 0.480834ms, LRAT checking 3.278672ms +Bitwuzla proved the goal after 62.365704ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.105811ms: rewriting 8.748024ms, bitblasting 0.076933ms, SAT solving 53.064469ms, LRAT trimming 0.687498ms, LRAT checking 3.935804ms diff --git a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_32_r0.txt b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_32_r0.txt index 3080a618ae..e1eea0dbeb 100644 --- a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_32_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_32_r0.txt @@ -1,44 +1,44 @@ -Bitwuzla proved the goal after 5.725360ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.436550ms: rewriting 5.404080ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 74.432241ms, solving context: 0.000000ms -LeanSAT proved the goal after 81.724708ms: rewriting 14.718929ms, bitblasting 0.000000ms, SAT solving 58.890939ms, LRAT trimming 1.680680ms, LRAT checking 4.697370ms -Bitwuzla proved the goal after 7.200110ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.242680ms: rewriting 7.229020ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 5.141160ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.353380ms: rewriting 5.343170ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 6.861890ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.109890ms: rewriting 7.100150ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 76.351370ms, solving context: 0.000000ms -LeanSAT proved the goal after 117.951599ms: rewriting 17.457019ms, bitblasting 0.000000ms, SAT solving 58.966740ms, LRAT trimming 16.793430ms, LRAT checking 22.187070ms -Bitwuzla proved the goal after 74.385930ms, solving context: 1.000000ms -LeanSAT proved the goal after 114.162660ms: rewriting 15.278810ms, bitblasting 3.051930ms, SAT solving 58.948589ms, LRAT trimming 11.851951ms, LRAT checking 20.173870ms -Bitwuzla proved the goal after 71.552361ms, solving context: 0.000000ms -LeanSAT proved the goal after 82.582398ms: rewriting 12.501960ms, bitblasting 0.000000ms, SAT solving 59.117339ms, LRAT trimming 2.952260ms, LRAT checking 6.032510ms -Bitwuzla proved the goal after 79.010820ms, solving context: 2.000000ms -LeanSAT proved the goal after 141.948409ms: rewriting 19.990559ms, bitblasting 3.450980ms, SAT solving 58.671520ms, LRAT trimming 22.307490ms, LRAT checking 31.741890ms -Bitwuzla proved the goal after 77.961209ms, solving context: 0.000000ms -LeanSAT proved the goal after 114.856200ms: rewriting 18.635661ms, bitblasting 0.000000ms, SAT solving 59.092890ms, LRAT trimming 14.384730ms, LRAT checking 19.848179ms -Bitwuzla proved the goal after 84.177090ms, solving context: 20.000000ms -LeanSAT proved the goal after 234.585709ms: rewriting 24.731300ms, bitblasting 3.550369ms, SAT solving 108.596159ms, LRAT trimming 40.094921ms, LRAT checking 50.946610ms -Bitwuzla proved the goal after 82.501930ms, solving context: 6.000000ms -LeanSAT proved the goal after 122.066189ms: rewriting 22.819329ms, bitblasting 0.000000ms, SAT solving 59.049180ms, LRAT trimming 15.762740ms, LRAT checking 21.241830ms -Bitwuzla proved the goal after 84.504410ms, solving context: 21.000000ms -LeanSAT proved the goal after 238.222209ms: rewriting 24.712840ms, bitblasting 3.641919ms, SAT solving 108.668910ms, LRAT trimming 40.712940ms, LRAT checking 53.701010ms -Bitwuzla proved the goal after 76.902970ms, solving context: 0.000000ms -LeanSAT proved the goal after 88.684959ms: rewriting 17.372429ms, bitblasting 0.000000ms, SAT solving 59.404751ms, LRAT trimming 3.167190ms, LRAT checking 6.417049ms -Bitwuzla proved the goal after 76.041319ms, solving context: 0.000000ms -LeanSAT proved the goal after 87.164551ms: rewriting 16.677501ms, bitblasting 0.000000ms, SAT solving 59.353280ms, LRAT trimming 3.114690ms, LRAT checking 5.795320ms -Bitwuzla proved the goal after 76.196171ms, solving context: 0.000000ms -LeanSAT proved the goal after 88.932248ms: rewriting 16.541409ms, bitblasting 0.000000ms, SAT solving 59.535449ms, LRAT trimming 4.830130ms, LRAT checking 5.814470ms -Bitwuzla proved the goal after 82.250609ms, solving context: 2.000000ms -LeanSAT proved the goal after 280.134269ms: rewriting 22.508170ms, bitblasting 0.000000ms, SAT solving 159.334700ms, LRAT trimming 44.619420ms, LRAT checking 50.095759ms -Bitwuzla proved the goal after 75.879620ms, solving context: 2.000000ms -LeanSAT proved the goal after 97.541359ms: rewriting 16.056880ms, bitblasting 0.000000ms, SAT solving 59.471309ms, LRAT trimming 7.492290ms, LRAT checking 11.842250ms -Bitwuzla proved the goal after 80.347530ms, solving context: 0.000000ms -LeanSAT proved the goal after 107.489599ms: rewriting 20.803339ms, bitblasting 0.000000ms, SAT solving 59.533160ms, LRAT trimming 9.507700ms, LRAT checking 14.818080ms -Bitwuzla proved the goal after 72.738159ms, solving context: 0.000000ms -LeanSAT proved the goal after 79.429920ms: rewriting 13.123540ms, bitblasting 0.000000ms, SAT solving 59.727090ms, LRAT trimming 0.000000ms, LRAT checking 3.767080ms -Bitwuzla proved the goal after 71.253159ms, solving context: 0.000000ms -LeanSAT proved the goal after 80.357980ms: rewriting 11.543790ms, bitblasting 0.000000ms, SAT solving 59.782020ms, LRAT trimming 2.115290ms, LRAT checking 5.117620ms -Bitwuzla proved the goal after 75.304531ms, solving context: 0.000000ms -LeanSAT proved the goal after 88.366649ms: rewriting 15.695860ms, bitblasting 0.000000ms, SAT solving 59.691558ms, LRAT trimming 3.639641ms, LRAT checking 7.067560ms +Bitwuzla proved the goal after 14.904575ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.389147ms: rewriting 14.371233ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.289445ms, solving context: 0.000000ms +LeanSAT proved the goal after 64.824502ms: rewriting 6.232420ms, bitblasting 0.106999ms, SAT solving 52.941171ms, LRAT trimming 1.127385ms, LRAT checking 3.781496ms +Bitwuzla proved the goal after 15.057610ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.292568ms: rewriting 14.285144ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.553542ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.499823ms: rewriting 14.494704ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 15.190586ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.228877ms: rewriting 15.223857ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 62.470528ms, solving context: 0.000000ms +LeanSAT proved the goal after 81.972305ms: rewriting 9.324777ms, bitblasting 0.176708ms, SAT solving 53.011302ms, LRAT trimming 6.546875ms, LRAT checking 11.987964ms +Bitwuzla proved the goal after 64.849238ms, solving context: 2.000000ms +LeanSAT proved the goal after 71.488784ms: rewriting 11.991812ms, bitblasting 0.118881ms, SAT solving 52.755646ms, LRAT trimming 1.491752ms, LRAT checking 4.482560ms +Bitwuzla proved the goal after 61.901651ms, solving context: 0.000000ms +LeanSAT proved the goal after 69.845972ms: rewriting 8.689577ms, bitblasting 0.199741ms, SAT solving 53.083264ms, LRAT trimming 1.863202ms, LRAT checking 5.308394ms +Bitwuzla proved the goal after 67.690057ms, solving context: 2.000000ms +LeanSAT proved the goal after 76.142851ms: rewriting 14.701567ms, bitblasting 0.124651ms, SAT solving 53.053978ms, LRAT trimming 2.219123ms, LRAT checking 5.211184ms +Bitwuzla proved the goal after 63.119334ms, solving context: 0.000000ms +LeanSAT proved the goal after 75.666457ms: rewriting 9.049906ms, bitblasting 0.146783ms, SAT solving 53.061796ms, LRAT trimming 4.601139ms, LRAT checking 7.946235ms +Bitwuzla proved the goal after 67.584110ms, solving context: 3.000000ms +LeanSAT proved the goal after 83.439992ms: rewriting 13.514231ms, bitblasting 0.164376ms, SAT solving 52.811420ms, LRAT trimming 5.341134ms, LRAT checking 10.621504ms +Bitwuzla proved the goal after 62.183705ms, solving context: 2.000000ms +LeanSAT proved the goal after 78.491927ms: rewriting 8.559034ms, bitblasting 0.147394ms, SAT solving 52.753643ms, LRAT trimming 6.243672ms, LRAT checking 10.059322ms +Bitwuzla proved the goal after 67.284576ms, solving context: 2.000000ms +LeanSAT proved the goal after 92.367017ms: rewriting 13.020142ms, bitblasting 0.173683ms, SAT solving 52.753482ms, LRAT trimming 10.790119ms, LRAT checking 14.564513ms +Bitwuzla proved the goal after 62.170641ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.547383ms: rewriting 8.902933ms, bitblasting 0.094836ms, SAT solving 52.780463ms, LRAT trimming 0.756937ms, LRAT checking 3.376754ms +Bitwuzla proved the goal after 61.831632ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.900409ms: rewriting 7.901242ms, bitblasting 0.080560ms, SAT solving 53.021149ms, LRAT trimming 0.978138ms, LRAT checking 4.222257ms +Bitwuzla proved the goal after 60.931578ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.049748ms: rewriting 7.333036ms, bitblasting 0.079287ms, SAT solving 53.086990ms, LRAT trimming 0.637124ms, LRAT checking 3.320009ms +Bitwuzla proved the goal after 61.860797ms, solving context: 2.000000ms +LeanSAT proved the goal after 85.667780ms: rewriting 7.479828ms, bitblasting 0.230718ms, SAT solving 52.830746ms, LRAT trimming 8.902432ms, LRAT checking 15.173164ms +Bitwuzla proved the goal after 60.416644ms, solving context: 3.000000ms +LeanSAT proved the goal after 73.131064ms: rewriting 6.746064ms, bitblasting 0.138527ms, SAT solving 53.255723ms, LRAT trimming 3.910377ms, LRAT checking 8.240993ms +Bitwuzla proved the goal after 62.266940ms, solving context: 0.000000ms +LeanSAT proved the goal after 71.161407ms: rewriting 8.169230ms, bitblasting 0.146662ms, SAT solving 52.128030ms, LRAT trimming 2.680521ms, LRAT checking 7.296467ms +Bitwuzla proved the goal after 61.175891ms, solving context: 0.000000ms +LeanSAT proved the goal after 64.889063ms: rewriting 6.909890ms, bitblasting 0.091089ms, SAT solving 53.325596ms, LRAT trimming 0.391768ms, LRAT checking 3.476880ms +Bitwuzla proved the goal after 59.840811ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.015477ms: rewriting 5.983638ms, bitblasting 0.090398ms, SAT solving 53.286173ms, LRAT trimming 1.047777ms, LRAT checking 3.963886ms +Bitwuzla proved the goal after 60.772193ms, solving context: 0.000000ms +LeanSAT proved the goal after 68.310559ms: rewriting 7.700980ms, bitblasting 0.112439ms, SAT solving 53.172139ms, LRAT trimming 1.568565ms, LRAT checking 4.955109ms diff --git a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_4_r0.txt b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_4_r0.txt index ecf16ca3a4..dd0424ccc4 100644 --- a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_4_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_4_r0.txt @@ -1,44 +1,44 @@ -Bitwuzla proved the goal after 5.674440ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.429420ms: rewriting 5.402600ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 74.562600ms, solving context: 0.000000ms -LeanSAT proved the goal after 77.471699ms: rewriting 14.690580ms, bitblasting 0.000000ms, SAT solving 59.063189ms, LRAT trimming 0.000000ms, LRAT checking 1.811920ms -Bitwuzla proved the goal after 7.210650ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.212770ms: rewriting 7.198860ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 5.132210ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.316460ms: rewriting 5.306450ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 6.883210ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.109610ms: rewriting 7.099150ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 76.190790ms, solving context: 0.000000ms -LeanSAT proved the goal after 82.029219ms: rewriting 17.523959ms, bitblasting 0.000000ms, SAT solving 58.897440ms, LRAT trimming 1.310320ms, LRAT checking 3.347560ms -Bitwuzla proved the goal after 74.100750ms, solving context: 0.000000ms -LeanSAT proved the goal after 78.545491ms: rewriting 15.343930ms, bitblasting 0.000000ms, SAT solving 58.940251ms, LRAT trimming 0.000000ms, LRAT checking 1.733620ms -Bitwuzla proved the goal after 71.529030ms, solving context: 0.000000ms -LeanSAT proved the goal after 74.998539ms: rewriting 12.485760ms, bitblasting 0.000000ms, SAT solving 58.950589ms, LRAT trimming 0.000000ms, LRAT checking 1.365250ms -Bitwuzla proved the goal after 78.607830ms, solving context: 0.000000ms -LeanSAT proved the goal after 84.015600ms: rewriting 19.808340ms, bitblasting 0.000000ms, SAT solving 58.960010ms, LRAT trimming 0.000000ms, LRAT checking 3.285600ms -Bitwuzla proved the goal after 78.044371ms, solving context: 0.000000ms -LeanSAT proved the goal after 83.854148ms: rewriting 18.702739ms, bitblasting 0.000000ms, SAT solving 59.246689ms, LRAT trimming 1.355461ms, LRAT checking 3.577399ms -Bitwuzla proved the goal after 83.916931ms, solving context: 0.000000ms -LeanSAT proved the goal after 91.746221ms: rewriting 24.757900ms, bitblasting 0.000000ms, SAT solving 58.649681ms, LRAT trimming 2.283570ms, LRAT checking 4.881280ms -Bitwuzla proved the goal after 82.029130ms, solving context: 0.000000ms -LeanSAT proved the goal after 88.025609ms: rewriting 22.888129ms, bitblasting 0.000000ms, SAT solving 58.941450ms, LRAT trimming 1.425080ms, LRAT checking 3.731360ms -Bitwuzla proved the goal after 83.706721ms, solving context: 0.000000ms -LeanSAT proved the goal after 90.813440ms: rewriting 24.604599ms, bitblasting 0.000000ms, SAT solving 58.588431ms, LRAT trimming 1.919540ms, LRAT checking 4.499300ms -Bitwuzla proved the goal after 76.471679ms, solving context: 0.000000ms -LeanSAT proved the goal after 80.629421ms: rewriting 17.391671ms, bitblasting 0.000000ms, SAT solving 59.057870ms, LRAT trimming 0.000000ms, LRAT checking 1.632070ms -Bitwuzla proved the goal after 75.754860ms, solving context: 0.000000ms -LeanSAT proved the goal after 79.400190ms: rewriting 16.695080ms, bitblasting 0.000000ms, SAT solving 58.969040ms, LRAT trimming 0.000000ms, LRAT checking 1.484060ms -Bitwuzla proved the goal after 75.954629ms, solving context: 0.000000ms -LeanSAT proved the goal after 79.737100ms: rewriting 16.599320ms, bitblasting 0.000000ms, SAT solving 59.033470ms, LRAT trimming 0.000000ms, LRAT checking 1.529590ms -Bitwuzla proved the goal after 81.628529ms, solving context: 0.000000ms -LeanSAT proved the goal after 89.691500ms: rewriting 22.426280ms, bitblasting 0.000000ms, SAT solving 58.885640ms, LRAT trimming 2.272020ms, LRAT checking 5.008820ms -Bitwuzla proved the goal after 75.248380ms, solving context: 0.000000ms -LeanSAT proved the goal after 79.982952ms: rewriting 16.062050ms, bitblasting 0.000000ms, SAT solving 59.122892ms, LRAT trimming 0.000000ms, LRAT checking 2.899660ms -Bitwuzla proved the goal after 79.841990ms, solving context: 0.000000ms -LeanSAT proved the goal after 84.633090ms: rewriting 20.616010ms, bitblasting 0.000000ms, SAT solving 58.997950ms, LRAT trimming 0.000000ms, LRAT checking 3.195260ms -Bitwuzla proved the goal after 72.022801ms, solving context: 0.000000ms -LeanSAT proved the goal after 75.387459ms: rewriting 13.085560ms, bitblasting 0.000000ms, SAT solving 59.067799ms, LRAT trimming 0.000000ms, LRAT checking 1.456510ms -Bitwuzla proved the goal after 70.763590ms, solving context: 0.000000ms -LeanSAT proved the goal after 73.668299ms: rewriting 11.488169ms, bitblasting 0.000000ms, SAT solving 59.103410ms, LRAT trimming 0.000000ms, LRAT checking 1.368250ms -Bitwuzla proved the goal after 74.764589ms, solving context: 0.000000ms -LeanSAT proved the goal after 78.705429ms: rewriting 15.552450ms, bitblasting 0.000000ms, SAT solving 58.974190ms, LRAT trimming 0.000000ms, LRAT checking 1.640810ms +Bitwuzla proved the goal after 15.825115ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.985154ms: rewriting 14.967782ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.132063ms, solving context: 0.000000ms +LeanSAT proved the goal after 61.610922ms: rewriting 5.728715ms, bitblasting 0.032490ms, SAT solving 52.809708ms, LRAT trimming 0.282035ms, LRAT checking 2.482111ms +Bitwuzla proved the goal after 14.777428ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.067980ms: rewriting 14.060456ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.493200ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.441524ms: rewriting 14.435853ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 15.234047ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.122329ms: rewriting 15.117029ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 62.239007ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.218963ms: rewriting 9.205445ms, bitblasting 0.034094ms, SAT solving 52.919871ms, LRAT trimming 0.688149ms, LRAT checking 3.002549ms +Bitwuzla proved the goal after 64.733462ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.072890ms: rewriting 10.735047ms, bitblasting 0.026479ms, SAT solving 51.971909ms, LRAT trimming 0.261706ms, LRAT checking 2.781138ms +Bitwuzla proved the goal after 61.949170ms, solving context: 0.000000ms +LeanSAT proved the goal after 64.782163ms: rewriting 8.304240ms, bitblasting 0.030527ms, SAT solving 52.989150ms, LRAT trimming 0.456859ms, LRAT checking 2.609489ms +Bitwuzla proved the goal after 66.740933ms, solving context: 0.000000ms +LeanSAT proved the goal after 70.355501ms: rewriting 13.542704ms, bitblasting 0.034844ms, SAT solving 53.092696ms, LRAT trimming 0.349920ms, LRAT checking 2.998292ms +Bitwuzla proved the goal after 62.092355ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.291580ms: rewriting 8.627731ms, bitblasting 0.033252ms, SAT solving 52.736722ms, LRAT trimming 0.665616ms, LRAT checking 2.870413ms +Bitwuzla proved the goal after 66.341250ms, solving context: 0.000000ms +LeanSAT proved the goal after 70.587512ms: rewriting 13.078181ms, bitblasting 0.037811ms, SAT solving 52.974736ms, LRAT trimming 0.685594ms, LRAT checking 3.457906ms +Bitwuzla proved the goal after 63.105364ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.618466ms: rewriting 10.073389ms, bitblasting 0.045835ms, SAT solving 53.235209ms, LRAT trimming 0.629710ms, LRAT checking 3.260208ms +Bitwuzla proved the goal after 69.168504ms, solving context: 0.000000ms +LeanSAT proved the goal after 73.501378ms: rewriting 15.485094ms, bitblasting 0.041727ms, SAT solving 53.211327ms, LRAT trimming 0.623989ms, LRAT checking 3.732205ms +Bitwuzla proved the goal after 63.661174ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.525297ms: rewriting 10.011922ms, bitblasting 0.032601ms, SAT solving 53.223762ms, LRAT trimming 0.180335ms, LRAT checking 2.723040ms +Bitwuzla proved the goal after 62.741390ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.712512ms: rewriting 9.127079ms, bitblasting 0.030867ms, SAT solving 52.984622ms, LRAT trimming 0.213397ms, LRAT checking 3.013541ms +Bitwuzla proved the goal after 61.867558ms, solving context: 0.000000ms +LeanSAT proved the goal after 64.176020ms: rewriting 7.843354ms, bitblasting 0.020268ms, SAT solving 53.126738ms, LRAT trimming 0.258911ms, LRAT checking 2.642990ms +Bitwuzla proved the goal after 63.009679ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.760771ms: rewriting 8.875041ms, bitblasting 0.048020ms, SAT solving 53.282850ms, LRAT trimming 0.921402ms, LRAT checking 4.246530ms +Bitwuzla proved the goal after 61.069084ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.554388ms: rewriting 7.628224ms, bitblasting 0.039373ms, SAT solving 53.386017ms, LRAT trimming 0.737360ms, LRAT checking 3.380211ms +Bitwuzla proved the goal after 64.311726ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.691631ms: rewriting 10.186981ms, bitblasting 0.041026ms, SAT solving 52.980183ms, LRAT trimming 0.437412ms, LRAT checking 3.666583ms +Bitwuzla proved the goal after 61.680910ms, solving context: 0.000000ms +LeanSAT proved the goal after 64.407847ms: rewriting 7.673188ms, bitblasting 0.040947ms, SAT solving 53.311759ms, LRAT trimming 0.163394ms, LRAT checking 2.802257ms +Bitwuzla proved the goal after 60.802959ms, solving context: 0.000000ms +LeanSAT proved the goal after 63.301272ms: rewriting 6.678870ms, bitblasting 0.029475ms, SAT solving 53.309185ms, LRAT trimming 0.272917ms, LRAT checking 2.623895ms +Bitwuzla proved the goal after 62.918951ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.429543ms: rewriting 8.801073ms, bitblasting 0.035506ms, SAT solving 53.360389ms, LRAT trimming 0.442442ms, LRAT checking 3.410447ms diff --git a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_64_r0.txt b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_64_r0.txt index 7dc8ad49cb..ce9c7f210c 100644 --- a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_64_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_64_r0.txt @@ -1,44 +1,44 @@ -Bitwuzla proved the goal after 5.562130ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.368230ms: rewriting 5.341330ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 73.752270ms, solving context: 1.000000ms -LeanSAT proved the goal after 87.401120ms: rewriting 14.253960ms, bitblasting 0.000000ms, SAT solving 58.653921ms, LRAT trimming 4.012200ms, LRAT checking 7.825889ms -Bitwuzla proved the goal after 7.106280ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.085710ms: rewriting 7.073220ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 5.065540ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.241930ms: rewriting 5.231790ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 6.858740ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.037660ms: rewriting 7.025540ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 75.766680ms, solving context: 0.000000ms -LeanSAT proved the goal after 362.658978ms: rewriting 17.086779ms, bitblasting 0.000000ms, SAT solving 208.700320ms, LRAT trimming 62.974529ms, LRAT checking 69.285940ms -Bitwuzla proved the goal after 74.116680ms, solving context: 3.000000ms -LeanSAT proved the goal after 269.638959ms: rewriting 14.875340ms, bitblasting 11.796130ms, SAT solving 108.420369ms, LRAT trimming 47.099700ms, LRAT checking 72.346870ms -Bitwuzla proved the goal after 71.592820ms, solving context: 1.000000ms -LeanSAT proved the goal after 91.111779ms: rewriting 12.161819ms, bitblasting 0.000000ms, SAT solving 59.080070ms, LRAT trimming 5.983560ms, LRAT checking 10.663650ms -Bitwuzla proved the goal after 78.578940ms, solving context: 3.000000ms -LeanSAT proved the goal after 480.488858ms: rewriting 19.441520ms, bitblasting 14.174640ms, SAT solving 258.863561ms, LRAT trimming 76.126318ms, LRAT checking 93.421939ms -Bitwuzla proved the goal after 78.349330ms, solving context: 0.000000ms -LeanSAT proved the goal after 308.933488ms: rewriting 19.061350ms, bitblasting 0.000000ms, SAT solving 158.662109ms, LRAT trimming 57.177990ms, LRAT checking 68.819489ms -Bitwuzla proved the goal after 184.712379ms, solving context: 111.000000ms -LeanSAT proved the goal after 674.987027ms: rewriting 24.442580ms, bitblasting 14.341650ms, SAT solving 359.393478ms, LRAT trimming 116.131930ms, LRAT checking 140.086959ms -Bitwuzla proved the goal after 82.805539ms, solving context: 23.000000ms -LeanSAT proved the goal after 283.447019ms: rewriting 22.406700ms, bitblasting 0.000000ms, SAT solving 159.467779ms, LRAT trimming 43.283920ms, LRAT checking 52.666470ms -Bitwuzla proved the goal after 184.459049ms, solving context: 127.000000ms -LeanSAT proved the goal after 869.463886ms: rewriting 24.342200ms, bitblasting 14.852320ms, SAT solving 459.973030ms, LRAT trimming 162.449947ms, LRAT checking 187.130589ms -Bitwuzla proved the goal after 77.399430ms, solving context: 0.000000ms -LeanSAT proved the goal after 109.533000ms: rewriting 16.926740ms, bitblasting 0.000000ms, SAT solving 60.228650ms, LRAT trimming 11.638490ms, LRAT checking 16.977970ms -Bitwuzla proved the goal after 76.560251ms, solving context: 0.000000ms -LeanSAT proved the goal after 95.131588ms: rewriting 16.219519ms, bitblasting 0.000000ms, SAT solving 60.098379ms, LRAT trimming 5.697220ms, LRAT checking 9.429230ms -Bitwuzla proved the goal after 76.428839ms, solving context: 0.000000ms -LeanSAT proved the goal after 109.503110ms: rewriting 16.181991ms, bitblasting 0.000000ms, SAT solving 60.022209ms, LRAT trimming 10.723220ms, LRAT checking 19.151030ms -Bitwuzla proved the goal after 82.589910ms, solving context: 5.000000ms -LeanSAT proved the goal after 656.310447ms: rewriting 22.125520ms, bitblasting 0.000000ms, SAT solving 360.337429ms, LRAT trimming 129.332259ms, LRAT checking 138.082539ms -Bitwuzla proved the goal after 76.354590ms, solving context: 5.000000ms -LeanSAT proved the goal after 201.597749ms: rewriting 15.607849ms, bitblasting 0.000000ms, SAT solving 110.482420ms, LRAT trimming 32.937270ms, LRAT checking 38.025220ms -Bitwuzla proved the goal after 80.787699ms, solving context: 0.000000ms -LeanSAT proved the goal after 134.688490ms: rewriting 20.386270ms, bitblasting 0.000000ms, SAT solving 60.030250ms, LRAT trimming 20.335200ms, LRAT checking 29.239800ms -Bitwuzla proved the goal after 72.937310ms, solving context: 0.000000ms -LeanSAT proved the goal after 83.651509ms: rewriting 12.774200ms, bitblasting 0.000000ms, SAT solving 60.240819ms, LRAT trimming 1.900220ms, LRAT checking 5.657000ms -Bitwuzla proved the goal after 71.421269ms, solving context: 0.000000ms -LeanSAT proved the goal after 92.443259ms: rewriting 11.221980ms, bitblasting 0.000000ms, SAT solving 60.249029ms, LRAT trimming 5.466170ms, LRAT checking 12.685970ms -Bitwuzla proved the goal after 75.458949ms, solving context: 0.000000ms -LeanSAT proved the goal after 98.607130ms: rewriting 15.286960ms, bitblasting 0.000000ms, SAT solving 60.383670ms, LRAT trimming 7.447310ms, LRAT checking 11.854570ms +Bitwuzla proved the goal after 14.665380ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.297356ms: rewriting 14.281777ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.552795ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.387886ms: rewriting 6.202335ms, bitblasting 0.174284ms, SAT solving 52.660451ms, LRAT trimming 1.434004ms, LRAT checking 5.109014ms +Bitwuzla proved the goal after 14.834805ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.362056ms: rewriting 14.354934ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.559544ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.572187ms: rewriting 14.566928ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 15.272989ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.245488ms: rewriting 15.240569ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 62.723890ms, solving context: 0.000000ms +LeanSAT proved the goal after 239.101990ms: rewriting 9.303006ms, bitblasting 0.334221ms, SAT solving 153.094447ms, LRAT trimming 30.184667ms, LRAT checking 44.541293ms +Bitwuzla proved the goal after 65.083253ms, solving context: 2.000000ms +LeanSAT proved the goal after 77.415618ms: rewriting 11.265713ms, bitblasting 0.199080ms, SAT solving 53.067945ms, LRAT trimming 3.802536ms, LRAT checking 7.936447ms +Bitwuzla proved the goal after 62.032325ms, solving context: 1.000000ms +LeanSAT proved the goal after 74.505961ms: rewriting 8.272421ms, bitblasting 0.253922ms, SAT solving 53.061486ms, LRAT trimming 3.669608ms, LRAT checking 8.132391ms +Bitwuzla proved the goal after 67.430286ms, solving context: 4.000000ms +LeanSAT proved the goal after 79.308964ms: rewriting 13.580052ms, bitblasting 0.197968ms, SAT solving 52.775563ms, LRAT trimming 4.083588ms, LRAT checking 7.574884ms +Bitwuzla proved the goal after 61.878979ms, solving context: 0.000000ms +LeanSAT proved the goal after 79.545506ms: rewriting 8.645254ms, bitblasting 0.240717ms, SAT solving 53.147885ms, LRAT trimming 5.910032ms, LRAT checking 10.382081ms +Bitwuzla proved the goal after 67.227156ms, solving context: 14.000000ms +LeanSAT proved the goal after 166.614691ms: rewriting 13.716617ms, bitblasting 0.298073ms, SAT solving 103.255013ms, LRAT trimming 19.078558ms, LRAT checking 28.697584ms +Bitwuzla proved the goal after 61.479506ms, solving context: 17.000000ms +LeanSAT proved the goal after 164.550285ms: rewriting 8.457976ms, bitblasting 0.295930ms, SAT solving 103.203734ms, LRAT trimming 21.630583ms, LRAT checking 29.574653ms +Bitwuzla proved the goal after 66.309441ms, solving context: 12.000000ms +LeanSAT proved the goal after 160.819202ms: rewriting 12.441949ms, bitblasting 0.329993ms, SAT solving 102.321346ms, LRAT trimming 20.104596ms, LRAT checking 24.199026ms +Bitwuzla proved the goal after 62.474667ms, solving context: 0.000000ms +LeanSAT proved the goal after 68.714779ms: rewriting 8.297778ms, bitblasting 0.157592ms, SAT solving 53.524775ms, LRAT trimming 1.646710ms, LRAT checking 4.141074ms +Bitwuzla proved the goal after 61.960300ms, solving context: 0.000000ms +LeanSAT proved the goal after 70.992242ms: rewriting 7.857139ms, bitblasting 0.147704ms, SAT solving 52.884005ms, LRAT trimming 2.546131ms, LRAT checking 6.648614ms +Bitwuzla proved the goal after 60.017992ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.559624ms: rewriting 7.216398ms, bitblasting 0.158104ms, SAT solving 53.190303ms, LRAT trimming 0.778837ms, LRAT checking 4.253895ms +Bitwuzla proved the goal after 61.896559ms, solving context: 10.000000ms +LeanSAT proved the goal after 409.207529ms: rewriting 7.899900ms, bitblasting 0.411735ms, SAT solving 253.397463ms, LRAT trimming 58.030698ms, LRAT checking 87.318619ms +Bitwuzla proved the goal after 60.739892ms, solving context: 8.000000ms +LeanSAT proved the goal after 78.572718ms: rewriting 6.495830ms, bitblasting 0.241218ms, SAT solving 53.441730ms, LRAT trimming 6.316969ms, LRAT checking 10.809988ms +Bitwuzla proved the goal after 63.144750ms, solving context: 0.000000ms +LeanSAT proved the goal after 80.294036ms: rewriting 8.712869ms, bitblasting 0.280962ms, SAT solving 53.476887ms, LRAT trimming 5.192559ms, LRAT checking 11.284699ms +Bitwuzla proved the goal after 60.987182ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.620711ms: rewriting 6.600475ms, bitblasting 0.169094ms, SAT solving 53.153466ms, LRAT trimming 0.527079ms, LRAT checking 4.246993ms +Bitwuzla proved the goal after 60.599009ms, solving context: 0.000000ms +LeanSAT proved the goal after 69.552628ms: rewriting 5.894372ms, bitblasting 0.172771ms, SAT solving 53.209760ms, LRAT trimming 2.415969ms, LRAT checking 6.868953ms +Bitwuzla proved the goal after 61.757684ms, solving context: 0.000000ms +LeanSAT proved the goal after 72.520544ms: rewriting 7.461354ms, bitblasting 0.208778ms, SAT solving 53.426165ms, LRAT trimming 3.505072ms, LRAT checking 6.830581ms diff --git a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_8_r0.txt b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_8_r0.txt index e9e64dc093..b25abf2d91 100644 --- a/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_8_r0.txt +++ b/bv-evaluation/results/HackersDelight/ch2_2AdditionAndLogicalOps_8_r0.txt @@ -1,44 +1,44 @@ -Bitwuzla proved the goal after 5.710830ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.469260ms: rewriting 5.439700ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 74.430880ms, solving context: 0.000000ms -LeanSAT proved the goal after 78.441400ms: rewriting 14.693790ms, bitblasting 0.000000ms, SAT solving 59.084430ms, LRAT trimming 0.000000ms, LRAT checking 2.929460ms -Bitwuzla proved the goal after 7.127780ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.140630ms: rewriting 7.127310ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 5.129110ms, solving context: 0.000000ms -LeanSAT proved the goal after 5.335460ms: rewriting 5.326200ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 6.871750ms, solving context: 0.000000ms -LeanSAT proved the goal after 7.047040ms: rewriting 7.035840ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms -Bitwuzla proved the goal after 76.225589ms, solving context: 0.000000ms -LeanSAT proved the goal after 87.484019ms: rewriting 17.421620ms, bitblasting 0.000000ms, SAT solving 59.024029ms, LRAT trimming 3.619410ms, LRAT checking 6.223710ms -Bitwuzla proved the goal after 74.275500ms, solving context: 0.000000ms -LeanSAT proved the goal after 80.611989ms: rewriting 15.323680ms, bitblasting 0.000000ms, SAT solving 59.140319ms, LRAT trimming 1.074670ms, LRAT checking 3.619900ms -Bitwuzla proved the goal after 71.481289ms, solving context: 0.000000ms -LeanSAT proved the goal after 76.232120ms: rewriting 12.615131ms, bitblasting 0.000000ms, SAT solving 59.010749ms, LRAT trimming 0.000000ms, LRAT checking 2.698480ms -Bitwuzla proved the goal after 78.642031ms, solving context: 0.000000ms -LeanSAT proved the goal after 95.611428ms: rewriting 19.993609ms, bitblasting 0.000000ms, SAT solving 58.890569ms, LRAT trimming 6.034140ms, LRAT checking 9.064590ms -Bitwuzla proved the goal after 77.750108ms, solving context: 0.000000ms -LeanSAT proved the goal after 88.566610ms: rewriting 18.712720ms, bitblasting 0.000000ms, SAT solving 59.082190ms, LRAT trimming 3.407100ms, LRAT checking 6.083160ms -Bitwuzla proved the goal after 83.794119ms, solving context: 1.000000ms -LeanSAT proved the goal after 96.511270ms: rewriting 24.821870ms, bitblasting 0.000000ms, SAT solving 58.396420ms, LRAT trimming 4.182710ms, LRAT checking 7.289540ms -Bitwuzla proved the goal after 82.185950ms, solving context: 1.000000ms -LeanSAT proved the goal after 94.605070ms: rewriting 22.927970ms, bitblasting 0.000000ms, SAT solving 58.868050ms, LRAT trimming 4.219580ms, LRAT checking 7.225530ms -Bitwuzla proved the goal after 83.797760ms, solving context: 1.000000ms -LeanSAT proved the goal after 109.643689ms: rewriting 24.726860ms, bitblasting 0.000000ms, SAT solving 58.640260ms, LRAT trimming 10.148769ms, LRAT checking 14.191580ms -Bitwuzla proved the goal after 76.700928ms, solving context: 0.000000ms -LeanSAT proved the goal after 83.673350ms: rewriting 17.519080ms, bitblasting 0.000000ms, SAT solving 59.203409ms, LRAT trimming 1.697050ms, LRAT checking 4.100111ms -Bitwuzla proved the goal after 76.133711ms, solving context: 0.000000ms -LeanSAT proved the goal after 81.373278ms: rewriting 16.632719ms, bitblasting 0.000000ms, SAT solving 59.178899ms, LRAT trimming 1.196480ms, LRAT checking 3.235540ms -Bitwuzla proved the goal after 79.927929ms, solving context: 0.000000ms -LeanSAT proved the goal after 82.643030ms: rewriting 16.697880ms, bitblasting 0.000000ms, SAT solving 59.079060ms, LRAT trimming 1.649640ms, LRAT checking 4.022810ms -Bitwuzla proved the goal after 82.073780ms, solving context: 1.000000ms -LeanSAT proved the goal after 99.789890ms: rewriting 22.400220ms, bitblasting 0.000000ms, SAT solving 58.932181ms, LRAT trimming 6.850790ms, LRAT checking 10.180169ms -Bitwuzla proved the goal after 75.168162ms, solving context: 1.000000ms -LeanSAT proved the goal after 84.397769ms: rewriting 16.099109ms, bitblasting 0.000000ms, SAT solving 59.051410ms, LRAT trimming 2.881480ms, LRAT checking 5.138410ms -Bitwuzla proved the goal after 79.805669ms, solving context: 0.000000ms -LeanSAT proved the goal after 86.794509ms: rewriting 20.779799ms, bitblasting 0.000000ms, SAT solving 59.068859ms, LRAT trimming 1.550560ms, LRAT checking 4.146190ms -Bitwuzla proved the goal after 72.077589ms, solving context: 0.000000ms -LeanSAT proved the goal after 76.002071ms: rewriting 13.108520ms, bitblasting 0.000000ms, SAT solving 59.212951ms, LRAT trimming 0.000000ms, LRAT checking 1.436660ms -Bitwuzla proved the goal after 70.699439ms, solving context: 0.000000ms -LeanSAT proved the goal after 74.395930ms: rewriting 11.535180ms, bitblasting 0.000000ms, SAT solving 59.251220ms, LRAT trimming 0.000000ms, LRAT checking 1.355950ms -Bitwuzla proved the goal after 74.664401ms, solving context: 0.000000ms -LeanSAT proved the goal after 81.609069ms: rewriting 15.596809ms, bitblasting 0.000000ms, SAT solving 59.136470ms, LRAT trimming 1.747360ms, LRAT checking 3.994130ms +Bitwuzla proved the goal after 15.023165ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.799087ms: rewriting 15.779670ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 60.742878ms, solving context: 0.000000ms +LeanSAT proved the goal after 62.945765ms: rewriting 6.471485ms, bitblasting 0.044232ms, SAT solving 52.967514ms, LRAT trimming 0.338750ms, LRAT checking 2.744609ms +Bitwuzla proved the goal after 14.772960ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.202179ms: rewriting 14.194625ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 14.491877ms, solving context: 0.000000ms +LeanSAT proved the goal after 14.473955ms: rewriting 14.468164ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 15.281785ms, solving context: 0.000000ms +LeanSAT proved the goal after 15.410524ms: rewriting 15.404323ms, bitblasting 0.000000ms, SAT solving 0.000000ms, LRAT trimming 0.000000ms, LRAT checking 0.000000ms +Bitwuzla proved the goal after 62.738786ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.771246ms: rewriting 9.301073ms, bitblasting 0.059721ms, SAT solving 52.976715ms, LRAT trimming 1.224115ms, LRAT checking 3.780004ms +Bitwuzla proved the goal after 65.379299ms, solving context: 0.000000ms +LeanSAT proved the goal after 68.468856ms: rewriting 11.418248ms, bitblasting 0.045645ms, SAT solving 52.676400ms, LRAT trimming 0.719117ms, LRAT checking 3.220575ms +Bitwuzla proved the goal after 62.029121ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.443992ms: rewriting 8.311774ms, bitblasting 0.043772ms, SAT solving 52.997406ms, LRAT trimming 0.583004ms, LRAT checking 3.018287ms +Bitwuzla proved the goal after 67.123787ms, solving context: 0.000000ms +LeanSAT proved the goal after 71.260890ms: rewriting 13.643360ms, bitblasting 0.044974ms, SAT solving 52.710161ms, LRAT trimming 0.868023ms, LRAT checking 3.602113ms +Bitwuzla proved the goal after 62.306841ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.647241ms: rewriting 8.619047ms, bitblasting 0.048300ms, SAT solving 52.990637ms, LRAT trimming 1.374133ms, LRAT checking 4.205753ms +Bitwuzla proved the goal after 66.368681ms, solving context: 1.000000ms +LeanSAT proved the goal after 75.346603ms: rewriting 13.485788ms, bitblasting 0.054822ms, SAT solving 53.092203ms, LRAT trimming 2.322466ms, LRAT checking 5.955706ms +Bitwuzla proved the goal after 62.149670ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.733768ms: rewriting 8.593329ms, bitblasting 0.049251ms, SAT solving 53.185303ms, LRAT trimming 1.388169ms, LRAT checking 4.103675ms +Bitwuzla proved the goal after 66.786117ms, solving context: 1.000000ms +LeanSAT proved the goal after 73.347990ms: rewriting 13.190649ms, bitblasting 0.058749ms, SAT solving 53.069601ms, LRAT trimming 1.609281ms, LRAT checking 4.945249ms +Bitwuzla proved the goal after 62.881973ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.417493ms: rewriting 9.836217ms, bitblasting 0.040956ms, SAT solving 52.930023ms, LRAT trimming 0.299016ms, LRAT checking 2.904156ms +Bitwuzla proved the goal after 62.772459ms, solving context: 0.000000ms +LeanSAT proved the goal after 66.137234ms: rewriting 9.118523ms, bitblasting 0.042589ms, SAT solving 53.255258ms, LRAT trimming 0.335183ms, LRAT checking 2.999293ms +Bitwuzla proved the goal after 62.752845ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.442319ms: rewriting 8.467863ms, bitblasting 0.041197ms, SAT solving 53.362023ms, LRAT trimming 0.347465ms, LRAT checking 2.822924ms +Bitwuzla proved the goal after 62.949251ms, solving context: 0.000000ms +LeanSAT proved the goal after 73.905221ms: rewriting 8.894877ms, bitblasting 0.075981ms, SAT solving 52.982276ms, LRAT trimming 3.371274ms, LRAT checking 8.110571ms +Bitwuzla proved the goal after 61.388888ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.031455ms: rewriting 7.456876ms, bitblasting 0.054932ms, SAT solving 53.275225ms, LRAT trimming 1.350168ms, LRAT checking 4.460799ms +Bitwuzla proved the goal after 63.834323ms, solving context: 0.000000ms +LeanSAT proved the goal after 69.142534ms: rewriting 10.171890ms, bitblasting 0.058880ms, SAT solving 53.327578ms, LRAT trimming 0.961536ms, LRAT checking 4.142437ms +Bitwuzla proved the goal after 61.730024ms, solving context: 0.000000ms +LeanSAT proved the goal after 65.040412ms: rewriting 7.805844ms, bitblasting 0.041657ms, SAT solving 53.508756ms, LRAT trimming 0.187057ms, LRAT checking 3.090643ms +Bitwuzla proved the goal after 60.592437ms, solving context: 0.000000ms +LeanSAT proved the goal after 63.518998ms: rewriting 6.584977ms, bitblasting 0.040555ms, SAT solving 53.305550ms, LRAT trimming 0.313723ms, LRAT checking 2.815431ms +Bitwuzla proved the goal after 62.640293ms, solving context: 0.000000ms +LeanSAT proved the goal after 67.323726ms: rewriting 8.644883ms, bitblasting 0.054972ms, SAT solving 53.003858ms, LRAT trimming 1.022189ms, LRAT checking 4.179306ms