mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-09 16:55:47 +00:00
Code Activity

Merge branch 'master' into ctrl-c-races

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-19 13:58:13 -07:00 • committed by GitHub
commit 78c5800a99
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
77 changed files with 1351 additions and 1207 deletions
Download patch file Download diff file Expand all files Collapse all files

125
.github/workflows/ocaml-all.yaml vendored Normal file
View file

@ -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

99
.github/workflows/ocaml.yaml vendored Normal file
View file

@ -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

3
README-CMake.md
View file

@ -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.

8
README.md
View file

@ -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)
<a href="https://github.com/z3prover/z3/pkgs/container/z3">Docker image</a>.
| 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

106
cmake/modules/FindOCaml.cmake Normal file
View file

@ -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()

12
src/CMakeLists.txt
View file

@ -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
################################################################################

2
src/api/api_config_params.cpp
View file

@ -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<param_descrs&>(gparams::get_global_param_descrs()));
auto r = of_param_descrs(d);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);

10
src/api/api_datatype.cpp
View file

@ -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);

1
src/api/api_solver.cpp
View file

@ -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;

4
src/api/java/Optimize.java
View file

@ -58,7 +58,7 @@ public class Optimize extends Z3Object {
/**
* Assert a constraint (or multiple) into the optimize solver.
**/
public void Assert(Expr<BoolSort> ... constraints)
public void Assert(Expr<BoolSort>... constraints)
{
getContext().checkContextMatch(constraints);
for (Expr<BoolSort> a : constraints)
@ -70,7 +70,7 @@ public class Optimize extends Z3Object {
/**
* Alias for Assert.
**/
public void Add(Expr<BoolSort> ... constraints)
public void Add(Expr<BoolSort>... constraints)
{
Assert(constraints);
}

19
src/api/mcp/z3mcp.py Normal file
View file

@ -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()

330
src/api/ml/CMakeLists.txt Normal file
View file

@ -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<pkg>.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 "$<TARGET_FILE:libz3>" "$<TARGET_FILE:libz3>"
COMMAND install_name_tool -change "@rpath/libz3.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.dylib" "$<TARGET_FILE:libz3>" "${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()

10
src/api/ml/z3.mli
View file

@ -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

1
src/api/python/setup.py
View file

@ -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)

4
src/api/python/z3/z3.py
View file

@ -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?)

7
src/api/z3_api.h
View file

@ -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.

1
src/ast/sls/sls_bv_fixed.cpp
View file

@ -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)

1
src/ast/sls/sls_bv_fixed.h
View file

