diff --git a/.github/workflows/ocaml-all.yaml b/.github/workflows/ocaml-all.yaml new file mode 100644 index 000000000..c225666c1 --- /dev/null +++ b/.github/workflows/ocaml-all.yaml @@ -0,0 +1,125 @@ +name: OCaml Binding CI (Ubuntu + macOS) + +on: + push: + branches: [ "**" ] + pull_request: + branches: [ "**" ] + +jobs: + build-test: + strategy: + matrix: + os: [ ubuntu-latest, macos-latest] + ocaml-version: ["5"] + fail-fast: false + runs-on: ${{ matrix.os }} + + steps: + - name: Checkout code + uses: actions/checkout@v4 + + # Cache ccache (shared across runs) + - name: Cache ccache + uses: actions/cache@v4 + with: + path: ~/.ccache + key: ${{ runner.os }}-ccache-${{ github.sha }} + restore-keys: | + ${{ runner.os }}-ccache- + + # Cache opam (compiler + packages) + - name: Cache opam + uses: actions/cache@v4 + with: + path: ~/.opam + key: ${{ runner.os }}-opam-${{ matrix.ocaml-version }}-${{ github.sha }} + restore-keys: | + ${{ runner.os }}-opam-${{ matrix.ocaml-version }}- + + # Setup OCaml via action + - uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: ${{ matrix.ocaml-version }} + opam-disable-sandboxing: true + + # Platform-specific dependencies + - name: Install system dependencies (Ubuntu) + if: matrix.os == 'ubuntu-latest' + run: | + sudo apt-get update + sudo apt-get install -y \ + bubblewrap m4 libgmp-dev pkg-config ninja-build ccache + + - name: Install system dependencies (macOS) + if: matrix.os == 'macos-latest' + run: | + brew install gmp pkg-config ninja ccache + + - name: Install required opam packages + run: opam install -y ocamlfind zarith + + # Configure + - name: Configure with CMake + env: + RUNNER_OS: ${{ runner.os }} + CC: ${{ matrix.os == 'macos-latest' && 'ccache clang' || 'ccache gcc' }} + CXX: ${{ matrix.os == 'macos-latest' && 'ccache clang++' || 'ccache g++' }} + run: | + mkdir -p build + cd build + eval $(opam env) + echo "CC: $CC" + echo "CXX: $CXX" + echo "OCAMLFIND: $(which ocamlfind)" + echo "OCAMLC: $(which ocamlc)" + echo "OCAMLOPT: $(which ocamlopt)" + echo "OCAML_VERSION: $(ocamlc -version)" + echo "OCAMLLIB: $OCAMLLIB" + env | grep OCAML + cmake .. \ + -G Ninja \ + -DZ3_BUILD_LIBZ3_SHARED=ON \ + -DZ3_BUILD_OCAML_BINDINGS=ON \ + -DZ3_BUILD_JAVA_BINDINGS=OFF \ + -DZ3_BUILD_PYTHON_BINDINGS=OFF \ + -DZ3_BUILD_CLI=OFF \ + -DZ3_BUILD_TEST_EXECUTABLES=OFF \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE + + - name: Build Z3 and OCaml bindings + run: | + ccache -z || true + eval $(opam env) + cd build + ninja build_z3_ocaml_bindings + ccache -s || true + + - name: Compile ml_example.byte + run: | + eval $(opam env) + ocamlfind ocamlc -o ml_example.byte \ + -package zarith \ + -linkpkg \ + -I build/src/api/ml \ + -dllpath build/src/api/ml \ + build/src/api/ml/z3ml.cma \ + examples/ml/ml_example.ml + + - name: Run ml_example.byte + run: | + eval $(opam env) + ocamlrun ./ml_example.byte + + - name: Compile ml_example (native) + run: | + eval $(opam env) + ocamlfind ocamlopt -o ml_example \ + -package zarith \ + -linkpkg \ + -I build/src/api/ml \ + build/src/api/ml/z3ml.cmxa \ + examples/ml/ml_example.ml + + - name: Run ml_example (native) + run: ./ml_example \ No newline at end of file diff --git a/.github/workflows/ocaml.yaml b/.github/workflows/ocaml.yaml new file mode 100644 index 000000000..d8b64b992 --- /dev/null +++ b/.github/workflows/ocaml.yaml @@ -0,0 +1,99 @@ +name: OCaml Binding CI (Ubuntu) + +on: + push: + branches: [ "**" ] + pull_request: + branches: [ "**" ] + +jobs: + build-test-ocaml: + runs-on: ubuntu-latest + + steps: + - name: Checkout code + uses: actions/checkout@v4 + + - name: Cache ccache + uses: actions/cache@v4 + with: + path: ~/.ccache + key: ${{ runner.os }}-ccache-${{ github.ref }} + restore-keys: | + ${{ runner.os }}-ccache- + + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y \ + opam bubblewrap m4 \ + libgmp-dev pkg-config \ + ninja-build ccache + + - name: Init opam (no sandbox, no default switch) + run: | + opam init --bare --no-setup --disable-sandboxing + opam switch create 5.3.0 + eval $(opam env) + opam install -y ocamlfind zarith + eval $(opam env) + + - name: Configure with CMake + run: | + eval $(opam env) + export CC="ccache gcc" + export CXX="ccache g++" + mkdir -p build + cd build + cmake .. \ + -G Ninja \ + -DZ3_BUILD_LIBZ3_SHARED=ON \ + -DZ3_BUILD_OCAML_BINDINGS=ON \ + -DZ3_BUILD_JAVA_BINDINGS=OFF \ + -DZ3_BUILD_PYTHON_BINDINGS=OFF \ + -DZ3_BUILD_CLI=OFF \ + -DZ3_BUILD_TEST_EXECUTABLES=OFF \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE + + - name: Build Z3 and OCaml bindings + run: | + eval $(opam env) + export CC="ccache gcc" + export CXX="ccache g++" + ocamlc -version + ccache -z # reset stats + cd build + ninja build_z3_ocaml_bindings + ccache -s # show stats + + - name: Compile ml_example.byte + run: | + eval $(opam env) + ocamlc -version + ocamlfind ocamlc -o ml_example.byte \ + -package zarith \ + -linkpkg \ + -I build/src/api/ml \ + -dllpath build/src/api/ml \ + build/src/api/ml/z3ml.cma \ + examples/ml/ml_example.ml + + - name: Run ml_example.byte + run: | + eval $(opam env) + ocamlrun ./ml_example.byte + + - name: Compile ml_example (native) + run: | + eval $(opam env) + ocamlopt -version + ocamlfind ocamlopt -o ml_example \ + -package zarith \ + -linkpkg \ + -I build/src/api/ml \ + build/src/api/ml/z3ml.cmxa \ + examples/ml/ml_example.ml + + - name: Run ml_example (native) + run: | + ./ml_example diff --git a/README-CMake.md b/README-CMake.md index c004f5c7c..dc1f33ec6 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -292,6 +292,9 @@ The following useful options can be passed to CMake whilst configuring. * ``Z3_INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings. * ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``. * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``. +* ``Z3_BUILD_OCAML_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's OCaml bindings will be built. +* ``Z3_BUILD_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Julia bindings will be built. +* ``Z3_INSTALL_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JULIA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Julia bindings. * ``Z3_INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build. * ``Z3_INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build. * ``Z3_BUILD_DOCUMENTATION`` - BOOL. If set to ``TRUE`` then documentation for the API bindings can be built by invoking the ``api_docs`` target. diff --git a/README.md b/README.md index 8f08e7eba..2797c2da2 100644 --- a/README.md +++ b/README.md @@ -16,11 +16,9 @@ See the [release notes](RELEASE_NOTES.md) for notes on various stable releases o ## Build status -| Azure Pipelines | Open Bugs | Android Build | WASM Build | Windows Build | Pyodide Build | -| --------------- | -----------|---------------|------------|---------------|---------------| -| [![Build Status](https://dev.azure.com/Z3Public/Z3/_apis/build/status/Z3Prover.z3?branchName=master)](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) | [![Open Issues](https://github.com/Z3Prover/z3/actions/workflows/wip.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) |[![Android Build](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [![WASM Build](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [![Windows](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml) | [![Pyodide Build](https://github.com/Z3Prover/z3/actions/workflows/pyodide.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/pyodide.yml) - -Docker image. +| Azure Pipelines | Open Bugs | Android Build | WASM Build | Windows Build | Pyodide Build | OCaml Build | +| --------------- | -----------|---------------|------------|---------------|---------------|-------------| +| [![Build Status](https://dev.azure.com/Z3Public/Z3/_apis/build/status/Z3Prover.z3?branchName=master)](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) | [![Open Issues](https://github.com/Z3Prover/z3/actions/workflows/wip.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) |[![Android Build](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [![WASM Build](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [![Windows](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml) | [![Pyodide Build](https://github.com/Z3Prover/z3/actions/workflows/pyodide.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/pyodide.yml) | [![OCaml Build](https://github.com/Z3Prover/z3/actions/workflows/ocaml-all.yaml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/ocaml-all.yaml) | [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang diff --git a/cmake/modules/FindOCaml.cmake b/cmake/modules/FindOCaml.cmake new file mode 100644 index 000000000..a1bbcd228 --- /dev/null +++ b/cmake/modules/FindOCaml.cmake @@ -0,0 +1,106 @@ +# Copied from https://github.com/llvm/llvm-project/tree/main/llvm/cmake/modules/FindOCaml.cmake +# Modified by arbipher at 05/2024 +# +# CMake find_package() module for the OCaml language. +# Assumes ocamlfind will be used for compilation. +# http://ocaml.org/ +# +# Example usage: +# +# find_package(OCaml) +# +# If successful, the following variables will be defined: +# OCAMLFIND +# OCAML_VERSION +# OCAML_STDLIB_PATH +# HAVE_OCAMLOPT +# +# Also provides find_ocamlfind_package() macro. +# +# Example usage: +# +# find_ocamlfind_package(ctypes) +# +# In any case, the following variables are defined: +# +# HAVE_OCAML_${pkg} +# +# If successful, the following variables will be defined: +# +# OCAML_${pkg}_VERSION + +include( FindPackageHandleStandardArgs ) + +find_program(OCAMLFIND + NAMES ocamlfind) + +if( OCAMLFIND ) + execute_process( + COMMAND ${OCAMLFIND} ocamlc -version + OUTPUT_VARIABLE OCAML_VERSION + OUTPUT_STRIP_TRAILING_WHITESPACE) + + execute_process( + COMMAND ${OCAMLFIND} ocamlc -where + OUTPUT_VARIABLE OCAML_STDLIB_PATH + OUTPUT_STRIP_TRAILING_WHITESPACE) + + execute_process( + COMMAND ${OCAMLFIND} ocamlc -version + OUTPUT_QUIET + RESULT_VARIABLE find_ocaml_result) + if( find_ocaml_result EQUAL 0 ) + set(HAVE_OCAMLOPT TRUE) + else() + set(HAVE_OCAMLOPT FALSE) + endif() +endif() + +find_package_handle_standard_args( OCaml DEFAULT_MSG + OCAMLFIND + OCAML_VERSION + OCAML_STDLIB_PATH) + +mark_as_advanced( + OCAMLFIND) + +function(find_ocamlfind_package pkg) + CMAKE_PARSE_ARGUMENTS(ARG "OPTIONAL" "VERSION" "" ${ARGN}) + + execute_process( + COMMAND "${OCAMLFIND}" "query" "${pkg}" "-format" "%v" + RESULT_VARIABLE result + OUTPUT_VARIABLE version + ERROR_VARIABLE error + OUTPUT_STRIP_TRAILING_WHITESPACE + ERROR_STRIP_TRAILING_WHITESPACE) + + if( NOT result EQUAL 0 AND NOT ARG_OPTIONAL ) + message(FATAL_ERROR ${error}) + endif() + + if( result EQUAL 0 ) + set(found TRUE) + else() + set(found FALSE) + endif() + + if( found AND ARG_VERSION ) + if( version VERSION_LESS ARG_VERSION AND ARG_OPTIONAL ) + # If it's optional and the constraint is not satisfied, pretend + # it wasn't found. + set(found FALSE) + elseif( version VERSION_LESS ARG_VERSION ) + message(FATAL_ERROR + "ocamlfind package ${pkg} should have version ${ARG_VERSION} or newer") + endif() + endif() + + string(TOUPPER ${pkg} pkg) + + set(HAVE_OCAML_${pkg} ${found} + PARENT_SCOPE) + + set(OCAML_${pkg}_VERSION ${version} + PARENT_SCOPE) +endfunction() diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5faede21f..071436200 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -299,6 +299,18 @@ if (Z3_BUILD_JAVA_BINDINGS) add_subdirectory(api/java) endif() +################################################################################ +# OCaml bindings +################################################################################ +option(Z3_BUILD_OCAML_BINDINGS "Build OCaml bindings for Z3" OFF) +if (Z3_BUILD_OCAML_BINDINGS) + if (NOT Z3_BUILD_LIBZ3_SHARED) + message(FATAL_ERROR "The OCaml bindings will not work with a static libz3. " + "You either need to disable Z3_BUILD_OCAML_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED") + endif() + add_subdirectory(api/ml) +endif() + ################################################################################ # Julia bindings ################################################################################ diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 193693874..02bcde2a9 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -69,7 +69,7 @@ extern "C" { LOG_Z3_get_global_param_descrs(c); Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c)); mk_c(c)->save_object(d); - d->m_descrs = gparams::get_global_param_descrs(); + d->m_descrs.copy(const_cast(gparams::get_global_param_descrs())); auto r = of_param_descrs(d); RETURN_Z3(r); Z3_CATCH_RETURN(nullptr); diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 5c85ea2cd..2509434f8 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -443,6 +443,16 @@ extern "C" { Z3_CATCH; } + bool Z3_API Z3_is_recursive_datatype_sort(Z3_context c, Z3_sort t) { + Z3_TRY; + LOG_Z3_is_recursive_datatype_sort(c, t); + RESET_ERROR_CODE(); + sort * s = to_sort(t); + datatype_util& dt_util = mk_c(c)->dtutil(); + return dt_util.is_datatype(s) && dt_util.is_recursive(s); + Z3_CATCH_RETURN(false); + } + unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t) { Z3_TRY; LOG_Z3_get_datatype_sort_num_constructors(c, t); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ac28be572..a7bafc0bc 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -1185,6 +1185,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_set_initial_value(c, s, var, value); RESET_ERROR_CODE(); + init_solver(c, s); if (to_expr(var)->get_sort() != to_expr(value)->get_sort()) { SET_ERROR_CODE(Z3_INVALID_USAGE, "variable and value should have same sort"); return; diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 9679a96cd..391cf943c 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -58,7 +58,7 @@ public class Optimize extends Z3Object { /** * Assert a constraint (or multiple) into the optimize solver. **/ - public void Assert(Expr ... constraints) + public void Assert(Expr... constraints) { getContext().checkContextMatch(constraints); for (Expr a : constraints) @@ -70,7 +70,7 @@ public class Optimize extends Z3Object { /** * Alias for Assert. **/ - public void Add(Expr ... constraints) + public void Add(Expr... constraints) { Assert(constraints); } diff --git a/src/api/mcp/z3mcp.py b/src/api/mcp/z3mcp.py new file mode 100644 index 000000000..b292ce1e9 --- /dev/null +++ b/src/api/mcp/z3mcp.py @@ -0,0 +1,19 @@ +# z3mcp.py +from mcp.server.fastmcp import FastMCP +from z3 import * + +# Create an MCP server +mcp = FastMCP("Z3 Solver") + + +# Evaluate SMT commands +@mcp.tool() +def eval(command : str) -> str: + """Evaluate an SMTLIB2 Command using Z3 + Whenever you are faced with a problem that can be formulated as SMTLIB2 constraints + always use this function to solve the problem. + """ + return Z3_eval_smtlib2_string(main_ctx().ctx, command) + +if __name__ == "__main__": + mcp.run() diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt new file mode 100644 index 000000000..e3f3168ad --- /dev/null +++ b/src/api/ml/CMakeLists.txt @@ -0,0 +1,330 @@ +find_package(OCaml REQUIRED) + +set(exe_ext ${CMAKE_EXECUTABLE_SUFFIX}) +set(so_ext ${CMAKE_SHARED_LIBRARY_SUFFIX}) +set(bc_ext ".byte") + +set(z3ml_src ${CMAKE_CURRENT_SOURCE_DIR}) +set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR}) + +if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3) + add_custom_target(libz3_z3ml + ALL + DEPENDS ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3${so_ext} + ) + set(libz3_path ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}) +else() + add_custom_target(libz3_z3ml + ALL + DEPENDS libz3 + ) + set(libz3_path ${PROJECT_BINARY_DIR}) +endif() + +add_custom_command( + OUTPUT + ${z3ml_bin}/z3native.ml + ${z3ml_bin}/z3native_stubs.c + COMMAND "${Python3_EXECUTABLE}" + "${PROJECT_SOURCE_DIR}/scripts/update_api.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--ml-src-dir" + "${CMAKE_CURRENT_SOURCE_DIR}" + "--ml-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + DEPENDS + ${PROJECT_SOURCE_DIR}/scripts/update_api.py + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${z3ml_bin}/z3native_stubs.c" + VERBATIM +) + +add_custom_command( + OUTPUT + ${z3ml_bin}/z3enums.ml + COMMAND "${Python3_EXECUTABLE}" + "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--ml-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + DEPENDS + ${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + COMMENT "Generating ${z3ml_bin}/z3enums.ml" + VERBATIM +) + + +set(z3ml_common_flags "-package" "zarith" + "-I" "${z3ml_bin}") + + # add_custom_command( +# OUTPUT ${z3ml_bin}/z3.ml +# ${z3ml_bin}/z3.mli +# COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.ml" "${z3ml_bin}/z3.ml" +# COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.mli" "${z3ml_bin}/z3.mli" +# DEPENDS ${z3ml_src}/z3.ml +# ${z3ml_src}/z3.mli +# COMMENT "Copying z3.ml and z3.mli to build area") + +# z3native_stubs.c depends on nothing +execute_process( + COMMAND ${OCAMLFIND} ocamlc "-where" + OUTPUT_VARIABLE ocaml_stub_lib_path + OUTPUT_STRIP_TRAILING_WHITESPACE) + +add_custom_command( + OUTPUT ${z3ml_bin}/z3native_stubs.o + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-o" "${z3ml_bin}/z3native_stubs.o" + "-I" "${z3ml_src}" + "-I" "${PROJECT_SOURCE_DIR}/src/api" + "-I" "${ocaml_stub_lib_path}" + "-c" "${z3ml_bin}/z3native_stubs.c" + DEPENDS ${z3ml_bin}/z3native_stubs.c + COMMENT "Building z3native_stubs.o" + VERBATIM) + +message(STATUS "PATH: $ENV{PATH}") +message(STATUS "OCAMLFIND: $ENV{OCAMLFIND}") + +# z3enum.ml depends on nothing +add_custom_command( + OUTPUT ${z3ml_bin}/z3enums.mli + ${z3ml_bin}/z3enums.cmi + ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3enums.cmx + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-i" + "-c" "${z3ml_bin}/z3enums.ml" + ">" "${z3ml_bin}/z3enums.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3enums.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3enums.ml" + COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3enums.ml" + DEPENDS ${z3ml_bin}/z3enums.ml + COMMENT "Building z3enums.{mli,cmi,cmo,cmx}" + VERBATIM) + +# z3native.ml depends on z3enums +add_custom_command( + OUTPUT ${z3ml_bin}/z3native.mli + ${z3ml_bin}/z3native.cmi + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3native.cmx + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-i" + "-c" "${z3ml_bin}/z3native.ml" + ">" "${z3ml_bin}/z3native.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3native.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3native.ml" + COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3native.ml" + DEPENDS ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.ml + COMMENT "Building z3native.{mli,cmi,cmo,cmx}" + VERBATIM) + +# z3.ml depends on z3enums and z3native +add_custom_command( + OUTPUT ${z3ml_bin}/z3.cmi + ${z3ml_bin}/z3.cmo + ${z3ml_bin}/z3.cmx + # COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + # "-c" "${z3ml_bin}/z3.mli" + # COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + # "-c" "${z3ml_bin}/z3.ml" + # COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + # "-c" "${z3ml_bin}/z3.ml" +COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-o" "${z3ml_bin}/z3.cmi" + "-c" "${z3ml_src}/z3.mli" +COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-o" "${z3ml_bin}/z3.cmo" + "-c" "${z3ml_src}/z3.ml" +COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + "-o" "${z3ml_bin}/z3.cmx" + "-c" "${z3ml_src}/z3.ml" + DEPENDS ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.cmo + # ${z3ml_bin}/z3.ml + # ${z3ml_bin}/z3.mli + ${z3ml_src}/z3.ml + ${z3ml_src}/z3.mli + COMMENT "Building z3.cmo" + VERBATIM) + +# making ocaml stublibs +execute_process( + COMMAND ${OCAMLFIND} printconf destdir + OUTPUT_VARIABLE ocaml_destdir_path + OUTPUT_STRIP_TRAILING_WHITESPACE) + +set(ocaml_stublibs_path "${ocaml_destdir_path}/stublibs") + +set(c_lib_deps "-L${libz3_path}" "-lz3" "-lstdc++" "-lpthread") +if (Z3_USE_LIB_GMP) + list(APPEND c_lib_deps "-lgmp") +endif() + +if( APPLE ) + # set(ocaml_rpath "@executable_path/../libz3${so_ext}") +elseif( UNIX ) + set(ocaml_rpath "\\$ORIGIN/../libz3${so_ext}") + list(APPEND c_lib_deps "-dllpath" ${ocaml_rpath}) +endif() + +# We may not directly use CMake's BUILD_RPATH or INSTALL_RPATH since they don't set +# the ocaml stub libraries as a normal library target. + +set(ocamlmklib_flags "-o" "z3ml" + "-ocamlcflags" "-bin-annot" + "-package" "zarith" + ${c_lib_deps} + "-dllpath" "${libz3_path}" + "-L${ocaml_stublibs_path}" + "-dllpath" "${ocaml_stublibs_path}" + "-dllpath" "@rpath/dllz3ml.so" + "-I" "${z3ml_bin}") + +# OCaml's dll stublib hava platform-independent name `dll.so` + +add_custom_command( + OUTPUT ${z3ml_bin}/dllz3ml.so + ${z3ml_bin}/libz3ml.a + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/z3ml.cmxs + COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} + "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.cmo" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmo" + COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} + "${z3ml_bin}/z3enums.cmx" + "${z3ml_bin}/z3native.cmx" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmx" + COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" + "-o" "${z3ml_bin}/z3ml.cmxs" + "-I" "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" + DEPENDS + libz3_z3ml + ${z3ml_bin}/z3native_stubs.o + ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3.cmo + ${z3ml_bin}/z3enums.cmx + ${z3ml_bin}/z3native.cmx + ${z3ml_bin}/z3.cmx + COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml.so, and libz3ml.a" + VERBATIM) + +############################################################################### +# Example +############################################################################### + +execute_process( + COMMAND ${OCAMLFIND} query zarith + OUTPUT_VARIABLE ocaml_pkg_zarith_path + OUTPUT_STRIP_TRAILING_WHITESPACE) + +# Always define patch_z3ml_dylib for dependency consistency +if(APPLE) + add_custom_command( + OUTPUT ${z3ml_bin}/patched_dllz3ml + COMMAND install_name_tool -id "$" "$" + COMMAND install_name_tool -change "@rpath/libz3.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.dylib" "$" "${z3ml_bin}/dllz3ml.so" + COMMAND touch ${z3ml_bin}/patched_dllz3ml + DEPENDS ${z3ml_bin}/dllz3ml.so + COMMENT "Patch install name and reference for macOS" + VERBATIM + ) +else() + add_custom_command( + OUTPUT ${z3ml_bin}/patched_dllz3ml + COMMAND ${CMAKE_COMMAND} -E touch ${z3ml_bin}/patched_dllz3ml + COMMENT "Dummy patch target for non-macOS" + VERBATIM + ) +endif() + +add_custom_target(patch_z3ml_dylib ALL + DEPENDS ${z3ml_bin}/patched_dllz3ml) + +add_custom_target(build_z3_ocaml_bindings + ALL + DEPENDS + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/z3ml.cmxs + ${z3ml_bin}/dllz3ml.so + ${z3ml_bin}/libz3ml.a + patch_z3ml_dylib +) + +# test + +set(z3ml_example_src ${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml) + +add_custom_command( + TARGET build_z3_ocaml_bindings POST_BUILD + COMMAND "${OCAMLFIND}" ocamlc + -o "${z3ml_bin}/ml_example.byte" + -package zarith + -linkpkg + -I "${z3ml_bin}" + -dllpath "${z3ml_bin}" + "${z3ml_bin}/z3ml.cma" + "${z3ml_example_src}" + COMMAND ocamlrun "${z3ml_bin}/ml_example.byte" > "${z3ml_bin}/ml_example.bc.log" + COMMENT "Run OCaml bytecode example" + VERBATIM +) + +add_custom_command( + TARGET build_z3_ocaml_bindings POST_BUILD + COMMAND "${OCAMLFIND}" ocamlopt + -o "${z3ml_bin}/ml_example" + -package zarith + -linkpkg + -I "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" + "${z3ml_example_src}" + COMMAND "${z3ml_bin}/ml_example" > "${z3ml_bin}/ml_example.log" + COMMENT "Run OCaml native example" + VERBATIM +) + +############################################################################### +# Install +############################################################################### + +# Hacky: When the os is APPLE, a fix command will mutate `libz3.dylib` and `dlllibz3.so` inplace. +# I don't know how to use conditional `COMMAND` nor specify a file dependency for itself +# Renaming it and back seems a simple solution. + +# COMMAND mv "${z3ml_bin}/dllz3ml.so" "${z3ml_bin}/dllz3ml.pre.so" +# if (NOT APPLE) +# add_custom_command( +# OUTPUT "${z3ml_bin}/dllz3ml.so" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so}" +# DEPENDS "${z3ml_bin}/dllz3ml.pre.so" +# ) +# else() +# # if IS_OSX: +# # install_name_tool -id ${stubs_install_path}/libz3.dylib libz3.dylib +# # install_name_tool -change libz3.dylib ${stubs_install_path}/libz3.dylib api/ml/dllz3ml.so +# add_custom_command( +# OUTPUT "${z3ml_bin}/dllz3ml.so" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so" +# DEPENDS "${z3ml_bin}/dllz3ml.so" +# ) +# endif() \ No newline at end of file diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 5320fc38e..b7a74049f 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -42,9 +42,10 @@ type context - timeout (unsigned) default timeout (in milliseconds) used for solvers - well_sorted_check type checker - auto_config use heuristics to automatically select solver and configure it - - model model generation for solvers, this parameter can be overwritten when creating a solver - - model_validate validate models produced by solvers - - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver + - model (Boolean) model generation for solvers, this parameter can be overwritten when creating a solver + - model_validate (Boolean) validate models produced by solvers + - unsat_core (Boolean) unsat-core generation for solvers, this parameter can be overwritten when creating a solver + - encoding the string encoding used internally (must be either "unicode" - 18 bit, "bmp" - 16 bit or "ascii" - 8 bit) *) val mk_context : (string * string) list -> context @@ -3712,6 +3713,9 @@ end For example: (set_global_param "pp.decimal" "true") will set the parameter "decimal" in the module "pp" to true. + + Legal parameters are provided by running "z3 -p" or by consulting https://microsoft.github.io/z3guide/programming/Parameters. + *) val set_global_param : string -> string -> unit diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 8fd8ecb0b..9225c2658 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -245,6 +245,7 @@ def _copy_sources(): shutil.rmtree(SRC_DIR_LOCAL, ignore_errors=True) os.mkdir(SRC_DIR_LOCAL) + shutil.copy(os.path.join(SRC_DIR_REPO, 'LICENSE.txt'), ROOT_DIR) shutil.copy(os.path.join(SRC_DIR_REPO, 'LICENSE.txt'), SRC_DIR_LOCAL) shutil.copy(os.path.join(SRC_DIR_REPO, 'z3.pc.cmake.in'), SRC_DIR_LOCAL) shutil.copy(os.path.join(SRC_DIR_REPO, 'CMakeLists.txt'), SRC_DIR_LOCAL) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 4a681c6cb..7e7d9a7b7 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -54,7 +54,7 @@ import io import math import copy if sys.version_info.major >= 3: - from typing import Iterable + from typing import Iterable, Iterator from collections.abc import Callable from typing import ( @@ -155,6 +155,8 @@ def _get_args(args): return args[0] elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)): return [arg for arg in args[0]] + elif len(args) == 1 and isinstance(args[0], Iterator): + return list(args[0]) else: return args except TypeError: # len is not necessarily defined when args is not a sequence (use reflection?) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index dafc26881..b0ac82cab 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4588,6 +4588,13 @@ extern "C" { */ Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i); + /** + \brief Check if \c s is a recursive datatype sort. + + def_API('Z3_is_recursive_datatype_sort', BOOL, (_in(CONTEXT), _in(SORT))) + */ + bool Z3_API Z3_is_recursive_datatype_sort(Z3_context c, Z3_sort s); + /** \brief Return number of constructors for datatype. diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp index 34e45ee4f..7a4c852ef 100644 --- a/src/ast/sls/sls_bv_fixed.cpp +++ b/src/ast/sls/sls_bv_fixed.cpp @@ -21,7 +21,6 @@ namespace sls { bv_fixed::bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx) : ev(ev), - terms(terms), m(ev.m), bv(ev.bv), ctx(ctx) diff --git a/src/ast/sls/sls_bv_fixed.h b/src/ast/sls/sls_bv_fixed.h index d175e9d6a..96799111d 100644 --- a/src/ast/sls/sls_bv_fixed.h +++ b/src/ast/sls/sls_bv_fixed.h @@ -29,7 +29,6 @@ namespace sls { class bv_fixed { bv_eval& ev; - bv_terms& terms; ast_manager& m; bv_util& bv; sls::context& ctx; diff --git a/src/ast/sls/sls_bv_terms.cpp b/src/ast/sls/sls_bv_terms.cpp index fe44d109b..a88b16cb3 100644 --- a/src/ast/sls/sls_bv_terms.cpp +++ b/src/ast/sls/sls_bv_terms.cpp @@ -24,7 +24,6 @@ Author: namespace sls { bv_terms::bv_terms(sls::context& ctx): - ctx(ctx), m(ctx.get_manager()), bv(m), m_axioms(m) {} diff --git a/src/ast/sls/sls_bv_terms.h b/src/ast/sls/sls_bv_terms.h index 5dbf8d72f..062cfaec0 100644 --- a/src/ast/sls/sls_bv_terms.h +++ b/src/ast/sls/sls_bv_terms.h @@ -29,7 +29,6 @@ Author: namespace sls { class bv_terms { - context& ctx; ast_manager& m; bv_util bv; expr_ref_vector m_axioms; diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h index 818f2a9f3..4178c9d05 100644 --- a/src/ast/sls/sls_context.h +++ b/src/ast/sls/sls_context.h @@ -125,7 +125,6 @@ namespace sls { random_gen m_rand; bool m_initialized = false; bool m_new_constraint = false; - bool m_dirty = false; expr_ref_vector m_input_assertions; expr_ref_vector m_allterms; ptr_vector m_subterms; diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index d6ee28466..41b3d55dc 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -43,6 +43,8 @@ z3_add_component(lp polynomial nlsat smt_params + PYG_FILES + lp_params_helper.pyg ) include_directories(${src_SOURCE_DIR}) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index b80702e17..cbe640399 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -92,12 +92,12 @@ namespace lp { } const impq & ub(unsigned j) const { - lp_assert(upper_bound_is_available(j)); + SASSERT(upper_bound_is_available(j)); return get_upper_bound(j); } const impq & lb(unsigned j) const { - lp_assert(lower_bound_is_available(j)); + SASSERT(lower_bound_is_available(j)); return get_lower_bound(j); } @@ -287,7 +287,7 @@ namespace lp { // mpq a; unsigned j; // while (it->next(a, j)) { // if (be.m_j == j) continue; - // lp_assert(bound_is_available(j, is_neg(a) ? lower_bound : !lower_bound)); + // SASSERT(bound_is_available(j, is_neg(a) ? lower_bound : !lower_bound)); // be.m_vector_of_bound_signatures.emplace_back(a, j, numeric_traits:: // is_neg(a)? lower_bound: !lower_bound); // } diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h index 6d35273af..cdd99932a 100644 --- a/src/math/lp/core_solver_pretty_printer_def.h +++ b/src/math/lp/core_solver_pretty_printer_def.h @@ -326,7 +326,7 @@ template void core_solver_pretty_printer::print_g if (m_squash_blanks && string_is_trivial(s)) continue; int number_of_blanks = width - static_cast(s.size()); - lp_assert(number_of_blanks >= 0); + SASSERT(number_of_blanks >= 0); m_out << signs[col] << ' '; print_blanks_local(number_of_blanks, m_out); m_out << s << ' '; @@ -335,7 +335,7 @@ template void core_solver_pretty_printer::print_g string rs = T_to_string(rst); int nb = m_rs_width - static_cast(rs.size()); - lp_assert(nb >= 0); + SASSERT(nb >= 0); print_blanks_local(nb + 1, m_out); m_out << rs << std::endl; } diff --git a/src/math/lp/dense_matrix.h b/src/math/lp/dense_matrix.h index 6b039a920..ab1d92229 100644 --- a/src/math/lp/dense_matrix.h +++ b/src/math/lp/dense_matrix.h @@ -47,7 +47,7 @@ public: dense_matrix(unsigned m, unsigned n); dense_matrix operator*=(matrix const & a) { - lp_assert(column_count() == a.row_count()); + SASSERT(column_count() == a.row_count()); dense_matrix c(row_count(), a.column_count()); for (unsigned i = 0; i < row_count(); i++) { for (unsigned j = 0; j < a.column_count(); j++) { diff --git a/src/math/lp/dense_matrix_def.h b/src/math/lp/dense_matrix_def.h index e850a9acd..858d10eaa 100644 --- a/src/math/lp/dense_matrix_def.h +++ b/src/math/lp/dense_matrix_def.h @@ -175,7 +175,7 @@ template void dense_matrix::multiply_row_by_const template dense_matrix operator* (matrix & a, matrix & b){ - lp_assert(a.column_count() == b.row_count()); + SASSERT(a.column_count() == b.row_count()); dense_matrix ret(a.row_count(), b.column_count()); for (unsigned i = 0; i < ret.m_m; i++) for (unsigned j = 0; j< ret.m_n; j++) { diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 02cc62228..a517b520a 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -343,7 +343,10 @@ namespace lp { return out; } - bool m_has_non_integral_term = false; + // the maximal size of the term to try to tighten the bounds: + // if the size of the term is large than the chances are that the GCD of the coefficients is one + unsigned m_tighten_size_max = 10; + bool m_some_terms_are_ignored = false; std_vector m_sum_of_fixed; // we have to use m_var_register because of the fresh variables: otherwise they clash with the existing lar_solver column indices var_register m_var_register; @@ -353,15 +356,15 @@ namespace lp { int_solver& lia; lar_solver& lra; explanation m_infeas_explanation; - bool m_report_branch = false; // set F // iterate over all rows from 0 to m_e_matrix.row_count() - 1 and return those i such !m_k2s.has_val(i) // set S - iterate over bijection m_k2s mpq m_c; // the constant of the equation struct term_with_index { - // The invariant is that m_index[m_data[k].var()] = k, for each 0 <= k < m_data.size(), - // and m_index[j] = -1, or m_tmp[m_index[j]].var() = j, for every 0 <= j < m_index.size(). + // The invariant is + // 1) m_index[m_data[k].var()] = k, for each 0 <= k < m_data.size(), and + // 2) m_index[j] = -1, or m_data[m_index[j]].var() = j, for every 0 <= j < m_index.size(). // For example m_data = [(coeff, 5), (coeff, 3)] // then m_index = [-1,-1, -1, 1, -1, 0, -1, ....]. std_vector m_data; @@ -375,6 +378,8 @@ namespace lp { return r; } + auto size() const { return m_data.size(); } + bool has(unsigned k) const { return k < m_index.size() && m_index[k] >= 0; } @@ -498,9 +503,9 @@ namespace lp { std::unordered_map> m_row2fresh_defs; indexed_uint_set m_changed_rows; - // m_changed_columns are the columns that just became fixed, or those that just stopped being fixed. + // m_changed_f_columns are the columns that just became fixed, or those that just stopped being fixed. // If such a column appears in an entry it has to be recalculated. - indexed_uint_set m_changed_columns; + indexed_uint_set m_changed_f_columns; indexed_uint_set m_changed_terms; // represented by term columns indexed_uint_set m_terms_to_tighten; // represented by term columns // m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j @@ -516,44 +521,6 @@ namespace lp { m_normalize_conflict_gcd = gcd; lra.stats().m_dio_rewrite_conflicts++; } - unsigned m_max_of_branching_iterations = 0; - unsigned m_number_of_branching_calls; - struct branch { - unsigned m_j = UINT_MAX; - mpq m_rs; - // if m_left is true, then the branch is interpreted - // as x[j] <= m_rs - // otherwise x[j] >= m_rs - bool m_left; - bool m_fully_explored = false; - void flip() { - SASSERT(m_fully_explored == false); - m_left = !m_left; - m_fully_explored = true; - } - }; - struct variable_branch_stats { - std::vector m_ii_after_left; - // g_right[i] - the rumber of int infeasible after taking the i-ith - // right branch - std::vector m_ii_after_right; - - double score() const { - double avm_lefts = - m_ii_after_left.size() - ? static_cast(std::accumulate( - m_ii_after_left.begin(), m_ii_after_left.end(), 0)) / - m_ii_after_left.size() - : std::numeric_limits::infinity(); - double avm_rights = m_ii_after_right.size() - ? static_cast(std::accumulate( - m_ii_after_right.begin(), - m_ii_after_right.end(), 0)) / - m_ii_after_right.size() - : std::numeric_limits::infinity(); - return std::min(avm_lefts, avm_rights); - } - }; void undo_add_term_method(const lar_term* t) { TRACE("d_undo", tout << "t:" << t << ", t->j():" << t->j() << std::endl;); @@ -596,34 +563,61 @@ namespace lp { }; struct protected_queue { - std::queue m_q; - indexed_uint_set m_in_q; + std::list m_q; + std::unordered_map::iterator> m_positions; + bool empty() const { return m_q.empty(); } unsigned size() const { - return (unsigned)m_q.size(); + return static_cast(m_q.size()); } void push(unsigned j) { - if (m_in_q.contains(j)) return; - m_in_q.insert(j); - m_q.push(j); + if (m_positions.find(j) != m_positions.end()) return; + m_q.push_back(j); + m_positions[j] = std::prev(m_q.end()); } unsigned pop_front() { unsigned j = m_q.front(); - m_q.pop(); - SASSERT(m_in_q.contains(j)); - m_in_q.remove(j); + m_q.pop_front(); + m_positions.erase(j); return j; } + void remove(unsigned j) { + auto it = m_positions.find(j); + if (it != m_positions.end()) { + m_q.erase(it->second); + m_positions.erase(it); + } + SASSERT(invariant()); + } + + bool contains(unsigned j) const { + return m_positions.find(j) != m_positions.end(); + } + void reset() { - while (!m_q.empty()) - m_q.pop(); - m_in_q.reset(); + m_q.clear(); + m_positions.clear(); + } + // Invariant method to ensure m_q and m_positions are aligned + bool invariant() const { + if (m_q.size() != m_positions.size()) + return false; + + for (auto it = m_q.begin(); it != m_q.end(); ++it) { + auto pos_it = m_positions.find(*it); + if (pos_it == m_positions.end()) + return false; + if (pos_it->second != it) + return false; + } + + return true; } }; @@ -743,28 +737,33 @@ namespace lp { void add_changed_column(unsigned j) { TRACE("dio", lra.print_column_info(j, tout);); - m_changed_columns.insert(j); + m_changed_f_columns.insert(j); } std_vector m_added_terms; std::unordered_set m_active_terms; - std_vector m_branch_stats; - std_vector m_branch_stack; - std_vector m_explanation_of_branches; + // it is a non-const function : it can set m_some_terms_are_ignored to true + bool term_has_big_number(const lar_term& t) { + for (const auto& p : t) { + if (p.coeff().is_big() || (is_fixed(p.var()) && lra.get_lower_bound(p.var()).x.is_big())) { + m_some_terms_are_ignored = true; + return true; + } + } + return false; + } + + bool ignore_big_nums() const { return lra.settings().dio_ignore_big_nums(); } + + // we add all terms, even those with big numbers, but we might choose to non process the latter. void add_term_callback(const lar_term* t) { unsigned j = t->j(); TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;); if (!lra.column_is_int(j)) { TRACE("dio", tout << "ignored a non-integral column" << std::endl;); - m_has_non_integral_term = true; + m_some_terms_are_ignored = true; return; } - CTRACE("dio", !lra.column_has_term(j), tout << "added term that is not associated with a column yet" << std::endl;); - - if (!lia.column_is_int(t->j())) { - TRACE("dio", tout << "not all vars are integrall\n";); - return; - } m_added_terms.push_back(t); mark_term_change(t->j()); auto undo = undo_add_term(*this, t); @@ -784,7 +783,7 @@ namespace lp { if (!lra.column_is_fixed(j)) return; TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout);); - m_changed_columns.insert(j); + m_changed_f_columns.insert(j); lra.trail().push(undo_fixed_column(*this, j)); } @@ -812,7 +811,7 @@ namespace lp { } void register_columns_to_term(const lar_term& t) { - TRACE("dio_reg", tout << "register term:"; lra.print_term(t, tout); tout << ", t.j()=" << t.j() << std::endl;); + CTRACE("dio_reg", t.j() == 1337, tout << "register term:"; lra.print_term(t, tout); tout << ", t.j()=" << t.j() << std::endl;); for (const auto& p : t.ext_coeffs()) { auto it = m_columns_to_terms.find(p.var()); TRACE("dio_reg", tout << "register p.var():" << p.var() << "->" << t.j() << std::endl;); @@ -854,7 +853,7 @@ namespace lp { } subs_entry(entry_index); SASSERT(entry_invariant(entry_index)); - TRACE("dio", print_entry(entry_index, tout) << std::endl;); + TRACE("dio_entry", print_entry(entry_index, tout) << std::endl;); } void subs_entry(unsigned ei) { if (ei >= m_e_matrix.row_count()) return; @@ -965,7 +964,7 @@ namespace lp { } void find_changed_terms_and_more_changed_rows() { - for (unsigned j : m_changed_columns) { + for (unsigned j : m_changed_f_columns) { const auto it = m_columns_to_terms.find(j); if (it != m_columns_to_terms.end()) for (unsigned k : it->second) { @@ -1013,15 +1012,28 @@ namespace lp { } } - void process_changed_columns(std_vector &f_vector) { + // this is a non-const function - it can set m_some_terms_are_ignored to true + bool is_big_term_or_no_term(unsigned j) { + return + j >= lra.column_count() + || + !lra.column_has_term(j) + || + (ignore_big_nums() && term_has_big_number(lra.get_term(j))); + } + +// Processes columns that have changed due to variables becoming fixed/unfixed or terms being updated. +// It identifies affected terms and rows, recalculates entries, removes irrelevant fresh definitions, +// and ensures substituted variables are properly eliminated from changed F entries, m_e_matrix. +// The function maintains internal consistency of data structures after these updates. + void process_m_changed_f_columns(std_vector &f_vector) { find_changed_terms_and_more_changed_rows(); for (unsigned j: m_changed_terms) { - m_terms_to_tighten.insert(j); - if (j < m_l_matrix.column_count()) { - for (const auto& cs : m_l_matrix.column(j)) { - m_changed_rows.insert(cs.var()); - } - } + if (!is_big_term_or_no_term(j)) + m_terms_to_tighten.insert(j); + if (j < m_l_matrix.column_count()) + for (const auto& cs : m_l_matrix.column(j)) + m_changed_rows.insert(cs.var()); } // find more entries to recalculate @@ -1031,39 +1043,34 @@ namespace lp { if (it == m_row2fresh_defs.end()) continue; for (unsigned xt : it->second) { SASSERT(var_is_fresh(xt)); - for (const auto& p : m_e_matrix.m_columns[xt]) { + for (const auto& p : m_e_matrix.m_columns[xt]) more_changed_rows.push_back(p.var()); - } } } - for (unsigned ei : more_changed_rows) { + for (unsigned ei : more_changed_rows) m_changed_rows.insert(ei); - } - + for (unsigned ei : m_changed_rows) { if (ei >= m_e_matrix.row_count()) continue; if (belongs_to_s(ei)) f_vector.push_back(ei); + recalculate_entry(ei); if (m_e_matrix.m_columns.back().size() == 0) { m_e_matrix.m_columns.pop_back(); m_var_register.shrink(m_e_matrix.column_count()); } - if (m_l_matrix.m_columns.back().size() == 0) { + if (m_l_matrix.m_columns.back().size() == 0) m_l_matrix.m_columns.pop_back(); - } } - remove_irrelevant_fresh_defs(); - eliminate_substituted_in_changed_rows(); - m_changed_columns.reset(); + m_changed_f_columns.reset(); m_changed_rows.reset(); m_changed_terms.reset(); - SASSERT(entries_are_ok()); } int get_sign_in_e_row(unsigned ei, unsigned j) const { @@ -1123,15 +1130,11 @@ namespace lp { } void init(std_vector & f_vector) { - m_report_branch = false; m_infeas_explanation.clear(); lia.get_term().clear(); - m_number_of_branching_calls = 0; - m_branch_stack.clear(); - m_lra_level = 0; reset_conflict(); - process_changed_columns(f_vector); + process_m_changed_f_columns(f_vector); for (const lar_term* t : m_added_terms) { m_active_terms.insert(t); f_vector.push_back(m_e_matrix.row_count()); // going to add a row in fill_entry @@ -1186,8 +1189,7 @@ namespace lp { // A conflict is reported when the gcd of the monomial coefficients does not divide the free coefficent. // If there is no conflict the entry is divided, normalized, by gcd. - // The function returns true if and only if there is no conflict. In the case of a conflict a branch - // can be returned as well. + // The function returns true if and only if there is no conflict. bool normalize_e_by_gcd(unsigned ei, mpq& g) { mpq& e = m_sum_of_fixed[ei]; TRACE("dioph_eq", print_entry(ei, tout) << std::endl;); @@ -1295,6 +1297,59 @@ namespace lp { bool is_substituted_by_fresh(unsigned k) const { return m_fresh_k2xt_terms.has_key(k); } + + // find a variable in q, not neccessarily at the beginning of the queue, that when substituted would create the minimal + // number of non-zeroes + unsigned find_var_to_substitute_on_espace(protected_queue& q) { + // go over all q elements j + // say j is substituted by entry ei = m_k2s[j] + // count the number of variables i in m_e_matrix[ei] that m_espace does not contain i, + // and choose ei where this number is minimal + + unsigned best_var = UINT_MAX; + size_t min_new_vars = std::numeric_limits::max(); + unsigned num_candidates = 0; + std::vector to_remove; + for (unsigned j : q.m_q) { + size_t new_vars = 0; + if (!m_espace.has(j)) { + to_remove.push_back(j); + continue; + } + if (m_k2s.has_key(j)) { + unsigned ei = m_k2s[j]; // entry index for substitution + for (const auto& p : m_e_matrix.m_rows[ei]) + if (p.var() != j && !m_espace.has(p.var())) + ++new_vars; + } + else if (m_fresh_k2xt_terms.has_key(j)) { + const lar_term& fresh_term = m_fresh_k2xt_terms.get_by_key(j).first; + for (const auto& p : fresh_term) + if (p.var() != j && !m_espace.has(p.var())) + ++new_vars; + } + if (new_vars < min_new_vars) { + min_new_vars = new_vars; + best_var = j; + num_candidates = 1; + } + else if (new_vars == min_new_vars) { + ++num_candidates; + if ((lra.settings().random_next() % num_candidates) == 0) + best_var = j; + } + } + + if (best_var != UINT_MAX) + q.remove(best_var); + + for (unsigned j: to_remove) + q.remove(j); + + + return best_var; + } + // The term giving the substitution is in form (+-)x_k + sum {a_i*x_i} + c = 0. // We substitute x_k in t by (+-)coeff*(sum {a_i*x_i} + c), where coeff is // the coefficient of x_k in t. @@ -1303,11 +1358,11 @@ namespace lp { auto r = tighten_on_espace(j); if (r == lia_move::conflict) return lia_move::conflict; - unsigned k = q.pop_front(); - if (!m_espace.has(k)) - return lia_move::undef; + unsigned k = find_var_to_substitute_on_espace(q); + if (k == UINT_MAX) + return lia_move::undef; + SASSERT(m_espace.has(k)); // we might substitute with a term from S or a fresh term - SASSERT(can_substitute(k)); lia_move ret; if (is_substituted_by_fresh(k)) @@ -1385,7 +1440,7 @@ namespace lp { lia_move subs_with_S_and_fresh(protected_queue& q, unsigned j) { lia_move r = lia_move::undef; - while (!q.empty() && r != lia_move::conflict) { + while (!q.empty() && r != lia_move::conflict && m_espace.size() <= m_tighten_size_max) { lia_move ret = subs_front_with_S_and_fresh(q, j); r = join(ret, r); } @@ -1436,8 +1491,13 @@ namespace lp { // print_bounds(tout); ); for (unsigned j : sorted_changed_terms) { - m_terms_to_tighten.remove(j); + if (is_big_term_or_no_term(j)) { + m_terms_to_tighten.remove(j); + continue; + } auto ret = tighten_bounds_for_term_column(j); + m_terms_to_tighten.remove(j); + r = join(ret, r); if (r == lia_move::conflict) break; @@ -1459,25 +1519,37 @@ namespace lp { // We will have lar_t, and let j is lar_t.j(), the term column. // In the m_espace we have lar_t. The result of open_ml((1*j)) is lar_t - (1, j). - // So we have "equality" m_espace = open(m_lspace) + (1*lar_t.j()) - void init_substitutions(const lar_term& lar_t, protected_queue& q) { + // So we have "equality" m_espace = open(m_lspace) + (1*lar_t.j()) + // return false iff seen a big number and dio_ignore_big_nums() is true + bool init_substitutions(const lar_term& lar_t, protected_queue& q) { m_espace.clear(); m_c = mpq(0); m_lspace.clear(); m_lspace.add(mpq(1), lar_t.j()); + bool ret = true; SASSERT(get_extended_term_value(lar_t).is_zero()); for (const auto& p : lar_t) { if (is_fixed(p.j())) { - m_c += p.coeff() * lia.lower_bound(p.j()).x; + const mpq& b = lia.lower_bound(p.j()).x; + if (ignore_big_nums() && b.is_big()) { + ret = false; + break; + } + m_c += p.coeff() * b; } else { unsigned lj = lar_solver_to_local(p.j()); + if (ignore_big_nums() && p.coeff().is_big()) { + ret = false; + break; + } m_espace.add(p.coeff(), lj);; if (can_substitute(lj)) q.push(lj); } } SASSERT(subs_invariant(lar_t.j())); + return ret; } unsigned lar_solver_to_local(unsigned j) const { @@ -1499,8 +1571,6 @@ namespace lp { lia_move tighten_on_espace(unsigned j) { mpq g = gcd_of_coeffs(m_espace.m_data, true); - TRACE("dio", tout << "after process_q_with_S\nt:"; print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;); - if (g.is_one()) return lia_move::undef; if (g.is_zero()) { @@ -1509,15 +1579,11 @@ namespace lp { return lia_move::conflict; return lia_move::undef; } - if (create_branch_report(j, g)) { - lra.settings().stats().m_dio_branch_from_proofs++; - return lia_move::branch; - } // g is not trivial, trying to tighten the bounds auto r = tighten_bounds_for_non_trivial_gcd(g, j, true); if (r == lia_move::undef) r = tighten_bounds_for_non_trivial_gcd(g, j, false); - if (r == lia_move::undef && m_changed_columns.contains(j)) + if (r == lia_move::undef && m_changed_f_columns.contains(j)) r = lia_move::continue_with_check; return r; } @@ -1533,12 +1599,13 @@ namespace lp { lia_move tighten_bounds_for_term_column(unsigned j) { // q is the queue of variables that can be substituted in term_to_tighten protected_queue q; - TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(lra.get_term(j), tout) << std::endl; + TRACE("dio", tout << "j:" << j << " , initial term t: "; print_lar_term_L(lra.get_term(j), tout) << std::endl; for( const auto& p : lra.get_term(j).ext_coeffs()) { lra.print_column_info(p.var(), tout); } ); - init_substitutions(lra.get_term(j), q); + if (!init_substitutions(lra.get_term(j), q)) + return lia_move::undef; TRACE("dio", tout << "t:"; tout << "m_espace:"; @@ -1555,10 +1622,6 @@ namespace lp { return tighten_on_espace(j); } - bool should_report_branch() const { - return (lra.settings().stats().m_dio_calls% lra.settings().dio_report_branch_with_term_tigthening_period()) == 0; - } - void remove_fresh_from_espace() { protected_queue q; for (const auto& p : m_espace.m_data) { @@ -1608,34 +1671,6 @@ namespace lp { return r; } - bool create_branch_report(unsigned j, const mpq& g) { - if (!should_report_branch()) return false; - if (!lia.at_bound(j)) return false; - - mpq rs = (lra.get_column_value(j).x - m_c) / g; - if (rs.is_int()) return false; - m_report_branch = true; - remove_fresh_from_espace(); - SASSERT(get_value_of_espace() + m_c == lra.get_column_value(j).x && lra.get_column_value(j).x.is_int()); - - lar_term& t = lia.get_term(); - t.clear(); - for (const auto& p : m_espace.m_data) { - t.add_monomial(p.coeff() / g, local_to_lar_solver(p.var())); - } - lia.offset() = floor(rs); - lia.is_upper() = true; - m_report_branch = true; - TRACE("dioph_eq", tout << "prepare branch, t:"; - print_lar_term_L(t, tout) - << " <= " << lia.offset() - << std::endl; - tout << "current value of t:" << get_term_value(t) << std::endl; - ); - - SASSERT(get_value_of_espace() / g > lia.offset() ); - return true; - } void get_expl_from_meta_term(const lar_term& t, explanation& ex, const mpq & gcd) { u_dependency* dep = explain_fixed_in_meta_term(t, gcd); for (constraint_index ci : lra.flatten(dep)) @@ -1687,30 +1722,23 @@ namespace lp { mpq rs; bool is_strict = false; u_dependency* b_dep = nullptr; - SASSERT(!g.is_zero()); + SASSERT(!g.is_zero() && !g.is_one()); if (lra.has_bound_of_type(j, b_dep, rs, is_strict, is_upper)) { - TRACE("dio", - tout << "current " << (is_upper? "upper":"lower") << " bound for x" << j << ":" - << rs << std::endl;); + TRACE("dio", tout << "x" << j << (is_upper? " <= ":" >= ") << rs << std::endl;); mpq rs_g = (rs - m_c) % g; - if (rs_g.is_neg()) { + if (rs_g.is_neg()) rs_g += g; - } - if (! (!rs_g.is_neg() && rs_g.is_int())) { - std::cout << "rs:" << rs << "\n"; - std::cout << "m_c:" << m_c << "\n"; - std::cout << "g:" << g << "\n"; - std::cout << "rs_g:" << rs_g << "\n"; - } - SASSERT(rs_g.is_int()); + + SASSERT(rs_g.is_int() && !rs_g.is_neg()); + TRACE("dio", tout << "(rs - m_c) % g:" << rs_g << std::endl;); if (!rs_g.is_zero()) { if (tighten_bound_kind(g, j, rs, rs_g, is_upper)) return lia_move::conflict; - } else { - TRACE("dio", tout << "no improvement in the bound\n";); } + else + TRACE("dio", tout << "rs_g is zero: no improvement in the bound\n";); } return lia_move::undef; } @@ -1773,10 +1801,7 @@ namespace lp { for (const auto& p: fixed_part_of_the_term) { SASSERT(is_fixed(p.var())); if (p.coeff().is_int() && (p.coeff() % g).is_zero()) { - // we can skip this dependency - // because the monomial p.coeff()*p.var() is 0 modulo g, and it does not matter that p.var() is fixed. - // We could have added p.coeff()*p.var() to g*t_, substructed the value of p.coeff()*p.var() from m_c and - // still get the same result. + // we can skip this dependency as explained above TRACE("dio", tout << "skipped dep:\n"; print_deps(tout, lra.get_bound_constraint_witnesses_for_column(p.var()));); continue; } @@ -1788,7 +1813,6 @@ namespace lp { if (lra.settings().get_cancel_flag()) return false; lra.update_column_type_and_bound(j, kind, bound, dep); - lp_status st = lra.find_feasible_solution(); if (is_sat(st) || st == lp::lp_status::CANCELLED) return false; @@ -1852,7 +1876,7 @@ namespace lp { return lia_move::undef; if (r == lia_move::conflict || r == lia_move::undef) break; - SASSERT(m_changed_columns.size() == 0); + SASSERT(m_changed_f_columns.size() == 0); } while (f_vector.size()); @@ -1875,23 +1899,6 @@ namespace lp { return ret; } - void collect_evidence() { - lra.get_infeasibility_explanation(m_infeas_explanation); - for (const auto& p : m_infeas_explanation) { - m_explanation_of_branches.push_back(p.ci()); - } - } - - // returns true if the left and the right branches were explored - void undo_explored_branches() { - TRACE("dio_br", tout << "m_branch_stack.size():" << m_branch_stack.size() << std::endl;); - while (m_branch_stack.size() && m_branch_stack.back().m_fully_explored) { - m_branch_stack.pop_back(); - lra_pop(); - } - TRACE("dio_br", tout << "after pop:m_branch_stack.size():" << m_branch_stack.size() << std::endl;); - } - lia_move check_fixing(unsigned j) const { // do not change entry here unsigned ei = m_k2s[j]; // entry index @@ -1929,141 +1936,12 @@ namespace lp { tout << "fixed j:" << j << ", was substited by "; print_entry(m_k2s[j], tout);); if (check_fixing(j) == lia_move::conflict) { - for (auto ci : lra.flatten(explain_fixed_in_meta_term(m_l_matrix.m_rows[m_k2s[j]], mpq(0)))) { - m_explanation_of_branches.push_back(ci); - } return lia_move::conflict; } } return lia_move::undef; } - void undo_branching() { - while (m_lra_level--) { - lra.pop(); - } - lra.find_feasible_solution(); - SASSERT(lra.get_status() == lp_status::CANCELLED || lra.is_feasible()); - } - // Returns true if a branch is created, and false if not. - // The latter case can happen if we have a sat. - bool push_branch() { - branch br = create_branch(); - if (br.m_j == UINT_MAX) - return false; - m_branch_stack.push_back(br); - lra.stats().m_dio_branching_depth = std::max(lra.stats().m_dio_branching_depth, (unsigned)m_branch_stack.size()); - return true; - } - - lia_move add_var_bound_for_branch(const branch& b) { - if (b.m_left) - lra.add_var_bound(b.m_j, lconstraint_kind::LE, b.m_rs); - else - lra.add_var_bound(b.m_j, lconstraint_kind::GE, b.m_rs + mpq(1)); - TRACE("dio_br", lra.print_column_info(b.m_j, tout) << "add bound" << std::endl;); - if (lra.column_is_fixed(b.m_j)) { - unsigned local_bj; - if (!m_var_register.external_is_used(b.m_j, local_bj)) - return lia_move::undef; - - if (fix_var(local_bj) == lia_move::conflict) { - TRACE("dio_br", tout << "conflict in fix_var" << std::endl;); - return lia_move::conflict; - } - } - return lia_move::undef; - } - - unsigned m_lra_level = 0; - void lra_push() { - m_lra_level++; - lra.push(); - SASSERT(m_lra_level == m_branch_stack.size()); - } - void lra_pop() { - m_lra_level--; - SASSERT(m_lra_level != UINT_MAX); - lra.pop(); - lra.find_feasible_solution(); - SASSERT(lra.get_status() == lp_status::CANCELLED || lra.is_feasible()); - } - - void transfer_explanations_from_closed_branches() { - m_infeas_explanation.clear(); - for (auto ci : m_explanation_of_branches) { - if (this->lra.constraints().valid_index(ci)) - m_infeas_explanation.push_back(ci); - } - } - - lia_move branching_on_undef() { - m_explanation_of_branches.clear(); - bool need_create_branch = true; - m_number_of_branching_calls = 0; - while (++m_number_of_branching_calls < m_max_of_branching_iterations) { - lra.stats().m_dio_branch_iterations++; - if (need_create_branch) { - if (!push_branch()) { - undo_branching(); - lra.stats().m_dio_branching_sats++; - return lia_move::sat; - } - need_create_branch = false; - } - lra_push(); // exploring a new branch - - if (add_var_bound_for_branch(m_branch_stack.back()) == lia_move::conflict) { - undo_explored_branches(); - if (m_branch_stack.size() == 0) { - lra.stats().m_dio_branching_infeasibles++; - transfer_explanations_from_closed_branches(); - lra.stats().m_dio_branching_conflicts++; - return lia_move::conflict; - } - need_create_branch = false; - m_branch_stack.back().flip(); - lra_pop(); - continue; - } - auto st = lra.find_feasible_solution(); - TRACE("dio_br", tout << "st:" << lp_status_to_string(st) << std::endl;); - if (st == lp_status::CANCELLED) - return lia_move::undef; - else if (lp::is_sat(st)) { - // have a feasible solution - unsigned n_of_ii = get_number_of_int_inf(); - TRACE("dio_br", tout << "n_of_ii:" << n_of_ii << "\n";); - if (n_of_ii == 0) { - undo_branching(); - lra.stats().m_dio_branching_sats++; - return lia_move::sat; - } - // got to create a new branch - update_branch_stats(m_branch_stack.back(), n_of_ii); - need_create_branch = true; - } - else { - collect_evidence(); - undo_explored_branches(); - if (m_branch_stack.size() == 0) { - lra.stats().m_dio_branching_infeasibles++; - transfer_explanations_from_closed_branches(); - lra.stats().m_dio_branching_conflicts++; - return lia_move::conflict; - } - TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl; - tout << "explanation:\n"; lra.print_expl(tout, m_infeas_explanation);); - - need_create_branch = false; - lra_pop(); - m_branch_stack.back().flip(); - } - } - undo_branching(); - return lia_move::undef; - } - unsigned get_number_of_int_inf() const { return (unsigned)std::count_if( lra.r_basis().begin(), lra.r_basis().end(), @@ -2072,61 +1950,6 @@ namespace lp { }); } - double get_branch_score(unsigned j) { - if (j >= m_branch_stats.size()) - m_branch_stats.resize(j + 1); - return m_branch_stats[j].score(); - } - - void update_branch_stats(const branch& b, unsigned n_of_ii) { - // Ensure the branch stats vector is large enough - if (b.m_j >= m_branch_stats.size()) - m_branch_stats.resize(b.m_j + 1); - - if (b.m_left) - m_branch_stats[b.m_j].m_ii_after_left.push_back(n_of_ii); - else - m_branch_stats[b.m_j].m_ii_after_right.push_back(n_of_ii); - } - - branch create_branch() { - unsigned bj = UINT_MAX; - double score = std::numeric_limits::infinity(); - // looking for the minimal score - unsigned n = 0; - for (unsigned j : lra.r_basis()) { - if (!lia.column_is_int_inf(j)) - continue; - double sc = get_branch_score(j); - if (sc < score || - (sc == score && lra.settings().random_next() % (++n) == 0)) { - score = sc; - bj = j; - } - } - branch br; - if (bj == UINT_MAX) { // it the case when we cannot create a branch - SASSERT( - lra.settings().get_cancel_flag() || - (lra.is_feasible() && [&]() { - for (unsigned j = 0; j < lra.column_count(); ++j) { - if (lia.column_is_int_inf(j)) { - return false; - } - } - return true; - }())); - return br; // to signal that we have no ii variables - } - - br.m_j = bj; - br.m_left = (lra.settings().random_next() % 2 == 0); - br.m_rs = floor(lra.get_column_value(bj).x); - - TRACE("dio_br", tout << "score:" << score << "; br.m_j:" << br.m_j << "," - << (br.m_left ? "left" : "right") << ", br.m_rs:" << br.m_rs << std::endl;); - return br; - } bool columns_to_terms_is_correct() const { std::unordered_map> c2t; @@ -2180,11 +2003,12 @@ namespace lp { bool is_in_sync() const { for (unsigned j = 0; j < m_e_matrix.column_count(); j++) { unsigned external_j = m_var_register.local_to_external(j); - if (external_j == UINT_MAX) continue; - if (external_j >= lra.column_count() && m_e_matrix.m_columns[j].size()) { - // It is OK to have an empty column in m_e_matrix. + if (external_j == UINT_MAX) + continue; + if (external_j >= lra.column_count() && m_e_matrix.m_columns[j].size()) return false; - } + // It is OK to have an empty column in m_e_matrix. + } for (unsigned ei = 0; ei < m_e_matrix.row_count(); ei++) { @@ -2214,11 +2038,8 @@ namespace lp { if (ret != lia_move::undef) return ret; - - if (lra.stats().m_dio_calls % lra.settings().dio_branching_period() == 0) - ret = branching_on_undef(); - - m_max_of_branching_iterations = (unsigned)m_max_of_branching_iterations / 2; + if (ret == lia_move::undef) + lra.settings().dio_calls_period() *= 2; return ret; } @@ -2692,8 +2513,8 @@ namespace lp { // needed for the template bound_analyzer_on_row.h const lar_solver& lp() const { return lra; } lar_solver& lp() {return lra;} - bool has_non_integral_term() const { - return m_has_non_integral_term; + bool some_terms_are_ignored() const { + return m_some_terms_are_ignored; } }; // Constructor definition @@ -2712,8 +2533,8 @@ namespace lp { m_imp->explain(ex); } - bool dioph_eq::has_non_integral_term() const { - return m_imp->has_non_integral_term(); + bool dioph_eq::some_terms_are_ignored() const { + return m_imp->some_terms_are_ignored(); } diff --git a/src/math/lp/dioph_eq.h b/src/math/lp/dioph_eq.h index e266e7dd6..cefcecc54 100644 --- a/src/math/lp/dioph_eq.h +++ b/src/math/lp/dioph_eq.h @@ -11,8 +11,9 @@ Abstract: by Alberto Griggio(griggio@fbk.eu) Author: + Nikolaj Bjorner (nbjorner) Lev Nachmanson (levnach) - + Revision History: --*/ #pragma once @@ -30,6 +31,6 @@ namespace lp { ~dioph_eq(); lia_move check(); void explain(lp::explanation&); - bool has_non_integral_term() const; + bool some_terms_are_ignored() const; }; } diff --git a/src/math/lp/general_matrix.h b/src/math/lp/general_matrix.h index e42f01ad7..87a79ec27 100644 --- a/src/math/lp/general_matrix.h +++ b/src/math/lp/general_matrix.h @@ -98,16 +98,16 @@ public: void clear() { m_data.clear(); } bool row_is_initialized_correctly(const vector& row) { - lp_assert(row.size() == column_count()); + SASSERT(row.size() == column_count()); for (unsigned j = 0; j < row.size(); j ++) - lp_assert(is_zero(row[j])); + SASSERT(is_zero(row[j])); return true; } template void init_row_from_container(int i, const T & c, std::function column_fix, const mpq& sign) { auto & row = m_data[adjust_row(i)]; - lp_assert(row_is_initialized_correctly(row)); + SASSERT(row_is_initialized_correctly(row)); for (lp::lar_term::ival p : c) { unsigned j = adjust_column(column_fix(p.j())); row[j] = sign * p.coeff(); @@ -115,7 +115,7 @@ public: } general_matrix operator*(const general_matrix & m) const { - lp_assert(m.row_count() == column_count()); + SASSERT(m.row_count() == column_count()); general_matrix ret(row_count(), m.column_count()); for (unsigned i = 0; i < row_count(); i ++) { for (unsigned j = 0; j < m.column_count(); j++) { @@ -158,7 +158,7 @@ public: vector operator*(const vector & x) const { vector r; - lp_assert(x.size() == column_count()); + SASSERT(x.size() == column_count()); for (unsigned i = 0; i < row_count(); i++) { mpq v(0); for (unsigned j = 0; j < column_count(); j++) { @@ -171,12 +171,12 @@ public: void transpose_rows(unsigned i, unsigned l) { - lp_assert(i != l); + SASSERT(i != l); m_row_permutation.transpose_from_right(i, l); } void transpose_columns(unsigned j, unsigned k) { - lp_assert(j != k); + SASSERT(j != k); m_column_permutation.transpose_from_left(j, k); } @@ -210,7 +210,7 @@ public: // used for debug only general_matrix take_first_n_columns(unsigned n) const { - lp_assert(n <= column_count()); + SASSERT(n <= column_count()); if (n == column_count()) return *this; general_matrix ret(row_count(), n); diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index c6f9a4123..d5db5093d 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -58,7 +58,7 @@ struct create_cut { } void int_case_in_gomory_cut(unsigned j) { - lp_assert(is_int(j) && m_fj.is_pos()); + SASSERT(is_int(j) && m_fj.is_pos()); TRACE("gomory_cut_detail", tout << " k = " << m_k; tout << ", fj: " << m_fj << ", "; @@ -68,15 +68,15 @@ struct create_cut { if (at_lower(j)) { // here we have the product of new_a*(xj - lb(j)), so new_a*lb(j) is added to m_k new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f); - lp_assert(new_a.is_pos()); + SASSERT(new_a.is_pos()); m_k.addmul(new_a, lower_bound(j).x); push_explanation(column_lower_bound_constraint(j)); } else { - lp_assert(at_upper(j)); + SASSERT(at_upper(j)); // here we have the expression new_a*(xj - ub), so new_a*ub(j) is added to m_k new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f)); - lp_assert(new_a.is_neg()); + SASSERT(new_a.is_neg()); m_k.addmul(new_a, upper_bound(j).x); push_explanation(column_upper_bound_constraint(j)); } @@ -111,7 +111,7 @@ struct create_cut { push_explanation(column_lower_bound_constraint(j)); } else { - lp_assert(at_upper(j)); + SASSERT(at_upper(j)); if (a.is_pos()) { // the delta is works again m_f new_a = - a / m_f; @@ -134,7 +134,7 @@ struct create_cut { } lia_move report_conflict_from_gomory_cut() { - lp_assert(m_k.is_pos()); + SASSERT(m_k.is_pos()); // conflict 0 >= k where k is positive return lia_move::conflict; } @@ -204,7 +204,7 @@ struct create_cut { else if (at_lower(j)) dump_lower_bound_expl(out, j); else { - lp_assert(at_upper(j)); + SASSERT(at_upper(j)); dump_upper_bound_expl(out, j); } } @@ -259,7 +259,7 @@ public: m_found_big = false; TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", "; tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f << "\n";); - lp_assert(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); + SASSERT(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); auto set_polarity_for_int = [&](const mpq & a, lpvar j) { if (a.is_pos()) { if (at_lower(j)) diff --git a/src/math/lp/hnf.h b/src/math/lp/hnf.h index 75a69393f..d48c81f34 100644 --- a/src/math/lp/hnf.h +++ b/src/math/lp/hnf.h @@ -78,31 +78,31 @@ void extended_gcd_minimal_uv(const mpq & a, const mpq & b, mpq & d, mpq & u, mpq k -= one_of_type(); } - lp_assert(v == k * a_over_d + r); + SASSERT(v == k * a_over_d + r); if (is_pos(b)) { v = r - a_over_d; // v -= (k + 1) * a_over_d; - lp_assert(- a_over_d < v && v <= zero_of_type()); + SASSERT(- a_over_d < v && v <= zero_of_type()); if (is_pos(a)) { u += (k + 1) * (b / d); - lp_assert( one_of_type() <= u && u <= abs(b)/d); + SASSERT( one_of_type() <= u && u <= abs(b)/d); } else { u -= (k + 1) * (b / d); - lp_assert( one_of_type() <= -u && -u <= abs(b)/d); + SASSERT( one_of_type() <= -u && -u <= abs(b)/d); } } else { v = r; // v -= k * a_over_d; - lp_assert(- a_over_d < -v && -v <= zero_of_type()); + SASSERT(- a_over_d < -v && -v <= zero_of_type()); if (is_pos(a)) { u += k * (b / d); - lp_assert( one_of_type() <= u && u <= abs(b)/d); + SASSERT( one_of_type() <= u && u <= abs(b)/d); } else { u -= k * (b / d); - lp_assert( one_of_type() <= -u && -u <= abs(b)/d); + SASSERT( one_of_type() <= -u && -u <= abs(b)/d); } } - lp_assert(d == u * a + v * b); + SASSERT(d == u * a + v * b); } @@ -127,7 +127,7 @@ bool prepare_pivot_for_lower_triangle(M &m, unsigned r) { template void pivot_column_non_fractional(M &m, unsigned r, bool & overflow, const mpq & big_number) { - lp_assert(!is_zero(m[r][r])); + SASSERT(!is_zero(m[r][r])); for (unsigned j = r + 1; j < m.column_count(); j++) { for (unsigned i = r + 1; i < m.row_count(); i++) { if ( @@ -137,7 +137,7 @@ void pivot_column_non_fractional(M &m, unsigned r, bool & overflow, const mpq & overflow = true; return; } - lp_assert(is_integer(m[i][j])); + SASSERT(is_integer(m[i][j])); } } } @@ -154,7 +154,7 @@ unsigned to_lower_triangle_non_fractional(M &m, bool & overflow, const mpq& big_ if (overflow) return 0; } - lp_assert(i == m.row_count()); + SASSERT(i == m.row_count()); return i; } @@ -168,7 +168,7 @@ mpq gcd_of_row_starting_from_diagonal(const M& m, unsigned i) { if (!is_zero(t)) g = abs(t); } - lp_assert(!is_zero(g)); + SASSERT(!is_zero(g)); for (; j < m.column_count(); j++) { const auto & t = m[i][j]; if (!is_zero(t)) @@ -249,7 +249,7 @@ class hnf { } void buffer_p_col_i_plus_q_col_j_W_modulo(const mpq & p, const mpq & q) { - lp_assert(zeros_in_column_W_above(m_i)); + SASSERT(zeros_in_column_W_above(m_i)); for (unsigned k = m_i; k < m_m; k++) { m_buffer[k] = mod_R_balanced(mod_R_balanced(p * m_W[k][m_i]) + mod_R_balanced(q * m_W[k][m_j])); } @@ -262,7 +262,7 @@ class hnf { } void pivot_column_i_to_column_j_H(mpq u, unsigned i, mpq v, unsigned j) { - lp_assert(is_zero(u * m_H[i][i] + v * m_H[i][j])); + SASSERT(is_zero(u * m_H[i][i] + v * m_H[i][j])); m_H[i][j] = zero_of_type(); for (unsigned k = i + 1; k < m_m; k ++) m_H[k][j] = u * m_H[k][i] + v * m_H[k][j]; @@ -270,7 +270,7 @@ class hnf { } #endif void pivot_column_i_to_column_j_W_modulo(mpq u, mpq v) { - lp_assert(is_zero((u * m_W[m_i][m_i] + v * m_W[m_i][m_j]) % m_R)); + SASSERT(is_zero((u * m_W[m_i][m_i] + v * m_W[m_i][m_j]) % m_R)); m_W[m_i][m_j] = zero_of_type(); for (unsigned k = m_i + 1; k < m_m; k ++) m_W[k][m_j] = mod_R_balanced(mod_R_balanced(u * m_W[k][m_i]) + mod_R_balanced(v * m_W[k][m_j])); @@ -364,14 +364,14 @@ class hnf { } void replace_column_j_by_j_minus_u_col_i_H(unsigned i, unsigned j, const mpq & u) { - lp_assert(j < i); + SASSERT(j < i); for (unsigned k = i; k < m_m; k++) { m_H[k][j] -= u * m_H[k][i]; } } void replace_column_j_by_j_minus_u_col_i_U(unsigned i, unsigned j, const mpq & u) { - lp_assert(j < i); + SASSERT(j < i); for (unsigned k = 0; k < m_n; k++) { m_U[k][j] -= u * m_U[k][i]; } @@ -405,7 +405,7 @@ class hnf { process_row_column(i, j); } if (i >= m_n) { - lp_assert(m_H == m_A_orig * m_U); + SASSERT(m_H == m_A_orig * m_U); return; } if (is_neg(m_H[i][i])) @@ -427,7 +427,7 @@ class hnf { m_U_reverse = m_U; - lp_assert(m_H == m_A_orig * m_U); + SASSERT(m_H == m_A_orig * m_U); } bool row_is_correct_form(unsigned i) const { @@ -489,7 +489,7 @@ private: } void replace_column_j_by_j_minus_u_col_i_W(unsigned j, const mpq & u) { - lp_assert(j < m_i); + SASSERT(j < m_i); for (unsigned k = m_i; k < m_m; k++) { m_W[k][j] -= u * m_W[k][m_i]; // m_W[k][j] = mod_R_balanced(m_W[k][j]); @@ -546,7 +546,7 @@ private: if (is_zero(mii)) mii = d; - lp_assert(is_pos(mii)); + SASSERT(is_pos(mii)); // adjust column m_i for (unsigned k = m_i + 1; k < m_m; k++) { @@ -554,7 +554,7 @@ private: m_W[k][m_i] = mod_R_balanced(m_W[k][m_i]); } - lp_assert(is_pos(mii)); + SASSERT(is_pos(mii)); for (unsigned j = 0; j < m_i; j++) { const mpq & mij = m_W[m_i][j]; if (!is_pos(mij) && - mij < mii) @@ -575,9 +575,9 @@ private: void calculate_by_modulo() { for (m_i = 0; m_i < m_m; m_i ++) { process_row_modulo(); - lp_assert(is_pos(m_W[m_i][m_i])); + SASSERT(is_pos(m_W[m_i][m_i])); m_R /= m_W[m_i][m_i]; - lp_assert(is_integer(m_R)); + SASSERT(is_integer(m_R)); m_half_R = floor(m_R / 2); } } @@ -609,7 +609,7 @@ public: tout << "A = "; m_A_orig.print(tout, 4); tout << std::endl; tout << "H = "; m_H.print(tout, 4); tout << std::endl; tout << "W = "; m_W.print(tout, 4); tout << std::endl;); - lp_assert (m_H == m_W); + SASSERT (m_H == m_W); #endif } diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index 192be557d..294467177 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -99,7 +99,7 @@ namespace lp { if (is_integer(b[i])) continue; if (n == 0) { - lp_assert(ret == -1); + SASSERT(ret == -1); n = 1; ret = i; } @@ -202,7 +202,7 @@ branch y_i >= ceil(y0_i) is impossible. hnf h(m_A, d); vector b = create_b(basis_rows); #ifdef Z3DEBUG - lp_assert(m_A * x0 == b); + SASSERT(m_A * x0 == b); #endif find_h_minus_1_b(h.W(), b); @@ -274,7 +274,7 @@ branch y_i >= ceil(y0_i) is impossible. for (auto ci : lra.flatten(dep)) lra.constraints().display(tout, ci); ); - lp_assert(lia.current_solution_is_inf_on_cut()); + SASSERT(lia.current_solution_is_inf_on_cut()); lia.settings().stats().m_hnf_cuts++; lia.expl()->clear(); for (u_dependency* dep : constraints_for_explanation()) diff --git a/src/math/lp/incremental_vector.h b/src/math/lp/incremental_vector.h index 0bb2829eb..50a0a6f96 100644 --- a/src/math/lp/incremental_vector.h +++ b/src/math/lp/incremental_vector.h @@ -43,7 +43,7 @@ public: template void pop_tail(vector & v, unsigned k) { - lp_assert(v.size() >= k); + SASSERT(v.size() >= k); v.shrink(v.size() - k); } @@ -53,8 +53,8 @@ public: } void pop_scope(unsigned k) { - lp_assert(m_stack_of_vector_sizes.size() >= k); - lp_assert(k > 0); + SASSERT(m_stack_of_vector_sizes.size() >= k); + SASSERT(k > 0); m_vector.shrink(peek_size(k)); unsigned new_st_size = m_stack_of_vector_sizes.size() - k; m_stack_of_vector_sizes.shrink(new_st_size); @@ -65,7 +65,7 @@ public: } unsigned peek_size(unsigned k) const { - lp_assert(k > 0 && k <= m_stack_of_vector_sizes.size()); + SASSERT(k > 0 && k <= m_stack_of_vector_sizes.size()); return m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]; } }; diff --git a/src/math/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h index 1bb05ce84..724a08c28 100644 --- a/src/math/lp/indexed_vector_def.h +++ b/src/math/lp/indexed_vector_def.h @@ -39,7 +39,7 @@ void indexed_vector::resize(unsigned data_size) { template void indexed_vector::set_value(const T& value, unsigned index) { m_data[index] = value; - lp_assert(std::find(m_index.begin(), m_index.end(), index) == m_index.end()); + SASSERT(std::find(m_index.begin(), m_index.end(), index) == m_index.end()); m_index.push_back(index); } diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index 3e3b9e555..a5ce3c291 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -33,7 +33,7 @@ lia_move int_branch::create_branch_on_column(int j) { TRACE("check_main_int", tout << "branching" << std::endl;); lia.get_term().clear(); - lp_assert(j != -1); + SASSERT(j != -1); lia.get_term().add_monomial(mpq(1), j); if (lia.is_free(j)) { lia.is_upper() = lia.settings().random_next() % 2; diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp index c8488ca37..fc9d5678b 100644 --- a/src/math/lp/int_cube.cpp +++ b/src/math/lp/int_cube.cpp @@ -50,7 +50,7 @@ namespace lp { lra.pop(); lra.round_to_integer_solution(); lra.set_status(lp_status::FEASIBLE); - lp_assert(lia.settings().get_cancel_flag() || lia.is_feasible()); + SASSERT(lia.settings().get_cancel_flag() || lia.is_feasible()); TRACE("cube", tout << "success";); lia.settings().stats().m_cube_success++; return lia_move::sat; @@ -78,7 +78,7 @@ namespace lp { void int_cube::find_feasible_solution() { lra.find_feasible_solution(); - lp_assert(lp_status::OPTIMAL == lra.get_status() || lp_status::FEASIBLE == lra.get_status()); + SASSERT(lp_status::OPTIMAL == lra.get_status() || lp_status::FEASIBLE == lra.get_status()); } impq int_cube::get_cube_delta_for_term(const lar_term& t) const { diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 11648f7bd..960287ab4 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -41,7 +41,6 @@ namespace lp { mpq m_k; // the right side of the cut hnf_cutter m_hnf_cutter; unsigned m_hnf_cut_period; - unsigned m_dioph_eq_period; dioph_eq m_dio; int_gcd_test m_gcd; @@ -51,7 +50,6 @@ namespace lp { imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_dio(lia), m_gcd(lia) { m_hnf_cut_period = settings().hnf_cut_period(); - m_dioph_eq_period = settings().m_dioph_eq_period; } bool has_lower(unsigned j) const { @@ -113,7 +111,7 @@ namespace lp { } // if bj == v, then, because we are patching the lra.get_value(v), // we just need to assert that the lra.get_value(v) would be integral. - lp_assert(bj != v || lra.from_model_in_impq_to_mpq(new_val).is_int()); + SASSERT(bj != v || lra.from_model_in_impq_to_mpq(new_val).is_int()); } lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta)); @@ -142,8 +140,8 @@ namespace lp { return false; mpq a = fractional_part(c.coeff()); mpq r = fractional_part(lra.get_value(v)); - lp_assert(0 < r && r < 1); - lp_assert(0 < a && a < 1); + SASSERT(0 < r && r < 1); + SASSERT(0 < a && a < 1); mpq delta_plus, delta_minus; if (!get_patching_deltas(r, a, delta_plus, delta_minus)) return false; @@ -159,7 +157,7 @@ namespace lp { lia_move patch_basic_columns() { lia.settings().stats().m_patches++; lra.remove_fixed_vars_from_base(); - lp_assert(lia.is_feasible()); + SASSERT(lia.is_feasible()); for (unsigned j : lra.r_basis()) if (!lra.get_value(j).is_int() && lra.column_is_int(j) && !lia.is_fixed(j)) patch_basic_column(j); @@ -187,20 +185,19 @@ namespace lp { } bool should_gomory_cut() { - bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() || - m_dio.has_non_integral_term(); - + bool dio_allows_gomory = !settings().dio() || settings().dio_enable_gomory_cuts() || + m_dio.some_terms_are_ignored(); return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0; } bool should_solve_dioph_eq() { - return lia.settings().dio_eqs() && m_number_of_calls % m_dioph_eq_period == 0; + return lia.settings().dio() && (m_number_of_calls % settings().dio_calls_period() == 0); } // HNF bool should_hnf_cut() { - return (!settings().dio_eqs() || settings().dio_enable_hnf_cuts()) + return (!settings().dio() || settings().dio_enable_hnf_cuts()) && settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0; } @@ -226,7 +223,7 @@ namespace lp { lia_move r = lia_move::undef; - if (m_gcd.should_apply()) + if (m_gcd.should_apply() || (settings().dio() && m_dio.some_terms_are_ignored())) r = m_gcd(); check_return_helper pc(lra); @@ -405,16 +402,16 @@ namespace lp { // coprime. We can find u and v such that u*a1 + v*x2 = 1. rational u, v; gcd(a1, x2, u, v); - lp_assert(gcd(a1, x2, u, v).is_one()); - lp_assert((x + (a1 / a2) * (-u * t) * x1).is_int()); + SASSERT(gcd(a1, x2, u, v).is_one()); + SASSERT((x + (a1 / a2) * (-u * t) * x1).is_int()); // 1 = (u- l*x2 ) * a1 + (v + l*a1)*x2, for every integer l. rational d = u * t * x1; // We can prove that x+alpha*d is integral, // and any other delta, satisfying x+alpha*delta, is equal to d modulo a2. delta_plus = mod(d, a2); - lp_assert(delta_plus > 0); + SASSERT(delta_plus > 0); delta_minus = delta_plus - a2; - lp_assert(delta_minus < 0); + SASSERT(delta_minus < 0); return true; } @@ -551,7 +548,7 @@ namespace lp { const mpq & a = c.coeff(); unsigned i = lrac.m_r_basis[row_index]; impq const & xi = get_value(i); - lp_assert(lrac.m_r_solver.column_is_feasible(i)); + SASSERT(lrac.m_r_solver.column_is_feasible(i)); if (column_is_int(i) && !a.is_int() && xi.is_int()) m = lcm(m, denominator(a)); @@ -591,7 +588,7 @@ namespace lp { bool int_solver::is_feasible() const { - lp_assert( + SASSERT( lrac.m_r_solver.calc_current_x_is_feasible_include_non_basis() == lrac.m_r_solver.current_x_is_feasible()); return lrac.m_r_solver.current_x_is_feasible(); diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index 8e727bce9..b0252b624 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -117,8 +117,8 @@ public: void fill_not_improvable_zero_sum(); void push() { - lp_assert(m_r_solver.basis_heading_is_correct()); - lp_assert(m_column_types.size() == m_r_A.column_count()); + SASSERT(m_r_solver.basis_heading_is_correct()); + SASSERT(m_column_types.size() == m_r_A.column_count()); m_stacked_simplex_strategy = settings().simplex_strategy(); m_stacked_simplex_strategy.push(); m_column_types.push(); @@ -140,20 +140,20 @@ public: m_stacked_simplex_strategy.pop(k); m_r_solver.m_settings.simplex_strategy() = m_stacked_simplex_strategy; m_infeasible_linear_combination.reset(); - lp_assert(m_r_solver.basis_heading_is_correct()); + SASSERT(m_r_solver.basis_heading_is_correct()); } bool r_basis_is_OK() const { #ifdef Z3DEBUG for (unsigned j : m_r_solver.m_basis) { - lp_assert(m_r_solver.m_A.m_columns[j].size() == 1); + SASSERT(m_r_solver.m_A.m_columns[j].size() == 1); } for (unsigned j =0; j < m_r_solver.m_basis_heading.size(); j++) { if (m_r_solver.m_basis_heading[j] >= 0) continue; if (m_r_solver.m_column_types[j] == column_type::fixed) continue; - lp_assert(static_cast(- m_r_solver.m_basis_heading[j] - 1) < m_r_solver.m_column_types.size()); - lp_assert( m_r_solver.m_basis_heading[j] <= -1); + SASSERT(static_cast(- m_r_solver.m_basis_heading[j] - 1) < m_r_solver.m_column_types.size()); + SASSERT( m_r_solver.m_basis_heading[j] <= -1); } #endif return true; @@ -191,14 +191,14 @@ public: } void update_delta(mpq& delta, numeric_pair const& l, numeric_pair const& u) const { - lp_assert(l <= u); + SASSERT(l <= u); if (l.x < u.x && l.y > u.y) { mpq delta1 = (u.x - l.x) / (l.y - u.y); if (delta1 < delta) { delta = delta1; } } - lp_assert(l.x + delta * l.y <= u.x + delta * u.y); + SASSERT(l.x + delta * l.y <= u.x + delta * u.y); } @@ -234,14 +234,14 @@ public: const impq & lower_bound(unsigned j) const { - lp_assert(m_column_types()[j] == column_type::fixed || + SASSERT(m_column_types()[j] == column_type::fixed || m_column_types()[j] == column_type::boxed || m_column_types()[j] == column_type::lower_bound); return m_r_lower_bounds[j]; } const impq & upper_bound(unsigned j) const { - lp_assert(m_column_types()[j] == column_type::fixed || + SASSERT(m_column_types()[j] == column_type::fixed || m_column_types()[j] == column_type::boxed || m_column_types()[j] == column_type::upper_bound); return m_r_upper_bounds[j]; diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 8fc98db1d..5dbd32cb5 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -84,8 +84,8 @@ unsigned lar_core_solver::get_number_of_non_ints() const { void lar_core_solver::solve() { TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";); - lp_assert(m_r_solver.non_basic_columns_are_set_correctly()); - lp_assert(m_r_solver.inf_heap_is_correct()); + SASSERT(m_r_solver.non_basic_columns_are_set_correctly()); + SASSERT(m_r_solver.inf_heap_is_correct()); TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.inf_heap_size() << ", int_infs = " << get_number_of_non_ints() << std::endl;); if (m_r_solver.current_x_is_feasible() && m_r_solver.m_look_for_feasible_solution_only) { m_r_solver.set_status(lp_status::OPTIMAL); @@ -93,14 +93,14 @@ void lar_core_solver::solve() { return; } ++m_r_solver.m_settings.stats().m_need_to_solve_inf; - lp_assert( r_basis_is_OK()); + SASSERT( r_basis_is_OK()); if (m_r_solver.m_look_for_feasible_solution_only) //todo : should it be set? m_r_solver.find_feasible_solution(); else m_r_solver.solve(); - lp_assert(r_basis_is_OK()); + SASSERT(r_basis_is_OK()); switch (m_r_solver.get_status()) { @@ -114,9 +114,9 @@ void lar_core_solver::solve() { m_r_solver.set_status(lp_status::OPTIMAL); break; } - lp_assert(r_basis_is_OK()); - lp_assert(m_r_solver.non_basic_columns_are_set_correctly()); - lp_assert(m_r_solver.inf_heap_is_correct()); + SASSERT(r_basis_is_OK()); + SASSERT(m_r_solver.non_basic_columns_are_set_correctly()); + SASSERT(m_r_solver.inf_heap_is_correct()); TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index df5cf9524..767b5b4a1 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -43,9 +43,9 @@ namespace lp { } bool lar_solver::sizes_are_correct() const { - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size()); - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); return true; } @@ -90,7 +90,7 @@ namespace lp { else if (kind == LE || kind == LT) n_of_L++; rs_of_evidence += coeff * constr.rhs(); } - lp_assert(n_of_G == 0 || n_of_L == 0); + SASSERT(n_of_G == 0 || n_of_L == 0); lconstraint_kind kind = n_of_G ? GE : (n_of_L ? LE : EQ); if (strict) kind = static_cast((static_cast(kind) / 2)); @@ -221,10 +221,10 @@ namespace lp { unsigned n = m_columns.size(); m_var_register.shrink(n); - lp_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); - lp_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count()); - lp_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct()); - lp_assert(A_r().column_count() == n); + SASSERT(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); + SASSERT(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count()); + SASSERT(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct()); + SASSERT(A_r().column_count() == n); TRACE("lar_solver_details", for (unsigned j = 0; j < n; j++) print_column_info(j, tout) << "\n";); m_mpq_lar_core_solver.pop(k); @@ -242,8 +242,8 @@ namespace lp { m_constraints.pop(k); m_simplex_strategy.pop(k); m_settings.simplex_strategy() = m_simplex_strategy; - lp_assert(sizes_are_correct()); - lp_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + SASSERT(sizes_are_correct()); + SASSERT(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); m_usage_in_terms.pop(k); m_dependencies.pop_scope(k); // init the nbasis sorting @@ -351,13 +351,13 @@ namespace lp { bool lar_solver::costs_are_zeros_for_r_solver() const { for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_solver.m_costs.size(); j++) { - lp_assert(is_zero(m_mpq_lar_core_solver.m_r_solver.m_costs[j])); + SASSERT(is_zero(m_mpq_lar_core_solver.m_r_solver.m_costs[j])); } return true; } bool lar_solver::reduced_costs_are_zeroes_for_r_solver() const { for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_solver.m_d.size(); j++) { - lp_assert(is_zero(m_mpq_lar_core_solver.m_r_solver.m_d[j])); + SASSERT(is_zero(m_mpq_lar_core_solver.m_r_solver.m_d[j])); } return true; } @@ -377,15 +377,15 @@ namespace lp { d[rc.var()] = zero_of_type(); } - lp_assert(reduced_costs_are_zeroes_for_r_solver()); - lp_assert(costs_are_zeros_for_r_solver()); + SASSERT(reduced_costs_are_zeroes_for_r_solver()); + SASSERT(costs_are_zeros_for_r_solver()); } void lar_solver::prepare_costs_for_r_solver(const lar_term& term) { TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";); auto& rslv = m_mpq_lar_core_solver.m_r_solver; - lp_assert(costs_are_zeros_for_r_solver()); - lp_assert(reduced_costs_are_zeroes_for_r_solver()); + SASSERT(costs_are_zeros_for_r_solver()); + SASSERT(reduced_costs_are_zeroes_for_r_solver()); move_non_basic_columns_to_bounds(); rslv.m_costs.resize(A_r().column_count(), zero_of_type()); for (lar_term::ival p : term) { @@ -398,7 +398,7 @@ namespace lp { } if (settings().backup_costs) rslv.m_costs_backup = rslv.m_costs; - lp_assert(rslv.reduced_costs_are_correct_tableau()); + SASSERT(rslv.reduced_costs_are_correct_tableau()); } void lar_solver::move_non_basic_columns_to_bounds() { @@ -457,7 +457,7 @@ namespace lp { } void lar_solver::set_value_for_nbasic_column(unsigned j, const impq& new_val) { - lp_assert(!is_base(j)); + SASSERT(!is_base(j)); auto& x = m_mpq_lar_core_solver.r_x(j); auto delta = new_val - x; x = new_val; @@ -493,7 +493,7 @@ namespace lp { // returns true iff the row of j has a non-fixed column different from j bool lar_solver::remove_from_basis(unsigned j) { - lp_assert(is_base(j)); + SASSERT(is_base(j)); unsigned i = row_of_basic_column(j); for (const auto & c : A_r().m_rows[i]) if (j != c.var() && !column_is_fixed(c.var())) @@ -783,14 +783,14 @@ namespace lp { continue; } - lp_assert(is_base(j) && column_is_fixed(j)); + SASSERT(is_base(j) && column_is_fixed(j)); auto const& r = basic2row(j); for (auto const& c : r) { unsigned j_entering = c.var(); if (!column_is_fixed(j_entering)) { pivot(j_entering, j); to_remove.push_back(j); - lp_assert(is_base(j_entering)); + SASSERT(is_base(j_entering)); break; } } @@ -798,7 +798,7 @@ namespace lp { for (unsigned j : to_remove) { m_fixed_base_var_set.remove(j); } - lp_assert(fixed_base_removed_correctly()); + SASSERT(fixed_base_removed_correctly()); } #ifdef Z3DEBUG bool lar_solver::fixed_base_removed_correctly() const { @@ -912,7 +912,7 @@ namespace lp { update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(); m_mpq_lar_core_solver.solve(); set_status(m_mpq_lar_core_solver.m_r_solver.get_status()); - lp_assert(((stats().m_make_feasible% 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); + SASSERT(((stats().m_make_feasible% 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); } @@ -1006,7 +1006,7 @@ namespace lp { bool lar_solver::the_left_sides_sum_to_zero(const vector>& evidence) const { std::unordered_map coeff_map; for (auto const & [coeff, con_ind] : evidence) { - lp_assert(m_constraints.valid_index(con_ind)); + SASSERT(m_constraints.valid_index(con_ind)); register_in_map(coeff_map, m_constraints[con_ind], coeff); } @@ -1024,18 +1024,18 @@ namespace lp { // disabled: kind is uninitialized #ifdef Z3DEBUG lconstraint_kind kind; - lp_assert(the_left_sides_sum_to_zero(explanation)); + SASSERT(the_left_sides_sum_to_zero(explanation)); mpq rs = sum_of_right_sides_of_explanation(explanation); switch (kind) { - case LE: lp_assert(rs < zero_of_type()); + case LE: SASSERT(rs < zero_of_type()); break; - case LT: lp_assert(rs <= zero_of_type()); + case LT: SASSERT(rs <= zero_of_type()); break; - case GE: lp_assert(rs > zero_of_type()); + case GE: SASSERT(rs > zero_of_type()); break; - case GT: lp_assert(rs >= zero_of_type()); + case GT: SASSERT(rs >= zero_of_type()); break; - case EQ: lp_assert(rs != zero_of_type()); + case EQ: SASSERT(rs != zero_of_type()); break; default: UNREACHABLE(); @@ -1060,7 +1060,7 @@ namespace lp { for (auto it : exp) { mpq coeff = it.coeff(); constraint_index con_ind = it.ci(); - lp_assert(m_constraints.valid_index(con_ind)); + SASSERT(m_constraints.valid_index(con_ind)); ret += (m_constraints[con_ind].rhs() - m_constraints[con_ind].get_free_coeff_of_left_side()) * coeff; } return ret; @@ -1142,7 +1142,7 @@ namespace lp { int inf_sign; auto inf_row = m_mpq_lar_core_solver.get_infeasibility_info(inf_sign); get_infeasibility_explanation_for_inf_sign(exp, inf_row, inf_sign); - lp_assert(explanation_is_correct(exp)); + SASSERT(explanation_is_correct(exp)); } void lar_solver::get_infeasibility_explanation_for_inf_sign( @@ -1161,7 +1161,7 @@ namespace lp { svector deps; m_dependencies.linearize(bound_constr_i, deps); for (auto d : deps) { - lp_assert(m_constraints.valid_index(d)); + SASSERT(m_constraints.valid_index(d)); exp.add_pair(d, coeff); } } @@ -1184,9 +1184,10 @@ namespace lp { bool lar_solver::init_model() const { auto& rslv = m_mpq_lar_core_solver.m_r_solver; - lp_assert(A_r().column_count() == rslv.m_costs.size()); - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); - lp_assert(A_r().column_count() == rslv.m_d.size()); + (void)rslv; + SASSERT(A_r().column_count() == rslv.m_costs.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); + SASSERT(A_r().column_count() == rslv.m_d.size()); CTRACE("lar_solver_model",!m_columns_with_changed_bounds.empty(), tout << "non-empty changed bounds\n"); TRACE("lar_solver_model", tout << get_status() << "\n"); auto status = get_status(); @@ -1331,7 +1332,7 @@ namespace lp { for (auto& it : cns.coeffs()) { lpvar j = it.second; auto vi = var_map.find(j); - lp_assert(vi != var_map.end()); + SASSERT(vi != var_map.end()); ret += it.first * vi->second; } return ret; @@ -1376,7 +1377,7 @@ namespace lp { void lar_solver::make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j) { // i, j - is the indices of the bottom-right element of the tableau - lp_assert(A_r().row_count() == i + 1 && A_r().column_count() == j + 1); + SASSERT(A_r().row_count() == i + 1 && A_r().column_count() == j + 1); auto& last_column = A_r().m_columns[j]; int non_zero_column_cell_index = -1; for (unsigned k = static_cast(last_column.size()); k-- > 0;) { @@ -1386,13 +1387,13 @@ namespace lp { non_zero_column_cell_index = k; } - lp_assert(non_zero_column_cell_index != -1); - lp_assert(static_cast(non_zero_column_cell_index) != i); + SASSERT(non_zero_column_cell_index != -1); + SASSERT(static_cast(non_zero_column_cell_index) != i); m_mpq_lar_core_solver.m_r_solver.transpose_rows_tableau(last_column[non_zero_column_cell_index].var(), i); } void lar_solver::remove_last_row_and_column_from_tableau(unsigned j) { - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); auto& slv = m_mpq_lar_core_solver.m_r_solver; unsigned i = A_r().row_count() - 1; //last row index make_sure_that_the_bottom_right_elem_not_zero_in_tableau(i, j); @@ -1410,8 +1411,8 @@ namespace lp { } A_r().remove_element(last_row, rc); } - lp_assert(last_row.size() == 0); - lp_assert(A_r().m_columns[j].size() == 0); + SASSERT(last_row.size() == 0); + SASSERT(A_r().m_columns[j].size() == 0); A_r().m_rows.pop_back(); A_r().m_columns.pop_back(); CASSERT("check_static_matrix", A_r().is_correct()); @@ -1419,7 +1420,7 @@ namespace lp { void lar_solver::remove_last_column_from_A() { // the last column has to be empty - lp_assert(A_r().m_columns.back().size() == 0); + SASSERT(A_r().m_columns.back().size() == 0); A_r().m_columns.pop_back(); } @@ -1428,7 +1429,7 @@ namespace lp { int i = rslv.m_basis_heading[j]; if (i >= 0) { // j is a basic var int last_pos = static_cast(rslv.m_basis.size()) - 1; - lp_assert(last_pos >= 0); + SASSERT(last_pos >= 0); if (i != last_pos) { unsigned j_at_last_pos = rslv.m_basis[last_pos]; rslv.m_basis[i] = j_at_last_pos; @@ -1438,7 +1439,7 @@ namespace lp { } else { int last_pos = static_cast(rslv.m_nbasis.size()) - 1; - lp_assert(last_pos >= 0); + SASSERT(last_pos >= 0); i = -1 - i; if (i != last_pos) { unsigned j_at_last_pos = rslv.m_nbasis[last_pos]; @@ -1448,14 +1449,14 @@ namespace lp { rslv.m_nbasis.pop_back(); // remove j from the basis } rslv.m_basis_heading.pop_back(); - lp_assert(rslv.m_basis.size() == A_r().row_count()); - lp_assert(rslv.basis_heading_is_correct()); + SASSERT(rslv.m_basis.size() == A_r().row_count()); + SASSERT(rslv.basis_heading_is_correct()); } void lar_solver::remove_last_column_from_tableau() { auto& rslv = m_mpq_lar_core_solver.m_r_solver; unsigned j = A_r().column_count() - 1; - lp_assert(A_r().column_count() == rslv.m_costs.size()); + SASSERT(A_r().column_count() == rslv.m_costs.size()); if (column_represents_row_in_tableau(j)) { remove_last_row_and_column_from_tableau(j); if (rslv.m_basis_heading[j] < 0) @@ -1469,10 +1470,10 @@ namespace lp { rslv.m_costs.pop_back(); remove_last_column_from_basis_tableau(j); - lp_assert(m_mpq_lar_core_solver.r_basis_is_OK()); - lp_assert(A_r().column_count() == rslv.m_costs.size()); - lp_assert(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); - lp_assert(A_r().column_count() == rslv.m_d.size()); + SASSERT(m_mpq_lar_core_solver.r_basis_is_OK()); + SASSERT(A_r().column_count() == rslv.m_costs.size()); + SASSERT(A_r().column_count() == m_mpq_lar_core_solver.r_x().size()); + SASSERT(A_r().column_count() == rslv.m_d.size()); } @@ -1496,14 +1497,14 @@ namespace lp { } for (unsigned j : became_feas) { - lp_assert(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0); + SASSERT(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0); m_mpq_lar_core_solver.m_r_solver.m_d[j] -= m_mpq_lar_core_solver.m_r_solver.m_costs[j]; m_mpq_lar_core_solver.m_r_solver.m_costs[j] = zero_of_type(); m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_heap(j); } became_feas.clear(); for (unsigned j : m_mpq_lar_core_solver.m_r_solver.inf_heap()) { - lp_assert(m_mpq_lar_core_solver.m_r_heading[j] >= 0); + SASSERT(m_mpq_lar_core_solver.m_r_heading[j] >= 0); if (column_is_feasible(j)) became_feas.push_back(j); } @@ -1586,14 +1587,14 @@ namespace lp { lpvar local_j; if (m_var_register.external_is_used(ext_j, local_j)) return local_j; - lp_assert(m_columns.size() == A_r().column_count()); + SASSERT(m_columns.size() == A_r().column_count()); local_j = A_r().column_count(); m_columns.push_back(column()); m_trail.push(undo_add_column(*this)); while (m_usage_in_terms.size() <= local_j) m_usage_in_terms.push_back(0); add_non_basic_var_to_core_fields(ext_j, is_int); - lp_assert(sizes_are_correct()); + SASSERT(sizes_are_correct()); return local_j; } @@ -1602,7 +1603,7 @@ namespace lp { } void lar_solver::register_new_external_var(unsigned ext_v, bool is_int) { - lp_assert(!m_var_register.external_is_used(ext_v)); + SASSERT(!m_var_register.external_is_used(ext_v)); m_var_register.add_var(ext_v, is_int); } @@ -1620,8 +1621,8 @@ namespace lp { unsigned j = A_r().column_count(); TRACE("add_var", tout << "j = " << j << std::endl;); A_r().add_column(); - lp_assert(m_mpq_lar_core_solver.r_x().size() == j); - // lp_assert(m_mpq_lar_core_solver.m_r_lower_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later + SASSERT(m_mpq_lar_core_solver.r_x().size() == j); + // SASSERT(m_mpq_lar_core_solver.m_r_lower_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later m_mpq_lar_core_solver.resize_x(j + 1); auto& rslv = m_mpq_lar_core_solver.m_r_solver; m_mpq_lar_core_solver.m_r_lower_bounds.increase_size_by_one(); @@ -1629,7 +1630,7 @@ namespace lp { rslv.inf_heap_increase_size_by_one(); rslv.m_costs.resize(j + 1); rslv.m_d.resize(j + 1); - lp_assert(m_mpq_lar_core_solver.m_r_heading.size() == j); // as A().column_count() on the entry to the method + SASSERT(m_mpq_lar_core_solver.m_r_heading.size() == j); // as A().column_count() on the entry to the method if (register_in_basis) { A_r().add_row(); m_mpq_lar_core_solver.m_r_heading.push_back(m_mpq_lar_core_solver.m_r_basis.size()); @@ -1704,7 +1705,7 @@ namespace lp { lpvar ret = A_r().column_count(); add_row_from_term_no_constraint(t, ext_i); - lp_assert(m_var_register.size() == A_r().column_count()); + SASSERT(m_var_register.size() == A_r().column_count()); if (m_need_register_terms) register_normalized_term(*t, A_r().column_count() - 1); if (m_add_term_callback) @@ -1850,13 +1851,13 @@ namespace lp { constraint_index ci; if (!column_has_term(j)) { mpq rs = adjust_bound_for_int(j, kind, right_side); - lp_assert(bound_is_integer_for_integer_column(j, rs)); + SASSERT(bound_is_integer_for_integer_column(j, rs)); ci = m_constraints.add_var_constraint(j, kind, rs); } else { ci = add_var_bound_on_constraint_for_term(j, kind, right_side); } - lp_assert(sizes_are_correct()); + SASSERT(sizes_are_correct()); return ci; } @@ -2061,8 +2062,8 @@ namespace lp { } void lar_solver::update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { - lp_assert(column_has_lower_bound(j) && column_has_upper_bound(j)); - lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed || + SASSERT(column_has_lower_bound(j) && column_has_upper_bound(j)); + SASSERT(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed || m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed); mpq y_of_bound(0); @@ -2129,8 +2130,8 @@ namespace lp { } void lar_solver::update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { - lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j)); - lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound); + SASSERT(column_has_lower_bound(j) && !column_has_upper_bound(j)); + SASSERT(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound); mpq y_of_bound(0); switch (kind) { @@ -2183,8 +2184,8 @@ namespace lp { } void lar_solver::update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { - lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j)); - lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound); + SASSERT(!column_has_lower_bound(j) && column_has_upper_bound(j)); + SASSERT(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound); mpq y_of_bound(0); switch (kind) { case LT: @@ -2238,7 +2239,7 @@ namespace lp { } void lar_solver::update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { - lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j)); + SASSERT(!column_has_lower_bound(j) && !column_has_upper_bound(j)); mpq y_of_bound(0); switch (kind) { @@ -2388,7 +2389,7 @@ namespace lp { } bool lar_solver::get_equality_and_right_side_for_term_on_current_x(lpvar j, mpq& rs, u_dependency*& ci, bool& upper_bound) const { - lp_assert(column_has_term(j)); + SASSERT(column_has_term(j)); if (!column_is_int(j)) // todo - allow for the next version of hnf return false; bool rs_is_calculated = false; @@ -2396,7 +2397,7 @@ namespace lp { bool is_strict; const lar_term& term = get_term(j); if (has_upper_bound(j, ci, b, is_strict) && !is_strict) { - lp_assert(b.is_int()); + SASSERT(b.is_int()); if (!sum_first_coords(term, rs)) return false; rs_is_calculated = true; @@ -2410,7 +2411,7 @@ namespace lp { if (!sum_first_coords(term, rs)) return false; } - lp_assert(b.is_int()); + SASSERT(b.is_int()); if (rs == b) { upper_bound = false; @@ -2471,7 +2472,7 @@ namespace lp { // a_j.second givis the column bool lar_solver::fetch_normalized_term_column(const lar_term& c, std::pair& a_j) const { TRACE("lar_solver_terms", print_term_as_indices(c, tout << "looking for term ") << "\n";); - lp_assert(c.is_normalized()); + SASSERT(c.is_normalized()); auto it = m_normalized_terms_to_columns.find(c); if (it != m_normalized_terms_to_columns.end()) { TRACE("lar_solver_terms", tout << "got " << it->second << "\n";); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 575184b4f..889476331 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -335,7 +335,7 @@ public: int sign = j_sign * a_sign; const column& ul = m_columns[j]; auto* witness = sign > 0 ? ul.upper_bound_witness() : ul.lower_bound_witness(); - lp_assert(witness); + SASSERT(witness); for (auto ci : flatten(witness)) bp.consume(a, ci); } @@ -453,7 +453,7 @@ public: void set_value_for_nbasic_column_report(unsigned j, const impq& new_val, const ChangeReport& after) { - lp_assert(!is_base(j)); + SASSERT(!is_base(j)); auto& x = m_mpq_lar_core_solver.r_x(j); auto delta = new_val - x; x = new_val; diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 9da65db04..bfd728fc7 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -81,11 +81,11 @@ private: if (v1 == v2) return; #if Z3DEBUG - lp_assert(val(v1) == val(v2)); + SASSERT(val(v1) == val(v2)); unsigned debv1, debv2; - lp_assert(only_one_nfixed(r1, debv1) && only_one_nfixed(r2, debv2)); - lp_assert(debv1 == v1 && debv2 == v2); - lp_assert(ival(v1).y == ival(v2).y); + SASSERT(only_one_nfixed(r1, debv1) && only_one_nfixed(r2, debv2)); + SASSERT(debv1 == v1 && debv2 == v2); + SASSERT(ival(v1).y == ival(v2).y); #endif explanation ex; explain_fixed_in_row(r1, ex); @@ -214,8 +214,8 @@ public: } bool add_eq_on_columns(const explanation& exp, lpvar je, lpvar ke, bool is_fixed) { - lp_assert(je != ke && is_int(je) == is_int(ke)); - lp_assert(ival(je) == ival(ke)); + SASSERT(je != ke && is_int(je) == is_int(ke)); + SASSERT(ival(je) == ival(ke)); TRACE("eq", tout << "reported idx " << je << ", " << ke << "\n"; @@ -315,7 +315,7 @@ public: continue; if (++nf > 2) return nf; - lp_assert(is_not_set(y)); + SASSERT(is_not_set(y)); y = j; if (c.coeff().is_one()) { y_sign = 1; @@ -332,8 +332,8 @@ public: } void try_add_equation_with_lp_fixed_tables(unsigned row_index, unsigned v_j) { - lp_assert(lp().get_base_column_in_row(row_index) == v_j); - lp_assert(num_of_non_fixed_in_row(row_index) == 1 || column_is_fixed(v_j)); + SASSERT(lp().get_base_column_in_row(row_index) == v_j); + SASSERT(num_of_non_fixed_in_row(row_index) == 1 || column_is_fixed(v_j)); if (column_is_fixed(v_j)) { return; } @@ -366,7 +366,7 @@ public: if (nf == 0 || nf > 2) return; if (nf == 1) { - lp_assert(is_not_set(y)); + SASSERT(is_not_set(y)); try_add_equation_with_lp_fixed_tables(row_index, x); return; } @@ -374,8 +374,8 @@ public: // the coefficient before y is not 1 or -1 return; } - lp_assert(y_sign == -1 || y_sign == 1); - lp_assert(lp().is_base(y) == false); + SASSERT(y_sign == -1 || y_sign == 1); + SASSERT(lp().is_base(y) == false); auto& table = y_sign == 1 ? m_row2index_pos : m_row2index_neg; table.insert(val(x), row_index); TRACE("eq", tout << "y = " << y << "\n";); @@ -391,8 +391,8 @@ public: if (nf != 2 || y_sign == 0) continue; - lp_assert(y_nb == y); - lp_assert(y_sign == 1 || y_sign == -1); + SASSERT(y_nb == y); + SASSERT(y_sign == 1 || y_sign == -1); auto& table = y_sign == 1 ? m_row2index_pos : m_row2index_neg; const auto& v = val(x); unsigned found_i;; diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 67f7ffb6c..1656545ea 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -38,7 +38,7 @@ struct lpvar_lt { typedef heap lpvar_heap; template X dot_product(const vector & a, const vector & b) { - lp_assert(a.size() == b.size()); + SASSERT(a.size() == b.size()); auto r = zero_of_type(); for (unsigned i = 0; i < a.size(); i++) { r += a[i] * b[i]; @@ -180,7 +180,7 @@ public: unsigned m = m_A.row_count(); for (unsigned i = 0; i < m; i++) { unsigned bj = m_basis[i]; - lp_assert(m_A.m_columns[bj].size() > 0); + SASSERT(m_A.m_columns[bj].size() > 0); if (m_A.m_columns[bj].size() > 1) return true; for (const auto & c : m_A.m_columns[bj]) { @@ -293,11 +293,11 @@ public: bool make_column_feasible(unsigned j, numeric_pair & delta) { bool ret = false; - lp_assert(m_basis_heading[j] < 0); + SASSERT(m_basis_heading[j] < 0); const auto & x = m_x[j]; switch (m_column_types[j]) { case column_type::fixed: - lp_assert(m_lower_bounds[j] == m_upper_bounds[j]); + SASSERT(m_lower_bounds[j] == m_upper_bounds[j]); if (x != m_lower_bounds[j]) { delta = m_lower_bounds[j] - x; ret = true; @@ -365,7 +365,7 @@ public: void change_basis_unconditionally(unsigned entering, unsigned leaving) { TRACE("lar_solver", tout << "entering = " << entering << ", leaving = " << leaving << "\n";); - lp_assert(m_basis_heading[entering] < 0); + SASSERT(m_basis_heading[entering] < 0); int place_in_non_basis = -1 - m_basis_heading[entering]; if (static_cast(place_in_non_basis) >= m_nbasis.size()) { // entering variable in not in m_nbasis, we need to put it back; @@ -385,8 +385,8 @@ public: void change_basis(unsigned entering, unsigned leaving) { TRACE("lar_solver", tout << "entering = " << entering << ", leaving = " << leaving << "\n";); - lp_assert(m_basis_heading[entering] < 0); - lp_assert(m_basis_heading[leaving] >= 0); + SASSERT(m_basis_heading[entering] < 0); + SASSERT(m_basis_heading[leaving] >= 0); int place_in_basis = m_basis_heading[leaving]; int place_in_non_basis = - m_basis_heading[entering] - 1; @@ -573,14 +573,14 @@ public: m_inf_heap.insert(j); TRACE("lar_solver_inf_heap", tout << "insert into inf_heap j = " << j << "\n";); } - lp_assert(!column_is_feasible(j)); + SASSERT(!column_is_feasible(j)); } void remove_column_from_inf_heap(unsigned j) { if (m_inf_heap.contains(j)) { TRACE("lar_solver_inf_heap", tout << "erase from heap j = " << j << "\n";); m_inf_heap.erase(j); } - lp_assert(column_is_feasible(j)); + SASSERT(column_is_feasible(j)); } void clear_inf_heap() { @@ -589,10 +589,10 @@ public: } bool costs_on_nbasis_are_zeros() const { - lp_assert(this->basis_heading_is_correct()); + SASSERT(this->basis_heading_is_correct()); for (unsigned j = 0; j < this->m_n(); j++) { if (this->m_basis_heading[j] < 0) - lp_assert(is_zero(this->m_costs[j])); + SASSERT(is_zero(this->m_costs[j])); } return true; } diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index 4c0e8fc3e..82afd7a27 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -60,7 +60,7 @@ lp_core_solver_base(static_matrix & A, m_tracing_basis_changes(false), m_touched_rows(nullptr), m_look_for_feasible_solution_only(false) { - lp_assert(bounds_for_boxed_are_set_correctly()); + SASSERT(bounds_for_boxed_are_set_correctly()); init(); init_basis_heading_and_non_basic_columns_vector(); } @@ -68,7 +68,7 @@ lp_core_solver_base(static_matrix & A, template void lp_core_solver_base:: allocate_basis_heading() { // the rest of initialization will be handled by the factorization class init_basis_heading_and_non_basic_columns_vector(); - lp_assert(basis_heading_is_correct()); + SASSERT(basis_heading_is_correct()); } template void lp_core_solver_base:: init() { @@ -267,7 +267,7 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) { return false; if (pivot_col_cell_index != 0) { - lp_assert(column.size() > 1); + SASSERT(column.size() > 1); // swap the pivot column cell with the head cell auto c = column[0]; column[0] = column[pivot_col_cell_index]; @@ -278,7 +278,7 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) { } while (column.size() > 1) { auto & c = column.back(); - lp_assert(c.var() != piv_row_index); + SASSERT(c.var() != piv_row_index); if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) { return false; } @@ -324,7 +324,7 @@ non_basis_is_correctly_represented_in_heading(std::list* non_basis_lis for (unsigned j = 0; j < m_A.column_count(); j++) if (m_basis_heading[j] >= 0) - lp_assert(static_cast(m_basis_heading[j]) < m_A.row_count() && m_basis[m_basis_heading[j]] == j); + SASSERT(static_cast(m_basis_heading[j]) < m_A.row_count() && m_basis[m_basis_heading[j]] == j); if (non_basis_list == nullptr) return true; @@ -361,9 +361,9 @@ template bool lp_core_solver_base:: if ( m_A.column_count() > 10 ) // for the performance reason return true; - lp_assert(m_basis_heading.size() == m_A.column_count()); - lp_assert(m_basis.size() == m_A.row_count()); - lp_assert(m_nbasis.size() <= m_A.column_count() - m_A.row_count()); // for the dual the size of non basis can be smaller + SASSERT(m_basis_heading.size() == m_A.column_count()); + SASSERT(m_basis.size() == m_A.row_count()); + SASSERT(m_nbasis.size() <= m_A.column_count() - m_A.row_count()); // for the dual the size of non basis can be smaller if (!basis_has_no_doubles()) return false; @@ -391,8 +391,8 @@ template void lp_core_solver_base::transpose_row } // entering is the new base column, leaving - the column leaving the basis template bool lp_core_solver_base::pivot_column_general(unsigned entering, unsigned leaving, indexed_vector & w) { - lp_assert(m_basis_heading[entering] < 0); - lp_assert(m_basis_heading[leaving] >= 0); + SASSERT(m_basis_heading[entering] < 0); + SASSERT(m_basis_heading[leaving] >= 0); unsigned row_index = m_basis_heading[leaving]; // the tableau case if (!pivot_column_tableau(entering, row_index)) diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg new file mode 100644 index 000000000..328a0be09 --- /dev/null +++ b/src/math/lp/lp_params_helper.pyg @@ -0,0 +1,13 @@ +def_module_params(module_name='lp', + class_name='lp_params_helper', + description='linear programming parameters', + export=True, + params=(('dio', BOOL, True, 'use Diophantine equalities'), + ('dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'), + ('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'), + ('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'), + ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'), + ('dio_calls_period', UINT, 4, 'Period of calling the Diophantine handler in the final_check()'), + ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'), + )) + diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h index 0aa96a6f9..f925f74f3 100644 --- a/src/math/lp/lp_primal_core_solver.h +++ b/src/math/lp/lp_primal_core_solver.h @@ -56,7 +56,7 @@ namespace lp { int choose_entering_column_tableau(); bool needs_to_grow(unsigned bj) const { - lp_assert(!this->column_is_feasible(bj)); + SASSERT(!this->column_is_feasible(bj)); switch (this->m_column_types[bj]) { case column_type::free_column: return false; @@ -72,7 +72,7 @@ namespace lp { } int inf_sign_of_column(unsigned bj) const { - lp_assert(!this->column_is_feasible(bj)); + SASSERT(!this->column_is_feasible(bj)); switch (this->m_column_types[bj]) { case column_type::free_column: return 0; @@ -90,7 +90,7 @@ namespace lp { bool monoid_can_decrease(const row_cell &rc) const { unsigned j = rc.var(); - lp_assert(this->column_is_feasible(j)); + SASSERT(this->column_is_feasible(j)); switch (this->m_column_types[j]) { case column_type::free_column: return true; @@ -113,7 +113,7 @@ namespace lp { bool monoid_can_increase(const row_cell &rc) const { unsigned j = rc.var(); - lp_assert(this->column_is_feasible(j)); + SASSERT(this->column_is_feasible(j)); switch (this->m_column_types[j]) { case column_type::free_column: return true; @@ -247,25 +247,25 @@ namespace lp { void limit_theta_on_basis_column_for_inf_case_m_neg_upper_bound( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m < 0 && this->m_column_types[j] == column_type::upper_bound); + SASSERT(m < 0 && this->m_column_types[j] == column_type::upper_bound); limit_inf_on_upper_bound_m_neg(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited); } void limit_theta_on_basis_column_for_inf_case_m_neg_lower_bound( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m < 0 && this->m_column_types[j] == column_type::lower_bound); + SASSERT(m < 0 && this->m_column_types[j] == column_type::lower_bound); limit_inf_on_bound_m_neg(m, this->m_x[j], this->m_lower_bounds[j], theta, unlimited); } void limit_theta_on_basis_column_for_inf_case_m_pos_lower_bound( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m > 0 && this->m_column_types[j] == column_type::lower_bound); + SASSERT(m > 0 && this->m_column_types[j] == column_type::lower_bound); limit_inf_on_lower_bound_m_pos(m, this->m_x[j], this->m_lower_bounds[j], theta, unlimited); } void limit_theta_on_basis_column_for_inf_case_m_pos_upper_bound( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m > 0 && this->m_column_types[j] == column_type::upper_bound); + SASSERT(m > 0 && this->m_column_types[j] == column_type::upper_bound); limit_inf_on_bound_m_pos(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited); }; @@ -294,7 +294,7 @@ namespace lp { if (this->m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows) return false; - // lp_assert(calc_current_x_is_feasible() == + // SASSERT(calc_current_x_is_feasible() == // current_x_is_feasible()); return this->current_x_is_feasible() == this->using_infeas_costs(); } @@ -326,7 +326,7 @@ namespace lp { } void update_basis_and_x_tableau_rows(int entering, int leaving, X const &tt) { - lp_assert(entering != leaving); + SASSERT(entering != leaving); update_x_tableau_rows(entering, leaving, tt); this->pivot_column_tableau(entering, this->m_basis_heading[leaving]); this->change_basis(entering, leaving); @@ -346,7 +346,7 @@ namespace lp { } const X &get_val_for_leaving(unsigned j) const { - lp_assert(!this->column_is_feasible(j)); + SASSERT(!this->column_is_feasible(j)); switch (this->m_column_types[j]) { case column_type::fixed: case column_type::upper_bound: @@ -411,7 +411,7 @@ namespace lp { void limit_theta_on_basis_column_for_feas_case_m_neg_no_check( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m < 0); + SASSERT(m < 0); limit_theta((this->m_lower_bounds[j] - this->m_x[j]) / m, theta, unlimited); if (theta < zero_of_type()) theta = zero_of_type(); @@ -420,7 +420,7 @@ namespace lp { bool limit_inf_on_bound_m_neg(const T &m, const X &x, const X &bound, X &theta, bool &unlimited) { // x gets smaller - lp_assert(m < 0); + SASSERT(m < 0); if (this->below_bound(x, bound)) return false; if (this->above_bound(x, bound)) { @@ -435,7 +435,7 @@ namespace lp { bool limit_inf_on_bound_m_pos(const T &m, const X &x, const X &bound, X &theta, bool &unlimited) { // x gets larger - lp_assert(m > 0); + SASSERT(m > 0); if (this->above_bound(x, bound)) return false; if (this->below_bound(x, bound)) { @@ -451,7 +451,7 @@ namespace lp { void limit_inf_on_lower_bound_m_pos(const T &m, const X &x, const X &bound, X &theta, bool &unlimited) { // x gets larger - lp_assert(m > 0); + SASSERT(m > 0); if (this->below_bound(x, bound)) { limit_theta((bound - x) / m, theta, unlimited); } @@ -460,7 +460,7 @@ namespace lp { void limit_inf_on_upper_bound_m_neg(const T &m, const X &x, const X &bound, X &theta, bool &unlimited) { // x gets smaller - lp_assert(m < 0); + SASSERT(m < 0); if (this->above_bound(x, bound)) { limit_theta((bound - x) / m, theta, unlimited); } @@ -490,7 +490,7 @@ namespace lp { const T &m, X &theta, bool &unlimited) { - // lp_assert(m < 0 && this->m_column_type[j] == column_type::boxed); + // SASSERT(m < 0 && this->m_column_type[j] == column_type::boxed); const X &x = this->m_x[j]; const X &ubound = this->m_upper_bounds[j]; if (this->above_bound(x, ubound)) { @@ -508,7 +508,7 @@ namespace lp { void limit_theta_on_basis_column_for_feas_case_m_pos_no_check( unsigned j, const T &m, X &theta, bool &unlimited) { - lp_assert(m > 0); + SASSERT(m > 0); limit_theta((this->m_upper_bounds[j] - this->m_x[j]) / m, theta, unlimited); if (theta < zero_of_type()) { theta = zero_of_type(); @@ -617,7 +617,7 @@ namespace lp { // the delta is between the old and the new cost (old - new) void update_reduced_cost_for_basic_column_cost_change(const T &delta, unsigned j) { - lp_assert(this->m_basis_heading[j] >= 0); + SASSERT(this->m_basis_heading[j] >= 0); unsigned i = static_cast(this->m_basis_heading[j]); for (const row_cell &rc : this->m_A.m_rows[i]) { unsigned k = rc.var(); diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h index f14d268a3..74bbad1fc 100644 --- a/src/math/lp/lp_primal_core_solver_def.h +++ b/src/math/lp/lp_primal_core_solver_def.h @@ -179,7 +179,7 @@ lp_primal_core_solver::get_bound_on_variable_and_update_leaving_precisely( template void lp_primal_core_solver::check_Ax_equal_b() { dense_matrix d(this->m_A); T * ls = d.apply_from_left_with_different_dims(this->m_x); - lp_assert(vectors_are_equal(ls, this->m_b, this->m_m())); + SASSERT(vectors_are_equal(ls, this->m_b, this->m_m())); delete [] ls; } template void lp_primal_core_solver::check_the_bounds() { @@ -189,8 +189,8 @@ template void lp_primal_core_solver::check_the } template void lp_primal_core_solver::check_bound(unsigned i) { - lp_assert (!(this->column_has_lower_bound(i) && (numeric_traits::zero() > this->m_x[i]))); - lp_assert (!(this->column_has_upper_bound(i) && (this->m_upper_bounds[i] < this->m_x[i]))); + SASSERT (!(this->column_has_lower_bound(i) && (numeric_traits::zero() > this->m_x[i]))); + SASSERT (!(this->column_has_upper_bound(i) && (this->m_upper_bounds[i] < this->m_x[i]))); } template void lp_primal_core_solver::check_correctness() { @@ -231,7 +231,7 @@ template unsigned lp_primal_core_solver::get_num // calling it stage1 is too cryptic template void lp_primal_core_solver::find_feasible_solution() { this->m_look_for_feasible_solution_only = true; - lp_assert(this->non_basic_columns_are_set_correctly()); + SASSERT(this->non_basic_columns_are_set_correctly()); this->set_status(lp_status::UNKNOWN); solve(); } diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h index 76012cdbf..1a1bf0553 100644 --- a/src/math/lp/lp_primal_core_solver_tableau_def.h +++ b/src/math/lp/lp_primal_core_solver_tableau_def.h @@ -30,7 +30,7 @@ template void lp_primal_core_solver::one_iteratio else { advance_on_entering_tableau(entering); } - lp_assert(this->inf_heap_is_correct()); + SASSERT(this->inf_heap_is_correct()); } template void lp_primal_core_solver::advance_on_entering_tableau(int entering) { @@ -116,7 +116,7 @@ unsigned lp_primal_core_solver::solve() { UNREACHABLE(); break; case lp_status::UNBOUNDED: - lp_assert (this->current_x_is_feasible()); + SASSERT (this->current_x_is_feasible()); break; case lp_status::UNSTABLE: @@ -143,7 +143,7 @@ unsigned lp_primal_core_solver::solve() { !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) ); - lp_assert( + SASSERT( this->get_status() == lp_status::CANCELLED || this->current_x_is_feasible() == false @@ -153,12 +153,12 @@ unsigned lp_primal_core_solver::solve() { } template void lp_primal_core_solver::advance_on_entering_and_leaving_tableau(int entering, int leaving, X & t) { - lp_assert(leaving >= 0 && entering >= 0); - lp_assert((this->m_settings.simplex_strategy() == + SASSERT(leaving >= 0 && entering >= 0); + SASSERT((this->m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows) || m_non_basis_list.back() == static_cast(entering)); - lp_assert(!is_neg(t)); - lp_assert(entering != leaving || !is_zero(t)); // otherwise nothing changes + SASSERT(!is_neg(t)); + SASSERT(entering != leaving || !is_zero(t)); // otherwise nothing changes if (entering == leaving) { advance_on_entering_equal_leaving_tableau(entering, t); return; @@ -206,7 +206,7 @@ template int lp_primal_core_solver::find_leaving_ const column_cell & c = col[k]; unsigned i = c.var(); const T & ed = this->m_A.get_val(c); - lp_assert(!numeric_traits::is_zero(ed)); + SASSERT(!numeric_traits::is_zero(ed)); unsigned j = this->m_basis[i]; limit_theta_on_basis_column(j, - ed * m_sign_of_entering_delta, t, unlimited); if (!unlimited) { @@ -225,7 +225,7 @@ template int lp_primal_core_solver::find_leaving_ const column_cell & c = col[k]; unsigned i = c.var(); const T & ed = this->m_A.get_val(c); - lp_assert(!numeric_traits::is_zero(ed)); + SASSERT(!numeric_traits::is_zero(ed)); unsigned j = this->m_basis[i]; unlimited = true; limit_theta_on_basis_column(j, -ed * m_sign_of_entering_delta, ratio, unlimited); @@ -254,9 +254,9 @@ template int lp_primal_core_solver::find_leaving_ return m_leaving_candidates[k]; } template void lp_primal_core_solver::init_run_tableau() { - lp_assert(basis_columns_are_set_correctly()); + SASSERT(basis_columns_are_set_correctly()); this->iters_with_no_cost_growing() = 0; - lp_assert(this->inf_heap_is_correct()); + SASSERT(this->inf_heap_is_correct()); if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) return; if (this->m_settings.backup_costs) @@ -264,13 +264,13 @@ template void lp_primal_core_solver::init_run_tab if (this->m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows) init_tableau_rows(); - lp_assert(this->reduced_costs_are_correct_tableau()); - lp_assert(!this->need_to_pivot_to_basis_tableau()); + SASSERT(this->reduced_costs_are_correct_tableau()); + SASSERT(!this->need_to_pivot_to_basis_tableau()); } template bool lp_primal_core_solver:: update_basis_and_x_tableau(int entering, int leaving, X const & tt) { - lp_assert(entering != leaving); + SASSERT(entering != leaving); update_x_tableau(entering, tt); this->pivot_column_tableau(entering, this->m_basis_heading[leaving]); this->change_basis(entering, leaving); diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 9d2fe675e..ea662f111 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -17,6 +17,7 @@ Revision History: --*/ +#include "math/lp/lp_params_helper.hpp" #include #include "util/vector.h" #include "smt/params/smt_params_helper.hpp" @@ -25,6 +26,7 @@ template bool lp::vectors_are_equal(vector const&, vector(p.arith_simplex_strategy()); m_nlsat_delay = p.arith_nl_delay(); - m_dio_eqs = p.arith_lp_dio_eqs(); - m_dio_enable_gomory_cuts = p.arith_lp_dio_cuts_enable_gomory(); - m_dio_enable_hnf_cuts = p.arith_lp_dio_cuts_enable_hnf(); - m_dio_branching_period = p.arith_lp_dio_branching_period(); + m_dio = lp_p.dio(); + m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory(); + m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf(); + m_dio_branching_period = lp_p.dio_branching_period(); m_dump_bound_lemmas = p.arith_dump_bound_lemmas(); + m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); + m_dio_calls_period = lp_p.dio_calls_period(); + m_dio_run_gcd = lp_p.dio_run_gcd(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 8efff27bd..82af740d0 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -218,8 +218,12 @@ public: void updt_params(params_ref const& p); bool enable_hnf() const { return m_enable_hnf; } unsigned nlsat_delay() const { return m_nlsat_delay; } - bool int_run_gcd_test() const { return m_int_run_gcd_test; } - bool& int_run_gcd_test() { return m_int_run_gcd_test; } + bool int_run_gcd_test() const { + if (!m_dio) + return m_int_run_gcd_test; + return m_dio_run_gcd; + } + void set_run_gcd_test(bool v) { m_int_run_gcd_test = v; } unsigned reps_in_scaler = 20; int c_partial_pivoting = 10; // this is the constant c from page 410 unsigned depth_of_rook_search = 4; @@ -243,7 +247,6 @@ public: unsigned column_number_threshold_for_using_lu_in_lar_solver = 4000; unsigned m_int_gomory_cut_period = 4; unsigned m_int_find_cube_period = 4; - unsigned m_dioph_eq_period = 1; private: unsigned m_hnf_cut_period = 4; bool m_int_run_gcd_test = true; @@ -255,23 +258,30 @@ private: bool m_enable_hnf = true; bool m_print_external_var_name = false; bool m_propagate_eqs = false; - bool m_dio_eqs = false; + bool m_dio = false; bool m_dio_enable_gomory_cuts = false; bool m_dio_enable_hnf_cuts = true; unsigned m_dio_branching_period = 100; // do branching rarely unsigned m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening bool m_dump_bound_lemmas = false; + bool m_dio_ignore_big_nums = false; + unsigned m_dio_calls_period = 4; + bool m_dio_run_gcd = true; public: + unsigned dio_calls_period() const { return m_dio_calls_period; } + unsigned & dio_calls_period() { return m_dio_calls_period; } bool print_external_var_name() const { return m_print_external_var_name; } bool propagate_eqs() const { return m_propagate_eqs;} unsigned hnf_cut_period() const { return m_hnf_cut_period; } void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period; } unsigned random_next() { return m_rand(); } unsigned random_next(unsigned u ) { return m_rand(u); } - bool dio_eqs() { return m_dio_eqs; } - bool dio_enable_gomory_cuts() const { return m_dio_eqs && m_dio_enable_gomory_cuts; } - bool dio_enable_hnf_cuts() const { return m_dio_eqs && m_dio_enable_hnf_cuts; } + bool dio() { return m_dio; } + bool dio_enable_gomory_cuts() const { return m_dio && m_dio_enable_gomory_cuts; } + bool dio_run_gcd() const { return m_dio && m_dio_run_gcd; } + bool dio_enable_hnf_cuts() const { return m_dio && m_dio_enable_hnf_cuts; } unsigned dio_branching_period() const { return m_dio_branching_period; } + bool dio_ignore_big_nums() const { return m_dio_ignore_big_nums; } void set_random_seed(unsigned s) { m_rand.set_seed(s); } unsigned dio_report_branch_with_term_tigthening_period() const { return m_dio_report_branch_with_term_tigthening_period; } bool bound_progation() const { @@ -376,7 +386,7 @@ inline void print_blanks(int n, std::ostream & out) { // after a push of the last element we ensure that the vector increases // we also suppose that before the last push the vector was increasing inline void ensure_increasing(vector & v) { - lp_assert(v.size() > 0); + SASSERT(v.size() > 0); unsigned j = v.size() - 1; for (; j > 0; j-- ) if (v[j] <= v[j - 1]) { @@ -392,7 +402,7 @@ inline void ensure_increasing(vector & v) { inline static bool is_rational(const impq & n) { return is_zero(n.y); } inline static mpq fractional_part(const impq & n) { - lp_assert(is_rational(n)); + SASSERT(is_rational(n)); return n.x - floor(n.x); } inline static mpq fractional_part(const mpq & n) { diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h index d78ef080f..7e166f99e 100644 --- a/src/math/lp/lp_utils.h +++ b/src/math/lp/lp_utils.h @@ -151,7 +151,6 @@ inline void throw_exception(std::string && str) { } typedef z3_exception exception; -#define lp_assert(_x_) { SASSERT(_x_); } template inline X zero_of_type() { return numeric_traits::zero(); } template inline X one_of_type() { return numeric_traits::one(); } template inline bool is_zero(const X & v) { return numeric_traits::is_zero(v); } diff --git a/src/math/lp/permutation_matrix.h b/src/math/lp/permutation_matrix.h index df0897dbe..98d69ad1a 100644 --- a/src/math/lp/permutation_matrix.h +++ b/src/math/lp/permutation_matrix.h @@ -69,7 +69,7 @@ class permutation_matrix unsigned operator[](unsigned i) const { return m_permutation[i]; } void set_val(unsigned i, unsigned pi) { - lp_assert(i < size() && pi < size()); m_permutation[i] = pi; m_rev[pi] = i; } + SASSERT(i < size() && pi < size()); m_permutation[i] = pi; m_rev[pi] = i; } void transpose_from_left(unsigned i, unsigned j); diff --git a/src/math/lp/permutation_matrix_def.h b/src/math/lp/permutation_matrix_def.h index c86fef4f4..5ab2651ac 100644 --- a/src/math/lp/permutation_matrix_def.h +++ b/src/math/lp/permutation_matrix_def.h @@ -60,7 +60,7 @@ template void permutation_matrix::print(std::ostr template void permutation_matrix::transpose_from_left(unsigned i, unsigned j) { // the result will be this = (i,j)*this - lp_assert(i < size() && j < size() && i != j); + SASSERT(i < size() && j < size() && i != j); auto pi = m_rev[i]; auto pj = m_rev[j]; set_val(pi, j); @@ -69,7 +69,7 @@ template void permutation_matrix::transpose_from_ template void permutation_matrix::transpose_from_right(unsigned i, unsigned j) { // the result will be this = this * (i,j) - lp_assert(i < size() && j < size() && i != j); + SASSERT(i < size() && j < size() && i != j); auto pi = m_permutation[i]; auto pj = m_permutation[j]; set_val(i, pj); diff --git a/src/math/lp/stacked_vector.h b/src/math/lp/stacked_vector.h index 4c32de2d7..b1b956c76 100644 --- a/src/math/lp/stacked_vector.h +++ b/src/math/lp/stacked_vector.h @@ -38,7 +38,7 @@ public: unsigned m_i; public: ref(stacked_vector &m, unsigned key): m_vec(m), m_i(key) { - lp_assert(key < m.size()); + SASSERT(key < m.size()); } ref & operator=(const B & b) { m_vec.emplace_replace(m_i, b); @@ -81,7 +81,7 @@ public: unsigned m_i; public: ref_const(const stacked_vector &m, unsigned key) :m_vec(m), m_i(key) { - lp_assert(key < m.size()); + SASSERT(key < m.size()); } operator const B&() const { return m_vec.m_vector[m_i]; @@ -120,7 +120,7 @@ public: /* const B & operator[](unsigned a) const { - lp_assert(a < m_vector.size()); + SASSERT(a < m_vector.size()); return m_vector[a]; } */ @@ -139,7 +139,7 @@ public: template void pop_tail(svector & v, unsigned k) { - lp_assert(v.size() >= k); + SASSERT(v.size() >= k); v.resize(v.size() - k); } @@ -149,8 +149,8 @@ public: } void pop(unsigned k) { - lp_assert(m_stack_of_vector_sizes.size() >= k); - lp_assert(k > 0); + SASSERT(m_stack_of_vector_sizes.size() >= k); + SASSERT(k > 0); m_vector.resize(m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]); m_last_update.resize(m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]); pop_tail(m_stack_of_vector_sizes, k); @@ -179,7 +179,7 @@ public: } unsigned peek_size(unsigned k) const { - lp_assert(k > 0 && k <= m_stack_of_vector_sizes.size()); + SASSERT(k > 0 && k <= m_stack_of_vector_sizes.size()); return m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]; } diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 88046aeff..ee42c793b 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -236,7 +236,7 @@ public: for (auto & c : row) { unsigned j = c.var(); auto & col = m_columns[j]; - lp_assert(col[col.size() - 1].var() == m_rows.size() -1 ); // todo : start here!!!! + SASSERT(col[col.size() - 1].var() == m_rows.size() -1 ); // todo : start here!!!! col.pop_back(); } } @@ -263,7 +263,7 @@ public: m_columns.pop_back(); // delete the last column m_stack.pop(); } - lp_assert(is_correct()); + SASSERT(is_correct()); } void multiply_row(unsigned row, T const & alpha) { @@ -279,7 +279,7 @@ public: } T dot_product_with_column(const std_vector & y, unsigned j) const { - lp_assert(j < column_count()); + SASSERT(j < column_count()); T ret = numeric_traits::zero(); for (auto & it : m_columns[j]) { ret += y[it.var()] * get_val(it); // get_value_of_column_cell(it); @@ -302,12 +302,12 @@ public: // now fix the columns for (auto & rc : m_rows[i]) { column_cell & cc = m_columns[rc.var()][rc.offset()]; - lp_assert(cc.var() == ii); + SASSERT(cc.var() == ii); cc.var() = i; } for (auto & rc : m_rows[ii]) { column_cell & cc = m_columns[rc.var()][rc.offset()]; - lp_assert(cc.var() == i); + SASSERT(cc.var() == i); cc.var() = ii; } @@ -345,7 +345,7 @@ public: void fill_last_row_with_pivoting(const term& row, unsigned bj, // the index of the basis column const std_vector & basis_heading) { - lp_assert(row_count() > 0); + SASSERT(row_count() > 0); m_work_vector.clear(); m_work_vector.resize(column_count()); T a; @@ -366,7 +366,7 @@ public: for (unsigned j : m_work_vector.m_index) { set (last_row, j, m_work_vector.m_data[j]); } - lp_assert(column_count() > 0); + SASSERT(column_count() > 0); set(last_row, column_count() - 1, one_of_type()); } @@ -382,7 +382,7 @@ public: template L dot_product_with_row(unsigned row, const std_vector & w) const { L ret = zero_of_type(); - lp_assert(row < m_rows.size()); + SASSERT(row < m_rows.size()); for (auto & it : m_rows[row]) { ret += w[it.var()] * it.coeff(); } diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h index 0fd34adae..aa3fff3dc 100644 --- a/src/math/lp/static_matrix_def.h +++ b/src/math/lp/static_matrix_def.h @@ -87,7 +87,7 @@ namespace lp { template void static_matrix::add_rows(const mpq& alpha, unsigned i, unsigned k) { - lp_assert(i < row_count() && k < row_count() && i != k); + SASSERT(i < row_count() && k < row_count() && i != k); auto & rowk = m_rows[k]; scan_row_strip_to_work_vector(rowk); unsigned prev_size_k = static_cast(rowk.size()); diff --git a/src/math/lp/test_bound_analyzer.h b/src/math/lp/test_bound_analyzer.h index 1ca99d637..6cc78526f 100644 --- a/src/math/lp/test_bound_analyzer.h +++ b/src/math/lp/test_bound_analyzer.h @@ -89,7 +89,7 @@ public : void analyze_i_for_upper(unsigned i) { mpq l; bool strict = false; - lp_assert(is_zero(l)); + SASSERT(is_zero(l)); for (unsigned k = 0; k < m_index.size(); k++) { if (k == i) continue; @@ -179,7 +179,7 @@ public : void analyze_i_for_lower(unsigned i) { mpq l; - lp_assert(is_zero(l)); + SASSERT(is_zero(l)); bool strict = false; for (unsigned k = 0; k < m_index.size(); k++) { if (k == i) diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index dedbaa4d0..49771ae47 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -91,7 +91,7 @@ public: unsigned external_to_local(unsigned j) const { auto it = m_external_to_local.find(j); - lp_assert(it != m_external_to_local.end()); + SASSERT(it != m_external_to_local.end()); return it->second; } diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index a5c907208..702e0898d 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -157,6 +157,7 @@ void context_params::updt_params(params_ref const & p) { void context_params::collect_param_descrs(param_descrs & d) { insert_rlimit(d); insert_timeout(d); + insert_ctrl_c(d); d.insert("well_sorted_check", CPK_BOOL, "type checker", "false"); d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp index 40c3360f4..3d1c825f5 100644 --- a/src/qe/mbp/mbp_arrays_tg.cpp +++ b/src/qe/mbp/mbp_arrays_tg.cpp @@ -414,7 +414,6 @@ struct mbp_array_tg::impl { expr* a1 = e1->get_arg(0); for (unsigned j = i + 1; j < rdTerms.size(); j++) { app* e2 = rdTerms.get(j); - expr* a2 = e2->get_arg(0); if (!is_seen(e1, e2) && a1 == e2) { mark_seen(e1, e2); progress = true; diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index 2f2c76da6..9d1d8dd7e 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -17,7 +17,6 @@ z3_add_component(sat sat_ddfw_wrapper.cpp sat_drat.cpp sat_elim_eqs.cpp - sat_elim_vars.cpp sat_gc.cpp sat_integrity_checker.cpp sat_local_search.cpp diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp deleted file mode 100644 index e07dcea77..000000000 --- a/src/sat/sat_elim_vars.cpp +++ /dev/null @@ -1,335 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - sat_elim_vars.cpp - -Abstract: - - Helper class for eliminating variables - -Author: - - Nikolaj Bjorner (nbjorner) 2017-10-14 - -Revision History: - ---*/ - -#include "sat/sat_simplifier.h" -#include "sat/sat_elim_vars.h" -#include "sat/sat_solver.h" - -namespace sat{ - - elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20) { - m_mark_lim = 0; - m_max_literals = 11; - m_miss = 0; - m_hit1 = 0; - m_hit2 = 0; - } - - bool elim_vars::operator()(bool_var v) { - if (s.value(v) != l_undef) - return false; - - literal pos_l(v, false); - literal neg_l(v, true); - unsigned num_bin_pos = simp.num_nonlearned_bin(pos_l); - if (num_bin_pos > m_max_literals) return false; - unsigned num_bin_neg = simp.num_nonlearned_bin(neg_l); - if (num_bin_neg > m_max_literals) return false; - clause_use_list & pos_occs = simp.m_use_list.get(pos_l); - clause_use_list & neg_occs = simp.m_use_list.get(neg_l); - unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.num_irredundant() + neg_occs.num_irredundant(); - if (clause_size == 0) { - return false; - } - reset_mark(); - mark_var(v); - if (!mark_literals(pos_occs)) return false; - if (!mark_literals(neg_occs)) return false; - if (!mark_literals(pos_l)) return false; - if (!mark_literals(neg_l)) return false; - - // associate index with each variable. - sort_marked(); - dd::bdd b1 = elim_var(v); - double sz1 = b1.cnf_size(); - if (sz1 > 2*clause_size) { - ++m_miss; - return false; - } - if (sz1 <= clause_size) { - ++m_hit1; - return elim_var(v, b1); - } - m.try_cnf_reorder(b1); - sz1 = b1.cnf_size(); - if (sz1 <= clause_size) { - ++m_hit2; - return elim_var(v, b1); - } - ++m_miss; - return false; - } - - bool elim_vars::elim_var(bool_var v, dd::bdd const& b) { - literal pos_l(v, false); - literal neg_l(v, true); - clause_use_list & pos_occs = simp.m_use_list.get(pos_l); - clause_use_list & neg_occs = simp.m_use_list.get(neg_l); - - // eliminate variable - simp.m_pos_cls.reset(); - simp.m_neg_cls.reset(); - simp.collect_clauses(pos_l, simp.m_pos_cls); - simp.collect_clauses(neg_l, simp.m_neg_cls); - VERIFY(!simp.is_external(v)); - - model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); - simp.save_clauses(mc_entry, simp.m_pos_cls); - simp.save_clauses(mc_entry, simp.m_neg_cls); - s.m_eliminated[v] = true; - ++s.m_stats.m_elim_var_bdd; - simp.remove_bin_clauses(pos_l); - simp.remove_bin_clauses(neg_l); - simp.remove_clauses(pos_occs, pos_l); - simp.remove_clauses(neg_occs, neg_l); - pos_occs.reset(); - neg_occs.reset(); - literal_vector lits; - add_clauses(v, b, lits); - return true; - } - - dd::bdd elim_vars::elim_var(bool_var v) { - unsigned index = 0; - for (bool_var w : m_vars) { - m_var2index[w] = index++; - } - literal pos_l(v, false); - literal neg_l(v, true); - clause_use_list & pos_occs = simp.m_use_list.get(pos_l); - clause_use_list & neg_occs = simp.m_use_list.get(neg_l); - - dd::bdd b1 = make_clauses(pos_l); - dd::bdd b2 = make_clauses(neg_l); - dd::bdd b3 = make_clauses(pos_occs); - dd::bdd b4 = make_clauses(neg_occs); - dd::bdd b0 = b1 && b2 && b3 && b4; - dd::bdd b = m.mk_exists(m_var2index[v], b0); - TRACE("elim_vars", - tout << "eliminate " << v << "\n"; - for (watched const& w : simp.get_wlist(~pos_l)) { - if (w.is_binary_non_learned_clause()) { - tout << pos_l << " " << w.get_literal() << "\n"; - } - } - m.display(tout, b1); - for (watched const& w : simp.get_wlist(~neg_l)) { - if (w.is_binary_non_learned_clause()) { - tout << neg_l << " " << w.get_literal() << "\n"; - } - } - m.display(tout, b2); - clause_use_list::iterator itp = pos_occs.mk_iterator(); - while (!itp.at_end()) { - clause const& c = itp.curr(); - tout << c << "\n"; - itp.next(); - } - m.display(tout, b3); - clause_use_list::iterator itn = neg_occs.mk_iterator(); - while (!itn.at_end()) { - clause const& c = itn.curr(); - tout << c << "\n"; - itn.next(); - } - m.display(tout, b4); - tout << "eliminated:\n"; - tout << b << "\n"; - tout << b.cnf_size() << "\n"; - ); - - return b; - } - - void elim_vars::add_clauses(bool_var v0, dd::bdd const& b, literal_vector& lits) { - if (b.is_true()) { - // no-op - } - else if (b.is_false()) { - SASSERT(lits.size() > 0); - literal_vector c(lits); - if (simp.cleanup_clause(c)) - return; - - switch (c.size()) { - case 0: - s.set_conflict(); - break; - case 1: - simp.propagate_unit(c[0]); - break; - case 2: - s.m_stats.m_mk_bin_clause++; - simp.add_non_learned_binary_clause(c[0], c[1]); - simp.back_subsumption1(c[0], c[1], false); - break; - default: { - if (c.size() == 3) - s.m_stats.m_mk_ter_clause++; - else - s.m_stats.m_mk_clause++; - clause* cp = s.alloc_clause(c.size(), c.data(), false); - s.m_clauses.push_back(cp); - simp.m_use_list.insert(*cp); - if (simp.m_sub_counter > 0) - simp.back_subsumption1(*cp); - else - simp.back_subsumption0(*cp); - break; - } - } - } - else { - unsigned v = m_vars[b.var()]; - lits.push_back(literal(v, false)); - add_clauses(v0, b.lo(), lits); - lits.pop_back(); - lits.push_back(literal(v, true)); - add_clauses(v0, b.hi(), lits); - lits.pop_back(); - } - } - - - void elim_vars::get_clauses(dd::bdd const& b, literal_vector & lits, clause_vector& clauses, literal_vector& units) { - if (b.is_true()) { - return; - } - if (b.is_false()) { - if (lits.size() > 1) { - clause* c = s.alloc_clause(lits.size(), lits.data(), false); - clauses.push_back(c); - } - else { - units.push_back(lits.back()); - } - return; - } - - // if (v hi lo) - // (v | lo) & (!v | hi) - // if (v T lo) -> (v | lo) - unsigned v = m_vars[b.var()]; - lits.push_back(literal(v, false)); - get_clauses(b.lo(), lits, clauses, units); - lits.pop_back(); - lits.push_back(literal(v, true)); - get_clauses(b.hi(), lits, clauses, units); - lits.pop_back(); - } - - void elim_vars::reset_mark() { - m_vars.reset(); - m_mark.resize(s.num_vars()); - m_var2index.resize(s.num_vars()); - m_occ.resize(s.num_vars()); - ++m_mark_lim; - if (m_mark_lim == 0) { - ++m_mark_lim; - m_mark.fill(0); - } - } - - class elim_vars::compare_occ { - elim_vars& ev; - public: - compare_occ(elim_vars& ev):ev(ev) {} - - bool operator()(bool_var v1, bool_var v2) const { - return ev.m_occ[v1] < ev.m_occ[v2]; - } - }; - - void elim_vars::sort_marked() { - std::sort(m_vars.begin(), m_vars.end(), compare_occ(*this)); - } - - void elim_vars::shuffle_vars() { - unsigned sz = m_vars.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned x = m_rand(sz); - unsigned y = m_rand(sz); - std::swap(m_vars[x], m_vars[y]); - } - } - - void elim_vars::mark_var(bool_var v) { - if (m_mark[v] != m_mark_lim) { - m_mark[v] = m_mark_lim; - m_vars.push_back(v); - m_occ[v] = 1; - } - else { - ++m_occ[v]; - } - } - - bool elim_vars::mark_literals(clause_use_list & occs) { - clause_use_list::iterator it = occs.mk_iterator(); - while (!it.at_end()) { - clause const& c = it.curr(); - for (literal l : c) { - mark_var(l.var()); - } - if (num_vars() > m_max_literals) return false; - it.next(); - } - return true; - } - - bool elim_vars::mark_literals(literal lit) { - watch_list& wl = simp.get_wlist(lit); - for (watched const& w : wl) { - if (w.is_binary_non_learned_clause()) { - mark_var(w.get_literal().var()); - } - } - return num_vars() <= m_max_literals; - } - - dd::bdd elim_vars::make_clauses(clause_use_list & occs) { - dd::bdd result = m.mk_true(); - for (auto it = occs.mk_iterator(); !it.at_end(); it.next()) { - clause const& c = it.curr(); - dd::bdd cl = m.mk_false(); - for (literal l : c) { - cl |= mk_literal(l); - } - result &= cl; - } - return result; - } - - dd::bdd elim_vars::make_clauses(literal lit) { - dd::bdd result = m.mk_true(); - watch_list& wl = simp.get_wlist(~lit); - for (watched const& w : wl) { - if (w.is_binary_non_learned_clause()) { - result &= (mk_literal(lit) || mk_literal(w.get_literal())); - } - } - return result; - } - - dd::bdd elim_vars::mk_literal(literal l) { - return l.sign() ? m.mk_nvar(m_var2index[l.var()]) : m.mk_var(m_var2index[l.var()]); - } - -}; - diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h deleted file mode 100644 index 6465cbb87..000000000 --- a/src/sat/sat_elim_vars.h +++ /dev/null @@ -1,72 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - sat_elim_vars.h - -Abstract: - - Helper class for eliminating variables - -Author: - - Nikolaj Bjorner (nbjorner) 2017-10-14 - -Revision History: - ---*/ -#pragma once - -#include "sat/sat_types.h" -#include "math/dd/dd_bdd.h" - -namespace sat { - class solver; - class simplifier; - - class elim_vars { - class compare_occ; - - simplifier& simp; - solver& s; - dd::bdd_manager m; - random_gen m_rand; - - - svector m_vars; - unsigned_vector m_mark; - unsigned m_mark_lim; - unsigned_vector m_var2index; - unsigned_vector m_occ; - unsigned m_miss; - unsigned m_hit1; - unsigned m_hit2; - - unsigned m_max_literals; - - unsigned num_vars() const { return m_vars.size(); } - void reset_mark(); - void mark_var(bool_var v); - void sort_marked(); - void shuffle_vars(); - bool mark_literals(clause_use_list & occs); - bool mark_literals(literal lit); - dd::bdd make_clauses(clause_use_list & occs); - dd::bdd make_clauses(literal lit); - dd::bdd mk_literal(literal l); - void get_clauses(dd::bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units); - void add_clauses(bool_var v, dd::bdd const& b, literal_vector& lits); - bool elim_var(bool_var v, dd::bdd const& b); - dd::bdd elim_var(bool_var v); - - public: - elim_vars(simplifier& s); - bool operator()(bool_var v); - unsigned hit2() const { return m_hit1; } // first round bdd construction is minimal - unsigned hit1() const { return m_hit2; } // minimal after reshufling - unsigned miss() const { return m_miss; } // not-minimal - }; - -}; - diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 56b81604d..289afdd75 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -21,7 +21,6 @@ Revision History: #include "sat/sat_simplifier.h" #include "sat/sat_simplifier_params.hpp" #include "sat/sat_solver.h" -#include "sat/sat_elim_vars.h" #include "sat/sat_integrity_checker.h" #include "util/stopwatch.h" #include "util/trace.h" @@ -111,9 +110,6 @@ namespace sat { bool simplifier::cce_enabled() const { return bce_enabled_base() && (m_cce || m_acce); } bool simplifier::abce_enabled() const { return bce_enabled_base() && m_abce; } bool simplifier::bca_enabled() const { return bce_enabled_base() && m_bca; } - bool simplifier::elim_vars_bdd_enabled() const { - return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded(); - } bool simplifier::elim_vars_enabled() const { return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars && single_threaded(); } @@ -2076,24 +2072,19 @@ namespace sat { }; void simplifier::elim_vars() { - if (!elim_vars_enabled()) return; + if (!elim_vars_enabled()) + return; elim_var_report rpt(*this); bool_var_vector vars; order_vars_for_elim(vars); - sat::elim_vars elim_bdd(*this); for (bool_var v : vars) { checkpoint(); if (m_elim_counter < 0) break; - if (is_external(v)) { - // skip - } - else if (try_eliminate(v)) { - m_num_elim_vars++; - } - else if (elim_vars_bdd_enabled() && elim_bdd(v)) { - m_num_elim_vars++; - } + if (is_external(v)) + ; // skip + else if (try_eliminate(v)) + m_num_elim_vars++; } m_pos_cls.finalize(); @@ -2126,8 +2117,6 @@ namespace sat { m_subsumption = p.subsumption(); m_subsumption_limit = p.subsumption_limit(); m_elim_vars = p.elim_vars(); - m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy? - m_elim_vars_bdd_delay = p.elim_vars_bdd_delay(); m_incremental_mode = s.get_config().m_incremental && !p.override_incremental(); } diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg index 93864ce24..0275ef248 100644 --- a/src/sat/sat_simplifier_params.pyg +++ b/src/sat/sat_simplifier_params.pyg @@ -23,8 +23,6 @@ def_module_params(module_name='sat', ('resolution.cls_cutoff1', UINT, 100000000, 'limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination'), ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'), ('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'), - ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'), - ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'), ('probing', BOOL, True, 'apply failed literal detection during simplification'), ('probing_limit', UINT, 5000000, 'limit to the number of probe calls'), ('probing_cache', BOOL, True, 'add binary literals as lemmas'), diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 813faba3d..cd280d158 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -35,7 +35,7 @@ namespace arith { lp().updt_params(ctx.s().params()); lp().settings().set_resource_limit(m_resource_limit); lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode(); - lp().settings().int_run_gcd_test() = get_config().m_arith_gcd_test; + lp().settings().set_run_gcd_test(get_config().m_arith_gcd_test); lp().settings().set_random_seed(get_config().m_random_seed); m_lia = alloc(lp::int_solver, *m_solver.get()); diff --git a/src/sat/tactic/sat2goal.h b/src/sat/tactic/sat2goal.h index 8c0b1bf83..97a85ff65 100644 --- a/src/sat/tactic/sat2goal.h +++ b/src/sat/tactic/sat2goal.h @@ -53,6 +53,7 @@ public: mc(ast_manager& m); // flush model converter from SAT solver to this structure. void flush_smc(sat::solver& s, atom2bool_var const& map); + using model_converter::operator(); void operator()(sat::model& m); void operator()(model_ref& md) override; void operator()(expr_ref& fml) override; diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 15641315e..c1eb0148a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -57,10 +57,6 @@ def_module_params(module_name='smt', ('bv.solver', UINT, 0, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), - ('arith.lp.dio_eqs', BOOL, False, 'use Diophantine equalities'), - ('arith.lp.dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'), - ('arith.lp.dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'), - ('arith.lp.dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), ('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 72fac2371..657775a6a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -871,7 +871,7 @@ public: unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio; lp().set_cut_strategy(branch_cut_ratio); - lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test; + lp().settings().set_run_gcd_test(ctx().get_fparams().m_arith_gcd_test); lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); m_lia = alloc(lp::int_solver, *m_solver.get()); } diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 30eac685d..096633d4e 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -276,7 +276,7 @@ namespace smt { graph r_graph; for (enode* n : ctx.enodes_of(f)) { literal lit = ctx.enode2literal(n); - if (l_true == ctx.get_assignment(lit)) { + if (l_true == ctx.get_assignment(lit) && ctx.is_relevant(lit)) { expr* e = ctx.bool_var2expr(lit.var()); expr* arg1 = to_app(e)->get_arg(0); expr* arg2 = to_app(e)->get_arg(1); @@ -284,12 +284,14 @@ namespace smt { enode* tcn = ensure_enode(tc_app); if (ctx.get_assignment(tcn) != l_true) { literal consequent = ctx.get_literal(tc_app); + ctx.mark_as_relevant(consequent); justification* j = ctx.mk_justification(theory_propagation_justification(get_id(), ctx, 1, &lit, consequent)); TRACE("special_relations", tout << "propagate: " << tc_app << "\n";); ctx.assign(consequent, j); new_assertion = true; } else { + TRACE("special_relations", tout << "add edge " << tc_app << " relevant: " << ctx.is_relevant(tcn) << "\n"); theory_var v1 = get_representative(get_th_var(arg1)); theory_var v2 = get_representative(get_th_var(arg2)); r_graph.init_var(v1); @@ -333,6 +335,7 @@ namespace smt { expr_ref f_app(m.mk_app(f, arg1, arg2), m); ensure_enode(f_app); literal f_lit = ctx.get_literal(f_app); + ctx.mark_as_relevant(f_lit); switch (ctx.get_assignment(f_lit)) { case l_true: SASSERT(new_assertion); @@ -369,8 +372,12 @@ namespace smt { while (r.is_next(nxt)) { expr* left = to_app(nxt)->get_arg(0); expr* right = to_app(nxt)->get_arg(1); - ctx.assign(~mk_eq(next, left, false), nullptr); - ctx.assign(~mk_eq(next, right, false), nullptr); + literal eq1 = mk_eq(next, left, false); + literal eq2 = mk_eq(next, right, false); + ctx.mark_as_relevant(eq1); + ctx.mark_as_relevant(eq2); + ctx.assign(~eq1, nullptr); + ctx.assign(~eq2, nullptr); nxt = left; } ctx.set_true_first_flag(ctx.get_literal(next_b).var()); @@ -600,6 +607,7 @@ namespace smt { r.m_explanation.reset(); unsigned timestamp = r.m_graph.get_timestamp(); bool found_path = a.v1() == a.v2() || r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r); + TRACE("special_relations", tout << "check " << a.v1() << " -> " << a.v2() << " found_path: " << found_path << "\n"); if (found_path) { TRACE("special_relations", tout << "check po conflict\n";); r.m_explanation.push_back(a.explanation()); diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 7a51d01fe..015108cc3 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -245,7 +245,6 @@ class fix_dl_var_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { tactic_report report("fix-dl-var", *g); - bool produce_proofs = g->proofs_enabled(); m_produce_models = g->models_enabled(); TRACE("fix_dl_var", g->display(tout);); diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 9ac675d1a..04ec122ab 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -72,7 +72,7 @@ struct gomory_test { expl.add_pair(column_lower_bound_constraint(x_j), new_a); } else { - lp_assert(at_upper(x_j)); + SASSERT(at_upper(x_j)); if (a.is_pos()) { new_a = a / f_0; new_a.neg(); // the upper terms are inverted. @@ -88,9 +88,9 @@ struct gomory_test { } void int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term & t, explanation& expl, mpq & lcm_den, const mpq& f_0, const mpq& one_minus_f_0) { - lp_assert(is_integer(x_j)); - lp_assert(!a.is_int()); - lp_assert(f_0 > zero_of_type() && f_0 < one_of_type()); + SASSERT(is_integer(x_j)); + SASSERT(!a.is_int()); + SASSERT(f_0 > zero_of_type() && f_0 < one_of_type()); mpq f_j = fractional_part(a); TRACE("gomory_cut_detail", tout << a << " x_j = " << x_j << ", k = " << k << "\n"; @@ -99,7 +99,7 @@ struct gomory_test { tout << "1 - f_0: " << one_minus_f_0 << "\n"; tout << "at_low(" << x_j << ") = " << at_low(x_j) << std::endl; ); - lp_assert (!f_j.is_zero()); + SASSERT (!f_j.is_zero()); mpq new_a; if (at_low(x_j)) { if (f_j <= one_minus_f_0) { @@ -112,7 +112,7 @@ struct gomory_test { expl.add_pair(column_lower_bound_constraint(x_j), new_a); } else { - lp_assert(at_upper(x_j)); + SASSERT(at_upper(x_j)); if (f_j <= f_0) { new_a = f_j / f_0; } @@ -134,13 +134,13 @@ struct gomory_test { } void adjust_term_and_k_for_some_ints_case_gomory(lar_term& t, mpq& k, mpq &lcm_den) { - lp_assert(!t.is_empty()); + SASSERT(!t.is_empty()); auto pol = t.coeffs_as_vector(); t.clear(); if (pol.size() == 1) { TRACE("gomory_cut_detail", tout << "pol.size() is 1" << std::endl;); unsigned v = pol[0].second; - lp_assert(is_integer(v)); + SASSERT(is_integer(v)); const mpq& a = pol[0].first; k /= a; if (a.is_pos()) { // we have av >= k @@ -162,7 +162,7 @@ struct gomory_test { tout << pol[i].first << " " << pol[i].second << "\n"; } tout << "k: " << k << "\n";); - lp_assert(lcm_den.is_pos()); + SASSERT(lcm_den.is_pos()); if (!lcm_den.is_one()) { // normalize coefficients of integer parameters to be integers. for (auto & pi: pol) { @@ -183,7 +183,7 @@ struct gomory_test { k.neg(); } TRACE("gomory_cut_detail", tout << "k = " << k << std::endl;); - lp_assert(k.is_int()); + SASSERT(k.is_int()); } void print_term(lar_term & t, std::ostream & out) { diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 5afeea3fa..3de741d42 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -384,7 +384,7 @@ vector allocate_basis_heading( void init_basic_part_of_basis_heading(vector &basis, vector &basis_heading) { - lp_assert(basis_heading.size() >= basis.size()); + SASSERT(basis_heading.size() >= basis.size()); unsigned m = basis.size(); for (unsigned i = 0; i < m; i++) { unsigned column = basis[i]; @@ -577,7 +577,7 @@ void test_stacked_unsigned() { v = 3; v = 4; v.pop(); - lp_assert(v == 2); + SASSERT(v == 2); v++; v++; std::cout << "before push v=" << v << std::endl; @@ -587,7 +587,7 @@ void test_stacked_unsigned() { v += 1; std::cout << "v = " << v << std::endl; v.pop(2); - lp_assert(v == 4); + SASSERT(v == 4); const unsigned &rr = v; std::cout << rr << std::endl; } @@ -751,22 +751,23 @@ void test_numeric_pair() { numeric_pair c(0.1, 0.5); a += 2 * c; a -= c; - lp_assert(a == b + c); + SASSERT(a == b + c); numeric_pair d = a * 2; std::cout << a << std::endl; - lp_assert(b == b); - lp_assert(b < a); - lp_assert(b <= a); - lp_assert(a > b); - lp_assert(a != b); - lp_assert(a >= b); - lp_assert(-a < b); - lp_assert(a < 2 * b); - lp_assert(b + b > a); - lp_assert(lp::mpq(2.1) * b + b > a); - lp_assert(-b * lp::mpq(2.1) - b < lp::mpq(0.99) * a); + SASSERT(b == b); + SASSERT(b < a); + SASSERT(b <= a); + SASSERT(a > b); + SASSERT(a != b); + SASSERT(a >= b); + SASSERT(-a < b); + SASSERT(a < 2 * b); + SASSERT(b + b > a); + SASSERT(lp::mpq(2.1) * b + b > a); + SASSERT(-b * lp::mpq(2.1) - b < lp::mpq(0.99) * a); std::cout << -b * lp::mpq(2.1) - b << std::endl; - lp_assert(-b * (lp::mpq(2.1) + 1) == -b * lp::mpq(2.1) - b); + SASSERT(-b * (lp::mpq(2.1) + 1) == -b * lp::mpq(2.1) - b); + std::cout << -b * (lp::mpq(2.1) + 1) << std::endl; } void get_matrix_dimensions(std::ifstream &f, unsigned &m, unsigned &n) { @@ -829,7 +830,7 @@ void test_term() { << t.second.get_double() << ","; } - std::cout << "\ntableu after cube\n"; + std::cout << "\ntableau after cube\n"; solver.pp(std::cout).print(); std::cout << "Ax_is_correct = " << solver.ax_is_correct() << "\n"; } @@ -854,7 +855,7 @@ void test_evidence_for_total_inf_simple(argument_parser &args_parser) { auto status = solver.solve(); std::cout << lp_status_to_string(status) << std::endl; std::unordered_map model; - lp_assert(solver.get_status() == lp_status::INFEASIBLE); + SASSERT(solver.get_status() == lp_status::INFEASIBLE); } void test_bound_propagation_one_small_sample1() { /* @@ -1060,8 +1061,8 @@ void test_total_case_l() { // ls.solve(); // my_bound_propagator bp(ls); // ls.propagate_bounds_for_touched_rows(bp); - // lp_assert(ev.size() == 4); - // lp_assert(contains_j_kind(x, GE, - one_of_type(), ev)); + // SASSERT(ev.size() == 4); + // SASSERT(contains_j_kind(x, GE, - one_of_type(), ev)); } void test_bound_propagation() { test_total_case_u(); @@ -1077,14 +1078,14 @@ void test_int_set() { indexed_uint_set s; s.insert(1); s.insert(2); - lp_assert(s.contains(2)); - lp_assert(s.size() == 2); + SASSERT(s.contains(2)); + SASSERT(s.size() == 2); s.remove(2); - lp_assert(s.size() == 1); + SASSERT(s.size() == 1); s.insert(3); s.insert(2); s.reset(); - lp_assert(s.size() == 0); + SASSERT(s.size() == 0); std::cout << "done test_int_set\n"; } @@ -1192,13 +1193,13 @@ void get_random_interval(bool &neg_inf, bool &pos_inf, int &x, int &y) { pos_inf = false; if (!neg_inf) { y = x + my_random() % (101 - x); - lp_assert(y >= x); + SASSERT(y >= x); } else { y = my_random() % 100; } } - lp_assert((neg_inf || (0 <= x && x <= 100)) && - (pos_inf || (0 <= y && y <= 100))); + SASSERT((neg_inf || (0 <= x && x <= 100)) && + (pos_inf || (0 <= y && y <= 100))); } void test_gomory_cut_0() { @@ -1628,7 +1629,7 @@ void test_maximize_term() { solver.add_var_bound(term_x_min_y, LE, zero_of_type()); solver.add_var_bound(term_2x_pl_2y, LE, mpq(5)); solver.find_feasible_solution(); - lp_assert(solver.get_status() == lp_status::OPTIMAL); + SASSERT(solver.get_status() == lp_status::OPTIMAL); std::cout << solver.constraints(); std::unordered_map model; solver.get_model(model); @@ -1671,7 +1672,8 @@ void test_dio() { lpvar fx_7 = solver.add_var(_fx_7, true); lpvar fx_17 = solver.add_var(_fx_17, true); vector> term_ls; - /* 3x1 + 3x2 + 14x3 − 7 */ + /* 3x1 + 3x2 +```cpp + 14x3 − 7 */ term_ls.push_back(std::pair(mpq(3), x1)); term_ls.push_back(std::pair(mpq(3), x2)); term_ls.push_back(std::pair(mpq(14), x3)); @@ -1701,7 +1703,7 @@ void test_dio() { solver.add_var_bound(t1, LE, mpq(0)); solver.add_var_bound(t1, GE, mpq(0)); // solver.find_feasible_solution(); - //lp_assert(solver.get_status() == lp_status::OPTIMAL); + //SASSERT(solver.get_status() == lp_status::OPTIMAL); enable_trace("dioph_eq"); enable_trace("dioph_eq_fresh"); #ifdef Z3DEBUG @@ -1908,13 +1910,13 @@ void asserts_on_patching(const rational &x, const rational &alpha) { auto a2 = denominator(alpha); auto x1 = numerator(x); auto x2 = denominator(x); - lp_assert(a1.is_pos()); - lp_assert(abs(a1) < abs(a2)); - lp_assert(coprime(a1, a2)); - lp_assert(x1.is_pos()); - lp_assert(x1 < x2); - lp_assert(coprime(x1, x2)); - lp_assert((a2 / x2).is_int()); + SASSERT(a1.is_pos()); + SASSERT(abs(a1) < abs(a2)); + SASSERT(coprime(a1, a2)); + SASSERT(x1.is_pos()); + SASSERT(x1 < x2); + SASSERT(coprime(x1, x2)); + SASSERT((a2 / x2).is_int()); } void get_patching_deltas(const rational &x, const rational &alpha, rational &delta_0, rational &delta_1) { std::cout << "get_patching_deltas(" << x << ", " << alpha << ")" << std::endl; @@ -1922,7 +1924,7 @@ void get_patching_deltas(const rational &x, const rational &alpha, rational &del auto a2 = denominator(alpha); auto x1 = numerator(x); auto x2 = denominator(x); - lp_assert(divides(x2, a2)); + SASSERT(divides(x2, a2)); // delta has to be integral. // We need to find delta such that x1/x2 + (a1/a2)*delta is integral. // Then a2*x1/x2 + a1*delta is integral, that means that t = a2/x2 is integral. @@ -1936,17 +1938,17 @@ void get_patching_deltas(const rational &x, const rational &alpha, rational &del // We know that a2 and a1 are coprime, and x2 divides a2, so x2 and a1 are coprime. rational u, v; auto g = gcd(a1, x2, u, v); - lp_assert(g.is_one() && u.is_int() && v.is_int() && g == u * a1 + v * x2); + SASSERT(g.is_one() && u.is_int() && v.is_int() && g == u * a1 + v * x2); std::cout << "u = " << u << ", v = " << v << std::endl; std::cout << "x= " << (x1 / x2) << std::endl; std::cout << "x + (a1 / a2) * (-u * t) * x1 = " << x + (a1 / a2) * (-u * t) * x1 << std::endl; - lp_assert((x + (a1 / a2) * (-u * t) * x1).is_int()); + SASSERT((x + (a1 / a2) * (-u * t) * x1).is_int()); // 1 = (u- l*x2 ) * a1 + (v + l*a1)*x2, for every integer l. rational d = u * t * x1; delta_0 = mod(d, a2); - lp_assert(delta_0 > 0); + SASSERT(delta_0 > 0); delta_1 = delta_0 - a2; - lp_assert(delta_1 < 0); + SASSERT(delta_1 < 0); std::cout << "delta_0 = " << delta_0 << std::endl; std::cout << "delta_1 = " << delta_1 << std::endl; } @@ -1974,10 +1976,10 @@ void test_patching_alpha(const rational &x, const rational &alpha) { rational delta_0, delta_1; get_patching_deltas(x, alpha, delta_0, delta_1); - lp_assert(delta_0 * delta_1 < 0); + SASSERT(delta_0 * delta_1 < 0); - lp_assert((x - alpha * delta_0).is_int()); - lp_assert((x - alpha * delta_1).is_int()); + SASSERT((x - alpha * delta_0).is_int()); + SASSERT((x - alpha * delta_1).is_int()); try_find_smaller_delta(x, alpha, delta_0, delta_1); // std::cout << "delta_minus = " << delta_minus << ", delta_1 = " << delta_1 << "\n"; // std::cout << "x + alpha*delta_minus = " << x + alpha * delta_minus << "\n"; @@ -1988,7 +1990,7 @@ void find_a1_x1_x2_and_fix_a2(int &x1, int &x2, int &a1, int &a2) { x2 = (rand() % a2) + (int)(a2 / 3); auto g = gcd(rational(a2), rational(x2)); a2 *= (x2 / numerator(g).get_int32()); - lp_assert(rational(a2, x2).is_int()); + SASSERT(rational(a2, x2).is_int()); do { x1 = rand() % (unsigned)x2 + 1; } while (!coprime(x1, x2)); @@ -1998,6 +2000,7 @@ void find_a1_x1_x2_and_fix_a2(int &x1, int &x2, int &a1, int &a2) { } while (!coprime(a1, a2)); } + void test_patching() { srand(1); // repeat the test 100 times diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h index 0e638399f..3458e3b2a 100644 --- a/src/test/lp/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -117,13 +117,13 @@ namespace lp { void fill_simple_elem(lisp_elem & lm) { int separator = first_separator(); - lp_assert(-1 != separator && separator != 0); + SASSERT(-1 != separator && separator != 0); lm.m_head = m_line.substr(0, separator); m_line = m_line.substr(separator); } void fill_nested_elem(lisp_elem & lm) { - lp_assert(m_line[0] == '('); + SASSERT(m_line[0] == '('); m_line = m_line.substr(1); int separator = first_separator(); lm.m_head = m_line.substr(0, separator); @@ -190,11 +190,11 @@ namespace lp { } void adjust_right_side(formula_constraint & /* c*/, lisp_elem & /*el*/) { - // lp_assert(el.m_head == "0"); // do nothing for the time being + // SASSERT(el.m_head == "0"); // do nothing for the time being } void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) { - lp_assert(el.m_elems.size() == 2); + SASSERT(el.m_elems.size() == 2); set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]); adjust_right_side(c, el.m_elems[1]); } @@ -210,7 +210,7 @@ namespace lp { add_mult_elem(c, el.m_elems); } else if (el.m_head == "~") { lisp_elem & minel = el.m_elems[0]; - lp_assert(minel.is_simple()); + SASSERT(minel.is_simple()); c.m_right_side += mpq(str_to_int(minel.m_head)); } else { std::cout << "unexpected input " << el.m_head << std::endl; @@ -220,14 +220,14 @@ namespace lp { } std::string get_name(lisp_elem & name) { - lp_assert(name.is_simple()); - lp_assert(!is_integer(name.m_head)); + SASSERT(name.is_simple()); + SASSERT(!is_integer(name.m_head)); return name.m_head; } void add_mult_elem(formula_constraint & c, std::vector & els) { - lp_assert(els.size() == 2); + SASSERT(els.size() == 2); mpq coeff = get_coeff(els[0]); std::string col_name = get_name(els[1]); c.add_pair(coeff, col_name); @@ -237,16 +237,16 @@ namespace lp { if (le.is_simple()) { return mpq(str_to_int(le.m_head)); } else { - lp_assert(le.m_head == "~"); - lp_assert(le.size() == 1); + SASSERT(le.m_head == "~"); + SASSERT(le.size() == 1); lisp_elem & el = le.m_elems[0]; - lp_assert(el.is_simple()); + SASSERT(el.is_simple()); return -mpq(str_to_int(el.m_head)); } } int str_to_int(std::string & s) { - lp_assert(is_integer(s)); + SASSERT(is_integer(s)); return atoi(s.c_str()); } @@ -254,7 +254,7 @@ namespace lp { if (el.size()) { add_complex_sum_elem(c, el); } else { - lp_assert(is_integer(el.m_head)); + SASSERT(is_integer(el.m_head)); int v = atoi(el.m_head.c_str()); mpq vr(v); c.m_right_side -= vr; diff --git a/src/util/params.h b/src/util/params.h index 200b4aa2c..c499dd56e 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -115,6 +115,7 @@ class param_descrs { public: param_descrs(); ~param_descrs(); + param_descrs& operator=(param_descrs const&) = delete; void copy(param_descrs & other); void insert(char const * name, param_kind k, char const * descr, char const * def = nullptr, char const* module = nullptr); void insert(symbol const & name, param_kind k, char const * descr, char const * def = nullptr, char const* module = nullptr); diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index e5502dc33..b5021e9a2 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/src/util/scoped_ctrl_c.cpp @@ -21,6 +21,7 @@ Revision History: #include #include #include "util/scoped_ctrl_c.h" +#include "util/gparams.h" #ifdef _WINDOWS #define USE_SIGNAL @@ -105,7 +106,10 @@ scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool once, bool enabled): m_cancel_eh(eh), m_first(true), m_once(once), - m_enabled(enabled) { + m_enabled(enabled), + m_old_scoped_ctrl_c(g_obj) { + if (gparams::get_value("ctrl_c") == "false") + m_enabled = false; if (m_enabled) { signal_lock(); active_contexts.push_back(this); diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 4a62b9280..286dcda8c 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -48,7 +48,6 @@ struct scoped_timer_state { static std::vector available_workers; static std::mutex workers; -static atomic num_workers(0); static void thread_func(scoped_timer_state *s) { workers.lock(); @@ -94,7 +93,6 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { // start new thead workers.unlock(); s = new scoped_timer_state; - ++num_workers; init_state(ms, eh); s->m_thread = std::thread(thread_func, s); } @@ -131,25 +129,19 @@ void scoped_timer::initialize() { } void scoped_timer::finalize() { - unsigned deleted = 0; - while (deleted < num_workers) { - workers.lock(); - for (auto w : available_workers) { - w->work = EXITING; - w->cv.notify_one(); - } - decltype(available_workers) cleanup_workers; - std::swap(available_workers, cleanup_workers); - workers.unlock(); - - for (auto w : cleanup_workers) { - ++deleted; - w->m_thread.join(); - delete w; - } + workers.lock(); + for (auto w : available_workers) { + w->work = EXITING; + w->cv.notify_one(); + } + decltype(available_workers) cleanup_workers; + std::swap(available_workers, cleanup_workers); + workers.unlock(); + + for (auto w : cleanup_workers) { + w->m_thread.join(); + delete w; } - num_workers = 0; - available_workers.clear(); } void scoped_timer::init_state(unsigned ms, event_handler * eh) {