diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml new file mode 100644 index 000000000..843b1c75e --- /dev/null +++ b/.github/workflows/docker-image.yml @@ -0,0 +1,61 @@ +name: Publish Docker image + +on: + schedule: + - cron: "0 1 * * 0" # every Sunday at 1 am + workflow_dispatch: # on button click + +jobs: + push_to_registry: + name: Push Docker image to GitHub Docker registry + runs-on: ubuntu-latest + + steps: + - name: Check out the repo + uses: actions/checkout@v2 + + - name: Log in to GitHub Docker registry + uses: docker/login-action@v1 + with: + registry: ghcr.io + username: ${{ secrets.DOCKER_USERNAME }} + password: ${{ secrets.DOCKER_PASSWORD }} + + # ------- + # BARE Z3 + # ------- + - name: Extract metadata (tags, labels) for Bare Z3 Docker Image + id: meta + uses: docker/metadata-action@v3 + with: + images: ghcr.io/z3prover/z3 + flavor: | + latest=auto + prefix=ubuntu-20.04-bare-z3- + tags: | + type=schedule,pattern={{date 'YYYYMMDD'}} + type=ref,event=tag + type=edge + type=sha,prefix=ubuntu-20.04-bare-z3-sha- + - name: Build and push Bare Z3 Docker Image + uses: docker/build-push-action@v2.7.0 + with: + context: . + push: true + target: bare-z3 + file: ./docker/ubuntu-20-04.Dockerfile + tags: ${{ steps.meta.outputs.tags }} + labels: ${{ steps.meta.outputs.labels }} + + # ------------------------------ + # Repo description on GHCR + # ------------------------------ +# - name: Update repo description +# uses: peter-evans/dockerhub-description@v2 +# with: +# registry: ghcr.io +# repository: z3prover/z3 +# username: ${{ secrets.DOCKER_USERNAME }} +# password: ${{ secrets.DOCKER_PASSWORD }} +# short-description: ${{ github.event.repository.description }} +# readme-filepath: ./docker/README.md diff --git a/CMakeLists.txt b/CMakeLists.txt index f1ad74181..be300607d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.8.14.0 LANGUAGES CXX) +project(Z3 VERSION 4.8.15.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/README.md b/README.md index 5c5af803b..3cd3478be 100644 --- a/README.md +++ b/README.md @@ -14,10 +14,12 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z ## Build status -| Azure Pipelines | Code Coverage | Open Bugs | Android Build | WASM Build | +| Azure Pipelines | Code Coverage | Open Bugs | Android Build | WASM 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) | [![CodeCoverage](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml) | [![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) | +Docker image. + [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang [3]: #building-z3-using-cmake diff --git a/azure-pipelines.yml b/azure-pipelines.yml index ea894a93a..bff70c859 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -288,6 +288,7 @@ jobs: - job: "MacOSOCaml" displayName: "MacOS build with OCaml" + condition: eq(0,1) pool: vmImage: "macOS-latest" steps: @@ -310,9 +311,9 @@ jobs: eval `opam config env` make -j3 make -j3 _ex_ml_example_post_install - ./ml_example_shared.byte - ./ml_example_shared_custom.byte - ./ml_example_shared + # ./ml_example_shared.byte + # ./ml_example_shared_custom.byte + # ./ml_example_shared cd .. # Skip as dead-slow in debug mode: # - template: scripts/test-z3.yml diff --git a/docker/ubuntu-20-04.Dockerfile b/docker/ubuntu-20-04.Dockerfile new file mode 100644 index 000000000..6a37d05c0 --- /dev/null +++ b/docker/ubuntu-20-04.Dockerfile @@ -0,0 +1,45 @@ +# ------------- +# OS Base image +# ------------- +# >> Includes system-wide dependencies +FROM ubuntu:20.04 as lib-base +ARG DEBIAN_FRONTEND=noninteractive +RUN apt-get update && \ + apt-get -y --no-install-recommends install \ + cmake \ + make \ + clang \ + g++ \ + curl \ + default-jdk \ + python3 \ + python3-setuptools \ + python-is-python3 \ + sudo + +# ---------------- +# Z3 Builder Image +# ---------------- +# >> Includes build files and compiles the basic z3 sources +FROM lib-base as builder +COPY ./ /z3-source/ +WORKDIR /z3-source/ +RUN python scripts/mk_make.py +WORKDIR /z3-source/build/ +RUN make +RUN sudo make install +WORKDIR /z3-source/ + +# ------- +# Bare z3 +# ------- +# >> Includes only stnadard z3 installations. +# >> Can be used as a standalone interface to z3. +FROM builder as bare-z3 +ENTRYPOINT [ "z3" ] + +# TODO: introduce Python-binding stage +# ... + +# TODO(optional): introduce C/C++ -binding stage +# ... diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 69b67abc9..1143110aa 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -65,7 +65,7 @@ def unpack(packages, symbols): mk_dir(f"out/runtimes/{dst}/native") replace(f"{tmp}/{package_dir}/bin/libz3.{ext}", f"out/runtimes/{dst}/native/libz3.{ext}") if "x64-win" in f: - mk_dir("out/lib/netstandard1.4/") + mk_dir("out/lib/netstandard2.0/") if symbols: zip_ref.extract(f"{package_dir}/bin/libz3.pdb", f"{tmp}") replace(f"{tmp}/{package_dir}/bin/libz3.pdb", f"out/runtimes/{dst}/native/libz3.pdb") @@ -74,7 +74,7 @@ def unpack(packages, symbols): files += ["Microsoft.Z3.pdb", "Microsoft.Z3.xml"] for b in files: zip_ref.extract(f"{package_dir}/bin/{b}", f"{tmp}") - replace(f"{tmp}/{package_dir}/bin/{b}", f"out/lib/netstandard1.4/{b}") + replace(f"{tmp}/{package_dir}/bin/{b}", f"out/lib/netstandard2.0/{b}") def mk_targets(source_root): mk_dir("out/build") @@ -107,7 +107,7 @@ Linux Dependencies: true en - + """.format(version, repo, branch, commit) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 105c097d4..17a76060a 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 8, 14, 0) + set_version(4, 8, 15, 0) # Z3 Project definition def init_project_def(): diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e6d34dc3e..042e6af46 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -15,7 +15,7 @@ import shutil from mk_exception import * import mk_genfile_common from fnmatch import fnmatch -import distutils.sysconfig +import sysconfig import compileall import subprocess @@ -48,7 +48,7 @@ CXX_COMPILERS=['g++', 'clang++'] C_COMPILERS=['gcc', 'clang'] JAVAC=None JAR=None -PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib(prefix=getenv("PREFIX", None)) +PYTHON_PACKAGE_DIR=sysconfig.get_path('purelib') BUILD_DIR='build' REV_BUILD_DIR='..' SRC_DIR='src' @@ -92,7 +92,6 @@ DOTNET_CORE_ENABLED=False DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None) JAVA_ENABLED=False ML_ENABLED=False -JS_ENABLED=False PYTHON_INSTALL_ENABLED=False STATIC_LIB=False STATIC_BIN=False @@ -681,7 +680,7 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED + global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED global GUARD_CF, ALWAYS_DYNAMIC_BASE try: @@ -749,8 +748,6 @@ def parse_options(): GIT_DESCRIBE = True elif opt in ('', '--ml'): ML_ENABLED = True - elif opt == "--js": - JS_ENABLED = True elif opt in ('', '--log-sync'): LOG_SYNC = True elif opt == '--single-threaded': @@ -813,16 +810,6 @@ def set_build_dir(d): BUILD_DIR = norm_path(d) REV_BUILD_DIR = reverse_path(d) -def set_z3js_dir(p): - global SRC_DIR, Z3JS_SRC_DIR - p = norm_path(p) - full = os.path.join(SRC_DIR, p) - if not os.path.exists(full): - raise MKException("Python bindings directory '%s' does not exist" % full) - Z3JS_SRC_DIR = full - if VERBOSE: - print("Js bindings directory was detected.") - def set_z3py_dir(p): global SRC_DIR, Z3PY_SRC_DIR p = norm_path(p) @@ -858,9 +845,6 @@ def get_components(): def get_z3py_dir(): return Z3PY_SRC_DIR -# Return directory where the js bindings are located -def get_z3js_dir(): - return Z3JS_SRC_DIR # Return true if in verbose mode def is_verbose(): @@ -872,9 +856,6 @@ def is_java_enabled(): def is_ml_enabled(): return ML_ENABLED -def is_js_enabled(): - return JS_ENABLED - def is_dotnet_core_enabled(): return DOTNET_CORE_ENABLED @@ -1611,7 +1592,7 @@ class PythonInstallComponent(Component): os.path.join(self.pythonPkgDir,'z3'), in_prefix=self.in_prefix_install) - if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): + if PYTHON_PACKAGE_DIR != sysconfig.get_path('purelib'): out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) def mk_uninstall(self, out): @@ -2692,7 +2673,7 @@ def mk_config(): print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR) if GPROF: print('gprof: enabled') - print('Python version: %s' % distutils.sysconfig.get_python_version()) + print('Python version: %s' % sysconfig.get_python_version()) if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) @@ -3025,17 +3006,14 @@ def mk_bindings(api_files): ml_output_dir = None if is_ml_enabled(): ml_output_dir = get_component('ml').src_dir - if is_js_enabled(): - set_z3js_dir("api/js") - js_output_dir = get_component('js').src_dir # Get the update_api module to do the work for us + update_api.VERBOSE = is_verbose() update_api.generate_files(api_files=new_api_files, api_output_dir=get_component('api').src_dir, z3py_output_dir=get_z3py_dir(), dotnet_output_dir=dotnet_output_dir, java_output_dir=java_output_dir, java_package_name=java_package_name, - js_output_dir=get_z3js_dir(), ml_output_dir=ml_output_dir, ml_src_dir=ml_output_dir ) diff --git a/scripts/release.yml b/scripts/release.yml index fc026abb6..c4ff7e07a 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -171,6 +171,7 @@ stages: inputs: artifact: 'WindowsBuild-x64' path: $(Agent.TempDirectory)\package + - task: DownloadPipelineArtifact@2 displayName: 'Download Win32 Build' inputs: artifact: 'WindowsBuild-x86' @@ -313,7 +314,7 @@ stages: jobs: - job: GitHubPublish - condition: eq(0,1) + condition: eq(1,1) displayName: "Publish to GitHub" pool: vmImage: "windows-latest" diff --git a/scripts/update_api.py b/scripts/update_api.py index 6392e439e..2daf0a7a7 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -15,7 +15,7 @@ several API header files. It can also optionally emit some of the files required for Z3's different language bindings. """ -import mk_util + import mk_exception import argparse import logging @@ -23,6 +23,10 @@ import re import os import sys +VERBOSE = True +def is_verbose(): + return VERBOSE + ########################################################## # TODO: rewrite this file without using global variables. # This file is a big HACK. @@ -78,42 +82,44 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'byte', SYMBOL : 'IntPtr', PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char', CHAR_PTR : 'IntPtr' } -# Mapping to Java types -Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double', - FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr', - BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'long' } - -Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble', - FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject', - BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar', CHAR_PTR : 'jlong'} # Mapping to ML types Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**', BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string' } -next_type_id = FIRST_OBJ_ID +class APITypes: + def __init__(self): + self.next_type_id = FIRST_OBJ_ID -def def_Type(var, c_type, py_type): - global next_type_id - exec('%s = %s' % (var, next_type_id), globals()) - Type2Str[next_type_id] = c_type - Type2PyStr[next_type_id] = py_type - next_type_id = next_type_id + 1 - -def def_Types(api_files): - pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") - for api_file in api_files: - api = open(api_file, 'r') - for line in api: - m = pat1.match(line) - if m: - def_Type(m.group(1), m.group(2), m.group(3)) - for k in Type2Str: - v = Type2Str[k] - if is_obj(k): - Type2Dotnet[k] = v - Type2ML[k] = v.lower() + def def_Type(self, var, c_type, py_type): + """Process type definitions of the form def_Type(var, c_type, py_type) + The variable 'var' is set to a unique number and recorded globally using exec + It is used by 'def_APIs' to that uses the unique numbers to access the + corresponding C and Python types. + """ + id = self.next_type_id + exec('%s = %s' % (var, id), globals()) + Type2Str[id] = c_type + Type2PyStr[id] = py_type + self.next_type_id += 1 + + def def_Types(self, api_files): + pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") + for api_file in api_files: + with open(api_file, 'r') as api: + for line in api: + m = pat1.match(line) + if m: + self.def_Type(m.group(1), m.group(2), m.group(3)) + # + # Populate object type entries in dotnet and ML bindings. + # + for k in Type2Str: + v = Type2Str[k] + if is_obj(k): + Type2Dotnet[k] = v + Type2ML[k] = v.lower() def type2str(ty): global Type2Str @@ -127,20 +133,6 @@ def type2dotnet(ty): global Type2Dotnet return Type2Dotnet[ty] -def type2java(ty): - global Type2Java - if (ty >= FIRST_OBJ_ID): - return 'long' - else: - return Type2Java[ty] - -def type2javaw(ty): - global Type2JavaW - if (ty >= FIRST_OBJ_ID): - return 'jlong' - else: - return Type2JavaW[ty] - def type2ml(ty): global Type2ML q = Type2ML[ty] @@ -214,42 +206,8 @@ def param2dotnet(p): else: return type2dotnet(param_type(p)) -def param2java(p): - k = param_kind(p) - if k == OUT: - if param_type(p) == INT or param_type(p) == UINT: - return "IntPtr" - elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) == VOID_PTR or param_type(p) >= FIRST_OBJ_ID: - return "LongPtr" - elif param_type(p) == STRING: - return "StringPtr" - else: - print("ERROR: unreachable code") - assert(False) - exit(1) - elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: - return "%s[]" % type2java(param_type(p)) - elif k == OUT_MANAGED_ARRAY: - if param_type(p) == UINT: - return "UIntArrayPtr" - else: - return "ObjArrayPtr" - else: - return type2java(param_type(p)) -def param2javaw(p): - k = param_kind(p) - if k == OUT: - return "jobject" - elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: - if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL: - return "jintArray" - else: - return "jlongArray" - elif k == OUT_MANAGED_ARRAY: - return "jlong" - else: - return type2javaw(param_type(p)) +# -------------- def param2pystr(p): if param_kind(p) == IN_ARRAY or param_kind(p) == OUT_ARRAY or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT: @@ -257,6 +215,9 @@ def param2pystr(p): else: return type2pystr(param_type(p)) +# -------------- +# ML + def param2ml(p): k = param_kind(p) if k == OUT: @@ -507,6 +468,68 @@ def mk_dotnet_wrappers(dotnet): dotnet.write(" }\n\n") dotnet.write("}\n\n") +# ---------------------- +# Java + +Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double', + FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr', + BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'long' } + +Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble', + FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject', + BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar', CHAR_PTR : 'jlong'} + +def type2java(ty): + global Type2Java + if (ty >= FIRST_OBJ_ID): + return 'long' + else: + return Type2Java[ty] + +def type2javaw(ty): + global Type2JavaW + if (ty >= FIRST_OBJ_ID): + return 'jlong' + else: + return Type2JavaW[ty] + +def param2java(p): + k = param_kind(p) + if k == OUT: + if param_type(p) == INT or param_type(p) == UINT: + return "IntPtr" + elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) == VOID_PTR or param_type(p) >= FIRST_OBJ_ID: + return "LongPtr" + elif param_type(p) == STRING: + return "StringPtr" + else: + print("ERROR: unreachable code") + assert(False) + exit(1) + elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: + return "%s[]" % type2java(param_type(p)) + elif k == OUT_MANAGED_ARRAY: + if param_type(p) == UINT: + return "UIntArrayPtr" + else: + return "ObjArrayPtr" + else: + return type2java(param_type(p)) + +def param2javaw(p): + k = param_kind(p) + if k == OUT: + return "jobject" + elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: + if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL: + return "jintArray" + else: + return "jlongArray" + elif k == OUT_MANAGED_ARRAY: + return "jlong" + else: + return type2javaw(param_type(p)) + def java_method_name(name): result = '' name = name[3:] # Remove Z3_ @@ -776,62 +799,9 @@ def mk_java(java_dir, package_name): java_wrapper.write('#ifdef __cplusplus\n') java_wrapper.write('}\n') java_wrapper.write('#endif\n') - if mk_util.is_verbose(): + if is_verbose(): print("Generated '%s'" % java_nativef) - -Type2Napi = { VOID : '', VOID_PTR : '', INT : 'number', UINT : 'number', INT64 : 'number', UINT64 : 'number', DOUBLE : 'number', - FLOAT : 'number', STRING : 'string', STRING_PTR : 'array', - BOOL : 'number', SYMBOL : 'external', PRINT_MODE : 'number', ERROR_CODE : 'number', CHAR : 'number' } - -def type2napi(t): - try: - return Type2Napi[t] - except: - return "external" - -Type2NapiBuilder = { VOID : '', VOID_PTR : '', INT : 'int32', UINT : 'uint32', INT64 : 'int64', UINT64 : 'uint64', DOUBLE : 'double', - FLOAT : 'float', STRING : 'string', STRING_PTR : 'array', - BOOL : 'bool', SYMBOL : 'external', PRINT_MODE : 'int32', ERROR_CODE : 'int32', CHAR : 'char' } - -def type2napibuilder(t): - try: - return Type2NapiBuilder[t] - except: - return "external" - - -def mk_js(js_output_dir): - with open(os.path.join(js_output_dir, "z3.json"), 'w') as ous: - ous.write("{\n") - ous.write(" \"api\": [\n") - for name, result, params in _dotnet_decls: - ous.write(" {\n") - ous.write(" \"name\": \"%s\",\n" % name) - ous.write(" \"c_type\": \"%s\",\n" % Type2Str[result]) - ous.write(" \"napi_type\": \"%s\",\n" % type2napi(result)) - ous.write(" \"arg_list\": [") - first = True - for p in params: - if first: - first = False - ous.write("\n {\n") - else: - ous.write(",\n {\n") - t = param_type(p) - k = t - ous.write(" \"name\": \"%s\",\n" % "") # TBD - ous.write(" \"c_type\": \"%s\",\n" % type2str(t)) - ous.write(" \"napi_type\": \"%s\",\n" % type2napi(t)) - ous.write(" \"napi_builder\": \"%s\"\n" % type2napibuilder(t)) - ous.write( " }") - ous.write("],\n") - ous.write(" \"napi_builder\": \"%s\"\n" % type2napibuilder(result)) - ous.write(" },\n") - ous.write(" ]\n") - ous.write("}\n") - - def mk_log_header(file, name, params): file.write("void log_%s(" % name) i = 0 @@ -842,6 +812,10 @@ def mk_log_header(file, name, params): i = i + 1 file.write(")") +# --------------------------------- +# Logging + + def log_param(p): kind = param_kind(p) ty = param_type(p) @@ -1364,7 +1338,7 @@ def mk_ml(ml_src_dir, ml_output_dir): ml_native.write('(**/**)\n') ml_native.close() - if mk_util.is_verbose(): + if is_verbose(): print ('Generated "%s"' % ml_nativef) mk_z3native_stubs_c(ml_src_dir, ml_output_dir) @@ -1689,7 +1663,7 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface ml_wrapper.write('}\n') ml_wrapper.write('#endif\n') - if mk_util.is_verbose(): + if is_verbose(): print ('Generated "%s"' % ml_wrapperf) # Collect API(...) commands from @@ -1889,7 +1863,6 @@ def generate_files(api_files, dotnet_output_dir=None, java_output_dir=None, java_package_name=None, - js_output_dir=None, ml_output_dir=None, ml_src_dir=None): """ @@ -1933,6 +1906,7 @@ def generate_files(api_files, import tempfile return tempfile.TemporaryFile(mode=mode) + apiTypes = APITypes() with mk_file_or_temp(api_output_dir, 'api_log_macros.h') as log_h: with mk_file_or_temp(api_output_dir, 'api_log_macros.cpp') as log_c: with mk_file_or_temp(api_output_dir, 'api_commands.cpp') as exe_c: @@ -1944,13 +1918,13 @@ def generate_files(api_files, write_core_py_preamble(core_py) # FIXME: these functions are awful - def_Types(api_files) + apiTypes.def_Types(api_files) def_APIs(api_files) mk_bindings(exe_c) mk_py_wrappers() write_core_py_post(core_py) - if mk_util.is_verbose(): + if is_verbose(): print("Generated '{}'".format(log_h.name)) print("Generated '{}'".format(log_c.name)) print("Generated '{}'".format(exe_c.name)) @@ -1960,7 +1934,7 @@ def generate_files(api_files, with open(os.path.join(dotnet_output_dir, 'Native.cs'), 'w') as dotnet_file: mk_dotnet(dotnet_file) mk_dotnet_wrappers(dotnet_file) - if mk_util.is_verbose(): + if is_verbose(): print("Generated '{}'".format(dotnet_file.name)) if java_output_dir: @@ -1970,8 +1944,6 @@ def generate_files(api_files, assert not ml_src_dir is None mk_ml(ml_src_dir, ml_output_dir) - if js_output_dir: - mk_js(js_output_dir) def main(args): logging.basicConfig(level=logging.INFO) @@ -2006,10 +1978,6 @@ def main(args): dest="ml_output_dir", default=None, help="Directory to emit OCaml files. If not specified no files are emitted.") - parser.add_argument("--js_output_dir", - dest="js_output_dir", - default=None, - help="Directory to emit js bindings. If not specified no files are emitted.") pargs = parser.parse_args(args) if pargs.java_output_dir: @@ -2033,7 +2001,6 @@ def main(args): dotnet_output_dir=pargs.dotnet_output_dir, java_output_dir=pargs.java_output_dir, java_package_name=pargs.java_package_name, - js_output_dir=pargs.js_output_dir, ml_output_dir=pargs.ml_output_dir, ml_src_dir=pargs.ml_src_dir) return 0 diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index fd7c94f22..1b551bd73 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -47,7 +47,7 @@ extern "C" { env_params::updt_params(); } - Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) { + Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) { memory::initialize(UINT_MAX); LOG_Z3_global_param_get(param_id, param_value); *param_value = nullptr; diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 3a6e8e56f..8c6227d7d 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -585,7 +585,7 @@ extern "C" { to_fixedpoint_ref(d)->collect_param_descrs(descrs); to_params(p)->m_params.validate(descrs); to_fixedpoint_ref(d)->updt_params(to_param_ref(p)); - to_fixedpoint(d)->m_params = to_param_ref(p); + to_fixedpoint(d)->m_params.append(to_param_ref(p)); Z3_CATCH; } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 7ac4eacdc..2c8505f27 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -701,6 +701,9 @@ namespace z3 { sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); } friend std::ostream & operator<<(std::ostream & out, sort const & s) { return out << Z3_sort_to_string(s.ctx(), Z3_sort(s.m_ast)); } + + func_decl_vector constructors(); + func_decl_vector recognizers(); }; /** @@ -741,6 +744,9 @@ namespace z3 { expr operator()(expr const & a1, expr const & a2, expr const & a3) const; expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const; expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const; + + func_decl_vector accessors(); + }; /** @@ -3863,6 +3869,42 @@ namespace z3 { return expr_vector(*this, r); } + inline func_decl_vector sort::constructors() { + assert(is_datatype()); + func_decl_vector cs(ctx()); + unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this); + for (unsigned i = 0; i < n; ++i) + cs.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor(ctx(), *this, i))); + return cs; + } + + inline func_decl_vector sort::recognizers() { + assert(is_datatype()); + func_decl_vector rs(ctx()); + unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this); + for (unsigned i = 0; i < n; ++i) + rs.push_back(func_decl(ctx(), Z3_get_datatype_sort_recognizer(ctx(), *this, i))); + return rs; + } + + inline func_decl_vector func_decl::accessors() { + sort s = range(); + assert(s.is_datatype()); + unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s); + unsigned idx = 0; + for (; idx < n; ++idx) { + func_decl f(ctx(), Z3_get_datatype_sort_constructor(ctx(), s, idx)); + if (id() == f.id()) + break; + } + assert(idx < n); + n = arity(); + func_decl_vector as(ctx()); + for (unsigned i = 0; i < n; ++i) + as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i))); + return as; + } + inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) { assert(src.size() == dst.size()); diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 98d4b9503..bab8ac982 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -18,8 +18,6 @@ add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency - "${PROJECT_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating ${Z3_DOTNET_NATIVE_FILE}" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 1448a9ea5..b904937a9 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -203,7 +203,7 @@ end = struct let equal = (=) (* The standard comparison uses the custom operations of the C layer *) - let compare = Pervasives.compare + let compare = Stdlib.compare let translate (x:ast) (to_ctx:context) = if gc x = to_ctx then diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 8e50ad255..e791a2f11 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -99,7 +99,7 @@ if (Z3_INSTALL_PYTHON_BINDINGS) message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR not set. Trying to guess") execute_process( COMMAND "${PYTHON_EXECUTABLE}" "-c" - "import distutils.sysconfig; print(distutils.sysconfig.get_python_lib())" + "import sysconfig; print(sysconfig.get_path('purelib'))" RESULT_VARIABLE exit_code OUTPUT_VARIABLE CMAKE_INSTALL_PYTHON_PKG_DIR OUTPUT_STRIP_TRAILING_WHITESPACE diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a11061970..2b0286608 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8789,6 +8789,10 @@ def Product(*args): _args, sz = _to_ast_array(args) return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx) +def Abs(arg): + """Create the absolute value of an arithmetic expression""" + return If(arg > 0, arg, -arg) + def AtMost(*args): """Create an at-most Pseudo-Boolean k constraint. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index d5bd1e11c..3f964adc6 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1516,7 +1516,7 @@ extern "C" { def_API('Z3_global_param_get', BOOL, (_in(STRING), _out(STRING))) */ - Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value); + Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value); /**@}*/ @@ -4325,7 +4325,7 @@ extern "C" { def_API('Z3_get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64))) */ - Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r); + Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r); /** \brief Return the domain of the given array sort. @@ -5264,7 +5264,7 @@ extern "C" { def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST))) */ - Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v); + Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v); /** \brief Return the interpretation (i.e., assignment) of constant \c a in the model \c m. diff --git a/src/api/z3_macros.h b/src/api/z3_macros.h index d1ac18804..d42eb508a 100644 --- a/src/api/z3_macros.h +++ b/src/api/z3_macros.h @@ -4,9 +4,6 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#ifndef Z3_bool_opt -#define Z3_bool_opt Z3_bool -#endif #ifndef Z3_API # ifdef __GNUC__ diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 399aa76f2..d229865ad 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -273,6 +273,17 @@ public: bool is_rem0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_REM0); } bool is_mod0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_MOD0); } bool is_power0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER0); } + bool is_power(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER); } + bool is_add(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_ADD); } + bool is_mul(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MUL); } + bool is_sub(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_SUB); } + bool is_uminus(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_UMINUS); } + bool is_div(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_DIV); } + bool is_rem(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_REM); } + bool is_mod(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MOD); } + bool is_to_real(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_REAL); } + bool is_to_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_INT); } + bool is_is_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_IS_INT); } bool is_add(expr const * n) const { return is_app_of(n, arith_family_id, OP_ADD); } bool is_sub(expr const * n) const { return is_app_of(n, arith_family_id, OP_SUB); } diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index f986eb46a..0800b6af3 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -150,6 +150,10 @@ public: bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); } bool is_ext(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_EXT); } bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); } + bool is_union(expr* n) const { return is_app_of(n, m_fid, OP_SET_UNION); } + bool is_intersect(expr* n) const { return is_app_of(n, m_fid, OP_SET_INTERSECT); } + bool is_difference(expr* n) const { return is_app_of(n, m_fid, OP_SET_DIFFERENCE); } + bool is_complement(expr* n) const { return is_app_of(n, m_fid, OP_SET_COMPLEMENT); } bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); } bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); } bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); } @@ -158,11 +162,14 @@ public: bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); } bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); } bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); } + bool is_union(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_UNION); } + bool is_intersect(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_INTERSECT); } bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); } bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); } bool is_set_card(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_CARD); } bool is_default(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_DEFAULT); } bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); } + bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_SET_SUBSET); } bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); } func_decl * get_as_array_func_decl(expr * n) const; func_decl * get_as_array_func_decl(func_decl* f) const; @@ -172,6 +179,8 @@ public: bool is_const(expr* e, expr*& v) const; bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value); + + MATCH_BINARY(is_subset); }; class array_util : public array_recognizers { diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 69b63af0f..090a2ff9d 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -264,8 +264,12 @@ void flatten_and(expr_ref_vector& result) { expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++i) { expr* e = result.get(i); - if (seen.is_marked(e)) + if (seen.is_marked(e)) { + result[i] = result.back(); + result.pop_back(); + --i; continue; + } seen.mark(e); pin.push_back(e); if (m.is_and(e)) { @@ -330,8 +334,12 @@ void flatten_or(expr_ref_vector& result) { expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++i) { expr* e = result.get(i); - if (seen.is_marked(e)) + if (seen.is_marked(e)) { + result[i] = result.back(); + result.pop_back(); + --i; continue; + } seen.mark(e); pin.push_back(e); if (m.is_or(e)) { diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 1f8e14565..8a3a4e002 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -25,6 +25,8 @@ namespace euf { enode* egraph::mk_enode(expr* f, unsigned generation, unsigned num_args, enode * const* args) { enode* n = enode::mk(m_region, f, generation, num_args, args); + if (m_default_relevant) + n->set_relevant(true); m_nodes.push_back(n); m_exprs.push_back(f); if (is_app(f) && num_args > 0) { @@ -187,10 +189,10 @@ namespace euf { add_th_diseq(id, v1, v2, n->get_expr()); return; } - for (auto p : euf::enode_th_vars(r1)) { + for (auto const& p : euf::enode_th_vars(r1)) { if (!th_propagates_diseqs(p.get_id())) continue; - for (auto q : euf::enode_th_vars(r2)) + for (auto const& q : euf::enode_th_vars(r2)) if (p.get_id() == q.get_id()) add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n->get_expr()); } @@ -269,6 +271,13 @@ namespace euf { } } + void egraph::set_relevant(enode* n) { + if (n->is_relevant()) + return; + n->set_relevant(true); + m_updates.push_back(update_record(n, update_record::set_relevant())); + } + void egraph::toggle_merge_enabled(enode* n, bool backtracking) { bool enable_merge = !n->merge_enabled(); n->set_merge_enabled(enable_merge); @@ -380,6 +389,10 @@ namespace euf { case update_record::tag_t::is_lbl_set: p.r1->m_lbls.set(p.m_lbls); break; + case update_record::tag_t::is_set_relevant: + SASSERT(p.r1->is_relevant()); + p.r1->set_relevant(false); + break; case update_record::tag_t::is_update_children: for (unsigned i = 0; i < p.r1->num_args(); ++i) { SASSERT(p.r1->m_args[i]->get_root()->m_parents.back() == p.r1); @@ -446,8 +459,8 @@ namespace euf { r2->inc_class_size(r1->class_size()); merge_th_eq(r1, r2); reinsert_parents(r1, r2); - if (m_on_merge) - m_on_merge(r2, r1); + for (auto& cb : m_on_merge) + cb(r2, r1); } void egraph::remove_parents(enode* r1, enode* r2) { @@ -493,7 +506,7 @@ namespace euf { void egraph::merge_th_eq(enode* n, enode* root) { SASSERT(n != root); - for (auto iv : enode_th_vars(n)) { + for (auto const& iv : enode_th_vars(n)) { theory_id id = iv.get_id(); theory_var v = root->get_th_var(id); if (v == null_theory_var) { @@ -754,6 +767,8 @@ namespace euf { } std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const { + if (!n->is_relevant()) + out << "n"; out << "#" << n->get_expr_id() << " := "; expr* f = n->get_expr(); if (is_app(f)) @@ -770,11 +785,18 @@ namespace euf { out << " " << p->get_expr_id(); out << "] "; } - if (n->value() != l_undef) - out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << (n->merge_tf()?"":" no merge") << "] "; + auto value_of = [&]() { + switch (n->value()) { + case l_true: return "T"; + case l_false: return "F"; + default: return "?"; + } + }; + if (n->bool_var() != sat::null_bool_var) + out << "[b" << n->bool_var() << " := " << value_of() << (n->merge_tf() ? "" : " no merge") << "] "; if (n->has_th_vars()) { out << "[t"; - for (auto v : enode_th_vars(n)) + for (auto const& v : enode_th_vars(n)) out << " " << v.get_id() << ":" << v.get_var(); out << "] "; } diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 7c1f9e566..a91dbf4a4 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -32,6 +32,7 @@ Notes: #include "ast/euf/euf_enode.h" #include "ast/euf/euf_etable.h" #include "ast/ast_ll_pp.h" +#include namespace euf { @@ -105,10 +106,11 @@ namespace euf { struct lbl_hash {}; struct lbl_set {}; struct update_children {}; + struct set_relevant {}; enum class tag_t { is_set_parent, is_add_node, is_toggle_merge, is_update_children, is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq, is_lbl_hash, is_new_th_eq_qhead, is_new_lits_qhead, - is_inconsistent, is_value_assignment, is_lbl_set }; + is_inconsistent, is_value_assignment, is_lbl_set, is_set_relevant }; tag_t tag; enode* r1; enode* n1; @@ -151,6 +153,8 @@ namespace euf { tag(tag_t::is_lbl_set), r1(n), n1(nullptr), m_lbls(n->m_lbls.get()) {} update_record(enode* n, update_children) : tag(tag_t::is_update_children), r1(n), n1(nullptr), r2_num_parents(UINT_MAX) {} + update_record(enode* n, set_relevant) : + tag(tag_t::is_set_relevant), r1(n), n1(nullptr), r2_num_parents(UINT_MAX) {} }; ast_manager& m; svector m_to_merge; @@ -181,7 +185,8 @@ namespace euf { enode_vector m_todo; stats m_stats; bool m_uses_congruence = false; - std::function m_on_merge; + bool m_default_relevant = true; + std::vector> m_on_merge; std::function m_on_make; std::function m_used_eq; std::function m_used_cc; @@ -292,8 +297,10 @@ namespace euf { void set_merge_enabled(enode* n, bool enable_merge); void set_value(enode* n, lbool value); void set_bool_var(enode* n, unsigned v) { n->set_bool_var(v); } + void set_relevant(enode* n); + void set_default_relevant(bool b) { m_default_relevant = b; } - void set_on_merge(std::function& on_merge) { m_on_merge = on_merge; } + void set_on_merge(std::function& on_merge) { m_on_merge.push_back(on_merge); } void set_on_make(std::function& on_make) { m_on_make = on_make; } void set_used_eq(std::function& used_eq) { m_used_eq = used_eq; } void set_used_cc(std::function& used_cc) { m_used_cc = used_cc; } diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h index 8498c9790..9cd812a9a 100644 --- a/src/ast/euf/euf_enode.h +++ b/src/ast/euf/euf_enode.h @@ -49,6 +49,7 @@ namespace euf { bool m_interpreted = false; bool m_merge_enabled = true; bool m_is_equality = false; // Does the expression represent an equality + bool m_is_relevant = false; lbool m_value = l_undef; // Assignment by SAT solver for Boolean node sat::bool_var m_bool_var = sat::null_bool_var; // SAT solver variable associated with Boolean node unsigned m_class_size = 1; // Size of the equivalence class if the enode is the root. @@ -145,6 +146,8 @@ namespace euf { unsigned num_parents() const { return m_parents.size(); } bool interpreted() const { return m_interpreted; } bool is_equality() const { return m_is_equality; } + bool is_relevant() const { return m_is_relevant; } + void set_relevant(bool b) { m_is_relevant = b; } lbool value() const { return m_value; } bool value_conflict() const { return value() != l_undef && get_root()->value() != l_undef && value() != get_root()->value(); } sat::bool_var bool_var() const { return m_bool_var; } diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 4c2ed7e12..1e58db340 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -722,12 +722,12 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { return BR_DONE; } - if (m().is_not(rhs)) + if (m().is_not(rhs)) std::swap(lhs, rhs); - if (m().is_not(lhs, lhs)) { - result = m().mk_not(m().mk_eq(lhs, rhs)); - return BR_REWRITE2; + if (m().is_not(lhs, lhs)) { + result = m().mk_not(m().mk_eq(lhs, rhs)); + return BR_REWRITE2; } if (unfolded) { diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 55d58e3f7..ab19a5586 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -21,8 +21,11 @@ Revision History: #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" +#include "ast/recfun_decl_plugin.h" +#include "ast/rewriter/recfun_replace.h" #include "ast/rewriter/seq_axioms.h" + namespace seq { axioms::axioms(th_rewriter& r): @@ -1052,6 +1055,79 @@ namespace seq { NOT_IMPLEMENTED_YET(); } + // A basic strategy for supporting replace_all and other + // similar functions is to use recursive relations. + // Then the features for recursive functions that allow expanding definitions + // using iterative deepening can be re-used. + // + // create recursive relation 'ra' with properties: + // ra(i, j, s, p, t, r) <- len(s) = i && len(r) = j + // ra(i, j, s, p, t, r) <- len(s) > i = 0 && p = "" && r = t + s + // ra(i, j, s, p, t, r) <- len(s) > i && p != "" && s = extract(s, 0, i) + p + extract(s, i + len(p), len(s)) && r = extract(r, 0, i) + t + extract(r, i + len(p), len(r)) && ra(i + len(p), j + len(t), s, p, t, r) + // ra(i, s, p, t, r) <- ~prefix(p, extract(s, i, len(s)) && at(s,i) = at(r,j) && ra(i + 1, j + 1, s, p, t, r) + // which amounts to: + // + // + // Then assert + // ra(s, p, t, replace_all(s, p, t)) + // + void axioms::replace_all_axiom(expr* r) { + expr* s = nullptr, *p = nullptr, *t = nullptr; + VERIFY(seq.str.is_replace_all(r, s, p, t)); + recfun::util rec(m); + recfun::decl::plugin& plugin = rec.get_plugin(); + recfun_replace replace(m); + sort* srt = s->get_sort(); + sort* domain[4] = { srt, srt, srt, srt }; + auto d = plugin.ensure_def(symbol("ra"), 4, domain, m.mk_bool_sort(), true); + func_decl* ra = d.get_def()->get_decl(); + sort* isrt = a.mk_int(); + var_ref vi(m.mk_var(5, isrt), m); + var_ref vj(m.mk_var(4, isrt), m); + var_ref vs(m.mk_var(3, srt), m); + var_ref vp(m.mk_var(2, srt), m); + var_ref vt(m.mk_var(1, srt), m); + var_ref vr(m.mk_var(0, srt), m); + var* vars[6] = { vi, vj, vs, vp, vt, vr }; + expr_ref len_s(seq.str.mk_length(vs), m); + expr_ref len_r(seq.str.mk_length(vr), m); + expr_ref test1(m.mk_eq(len_s, vi), m); + expr_ref branch1(m.mk_eq(len_r, vj), m); + expr_ref test2(m.mk_and(a.mk_gt(len_s, vi), m.mk_eq(vi, a.mk_int(0)), seq.str.mk_is_empty(vp)), m); + expr_ref branch2(m.mk_eq(vr, seq.str.mk_concat(vt, vs)), m); + NOT_IMPLEMENTED_YET(); +#if 0 + expr_ref test3(, m); + expr_ref s1(m_sk.mk_prefix_inv(vp, vs), m); + expr_ref r1(m_sk.mk_prefix_inv(vp, vr), m); + expr* args1[4] = { s1, vp, vt, r1 }; + expr_ref branch3(m.mk_and(m.mk_eq(seq.str.mk_concat(vp, s1), vs), + m.mk_eq(seq.str.mk_concat(vr, r1), vr), + m.mk_app(ra, 4, args1) + ), m); + expr_ref s0(m), r0(m); + m_sk.decompose(vs, s0, s1); + m_sk.decompose(vr, r0, r1); + expr* args2[4] = { s1, vp, vt, r1 }; + expr_ref branch4(m.mk_and(m.mk_eq(vs, seq.str.mk_concat(s0, s1)), + m.mk_eq(vr, seq.str.mk_concat(s0, r1)), + m.mk_app(ra, 4, args2)), m); + // s = [s0] + s' && r = [s0] + r' && ra(s', p, t, r') + + expr_ref body(m.mk_ite(test1, branch1, m.mk_ite(test2, branch2, m.mk_ite(test3, branch3, branch4))), m); + plugin.set_definition(replace, d, true, 4, vars, body); + expr* args3[4] = { s, p, t, r }; + expr_ref lit(m.mk_app(ra, 4, args3), m); + add_clause(lit); +#endif + } + + void axioms::replace_re_all_axiom(expr* e) { + expr* s = nullptr, *p = nullptr, *t = nullptr; + VERIFY(seq.str.is_replace_re_all(e, s, p, t)); + NOT_IMPLEMENTED_YET(); + } + /** diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index 0a2eb2ed2..583898562 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -107,6 +107,8 @@ namespace seq { void length_axiom(expr* n); void unroll_not_contains(expr* e); void replace_re_axiom(expr* e); + void replace_all_axiom(expr* e); + void replace_re_all_axiom(expr* e); expr_ref length_limit(expr* s, unsigned k); expr_ref is_digit(expr* ch); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index aeda76da5..c04c9991b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3112,7 +3112,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref else // D(e,r1)r2|(ite (r1nullable) (D(e,r2)) []) // observe that (mk_ite_simplify(true, D(e,r2), []) = D(e,r2) - result = mk_regex_union_normalize(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing())); + result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing())); } else if (m().is_ite(r, c, r1, r2)) { c1 = simplify_path(e, m().mk_and(c, path)); @@ -3171,7 +3171,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref result = re().mk_ite_simplify(range, epsilon(), nothing()); } else if (re().is_union(r, r1, r2)) - result = mk_regex_union_normalize(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path)); + result = mk_antimirov_deriv_union(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path)); else if (re().is_intersection(r, r1, r2)) result = mk_antimirov_deriv_intersection(e, mk_antimirov_deriv(e, r1, path), @@ -3237,11 +3237,11 @@ expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr* result = mk_antimirov_deriv_restrict(e, d2, path); else if (re().is_union(d1, a, b)) // distribute intersection over the union in d1 - result = mk_regex_union_normalize(mk_antimirov_deriv_intersection(e, a, d2, path), + result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, a, d2, path), mk_antimirov_deriv_intersection(e, b, d2, path)); else if (re().is_union(d2, a, b)) // distribute intersection over the union in d2 - result = mk_regex_union_normalize(mk_antimirov_deriv_intersection(e, d1, a, path), + result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, d1, a, path), mk_antimirov_deriv_intersection(e, d1, b, path)); else result = mk_regex_inter_normalize(d1, d2); @@ -3256,7 +3256,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) { if (m().is_ite(d, c, t, e)) result = m().mk_ite(c, mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r)); else if (re().is_union(d, t, e)) - result = mk_regex_union_normalize(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r)); + result = mk_antimirov_deriv_union(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r)); else result = mk_re_append(d, r); return result; @@ -3284,7 +3284,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) { else if (re().is_union(d, t, e)) result = mk_antimirov_deriv_intersection(elem, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e), m().mk_true()); else if (re().is_intersection(d, t, e)) - result = mk_regex_union_normalize(mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e)); + result = mk_antimirov_deriv_union(mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e)); else if (re().is_complement(d, t)) result = t; else @@ -3292,6 +3292,20 @@ expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) { return result; } +expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2) { + sort* seq_sort = nullptr, * ele_sort = nullptr; + VERIFY(m_util.is_re(d1, seq_sort)); + VERIFY(m_util.is_seq(seq_sort, ele_sort)); + expr_ref result(m()); + expr* c1, * t1, * e1, * c2, * t2, * e2; + if (m().is_ite(d1, c1, t1, e1) && m().is_ite(d2, c2, t2, e2) && c1 == c2) + // eliminate duplicate branching on exactly the same condition + result = m().mk_ite(c1, mk_antimirov_deriv_union(t1, t2), mk_antimirov_deriv_union(e1, e2)); + else + result = mk_regex_union_normalize(d1, d2); + return result; +} + // restrict the guards of all conditionals id d and simplify the resulting derivative // restrict(if(c, a, b), cond) = if(c, restrict(a, cond & c), restrict(b, cond & ~c)) // restrict(a U b, cond) = restrict(a, cond) U restrict(b, cond) @@ -3320,7 +3334,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond) else if (re().is_union(d, a, b)) { expr_ref a1(mk_antimirov_deriv_restrict(e, a, cond), m()); expr_ref b1(mk_antimirov_deriv_restrict(e, b, cond), m()); - result = mk_regex_union_normalize(a1, b1); + result = mk_antimirov_deriv_union(a1, b1); } return result; } @@ -3331,7 +3345,7 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { SASSERT(m_util.is_re(r2)); expr_ref result(m()); std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); }; - std::function compose = [&](expr* r1, expr* r2) { return re().mk_union(r1, r2); }; + std::function compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r2 : (is_subset(r2, r1) ? r1 : re().mk_union(r1, r2))); }; if (r1 == r2 || re().is_empty(r2) || re().is_full_seq(r1)) result = r1; else if (re().is_empty(r1) || re().is_full_seq(r2)) @@ -3353,7 +3367,7 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { if (re().is_epsilon(r2)) std::swap(r1, r2); std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); }; - std::function compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); }; + std::function compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r1 : (is_subset(r2, r1) ? r2 : re().mk_inter(r1, r2))); }; if (r1 == r2 || re().is_empty(r1) || re().is_full_seq(r2)) result = r1; else if (re().is_empty(r2) || re().is_full_seq(r1)) @@ -4586,6 +4600,7 @@ bool seq_rewriter::is_subset(expr* r1, expr* r2) const { // return false; expr* ra1 = nullptr, *ra2 = nullptr, *ra3 = nullptr; expr* rb1 = nullptr, *rb2 = nullptr, *rb3 = nullptr; + unsigned la, ua, lb, ub; if (re().is_complement(r1, ra1) && re().is_complement(r2, rb1)) { return is_subset(rb1, ra1); @@ -4598,6 +4613,8 @@ bool seq_rewriter::is_subset(expr* r1, expr* r2) const { return true; if (re().is_full_seq(r2)) return true; + if (re().is_dot_plus(r2) && re().get_info(r1).nullable == l_false) + return true; if (is_concat(r1, ra1, ra2, ra3) && is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) { r1 = ra3; @@ -4609,6 +4626,20 @@ bool seq_rewriter::is_subset(expr* r1, expr* r2) const { r1 = ra2; continue; } + // r1=ra3{la,ua}ra2, r2=rb3{lb,ub}rb2, ra3=rb3, lb<=la, ua<=ub + if (re().is_concat(r1, ra1, ra2) && re().is_loop(ra1, ra3, la, ua) && + re().is_concat(r2, rb1, rb2) && re().is_loop(rb1, rb3, lb, ub) && + ra3 == rb3 && lb <= la && ua <= ub) { + r1 = ra2; + r2 = rb2; + continue; + } + // ra1=ra3{la,ua}, r2=rb3{lb,ub}, ra3=rb3, lb<=la, ua<=ub + if (re().is_loop(r1, ra3, la, ua) && + re().is_loop(r2, rb3, lb, ub) && + ra3 == rb3 && lb <= la && ua <= ub) { + return true; + } return false; } } diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 9357a2be8..0d8ac029c 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -217,6 +217,7 @@ class seq_rewriter { expr_ref mk_antimirov_deriv_intersection(expr* elem, expr* d1, expr* d2, expr* path); expr_ref mk_antimirov_deriv_concat(expr* d, expr* r); expr_ref mk_antimirov_deriv_negate(expr* elem, expr* d); + expr_ref mk_antimirov_deriv_union(expr* d1, expr* d2); expr_ref mk_antimirov_deriv_restrict(expr* elem, expr* d1, expr* cond); expr_ref mk_regex_reverse(expr* r); expr_ref mk_regex_concat(expr* r1, expr* r2); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 0c2461dd6..2aaf4626c 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -627,7 +627,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { count_down_subterm_references(result, reference_map); // Any term that was newly introduced by the rewrite step is only referenced within / reachable from the result term. - for (auto kv : reference_map) { + for (auto const& kv : reference_map) { if (kv.m_value == 0) { m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n"; } @@ -691,7 +691,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return; if (m_new_subst) { m_rep.reset(); - for (auto kv : m_subst->sub()) + for (auto const& kv : m_subst->sub()) m_rep.insert(kv.m_key, kv.m_value); m_new_subst = false; } @@ -859,8 +859,8 @@ ast_manager & th_rewriter::m() const { } void th_rewriter::updt_params(params_ref const & p) { - m_params = p; - m_imp->cfg().updt_params(p); + m_params.append(p); + m_imp->cfg().updt_params(m_params); } void th_rewriter::get_param_descrs(param_descrs & r) { diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 23915f7fe..823f48e01 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -301,10 +301,23 @@ UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr ctx.regular_stream() << std::endl; }); -UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, - bool smt2c = ctx.params().m_smtlib2_compliant; - ctx.regular_stream() << (smt2c ? "\"" : "") << arg << (smt2c ? "\"" : "") << std::endl;); +static std::string escape_string(char const* arg) { + std::string result; + while (*arg) { + auto ch = *arg++; + if (ch == '"') + result.push_back(ch); + result.push_back(ch); + } + return result; +} +UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, + bool smt2c = ctx.params().m_smtlib2_compliant; + if (smt2c) + ctx.regular_stream() << "\"" << escape_string(arg) << "\"" << std::endl; + else + ctx.regular_stream() << arg << std::endl;); class set_get_option_cmd : public cmd { protected: diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 845ac645c..968dcacd8 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2107,6 +2107,21 @@ void cmd_context::analyze_failure(expr_mark& seen, model_evaluator& ev, expr* a, << (expected_value?"true":"false") << "\n";); IF_VERBOSE(11, display_detailed_analysis(verbose_stream(), ev, a)); + + if (m().is_iff(a)) { + ptr_vector todo; + todo.push_back(a); + for (unsigned i = 0; i < todo.size(); ++i) { + e = todo[i]; + if (m().is_and(e) || m().is_or(e) || m().is_iff(e) || m().is_implies(e) || m().is_not(e)) + for (expr* arg : *to_app(e)) + todo.push_back(arg); + else + IF_VERBOSE(10, verbose_stream() << "#" << e->get_id() << " " << mk_bounded_pp(e, m()) << " " << (ev.is_true(e)?"true":"false") << "\n"); + } + return; + } + } void cmd_context::display_detailed_analysis(std::ostream& out, model_evaluator& ev, expr* e) { diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 5b648741c..5a628ce58 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -199,12 +199,12 @@ void tst_params(cmd_context & ctx) { params_ref p1; params_ref p2; p1.set_uint("val", 100); - p2 = p1; + p2.append(p1); SASSERT(p2.get_uint("val", 0) == 100); p2.set_uint("val", 200); SASSERT(p2.get_uint("val", 0) == 200); SASSERT(p1.get_uint("val", 0) == 100); - p2 = p1; + p2.append(p1); SASSERT(p2.get_uint("val", 0) == 100); SASSERT(p1.get_uint("val", 0) == 100); ctx.regular_stream() << "worked" << std::endl; diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index 1bc0cb630..6124e726e 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -227,8 +227,8 @@ public: } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index da0cfb883..a23fc9800 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -111,6 +111,7 @@ void model_core::unregister_decl(func_decl * d) { m_interp[m_const_decls.back()].first = v.first; m_const_decls.pop_back(); m_interp.remove(d); + m_decls.erase(d); m.dec_ref(k); m.dec_ref(v.second); return; @@ -122,6 +123,7 @@ void model_core::unregister_decl(func_decl * d) { auto v = ef->get_data().m_value; m_finterp.remove(d); m_func_decls.erase(d); + m_decls.erase(d); m.dec_ref(k); dealloc(v); } diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index b66ddf275..6ffd0f745 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -395,8 +395,8 @@ public: char const* name() const override { return "horn"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index ddf85ce19..3baf9da87 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -55,8 +55,8 @@ class nlsat_tactic : public tactic { } void updt_params(params_ref const & p) { - m_params = p; - m_solver.updt_params(p); + m_params.append(p); + m_solver.updt_params(m_params); } bool contains_unsupported(expr_ref_vector & b2a, expr_ref_vector & x2t) { @@ -226,7 +226,7 @@ public: char const* name() const override { return "nlsat"; } void updt_params(params_ref const & p) override { - m_params = p; + m_params.append(p); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 39a7bb032..01975464a 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -259,6 +259,12 @@ namespace opt { if (!m_models[i]) m_models.set(i, m_last_model.get()); + if (val > m_objective_values[i]) + m_objective_values[i] = val; + + if (!m_last_model) + return true; + // // retrieve value of objective from current model and update // current optimal. @@ -267,7 +273,7 @@ namespace opt { rational r; expr_ref value = (*m_last_model)(m_objective_terms.get(i)); if (arith_util(m).is_numeral(value, r) && r > m_objective_values[i]) - m_objective_values[i] = inf_eps(r); + m_objective_values[i] = inf_eps(r); }; update_objective(); diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 21489be58..58cdd0cda 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -49,14 +49,14 @@ namespace opt { dst[i] = src[i]; m_models.set(i, m_s->get_model_idx(i)); m_s->get_labels(m_labels); - m_lower_fmls[i] = fmls[i].get(); + m_lower_fmls[i] = fmls.get(i); if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already. m_lower_fmls[i] = m.mk_false(); fmls[i] = m.mk_false(); } } - else if (src[i] < dst[i] && !m.is_true(m_lower_fmls[i].get())) { - fmls[i] = m_lower_fmls[i].get(); + else if (src[i] < dst[i] && !m.is_true(m_lower_fmls.get(i))) { + fmls[i] = m_lower_fmls.get(i); } } } @@ -202,6 +202,9 @@ namespace opt { for (unsigned i = 0; i < obj_index; ++i) commit_assignment(i); +// m_s->maximize_objective(obj_index, bound); +// m_s->assert_expr(bound); + unsigned steps = 0; unsigned step_incs = 0; rational delta_per_step(1); @@ -282,7 +285,7 @@ namespace opt { bool optsmt::can_increment_delta(vector const& lower, unsigned i) { arith_util arith(m); inf_eps max_delta; - if (m_lower[i] < m_upper[i] && arith.is_int(m_objs[i].get())) { + if (m_lower[i] < m_upper[i] && arith.is_int(m_objs.get(i))) { inf_eps delta = m_lower[i] - lower[i]; if (m_lower[i].is_finite() && delta > max_delta) { return true; @@ -435,7 +438,7 @@ namespace opt { bool progress = false; for (unsigned i = 0; i < m_lower.size() && m.inc(); ++i) { if (m_lower[i] <= mid[i] && mid[i] <= m_upper[i] && m_lower[i] < m_upper[i]) { - th.enable_record_conflict(bounds[i].get()); + th.enable_record_conflict(bounds.get(i)); lbool is_sat = m_s->check_sat(1, bounds.data() + i); switch(is_sat) { case l_true: @@ -484,10 +487,10 @@ namespace opt { } for (unsigned i = 0; i < m_objs.size(); ++i) { - smt::theory_var v = solver.add_objective(m_objs[i].get()); + smt::theory_var v = solver.add_objective(m_objs.get(i)); if (v == smt::null_theory_var) { std::ostringstream out; - out << "Objective function '" << mk_pp(m_objs[i].get(), m) << "' is not supported"; + out << "Objective function '" << mk_pp(m_objs.get(i), m) << "' is not supported"; throw default_exception(out.str()); } m_vars.push_back(v); @@ -547,7 +550,7 @@ namespace opt { // force lower_bound(i) <= objective_value(i) void optsmt::commit_assignment(unsigned i) { inf_eps lo = m_lower[i]; - TRACE("opt", tout << "set lower bound of " << mk_pp(m_objs[i].get(), m) << " to: " << lo << "\n"; + TRACE("opt", tout << "set lower bound of " << mk_pp(m_objs.get(i), m) << " to: " << lo << "\n"; tout << get_lower(i) << ":" << get_upper(i) << "\n";); // Only assert bounds for bounded objectives if (lo.is_finite()) { diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index 4bc37b86b..294c5cbbe 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -190,7 +190,8 @@ void context_params::get_solver_params(params_ref & p, bool & proofs_enabled, bo proofs_enabled &= p.get_bool("proof", m_proof); models_enabled &= p.get_bool("model", m_model); unsat_core_enabled = m_unsat_core || p.get_bool("unsat_core", false); - p = merge_default_params(p); + if (!m_auto_config && !p.contains("auto_config")) + p.set_bool("auto_config", false); } diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 120931536..377b62ac0 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -249,8 +249,8 @@ namespace mbp { bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) { app_ref_vector vs(m); vs.push_back(v); - project(model, vs, lits, false); - return vs.empty(); + vector defs; + return project(model, vs, lits, defs, false) && vs.empty(); } typedef opt::model_based_opt::var var; @@ -265,12 +265,12 @@ namespace mbp { return t; } - vector project(model& model, app_ref_vector& vars, expr_ref_vector& fmls, bool compute_def) { + bool project(model& model, app_ref_vector& vars, expr_ref_vector& fmls, vector& result, bool compute_def) { bool has_arith = false; for (expr* v : vars) has_arith |= is_arith(v); if (!has_arith) - return vector(); + return true; model_evaluator eval(model); TRACE("qe", tout << model;); eval.set_model_completion(true); @@ -294,7 +294,7 @@ namespace mbp { } fmls.shrink(j); TRACE("qe", tout << "formulas\n" << fmls << "\n"; - for (auto [e, id] : tids) + for (auto const& [e, id] : tids) tout << mk_pp(e, m) << " -> " << id << "\n";); // fmls holds residue, @@ -312,7 +312,7 @@ namespace mbp { rational r; expr_ref val = eval(v); if (!m.inc()) - return vector(); + return false; if (!a.is_numeral(val, r)) throw default_exception("evaluation did not produce a numeral"); TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";); @@ -326,15 +326,13 @@ namespace mbp { if (is_arith(e) && !var_mark.is_marked(e)) mark_rec(fmls_mark, e); } - if (m_check_purified) { for (expr* fml : fmls) mark_rec(fmls_mark, fml); for (auto& kv : tids) { expr* e = kv.m_key; - if (!var_mark.is_marked(e)) { - mark_rec(fmls_mark, e); - } + if (!var_mark.is_marked(e)) + mark_rec(fmls_mark, e); } } @@ -364,16 +362,18 @@ namespace mbp { for (auto const& d : defs) tout << "def: " << d << "\n"; tout << fmls << "\n";); - vector result; if (compute_def) optdefs2mbpdef(defs, index2expr, real_vars, result); - if (m_apply_projection) - apply_projection(result, fmls); + if (m_apply_projection && !apply_projection(eval, result, fmls)) + return false; + TRACE("qe", - for (auto [v, t] : result) + for (auto const& [v, t] : result) tout << v << " := " << t << "\n"; + for (auto* f : fmls) + tout << mk_pp(f, m) << " := " << eval(f) << "\n"; tout << "fmls:" << fmls << "\n";); - return result; + return true; } void optdefs2mbpdef(vector const& defs, ptr_vector const& index2expr, unsigned_vector const& real_vars, vector& result) { @@ -548,10 +548,11 @@ namespace mbp { } } - void apply_projection(vector& defs, expr_ref_vector& fmls) { + bool apply_projection(model_evaluator& eval, vector const& defs, expr_ref_vector& fmls) { if (fmls.empty() || defs.empty()) - return; + return true; expr_safe_replace subst(m); + expr_ref_vector fmls_tmp(m); expr_ref tmp(m); for (unsigned i = defs.size(); i-- > 0; ) { auto const& d = defs[i]; @@ -561,8 +562,11 @@ namespace mbp { unsigned j = 0; for (expr* fml : fmls) { subst(fml, tmp); + if (m.is_false(eval(tmp))) + return false; fmls[j++] = tmp; } + return true; } }; @@ -579,12 +583,13 @@ namespace mbp { return (*m_imp)(model, var, vars, lits); } - void arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - m_imp->project(model, vars, lits, false); + bool arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + vector defs; + return m_imp->project(model, vars, lits, defs, false); } - vector arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - return m_imp->project(model, vars, lits, true); + bool arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) { + return m_imp->project(model, vars, lits, defs, true); } void arith_project_plugin::set_check_purified(bool check_purified) { diff --git a/src/qe/mbp/mbp_arith.h b/src/qe/mbp/mbp_arith.h index 51d80a870..ca4cccb74 100644 --- a/src/qe/mbp/mbp_arith.h +++ b/src/qe/mbp/mbp_arith.h @@ -29,8 +29,8 @@ namespace mbp { bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override; bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; } family_id get_family_id() override; - void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; - vector project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) override; void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); } opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt); diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp index 149d11987..0f4c805b7 100644 --- a/src/qe/mbp/mbp_arrays.cpp +++ b/src/qe/mbp/mbp_arrays.cpp @@ -1624,8 +1624,8 @@ namespace mbp { ); } - vector array_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - return vector(); + bool array_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) { + return true; } void array_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) { diff --git a/src/qe/mbp/mbp_arrays.h b/src/qe/mbp/mbp_arrays.h index bb18cde11..7dd904108 100644 --- a/src/qe/mbp/mbp_arrays.h +++ b/src/qe/mbp/mbp_arrays.h @@ -35,7 +35,7 @@ namespace mbp { bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; void operator()(model& model, app_ref_vector& vars, expr_ref& fml, app_ref_vector& aux_vars, bool reduce_all_selects); family_id get_family_id() override; - vector project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) override; void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override; }; diff --git a/src/qe/mbp/mbp_datatypes.cpp b/src/qe/mbp/mbp_datatypes.cpp index 798258599..e40a19546 100644 --- a/src/qe/mbp/mbp_datatypes.cpp +++ b/src/qe/mbp/mbp_datatypes.cpp @@ -300,8 +300,8 @@ namespace mbp { return m_imp->solve(model, vars, lits); } - vector datatype_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - return vector(); + bool datatype_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) { + return true; } void datatype_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) { diff --git a/src/qe/mbp/mbp_datatypes.h b/src/qe/mbp/mbp_datatypes.h index 345260970..f30aaaa9f 100644 --- a/src/qe/mbp/mbp_datatypes.h +++ b/src/qe/mbp/mbp_datatypes.h @@ -34,7 +34,7 @@ namespace mbp { bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override; bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; family_id get_family_id() override; - vector project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) override; void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override; }; diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index 741639aaa..12b592960 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -67,7 +67,7 @@ namespace mbp { virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; } virtual family_id get_family_id() { return null_family_id; } - virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { }; + virtual bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }; /** \brief project vars modulo model, return set of definitions for eliminated variables. @@ -76,7 +76,7 @@ namespace mbp { - returns set of definitions (TBD: in triangular form, the last definition can be substituted into definitions that come before) */ - virtual vector project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return vector(); } + virtual bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) { return true; } /** \brief model based saturation. Saturates theory axioms to equi-satisfiable literals over EUF, diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index f6dd9c712..68ab215a2 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2466,7 +2466,7 @@ public: } void updt_params(params_ref const & p) override { - m_params = p; + m_params.append(p); // m_imp->updt_params(p); } diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 1dcbb178f..5d00d8a6b 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -266,7 +266,10 @@ namespace qe { vector uflia_mbi::arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits) { mbp::arith_project_plugin ap(m); ap.set_check_purified(false); - return ap.project(*mdl.get(), avars, lits); + vector defs; + bool ok = ap.project(*mdl.get(), avars, lits, defs); + CTRACE("qe", !ok, tout << "projection failure ignored!!!!\n"); + return defs; } mbi_result uflia_mbi::operator()(expr_ref_vector& lits, model_ref& mdl) { diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index da1ce5efd..76f4f5715 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -103,8 +103,8 @@ public: char const* name() const override { return "qe"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 51f2c3d98..0e72de37f 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -288,6 +288,7 @@ namespace sat { m_free_vars.pop_back(); m_active_vars.push_back(v); reset_var(v, ext, dvar); + SASSERT(v < m_justification.size()); return v; } m_active_vars.push_back(v); @@ -3008,7 +3009,7 @@ namespace sat { svector logits(vars.size(), 0.0); double itau = m_config.m_reorder_itau; double lse = 0; - double mid = m_rand.max_value()/2; + double mid = (double)(m_rand.max_value()/2); double max = 0; for (double& f : logits) { f = itau * (m_rand() - mid)/mid; @@ -3508,7 +3509,6 @@ namespace sat { unsigned old_num_vars = m_vars_lim.pop(num_scopes); if (old_num_vars == m_active_vars.size()) return; - unsigned free_vars_head = m_free_vars.size(); unsigned sz = m_active_vars.size(), j = old_num_vars; unsigned new_lvl = m_scopes.size() - num_scopes; @@ -3538,9 +3538,7 @@ namespace sat { } else { set_eliminated(v, true); - if (!is_external(v) || true) { - m_free_vars.push_back(v); - } + m_vars_to_free.push_back(v); } } m_active_vars.shrink(j); @@ -3550,8 +3548,7 @@ namespace sat { IF_VERBOSE(0, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n"); } }; - for (unsigned i = m_free_vars.size(); i-- > free_vars_head; ) { - bool_var v = m_free_vars[i]; + for (bool_var v : m_vars_to_free) { cleanup_watch(literal(v, false)); cleanup_watch(literal(v, true)); @@ -3560,7 +3557,7 @@ namespace sat { tout << "clauses to reinit: " << (m_clauses_to_reinit.size() - old_sz) << "\n"; tout << "new level: " << new_lvl << "\n"; tout << "vars to reinit: " << m_vars_to_reinit << "\n"; - tout << "free vars: " << bool_var_vector(m_free_vars.size() - free_vars_head, m_free_vars.data() + free_vars_head) << "\n"; + tout << "free vars: " << bool_var_vector(m_vars_to_free) << "\n"; for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; ) tout << "reinit: " << m_clauses_to_reinit[i] << "\n"; display(tout);); @@ -3599,7 +3596,6 @@ namespace sat { void solver::pop(unsigned num_scopes) { if (num_scopes == 0) return; - unsigned free_vars_head = m_free_vars.size(); if (m_ext) { pop_vars(num_scopes); m_ext->pop(num_scopes); @@ -3609,13 +3605,16 @@ namespace sat { scope & s = m_scopes[new_lvl]; m_inconsistent = false; // TBD: use model seems to make this redundant: s.m_inconsistent; unassign_vars(s.m_trail_lim, new_lvl); - for (unsigned i = m_free_vars.size(); i-- > free_vars_head; ) - m_case_split_queue.del_var_eh(m_free_vars[i]); + for (bool_var v : m_vars_to_free) + m_case_split_queue.del_var_eh(v); m_scope_lvl -= num_scopes; reinit_clauses(s.m_clauses_to_reinit_lim); m_scopes.shrink(new_lvl); - if (m_ext) + if (m_ext) { m_ext->pop_reinit(); + m_free_vars.append(m_vars_to_free); + m_vars_to_free.reset(); + } } void solver::unassign_vars(unsigned old_sz, unsigned new_lvl) { @@ -3692,6 +3691,7 @@ namespace sat { // void solver::user_push() { + pop_to_base_level(); m_free_var_freeze.push_back(m_free_vars); m_free_vars.reset(); // resetting free_vars forces new variables to be assigned above new_v diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index b6affe4ee..74bb182e8 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -124,7 +124,7 @@ namespace sat { clause_vector m_clauses; clause_vector m_learned; unsigned m_num_frozen; - unsigned_vector m_active_vars, m_free_vars, m_vars_to_reinit; + unsigned_vector m_active_vars, m_free_vars, m_vars_to_free, m_vars_to_reinit; vector m_watches; svector m_assignment; svector m_justification; @@ -266,6 +266,11 @@ namespace sat { // // ----------------------- void add_clause(unsigned num_lits, literal * lits, sat::status st) override { mk_clause(num_lits, lits, st); } + void add_clause(literal l1, literal l2, status st) { + literal lits[2] = { l1, l2 }; + add_clause(2, lits, st); + } + void add_clause(literal lit, status st) { literal lits[1] = { lit }; add_clause(1, lits, st); } bool_var add_var(bool ext) override { return mk_var(ext, true); } bool_var mk_var(bool ext = false, bool dvar = true); @@ -444,9 +449,10 @@ namespace sat { void flush_roots(); typedef std::pair bin_clause; struct bin_clause_hash { unsigned operator()(bin_clause const& b) const { return b.first.hash() + 2*b.second.hash(); } }; - protected: - watch_list & get_wlist(literal l) { return m_watches[l.index()]; } - watch_list const & get_wlist(literal l) const { return m_watches[l.index()]; } + + watch_list const& get_wlist(literal l) const { return m_watches[l.index()]; } + watch_list& get_wlist(literal l) { return m_watches[l.index()]; } + protected: watch_list & get_wlist(unsigned l_idx) { return m_watches[l_idx]; } bool is_marked(bool_var v) const { return m_mark[v]; } void mark(bool_var v) { SASSERT(!is_marked(v)); m_mark[v] = true; } diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h index ca66003cb..407deae5c 100644 --- a/src/sat/sat_solver_core.h +++ b/src/sat/sat_solver_core.h @@ -35,10 +35,7 @@ namespace sat { // add clauses virtual void add_clause(unsigned n, literal* lits, status st) = 0; - void add_clause(literal l1, literal l2, status st) { - literal lits[2] = {l1, l2}; - add_clause(2, lits, st); - } + void add_clause(literal l1, literal l2, literal l3, status st) { literal lits[3] = {l1, l2, l3}; add_clause(3, lits, st); diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 43b91b2f2..a75c0022d 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -38,7 +38,6 @@ z3_add_component(sat_smt q_queue.cpp q_solver.cpp recfun_solver.cpp - sat_dual_solver.cpp sat_th.cpp user_solver.cpp COMPONENT_DEPENDENCIES diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 882dd23b0..d81efc43b 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -545,11 +545,13 @@ namespace arith { } m_left_side.clear(); // reset the coefficients after they have been used. - for (unsigned i = 0; i < vars.size(); ++i) { - theory_var var = vars[i]; + for (theory_var var : vars) { rational const& r = m_columns[var]; if (!r.is_zero()) { - m_left_side.push_back(std::make_pair(r, register_theory_var_in_lar_solver(var))); + auto vi = register_theory_var_in_lar_solver(var); + if (lp::tv::is_term(vi)) + vi = lp().map_term_index_to_column_index(vi); + m_left_side.push_back(std::make_pair(r, vi)); m_columns[var].reset(); } } diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index da68691c7..80dea338a 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -953,6 +953,7 @@ namespace arith { if (n1->get_root() == n2->get_root()) continue; literal eq = eq_internalize(n1, n2); + ctx.mark_relevant(eq); if (s().value(eq) != l_true) return true; } @@ -1446,21 +1447,19 @@ namespace arith { TRACE("arith", tout << "canceled\n";); return l_undef; } - if (!m_nla) { - TRACE("arith", tout << "no nla\n";); + CTRACE("arith", !m_nla, tout << "no nla\n";); + if (!m_nla) return l_true; - } if (!m_nla->need_check()) return l_true; m_a1 = nullptr; m_a2 = nullptr; lbool r = m_nla->check(m_nla_lemma_vector); switch (r) { - case l_false: { + case l_false: for (const nla::lemma& l : m_nla_lemma_vector) false_case_of_check_nla(l); break; - } case l_true: if (assume_eqs()) return l_false; @@ -1477,11 +1476,27 @@ namespace arith { } bool solver::include_func_interp(func_decl* f) const { - return - a.is_div0(f) || - a.is_idiv0(f) || - a.is_power0(f) || - a.is_rem0(f) || - a.is_mod0(f); + SASSERT(f->get_family_id() == get_id()); + switch (f->get_decl_kind()) { + case OP_ADD: + case OP_SUB: + case OP_UMINUS: + case OP_MUL: + case OP_LE: + case OP_LT: + case OP_GE: + case OP_GT: + case OP_MOD: + case OP_REM: + case OP_DIV: + case OP_IDIV: + case OP_POWER: + case OP_IS_INT: + case OP_TO_INT: + case OP_TO_REAL: + return false; + default: + return true; + } } } diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 759c85fae..76c74f93d 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -445,6 +445,7 @@ namespace arith { bool is_shared(theory_var v) const override; lbool get_phase(bool_var v) override; bool include_func_interp(func_decl* f) const override; + bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_add(n->get_expr()); } // bounds and equality propagation callbacks lp::lar_solver& lp() { return *m_solver; } diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index d362dacb6..296c35b8c 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -57,8 +57,6 @@ namespace array { bool solver::assert_axiom(unsigned idx) { axiom_record& r = m_axiom_trail[idx]; - if (!is_relevant(r)) - return false; switch (r.m_kind) { case axiom_record::kind_t::is_store: return assert_store_axiom(to_app(r.n->get_expr())); @@ -86,35 +84,12 @@ namespace array { return assert_default_const_axiom(to_app(child)); else if (a.is_store(child)) return assert_default_store_axiom(to_app(child)); - else if (a.is_map(child)) + else if (is_map_combinator(child)) return assert_default_map_axiom(to_app(child)); else return false; } - - bool solver::is_relevant(axiom_record const& r) const { - return true; -#if 0 - // relevancy propagation is currently incomplete on terms - - expr* child = r.n->get_expr(); - switch (r.m_kind) { - case axiom_record::kind_t::is_select: { - app* select = r.select->get_app(); - for (unsigned i = 1; i < select->get_num_args(); ++i) - if (!ctx.is_relevant(select->get_arg(i))) - return false; - return ctx.is_relevant(child); - } - case axiom_record::kind_t::is_default: - return ctx.is_relevant(child); - default: - return true; - } -#endif - } - bool solver::assert_select(unsigned idx, axiom_record& r) { expr* child = r.n->get_expr(); app* select = r.select->get_app(); @@ -140,7 +115,7 @@ namespace array { return assert_select_as_array_axiom(select, to_app(child)); else if (a.is_store(child)) return assert_select_store_axiom(select, to_app(child)); - else if (a.is_map(child)) + else if (is_map_combinator(child)) return assert_select_map_axiom(select, to_app(child)); else if (is_lambda(child)) return assert_select_lambda_axiom(select, child); @@ -215,10 +190,17 @@ namespace array { return new_prop; sat::literal sel_eq = sat::null_literal; + auto ensure_relevant = [&](sat::literal lit) { + if (ctx.is_relevant(lit)) + return; + new_prop = true; + ctx.mark_relevant(lit); + }; auto init_sel_eq = [&]() { if (sel_eq != sat::null_literal) return true; sel_eq = mk_literal(sel_eq_e); + ensure_relevant(sel_eq); return s().value(sel_eq) != l_true; }; @@ -235,6 +217,7 @@ namespace array { break; } sat::literal idx_eq = eq_internalize(idx1, idx2); + ensure_relevant(idx_eq); if (s().value(idx_eq) == l_true) continue; if (s().value(idx_eq) == l_undef) @@ -253,8 +236,7 @@ namespace array { * Assert * select(const(v), i) = v */ - bool solver::assert_select_const_axiom(app* select, app* cnst) { - + bool solver::assert_select_const_axiom(app* select, app* cnst) { ++m_stats.m_num_select_const_axiom; expr* val = nullptr; VERIFY(a.is_const(cnst, val)); @@ -291,16 +273,19 @@ namespace array { return add_clause(lit1, ~lit2); } + bool solver::is_map_combinator(expr* map) const { + return a.is_map(map) || a.is_union(map) || a.is_intersect(map) || a.is_difference(map) || a.is_complement(map); + } + /** * Assert axiom: * select(map[f](a, ... d), i) = f(select(a,i),...,select(d,i)) */ bool solver::assert_select_map_axiom(app* select, app* map) { ++m_stats.m_num_select_map_axiom; - SASSERT(a.is_map(map)); SASSERT(a.is_select(select)); + SASSERT(is_map_combinator(map)); SASSERT(map->get_num_args() > 0); - func_decl* f = a.get_map_func_decl(map); unsigned num_args = select->get_num_args(); ptr_buffer args1, args2; vector > args2l; @@ -321,7 +306,8 @@ namespace array { expr_ref sel1(m), sel2(m); sel1 = a.mk_select(args1); - sel2 = m.mk_app(f, args2); + sel2 = apply_map(map, args2.size(), args2.data()); + rewrite(sel2); euf::enode* n1 = e_internalize(sel1); euf::enode* n2 = e_internalize(sel2); @@ -348,21 +334,44 @@ namespace array { return ctx.propagate(n1, n2, array_axiom()); } + expr_ref solver::apply_map(app* map, unsigned n, expr* const* args) { + expr_ref result(m); + if (a.is_map(map)) + result = m.mk_app(a.get_map_func_decl(map), n, args); + else if (a.is_union(map)) + result = m.mk_or(n, args); + else if (a.is_intersect(map)) + result = m.mk_and(n, args); + else if (a.is_difference(map)) { + SASSERT(n > 0); + result = args[0]; + for (unsigned i = 1; i < n; ++i) + result = m.mk_and(result, m.mk_not(args[i])); + } + else if (a.is_complement(map)) { + SASSERT(n == 1); + result = m.mk_not(args[0]); + } + else { + UNREACHABLE(); + } + rewrite(result); + return result; + } + + /** * Assert: * default(map[f](a,..,d)) = f(default(a),..,default(d)) */ bool solver::assert_default_map_axiom(app* map) { ++m_stats.m_num_default_map_axiom; - SASSERT(a.is_map(map)); - func_decl* f = a.get_map_func_decl(map); - SASSERT(map->get_num_args() == f->get_arity()); + SASSERT(is_map_combinator(map)); expr_ref_vector args2(m); for (expr* arg : *map) args2.push_back(a.mk_default(arg)); expr_ref def1(a.mk_default(map), m); - expr_ref def2(m.mk_app(f, args2), m); - rewrite(def2); + expr_ref def2 = apply_map(map, args2.size(), args2.data()); return ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom()); } @@ -534,11 +543,14 @@ namespace array { unsigned num_vars = get_num_vars(); bool change = false; for (unsigned v = 0; v < num_vars; v++) { - propagate_parent_select_axioms(v); auto& d = get_var_data(v); if (!d.m_prop_upward) continue; euf::enode* n = var2enode(v); + if (!ctx.is_relevant(n)) + continue; + for (euf::enode* lambda : d.m_parent_lambdas) + propagate_select_axioms(d, lambda); if (add_as_array_eqs(n)) change = true; bool has_default = false; @@ -552,8 +564,8 @@ namespace array { m_delay_qhead = 0; for (; m_delay_qhead < sz; ++m_delay_qhead) - if (m_axiom_trail[m_delay_qhead].is_delayed() && assert_axiom(m_delay_qhead)) - change = true; + if (m_axiom_trail[m_delay_qhead].is_delayed() && assert_axiom(m_delay_qhead)) + change = true; flet _enable_delay(m_enable_delay, false); if (unit_propagate()) change = true; @@ -567,6 +579,8 @@ namespace array { return false; for (unsigned i = 0; i < ctx.get_egraph().enodes_of(f).size(); ++i) { euf::enode* p = ctx.get_egraph().enodes_of(f)[i]; + if (!ctx.is_relevant(p)) + continue; expr_ref_vector select(m); select.push_back(n->get_expr()); for (expr* arg : *to_app(p->get_expr())) @@ -574,7 +588,8 @@ namespace array { expr_ref _e(a.mk_select(select.size(), select.data()), m); euf::enode* e = e_internalize(_e); if (e->get_root() != p->get_root()) { - add_unit(eq_internalize(_e, p->get_expr())); + sat::literal eq = eq_internalize(_e, p->get_expr()); + add_unit(eq); change = true; } } @@ -594,13 +609,12 @@ namespace array { expr* e2 = var2expr(v2); if (e1->get_sort() != e2->get_sort()) continue; - if (must_have_different_model_values(v1, v2)) { - continue; - } - if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) { - continue; - } + if (must_have_different_model_values(v1, v2)) + continue; + if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) + continue; sat::literal lit = eq_internalize(e1, e2); + ctx.mark_relevant(lit); if (s().value(lit) == l_undef) prop = true; } @@ -612,10 +626,11 @@ namespace array { ptr_buffer to_unmark; unsigned num_vars = get_num_vars(); for (unsigned i = 0; i < num_vars; i++) { - euf::enode * n = var2enode(i); - + euf::enode * n = var2enode(i); if (!is_array(n)) - continue; + continue; + if (!ctx.is_relevant(n)) + continue; euf::enode * r = n->get_root(); if (r->is_marked1()) continue; diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index aa94f12a7..5e1a76b9f 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -49,7 +49,7 @@ namespace array { if (v == euf::null_theory_var) { mk_var(n); if (is_lambda(n->get_expr())) - internalize_lambda(n); + internalize_lambda_eh(n); } } @@ -57,45 +57,6 @@ namespace array { ensure_var(n); } - void solver::internalize_store(euf::enode* n) { - add_parent_lambda(n->get_arg(0)->get_th_var(get_id()), n); - push_axiom(store_axiom(n)); - add_lambda(n->get_th_var(get_id()), n); - SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward); - } - - void solver::internalize_map(euf::enode* n) { - for (auto* arg : euf::enode_args(n)) { - add_parent_lambda(arg->get_th_var(get_id()), n); - set_prop_upward(arg); - } - push_axiom(default_axiom(n)); - add_lambda(n->get_th_var(get_id()), n); - SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward); - } - - void solver::internalize_lambda(euf::enode* n) { - SASSERT(is_lambda(n->get_expr()) || a.is_const(n->get_expr()) || a.is_as_array(n->get_expr())); - theory_var v = n->get_th_var(get_id()); - push_axiom(default_axiom(n)); - add_lambda(v, n); - set_prop_upward(v); - } - - void solver::internalize_select(euf::enode* n) { - add_parent_select(n->get_arg(0)->get_th_var(get_id()), n); - } - - void solver::internalize_ext(euf::enode* n) { - SASSERT(is_array(n->get_arg(0))); - push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1))); - } - - void solver::internalize_default(euf::enode* n) { - add_parent_default(n->get_arg(0)->get_th_var(get_id()), n); - set_prop_upward(n); - } - bool solver::visited(expr* e) { euf::enode* n = expr2enode(e); return n && n->is_attached_to(get_id()); @@ -124,40 +85,111 @@ namespace array { mk_var(n); for (auto* arg : euf::enode_args(n)) ensure_var(arg); - switch (a->get_decl_kind()) { - case OP_STORE: - internalize_store(n); + internalize_eh(n); + if (ctx.is_relevant(n)) + relevant_eh(n); + return true; + } + + void solver::internalize_lambda_eh(euf::enode* n) { + push_axiom(default_axiom(n)); + auto& d = get_var_data(find(n)); + ctx.push_vec(d.m_lambdas, n); + } + + void solver::internalize_eh(euf::enode* n) { + switch (n->get_decl()->get_decl_kind()) { + case OP_STORE: + ctx.push_vec(get_var_data(find(n)).m_lambdas, n); + push_axiom(store_axiom(n)); break; - case OP_SELECT: - internalize_select(n); + case OP_SELECT: break; case OP_AS_ARRAY: - case OP_CONST_ARRAY: - internalize_lambda(n); + case OP_CONST_ARRAY: + internalize_lambda_eh(n); break; - case OP_ARRAY_EXT: - internalize_ext(n); + case OP_ARRAY_EXT: + SASSERT(is_array(n->get_arg(0))); + push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1))); break; - case OP_ARRAY_DEFAULT: - internalize_default(n); + case OP_ARRAY_DEFAULT: + add_parent_default(find(n->get_arg(0)), n); break; - case OP_ARRAY_MAP: - internalize_map(n); + case OP_ARRAY_MAP: + case OP_SET_UNION: + case OP_SET_INTERSECT: + case OP_SET_DIFFERENCE: + case OP_SET_COMPLEMENT: + for (auto* arg : euf::enode_args(n)) + add_parent_lambda(find(arg), n); + internalize_lambda_eh(n); break; - case OP_SET_UNION: - case OP_SET_INTERSECT: - case OP_SET_DIFFERENCE: - case OP_SET_COMPLEMENT: - case OP_SET_SUBSET: - case OP_SET_HAS_SIZE: - case OP_SET_CARD: - ctx.unhandled_function(a->get_decl()); + case OP_SET_SUBSET: { + expr* x, *y; + VERIFY(a.is_subset(n->get_expr(), x, y)); + expr_ref diff(a.mk_setminus(x, y), m); + expr_ref emp(a.mk_empty_set(x->get_sort()), m); + sat::literal eq = eq_internalize(diff, emp); + sat::literal sub = expr2literal(n->get_expr()); + add_equiv(eq, sub); + break; + } + case OP_SET_HAS_SIZE: + case OP_SET_CARD: + ctx.unhandled_function(n->get_decl()); break; default: UNREACHABLE(); - break; + break; + } + } + + void solver::relevant_eh(euf::enode* n) { + if (is_lambda(n->get_expr())) { + set_prop_upward(find(n)); + return; + } + if (!is_app(n->get_expr())) + return; + if (n->get_decl()->get_family_id() != a.get_family_id()) + return; + switch (n->get_decl()->get_decl_kind()) { + case OP_STORE: + add_parent_lambda(find(n->get_arg(0)), n); + break; + case OP_SELECT: + add_parent_select(find(n->get_arg(0)), n); + break; + case OP_CONST_ARRAY: + case OP_AS_ARRAY: + set_prop_upward(find(n)); + propagate_parent_default(find(n)); + break; + case OP_ARRAY_EXT: + break; + case OP_ARRAY_DEFAULT: + set_prop_upward(find(n->get_arg(0))); + break; + case OP_ARRAY_MAP: + case OP_SET_UNION: + case OP_SET_INTERSECT: + case OP_SET_DIFFERENCE: + case OP_SET_COMPLEMENT: + for (auto* arg : euf::enode_args(n)) + set_prop_upward_store(arg); + set_prop_upward(find(n)); + break; + case OP_SET_SUBSET: + break; + case OP_SET_HAS_SIZE: + case OP_SET_CARD: + ctx.unhandled_function(n->get_decl()); + break; + default: + UNREACHABLE(); + break; } - return true; } /** diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index 15978747c..f2836d9aa 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -186,17 +186,16 @@ namespace array { if (should_set_prop_upward(d)) set_prop_upward(d); ctx.push_vec(d.m_lambdas, lambda); - if (should_set_prop_upward(d)) { - set_prop_upward(lambda); - propagate_select_axioms(d, lambda); - } + propagate_select_axioms(d, lambda); + if (should_set_prop_upward(d)) + set_prop_upward_store(lambda); } void solver::add_parent_lambda(theory_var v_child, euf::enode* lambda) { SASSERT(can_beta_reduce(lambda)); auto& d = get_var_data(find(v_child)); ctx.push_vec(d.m_parent_lambdas, lambda); - if (should_set_prop_upward(d)) + if (should_prop_upward(d)) propagate_select_axioms(d, lambda); } @@ -231,6 +230,9 @@ namespace array { for (euf::enode* lambda : d.m_lambdas) propagate_select_axioms(d, lambda); + if (!should_prop_upward(d)) + return; + for (euf::enode* lambda : d.m_parent_lambdas) propagate_select_axioms(d, lambda); } @@ -246,14 +248,14 @@ namespace array { set_prop_upward(d); } - void solver::set_prop_upward(euf::enode* n) { + void solver::set_prop_upward_store(euf::enode* n) { if (a.is_store(n->get_expr())) set_prop_upward(n->get_arg(0)->get_th_var(get_id())); } void solver::set_prop_upward(var_data& d) { for (auto* p : d.m_lambdas) - set_prop_upward(p); + set_prop_upward_store(p); } /** @@ -273,6 +275,6 @@ namespace array { } bool solver::can_beta_reduce(expr* c) const { - return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || a.is_map(c); + return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || is_map_combinator(c); } } diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index 0c0fc82d6..1c2935c99 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -66,6 +66,7 @@ namespace array { array_union_find m_find; theory_var find(theory_var v) { return m_find.find(v); } + theory_var find(euf::enode* n) { return find(n->get_th_var(get_id())); } func_decl_ref_vector const& sort2diff(sort* s); // internalize @@ -73,12 +74,8 @@ namespace array { bool visited(expr* e) override; bool post_visit(expr* e, bool sign, bool root) override; void ensure_var(euf::enode* n); - void internalize_store(euf::enode* n); - void internalize_select(euf::enode* n); - void internalize_lambda(euf::enode* n); - void internalize_ext(euf::enode* n); - void internalize_default(euf::enode* n); - void internalize_map(euf::enode* n); + void internalize_eh(euf::enode* n); + void internalize_lambda_eh(euf::enode* n); // axioms struct axiom_record { @@ -157,7 +154,6 @@ namespace array { bool assert_axiom(unsigned idx); bool assert_select(unsigned idx, axiom_record & r); bool assert_default(axiom_record & r); - bool is_relevant(axiom_record const& r) const; void set_applied(unsigned idx) { m_axiom_trail[idx].set_applied(); } bool is_applied(unsigned idx) const { return m_axiom_trail[idx].is_applied(); } bool is_delayed(unsigned idx) const { return m_axiom_trail[idx].is_delayed(); } @@ -185,7 +181,9 @@ namespace array { bool assert_congruent_axiom(expr* e1, expr* e2); bool add_delayed_axioms(); bool add_as_array_eqs(euf::enode* n); - + expr_ref apply_map(app* map, unsigned n, expr* const* args); + bool is_map_combinator(expr* e) const; + bool has_unitary_domain(app* array_term); bool has_large_domain(expr* array_term); std::pair mk_epsilon(sort* s); @@ -197,7 +195,7 @@ namespace array { // solving void add_parent_select(theory_var v_child, euf::enode* select); void add_parent_default(theory_var v_child, euf::enode* def); - void add_lambda(theory_var v, euf::enode* lambda); + void add_lambda(theory_var v, euf::enode* lambda); void add_parent_lambda(theory_var v_child, euf::enode* lambda); void propagate_select_axioms(var_data const& d, euf::enode* a); @@ -206,7 +204,7 @@ namespace array { void set_prop_upward(theory_var v); void set_prop_upward(var_data& d); - void set_prop_upward(euf::enode* n); + void set_prop_upward_store(euf::enode* n); unsigned get_lambda_equiv_size(var_data const& d) const; bool should_set_prop_upward(var_data const& d) const; bool should_prop_upward(var_data const& d) const; @@ -264,7 +262,9 @@ namespace array { void apply_sort_cnstr(euf::enode* n, sort* s) override; bool is_shared(theory_var v) const override; bool enable_self_propagate() const override { return true; } - + void relevant_eh(euf::enode* n) override; + bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_array(n->get_sort()); } + void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2); void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {} void unmerge_eh(theory_var v1, theory_var v2) {} diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp index ca4841656..6ad10c53a 100644 --- a/src/sat/smt/bv_delay_internalize.cpp +++ b/src/sat/smt/bv_delay_internalize.cpp @@ -21,7 +21,10 @@ Author: namespace bv { bool solver::check_delay_internalized(expr* e) { - if (!ctx.is_relevant(e)) + euf::enode* n = expr2enode(e); + if (!n) + return true; + if (!ctx.is_relevant(n)) return true; if (get_internalize_mode(e) != internalize_mode::delay_i) return true; @@ -247,7 +250,7 @@ namespace bv { return; expr_ref tmp = literal2expr(bits.back()); for (unsigned i = bits.size() - 1; i-- > 0; ) { - auto b = bits[i]; + sat::literal b = bits[i]; tmp = m.mk_or(literal2expr(b), tmp); xs.push_back(tmp); } diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 439764515..77115b441 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -166,6 +166,7 @@ namespace bv { #define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun); #define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin); #define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun); +#define if_unary(F) if (a->get_num_args() == 1) { internalize_un(F); break; } switch (a->get_decl_kind()) { case OP_BV_NUM: internalize_num(a); break; @@ -190,7 +191,7 @@ namespace bv { case OP_BXOR: internalize_ac(mk_xor); break; case OP_BNAND: internalize_bin(mk_nand); break; case OP_BNOR: internalize_bin(mk_nor); break; - case OP_BXNOR: internalize_bin(mk_xnor); break; + case OP_BXNOR: if_unary(mk_not); internalize_bin(mk_xnor); break; case OP_BCOMP: internalize_bin(mk_comp); break; case OP_SIGN_EXT: internalize_pun(mk_sign_extend); break; case OP_ZERO_EXT: internalize_pun(mk_zero_extend); break; @@ -426,7 +427,6 @@ namespace bv { expr_ref sum(m_autil.mk_add(sz, args.data()), m); sat::literal lit = eq_internalize(n, sum); add_unit(lit); - ctx.add_root(lit); } void solver::internalize_int2bv(app* n) { @@ -456,7 +456,6 @@ namespace bv { rhs = m_autil.mk_mod(e, m_autil.mk_int(mod)); sat::literal eq_lit = eq_internalize(lhs, rhs); add_unit(eq_lit); - ctx.add_root(eq_lit); expr_ref_vector n_bits(m); get_bits(n_enode, n_bits); @@ -469,7 +468,6 @@ namespace bv { lhs = n_bits.get(i); eq_lit = eq_internalize(lhs, rhs); add_unit(eq_lit); - ctx.add_root(eq_lit); } } @@ -535,7 +533,6 @@ namespace bv { if (p.hi_div0()) { eq_lit = eq_internalize(n, ibin(arg1, arg2)); add_unit(eq_lit); - ctx.add_root(eq_lit); } else { unsigned sz = bv.get_bv_size(n); @@ -653,7 +650,6 @@ namespace bv { mk_bits(get_th_var(e)); sat::literal eq_lit = eq_internalize(e, r); add_unit(eq_lit); - ctx.add_root(eq_lit); } void solver::internalize_bit2bool(app* n) { diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index 941b1e0ac..c8639e302 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -99,14 +99,38 @@ namespace euf { m_tmp_inference->init(m_tmp_inference); } + bool ackerman::enable_cc(app* a, app* b) { + if (!s.enable_ackerman_axioms(a)) + return false; + if (!s.enable_ackerman_axioms(b)) + return false; + for (expr* arg : *a) + if (!s.enable_ackerman_axioms(arg)) + return false; + for (expr* arg : *b) + if (!s.enable_ackerman_axioms(arg)) + return false; + return true; + } + + bool ackerman::enable_eq(expr* a, expr* b, expr* c) { + return s.enable_ackerman_axioms(a) && + s.enable_ackerman_axioms(b) && + s.enable_ackerman_axioms(c); + } + void ackerman::cg_conflict_eh(expr * n1, expr * n2) { if (!is_app(n1) || !is_app(n2)) return; + if (!s.enable_ackerman_axioms(n1)) + return; SASSERT(!s.m_drating); app* a = to_app(n1); app* b = to_app(n2); if (a->get_decl() != b->get_decl() || a->get_num_args() != b->get_num_args()) return; + if (!enable_cc(a, b)) + return; TRACE("ack", tout << "conflict eh: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";); insert(a, b); gc(); @@ -117,6 +141,8 @@ namespace euf { return; if (s.m_drating) return; + if (!enable_eq(a, b, c)) + return; TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";); insert(a, b, c); gc(); @@ -128,6 +154,8 @@ namespace euf { TRACE("ack", tout << "used cc: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";); SASSERT(a->get_decl() == b->get_decl()); SASSERT(a->get_num_args() == b->get_num_args()); + if (!enable_cc(a, b)) + return; insert(a, b); gc(); } @@ -173,13 +201,13 @@ namespace euf { app* b = to_app(_b); TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";); sat::literal_vector lits; - unsigned sz = a->get_num_args(); + unsigned sz = a->get_num_args(); for (unsigned i = 0; i < sz; ++i) { - expr_ref eq(m.mk_eq(a->get_arg(i), b->get_arg(i)), m); + expr_ref eq = s.mk_eq(a->get_arg(i), b->get_arg(i)); lits.push_back(~s.mk_literal(eq)); } - expr_ref eq(m.mk_eq(a, b), m); + expr_ref eq = s.mk_eq(a, b); lits.push_back(s.mk_literal(eq)); s.s().mk_clause(lits, sat::status::th(true, m.get_basic_family_id())); } @@ -187,9 +215,9 @@ namespace euf { void ackerman::add_eq(expr* a, expr* b, expr* c) { flet _is_redundant(s.m_is_redundant, true); sat::literal lits[3]; - expr_ref eq1(m.mk_eq(a, c), m); - expr_ref eq2(m.mk_eq(b, c), m); - expr_ref eq3(m.mk_eq(a, b), m); + expr_ref eq1(s.mk_eq(a, c), m); + expr_ref eq2(s.mk_eq(b, c), m); + expr_ref eq3(s.mk_eq(a, b), m); TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";); lits[0] = ~s.mk_literal(eq1); lits[1] = ~s.mk_literal(eq2); diff --git a/src/sat/smt/euf_ackerman.h b/src/sat/smt/euf_ackerman.h index 7b9c4c3d9..479ad2933 100644 --- a/src/sat/smt/euf_ackerman.h +++ b/src/sat/smt/euf_ackerman.h @@ -70,6 +70,9 @@ namespace euf { void add_cc(expr* a, expr* b); void add_eq(expr* a, expr* b, expr* c); void gc(); + bool enable_cc(app* a, app* b); + bool enable_eq(expr* a, expr* b, expr* c); + public: ackerman(solver& s, ast_manager& m); diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 90a268661..51f342fe1 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -162,10 +162,8 @@ namespace euf { sat::literal lit2 = literal(v, false); s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); - if (relevancy_enabled()) { - add_aux(~lit, lit2); - add_aux(lit, ~lit2); - } + add_aux(~lit, lit2); + add_aux(lit, ~lit2); lit = lit2; } @@ -185,8 +183,6 @@ namespace euf { m_egraph.set_bool_var(n, v); if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e)) m_egraph.set_merge_enabled(n, false); - if (!si.is_bool_op(e)) - track_relevancy(lit.var()); if (s().value(lit) != l_undef) m_egraph.set_value(n, s().value(lit)); return lit; @@ -224,9 +220,8 @@ namespace euf { lits.push_back(lit); } } + add_root(lits); s().mk_clause(lits, st); - if (relevancy_enabled()) - add_root(lits); } else { // g(f(x_i)) = x_i @@ -244,15 +239,13 @@ namespace euf { expr_ref gapp(m.mk_app(g, fapp.get()), m); expr_ref eq = mk_eq(gapp, arg); sat::literal lit = mk_literal(eq); - s().add_clause(1, &lit, st); + s().add_clause(lit, st); eqs.push_back(mk_eq(fapp, a)); } pb_util pb(m); expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m); sat::literal lit = si.internalize(at_least2, m_is_redundant); - s().mk_clause(1, &lit, st); - if (relevancy_enabled()) - add_root(1, &lit); + s().add_clause(lit, st); } } @@ -268,9 +261,7 @@ namespace euf { for (unsigned j = i + 1; j < sz; ++j) { expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr()); sat::literal lit = ~mk_literal(eq); - s().add_clause(1, &lit, st); - if (relevancy_enabled()) - add_root(1, &lit); + s().add_clause(lit, st); } } } @@ -287,9 +278,7 @@ namespace euf { n->mark_interpreted(); expr_ref eq = mk_eq(fapp, fresh); sat::literal lit = mk_literal(eq); - s().add_clause(1, &lit, st); - if (relevancy_enabled()) - add_root(1, &lit); + s().add_clause(lit, st); } } } @@ -302,16 +291,16 @@ namespace euf { expr_ref eq_th = mk_eq(e, th); sat::literal lit_th = mk_literal(eq_th); if (th == el) { - s().add_clause(1, &lit_th, st); + s().add_clause(lit_th, st); } else { sat::literal lit_c = mk_literal(c); expr_ref eq_el = mk_eq(e, el); sat::literal lit_el = mk_literal(eq_el); - literal lits1[2] = { ~lit_c, lit_th }; - literal lits2[2] = { lit_c, lit_el }; - s().add_clause(2, lits1, st); - s().add_clause(2, lits2, st); + add_root(~lit_c, lit_th); + add_root(lit_c, lit_el); + s().add_clause(~lit_c, lit_th, st); + s().add_clause(lit_c, lit_el, st); } } else if (m.is_distinct(e)) { @@ -326,10 +315,10 @@ namespace euf { expr_ref fml(m.mk_or(eqs), m); sat::literal dist(si.to_bool_var(e), false); sat::literal some_eq = si.internalize(fml, m_is_redundant); - sat::literal lits1[2] = { ~dist, ~some_eq }; - sat::literal lits2[2] = { dist, some_eq }; - s().add_clause(2, lits1, st); - s().add_clause(2, lits2, st); + add_root(~dist, ~some_eq); + add_root(dist, some_eq); + s().add_clause(~dist, ~some_eq, st); + s().add_clause(dist, some_eq, st); } else if (m.is_eq(e, th, el) && !m.is_iff(e)) { sat::literal lit1 = expr2literal(e); @@ -338,10 +327,10 @@ namespace euf { enode* n2 = m_egraph.find(e2); if (n2) { sat::literal lit2 = expr2literal(e2); - sat::literal lits1[2] = { ~lit1, lit2 }; - sat::literal lits2[2] = { lit1, ~lit2 }; - s().add_clause(2, lits1, st); - s().add_clause(2, lits2, st); + add_root(~lit1, lit2); + add_root(lit1, ~lit2); + s().add_clause(~lit1, lit2, st); + s().add_clause(lit1, ~lit2, st); } } } @@ -357,7 +346,7 @@ namespace euf { // contains a parent application. family_id th_id = m.get_basic_family_id(); - for (auto p : euf::enode_th_vars(n)) { + for (auto const& p : euf::enode_th_vars(n)) { family_id id = p.get_id(); if (m.get_basic_family_id() != id) { if (th_id != m.get_basic_family_id()) @@ -402,7 +391,7 @@ namespace euf { // Remark: The inconsistency is not going to be detected if they are // not marked as shared. - for (auto p : euf::enode_th_vars(n)) + for (auto const& p : euf::enode_th_vars(n)) if (fid2solver(p.get_id())->is_shared(p.get_var())) return true; diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index ea5bfe274..9540cd016 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -35,7 +35,7 @@ namespace euf { s(s), m(s.m), mdl(mdl), values(values), factory(m) {} ~user_sort() { - for (auto kv : sort2values) + for (auto const& kv : sort2values) mdl->register_usort(kv.m_key, kv.m_value->size(), kv.m_value->data()); } @@ -161,10 +161,9 @@ namespace euf { default: break; } - if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id()) - continue; sat::bool_var v = get_enode(e)->bool_var(); - SASSERT(v != sat::null_bool_var); + if (v == sat::null_bool_var) + continue; switch (s().value(v)) { case l_true: m_values.set(id, m.mk_true()); @@ -200,6 +199,8 @@ namespace euf { expr* e = n->get_expr(); if (!is_app(e)) continue; + if (!is_relevant(n)) + continue; app* a = to_app(e); func_decl* f = a->get_decl(); if (!include_func_interp(f)) @@ -224,7 +225,7 @@ namespace euf { enode* earg = get_enode(arg); expr* val = m_values.get(earg->get_root_id()); args.push_back(val); - CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n";); + CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n" << bpp(n) << "\n"; display(tout);); SASSERT(val); } SASSERT(args.size() == arity); @@ -259,7 +260,7 @@ namespace euf { if (n->is_root() && m_values.get(n->get_expr_id())) m_values2root.insert(m_values.get(n->get_expr_id()), n); TRACE("model", - for (auto kv : m_values2root) + for (auto const& kv : m_values2root) tout << mk_bounded_pp(kv.m_key, m) << "\n -> " << bpp(kv.m_value) << "\n";); return m_values2root; @@ -271,6 +272,8 @@ namespace euf { void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) { out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n"; + s().display(out); + return; euf::enode_vector nodes; nodes.push_back(n); for (unsigned i = 0; i < nodes.size(); ++i) { @@ -289,7 +292,6 @@ namespace euf { for (euf::enode* r : nodes) r->unmark1(); out << mdl << "\n"; - s().display(out); } void solver::validate_model(model& mdl) { @@ -297,6 +299,8 @@ namespace euf { ev.set_model_completion(true); TRACE("model", for (enode* n : m_egraph.nodes()) { + if (!is_relevant(n)) + continue; unsigned id = n->get_root_id(); expr* val = m_values.get(id, nullptr); if (!val) @@ -322,6 +326,8 @@ namespace euf { IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n);); CTRACE("euf", first, display_validation_failure(tout, mdl, n);); (void)first; + first = false; + return; exit(1); first = false; } diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp index 40dff962a..73fe49506 100644 --- a/src/sat/smt/euf_relevancy.cpp +++ b/src/sat/smt/euf_relevancy.cpp @@ -3,157 +3,326 @@ Copyright (c) 2020 Microsoft Corporation Module Name: - euf_relevancy.cpp + smt_relevant.cpp Abstract: - Features for relevancy tracking. - A reduced (minimal) implicant is extracted by running a dual solver. - Then the literals in the implicant are used as a basis for marking - subterms relevant. + Relevancy propagation Author: - Nikolaj Bjorner (nbjorner) 2020-09-22 + Nikolaj Bjorner (nbjorner) 2021-12-27 --*/ - +#include "sat/sat_solver.h" #include "sat/smt/euf_solver.h" +#include "sat/smt/euf_relevancy.h" + namespace euf { - - void solver::add_auto_relevant(expr* e) { - if (!relevancy_enabled()) - return; - for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes) - m_auto_relevant_lim.push_back(m_auto_relevant.size()); - // std::cout << "add-auto " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; - m_auto_relevant.push_back(e); - } - void solver::pop_relevant(unsigned n) { - if (m_auto_relevant_scopes >= n) { - m_auto_relevant_scopes -= n; + void relevancy::pop(unsigned n) { + if (!m_enabled) + return; + if (n <= m_num_scopes) { + m_num_scopes -= n; return; } - n -= m_auto_relevant_scopes; - m_auto_relevant_scopes = 0; - unsigned top = m_auto_relevant_lim.size() - n; - unsigned lim = m_auto_relevant_lim[top]; - m_auto_relevant_lim.shrink(top); - m_auto_relevant.shrink(lim); + else if (m_num_scopes > 0) { + n -= m_num_scopes; + m_num_scopes = 0; + } + SASSERT(n > 0); + unsigned sz = m_lim[m_lim.size() - n]; + for (unsigned i = m_trail.size(); i-- > sz; ) { + auto const& [u, idx] = m_trail[i]; + switch (u) { + case update::relevant_var: + m_relevant_var_ids[idx] = false; + break; + case update::add_queue: + m_queue.pop_back(); + break; + case update::add_clause: { + sat::clause* c = m_clauses.back(); + for (sat::literal lit : *c) { + SASSERT(m_occurs[lit.index()].back() == m_clauses.size() - 1); + m_occurs[lit.index()].pop_back(); + } + m_clauses.pop_back(); + m_roots.pop_back(); + m_alloc.del_clause(c); + break; + } + case update::set_root: + m_roots[idx] = false; + break; + case update::set_qhead: + m_qhead = idx; + break; + default: + UNREACHABLE(); + break; + } + } + m_trail.shrink(sz); + m_lim.shrink(m_lim.size() - n); } - void solver::push_relevant() { - ++m_auto_relevant_scopes; - } - - bool solver::is_relevant(expr* e) const { - return m_relevant_expr_ids.get(e->get_id(), true); - } - - bool solver::is_relevant(enode* n) const { - return m_relevant_expr_ids.get(n->get_expr_id(), true); - } - - void solver::ensure_dual_solver() { - if (m_dual_solver) + void relevancy::add_root(unsigned n, sat::literal const* lits) { + if (!m_enabled) return; - m_dual_solver = alloc(sat::dual_solver, s().rlimit()); - for (unsigned i = s().num_user_scopes(); i-- > 0; ) - m_dual_solver->push(); + flush(); + TRACE("relevancy", tout << "root " << sat::literal_vector(n, lits) << "\n"); + sat::literal true_lit = sat::null_literal; + for (unsigned i = 0; i < n; ++i) { + if (ctx.s().value(lits[i]) == l_true) { + if (is_relevant(lits[i])) + return; + true_lit = lits[i]; + } + } + if (true_lit != sat::null_literal) { + mark_relevant(true_lit); + return; + } + + sat::clause* cl = m_alloc.mk_clause(n, lits, false); + unsigned sz = m_clauses.size(); + m_clauses.push_back(cl); + m_roots.push_back(true); + m_trail.push_back(std::make_pair(update::add_clause, 0)); + for (sat::literal lit : *cl) { + ctx.s().set_external(lit.var()); + occurs(lit).push_back(sz); + } + } + + void relevancy::add_def(unsigned n, sat::literal const* lits) { + if (!m_enabled) + return; + flush(); + TRACE("relevancy", tout << "def " << sat::literal_vector(n, lits) << "\n"); + for (unsigned i = 0; i < n; ++i) { + if (ctx.s().value(lits[i]) == l_false && is_relevant(lits[i])) { + add_root(n, lits); + return; + } + } + sat::clause* cl = m_alloc.mk_clause(n, lits, false); + unsigned sz = m_clauses.size(); + m_clauses.push_back(cl); + m_roots.push_back(false); + m_trail.push_back(std::make_pair(update::add_clause, 0)); + for (sat::literal lit : *cl) { + ctx.s().set_external(lit.var()); + occurs(lit).push_back(sz); + } + } + + void relevancy::add_to_propagation_queue(sat::literal lit) { + m_trail.push_back(std::make_pair(update::add_queue, lit.var())); + m_queue.push_back(std::make_pair(lit, nullptr)); + } + + void relevancy::set_relevant(sat::literal lit) { + euf::enode* n = ctx.bool_var2enode(lit.var()); + if (n) + mark_relevant(n); + m_relevant_var_ids.setx(lit.var(), true, false); + m_trail.push_back(std::make_pair(update::relevant_var, lit.var())); + } + + void relevancy::set_asserted(sat::literal lit) { + SASSERT(!is_relevant(lit)); + SASSERT(ctx.s().value(lit) == l_true); + set_relevant(lit); + add_to_propagation_queue(lit); + ctx.asserted(lit); } /** - * Add a root clause. Root clauses must all be satisfied by the - * final assignment. If a clause is added above search level it - * is subject to removal on backtracking. These clauses are therefore - * not tracked. - */ - void solver::add_root(unsigned n, sat::literal const* lits) { - if (!relevancy_enabled()) + * Boolean variable is set relevant because an E-node is relevant. + * + */ + void relevancy::relevant_eh(sat::bool_var v) { + if (is_relevant(v)) return; - ensure_dual_solver(); - m_dual_solver->add_root(n, lits); - } - - void solver::add_aux(unsigned n, sat::literal const* lits) { - if (!relevancy_enabled()) - return; - ensure_dual_solver(); - m_dual_solver->add_aux(n, lits); - } - - void solver::track_relevancy(sat::bool_var v) { - ensure_dual_solver(); - m_dual_solver->track_relevancy(v); - } - - bool solver::init_relevancy() { - m_relevant_expr_ids.reset(); - if (!relevancy_enabled()) - return true; - if (!m_dual_solver) - return true; - if (!(*m_dual_solver)(s())) - return false; - unsigned max_id = 0; - for (enode* n : m_egraph.nodes()) - max_id = std::max(max_id, n->get_expr_id()); - m_relevant_expr_ids.resize(max_id + 1, false); - ptr_vector& todo = m_relevant_todo; - bool_vector& visited = m_relevant_visited; - auto const& core = m_dual_solver->core(); - todo.reset(); - for (auto lit : core) { - expr* e = m_bool_var2expr.get(lit.var(), nullptr); - if (e) - todo.push_back(e); + sat::literal lit(v); + switch (ctx.s().value(lit)) { + case l_undef: + set_relevant(lit); + break; + case l_true: + set_asserted(lit); + break; + case l_false: + set_asserted(~lit); + break; } -#if 0 - std::cout << "init-relevant\n"; - for (expr* e : m_auto_relevant) - std::cout << "auto-relevant " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; -#endif - todo.append(m_auto_relevant); - for (unsigned i = 0; i < todo.size(); ++i) { - expr* e = todo[i]; - if (visited.get(e->get_id(), false)) + } + + void relevancy::asserted(sat::literal lit) { + TRACE("relevancy", tout << "asserted " << lit << " relevant " << is_relevant(lit) << "\n"); + if (!m_enabled) + return; + flush(); + if (is_relevant(lit)) { + add_to_propagation_queue(lit); + return; + } + if (ctx.s().lvl(lit) <= ctx.s().search_lvl()) { + set_relevant(lit); + add_to_propagation_queue(lit); + return; + } + + for (auto idx : occurs(lit)) { + if (!m_roots[idx]) continue; - visited.setx(e->get_id(), true, false); - if (!si.is_bool_op(e)) - m_relevant_expr_ids.setx(e->get_id(), true, false); - if (!is_app(e)) + for (sat::literal lit2 : *m_clauses[idx]) + if (lit2 != lit && ctx.s().value(lit2) == l_true && is_relevant(lit2)) + goto next; + set_relevant(lit); + add_to_propagation_queue(lit); + return; + next: + ; + } + } + + void relevancy::propagate() { + if (!m_enabled) + return; + flush(); + if (m_qhead == m_queue.size()) + return; + m_trail.push_back(std::make_pair(update::set_qhead, m_qhead)); + while (m_qhead < m_queue.size() && !ctx.s().inconsistent() && ctx.get_manager().inc()) { + auto const& [lit, n] = m_queue[m_qhead++]; + SASSERT(n || lit != sat::null_literal); + SASSERT(!n || lit == sat::null_literal); + if (n) + propagate_relevant(n); + else + propagate_relevant(lit); + } + } + + void relevancy::merge(euf::enode* root, euf::enode* other) { + TRACE("relevancy", tout << "merge #" << ctx.bpp(root) << " " << is_relevant(root) << " #" << ctx.bpp(other) << " " << is_relevant(other) << "\n"); + if (is_relevant(root)) + mark_relevant(other); + else if (is_relevant(other)) + mark_relevant(root); + } + + void relevancy::mark_relevant(euf::enode* n) { + if (!m_enabled) + return; + flush(); + if (is_relevant(n)) + return; + TRACE("relevancy", tout << "mark #" << ctx.bpp(n) << "\n"); + m_trail.push_back(std::make_pair(update::add_queue, 0)); + m_queue.push_back(std::make_pair(sat::null_literal, n)); + } + + void relevancy::mark_relevant(sat::literal lit) { + TRACE("relevancy", tout << "mark " << lit << " " << is_relevant(lit) << " " << ctx.s().value(lit) << " lim: " << m_lim.size() << "\n"); + if (!m_enabled) + return; + flush(); + if (is_relevant(lit)) + return; + set_relevant(lit); + switch (ctx.s().value(lit)) { + case l_true: + break; + case l_false: + lit.neg(); + break; + default: + return; + } + add_to_propagation_queue(lit); + } + + void relevancy::propagate_relevant(sat::literal lit) { + SASSERT(m_num_scopes == 0); + TRACE("relevancy", tout << "propagate " << lit << " lim: " << m_lim.size() << "\n"); + SASSERT(ctx.s().value(lit) == l_true); + SASSERT(is_relevant(lit)); + euf::enode* n = ctx.bool_var2enode(lit.var()); + if (n && !ctx.get_si().is_bool_op(n->get_expr())) + return; + for (auto idx : occurs(~lit)) { + if (m_roots[idx]) continue; - expr* c = nullptr, *th = nullptr, *el = nullptr; - if (m.is_ite(e, c, th, el) && get_enode(c)) { - sat::literal lit = expr2literal(c); - todo.push_back(c); - switch (s().value(lit)) { - case l_true: - todo.push_back(th); - break; - case l_false: - todo.push_back(el); - break; - default: - todo.push_back(th); - todo.push_back(el); - break; + sat::clause* cl = m_clauses[idx]; + sat::literal true_lit = sat::null_literal; + for (sat::literal lit2 : *cl) { + if (ctx.s().value(lit2) == l_true) { + if (is_relevant(lit2)) + goto next; + true_lit = lit2; } - continue; } - for (expr* arg : *to_app(e)) - todo.push_back(arg); + + if (true_lit != sat::null_literal) + set_asserted(true_lit); + else { + m_trail.push_back(std::make_pair(update::set_root, idx)); + m_roots[idx] = true; + } + next: + TRACE("relevancy", tout << "propagate " << lit << " " << true_lit << " " << m_roots[idx] << "\n"); + ; } - - for (auto * e : todo) - visited[e->get_id()] = false; - - TRACE("euf", - for (enode* n : m_egraph.nodes()) - if (is_relevant(n)) - tout << "relevant " << n->get_expr_id() << " [r" << n->get_root_id() << "]: " << mk_bounded_pp(n->get_expr(), m) << "\n";); - return true; } + + void relevancy::propagate_relevant(euf::enode* n) { + m_todo.push_back(n); + while (!m_todo.empty()) { + n = m_todo.back(); + m_todo.pop_back(); + TRACE("relevancy", tout << "propagate #" << ctx.bpp(n) << " lim: " << m_lim.size() << "\n"); + if (n->is_relevant()) + continue; + m_stack.push_back(n); + while (!m_stack.empty()) { + n = m_stack.back(); + unsigned sz = m_stack.size(); + bool is_bool_op = ctx.get_si().is_bool_op(n->get_expr()); + if (!is_bool_op) + for (euf::enode* arg : euf::enode_args(n)) + if (!arg->is_relevant()) + m_stack.push_back(arg); + if (sz != m_stack.size()) + continue; + if (!n->is_relevant()) { + ctx.get_egraph().set_relevant(n); + ctx.relevant_eh(n); + sat::bool_var v = n->bool_var(); + if (v != sat::null_bool_var) + relevant_eh(v); + for (euf::enode* sib : euf::enode_class(n)) + if (!sib->is_relevant()) + m_todo.push_back(sib); + } + if (!ctx.get_manager().inc()) { + m_todo.reset(); + m_stack.reset(); + return; + } + m_stack.pop_back(); + } + } + } + + void relevancy::set_enabled(bool e) { + m_enabled = e; + ctx.get_egraph().set_default_relevant(!e); + } + } diff --git a/src/sat/smt/euf_relevancy.h b/src/sat/smt/euf_relevancy.h new file mode 100644 index 000000000..382b054fc --- /dev/null +++ b/src/sat/smt/euf_relevancy.h @@ -0,0 +1,173 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + smt_relevant.h + +Abstract: + + Relevancy propagation + +Author: + + Nikolaj Bjorner (nbjorner) 2021-12-27 + + +Clauses are split into two parts: + +- Roots +- Defs + +The goal is to establish a labeling of literals as "relevant" such that +- the set of relevant literals satisfies Roots +- there is a set of blocked literals that can be used to satisfy the clauses in Defs + independent of their real assignment. + +The idea is that the Defs clauses are obtained from Tseitin transformation so they can be +grouped by the blocked literal that was used to introduce them. +For example, when clausifying (and a b) we have the clauses +(=> (and a b) a) +(=> (and a b) b) +(or (not a) (not b) (and a b)) +then the literal for "(and a b)" is blocked. +And recursively for clauses introduced for a, b if they use a Boolean connectives +at top level. + +The state transitions are: + +- A literal lit is assigned: + lit appears positively in a Root clause R and no other literal in R are relevant. + -> + lit is set relevant + + lit is justified at search level + -> + lit is set relevant + +- An equality n1 = n2 is assigned: + n1 is relevant + -> + n2 is marked as relevant + +- A lit is set relevant: + -> + all clauses D in Defs where lit appears negatively are added to Roots + +- When a clause R is added to Roots: + R contains a positive literal lit that is relevant + -> + skip adding R to Roots + +- When a clause R is added to Roots: + R contains a positive literal lit, no positive literal in R are relevant + -> + lit is set relevant + +- When a clause D is added to Defs: + D contains a negative literal that is relevant + -> + Add D to Roots + +- When an expression is set relevant: + All non-relevant children above Boolean connectives are set relevant + If nodes are treated as Boolean connectives because they are clausified + to (=> cond (= n then)) and (=> (not cond) (= n else)) + +Replay: + - literals that are replayed in clauses that are marked relevant are + marked relevant again. + + - expressions corresponding to auxiliary clauses are added as auxiliary clauses. + + - TBD: Are root clauses added under a scope discarded? + The SAT solver re-initializes clauses on its own, should we just use this mechanism? + +Can a literal that is not in a root be set relevant? + - yes, if we propagate over expressions + +Do we need full watch lists instead of 2-watch lists? + - probably, but unclear. The dual SAT solver only uses 2-watch lists, but uses a large clause for tracking + roots. + + + State machine for literals: relevant(lit), assigned(lit) + +relevant(lit) transitions false -> true + if assigned(lit): add to propagation queue + if not assigned(lit): no-op (or mark enodes as relevant) + +assigned(lit) transitions false -> true + if relevant(lit): add to propagation queue + if not relevant(lit): set relevant if member of root, add to propagation queue + + +--*/ +#pragma once +#include "sat/sat_solver.h" +#include "sat/smt/sat_th.h" + + +namespace euf { + + class solver; + + class relevancy { + euf::solver& ctx; + + enum class update { relevant_var, add_queue, add_clause, set_root, set_qhead }; + + bool m_enabled = false; + svector> m_trail; + unsigned_vector m_lim; + unsigned m_num_scopes = 0; + bool_vector m_relevant_var_ids; // identifiers of relevant Boolean variables + sat::clause_allocator m_alloc; + sat::clause_vector m_clauses; // clauses + bool_vector m_roots; // indicate if clause is a root + vector m_occurs; // where do literals occur + unsigned m_qhead = 0; // queue head for relevancy + svector> m_queue; // propagation queue for relevancy + euf::enode_vector m_stack, m_todo; + + void push_core() { m_lim.push_back(m_trail.size()); } + void flush() { for (; m_num_scopes > 0; --m_num_scopes) push_core(); } + + unsigned_vector& occurs(sat::literal lit) { m_occurs.reserve(lit.index() + 1); return m_occurs[lit.index()]; } + + void propagate_relevant(sat::literal lit); + + void add_to_propagation_queue(sat::literal lit); + + void set_relevant(sat::literal lit); + + void set_asserted(sat::literal lit); + + void relevant_eh(sat::bool_var v); + + void propagate_relevant(euf::enode* n); + + public: + relevancy(euf::solver& ctx): ctx(ctx) {} + + void push() { if (m_enabled) ++m_num_scopes; } + void pop(unsigned n); + + void add_root(unsigned n, sat::literal const* lits); + void add_def(unsigned n, sat::literal const* lits); + void asserted(sat::literal lit); + void propagate(); + bool can_propagate() const { return m_qhead < m_queue.size(); } + + void mark_relevant(euf::enode* n); + void mark_relevant(sat::literal lit); + void merge(euf::enode* n1, euf::enode* n2); + + bool is_relevant(sat::bool_var v) const { return !m_enabled || m_relevant_var_ids.get(v, false); } + bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); } + bool is_relevant(euf::enode* n) const { return !m_enabled || n->is_relevant(); } + + bool enabled() const { return m_enabled; } + void set_enabled(bool e); + }; +} diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index bbdd6ce0e..bb2d61b0a 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -41,6 +41,7 @@ namespace euf { extension(symbol("euf"), m.mk_family_id("euf")), m(m), si(si), + m_relevancy(*this), m_egraph(m), m_trail(), m_rewriter(m), @@ -51,12 +52,21 @@ namespace euf { m_values(m) { updt_params(p); + m_relevancy.set_enabled(get_config().m_relevancy_lvl > 2); std::function disp = [&](std::ostream& out, void* j) { display_justification_ptr(out, reinterpret_cast(j)); }; m_egraph.set_display_justification(disp); + + if (m_relevancy.enabled()) { + std::function on_merge = + [&](enode* root, enode* other) { + m_relevancy.merge(root, other); + }; + m_egraph.set_on_merge(on_merge); + } } void solver::updt_params(params_ref const& p) { @@ -183,7 +193,7 @@ namespace euf { } void solver::propagate(literal lit, ext_justification_idx idx) { - add_auto_relevant(bool_var2expr(lit.var())); + mark_relevant(lit); s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx)); } @@ -286,6 +296,11 @@ namespace euf { } void solver::asserted(literal l) { + + m_relevancy.asserted(l); + if (!m_relevancy.is_relevant(l)) + return; + expr* e = m_bool_var2expr.get(l.var(), nullptr); TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";); if (!e) @@ -329,6 +344,8 @@ namespace euf { bool solver::unit_propagate() { bool propagated = false; while (!s().inconsistent()) { + if (m_relevancy.enabled()) + m_relevancy.propagate(); if (m_egraph.inconsistent()) { unsigned lvl = s().scope_lvl(); s().set_conflict(sat::justification::mk_ext_justification(lvl, conflict_constraint().to_index())); @@ -345,9 +362,13 @@ namespace euf { if (m_solvers[i]->unit_propagate()) propagated1 = true; - if (!propagated1) - break; - propagated = true; + if (propagated1) { + propagated = true; + continue; + } + if (m_relevancy.enabled() && m_relevancy.can_propagate()) + continue; + break; } DEBUG_CODE(if (!propagated && !s().inconsistent()) check_missing_eq_propagation();); return propagated; @@ -422,12 +443,10 @@ namespace euf { void solver::propagate_th_eqs() { for (; m_egraph.has_th_eq() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_th_eq()) { th_eq eq = m_egraph.get_th_eq(); - if (eq.is_eq()) { - if (!is_self_propagated(eq)) - m_id2solver[eq.id()]->new_eq_eh(eq); - } - else + if (!eq.is_eq()) m_id2solver[eq.id()]->new_diseq_eh(eq); + else if (!is_self_propagated(eq)) + m_id2solver[eq.id()]->new_eq_eh(eq); } } @@ -458,9 +477,6 @@ namespace euf { if (unit_propagate()) return sat::check_result::CR_CONTINUE; - - if (!init_relevancy()) - give_up = true; unsigned num_nodes = m_egraph.num_nodes(); auto apply_solver = [&](th_solver* e) { @@ -525,9 +541,7 @@ namespace euf { for (auto* e : m_solvers) e->push(); m_egraph.push(); - if (m_dual_solver) - m_dual_solver->push(); - push_relevant(); + m_relevancy.push(); } void solver::pop(unsigned n) { @@ -537,7 +551,7 @@ namespace euf { e->pop(n); si.pop(n); m_egraph.pop(n); - pop_relevant(n); + m_relevancy.pop(n); scope const & sc = m_scopes[m_scopes.size() - n]; for (unsigned i = m_var_trail.size(); i-- > sc.m_var_lim; ) { bool_var v = m_var_trail[i]; @@ -546,8 +560,6 @@ namespace euf { } m_var_trail.shrink(sc.m_var_lim); m_scopes.shrink(m_scopes.size() - n); - if (m_dual_solver) - m_dual_solver->pop(n); SASSERT(m_egraph.num_scopes() == m_scopes.size()); TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n");); } @@ -720,6 +732,35 @@ namespace euf { } } + bool solver::is_relevant(bool_var v) const { + if (m_relevancy.enabled()) + return m_relevancy.is_relevant(v); + auto* e = bool_var2enode(v); + return !e || is_relevant(e); + } + + void solver::relevant_eh(euf::enode* n) { + if (m_qsolver) + m_qsolver->relevant_eh(n); + for (auto const& thv : enode_th_vars(n)) { + auto* th = m_id2solver.get(thv.get_id(), nullptr); + if (th && th != m_qsolver) + th->relevant_eh(n); + } + } + + bool solver::enable_ackerman_axioms(expr* e) const { + euf::enode* n = get_enode(e); + if (!n) + return false; + for (auto const& thv : enode_th_vars(n)) { + auto* th = m_id2solver.get(thv.get_id(), nullptr); + if (th && !th->enable_ackerman_axioms(n)) + return false; + } + return true; + } + void solver::pre_simplify() { for (auto* e : m_solvers) e->pre_simplify(); @@ -765,6 +806,8 @@ namespace euf { } bool solver::set_root(literal l, literal r) { + if (m_relevancy.enabled()) + return false; expr* e = bool_var2expr(l.var()); if (!e) return true; @@ -794,7 +837,7 @@ namespace euf { out << "bool-vars\n"; for (unsigned v : m_var_trail) { expr* e = m_bool_var2expr[v]; - out << v << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n"; + out << v << (is_relevant(v)?"":"n") << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n"; } for (auto* e : m_solvers) e->display(out); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 384e15822..859c0640c 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -25,11 +25,12 @@ Author: #include "sat/sat_extension.h" #include "sat/smt/atom2bool_var.h" #include "sat/smt/sat_th.h" -#include "sat/smt/sat_dual_solver.h" #include "sat/smt/euf_ackerman.h" #include "sat/smt/user_solver.h" +#include "sat/smt/euf_relevancy.h" #include "smt/params/smt_params.h" + namespace euf { typedef sat::literal literal; typedef sat::ext_constraint_idx ext_constraint_idx; @@ -91,6 +92,7 @@ namespace euf { std::function<::solver*(void)> m_mk_solver; ast_manager& m; sat::sat_internalizer& si; + relevancy m_relevancy; smt_params m_config; euf::egraph m_egraph; trail_stack m_trail; @@ -181,17 +183,17 @@ namespace euf { void init_drat(); // relevancy - bool_vector m_relevant_expr_ids; - bool_vector m_relevant_visited; - ptr_vector m_relevant_todo; - void ensure_dual_solver(); - bool init_relevancy(); - - + //bool_vector m_relevant_expr_ids; + //bool_vector m_relevant_visited; + //ptr_vector m_relevant_todo; + //void init_relevant_expr_ids(); + //void push_relevant(sat::bool_var v); + bool is_propagated(sat::literal lit); // invariant void check_eqc_bool_assignment() const; void check_missing_bool_enode_propagation() const; void check_missing_eq_propagation() const; + // diagnosis std::ostream& display_justification_ptr(std::ostream& out, size_t* j) const; @@ -250,6 +252,10 @@ namespace euf { sat::sat_internalizer& get_si() { return si; } ast_manager& get_manager() { return m; } enode* get_enode(expr* e) const { return m_egraph.find(e); } + enode* bool_var2enode(sat::bool_var b) const { + expr* e = m_bool_var2expr.get(b, nullptr); + return e ? get_enode(e) : nullptr; + } sat::literal expr2literal(expr* e) const { return enode2literal(get_enode(e)); } sat::literal enode2literal(enode* n) const { return sat::literal(n->bool_var(), false); } lbool value(enode* n) const { return s().value(enode2literal(n)); } @@ -362,32 +368,28 @@ namespace euf { th_rewriter& get_rewriter() { return m_rewriter; } void rewrite(expr_ref& e) { m_rewriter(e); } bool is_shared(euf::enode* n) const; + bool enable_ackerman_axioms(expr* n) const; // relevancy - bool m_relevancy = true; - scoped_ptr m_dual_solver; - ptr_vector m_auto_relevant; - unsigned_vector m_auto_relevant_lim; - unsigned m_auto_relevant_scopes = 0; - bool relevancy_enabled() const { return m_relevancy && get_config().m_relevancy_lvl > 0; } - void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy = false; } - void add_root(unsigned n, sat::literal const* lits); + bool relevancy_enabled() const { return m_relevancy.enabled(); } + void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy.set_enabled(false); } + void add_root(unsigned n, sat::literal const* lits) { m_relevancy.add_root(n, lits); } void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); } void add_root(sat::literal lit) { add_root(1, &lit); } - void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); } + void add_root(sat::literal lit1, sat::literal lit2) { sat::literal lits[2] = { lit1, lit2, }; add_root(2, lits); } void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); } - void add_aux(unsigned n, sat::literal const* lits); + void add_aux(unsigned n, sat::literal const* lits) { m_relevancy.add_def(n, lits); } void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); } void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); } - void track_relevancy(sat::bool_var v); - bool is_relevant(expr* e) const; - bool is_relevant(enode* n) const; - void add_auto_relevant(expr* e); - void pop_relevant(unsigned n); - void push_relevant(); + void mark_relevant(sat::literal lit) { m_relevancy.mark_relevant(lit); } + bool is_relevant(enode* n) const { return m_relevancy.is_relevant(n); } + bool is_relevant(bool_var v) const; + bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); } + void relevant_eh(euf::enode* n); + relevancy& get_relevancy() { return m_relevancy; } // model construction void update_model(model_ref& mdl); diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index f655a0241..55e41fea4 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -269,7 +269,7 @@ namespace fpa { expr* xe = e_x->get_expr(); expr* ye = e_y->get_expr(); - if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye)) + if (fu.is_bvwrap(xe) || fu.is_bvwrap(ye)) return; expr_ref xc = convert(xe); diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index 33fd1c48d..0eebd5247 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -2006,7 +2006,7 @@ namespace pb { s().pop_to_base_level(); if (s().inconsistent()) return; - unsigned trail_sz, count = 0; + unsigned trail_sz = 0, count = 0; do { trail_sz = s().init_trail_size(); m_simplify_change = false; diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index e4e01b964..1665ec74c 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -69,10 +69,16 @@ namespace q { m_mam->add_node(n, false); }; ctx.get_egraph().set_on_merge(_on_merge); - ctx.get_egraph().set_on_make(_on_make); + if (!ctx.relevancy_enabled()) + ctx.get_egraph().set_on_make(_on_make); m_mam = mam::mk(ctx, *this); } + void ematch::relevant_eh(euf::enode* n) { + if (ctx.relevancy_enabled()) + m_mam->add_node(n, false); + } + void ematch::ensure_ground_enodes(expr* e) { mam::ground_subterms(e, m_ground); for (expr* g : m_ground) @@ -352,7 +358,7 @@ namespace q { if (m_prop_queue.empty()) return false; for (unsigned i = 0; i < m_prop_queue.size(); ++i) { - auto [is_conflict, idx, j_idx] = m_prop_queue[i]; + auto const& [is_conflict, idx, j_idx] = m_prop_queue[i]; propagate(is_conflict, idx, j_idx); } m_prop_queue.reset(); @@ -581,7 +587,7 @@ namespace q { return m_inst_queue.propagate() || propagated; ctx.push(value_trail(m_qhead)); ptr_buffer to_remove; - for (; m_qhead < m_clause_queue.size(); ++m_qhead) { + for (; m_qhead < m_clause_queue.size() && m.inc(); ++m_qhead) { unsigned idx = m_clause_queue[m_qhead]; clause& c = *m_clauses[idx]; binding* b = c.m_bindings; diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h index 3cdcfc80e..0db541c1c 100644 --- a/src/sat/smt/q_ematch.h +++ b/src/sat/smt/q_ematch.h @@ -135,9 +135,10 @@ namespace q { bool unit_propagate(); - void add(quantifier* q); + void relevant_eh(euf::enode* n); + void collect_statistics(statistics& st) const; void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing); diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index a968314c2..3debc3e47 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -424,15 +424,19 @@ namespace q { friend class compiler; friend class code_tree_manager; - void display_seq(std::ostream & out, instruction * head, unsigned indent) const { - for (unsigned i = 0; i < indent; i++) { + void spaces(std::ostream& out, unsigned indent) const { + for (unsigned i = 0; i < indent; i++) out << " "; - } + } + + void display_seq(std::ostream & out, instruction * head, unsigned indent) const { + spaces(out, indent); instruction * curr = head; out << *curr; curr = curr->m_next; while (curr != nullptr && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) { out << "\n"; + spaces(out, indent); out << *curr; curr = curr->m_next; } @@ -598,7 +602,7 @@ namespace q { ast_manager & m = m_egraph->get_manager(); out << "patterns:\n"; for (auto [q, a] : m_patterns) - out << mk_pp(q, m) << " " << mk_pp(a, m) << "\n"; + out << q->get_id() << ": " << mk_pp(q, m) << " " << mk_pp(a, m) << "\n"; } #endif out << "function: " << m_root_lbl->get_name(); @@ -2878,8 +2882,10 @@ namespace q { if (tree->expected_num_args() == p->get_num_args()) m_compiler.insert(tree, qa, mp, first_idx, false); } - DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp)); - ctx.push(push_back_trail, false>(m_trees[lbl_id]->get_patterns()));); + DEBUG_CODE(if (first_idx == 0) { + m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp)); + ctx.push(push_back_trail, false>(m_trees[lbl_id]->get_patterns())); + }); TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout);); } diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index a7a2d67d7..8589dfc6d 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -51,7 +51,7 @@ namespace q { m_instantiations.reset(); for (sat::literal lit : m_qs.m_universal) { quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var())); - if (!ctx.is_relevant(q)) + if (!ctx.is_relevant(lit.var())) continue; init_model(); switch (check_forall(q)) { @@ -67,11 +67,10 @@ namespace q { } } m_max_cex += ctx.get_config().m_mbqi_max_cexs; - for (auto [qlit, fml, generation] : m_instantiations) { + for (auto const& [qlit, fml, generation] : m_instantiations) { euf::solver::scoped_generation sg(ctx, generation + 1); sat::literal lit = ctx.mk_literal(fml); m_qs.add_clause(~qlit, ~lit); - ctx.add_root(~qlit, ~lit); } m_instantiations.reset(); return result; @@ -130,7 +129,7 @@ namespace q { r = n; } else if (n->generation() == gen) { - if ((++count) % m_qs.random() == 0) + if ((m_qs.random() % ++count) == 0) r = n; } if (count > m_max_choose_candidates) @@ -309,8 +308,10 @@ namespace q { proj.extract_literals(*m_model, vars, fmls); fmls_extracted = true; } - if (p) - (*p)(*m_model, vars, fmls); + if (!p) + continue; + if (!(*p)(*m_model, vars, fmls)) + return expr_ref(nullptr, m); } for (app* v : vars) { expr_ref term(m); diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index 3339daf2d..456525c42 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -66,7 +66,7 @@ namespace q { ptr_vector univ; for (sat::literal lit : m_qs.universal()) { quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var())); - if (ctx.is_relevant(q)) + if (ctx.is_relevant(lit.var())) univ.push_back(q); } if (univ.empty()) @@ -256,7 +256,7 @@ namespace q { tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n"; if (v2r.find(value, r)) tout << "inverse " << mk_pp(r->get_expr(), m) << "\n"; - ctx.display(tout); + /*ctx.display(tout); */ ); if (v2r.find(value, r)) return r->get_expr(); diff --git a/src/sat/smt/q_queue.cpp b/src/sat/smt/q_queue.cpp index d74ee4e39..ff7dbc8ab 100644 --- a/src/sat/smt/q_queue.cpp +++ b/src/sat/smt/q_queue.cpp @@ -149,12 +149,7 @@ namespace q { if (false && em.propagate(true, f.nodes(), gen, *f.c, new_propagation)) return; -#if 0 - std::cout << mk_pp(q, m) << "\n"; - std::cout << num_bindings << "\n"; - for (unsigned i = 0; i < num_bindings; ++i) - std::cout << mk_pp(f[i]->get_expr(), m) << " " << mk_pp(f[i]->get_sort(), m) << "\n"; -#endif + auto* ebindings = m_subst(q, num_bindings); for (unsigned i = 0; i < num_bindings; ++i) ebindings[i] = f[i]->get_expr(); @@ -168,7 +163,15 @@ namespace q { m_stats.m_num_instances++; - // f.display(ctx, std::cout << mk_pp(f.q(), m) << "\n" << instance << "\n") << "\n"; +#if 0 + std::cout << "instantiate\n"; + for (unsigned i = 0; i < num_bindings; ++i) + std::cout << ctx.bpp(f[i]) << " "; + std::cout << "\n"; + std::cout << mk_pp(q, m) << "\n"; +#endif + +// f.display(ctx, std::cout << mk_pp(f.q(), m) << "\n" << instance << "\n") << "\n"; euf::solver::scoped_generation _sg(ctx, gen); diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 148383c2b..6ef4012af 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -44,19 +44,16 @@ namespace q { if (l.sign() == is_forall(e)) { sat::literal lit = skolemize(q); add_clause(~l, lit); - ctx.add_root(~l, lit); } else if (expand(q)) { for (expr* e : m_expanded) { sat::literal lit = ctx.internalize(e, l.sign(), false, false); add_clause(~l, lit); - ctx.add_root(~l, lit); } } else if (is_ground(q->get_expr())) { auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false); add_clause(~l, lit); - ctx.add_root(~l, lit); } else { ctx.push_vec(m_universal, l); diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index 934864669..5d6a52c8f 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -83,6 +83,7 @@ namespace q { void init_search() override; void finalize_model(model& mdl) override; bool is_shared(euf::theory_var v) const override { return true; } + void relevant_eh(euf::enode* n) override { m_ematch.relevant_eh(n); } ast_manager& get_manager() { return m; } sat::literal_vector const& universal() const { return m_universal; } diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp index be7322a75..b908297ad 100644 --- a/src/sat/smt/recfun_solver.cpp +++ b/src/sat/smt/recfun_solver.cpp @@ -68,8 +68,8 @@ namespace recfun { TRACEFN("case expansion " << e); SASSERT(e.m_def->is_fun_macro()); auto & vars = e.m_def->get_vars(); - auto lhs = e.m_lhs; - auto rhs = apply_args(vars, e.m_args, e.m_def->get_rhs()); + app_ref lhs = e.m_lhs; + expr_ref rhs = apply_args(vars, e.m_args, e.m_def->get_rhs()); unsigned generation = std::max(ctx.get_max_generation(lhs), ctx.get_max_generation(rhs)); euf::solver::scoped_generation _sgen(ctx, generation + 1); auto eq = eq_internalize(lhs, rhs); diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp deleted file mode 100644 index 86d73a2d8..000000000 --- a/src/sat/smt/sat_dual_solver.cpp +++ /dev/null @@ -1,185 +0,0 @@ -/*++ -Copyright (c) 2020 Microsoft Corporation - -Module Name: - - sat_dual_solver.cpp - -Abstract: - - Solver for obtaining implicant. - -Author: - - Nikolaj Bjorner (nbjorner) 2020-08-25 - ---*/ -#include "sat/smt/sat_dual_solver.h" - -namespace sat { - - dual_solver::dual_solver(reslimit& l): - m_solver(m_params, l) - { - SASSERT(!m_solver.get_config().m_drat); - m_solver.set_incremental(true); - } - - void dual_solver::flush() { - while (m_num_scopes > 0) { - m_solver.user_push(); - m_roots.push_scope(); - m_tracked_vars.push_scope(); - m_units.push_scope(); - m_vars.push_scope(); - --m_num_scopes; - } - } - - void dual_solver::push() { - ++m_num_scopes; - } - - void dual_solver::pop(unsigned num_scopes) { - if (m_num_scopes >= num_scopes) { - m_num_scopes -= num_scopes; - return; - } - num_scopes -= m_num_scopes; - m_num_scopes = 0; - m_solver.user_pop(num_scopes); - unsigned old_sz = m_tracked_vars.old_size(num_scopes); - for (unsigned i = m_tracked_vars.size(); i-- > old_sz; ) - m_is_tracked[m_tracked_vars[i]] = false; - old_sz = m_vars.old_size(num_scopes); - for (unsigned i = m_vars.size(); i-- > old_sz; ) { - unsigned v = m_vars[i]; - unsigned w = m_ext2var[v]; - m_ext2var[v] = null_bool_var; - m_var2ext[w] = null_bool_var; - } - m_vars.pop_scope(num_scopes); - m_units.pop_scope(num_scopes); - m_roots.pop_scope(num_scopes); - m_tracked_vars.pop_scope(num_scopes); - } - - bool_var dual_solver::ext2var(bool_var v) { - bool_var w = m_ext2var.get(v, null_bool_var); - if (null_bool_var == w) { - w = m_solver.mk_var(); - m_solver.set_external(w); - m_ext2var.setx(v, w, null_bool_var); - m_var2ext.setx(w, v, null_bool_var); - m_vars.push_back(v); - } - return w; - } - - void dual_solver::track_relevancy(bool_var w) { - flush(); - bool_var v = ext2var(w); - if (!m_is_tracked.get(v, false)) { - m_is_tracked.setx(v, true, false); - m_tracked_vars.push_back(v); - } - } - - literal dual_solver::ext2lit(literal lit) { - return literal(ext2var(lit.var()), lit.sign()); - } - - literal dual_solver::lit2ext(literal lit) { - return literal(m_var2ext[lit.var()], lit.sign()); - } - - void dual_solver::add_root(unsigned sz, literal const* clause) { - flush(); - if (false && sz == 1) { - TRACE("dual", tout << "unit: " << clause[0] << "\n";); - m_units.push_back(clause[0]); - return; - } - literal root; - if (sz == 1) - root = ext2lit(clause[0]); - else { - root = literal(m_solver.mk_var(), false); - for (unsigned i = 0; i < sz; ++i) - m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input()); - } - m_solver.set_external(root.var()); - m_roots.push_back(~root); - TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";); - } - - void dual_solver::add_aux(unsigned sz, literal const* clause) { - flush(); - m_lits.reset(); - for (unsigned i = 0; i < sz; ++i) - m_lits.push_back(ext2lit(clause[i])); - TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << " -> " << m_lits << "\n";); - m_solver.mk_clause(sz, m_lits.data(), status::input()); - } - - void dual_solver::add_assumptions(solver const& s) { - flush(); - m_lits.reset(); - for (bool_var v : m_tracked_vars) - m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v]))); - for (auto lit : m_units) { - bool_var w = m_ext2var.get(lit.var(), null_bool_var); - if (w != null_bool_var) - m_lits.push_back(ext2lit(lit)); - } - } - - bool dual_solver::operator()(solver const& s) { - m_core.reset(); - m_core.append(m_units); - if (m_roots.empty()) - return true; - m_solver.user_push(); - m_solver.add_clause(m_roots.size(), m_roots.data(), status::input()); - add_assumptions(s); - lbool is_sat = m_solver.check(m_lits.size(), m_lits.data()); - if (is_sat == l_false) - for (literal lit : m_solver.get_core()) - m_core.push_back(lit2ext(lit)); - if (is_sat == l_true) { - TRACE("dual", display(s, tout); s.display(tout);); - IF_VERBOSE(0, verbose_stream() << "unexpected SAT\n"); - UNREACHABLE(); - return false; - } - TRACE("dual", m_solver.display(tout << "is-sat: " << is_sat << " core: " << m_core << "\n");); - m_solver.user_pop(1); - return is_sat == l_false; - } - - std::ostream& dual_solver::display(solver const& s, std::ostream& out) const { - for (unsigned v = 0; v < m_solver.num_vars(); ++v) { - bool_var w = m_var2ext.get(v, null_bool_var); - if (w == null_bool_var) - continue; - lbool v1 = m_solver.value(v); - lbool v2 = s.value(w); - if (v1 == v2 || v2 == l_undef) - continue; - out << "ext: " << w << " " << v2 << "\n"; - out << "int: " << v << " " << v1 << "\n"; - } - literal_vector lits; - for (bool_var v : m_tracked_vars) - lits.push_back(literal(m_var2ext[v], l_false == s.value(m_var2ext[v]))); - out << "tracked: " << lits << "\n"; - lits.reset(); - for (literal r : m_roots) - if (m_solver.value(r) == l_true) - lits.push_back(r); - out << "roots: " << lits << "\n"; - m_solver.display(out); - - return out; - } -} diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h deleted file mode 100644 index 08a31084e..000000000 --- a/src/sat/smt/sat_dual_solver.h +++ /dev/null @@ -1,83 +0,0 @@ -/*++ -Copyright (c) 2020 Microsoft Corporation - -Module Name: - - sat_dual_solver.h - -Abstract: - - Solver for obtaining implicant. - Based on an idea by Armin Biere to use dual propagation - for representation of negated goal. - -Author: - - Nikolaj Bjorner (nbjorner) 2020-08-25 - ---*/ -#pragma once -#include "util/lim_vector.h" -#include "sat/sat_solver.h" - -namespace sat { - - class dual_solver { - class dual_params : public no_drat_params { - public: - dual_params() { - set_bool("core.minimize", false); - } - }; - dual_params m_params; - solver m_solver; - lim_svector m_units, m_roots; - lim_svector m_tracked_vars; - literal_vector m_lits, m_core; - bool_var_vector m_is_tracked; - unsigned_vector m_ext2var; - unsigned_vector m_var2ext; - lim_svector m_vars; - unsigned m_num_scopes = 0; - void add_literal(literal lit); - - bool_var ext2var(bool_var v); - bool_var var2ext(bool_var v); - literal ext2lit(literal lit); - literal lit2ext(literal lit); - - void add_assumptions(solver const& s); - - std::ostream& display(solver const& s, std::ostream& out) const; - - void flush(); - - public: - dual_solver(reslimit& l); - void push(); - void pop(unsigned num_scopes); - - /* - * track model relevancy for variable - */ - void track_relevancy(bool_var v); - - /* - * Add a root clause from the input problem. - * At least one literal has to be satisfied in every root. - */ - void add_root(unsigned sz, literal const* clause); - - /* - * Add auxiliary clauses that originate from compiling definitions. - */ - void add_aux(unsigned sz, literal const* clause); - - /* - * Extract a minimized subset of relevant literals from a model for s. - */ - bool operator()(solver const& s); - - literal_vector const& core() const { return m_core; } - }; -} diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 06efccaf0..f72ff601a 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -132,6 +132,7 @@ namespace euf { bool th_euf_solver::add_unit(sat::literal lit) { bool was_true = is_true(lit); ctx.s().add_clause(1, &lit, mk_status()); + ctx.add_root(lit); return !was_true; } @@ -143,32 +144,27 @@ namespace euf { return is_new; } - bool th_euf_solver::add_clause(sat::literal a, sat::literal b) { - bool was_true = is_true(a, b); + bool th_euf_solver::add_clause(sat::literal a, sat::literal b) { sat::literal lits[2] = { a, b }; - ctx.s().add_clause(2, lits, mk_status()); - return !was_true; + return add_clause(2, lits); } - bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) { - bool was_true = is_true(a, b, c); + bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; - ctx.s().add_clause(3, lits, mk_status()); - return !was_true; + return add_clause(3, lits); } bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) { - bool was_true = is_true(a, b, c, d); sat::literal lits[4] = { a, b, c, d }; - ctx.s().add_clause(4, lits, mk_status()); - return !was_true; + return add_clause(4, lits); } - bool th_euf_solver::add_clause(sat::literal_vector const& lits) { + bool th_euf_solver::add_clause(unsigned n, sat::literal* lits) { bool was_true = false; - for (auto lit : lits) - was_true |= is_true(lit); - s().add_clause(lits.size(), lits.data(), mk_status()); + for (unsigned i = 0; i < n; ++i) + was_true |= is_true(lits[i]); + ctx.add_root(n, lits); + s().add_clause(n, lits, mk_status()); return !was_true; } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 7e66a7156..9d1d9ebb1 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -111,6 +111,10 @@ namespace euf { virtual void new_diseq_eh(euf::th_eq const& eq) {} + virtual bool enable_ackerman_axioms(euf::enode* n) const { return true; } + + virtual void relevant_eh(euf::enode* n) {} + /** \brief Parametric theories (e.g. Arrays) should implement this method. */ @@ -139,7 +143,8 @@ namespace euf { bool add_clause(sat::literal a, sat::literal b); bool add_clause(sat::literal a, sat::literal b, sat::literal c); bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d); - bool add_clause(sat::literal_vector const& lits); + bool add_clause(sat::literal_vector const& lits) { return add_clause(lits.size(), lits.data()); } + bool add_clause(unsigned n, sat::literal* lits); void add_equiv(sat::literal a, sat::literal b); void add_equiv_and(sat::literal a, sat::literal_vector const& bs); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index bdb37bc79..30d73a21a 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -125,20 +125,6 @@ struct goal2sat::imp : public sat::sat_internalizer { bool top_level_relevant() { return m_top_level && relevancy_enabled(); } - - void add_dual_def(unsigned n, sat::literal const* lits) { - if (relevancy_enabled()) - ensure_euf()->add_aux(n, lits); - } - - void add_dual_root(unsigned n, sat::literal const* lits) { - if (relevancy_enabled()) - ensure_euf()->add_root(n, lits); - } - - void add_dual_root(sat::literal lit) { - add_dual_root(1, &lit); - } void mk_clause(sat::literal l) { mk_clause(1, &l); @@ -156,7 +142,8 @@ struct goal2sat::imp : public sat::sat_internalizer { void mk_clause(unsigned n, sat::literal * lits) { TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";); - add_dual_def(n, lits); + if (relevancy_enabled()) + ensure_euf()->add_aux(n, lits); m_solver.add_clause(n, lits, mk_status()); } @@ -176,7 +163,8 @@ struct goal2sat::imp : public sat::sat_internalizer { void mk_root_clause(unsigned n, sat::literal * lits) { TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";); - add_dual_root(n, lits); + if (relevancy_enabled()) + ensure_euf()->add_root(n, lits); m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input()); } @@ -186,8 +174,6 @@ struct goal2sat::imp : public sat::sat_internalizer { return v; v = m_solver.add_var(is_ext); log_def(v, n); - if (top_level_relevant() && !is_bool_op(n)) - ensure_euf()->track_relevancy(v); return v; } @@ -216,14 +202,11 @@ struct goal2sat::imp : public sat::sat_internalizer { if (!m_expr2var_replay || !m_expr2var_replay->find(t, v)) v = add_var(true, t); m_map.insert(t, v); - if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) { - add_dual_root(sat::literal(v, m.is_false(t))); - ensure_euf()->track_relevancy(v); - } return v; } sat::bool_var add_bool_var(expr* t) override { + force_push(); sat::bool_var v = m_map.to_bool_var(t); if (v == sat::null_bool_var) v = mk_bool_var(t); @@ -238,11 +221,11 @@ struct goal2sat::imp : public sat::sat_internalizer { for (; m_num_scopes > 0; --m_num_scopes) { m_map.push(); m_cache_lim.push_back(m_cache_trail.size()); - } + } } void push() override { - ++m_num_scopes; + ++m_num_scopes; } void pop(unsigned n) override { @@ -263,7 +246,7 @@ struct goal2sat::imp : public sat::sat_internalizer { } } m_cache_trail.shrink(k); - m_cache_lim.shrink(m_cache_lim.size() - n); + m_cache_lim.shrink(m_cache_lim.size() - n); } // remove non-external literals from cache. @@ -677,8 +660,6 @@ struct goal2sat::imp : public sat::sat_internalizer { } if (lit == sat::null_literal) return; - if (top_level_relevant()) - euf->track_relevancy(lit.var()); if (root) mk_root_clause(lit); else diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 38c25eae3..892a88f89 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -201,8 +201,8 @@ public: char const* name() const override { return "sat"; } void updt_params(params_ref const & p) override { - m_params = p; - if (m_imp) m_imp->updt_params(p); + m_params.append(p); + if (m_imp) m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index f359136af..1cef2a0f1 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -226,6 +226,7 @@ namespace smt { ebindings[i] = bindings[i]->get_expr(); expr_ref instance = m_subst(); + TRACE("qi_queue", tout << "new instance:\n" << mk_pp(instance, m) << "\n";); TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m) << "\n";); expr_ref s_instance(m); @@ -244,6 +245,15 @@ namespace smt { return; } +#if 0 + std::cout << "instantiate\n"; + enode_vector _bindings(num_bindings, bindings); + for (auto * b : _bindings) + std::cout << enode_pp(b, m_context) << " "; + std::cout << "\n"; + std::cout << mk_pp(q, m) << "\n"; +#endif + TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";); stat->inc_num_instances(); if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) { diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index e9fc3cb53..525f6b3db 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -73,6 +73,7 @@ namespace smt { void add_indexof_axiom(expr* n) { m_ax.indexof_axiom(n); } void add_last_indexof_axiom(expr* n) { m_ax.last_indexof_axiom(n); } void add_replace_axiom(expr* n) { m_ax.replace_axiom(n); } + void add_replace_all_axiom(expr* n) { m_ax.replace_all_axiom(n); } void add_at_axiom(expr* n) { m_ax.at_axiom(n); } void add_nth_axiom(expr* n) { m_ax.nth_axiom(n); } void add_itos_axiom(expr* n) { m_ax.itos_axiom(n); } diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 6e739a499..8995f7fba 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -158,7 +158,6 @@ namespace smt { void mark_as_interpreted() { SASSERT(!m_interpreted); - SASSERT(m_owner->get_num_args() == 0); SASSERT(m_class_size == 1); m_interpreted = true; } diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 77b3f14d5..1c899ef18 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -974,7 +974,7 @@ namespace smt { } enode * e = enode::mk(m, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true); TRACE("mk_enode_detail", tout << "e.get_num_args() = " << e->get_num_args() << "\n";); - if (n->get_num_args() == 0 && m.is_unique_value(n)) + if (m.is_unique_value(n)) e->mark_as_interpreted(); TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";); TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";); diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 5c28d52fd..681bdd55b 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -307,13 +307,13 @@ namespace smt { /** \brief Return a reference to smt::context. - This is a temporary hack to support user theories. - TODO: remove this hack. - We need to revamp user theories too. + This breaks abstractions. + + It is currently used by the opt-solver + to access optimization services from arithmetic solvers + and to ensure that the solver has registered PB theory solver. - This method breaks the abstraction barrier. - - \warning We should not use this method + \warning This method should not be used in new code. */ context & get_context(); }; diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index 6d20072cb..4b787561d 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -134,11 +134,11 @@ namespace smt { obj_map m_relevant_ehs; obj_map m_watches[2]; struct eh_trail { - enum kind { POS_WATCH, NEG_WATCH, HANDLER }; + enum class kind { POS_WATCH, NEG_WATCH, HANDLER }; kind m_kind; expr * m_node; - eh_trail(expr * n):m_kind(HANDLER), m_node(n) {} - eh_trail(expr * n, bool val):m_kind(val ? POS_WATCH : NEG_WATCH), m_node(n) {} + eh_trail(expr * n):m_kind(kind::HANDLER), m_node(n) {} + eh_trail(expr * n, bool val):m_kind(val ? kind::POS_WATCH : kind::NEG_WATCH), m_node(n) {} kind get_kind() const { return m_kind; } expr * get_node() const { return m_node; } }; @@ -292,9 +292,9 @@ namespace smt { expr * n = t.get_node(); relevancy_ehs * ehs; switch (t.get_kind()) { - case eh_trail::POS_WATCH: ehs = get_watches(n, true); SASSERT(ehs); set_watches(n, true, ehs->tail()); break; - case eh_trail::NEG_WATCH: ehs = get_watches(n, false); SASSERT(ehs); set_watches(n, false, ehs->tail()); break; - case eh_trail::HANDLER: ehs = get_handlers(n); SASSERT(ehs); set_handlers(n, ehs->tail()); break; + case eh_trail::kind::POS_WATCH: ehs = get_watches(n, true); SASSERT(ehs); set_watches(n, true, ehs->tail()); break; + case eh_trail::kind::NEG_WATCH: ehs = get_watches(n, false); SASSERT(ehs); set_watches(n, false, ehs->tail()); break; + case eh_trail::kind::HANDLER: ehs = get_handlers(n); SASSERT(ehs); set_handlers(n, ehs->tail()); break; default: UNREACHABLE(); break; } m.dec_ref(n); @@ -378,9 +378,7 @@ namespace smt { break; case l_true: { expr * true_arg = nullptr; - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - expr * arg = n->get_arg(i); + for (expr* arg : *n) { if (m_context.find_assignment(arg) == l_true) { if (is_relevant_core(arg)) return; @@ -402,9 +400,7 @@ namespace smt { switch (val) { case l_false: { expr * false_arg = nullptr; - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - expr * arg = n->get_arg(i); + for (expr* arg : *n) { if (m_context.find_assignment(arg) == l_false) { if (is_relevant_core(arg)) return; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 4f917ba00..aa775c6a3 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -125,7 +125,7 @@ namespace { smt_params m_smt_params_save; void push_params() override { - m_params_save = params_ref(); + m_params_save.reset(); m_params_save.copy(solver::get_params()); m_smt_params_save = m_smt_params; } diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index c99e50393..943facb98 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -127,7 +127,8 @@ public: scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) { m_params = o.fparams(); - m_params_ref = o.params(); + m_params_ref.reset(); + m_params_ref.append(o.params()); smt::kernel * new_ctx = alloc(smt::kernel, m, m_params, m_params_ref); TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";); new_ctx->set_logic(o.m_logic); diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp index 97ce4a1c1..e0197d15d 100644 --- a/src/smt/tactic/unit_subsumption_tactic.cpp +++ b/src/smt/tactic/unit_subsumption_tactic.cpp @@ -50,7 +50,7 @@ struct unit_subsumption_tactic : public tactic { } void updt_params(params_ref const& p) override { - m_params = p; + m_params.append(p); // m_context.updt_params(p); does not exist. } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 5ef415d6a..c86db1aa5 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2646,6 +2646,9 @@ void theory_seq::deque_axiom(expr* n) { else if (m_util.str.is_replace(n)) { m_ax.add_replace_axiom(n); } + else if (m_util.str.is_replace_all(n)) { + m_ax.add_replace_all_axiom(n); + } else if (m_util.str.is_extract(n)) { m_ax.add_extract_axiom(n); } @@ -3190,6 +3193,7 @@ void theory_seq::relevant_eh(app* n) { m_util.str.is_to_code(n) || m_util.str.is_unit(n) || m_util.str.is_length(n) || + /* m_util.str.is_replace_all(n) || uncomment to enable axiomatization */ m_util.str.is_le(n)) { enque_axiom(n); } diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp index b772f21ae..d29e0f2bd 100644 --- a/src/solver/check_sat_result.cpp +++ b/src/solver/check_sat_result.cpp @@ -20,7 +20,10 @@ Notes: void check_sat_result::set_reason_unknown(event_handler& eh) { switch (eh.caller_id()) { - case UNSET_EH_CALLER: break; + case UNSET_EH_CALLER: + if (reason_unknown() == "") + set_reason_unknown("unclassifed exception"); + break; case CTRL_C_EH_CALLER: set_reason_unknown("interrupted from keyboard"); break; diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index b53e3daed..7dcca2ecc 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -226,7 +226,7 @@ void solver::collect_param_descrs(param_descrs & r) { } void solver::reset_params(params_ref const & p) { - m_params = p; + m_params.append(p); solver_params sp(m_params); m_cancel_backup_file = sp.cancel_backup_file(); } diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 37027e63a..b689a53e2 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -559,7 +559,7 @@ struct aig_manager::imp { aig_lit r; switch (num) { case 0: - r = m.m_true; + r = m.m_false; break; case 1: r = m_result_stack[spos]; diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index 4493568bf..33ffbf282 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -149,8 +149,8 @@ public: char const* name() const override { return "add_bounds"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index fce096f23..3cc7436d1 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -45,7 +45,7 @@ public: char const* name() const override { return "card2bv"; } void updt_params(params_ref const & p) override { - m_params = p; + m_params.append(p); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 92ce7cd29..4269aff85 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -360,8 +360,8 @@ public: char const* name() const override { return "diff_neq"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 07b59a3f9..6b9b226b3 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -297,8 +297,8 @@ public: char const* name() const override { return "factor"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->m_rw.cfg().updt_params(p); + m_params.append(p); + m_imp->m_rw.cfg().updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index f2039c378..87061b189 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -303,8 +303,8 @@ public: char const* name() const override { return "fix_dl_var"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index ef8109de0..569dbff21 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -1645,8 +1645,8 @@ public: char const* name() const override { return "fm"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 77786e267..5f6edf6ea 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -135,8 +135,8 @@ public: char const* name() const override { return "lia2card"; } void updt_params(params_ref const & p) override { - m_params = p; - m_compile_equality = p.get_bool("compile_equality", true); + m_params.append(p); + m_compile_equality = m_params.get_bool("compile_equality", true); } expr_ref mk_bounded(expr_ref_vector& axioms, app* x, unsigned lo, unsigned hi) { diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index d67f49a37..46404ffb0 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -308,8 +308,8 @@ public: char const* name() const override { return "lia2pb"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index b63c85f1b..2d405895f 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -1010,8 +1010,8 @@ public: char const* name() const override { return "pb2bv"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index d55ea4ecf..0f62b45f4 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ b/src/tactic/arith/propagate_ineqs_tactic.cpp @@ -543,8 +543,8 @@ propagate_ineqs_tactic::~propagate_ineqs_tactic() { } void propagate_ineqs_tactic::updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void propagate_ineqs_tactic::operator()(goal_ref const & g, diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index db43a3ee6..9c07bcadc 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -906,7 +906,7 @@ public: char const* name() const override { return "purify_arith"; } void updt_params(params_ref const & p) override { - m_params = p; + m_params.append(p); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index a7cef82e3..251d78e72 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -401,8 +401,8 @@ public: char const* name() const override { return "recover_01"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 744f207f3..978a0a9a6 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -122,8 +122,8 @@ public: char const* name() const override { return "bit_blaster"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 3af58bf66..0fc38f2db 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -434,8 +434,8 @@ public: char const* name() const override { return "bv1_blaster"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->m_rw.cfg().updt_params(p); + m_params.append(p); + m_imp->m_rw.cfg().updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index e0b6e4d81..7ea7c0a69 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -206,8 +206,8 @@ tactic * bv_bound_chk_tactic::translate(ast_manager & m) { void bv_bound_chk_tactic::updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void bv_bound_chk_tactic::cleanup() { diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index d0bd6538b..da86ed663 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -116,8 +116,8 @@ public: char const* name() const override { return "bvarray2uf"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 7c72abde9..02ec522c6 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -145,11 +145,13 @@ class elim_small_bv_tactic : public tactic { "; sort = " << mk_ismt2_pp(s, m) << "; body = " << mk_ismt2_pp(body, m) << std::endl;); - if (bv_sz >= 31ul || ((unsigned)(1ul << bv_sz)) + num_steps > m_max_steps) { + if (bv_sz >= 31) + return false; + unsigned max_num = 1u << bv_sz; + if (max_num > m_max_steps || max_num + num_steps > m_max_steps) return false; - } - for (unsigned j = 0; j < (1ul << bv_sz) && !max_steps_exceeded(num_steps); j++) { + for (unsigned j = 0; j < max_num && !max_steps_exceeded(num_steps); j++) { expr_ref n(m_util.mk_numeral(j, bv_sz), m); new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n)); num_steps++; @@ -207,10 +209,10 @@ class elim_small_bv_tactic : public tactic { } void updt_params(params_ref const & p) { - m_params = p; - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_max_steps = p.get_uint("max_steps", UINT_MAX); - m_max_bits = p.get_uint("max_bits", 4); + m_params.append(p); + m_max_memory = megabytes_to_bytes(m_params.get_uint("max_memory", UINT_MAX)); + m_max_steps = m_params.get_uint("max_steps", UINT_MAX); + m_max_bits = m_params.get_uint("max_bits", 4); } }; @@ -241,8 +243,8 @@ public: } void updt_params(params_ref const & p) override { - m_params = p; - m_rw.cfg().updt_params(p); + m_params.append(p); + m_rw.cfg().updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index 0efe4f58c..2bc99806e 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -280,8 +280,8 @@ public: char const* name() const override { return "max_bv_sharing"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->m_rw.cfg().updt_params(p); + m_params.append(p); + m_imp->m_rw.cfg().updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index fe1269732..38b4e172e 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -174,8 +174,8 @@ public: char const* name() const override { return "blast_term_ite"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->m_rw.m_cfg.updt_params(p); + m_params.append(p); + m_imp->m_rw.m_cfg.updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index d1b8f5b1b..234b7262c 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -52,7 +52,7 @@ public: ~cofactor_term_ite_tactic() override {} char const* name() const override { return "cofactor"; } - void updt_params(params_ref const & p) override { m_params = p; m_elim_ite.updt_params(p); } + void updt_params(params_ref const & p) override { m_params.append(p); m_elim_ite.updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); } void operator()(goal_ref const & g, goal_ref_buffer& result) override { diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index 3d8ebfb12..e507f49dd 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -60,7 +60,7 @@ public: } void updt_params(params_ref const & p) override { - m_params = p; + m_params.append(p); } void collect_param_descrs(param_descrs & r) override {} diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index c8aa1a4c4..47b2fa389 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -605,8 +605,8 @@ ctx_simplify_tactic::~ctx_simplify_tactic() { } void ctx_simplify_tactic::updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void ctx_simplify_tactic::get_param_descrs(param_descrs & r) { diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index 42adf04a9..2a0593ade 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -143,8 +143,8 @@ public: } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->m_rw.cfg().updt_params(p); + m_params.append(p); + m_imp->m_rw.cfg().updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index a9f5ffcf8..26a69fd4a 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -862,9 +862,9 @@ public: } void updt_params(params_ref const & p) override { - m_params = p; - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_max_steps = p.get_uint("max_steps", UINT_MAX); + m_params.append(p); + m_max_memory = megabytes_to_bytes(m_params.get_uint("max_memory", UINT_MAX)); + m_max_steps = m_params.get_uint("max_steps", UINT_MAX); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 485eda4dd..dfcb152a2 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -258,8 +258,8 @@ public: char const* name() const override { return "injectivity"; } void updt_params(params_ref const & p) override { - m_params = p; - m_finder->updt_params(p); + m_params.append(p); + m_finder->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index 164cf9311..fccfdf53e 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -51,7 +51,7 @@ public: char const* name() const override { return "nnf"; } - void updt_params(params_ref const & p) override { m_params = p; } + void updt_params(params_ref const & p) override { m_params.append(p); } void collect_param_descrs(param_descrs & r) override { nnf::get_param_descrs(r); } diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index fdc8bd93d..5ad25bd91 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -607,7 +607,7 @@ private: sub.insert(e, v); expr_ref tmp(m); m_r.set_substitution(&sub); - for (unsigned i = 0; i < positions.size(); ++i) { + for (unsigned i = 0; !g->inconsistent() && i < positions.size(); ++i) { unsigned idx = positions[i]; expr_ref f(m); proof_ref new_pr(m); diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index b735de4b7..b2ed7cab9 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -219,9 +219,9 @@ public: char const* name() const override { return "propagate_values"; } void updt_params(params_ref const & p) override { - m_params = p; + m_params.append(p); m_r.updt_params(p); - updt_params_core(p); + updt_params_core(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index ca76cafc7..8d9ff759f 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -80,8 +80,8 @@ simplify_tactic::~simplify_tactic() { } void simplify_tactic::updt_params(params_ref const & p) { - m_params = p; - m_imp->m_r.updt_params(p); + m_params.append(p); + m_imp->m_r.updt_params(m_params); } void simplify_tactic::get_param_descrs(param_descrs & r) { diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 9d844b7ed..a73fe88b6 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -1092,8 +1092,8 @@ public: char const* name() const override { return "solve_eqs"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h index a1cafb7c0..dae38304a 100644 --- a/src/tactic/core/special_relations_tactic.h +++ b/src/tactic/core/special_relations_tactic.h @@ -49,7 +49,7 @@ public: ~special_relations_tactic() override {} - void updt_params(params_ref const & p) override { m_params = p; } + void updt_params(params_ref const & p) override { m_params.append(p); } void collect_param_descrs(param_descrs & r) override { } diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index e26fded8f..c141aaa3b 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -894,8 +894,8 @@ public: char const* name() const override { return "tseitin_cnf"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index be98dea00..282439228 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -123,8 +123,8 @@ public: char const* name() const override { return "fp2bv"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp index 6b275508b..c92968c8c 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.cpp +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -136,8 +136,8 @@ public: char const* name() const override { return "solver_subsumption"; } void updt_params(params_ref const& p) override { - m_params = p; - unsigned max_conflicts = p.get_uint("max_conflicts", 2); + m_params.append(p); + unsigned max_conflicts = m_params.get_uint("max_conflicts", 2); m_params.set_uint("sat.max_conflicts", max_conflicts); m_params.set_uint("smt.max_conflicts", max_conflicts); } diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index ece6940f3..e631c23e9 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -53,8 +53,8 @@ public: char const* name() const override { return "sls"; } void updt_params(params_ref const & p) override { - m_params = p; - m_engine->updt_params(p); + m_params.append(p); + m_engine->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index fca2f8481..c5a9e6984 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -336,6 +336,25 @@ public: catch (tactic_exception &) { result.reset(); } + catch (z3_error & ex) { + IF_VERBOSE(10, verbose_stream() << "z3 error: " << ex.error_code() << " in or-else\n"); + throw; + } + catch (z3_exception& ex) { + IF_VERBOSE(10, verbose_stream() << ex.msg() << " in or-else\n"); + throw; + } + catch (const std::exception &ex) { + IF_VERBOSE(10, verbose_stream() << ex.what() << " in or-else\n"); + throw; + } + catch (...) { + IF_VERBOSE(10, verbose_stream() << " unclassified exception in or-else\n"); + // std::current_exception returns a std::exception_ptr, which apparently + // needs to be re-thrown to extract type information. + // typeid(ex).name() would be nice. + throw; + } } else { t->operator()(in, result); diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index c5745d85c..2358abcd1 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -108,8 +108,8 @@ public: char const* name() const override { return "macro_finder"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 0e0cb7cb2..b0eb113b8 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -103,8 +103,8 @@ public: char const* name() const override { return "quasi_macros"; } void updt_params(params_ref const & p) override { - m_params = p; - m_imp->updt_params(p); + m_params.append(p); + m_imp->updt_params(m_params); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index d5bfec8fe..e254523c0 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -35,7 +35,7 @@ public: } void updt_params(params_ref const & p) override { - m_params = p; + m_params.append(p); } void collect_param_descrs(param_descrs & r) override { diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index 534b9dbc0..403df8af5 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -14,7 +14,7 @@ namespace user_propagator { class context_obj { public: - virtual ~context_obj() {} + virtual ~context_obj() = default; }; typedef std::function final_eh_t; @@ -33,11 +33,7 @@ namespace user_propagator { enum kind_t { OP_USER_PROPAGATE }; - virtual ~plugin() {} - - virtual decl_plugin* mk_fresh() { return alloc(plugin); } - - family_id get_family_id() const { return m_family_id; } + decl_plugin* mk_fresh() override { return alloc(plugin); } sort* mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) override { UNREACHABLE(); @@ -45,7 +41,7 @@ namespace user_propagator { } func_decl* mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters, - unsigned arity, sort* const* domain, sort* range) { + unsigned arity, sort* const* domain, sort* range) override { UNREACHABLE(); return nullptr; } diff --git a/src/util/params.cpp b/src/util/params.cpp index 1819684e0..aefe4e074 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -520,7 +520,7 @@ params_ref::~params_ref() { params_ref::params_ref(params_ref const & p): m_params(nullptr) { - operator=(p); + set(p); } void params_ref::display(std::ostream & out) const { @@ -553,18 +553,20 @@ void params_ref::validate(param_descrs const & p) { m_params->validate(p); } -params_ref & params_ref::operator=(params_ref const & p) { + +void params_ref::set(params_ref const & p) { if (p.m_params) p.m_params->inc_ref(); if (m_params) m_params->dec_ref(); m_params = p.m_params; - return *this; } void params_ref::copy(params_ref const & src) { - if (m_params == nullptr) - operator=(src); + if (m_params == nullptr || m_params->empty()) + set(src); + else if (src.empty()) + return; else { init(); copy_core(src.m_params); diff --git a/src/util/params.h b/src/util/params.h index 989d112bd..da05dff90 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -35,6 +35,8 @@ class params_ref { params * m_params; void init(); void copy_core(params const * p); + params_ref& operator=(params_ref const& p) = delete; + void set(params_ref const& p); public: params_ref():m_params(nullptr) {} params_ref(params_ref const & p); @@ -42,8 +44,7 @@ public: static params_ref const & get_empty() { return g_empty_params_ref; } - params_ref & operator=(params_ref const & p); - + // copy params from src void copy(params_ref const & src); void append(params_ref const & src) { copy(src); } diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index e144cf636..a36e762aa 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -33,12 +33,14 @@ Revision History: #include #endif +enum scoped_timer_work_state { IDLE = 0, WORKING = 1, EXITING = 2 }; + struct scoped_timer_state { std::thread m_thread; std::timed_mutex m_mutex; event_handler * eh; unsigned ms; - std::atomic work; + std::atomic work; std::condition_variable_any cv; }; @@ -49,11 +51,11 @@ static atomic num_workers(0); static void thread_func(scoped_timer_state *s) { workers.lock(); while (true) { - s->cv.wait(workers, [=]{ return s->work > 0; }); + s->cv.wait(workers, [=]{ return s->work > IDLE; }); workers.unlock(); // exiting.. - if (s->work == 2) + if (s->work == EXITING) return; auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(s->ms); @@ -68,9 +70,8 @@ static void thread_func(scoped_timer_state *s) { s->m_mutex.unlock(); next: - s->work = 0; + s->work = IDLE; workers.lock(); - available_workers.push_back(s); } } @@ -97,7 +98,7 @@ public: s->ms = ms; s->eh = eh; s->m_mutex.lock(); - s->work = 1; + s->work = WORKING; if (new_worker) { s->m_thread = std::thread(thread_func, s); } @@ -108,8 +109,11 @@ public: ~imp() { s->m_mutex.unlock(); - while (s->work == 1) + while (s->work == WORKING) std::this_thread::yield(); + workers.lock(); + available_workers.push_back(s); + workers.unlock(); } }; @@ -139,7 +143,7 @@ void scoped_timer::finalize() { while (deleted < num_workers) { workers.lock(); for (auto w : available_workers) { - w->work = 2; + w->work = EXITING; w->cv.notify_one(); } decltype(available_workers) cleanup_workers;