@ -29,7 +29,6 @@ namespace sls {
class bv_fixed {
bv_eval& ev;
bv_terms& terms;
ast_manager& m;
bv_util& bv;
sls::context& ctx;

1
src/ast/sls/sls_bv_terms.cpp
View file

@ -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) {}

1
src/ast/sls/sls_bv_terms.h
View file

@ -29,7 +29,6 @@ Author:
namespace sls {
class bv_terms {
context& ctx;
ast_manager& m;
bv_util bv;
expr_ref_vector m_axioms;

1
src/ast/sls/sls_context.h
View file

@ -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<expr> m_subterms;

2
src/math/lp/CMakeLists.txt
View file

@ -43,6 +43,8 @@ z3_add_component(lp
polynomial
nlsat
smt_params
PYG_FILES
lp_params_helper.pyg
)
include_directories(${src_SOURCE_DIR})

6
src/math/lp/bound_analyzer_on_row.h
View file

@ -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<impq>::
// is_neg(a)? lower_bound: !lower_bound);
// }

4
src/math/lp/core_solver_pretty_printer_def.h
View file

@ -326,7 +326,7 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_g
if (m_squash_blanks && string_is_trivial(s))
continue;
int number_of_blanks = width - static_cast<unsigned>(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 <typename T, typename X> void core_solver_pretty_printer<T, X>::print_g
string rs = T_to_string(rst);
int nb = m_rs_width - static_cast<int>(rs.size());
lp_assert(nb >= 0);
SASSERT(nb >= 0);
print_blanks_local(nb + 1, m_out);
m_out << rs << std::endl;
}

2
src/math/lp/dense_matrix.h
View file

@ -47,7 +47,7 @@ public:
dense_matrix(unsigned m, unsigned n);
dense_matrix operator*=(matrix<T, X> 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++) {

2
src/math/lp/dense_matrix_def.h
View file

@ -175,7 +175,7 @@ template <typename T, typename X> void dense_matrix<T, X>::multiply_row_by_const
template <typename T, typename X>
dense_matrix<T, X> operator* (matrix<T, X> & a, matrix<T, X> & b){
lp_assert(a.column_count() == b.row_count());
SASSERT(a.column_count() == b.row_count());
dense_matrix<T, X> 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++) {

571
src/math/lp/dioph_eq.cpp
View file

@ -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<mpq> 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<iv> 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<unsigned, std_vector<unsigned>> 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<unsigned> m_ii_after_left;
// g_right[i] - the rumber of int infeasible after taking the i-ith
// right branch
std::vector<unsigned> m_ii_after_right;
double score() const {
double avm_lefts =
m_ii_after_left.size()
? static_cast<double>(std::accumulate(
m_ii_after_left.begin(), m_ii_after_left.end(), 0)) /
m_ii_after_left.size()
: std::numeric_limits<double>::infinity();
double avm_rights = m_ii_after_right.size()
? static_cast<double>(std::accumulate(
m_ii_after_right.begin(),
m_ii_after_right.end(), 0)) /
m_ii_after_right.size()
: std::numeric_limits<double>::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<unsigned> m_q;
indexed_uint_set m_in_q;
std::list<unsigned> m_q;
std::unordered_map<unsigned, std::list<unsigned>::iterator> m_positions;
bool empty() const {
return m_q.empty();
}
unsigned size() const {
return (unsigned)m_q.size();
return static_cast<unsigned>(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<const lar_term*> m_added_terms;
std::unordered_set<const lar_term*> m_active_terms;
std_vector<variable_branch_stats> m_branch_stats;
std_vector<branch> m_branch_stack;
std_vector<constraint_index> 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,16 +1012,29 @@ namespace lp {
}
}
void process_changed_columns(std_vector<unsigned> &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<unsigned> &f_vector) {
find_changed_terms_and_more_changed_rows();
for (unsigned j: m_changed_terms) {
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)) {
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
std_vector<unsigned> more_changed_rows;
@ -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<unsigned> & 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<size_t>::max();
unsigned num_candidates = 0;
std::vector<unsigned> 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))
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) {
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;
@ -1460,24 +1520,36 @@ 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) {
// 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<double>::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<unsigned, std::unordered_set<unsigned>> 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();
}

3
src/math/lp/dioph_eq.h
View file

@ -11,6 +11,7 @@ Abstract:
by Alberto Griggio(griggio@fbk.eu)
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
Revision History:
@ -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;
};
}

16
src/math/lp/general_matrix.h
View file

@ -98,16 +98,16 @@ public:
void clear() { m_data.clear(); }
bool row_is_initialized_correctly(const vector<mpq>& 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 <typename T>
void init_row_from_container(int i, const T & c, std::function<unsigned (unsigned)> 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<mpq> operator*(const vector<mpq> & x) const {
vector<mpq> 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);

16
src/math/lp/gomory.cpp
View file

@ -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))

50
src/math/lp/hnf.h
View file

@ -78,31 +78,31 @@ void extended_gcd_minimal_uv(const mpq & a, const mpq & b, mpq & d, mpq & u, mpq
k -= one_of_type<mpq>();
}
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<mpq>());
SASSERT(- a_over_d < v && v <= zero_of_type<mpq>());
if (is_pos(a)) {
u += (k + 1) * (b / d);
lp_assert( one_of_type<mpq>() <= u && u <= abs(b)/d);
SASSERT( one_of_type<mpq>() <= u && u <= abs(b)/d);
} else {
u -= (k + 1) * (b / d);
lp_assert( one_of_type<mpq>() <= -u && -u <= abs(b)/d);
SASSERT( one_of_type<mpq>() <= -u && -u <= abs(b)/d);
}
} else {
v = r; // v -= k * a_over_d;
lp_assert(- a_over_d < -v && -v <= zero_of_type<mpq>());
SASSERT(- a_over_d < -v && -v <= zero_of_type<mpq>());
if (is_pos(a)) {
u += k * (b / d);
lp_assert( one_of_type<mpq>() <= u && u <= abs(b)/d);
SASSERT( one_of_type<mpq>() <= u && u <= abs(b)/d);
} else {
u -= k * (b / d);
lp_assert( one_of_type<mpq>() <= -u && -u <= abs(b)/d);
SASSERT( one_of_type<mpq>() <= -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 <typename M>
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<mpq>();
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<mpq>();
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
}

6
src/math/lp/hnf_cutter.cpp
View file

@ -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<general_matrix> h(m_A, d);
vector<mpq> 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())

8
src/math/lp/incremental_vector.h
View file

@ -43,7 +43,7 @@ public:
template <typename T>
void pop_tail(vector<T> & 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];
}
};

2
src/math/lp/indexed_vector_def.h
View file

@ -39,7 +39,7 @@ void indexed_vector<T>::resize(unsigned data_size) {
template <typename T>
void indexed_vector<T>::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);
}

2
src/math/lp/int_branch.cpp
View file

@ -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;

4
src/math/lp/int_cube.cpp
View file

@ -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 {

33
src/math/lp/int_solver.cpp
View file

@ -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();

20
src/math/lp/lar_core_solver.h
View file

@ -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<unsigned>(- 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<unsigned>(- 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<mpq> const& l, numeric_pair<mpq> 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];

14
src/math/lp/lar_core_solver_def.h
View file

@ -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";);
}

151
src/math/lp/lar_solver.cpp
View file

@ -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<lconstraint_kind>((static_cast<int>(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<mpq>();
}
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<mpq>());
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<std::pair<mpq, unsigned>>& evidence) const {
std::unordered_map<lpvar, mpq> 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<mpq>());
case LE: SASSERT(rs < zero_of_type<mpq>());
break;
case LT: lp_assert(rs <= zero_of_type<mpq>());
case LT: SASSERT(rs <= zero_of_type<mpq>());
break;
case GE: lp_assert(rs > zero_of_type<mpq>());
case GE: SASSERT(rs > zero_of_type<mpq>());
break;
case GT: lp_assert(rs >= zero_of_type<mpq>());
case GT: SASSERT(rs >= zero_of_type<mpq>());
break;
case EQ: lp_assert(rs != zero_of_type<mpq>());
case EQ: SASSERT(rs != zero_of_type<mpq>());
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<constraint_index> 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<unsigned>(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<unsigned>(non_zero_column_cell_index) != i);
SASSERT(non_zero_column_cell_index != -1);
SASSERT(static_cast<unsigned>(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<int>(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<int>(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<mpq>();
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<mpq, lpvar>& 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";);

4
src/math/lp/lar_solver.h
View file

@ -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;

28
src/math/lp/lp_bound_propagator.h
View file

@ -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;;

22
src/math/lp/lp_core_solver_base.h
View file

@ -38,7 +38,7 @@ struct lpvar_lt {
typedef heap<lpvar_lt> lpvar_heap;
template <typename T, typename X>
X dot_product(const vector<T> & a, const vector<X> & b) {
lp_assert(a.size() == b.size());
SASSERT(a.size() == b.size());
auto r = zero_of_type<X>();
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<mpq> & 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<unsigned>(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;
}

20
src/math/lp/lp_core_solver_base_def.h
View file

@ -60,7 +60,7 @@ lp_core_solver_base(static_matrix<T, X> & 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<T, X> & A,
template <typename T, typename X> void lp_core_solver_base<T, X>::
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 <typename T, typename X> void lp_core_solver_base<T, X>::
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<unsigned>* non_basis_lis
for (unsigned j = 0; j < m_A.column_count(); j++)
if (m_basis_heading[j] >= 0)
lp_assert(static_cast<unsigned>(m_basis_heading[j]) < m_A.row_count() && m_basis[m_basis_heading[j]] == j);
SASSERT(static_cast<unsigned>(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 <typename T, typename X> bool lp_core_solver_base<T, X>::
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 <typename T, typename X> void lp_core_solver_base<T, X>::transpose_row
}
// entering is the new base column, leaving - the column leaving the basis
template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned entering, unsigned leaving, indexed_vector<T> & 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))

13
src/math/lp/lp_params_helper.pyg Normal file
View file

@ -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'),
))

38
src/math/lp/lp_primal_core_solver.h
View file

@ -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<T> &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<T> &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<X>())
theta = zero_of_type<X>();
@ -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<X>()) {
theta = zero_of_type<X>();
@ -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<unsigned>(this->m_basis_heading[j]);
for (const row_cell<T> &rc : this->m_A.m_rows[i]) {
unsigned k = rc.var();

8
src/math/lp/lp_primal_core_solver_def.h
View file

@ -179,7 +179,7 @@ lp_primal_core_solver<T, X>::get_bound_on_variable_and_update_leaving_precisely(
template <typename T, typename X> void lp_primal_core_solver<T, X>::check_Ax_equal_b() {
dense_matrix<T, X> d(this->m_A);
T * ls = d.apply_from_left_with_different_dims(this->m_x);
lp_assert(vectors_are_equal<T>(ls, this->m_b, this->m_m()));
SASSERT(vectors_are_equal<T>(ls, this->m_b, this->m_m()));
delete [] ls;
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::check_the_bounds() {
@ -189,8 +189,8 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::check_the
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::check_bound(unsigned i) {
lp_assert (!(this->column_has_lower_bound(i) && (numeric_traits<T>::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<T>::zero() > this->m_x[i])));
SASSERT (!(this->column_has_upper_bound(i) && (this->m_upper_bounds[i] < this->m_x[i])));
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::check_correctness() {
@ -231,7 +231,7 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::get_num
// calling it stage1 is too cryptic
template <typename T, typename X> void lp_primal_core_solver<T, X>::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();
}

28
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -30,7 +30,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::one_iteratio
else {
advance_on_entering_tableau(entering);
}
lp_assert(this->inf_heap_is_correct());
SASSERT(this->inf_heap_is_correct());
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_entering_tableau(int entering) {
@ -116,7 +116,7 @@ unsigned lp_primal_core_solver<T, X>::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<T, X>::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<T, X>::solve() {
}
template <typename T, typename X>void lp_primal_core_solver<T, X>::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<unsigned>(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 <typename T, typename X> int lp_primal_core_solver<T, X>::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<T>::is_zero(ed));
SASSERT(!numeric_traits<T>::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 <typename T, typename X> int lp_primal_core_solver<T, X>::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<T>::is_zero(ed));
SASSERT(!numeric_traits<T>::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 <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
return m_leaving_candidates[k];
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::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 <typename T, typename X> void lp_primal_core_solver<T, X>::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 <typename T, typename X> bool lp_primal_core_solver<T, X>::
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);

13
src/math/lp/lp_settings.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include "math/lp/lp_params_helper.hpp"
#include <memory>
#include "util/vector.h"
#include "smt/params/smt_params_helper.hpp"
@ -25,6 +26,7 @@ template bool lp::vectors_are_equal<lp::mpq>(vector<lp::mpq > const&, vector<lp:
void lp::lp_settings::updt_params(params_ref const& _p) {
smt_params_helper p(_p);
lp_params_helper lp_p(_p);
m_enable_hnf = p.arith_enable_hnf();
m_propagate_eqs = p.arith_propagate_eqs();
print_statistics = p.arith_print_stats();
@ -32,9 +34,12 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
report_frequency = p.arith_rep_freq();
m_simplex_strategy = static_cast<lp::simplex_strategy_enum>(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();
}

28
src/math/lp/lp_settings.h
View file

@ -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<unsigned> & 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<unsigned> & 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) {

1
src/math/lp/lp_utils.h
View file

@ -151,7 +151,6 @@ inline void throw_exception(std::string && str) {
}
typedef z3_exception exception;
#define lp_assert(_x_) { SASSERT(_x_); }
template <typename X> inline X zero_of_type() { return numeric_traits<X>::zero(); }
template <typename X> inline X one_of_type() { return numeric_traits<X>::one(); }
template <typename X> inline bool is_zero(const X & v) { return numeric_traits<X>::is_zero(v); }

2
src/math/lp/permutation_matrix.h
View file

@ -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);

4
src/math/lp/permutation_matrix_def.h
View file

@ -60,7 +60,7 @@ template <typename T, typename X> void permutation_matrix<T, X>::print(std::ostr
template <typename T, typename X> void permutation_matrix<T, X>::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 <typename T, typename X> void permutation_matrix<T, X>::transpose_from_
template <typename T, typename X> void permutation_matrix<T, X>::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);

14
src/math/lp/stacked_vector.h
View file

@ -38,7 +38,7 @@ public:
unsigned m_i;
public:
ref(stacked_vector<B> &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<B> &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 <typename T>
void pop_tail(svector<T> & 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];
}

16
src/math/lp/static_matrix.h
View file

@ -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<T> & y, unsigned j) const {
lp_assert(j < column_count());
SASSERT(j < column_count());
T ret = numeric_traits<T>::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<int> & 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<T>());
}
@ -382,7 +382,7 @@ public:
template <typename L>
L dot_product_with_row(unsigned row, const std_vector<L> & w) const {
L ret = zero_of_type<L>();
lp_assert(row < m_rows.size());
SASSERT(row < m_rows.size());
for (auto & it : m_rows[row]) {
ret += w[it.var()] * it.coeff();
}

2
src/math/lp/static_matrix_def.h
View file

@ -87,7 +87,7 @@ namespace lp {
template <typename T, typename X> void static_matrix<T, X>::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<unsigned>(rowk.size());

4
src/math/lp/test_bound_analyzer.h
View file

@ -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)

2
src/math/lp/var_register.h
View file

@ -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;
}

1
src/params/context_params.cpp
View file

@ -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");

1
src/qe/mbp/mbp_arrays_tg.cpp
View file

@ -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;

1
src/sat/CMakeLists.txt
View file

@ -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

335
src/sat/sat_elim_vars.cpp
View file

@ -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()]);
}
};

72
src/sat/sat_elim_vars.h
View file

@ -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<bool_var> 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
};
};

21
src/sat/sat_simplifier.cpp
View file

@ -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,25 +2072,20 @@ 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)) {
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++;
}
}
m_pos_cls.finalize();
m_neg_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();
}

2
src/sat/sat_simplifier_params.pyg
View file

@ -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'),

2
src/sat/smt/arith_solver.cpp
View file

@ -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());

1
src/sat/tactic/sat2goal.h
View file

@ -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;

4
src/smt/params/smt_params_helper.pyg
View file

@ -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'),

2
src/smt/theory_lra.cpp
View file

@ -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());
}

14
src/smt/theory_special_relations.cpp
View file

@ -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());

1
src/tactic/arith/fix_dl_var_tactic.cpp
View file

@ -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););

20
src/test/lp/gomory_test.h
View file

@ -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<mpq>() && f_0 < one_of_type<mpq>());
SASSERT(is_integer(x_j));
SASSERT(!a.is_int());
SASSERT(f_0 > zero_of_type<mpq>() && f_0 < one_of_type<mpq>());
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) {

93
src/test/lp/lp.cpp
View file

@ -384,7 +384,7 @@ vector<int> allocate_basis_heading(
void init_basic_part_of_basis_heading(vector<unsigned> &basis,
vector<int> &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<lp::mpq> c(0.1, 0.5);
a += 2 * c;
a -= c;
lp_assert(a == b + c);
SASSERT(a == b + c);
numeric_pair<lp::mpq> 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<lpvar, mpq> 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<mpq>(), ev));
// SASSERT(ev.size() == 4);
// SASSERT(contains_j_kind(x, GE, - one_of_type<mpq>(), 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,12 +1193,12 @@ 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)) &&
SASSERT((neg_inf || (0 <= x && x <= 100)) &&
(pos_inf || (0 <= y && y <= 100)));
}
@ -1628,7 +1629,7 @@ void test_maximize_term() {
solver.add_var_bound(term_x_min_y, LE, zero_of_type<mpq>());
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<lpvar, mpq> 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<std::pair<mpq, lpvar>> term_ls;
/* 3x1 + 3x2 + 14x3 − 7 */
/* 3x1 + 3x2 +```cpp
14x3 − 7 */
term_ls.push_back(std::pair<mpq, lpvar>(mpq(3), x1));
term_ls.push_back(std::pair<mpq, lpvar>(mpq(3), x2));
term_ls.push_back(std::pair<mpq, lpvar>(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

26
src/test/lp/smt_reader.h
View file

@ -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<lisp_elem> & 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;

1
src/util/params.h
View file

@ -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);

6
src/util/scoped_ctrl_c.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include <cstring>
#include <mutex>
#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);

8
src/util/scoped_timer.cpp
View file

@ -48,7 +48,6 @@ struct scoped_timer_state {
static std::vector<scoped_timer_state*> available_workers;
static std::mutex workers;
static atomic<unsigned> 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,8 +129,6 @@ 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;
@ -143,13 +139,9 @@ void scoped_timer::finalize() {
workers.unlock();
for (auto w : cleanup_workers) {
++deleted;
w->m_thread.join();
delete w;
}
}
num_workers = 0;
available_workers.clear();
}
void scoped_timer::init_state(unsigned ms, event_handler * eh) {