mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
jofleish 2022-07-18 12:22:39 -04:00
parent 8dad9a29c2 527914db05
commit 8c25f7081b
125 changed files with 6618 additions and 4683 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/wasm-release.yml vendored
View file

@ -10,7 +10,7 @@ defaults:
working-directory: src/api/js
env:
EM_VERSION: 3.1.0
EM_VERSION: 3.1.15
jobs:
publish:

2
.github/workflows/wasm.yml vendored
View file

@ -10,7 +10,7 @@ defaults:
working-directory: src/api/js
env:
EM_VERSION: 3.1.0
EM_VERSION: 3.1.15
jobs:
check:

1
.gitignore vendored
View file

@ -46,6 +46,7 @@ bld_rel/*
bld_dbg_x64/*
bld_rel_x64/*
.vscode
*build*/**
# Auto generated files.
config.log
config.status

12
CMakeLists.txt
View file

@ -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.18.0 LANGUAGES CXX)
project(Z3 VERSION 4.9.2.0 LANGUAGES CXX)
################################################################################
# Project version
@ -160,7 +160,7 @@ list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEAS
################################################################################
# Find Python
################################################################################
find_package(PythonInterp REQUIRED)
find_package(PythonInterp 3 REQUIRED)
message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}")
################################################################################
@ -230,7 +230,7 @@ else()
message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised")
endif()
list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS
list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS
"${PROJECT_BINARY_DIR}/src"
"${PROJECT_SOURCE_DIR}/src"
)
@ -293,8 +293,8 @@ if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i6
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
elseif (CMAKE_CXX_COMPILER_ID MATCHES "Intel")
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
# Intel's compiler requires linking with libiomp5
list(APPEND Z3_DEPENDENT_LIBS "iomp5")
# Intel's compiler requires linking with libiomp5
list(APPEND Z3_DEPENDENT_LIBS "iomp5")
elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
set(SSE_FLAGS "/arch:SSE2")
else()
@ -624,7 +624,7 @@ install(
################################################################################
# Examples
################################################################################
cmake_dependent_option(Z3_ENABLE_EXAMPLE_TARGETS
cmake_dependent_option(Z3_ENABLE_EXAMPLE_TARGETS
"Build Z3 api examples" ON
"CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
if (Z3_ENABLE_EXAMPLE_TARGETS)

69
RELEASE_NOTES → RELEASE_NOTES.md
View file

@ -1,6 +1,6 @@
RELEASE NOTES
Version 4.8.next
Version 4.9.next
================
- Planned features
- sat.euf
@ -10,6 +10,42 @@ Version 4.8.next
- native word level bit-vector solving.
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
Version 4.9.1
=============
- Bugfix release to ensure npm package works
Version 4.9.0
=============
- Native M1 (Mac ARM64) binaries and pypi distribution.
- thanks to Isabel Garcia Contreras and Arie Gurfinkel for testing and fixes
- API for incremental parsing of assertions.
A description of the feature is given by example here: https://github.com/Z3Prover/z3/commit/815518dc026e900392bf0d08ed859e5ec42d1e43
It also allows incrementality at the level of adding assertions to the
solver object.
- Fold/map for sequences:
https://microsoft.github.io/z3guide/docs/guide/Sequences#map-and-fold
At this point these functions are only exposed over the SMTLIB2 interface (and not programmatic API)
maxdiff/mindiff on arrays are more likely to be deprecated
- User Propagator:
- Add functions and callbacks for external control over branching thanks to Clemens Eisenhofer
- A functioning dotnet API for the User Propagator
https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/UserPropagator.cs
- Java Script API
- higher level object wrappers are available thanks to Kevin Gibbons and Olaf Tomalka
- Totalizers and RC2
- The MaxSAT engine now allows to run RC2 with totalizer encoding.
Totalizers are on by default as preliminary tests suggest this solves already 10% more problems on
standard benchmarks. The option opt.rc2.totalizer (which by default is true) is used to control whether to use
totalizer encoding or built-in cardinality constraints.
The default engine is still maxres, so you have to set opt.maxsat_engine=rc2 to
enable the rc2 option at this point. The engines maxres-bin and rc2bin are experimental should not be used
(they are inferior to default options).
- Incremental constraints during optimization set option opt.incremental = true
- The interface `Z3_optimize_register_model_eh` allows to monitor incremental results during optimization.
It is now possible to also add constraints to the optimization context during search.
You have to set the option opt.incremental=true to be able to add constraints. The option
disables some pre-processing functionality that removes variables from the constraints.
Version 4.8.17
==============
- fix breaking bug in python interface for user propagator pop
@ -17,6 +53,29 @@ Version 4.8.17
- initial support for nested algebraic datatypes with sequences
- initiate map/fold operators on sequences - full integration for next releases
- initiate maxdiff/mindiff on arrays - full integration for next releases
Examples:
```
(declare-sort Expr)
(declare-sort Var)
(declare-datatypes ((Stmt 0))
(((Assignment (lval Var) (rval Expr))
(If (cond Expr) (th Stmt) (el Stmt))
(Seq (stmts (Seq Stmt))))))
(declare-const s Stmt)
(declare-const t Stmt)
(assert ((_ is Seq) t))
(assert ((_ is Seq) s))
(assert (= s (seq.nth (stmts t) 2)))
(assert (>= (seq.len (stmts s)) 5))
(check-sat)
(get-model)
(assert (= s (Seq (seq.unit s))))
(check-sat)
```
Version 4.8.16
==============
@ -964,7 +1023,7 @@ The following bugs are fixed in this release:
- Non-termination problem associated with option LOOKAHEAD=true.
It gets set for QF_UF in auto-configuration mode.
Thanks to Pierre-Christophe Bué.
Thanks to Pierre-Christophe Bué.
- Incorrect axioms created for injective functions.
Thanks to Sascha Boehme.
@ -986,7 +1045,7 @@ Version 2.6
===========
This release fixes a few bugs.
Thanks to Marko Kääramees for reporting a bug in the strong context simplifier and
Thanks to Marko Kääramees for reporting a bug in the strong context simplifier and
to Josh Berdine.
This release also introduces some new preprocessing features:
@ -1018,7 +1077,7 @@ This release introduces the following features:
<tt>Z3_update_param_value</tt> in the C API. This is particularly useful
for turning the strong context simplifier on and off.
It also fixes bugs reported by Enric Rodríguez Carbonell,
It also fixes bugs reported by Enric Rodríguez Carbonell,
Nuno Lopes, Josh Berdine, Ethan Jackson, Rob Quigley and
Lucas Cordeiro.
@ -1085,7 +1144,7 @@ Version 2.1
===========
This is a bug fix release.
Many thanks to Robert Brummayer, Carine Pascal, François Remy,
Many thanks to Robert Brummayer, Carine Pascal, François Remy,
Rajesh K Karmani, Roberto Lublinerman and numerous others for their
feedback and bug reports.

1
doc/mk_api_doc.py
View file

@ -335,6 +335,7 @@ try:
for modulename in (
'z3',
'z3.z3',
'z3.z3consts',
'z3.z3core',
'z3.z3num',

3
doc/website.dox.in
View file

@ -8,6 +8,5 @@
This website hosts the automatically generated documentation for the Z3 APIs.
- \ref @C_API@
- \ref @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@
- \ref @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@
*/

27
package-lock.json generated Normal file
View file

@ -0,0 +1,27 @@
{
"requires": true,
"lockfileVersion": 1,
"dependencies": {
"async-mutex": {
"version": "0.3.2",
"resolved": "https://registry.npmjs.org/async-mutex/-/async-mutex-0.3.2.tgz",
"integrity": "sha512-HuTK7E7MT7jZEh1P9GtRW9+aTWiDWWi9InbZ5hjxrnRa39KS4BW04+xLBhYNS2aXhHUIKZSw3gj4Pn1pj+qGAA==",
"requires": {
"tslib": "^2.3.1"
}
},
"tslib": {
"version": "2.4.0",
"resolved": "https://registry.npmjs.org/tslib/-/tslib-2.4.0.tgz",
"integrity": "sha512-d6xOpEDfsi2CZVlPQzGeux8XMwLT9hssAsaPYExaQMuYskwb+x1x7J371tWlbBdWHroy99KnVB6qIkUbs5X3UQ=="
},
"z3-solver": {
"version": "4.9.0",
"resolved": "https://registry.npmjs.org/z3-solver/-/z3-solver-4.9.0.tgz",
"integrity": "sha512-clSV0uyHsfrO84pSbHxoqvmd5HgSG4CoSJG2f8U65hBVylbV6p/0svctQWee9W2fWo0IsxHYRjxz2Z85GT0LAA==",
"requires": {
"async-mutex": "^0.3.2"
}
}
}
}

2
scripts/mk_project.py
View file

@ -8,7 +8,7 @@
from mk_util import *
def init_version():
set_version(4, 8, 18, 0)
set_version(4, 9, 2, 0)
# Z3 Project definition
def init_project_def():

2
scripts/mk_util.py
View file

@ -1831,7 +1831,7 @@ class JavaDLLComponent(Component):
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
os.path.join('api', 'java', 'Native'))
else:
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) $(SLINK_EXTRA_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
os.path.join('api', 'java', 'Native'))
out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
deps = ''

4
scripts/nightly.yaml
View file

@ -1,8 +1,8 @@
variables:
Major: '4'
Minor: '8'
Patch: '18'
Minor: '9'
Patch: '2'
NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
stages:

65
scripts/release.yml
View file

@ -6,7 +6,7 @@
trigger: none
variables:
ReleaseVersion: '4.8.18'
ReleaseVersion: '4.9.2'
stages:
@ -44,25 +44,18 @@ stages:
targetPath: $(Build.ArtifactStagingDirectory)
- job: MacBuildArm64
displayName: "macOS Build"
displayName: "macOS ARM64 Build"
pool:
vmImage: "macOS-latest"
steps:
- task: PythonScript@0
displayName: Build
- script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 --os=osx-11.0
- script: git clone https://github.com/z3prover/z3test z3test
- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
- task: PublishPipelineArtifact@1
inputs:
scriptSource: 'filepath'
scriptPath: scripts/mk_unix_dist.py
arguments: --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --nojava --arch=arm64 --os=osx-11.0
- task: CopyFiles@2
inputs:
sourceFolder: dist
contents: '*.zip'
targetFolder: $(Build.ArtifactStagingDirectory)
- task: PublishPipelineArtifact@0
inputs:
artifactName: 'macOSBuildArm64'
artifactName: 'MacArm64'
targetPath: $(Build.ArtifactStagingDirectory)
- job: UbuntuBuild
@ -130,22 +123,14 @@ stages:
targetPath: $(Build.ArtifactStagingDirectory)
- job: LinuxBuilds
strategy:
matrix:
manyLinux:
name: ManyLinux
image: "quay.io/pypa/manylinux2010_x86_64:latest"
python: "/opt/python/cp37-cp37m/bin/python"
muslLinux:
name: MuslLinux
image: "quay.io/pypa/musllinux_1_1_x86_64:latest"
python: "/opt/python/cp310-cp310/bin/python"
displayName: "$(name) build"
displayName: "ManyLinux build"
variables:
name: ManyLinux
image: "quay.io/pypa/manylinux2010_x86_64:latest"
python: "/opt/python/cp37-cp37m/bin/python"
pool:
vmImage: "ubuntu-latest"
container: $(image)
variables:
python: $(python)
container: "quay.io/pypa/manylinux2010_x86_64:latest"
steps:
- task: PythonScript@0
displayName: Build
@ -170,7 +155,7 @@ stages:
targetFolder: $(Build.ArtifactStagingDirectory)
- task: PublishPipelineArtifact@0
inputs:
artifactName: '$(name)Build'
artifactName: 'ManyLinuxBuild'
targetPath: $(Build.ArtifactStagingDirectory)
- template: build-win-signed.yml
@ -405,16 +390,16 @@ stages:
inputs:
artifact: 'macOSBuild'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download macOS Arm64 Build'
inputs:
artifact: 'MacArm64'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download ManyLinux Build'
inputs:
artifact: 'ManyLinuxBuild'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download MuslLinux Build'
inputs:
artifact: 'MuslLinuxBuild'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download Win32 Build'
inputs:
@ -425,19 +410,17 @@ stages:
inputs:
artifact: 'WindowsBuild-x64'
path: $(Agent.TempDirectory)
- script: cd $(Agent.TempDirectory); mkdir osx-bin; cd osx-bin; unzip ../*osx*.zip
- script: cd $(Agent.TempDirectory); mkdir osx-x64-bin; cd osx-x64-bin; unzip ../*x64-osx*.zip
- script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*arm64-osx*.zip
- script: cd $(Agent.TempDirectory); mkdir libc-bin; cd libc-bin; unzip ../*glibc*.zip
- script: cd $(Agent.TempDirectory); mkdir musl-bin; cd musl-bin; unzip ../*-linux.zip
- script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip
- script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip
- script: python3 -m pip install --user -U setuptools wheel
- script: cd src/api/python; python3 setup.py sdist
# take a look at this PREMIUM HACK I came up with to get around the fact that the azure variable syntax overloads the bash syntax for subshells
- script: cd src/api/python; echo $(Agent.TempDirectory)/osx-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/osx-x64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/osx-arm64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/libc-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/musl-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win32-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- task: PublishPipelineArtifact@0
@ -473,7 +456,7 @@ stages:
- task: DownloadPipelineArtifact@2
displayName: 'Download macOSArm64 Build'
inputs:
artifact: 'macOSBuildArm64'
artifact: 'MacArm64'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download Win32 Build'
@ -513,7 +496,7 @@ stages:
releaseNotes: '$(ReleaseVersion) release'
assets: '$(Agent.TempDirectory)/*.*'
isDraft: true
isPreRelease: false
isPreRelease: true
# Enable on release (after fixing Nuget key)
- job: NuGetPublish

13
scripts/update_api.py
View file

@ -91,7 +91,7 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint',
# Mapping to ML types
Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int64', UINT64 : 'int64', 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', LBOOL : 'int' }
@ -254,8 +254,10 @@ def param2pystr(p):
def param2ml(p):
k = param_kind(p)
if k == OUT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL or param_type(p) == INT64 or param_type(p) == UINT64:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return "int"
elif param_type(p) == INT64 or param_type(p) == UINT64:
return "int64"
elif param_type(p) == STRING:
return "string"
else:
@ -689,6 +691,7 @@ def mk_java(java_src, java_dir, package_name):
java_native.write('}\n')
java_wrapper = open(java_wrapperf, 'w')
pkg_str = package_name.replace('.', '_')
java_wrapper.write("// Automatically generated file\n")
with open(java_src + "/NativeStatic.txt") as ins:
for line in ins:
java_wrapper.write(line)
@ -1251,9 +1254,9 @@ def ml_unwrap(t, ts, s):
elif t == UINT:
return '(' + ts + ') Unsigned_int_val(' + s + ')'
elif t == INT64:
return '(' + ts + ') Long_val(' + s + ')'
return '(' + ts + ') Int64_val(' + s + ')'
elif t == UINT64:
return '(' + ts + ') Unsigned_long_val(' + s + ')'
return '(' + ts + ') Int64_val(' + s + ')'
elif t == DOUBLE:
return '(' + ts + ') Double_val(' + s + ')'
elif ml_has_plus_type(ts):
@ -1270,7 +1273,7 @@ def ml_set_wrap(t, d, n):
elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == LBOOL:
return d + ' = Val_int(' + n + ');'
elif t == INT64 or t == UINT64:
return d + ' = Val_long(' + n + ');'
return d + ' = caml_copy_int64(' + n + ');'
elif t == DOUBLE:
return d + '= caml_copy_double(' + n + ');'
elif t == STRING:

14
src/ackermannization/ackr_model_converter.cpp
View file

@ -46,11 +46,15 @@ public:
void operator()(model_ref & md) override {
TRACE("ackermannize", tout << (fixed_model? "fixed" : "nonfixed") << "\n";);
SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
model_ref& old_model = fixed_model ? abstr_model : md;
SASSERT(old_model.get());
model * new_model = alloc(model, m);
convert(old_model.get(), new_model);
CTRACE("ackermannize", md, tout << *md << "\n");
CTRACE("ackermannize", fixed_model, tout << *abstr_model << "\n");
model* new_model = alloc(model, m);
if (abstr_model)
convert(abstr_model.get(), new_model);
if (md)
convert(md.get(), new_model);
md = new_model;
}

13
src/ackermannization/lackr_model_constructor.cpp
View file

@ -21,6 +21,7 @@
#include "ast/for_each_expr.h"
#include "ast/rewriter/bv_rewriter.h"
#include "ast/rewriter/bool_rewriter.h"
#include <iostream>
struct lackr_model_constructor::imp {
public:
@ -186,7 +187,7 @@ private:
return m_app2val.find(a, val);
}
bool evaluate(app * const a, expr_ref& result) {
bool evaluate(app * a, expr_ref& result) {
SASSERT(!is_val(a));
const unsigned num = a->get_num_args();
if (num == 0) { // handle constants
@ -232,20 +233,20 @@ private:
// Check and record the value for a given term, given that all arguments are already checked.
//
bool mk_value(app * a) {
if (is_val(a)) return true; // skip numerals
if (is_val(a))
return true; // skip numerals
TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m, 2) << ")\n";);
SASSERT(!m_app2val.contains(a));
expr_ref result(m);
if (!evaluate(a, result)) return false;
SASSERT(is_val(result));
if (!evaluate(a, result))
return false;
TRACE("model_constructor",
tout << "map term(\n" << mk_ismt2_pp(a, m, 2) << "\n->"
<< mk_ismt2_pp(result.get(), m, 2)<< ")\n"; );
CTRACE("model_constructor",
!is_val(result.get()),
tout << "eval fail\n" << mk_ismt2_pp(a, m, 2) << mk_ismt2_pp(result, m, 2) << "\n";
tout << "eval didn't create a constant \n" << mk_ismt2_pp(a, m, 2) << " " << mk_ismt2_pp(result, m, 2) << "\n";
);
SASSERT(is_val(result.get()));
m_app2val.insert(a, result.get()); // memoize
m_pinned.push_back(a);
m_pinned.push_back(result);

65
src/api/api_context.cpp
View file

@ -35,11 +35,12 @@ namespace api {
object::object(context& c): m_ref_count(0), m_context(c) { this->m_id = m_context.add_object(this); }
void object::inc_ref() { m_ref_count++; }
void object::inc_ref() { ++m_ref_count; }
void object::dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) m_context.del_object(this); }
void object::dec_ref() { SASSERT(m_ref_count > 0); if (--m_ref_count == 0) m_context.del_object(this); }
unsigned context::add_object(api::object* o) {
flush_objects();
unsigned id = m_allocated_objects.size();
if (!m_free_object_ids.empty()) {
id = m_free_object_ids.back();
@ -50,9 +51,52 @@ namespace api {
}
void context::del_object(api::object* o) {
m_free_object_ids.push_back(o->id());
m_allocated_objects.remove(o->id());
dealloc(o);
#ifndef SINGLE_THREAD
if (m_concurrent_dec_ref) {
lock_guard lock(m_mux);
m_objects_to_flush.push_back(o);
}
else
#endif
{
m_free_object_ids.push_back(o->id());
m_allocated_objects.remove(o->id());
dealloc(o);
}
}
void context::dec_ref(ast* a) {
#ifndef SINGLE_THREAD
if (m_concurrent_dec_ref) {
lock_guard lock(m_mux);
m_asts_to_flush.push_back(a);
}
else
#endif
m().dec_ref(a);
}
void context::flush_objects() {
#ifndef SINGLE_THREAD
if (!m_concurrent_dec_ref)
return;
{
lock_guard lock(m_mux);
if (m_asts_to_flush.empty() && m_objects_to_flush.empty())
return;
m_asts_to_flush2.swap(m_asts_to_flush);
m_objects_to_flush2.swap(m_objects_to_flush);
}
for (ast* a : m_asts_to_flush2)
m().dec_ref(a);
for (auto* o : m_objects_to_flush2) {
m_free_object_ids.push_back(o->id());
m_allocated_objects.remove(o->id());
dealloc(o);
}
m_objects_to_flush2.reset();
m_asts_to_flush2.reset();
#endif
}
static void default_error_handler(Z3_context ctx, Z3_error_code c) {
@ -106,6 +150,7 @@ namespace api {
context::~context() {
m_last_obj = nullptr;
flush_objects();
for (auto& kv : m_allocated_objects) {
api::object* val = kv.m_value;
DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name()););
@ -356,6 +401,13 @@ extern "C" {
Z3_CATCH;
}
void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c) {
Z3_TRY;
LOG_Z3_enable_concurrent_dec_ref(c);
mk_c(c)->enable_concurrent_dec_ref();
Z3_CATCH;
}
void Z3_API Z3_toggle_warning_messages(bool enabled) {
LOG_Z3_toggle_warning_messages(enabled);
enable_warning_messages(enabled != 0);
@ -365,6 +417,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_inc_ref(c, a);
RESET_ERROR_CODE();
mk_c(c)->flush_objects();
mk_c(c)->m().inc_ref(to_ast(a));
Z3_CATCH;
}
@ -379,7 +432,7 @@ extern "C" {
return;
}
if (a) {
mk_c(c)->m().dec_ref(to_ast(a));
mk_c(c)->dec_ref(to_ast(a));
}
Z3_CATCH;
}

20
src/api/api_context.h
View file

@ -75,6 +75,9 @@ namespace api {
struct add_plugins { add_plugins(ast_manager & m); };
ast_context_params m_params;
bool m_user_ref_count; //!< if true, the user is responsible for managing reference counters.
#ifndef SINGLE_THREAD
bool m_concurrent_dec_ref = false;
#endif
scoped_ptr<ast_manager> m_manager;
scoped_ptr<cmd_context> m_cmd;
add_plugins m_plugins;
@ -91,8 +94,12 @@ namespace api {
smt_params m_fparams;
// -------------------------------
ast_ref_vector m_ast_trail;
#ifndef SINGLE_THREAD
ptr_vector<ast> m_asts_to_flush, m_asts_to_flush2;
ptr_vector<api::object> m_objects_to_flush, m_objects_to_flush2;
#endif
ast_ref_vector m_ast_trail;
ref<api::object> m_last_obj; //!< reference to the last API object returned by the APIs
u_map<api::object*> m_allocated_objects; // !< table containing current set of allocated API objects
unsigned_vector m_free_object_ids; // !< free list of identifiers available for allocated objects.
@ -169,9 +176,18 @@ namespace api {
void set_error_code(Z3_error_code err, char const* opt_msg);
void set_error_code(Z3_error_code err, std::string &&opt_msg);
void set_error_handler(Z3_error_handler h) { m_error_handler = h; }
void enable_concurrent_dec_ref() {
#ifdef SINGLE_THREAD
set_error_code(Z3_EXCEPTION, "Can't use concurrent features with a single-thread build");
#else
m_concurrent_dec_ref = true;
#endif
}
unsigned add_object(api::object* o);
void del_object(api::object* o);
void dec_ref(ast* a);
void flush_objects();
Z3_ast_print_mode get_print_mode() const { return m_print_mode; }
void set_print_mode(Z3_ast_print_mode m) { m_print_mode = m; }

210
src/api/api_parsers.cpp
View file

@ -35,6 +35,136 @@ extern "C" {
// ---------------
// Support for SMTLIB2
struct Z3_parser_context_ref : public api::object {
scoped_ptr<cmd_context> ctx;
Z3_parser_context_ref(api::context& c): api::object(c) {
ast_manager& m = c.m();
ctx = alloc(cmd_context, false, &(m));
install_dl_cmds(*ctx.get());
install_opt_cmds(*ctx.get());
install_smt2_extra_cmds(*ctx.get());
ctx->register_plist();
ctx->set_ignore_check(true);
}
~Z3_parser_context_ref() override {}
};
inline Z3_parser_context_ref * to_parser_context(Z3_parser_context pc) { return reinterpret_cast<Z3_parser_context_ref*>(pc); }
inline Z3_parser_context of_parser_context(Z3_parser_context_ref* pc) { return reinterpret_cast<Z3_parser_context>(pc); }
Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c) {
Z3_TRY;
LOG_Z3_mk_parser_context(c);
RESET_ERROR_CODE();
Z3_parser_context_ref * pc = alloc(Z3_parser_context_ref, *mk_c(c));
mk_c(c)->save_object(pc);
Z3_parser_context r = of_parser_context(pc);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}
void Z3_API Z3_parser_context_inc_ref(Z3_context c, Z3_parser_context pc) {
Z3_TRY;
LOG_Z3_parser_context_inc_ref(c, pc);
RESET_ERROR_CODE();
to_parser_context(pc)->inc_ref();
Z3_CATCH;
}
void Z3_API Z3_parser_context_dec_ref(Z3_context c, Z3_parser_context pc) {
Z3_TRY;
LOG_Z3_parser_context_dec_ref(c, pc);
RESET_ERROR_CODE();
to_parser_context(pc)->dec_ref();
Z3_CATCH;
}
static void insert_datatype(ast_manager& m, scoped_ptr<cmd_context>& ctx, sort* srt) {
datatype_util dt(m);
if (!dt.is_datatype(srt))
return;
for (func_decl * c : *dt.get_datatype_constructors(srt)) {
ctx->insert(c->get_name(), c);
func_decl * r = dt.get_constructor_recognizer(c);
ctx->insert(r->get_name(), r);
for (func_decl * a : *dt.get_constructor_accessors(c)) {
ctx->insert(a->get_name(), a);
}
}
}
static void insert_sort(ast_manager& m, scoped_ptr<cmd_context>& ctx, symbol const& name, sort* srt) {
if (ctx->find_psort_decl(name))
return;
psort* ps = ctx->pm().mk_psort_cnst(srt);
ctx->insert(ctx->pm().mk_psort_user_decl(0, name, ps));
insert_datatype(m, ctx, srt);
}
void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s) {
Z3_TRY;
LOG_Z3_parser_context_add_sort(c, pc, s);
RESET_ERROR_CODE();
auto& ctx = to_parser_context(pc)->ctx;
sort* srt = to_sort(s);
symbol name = srt->get_name();
insert_sort(mk_c(c)->m(), ctx, name, srt);
Z3_CATCH;
}
void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f) {
Z3_TRY;
LOG_Z3_parser_context_add_decl(c, pc, f);
RESET_ERROR_CODE();
auto& ctx = *to_parser_context(pc)->ctx;
func_decl* fn = to_func_decl(f);
symbol name = fn->get_name();
ctx.insert(name, fn);
Z3_CATCH;
}
Z3_ast_vector Z3_parser_context_parse_stream(Z3_context c, scoped_ptr<cmd_context>& ctx, bool owned, std::istream& is) {
Z3_TRY;
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
std::stringstream errstrm;
ctx->set_regular_stream(errstrm);
try {
if (!parse_smt2_commands(*ctx, is)) {
if (owned)
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return of_ast_vector(v);
}
}
catch (z3_exception& e) {
if (owned)
ctx = nullptr;
errstrm << e.msg();
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return of_ast_vector(v);
}
for (expr* e : ctx->tracked_assertions())
v->m_ast_vector.push_back(e);
ctx->reset_tracked_assertions();
return of_ast_vector(v);
Z3_CATCH_RETURN(nullptr);
}
Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string str) {
Z3_TRY;
LOG_Z3_parser_context_from_string(c, pc, str);
std::string s(str);
std::istringstream is(s);
auto& ctx = to_parser_context(pc)->ctx;
Z3_ast_vector r = Z3_parser_context_parse_stream(c, ctx, false, is);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}
Z3_ast_vector parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is,
unsigned num_sorts,
Z3_symbol const _sort_names[],
@ -48,70 +178,16 @@ extern "C" {
install_dl_cmds(*ctx.get());
install_opt_cmds(*ctx.get());
install_smt2_extra_cmds(*ctx.get());
ctx->register_plist();
ctx->set_ignore_check(true);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
vector<symbol> sort_names;
ptr_vector<sort> sorts;
for (unsigned i = 0; i < num_sorts; ++i) {
sorts.push_back(to_sort(_sorts[i]));
sort_names.push_back(to_symbol(_sort_names[i]));
}
mk_c(c)->save_object(v);
for (unsigned i = 0; i < num_decls; ++i) {
func_decl* d = to_func_decl(decls[i]);
ctx->insert(to_symbol(decl_names[i]), d);
sort_names.push_back(d->get_range()->get_name());
sorts.push_back(d->get_range());
for (sort* s : *d) {
sort_names.push_back(s->get_name());
sorts.push_back(s);
}
}
datatype_util dt(m);
for (unsigned i = 0; i < num_sorts; ++i) {
sort* srt = sorts[i];
symbol name = sort_names[i];
if (ctx->find_psort_decl(name)) {
continue;
}
psort* ps = ctx->pm().mk_psort_cnst(srt);
ctx->insert(ctx->pm().mk_psort_user_decl(0, name, ps));
if (!dt.is_datatype(srt)) {
continue;
}
for (unsigned i = 0; i < num_decls; ++i)
ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
for (func_decl * c : *dt.get_datatype_constructors(srt)) {
ctx->insert(c->get_name(), c);
func_decl * r = dt.get_constructor_recognizer(c);
ctx->insert(r->get_name(), r);
for (func_decl * a : *dt.get_constructor_accessors(c)) {
ctx->insert(a->get_name(), a);
}
}
}
std::stringstream errstrm;
ctx->set_regular_stream(errstrm);
try {
if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return of_ast_vector(v);
}
}
catch (z3_exception& e) {
errstrm << e.msg();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return of_ast_vector(v);
}
for (expr* e : ctx->tracked_assertions()) {
v->m_ast_vector.push_back(e);
}
return of_ast_vector(v);
for (unsigned i = 0; i < num_sorts; ++i)
insert_sort(m, ctx, to_symbol(_sort_names[i]), to_sort(_sorts[i]));
return Z3_parser_context_parse_stream(c, ctx, true, is);
Z3_CATCH_RETURN(nullptr);
}
@ -155,11 +231,13 @@ extern "C" {
Z3_TRY;
LOG_Z3_eval_smtlib2_string(c, str);
if (!mk_c(c)->cmd()) {
mk_c(c)->cmd() = alloc(cmd_context, false, &(mk_c(c)->m()));
install_dl_cmds(*mk_c(c)->cmd());
install_opt_cmds(*mk_c(c)->cmd());
install_smt2_extra_cmds(*mk_c(c)->cmd());
mk_c(c)->cmd()->set_solver_factory(mk_smt_strategic_solver_factory());
auto* ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
mk_c(c)->cmd() = ctx;
install_dl_cmds(*ctx);
install_opt_cmds(*ctx);
install_smt2_extra_cmds(*ctx);
ctx->register_plist();
ctx->set_solver_factory(mk_smt_strategic_solver_factory());
}
scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd();
std::string s(str);
@ -180,4 +258,6 @@ extern "C" {
RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str()));
}
};

14
src/api/api_solver.cpp
View file

@ -256,7 +256,10 @@ extern "C" {
}
void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) {
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
auto& solver = *to_solver(s);
if (!solver.m_cmd_context)
solver.m_cmd_context = alloc(cmd_context, false, &(mk_c(c)->m()));
auto& ctx = solver.m_cmd_context;
ctx->set_ignore_check(true);
std::stringstream errstrm;
ctx->set_regular_stream(errstrm);
@ -272,6 +275,7 @@ extern "C" {
init_solver(c, s);
for (expr* e : ctx->tracked_assertions())
to_solver(s)->assert_expr(e);
ctx->reset_tracked_assertions();
to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
}
@ -387,9 +391,11 @@ extern "C" {
bool new_model = params.get_bool("model", true);
if (old_model != new_model)
to_solver_ref(s)->set_produce_models(new_model);
param_descrs r;
to_solver_ref(s)->collect_param_descrs(r);
context_params::collect_solver_param_descrs(r);
param_descrs& r = to_solver(s)->m_param_descrs;
if(r.size () == 0) {
to_solver_ref(s)->collect_param_descrs(r);
context_params::collect_solver_param_descrs(r);
}
params.validate(r);
to_solver_ref(s)->updt_params(params);
}

2
src/api/api_solver.h
View file

@ -42,8 +42,10 @@ struct Z3_solver_ref : public api::object {
scoped_ptr<solver_factory> m_solver_factory;
ref<solver> m_solver;
params_ref m_params;
param_descrs m_param_descrs;
symbol m_logic;
scoped_ptr<solver2smt2_pp> m_pp;
scoped_ptr<cmd_context> m_cmd_context;
mutex m_mux;
event_handler* m_eh;

5
src/api/api_util.h
View file

@ -19,6 +19,7 @@ Revision History:
#include "util/params.h"
#include "util/lbool.h"
#include "util/mutex.h"
#include "ast/ast.h"
#define Z3_TRY try {
@ -34,7 +35,7 @@ namespace api {
// Generic wrapper for ref-count objects exposed by the API
class object {
unsigned m_ref_count;
atomic<unsigned> m_ref_count;
unsigned m_id;
context& m_context;
public:
@ -87,7 +88,6 @@ inline lbool to_lbool(Z3_lbool b) { return static_cast<lbool>(b); }
struct Z3_params_ref : public api::object {
params_ref m_params;
Z3_params_ref(api::context& c): api::object(c) {}
~Z3_params_ref() override {}
};
inline Z3_params_ref * to_params(Z3_params p) { return reinterpret_cast<Z3_params_ref *>(p); }
@ -97,7 +97,6 @@ inline params_ref& to_param_ref(Z3_params p) { return p == nullptr ? const_cast<
struct Z3_param_descrs_ref : public api::object {
param_descrs m_descrs;
Z3_param_descrs_ref(api::context& c): api::object(c) {}
~Z3_param_descrs_ref() override {}
};
inline Z3_param_descrs_ref * to_param_descrs(Z3_param_descrs p) { return reinterpret_cast<Z3_param_descrs_ref *>(p); }

8
src/api/dotnet/Context.cs
View file

@ -4620,16 +4620,16 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// Produces a term that represents the conversion of the floating-point term t into a
/// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary,
/// bit-vector term of size sz in 2's complement format (signed when sign==true). If necessary,
/// the result will be rounded according to rounding mode rm.
/// </remarks>
/// <param name="rm">RoundingMode term.</param>
/// <param name="t">FloatingPoint term</param>
/// <param name="sz">Size of the resulting bit-vector.</param>
/// <param name="signed">Indicates whether the result is a signed or unsigned bit-vector.</param>
public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
/// <param name="sign">Indicates whether the result is a signed or unsigned bit-vector.</param>
public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool sign)
{
if (signed)
if (sign)
return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
else
return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));

10
src/api/dotnet/Expr.cs
View file

@ -168,6 +168,16 @@ namespace Microsoft.Z3
{
return (Expr)base.Translate(ctx);
}
/// <summary>
/// Create a duplicate of expression.
/// This feature is to allow extending the life-time of expressions that were passed down as arguments
/// by the user propagator callbacks. By default the life-time of arguments to callbacks is within the
/// callback only.
/// </summary>
public Expr Dup() {
return Expr.Create(Context, NativeObject);
}
/// <summary>
/// Returns a string representation of the expression.

413
src/api/dotnet/UserPropagator.cs
View file

@ -37,277 +37,326 @@ namespace Microsoft.Z3
/// <summary>
/// Propagator context for .Net
/// </summary>
public class UserPropagator
public class UserPropagator
{
/// <summary>
/// Delegate type for fixed callback
/// Note that the life-time of the term and value only applies within the scope of the callback.
/// That means the term and value cannot be stored in an array, dictionary or similar and accessed after the callback has returned.
/// Use the functionality Dup on expressions to create a duplicate copy that extends the lifetime.
/// </summary>
public delegate void FixedEh(Expr term, Expr value);
public delegate void FixedEh(Expr term, Expr value);
/// <summary>
/// Delegate type for equality or disequality callback
/// </summary>
public delegate void EqEh(Expr term, Expr value);
public delegate void EqEh(Expr term, Expr value);
/// <summary>
/// Delegate type for when a new term using a registered function symbol is created internally
/// </summary>
public delegate void CreatedEh(Expr term);
public delegate void CreatedEh(Expr term);
/// <summary>
/// Delegate type for callback into solver's branching
/// <param name="term">A bit-vector or Boolean used for branching</param>
/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
/// <param name="phase">Set phase to -1 (false) or 1 (true) to override solver's phase</param>
/// </summary>
public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase);
/// <param name="term">A bit-vector or Boolean used for branching</param>
/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
/// <param name="phase">Set phase to -1 (false) or 1 (true) to override solver's phase</param>
/// </summary>
public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase);
// access managed objects through a static array.
// thread safety is ignored for now.
GCHandle gch;
Solver solver;
Context ctx;
Z3_solver_callback callback = IntPtr.Zero;
FixedEh fixed_eh;
Action final_eh;
EqEh eq_eh;
EqEh diseq_eh;
CreatedEh created_eh;
DecideEh decide_eh;
Solver solver;
Context ctx;
GCHandle gch;
Z3_solver_callback callback = IntPtr.Zero;
FixedEh fixed_eh;
Action final_eh;
EqEh eq_eh;
EqEh diseq_eh;
CreatedEh created_eh;
DecideEh decide_eh;
Native.Z3_push_eh push_eh;
Native.Z3_pop_eh pop_eh;
Native.Z3_fresh_eh fresh_eh;
void Callback(Action fn, Z3_solver_callback cb) {
this.callback = cb;
try {
fn();
}
catch {
// TBD: add debug log or exception handler
}
finally {
this.callback = IntPtr.Zero;
}
}
Native.Z3_fixed_eh fixed_wrapper;
Native.Z3_final_eh final_wrapper;
Native.Z3_eq_eh eq_wrapper;
Native.Z3_eq_eh diseq_wrapper;
Native.Z3_decide_eh decide_wrapper;
Native.Z3_created_eh created_wrapper;
void Callback(Action fn, Z3_solver_callback cb)
{
this.callback = cb;
try
{
fn();
}
catch
{
// TBD: add debug log or exception handler
}
finally
{
this.callback = IntPtr.Zero;
}
}
static void _push(voidp ctx, Z3_solver_callback cb) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
prop.Callback(() => prop.Push(), cb);
}
static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
prop.Callback(() => prop.Pop(num_scopes), cb);
}
static voidp _fresh(voidp _ctx, Z3_context new_context) {
var gch = GCHandle.FromIntPtr(_ctx);
var prop = (UserPropagator)gch.Target;
var ctx = new Context(new_context);
var prop1 = prop.Fresh(ctx);
return GCHandle.ToIntPtr(prop1.gch);
}
static void _push(voidp ctx, Z3_solver_callback cb)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(ctx).Target;
prop.Callback(() => prop.Push(), cb);
}
static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
using var term = Expr.Create(prop.ctx, _term);
using var value = Expr.Create(prop.ctx, _value);
prop.Callback(() => prop.fixed_eh(term, value), cb);
}
static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(ctx).Target;
prop.Callback(() => prop.Pop(num_scopes), cb);
}
static void _final(voidp ctx, Z3_solver_callback cb) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
prop.Callback(() => prop.final_eh(), cb);
}
static voidp _fresh(voidp _ctx, Z3_context new_context)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(_ctx).Target;
var ctx = new Context(new_context);
var prop1 = prop.Fresh(prop.ctx);
return GCHandle.ToIntPtr(prop1.gch);
}
static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b);
prop.Callback(() => prop.eq_eh(s, t), cb);
}
static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(ctx).Target;
using var term = Expr.Create(prop.ctx, _term);
using var value = Expr.Create(prop.ctx, _value);
prop.Callback(() => prop.fixed_eh(term, value), cb);
}
static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b);
prop.Callback(() => prop.diseq_eh(s, t), cb);
}
static void _final(voidp ctx, Z3_solver_callback cb)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(ctx).Target;
prop.Callback(() => prop.final_eh(), cb);
}
static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
using var t = Expr.Create(prop.ctx, a);
prop.Callback(() => prop.created_eh(t), cb);
}
static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(ctx).Target;
using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b);
prop.Callback(() => prop.eq_eh(s, t), cb);
}
static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) {
var gch = GCHandle.FromIntPtr(ctx);
var prop = (UserPropagator)gch.Target;
var t = Expr.Create(prop.ctx, a);
var u = t;
prop.callback = cb;
prop.decide_eh(ref t, ref idx, ref phase);
prop.callback = IntPtr.Zero;
if (u != t)
a = t.NativeObject;
}
static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(ctx).Target;
using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b);
prop.Callback(() => prop.diseq_eh(s, t), cb);
}
static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(ctx).Target;
using var t = Expr.Create(prop.ctx, a);
prop.Callback(() => prop.created_eh(t), cb);
}
static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(ctx).Target;
var t = Expr.Create(prop.ctx, a);
var u = t;
prop.callback = cb;
prop.decide_eh(ref t, ref idx, ref phase);
prop.callback = IntPtr.Zero;
if (u != t)
a = t.NativeObject;
}
/// <summary>
/// Propagator constructor from a solver class.
/// </summary>
public UserPropagator(Solver s)
{
gch = GCHandle.Alloc(this);
solver = s;
ctx = solver.Context;
var cb = GCHandle.ToIntPtr(gch);
Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, cb, _push, _pop, _fresh);
}
{
gch = GCHandle.Alloc(this);
solver = s;
ctx = solver.Context;
push_eh = _push;
pop_eh = _pop;
fresh_eh = _fresh;
Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, GCHandle.ToIntPtr(gch), push_eh, pop_eh, fresh_eh);
}
/// <summary>
/// Propagator constructor from a context. It is used from inside of Fresh.
/// </summary>
public UserPropagator(Context _ctx)
{
gch = GCHandle.Alloc(this);
{
gch = GCHandle.Alloc(this);
solver = null;
ctx = _ctx;
}
ctx = _ctx;
}
/// <summary>
/// Release provate memory.
/// </summary>
~UserPropagator()
{
if (gch != null)
gch.Free();
~UserPropagator()
{
gch.Free();
if (solver == null)
ctx.Dispose();
}
}
/// <summary>
/// Virtual method for push. It must be overwritten by inherited class.
/// </summary>
public virtual void Push() { throw new Z3Exception("Push method should be overwritten"); }
/// </summary>
public virtual void Push() { throw new Z3Exception("Push method should be overwritten"); }
/// <summary>
/// Virtual method for pop. It must be overwritten by inherited class.
/// </summary>
public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); }
/// </summary>
public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); }
/// <summary>
/// Virtual method for fresh. It can be overwritten by inherited class.
/// </summary>
public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); }
/// </summary>
public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); }
/// <summary>
/// Declare combination of assigned expressions a conflict
/// </summary>
void Conflict(params Expr[] terms) {
Propagate(terms, ctx.MkFalse());
/// </summary>
public void Conflict(params Expr[] terms)
{
Propagate(terms, ctx.MkFalse());
}
/// <summary>
/// Declare combination of assigned expressions a conflict
/// </summary>
public void Conflict(IEnumerable<Expr> terms)
{
Propagate(terms, ctx.MkFalse());
}
/// <summary>
/// Propagate consequence
/// </summary>
void Propagate(Expr[] terms, Expr conseq) {
var nTerms = Z3Object.ArrayToNative(terms);
Native.Z3_solver_propagate_consequence(ctx.nCtx, this.callback, (uint)nTerms.Length, nTerms, 0u, null, null, conseq.NativeObject);
/// </summary>
public void Propagate(IEnumerable<Expr> terms, Expr conseq)
{
var nTerms = Z3Object.ArrayToNative(terms.ToArray());
Native.Z3_solver_propagate_consequence(ctx.nCtx, this.callback, (uint)nTerms.Length, nTerms, 0u, null, null, conseq.NativeObject);
}
/// <summary>
/// Set fixed callback
/// </summary>
/// </summary>
public FixedEh Fixed
{
set
{
this.fixed_eh = value;
if (solver != null)
Native.Z3_solver_propagate_fixed(ctx.nCtx, solver.NativeObject, _fixed);
}
}
{
set
{
this.fixed_wrapper = _fixed;
this.fixed_eh = value;
if (solver != null)
Native.Z3_solver_propagate_fixed(ctx.nCtx, solver.NativeObject, fixed_wrapper);
}
}
/// <summary>
/// Set final callback
/// </summary>
public Action Final
{
set
{
this.final_eh = value;
if (solver != null)
Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, _final);
/// </summary>
public Action Final
{
set
{
this.final_wrapper = _final;
this.final_eh = value;
if (solver != null)
Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, final_wrapper);
}
}
/// <summary>
/// Set equality event callback
/// </summary>
public EqEh Eq
{
set
{
this.eq_eh = value;
if (solver != null)
Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, _eq);
}
/// </summary>
public EqEh Eq
{
set
{
this.eq_wrapper = _eq;
this.eq_eh = value;
if (solver != null)
Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, eq_wrapper);
}
}
/// <summary>
/// Set disequality event callback
/// </summary>
public EqEh Diseq
{
set
{
this.diseq_eh = value;
if (solver != null)
Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, _diseq);
}
/// </summary>
public EqEh Diseq
{
set
{
this.diseq_wrapper = _diseq;
this.diseq_eh = value;
if (solver != null)
Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, diseq_wrapper);
}
}
/// <summary>
/// Set created callback
/// </summary>
public CreatedEh Created
{
set
{
this.created_eh = value;
if (solver != null)
Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, _created);
}
/// </summary>
public CreatedEh Created
{
set
{
this.created_wrapper = _created;
this.created_eh = value;
if (solver != null)
Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, created_wrapper);
}
}
/// <summary>
/// Set decision callback
/// </summary>
public DecideEh Decide
{
set
{
this.decide_eh = value;
if (solver != null)
Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide);
}
/// </summary>
public DecideEh Decide
{
set
{
this.decide_wrapper = _decide;
this.decide_eh = value;
if (solver != null)
Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, decide_wrapper);
}
}
/// <summary>
/// Set the next decision
/// </summary>
public void NextSplit(Expr e, uint idx, int phase)
{
Native.Z3_solver_next_split(ctx.nCtx, this.callback, e.NativeObject, idx, phase);
}
/// <summary>
/// Track assignments to a term
/// </summary>
public void Register(Expr term) {
if (this.callback != IntPtr.Zero) {
Native.Z3_solver_propagate_register_cb(ctx.nCtx, callback, term.NativeObject);
/// </summary>
public void Register(Expr term)
{
if (this.callback != IntPtr.Zero)
{
Native.Z3_solver_propagate_register_cb(ctx.nCtx, callback, term.NativeObject);
}
else {
Native.Z3_solver_propagate_register(ctx.nCtx, solver.NativeObject, term.NativeObject);
else
{
Native.Z3_solver_propagate_register(ctx.nCtx, solver.NativeObject, term.NativeObject);
}
}
}
}
}

5
src/api/dotnet/Z3Object.cs
View file

@ -113,7 +113,10 @@ namespace Microsoft.Z3
return s.NativeObject;
}
public Context Context
/// <summary>
/// Access Context object
/// </summary>
public Context Context
{
get
{

32
src/api/java/Context.java
View file

@ -1717,8 +1717,8 @@ public class Context implements AutoCloseable {
* {@code [domain -> range]}, and {@code i} must have the sort
* {@code domain}. The sort of the result is {@code range}.
*
* @see #mkArraySort(Sort[], Sort)
* @see #mkStore
* @see #mkArraySort(Sort[], R)
* @see #mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)
**/
public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
{
@ -1739,8 +1739,8 @@ public class Context implements AutoCloseable {
* {@code [domains -> range]}, and {@code args} must have the sorts
* {@code domains}. The sort of the result is {@code range}.
*
* @see #mkArraySort(Sort[], Sort)
* @see #mkStore
* @see #mkArraySort(Sort[], R)
* @see #mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)
**/
public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] args)
{
@ -1763,8 +1763,8 @@ public class Context implements AutoCloseable {
* {@code select}) on all indices except for {@code i}, where it
* maps to {@code v} (and the {@code select} of {@code a}
* with respect to {@code i} may be a different value).
* @see #mkArraySort(Sort[], Sort)
* @see #mkSelect
* @see #mkArraySort(Sort[], R)
* @see #mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
**/
public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)
@ -1788,8 +1788,8 @@ public class Context implements AutoCloseable {
* {@code select}) on all indices except for {@code args}, where it
* maps to {@code v} (and the {@code select} of {@code a}
* with respect to {@code args} may be a different value).
* @see #mkArraySort(Sort[], Sort)
* @see #mkSelect
* @see #mkArraySort(Sort[], R)
* @see #mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
**/
public <R extends Sort> ArrayExpr<Sort, R> mkStore(Expr<ArraySort<Sort, R>> a, Expr<?>[] args, Expr<R> v)
@ -1806,8 +1806,8 @@ public class Context implements AutoCloseable {
* Remarks: The resulting term is an array, such
* that a {@code select} on an arbitrary index produces the value
* {@code v}.
* @see #mkArraySort(Sort[], Sort)
* @see #mkSelect
* @see #mkArraySort(Sort[], R)
* @see #mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
*
**/
public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkConstArray(D domain, Expr<R> v)
@ -1826,9 +1826,9 @@ public class Context implements AutoCloseable {
* {@code f} must have type {@code range_1 .. range_n -> range}.
* {@code v} must have sort range. The sort of the result is
* {@code [domain_i -> range]}.
* @see #mkArraySort(Sort[], Sort)
* @see #mkSelect
* @see #mkStore
* @see #mkArraySort(Sort[], R)
* @see #mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
* @see #mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)
**/
@SafeVarargs
@ -2476,7 +2476,7 @@ public class Context implements AutoCloseable {
*
* @return A Term with value {@code num}/{@code den}
* and sort Real
* @see #mkNumeral(String,Sort)
* @see #mkNumeral(String v, R ty)
**/
public RatNum mkReal(int num, int den)
{
@ -2612,7 +2612,7 @@ public class Context implements AutoCloseable {
* 'names' of the bound variables, and {@code body} is the body
* of the quantifier. Quantifiers are associated with weights indicating the
* importance of using the quantifier during instantiation.
* Note that the bound variables are de-Bruijn indices created using {@link #mkBound}.
* Note that the bound variables are de-Bruijn indices created using {#mkBound}.
* Z3 applies the convention that the last element in {@code names} and
* {@code sorts} refers to the variable with index 0, the second to last element
* of {@code names} and {@code sorts} refers to the variable
@ -2707,7 +2707,7 @@ public class Context implements AutoCloseable {
* with the sorts of the bound variables, {@code names} is an array with the
* 'names' of the bound variables, and {@code body} is the body of the
* lambda.
* Note that the bound variables are de-Bruijn indices created using {@link #mkBound}
* Note that the bound variables are de-Bruijn indices created using {#mkBound}
* Z3 applies the convention that the last element in {@code names} and
* {@code sorts} refers to the variable with index 0, the second to last element
* of {@code names} and {@code sorts} refers to the variable

2
src/api/java/Model.java
View file

@ -242,7 +242,7 @@ public class Model extends Z3Object {
* values. We say this finite set is the "universe" of the sort.
*
* @see #getNumSorts
* @see #getSortUniverse
* @see #getSortUniverse(R s)
*
* @throws Z3Exception
**/

3
src/api/java/NativeStatic.txt
View file

@ -1,4 +1,4 @@
// Automatically generated file
#include<jni.h>
#include<stdlib.h>
#include"z3.h"
@ -76,3 +76,4 @@ DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_setInternalErrorHand
{
Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);
}

6
src/api/java/Quantifier.java
View file

@ -161,6 +161,12 @@ public class Quantifier extends BoolExpr
/**
* Create a quantified expression.
*
* @param ctx Context to create the quantifier on.
* @param isForall Quantifier type.
* @param sorts Sorts of bound variables.
* @param names Names of bound variables
* @param body Body of quantifier
* @param weight Weight used to indicate priority for qunatifier instantiation
* @param patterns Nullable patterns
* @param noPatterns Nullable noPatterns
* @param quantifierID Nullable quantifierID

2
src/api/js/README.md
View file

@ -9,7 +9,7 @@ The readme for the bindings themselves is located in [`PUBLISHED_README.md`](./P
You'll need to have emscripten set up, along with all of its dependencies. The easiest way to do that is with [emsdk](https://github.com/emscripten-core/emsdk).
Then run `npm i` to install dependencies, `npm run build-ts` to build the TypeScript wrapper, and `npm run build-wasm` to build the wasm artifact.
Then run `npm i` to install dependencies, `npm run build:ts` to build the TypeScript wrapper, and `npm run build:wasm` to build the wasm artifact.
## Tests

206
src/api/js/examples/high-level/miracle-sudoku.ts Normal file
View file

@ -0,0 +1,206 @@
import { init } from '../../build/node';
import type { Solver, Arith } from '../../build/node';
// solve the "miracle sudoku"
// https://www.youtube.com/watch?v=yKf9aUIxdb4
// most of the interesting stuff is in `solve`
// the process is:
// - parse the board
// - create a Solver
// - create a Z3.Int variable for each square
// - for known cells, add a constraint which says the variable for that cell equals that value
// - add the usual uniqueness constraints
// - add the special "miracle sudoku" constraints
// - call `await solver.check()`
// - if the result is "sat", the board is solvable
// - call `solver.model()` to get a model, i.e. a concrete assignment of variables which satisfies the model
// - for each variable, call `model.evaluate(v)` to recover its value
function parseSudoku(str: string) {
// derive a list of { row, col, val } records, one for each specified position
// from a string like
// ....1..3.
// ..9..5..8
// 8.4..6.25
// ......6..
// ..8..4...
// 12..87...
// 3..9..2..
// .65..8...
// 9........
let cells = [];
let lines = str.trim().split('\n');
if (lines.length !== 9) {
throw new Error(`expected 9 lines, got ${lines.length}`);
}
for (let row = 0; row < 9; ++row) {
let line = lines[row].trim();
if (line.length !== 9) {
throw new Error(`expected line of length 9, got length ${line.length}`);
}
for (let col = 0; col < 9; ++col) {
let char = line[col];
if (char === '.') {
continue;
}
if (char < '1' || char > '9') {
throw new Error(`expected digit or '.', got ${char}`);
}
cells.push({ row, col, value: char.codePointAt(0)! - 48 /* '0' */ });
}
}
return cells;
}
(async () => {
let { Context, em } = await init();
// if you use 'main' as your context name, you won't need to name it in types like Solver
// if you're creating multiple contexts, give them different names
// then the type system will prevent you from mixing them
let Z3 = Context('main');
function addSudokuConstraints(solver: Solver, cells: Arith[][]) {
// the usual constraints:
// every square is between 1 and 9
for (let row of cells) {
for (let cell of row) {
solver.add(cell.ge(1));
solver.add(cell.le(9));
}
}
// values in each row are unique
for (let row of cells) {
solver.add(Z3.Distinct(...row));
}
// values in each column are unique
for (let col = 0; col < 9; ++col) {
solver.add(Z3.Distinct(...cells.map(row => row[col])));
}
// values in each 3x3 subdivision are unique
for (let suprow = 0; suprow < 3; ++suprow) {
for (let supcol = 0; supcol < 3; ++supcol) {
let square = [];
for (let row = 0; row < 3; ++row) {
for (let col = 0; col < 3; ++col) {
square.push(cells[suprow * 3 + row][supcol * 3 + col]);
}
}
solver.add(Z3.Distinct(...square));
}
}
}
function applyOffsets(x: number, y: number, offsets: [number, number][]) {
let out = [];
for (let offset of offsets) {
let rx = x + offset[0];
let ry = y + offset[1];
if (rx >= 0 && rx < 9 && ry >= 0 && ry < 8) {
out.push({ x: rx, y: ry });
}
}
return out;
}
function addMiracleConstraints(s: Solver, cells: Arith[][]) {
// the special "miracle sudoku" constraints
// any two cells separated by a knight's move or a kings move cannot contain the same digit
let knightOffets: [number, number][] = [
[1, -2],
[2, -1],
[2, 1],
[1, 2],
[-1, 2],
[-2, 1],
[-2, -1],
[-1, -2],
];
let kingOffsets: [number, number][] = [
[1, 1],
[1, -1],
[-1, 1],
[-1, -1],
]; // skipping immediately adjacent because those are covered by normal sudoku rules
let allOffets = [...knightOffets, ...kingOffsets];
for (let row = 0; row < 9; ++row) {
for (let col = 0; col < 9; ++col) {
for (let { x, y } of applyOffsets(row, col, allOffets)) {
s.add(cells[row][col].neq(cells[x][y]));
}
}
}
// any two orthogonally adjacent cells cannot contain consecutive digits
let orthoOffsets: [number, number][] = [
[0, 1],
[0, -1],
[1, 0],
[-1, 0],
];
for (let row = 0; row < 9; ++row) {
for (let col = 0; col < 9; ++col) {
for (let { x, y } of applyOffsets(row, col, orthoOffsets)) {
s.add(cells[row][col].sub(cells[x][y]).neq(1));
}
}
}
}
async function solve(str: string) {
let solver = new Z3.Solver();
let cells = Array.from({ length: 9 }, (_, col) => Array.from({ length: 9 }, (_, row) => Z3.Int.const(`c_${row}_${col}`)));
for (let { row, col, value } of parseSudoku(str)) {
solver.add(cells[row][col].eq(value));
}
addSudokuConstraints(solver, cells);
addMiracleConstraints(solver, cells); // remove this line to solve normal sudokus
let start = Date.now();
console.log('starting... this may take a minute or two');
let check = await solver.check();
console.log(`problem was determined to be ${check} in ${Date.now() - start} ms`);
if (check === 'sat') {
let model = solver.model();
let str = '';
for (let row = 0; row < 9; ++row) {
for (let col = 0; col < 9; ++col) {
str += model.eval(cells[row][col]).toString() + (col === 8 ? '' : ' ');
if (col === 2 || col === 5) {
str += ' ';
}
}
str += '\n';
if (row === 2 || row === 5) {
str += '\n';
}
}
console.log(str);
}
}
await solve(`
.........
.........
.........
.........
..1......
......2..
.........
.........
.........
`);
em.PThread.terminateAllThreads();
})().catch(e => {
console.error('error', e);
process.exit(1);
});

2
src/api/js/package-lock.json generated
View file

@ -27,7 +27,7 @@
"typescript": "^4.5.4"
},
"engines": {
"node": ">=16 <18"
"node": ">=16"
}
},
"node_modules/@ampproject/remapping": {

4
src/api/js/package.json
View file

@ -12,13 +12,13 @@
"homepage": "https://github.com/Z3Prover/z3/tree/master/src/api/js",
"repository": "github:Z3Prover/z3",
"engines": {
"node": ">=16 <18"
"node": ">=16"
},
"browser": "build/browser.js",
"main": "build/node.js",
"types": "build/node.d.ts",
"files": [
"build/*.{js,d.ts,wasm}"
"build/**/*.{js,d.ts,wasm}"
],
"scripts": {
"build:ts": "run-s -l build:ts:generate build:ts:tsc",

72
src/api/js/src/high-level/high-level.test.ts
View file

@ -1,7 +1,7 @@
import assert from 'assert';
import asyncToArray from 'iter-tools/methods/async-to-array';
import { init, killThreads } from '../jest';
import { Arith, Bool, Model, sat, unsat, Z3AssertionError, Z3HighLevel } from './types';
import { Arith, Bool, Model, Z3AssertionError, Z3HighLevel } from './types';
/**
* Generate all possible solutions from given assumptions.
@ -31,7 +31,7 @@ async function* allSolutions<Name extends string>(...assertions: Bool<Name>[]):
const solver = new assertions[0].ctx.Solver();
solver.add(...assertions);
while ((await solver.check()) === sat) {
while ((await solver.check()) === 'sat') {
const model = solver.model();
const decls = model.decls();
if (decls.length === 0) {
@ -59,13 +59,13 @@ async function prove(conjecture: Bool): Promise<void> {
const solver = new conjecture.ctx.Solver();
const { Not } = solver.ctx;
solver.add(Not(conjecture));
expect(await solver.check()).toStrictEqual(unsat);
expect(await solver.check()).toStrictEqual('unsat');
}
async function solve(conjecture: Bool): Promise<Model> {
const solver = new conjecture.ctx.Solver();
solver.add(conjecture);
expect(await solver.check()).toStrictEqual(sat);
expect(await solver.check()).toStrictEqual('sat');
return solver.model();
}
@ -96,7 +96,7 @@ describe('high-level', () => {
});
it('proves x = y implies g(x) = g(y)', async () => {
const { Solver, Int, Function, Implies, Not } = new api.Context('main');
const { Solver, Int, Function, Implies, Not } = api.Context('main');
const solver = new Solver();
const sort = Int.sort();
@ -106,11 +106,11 @@ describe('high-level', () => {
const conjecture = Implies(x.eq(y), g.call(x).eq(g.call(y)));
solver.add(Not(conjecture));
expect(await solver.check()).toStrictEqual(unsat);
expect(await solver.check()).toStrictEqual('unsat');
});
it('disproves x = y implies g(g(x)) = g(y)', async () => {
const { Solver, Int, Function, Implies, Not } = new api.Context('main');
const { Solver, Int, Function, Implies, Not } = api.Context('main');
const solver = new Solver();
const sort = Int.sort();
@ -119,14 +119,14 @@ describe('high-level', () => {
const g = Function.declare('g', sort, sort);
const conjecture = Implies(x.eq(y), g.call(g.call(x)).eq(g.call(y)));
solver.add(Not(conjecture));
expect(await solver.check()).toStrictEqual(sat);
expect(await solver.check()).toStrictEqual('sat');
});
it('checks that Context matches', () => {
const c1 = new api.Context('context');
const c2 = new api.Context('context');
const c3 = new api.Context('foo');
const c4 = new api.Context('bar');
const c1 = api.Context('context');
const c2 = api.Context('context');
const c3 = api.Context('foo');
const c4 = api.Context('bar');
// Contexts with the same name don't do type checking during compile time.
// We need to check for different context dynamically
@ -144,7 +144,7 @@ describe('high-level', () => {
describe('booleans', () => {
it("proves De Morgan's Law", async () => {
const { Bool, Not, And, Eq, Or } = new api.Context('main');
const { Bool, Not, And, Eq, Or } = api.Context('main');
const [x, y] = [Bool.const('x'), Bool.const('y')];
const conjecture = Eq(Not(And(x, y)), Or(Not(x), Not(y)));
@ -155,7 +155,7 @@ describe('high-level', () => {
describe('ints', () => {
it('finds a model', async () => {
const { Solver, Int, isIntVal } = new api.Context('main');
const { Solver, Int, isIntVal } = api.Context('main');
const solver = new Solver();
const x = Int.const('x');
const y = Int.const('y');
@ -163,10 +163,10 @@ describe('high-level', () => {
solver.add(x.ge(1)); // x >= 1
solver.add(y.lt(x.add(3))); // y < x + 3
expect(await solver.check()).toStrictEqual(sat);
expect(await solver.check()).toStrictEqual('sat');
const model = solver.model();
expect(model.length).toStrictEqual(2);
expect(model.length()).toStrictEqual(2);
for (const decl of model) {
expect(decl.arity()).toStrictEqual(0);
@ -175,8 +175,8 @@ describe('high-level', () => {
const yValueExpr = model.get(y);
assert(isIntVal(xValueExpr));
assert(isIntVal(yValueExpr));
const xValue = xValueExpr.value;
const yValue = yValueExpr.value;
const xValue = xValueExpr.value();
const yValue = yValueExpr.value();
assert(typeof xValue === 'bigint');
assert(typeof yValue === 'bigint');
expect(xValue).toBeGreaterThanOrEqual(1n);
@ -225,7 +225,7 @@ describe('high-level', () => {
541972386
`);
const { Solver, Int, Distinct, isIntVal } = new api.Context('main');
const { Solver, Int, Distinct, isIntVal } = api.Context('main');
const cells: Arith[][] = [];
// 9x9 matrix of integer variables
@ -284,7 +284,7 @@ describe('high-level', () => {
}
}
expect(await solver.check()).toStrictEqual(sat);
expect(await solver.check()).toStrictEqual('sat');
const model = solver.model();
const result = [];
@ -293,7 +293,7 @@ describe('high-level', () => {
for (let j = 0; j < 9; j++) {
const cell = model.eval(cells[i][j]);
assert(isIntVal(cell));
const value = cell.value;
const value = cell.value();
assert(typeof value === 'bigint');
expect(value).toBeGreaterThanOrEqual(0n);
expect(value).toBeLessThanOrEqual(9n);
@ -308,7 +308,7 @@ describe('high-level', () => {
describe('reals', () => {
it('can work with numerals', async () => {
const { Real, And } = new api.Context('main');
const { Real, And } = api.Context('main');
const n1 = Real.val('1/2');
const n2 = Real.val('0.5');
const n3 = Real.val(0.5);
@ -322,7 +322,7 @@ describe('high-level', () => {
it('can do non-linear arithmetic', async () => {
api.setParam('pp.decimal', true);
api.setParam('pp.decimal_precision', 20);
const { Real, Solver, isReal, isRealVal } = new api.Context('main');
const { Real, Solver, isReal, isRealVal } = api.Context('main');
const x = Real.const('x');
const y = Real.const('y');
const z = Real.const('z');
@ -331,7 +331,7 @@ describe('high-level', () => {
solver.add(x.mul(x).add(y.mul(y)).eq(1)); // x^2 + y^2 == 1
solver.add(x.mul(x).mul(x).add(z.mul(z).mul(z)).lt('1/2')); // x^3 + z^3 < 1/2
expect(await solver.check()).toStrictEqual(sat);
expect(await solver.check()).toStrictEqual('sat');
const model = solver.model();
expect(isRealVal(model.get(x))).toStrictEqual(true);
@ -344,7 +344,7 @@ describe('high-level', () => {
describe('bitvectors', () => {
it('can do simple proofs', async () => {
const { BitVec, Concat, Implies, isBitVecVal } = new api.Context('main');
const { BitVec, Concat, Implies, isBitVecVal } = api.Context('main');
const x = BitVec.const('x', 32);
@ -354,7 +354,7 @@ describe('high-level', () => {
assert(isBitVecVal(sSol) && isBitVecVal(uSol));
let v = sSol.asSignedValue();
expect(v - 10n <= 0n === v <= 10n).toStrictEqual(true);
v = uSol.value;
v = uSol.value();
expect(v - 10n <= 0n === v <= 10n).toStrictEqual(true);
const y = BitVec.const('y', 32);
@ -363,7 +363,7 @@ describe('high-level', () => {
});
it('finds x and y such that: x ^ y - 103 == x * y', async () => {
const { BitVec, isBitVecVal } = new api.Context('main');
const { BitVec, isBitVecVal } = api.Context('main');
const x = BitVec.const('x', 32);
const y = BitVec.const('y', 32);
@ -382,28 +382,28 @@ describe('high-level', () => {
describe('Solver', () => {
it('can use push and pop', async () => {
const { Solver, Int } = new api.Context('main');
const { Solver, Int } = api.Context('main');
const solver = new Solver();
const x = Int.const('x');
solver.add(x.gt(0));
expect(await solver.check()).toStrictEqual(sat);
expect(await solver.check()).toStrictEqual('sat');
solver.push();
solver.add(x.lt(0));
expect(solver.numScopes()).toStrictEqual(1);
expect(await solver.check()).toStrictEqual(unsat);
expect(await solver.check()).toStrictEqual('unsat');
solver.pop();
expect(solver.numScopes()).toStrictEqual(0);
expect(await solver.check()).toStrictEqual(sat);
expect(await solver.check()).toStrictEqual('sat');
});
it('can find multiple solutions', async () => {
const { Int, isIntVal } = new api.Context('main');
const { Int, isIntVal } = api.Context('main');
const x = Int.const('x');
@ -413,7 +413,7 @@ describe('high-level', () => {
.map(solution => {
const expr = solution.eval(x);
assert(isIntVal(expr));
return expr.value;
return expr.value();
})
.sort((a, b) => {
assert(a !== null && b !== null && typeof a === 'bigint' && typeof b === 'bigint');
@ -431,7 +431,7 @@ describe('high-level', () => {
describe('AstVector', () => {
it('can use basic methods', async () => {
const { Solver, AstVector, Int } = new api.Context('main');
const { Solver, AstVector, Int } = api.Context('main');
const solver = new Solver();
const vector = new AstVector<Arith>();
@ -439,12 +439,12 @@ describe('high-level', () => {
vector.push(Int.const(`int__${i}`));
}
const length = vector.length;
const length = vector.length();
for (let i = 0; i < length; i++) {
solver.add(vector.get(i).gt(1));
}
expect(await solver.check()).toStrictEqual(sat);
expect(await solver.check()).toStrictEqual('sat');
});
});
});

3193
src/api/js/src/high-level/high-level.ts
View file

File diff suppressed because it is too large Load diff

139
src/api/js/src/high-level/types.ts
View file

@ -16,13 +16,13 @@ import {
} from '../low-level';
/** @hidden */
export type AnySort<Name extends string = any> =
export type AnySort<Name extends string = 'main'> =
| Sort<Name>
| BoolSort<Name>
| ArithSort<Name>
| BitVecSort<number, Name>;
/** @hidden */
export type AnyExpr<Name extends string = any> =
export type AnyExpr<Name extends string = 'main'> =
| Expr<Name>
| Bool<Name>
| Arith<Name>
@ -31,10 +31,10 @@ export type AnyExpr<Name extends string = any> =
| BitVec<number, Name>
| BitVecNum<number, Name>;
/** @hidden */
export type AnyAst<Name extends string = any> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
export type AnyAst<Name extends string = 'main'> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
/** @hidden */
export type SortToExprMap<S extends AnySort<Name>, Name extends string = any> = S extends BoolSort
export type SortToExprMap<S extends AnySort<Name>, Name extends string = 'main'> = S extends BoolSort
? Bool<Name>
: S extends ArithSort<Name>
? Arith<Name>
@ -45,7 +45,7 @@ export type SortToExprMap<S extends AnySort<Name>, Name extends string = any> =
: never;
/** @hidden */
export type CoercibleToExprMap<S extends CoercibleToExpr<Name>, Name extends string = any> = S extends bigint
export type CoercibleToExprMap<S extends CoercibleToExpr<Name>, Name extends string = 'main'> = S extends bigint
? IntNum<Name>
: S extends number | CoercibleRational
? RatNum<Name>
@ -76,38 +76,20 @@ export type CoercibleToExprMap<S extends CoercibleToExpr<Name>, Name extends str
export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number };
/** @hidden */
export type CoercibleToExpr<Name extends string = any> = number | bigint | boolean | CoercibleRational | Expr<Name>;
export type CoercibleToExpr<Name extends string = 'main'> = number | bigint | boolean | CoercibleRational | Expr<Name>;
export class Z3Error extends Error {}
export class Z3AssertionError extends Z3Error {}
/**
* Returned by {@link Solver.check} when Z3 could find a solution
* @category Global
*/
export const sat = Symbol('Solver found a solution');
/**
* Returned by {@link Solver.check} when Z3 couldn't find a solution
* @category Global
*/
export const unsat = Symbol("Solver didn't find a solution");
/**
* Returned by {@link Solver.check} when Z3 couldn't reason about the assumptions
* @category Global
*/
export const unknown = Symbol("Solver couldn't reason about the assumptions");
/** @category Global */
export type CheckSatResult = typeof sat | typeof unsat | typeof unknown;
export type CheckSatResult = 'sat' | 'unsat' | 'unknown';
/** @hidden */
export interface ContextCtor {
new <Name extends string>(name: Name, options?: Record<string, any>): Context<Name>;
<Name extends string>(name: Name, options?: Record<string, any>): Context<Name>;
}
export interface Context<Name extends string = any> {
/** @hidden */
readonly __typename: 'Context';
export interface Context<Name extends string = 'main'> {
/** @hidden */
readonly ptr: Z3_context;
/**
@ -190,7 +172,7 @@ export interface Context<Name extends string = any> {
/** @category Functions */
isTactic(obj: unknown): obj is Tactic<Name>;
/** @category Functions */
isAstVector(obj: unknown): obj is AstVector<AnyAst<Name>, Name>;
isAstVector(obj: unknown): obj is AstVector<Name, AnyAst<Name>>;
/**
* Returns whether two Asts are the same thing
* @category Functions */
@ -202,9 +184,13 @@ export interface Context<Name extends string = any> {
* @category Functions */
from(primitive: boolean): Bool<Name>;
/**
* Coerce a number or rational into a Real expression
* Coerce a number to an Int or Real expression (integral numbers become Ints)
* @category Functions */
from(primitive: number | CoercibleRational): RatNum<Name>;
from(primitive: number): IntNum<Name> | RatNum<Name>;
/**
* Coerce a rational into a Real expression
* @category Functions */
from(primitive: CoercibleRational): RatNum<Name>;
/**
* Coerce a big number into a Integer expression
* @category Functions */
@ -232,7 +218,7 @@ export interface Context<Name extends string = any> {
*
* @see {@link Solver}
* @category Functions */
solve(...assertions: Bool[]): Promise<Model | typeof unsat | typeof unknown>;
solve(...assertions: Bool<Name>[]): Promise<Model<Name> | 'unsat' | 'unknown'>;
/////////////
// Classes //
@ -250,9 +236,9 @@ export interface Context<Name extends string = any> {
*/
readonly Model: new () => Model<Name>;
/** @category Classes */
readonly AstVector: new <Item extends Ast<Name> = AnyAst<Name>>() => AstVector<Item, Name>;
readonly AstVector: new <Item extends Ast<Name> = AnyAst<Name>>() => AstVector<Name, Item>;
/** @category Classes */
readonly AstMap: new <Key extends Ast = AnyAst, Value extends Ast = AnyAst>() => AstMap<Key, Value, Name>;
readonly AstMap: new <Key extends Ast<Name> = AnyAst<Name>, Value extends Ast<Name> = AnyAst<Name>>() => AstMap<Name, Key, Value>;
/** @category Classes */
readonly Tactic: new (name: string) => Tactic<Name>;
@ -309,7 +295,7 @@ export interface Context<Name extends string = any> {
/** @category Operations */
And(): Bool<Name>;
/** @category Operations */
And(vector: AstVector<Bool<Name>, Name>): Bool<Name>;
And(vector: AstVector<Name, Bool<Name>>): Bool<Name>;
/** @category Operations */
And(...args: (Bool<Name> | boolean)[]): Bool<Name>;
/** @category Operations */
@ -317,7 +303,7 @@ export interface Context<Name extends string = any> {
/** @category Operations */
Or(): Bool<Name>;
/** @category Operations */
Or(vector: AstVector<Bool<Name>, Name>): Bool<Name>;
Or(vector: AstVector<Name, Bool<Name>>): Bool<Name>;
/** @category Operations */
Or(...args: (Bool<Name> | boolean)[]): Bool<Name>;
/** @category Operations */
@ -368,9 +354,11 @@ export interface Context<Name extends string = any> {
Int2BV<Bits extends number>(a: Arith<Name> | bigint | number, bits: Bits): BitVec<Bits, Name>;
/** @category Operations */
Concat(...bitvecs: BitVec<number, Name>[]): BitVec<number, Name>;
/** @category Operations */
Cond(probe: Probe<Name>, onTrue: Tactic<Name>, onFalse: Tactic<Name>): Tactic<Name>
}
export interface Ast<Name extends string = any, Ptr = unknown> {
export interface Ast<Name extends string = 'main', Ptr = unknown> {
/** @hidden */
readonly __typename: 'Ast' | Sort['__typename'] | FuncDecl['__typename'] | Expr['__typename'];
@ -380,7 +368,7 @@ export interface Ast<Name extends string = any, Ptr = unknown> {
/** @virtual */
get ast(): Z3_ast;
/** @virtual */
get id(): number;
id(): number;
eqIdentity(other: Ast<Name>): boolean;
neqIdentity(other: Ast<Name>): boolean;
@ -392,7 +380,7 @@ export interface Ast<Name extends string = any, Ptr = unknown> {
export interface SolverCtor<Name extends string> {
new (): Solver<Name>;
}
export interface Solver<Name extends string = any> {
export interface Solver<Name extends string = 'main'> {
/** @hidden */
readonly __typename: 'Solver';
@ -407,10 +395,10 @@ export interface Solver<Name extends string = any> {
pop(num?: number): void;
numScopes(): number;
reset(): void;
add(...exprs: (Bool<Name> | AstVector<Bool<Name>, Name>)[]): void;
add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): void;
addAndTrack(expr: Bool<Name>, constant: Bool<Name> | string): void;
assertions(): AstVector<Bool<Name>, Name>;
check(...exprs: (Bool<Name> | AstVector<Bool<Name>, Name>)[]): Promise<CheckSatResult>;
assertions(): AstVector<Name, Bool<Name>>;
check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;
model(): Model<Name>;
}
@ -418,14 +406,14 @@ export interface Solver<Name extends string = any> {
export interface ModelCtor<Name extends string> {
new (): Model<Name>;
}
export interface Model<Name extends string = any> extends Iterable<FuncDecl<Name>> {
export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<Name>> {
/** @hidden */
readonly __typename: 'Model';
readonly ctx: Context<Name>;
readonly ptr: Z3_model;
get length(): number;
length(): number;
entries(): IterableIterator<[number, FuncDecl<Name>]>;
keys(): IterableIterator<number>;
@ -436,10 +424,10 @@ export interface Model<Name extends string = any> extends Iterable<FuncDecl<Name
eval(expr: Arith<Name>, modelCompletion?: boolean): Arith<Name>;
eval(expr: Expr<Name>, modelCompletion?: boolean): Expr<Name>;
get(i: number): FuncDecl<Name>;
get(from: number, to: number): FuncDecl[];
get(from: number, to: number): FuncDecl<Name>[];
get(declaration: FuncDecl<Name>): FuncInterp<Name> | Expr<Name>;
get(constant: Expr<Name>): Expr<Name>;
get(sort: Sort<Name>): AstVector<AnyExpr<Name>, Name>;
get(sort: Sort<Name>): AstVector<Name, AnyExpr<Name>>;
}
/**
@ -461,7 +449,7 @@ export interface Model<Name extends string = any> extends Iterable<FuncDecl<Name
export interface SortCreation<Name extends string> {
declare(name: string): Sort<Name>;
}
export interface Sort<Name extends string = any> extends Ast<Name, Z3_sort> {
export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {
/** @hidden */
readonly __typename: 'Sort' | BoolSort['__typename'] | ArithSort['__typename'] | BitVecSort['__typename'];
@ -476,7 +464,7 @@ export interface Sort<Name extends string = any> extends Ast<Name, Z3_sort> {
/**
* @category Functions
*/
export interface FuncInterp<Name extends string = any> {
export interface FuncInterp<Name extends string = 'main'> {
/** @hidden */
readonly __typename: 'FuncInterp';
@ -516,7 +504,7 @@ export interface RecFuncCreation<Name extends string> {
/**
* @category Functions
*/
export interface FuncDecl<Name extends string = any> extends Ast<Name, Z3_func_decl> {
export interface FuncDecl<Name extends string = 'main'> extends Ast<Name, Z3_func_decl> {
/** @hidden */
readonly __typename: 'FuncDecl';
@ -529,7 +517,7 @@ export interface FuncDecl<Name extends string = any> extends Ast<Name, Z3_func_d
call(...args: CoercibleToExpr<Name>[]): AnyExpr<Name>;
}
export interface Expr<Name extends string = any, S extends Sort<Name> = AnySort<Name>, Ptr = unknown>
export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySort<Name>, Ptr = unknown>
extends Ast<Name, Ptr> {
/** @hidden */
readonly __typename: 'Expr' | Bool['__typename'] | Arith['__typename'] | BitVec['__typename'];
@ -546,7 +534,7 @@ export interface Expr<Name extends string = any, S extends Sort<Name> = AnySort<
}
/** @category Booleans */
export interface BoolSort<Name extends string = any> extends Sort<Name> {
export interface BoolSort<Name extends string = 'main'> extends Sort<Name> {
/** @hidden */
readonly __typename: 'BoolSort';
@ -554,7 +542,7 @@ export interface BoolSort<Name extends string = any> extends Sort<Name> {
cast(expr: CoercibleToExpr<Name>): never;
}
/** @category Booleans */
export interface BoolCreation<Name extends string = any> {
export interface BoolCreation<Name extends string = 'main'> {
sort(): BoolSort<Name>;
const(name: string): Bool<Name>;
@ -565,7 +553,7 @@ export interface BoolCreation<Name extends string = any> {
val(value: boolean): Bool<Name>;
}
/** @category Booleans */
export interface Bool<Name extends string = any> extends Expr<Name, BoolSort<Name>, Z3_ast> {
export interface Bool<Name extends string = 'main'> extends Expr<Name, BoolSort<Name>, Z3_ast> {
/** @hidden */
readonly __typename: 'Bool';
@ -579,7 +567,7 @@ export interface Bool<Name extends string = any> extends Expr<Name, BoolSort<Nam
* A Sort that represents Integers or Real numbers
* @category Arithmetic
*/
export interface ArithSort<Name extends string = any> extends Sort<Name> {
export interface ArithSort<Name extends string = 'main'> extends Sort<Name> {
/** @hidden */
readonly __typename: 'ArithSort';
@ -615,7 +603,7 @@ export interface RealCreation<Name extends string> {
* Represents Integer or Real number expression
* @category Arithmetic
*/
export interface Arith<Name extends string = any> extends Expr<Name, ArithSort<Name>, Z3_ast> {
export interface Arith<Name extends string = 'main'> extends Expr<Name, ArithSort<Name>, Z3_ast> {
/** @hidden */
readonly __typename: 'Arith' | IntNum['__typename'] | RatNum['__typename'];
@ -683,11 +671,11 @@ export interface Arith<Name extends string = any> extends Expr<Name, ArithSort<N
* A constant Integer value expression
* @category Arithmetic
*/
export interface IntNum<Name extends string = any> extends Arith<Name> {
export interface IntNum<Name extends string = 'main'> extends Arith<Name> {
/** @hidden */
readonly __typename: 'IntNum';
get value(): bigint;
value(): bigint;
asString(): string;
asBinary(): string;
}
@ -707,11 +695,11 @@ export interface IntNum<Name extends string = any> extends Arith<Name> {
* ```
* @category Arithmetic
*/
export interface RatNum<Name extends string = any> extends Arith<Name> {
export interface RatNum<Name extends string = 'main'> extends Arith<Name> {
/** @hidden */
readonly __typename: 'RatNum';
get value(): { numerator: bigint; denominator: bigint };
value(): { numerator: bigint; denominator: bigint };
numerator(): IntNum<Name>;
denominator(): IntNum<Name>;
asNumber(): number;
@ -725,7 +713,7 @@ export interface RatNum<Name extends string = any> extends Arith<Name> {
* @typeParam Bits - A number representing amount of bits for this sort
* @category Bit Vectors
*/
export interface BitVecSort<Bits extends number = number, Name extends string = any> extends Sort<Name> {
export interface BitVecSort<Bits extends number = number, Name extends string = 'main'> extends Sort<Name> {
/** @hidden */
readonly __typename: 'BitVecSort';
@ -739,14 +727,14 @@ export interface BitVecSort<Bits extends number = number, Name extends string =
* // 32
* ```
*/
get size(): Bits;
size(): Bits;
cast(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
cast(other: CoercibleToExpr<Name>): Expr<Name>;
}
/** @hidden */
export type CoercibleToBitVec<Bits extends number = number, Name extends string = any> =
export type CoercibleToBitVec<Bits extends number = number, Name extends string = 'main'> =
| bigint
| number
| BitVec<Bits, Name>;
@ -769,7 +757,7 @@ export interface BitVecCreation<Name extends string> {
* Represents Bit Vector expression
* @category Bit Vectors
*/
export interface BitVec<Bits extends number = number, Name extends string = any>
export interface BitVec<Bits extends number = number, Name extends string = 'main'>
extends Expr<Name, BitVecSort<Bits, Name>, Z3_ast> {
/** @hidden */
readonly __typename: 'BitVec' | BitVecNum['__typename'];
@ -790,7 +778,7 @@ export interface BitVec<Bits extends number = number, Name extends string = any>
* // 8
* ```
*/
get size(): Bits;
size(): Bits;
/** @category Arithmetic */
add(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
@ -959,17 +947,17 @@ export interface BitVec<Bits extends number = number, Name extends string = any>
* Represents Bit Vector constant value
* @category Bit Vectors
*/
export interface BitVecNum<Bits extends number = number, Name extends string = any> extends BitVec<Bits, Name> {
export interface BitVecNum<Bits extends number = number, Name extends string = 'main'> extends BitVec<Bits, Name> {
/** @hidden */
readonly __typename: 'BitVecNum';
get value(): bigint;
value(): bigint;
asSignedValue(): bigint;
asString(): string;
asBinaryString(): string;
}
export interface Probe<Name extends string = any> {
export interface Probe<Name extends string = 'main'> {
/** @hidden */
readonly __typename: 'Probe';
@ -981,7 +969,7 @@ export interface Probe<Name extends string = any> {
export interface TacticCtor<Name extends string> {
new (name: string): Tactic<Name>;
}
export interface Tactic<Name extends string = any> {
export interface Tactic<Name extends string = 'main'> {
/** @hidden */
readonly __typename: 'Tactic';
@ -991,7 +979,7 @@ export interface Tactic<Name extends string = any> {
/** @hidden */
export interface AstVectorCtor<Name extends string> {
new <Item extends Ast<Name> = AnyAst<Name>>(): AstVector<Item, Name>;
new <Item extends Ast<Name> = AnyAst<Name>>(): AstVector<Name, Item>;
}
/**
* Stores multiple {@link Ast} objects
@ -1009,13 +997,13 @@ export interface AstVectorCtor<Name extends string> {
* // [2, x]
* ```
*/
export interface AstVector<Item extends Ast<Name> = AnyAst, Name extends string = any> extends Iterable<Item> {
export interface AstVector<Name extends string = 'main', Item extends Ast<Name> = AnyAst<Name>> extends Iterable<Item> {
/** @hidden */
readonly __typename: 'AstVector';
readonly ctx: Context<Name>;
readonly ptr: Z3_ast_vector;
get length(): number;
length(): number;
entries(): IterableIterator<[number, Item]>;
keys(): IterableIterator<number>;
@ -1031,7 +1019,7 @@ export interface AstVector<Item extends Ast<Name> = AnyAst, Name extends string
/** @hidden */
export interface AstMapCtor<Name extends string> {
new <Key extends Ast = AnyAst, Value extends Ast = AnyAst>(): AstMap<Key, Value, Name>;
new <Key extends Ast<Name> = AnyAst<Name>, Value extends Ast<Name> = AnyAst<Name>>(): AstMap<Name, Key, Value>;
}
/**
* Stores a mapping between different {@link Ast} objects
@ -1054,7 +1042,7 @@ export interface AstMapCtor<Name extends string> {
* // 0
* ```
*/
export interface AstMap<Key extends Ast<Name> = AnyAst, Value extends Ast = AnyAst, Name extends string = any>
export interface AstMap<Name extends string = 'main', Key extends Ast<Name> = AnyAst<Name>, Value extends Ast<Name> = AnyAst<Name>>
extends Iterable<[Key, Value]> {
/** @hidden */
readonly __typename: 'AstMap';
@ -1064,7 +1052,7 @@ export interface AstMap<Key extends Ast<Name> = AnyAst, Value extends Ast = AnyA
get size(): number;
entries(): IterableIterator<[Key, Value]>;
keys(): AstVector<Key, Name>;
keys(): AstVector<Name, Key>;
values(): IterableIterator<Value>;
get(key: Key): Value | undefined;
set(key: Key, value: Value): void;
@ -1119,11 +1107,6 @@ export interface Z3HighLevel {
*/
getParam(name: string): string | null;
/**
* Returns whether the given object is a {@link Context}
*/
isContext(obj: unknown): obj is Context;
/**
* Use this to create new contexts
* @see {@link Context}

24
src/api/js/src/high-level/utils.test.ts
View file

@ -1,5 +1,5 @@
import { Z3AssertionError } from './types';
import { allSatisfy, assert, assertExhaustive, autoBind } from './utils';
import { allSatisfy, assert, assertExhaustive } from './utils';
describe('allSatisfy', () => {
it('returns null on empty array', () => {
@ -56,28 +56,6 @@ describe('assertExhaustive', () => {
});
});
describe('autoBind', () => {
class Binded {
readonly name = 'Richard';
constructor(shouldBind: boolean) {
if (shouldBind === true) {
autoBind(this);
}
}
test(): string {
return `Hello ${this.name}`;
}
}
it('binds this', () => {
const { test: withoutBind } = new Binded(false);
const { test: withBind } = new Binded(true);
expect(() => withoutBind()).toThrowError(TypeError);
expect(withBind()).toStrictEqual('Hello Richard');
});
});
describe('assert', () => {
it('throws on failure', () => {
expect(() => assert(false)).toThrowError(Z3AssertionError);

26
src/api/js/src/high-level/utils.ts
View file

@ -10,32 +10,6 @@ function getAllProperties(obj: Record<string, any>) {
return properties;
}
// https://github.com/sindresorhus/auto-bind
// We modify it to use CommonJS instead of ESM
/*
MIT License
Copyright (c) Sindre Sorhus <sindresorhus@gmail.com> (https://sindresorhus.com)
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
export function autoBind<Self extends Record<string | symbol, any>>(self: Self): Self {
for (const [obj, key] of getAllProperties(self.constructor.prototype)) {
if (key === 'constructor') {
continue;
}
const descriptor = Reflect.getOwnPropertyDescriptor(obj, key);
if (descriptor && typeof descriptor.value === 'function') {
(self[key] as any) = self[key].bind(self);
}
}
return self;
}
/**
* Use to ensure that switches are checked to be exhaustive at compile time
*

1
src/api/ml/z3.ml
View file

@ -59,6 +59,7 @@ let mk_context (settings:(string * string) list) =
Z3native.del_config cfg;
Z3native.set_ast_print_mode res (Z3enums.int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT);
Z3native.set_internal_error_handler res;
Z3native.enable_concurrent_dec_ref res;
res
module Symbol =

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

@ -49,6 +49,13 @@ type context
val mk_context : (string * string) list -> context
(** Interaction logging for Z3
Interaction logs are used to record calls into the API into a text file.
The text file can be replayed using z3. It has to be the same version of z3
to ensure that low level codes emitted in a log are compatible with the
version of z3 replaying the log. The file suffix ".log" is understood
by z3 as the format of the file being an interaction log. You can use the
optional comman-line parameter "-log" to force z3 to treat an input file
as an interaction log.
Note that this is a global, static log and if multiple Context
objects are created, it logs the interaction with all of them. *)
module Log :
@ -927,10 +934,10 @@ end
module FiniteDomain :
sig
(** Create a new finite domain sort. *)
val mk_sort : context -> Symbol.symbol -> int -> Sort.sort
val mk_sort : context -> Symbol.symbol -> int64 -> Sort.sort
(** Create a new finite domain sort. *)
val mk_sort_s : context -> string -> int -> Sort.sort
val mk_sort_s : context -> string -> int64 -> Sort.sort
(** Indicates whether the term is of an array sort. *)
val is_finite_domain : Expr.expr -> bool
@ -939,7 +946,7 @@ sig
val is_lt : Expr.expr -> bool
(** The size of the finite domain sort. *)
val get_size : Sort.sort -> int
val get_size : Sort.sort -> int64
end
@ -2078,7 +2085,7 @@ sig
val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr
(** Create a numeral of FloatingPoint sort from a sign bit and two integers. *)
val mk_numeral_i_u : context -> bool -> int -> int -> Sort.sort -> Expr.expr
val mk_numeral_i_u : context -> bool -> int64 -> int64 -> Sort.sort -> Expr.expr
(** Create a numeral of FloatingPoint sort from a string *)
val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr
@ -2303,7 +2310,7 @@ sig
val get_numeral_exponent_string : context -> Expr.expr -> bool -> string
(** Return the exponent value of a floating-point numeral as a signed integer *)
val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int
val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int64
(** Return the exponent of a floating-point numeral as a bit-vector expression.
Remark: NaN's do not have a bit-vector exponent, so they are invalid arguments. *)
@ -2320,7 +2327,7 @@ sig
Remark: This function extracts the significand bits, without the
hidden bit or normalization. Throws an exception if the
significand does not fit into an int. *)
val get_numeral_significand_uint : context -> Expr.expr -> bool * int
val get_numeral_significand_uint : context -> Expr.expr -> bool * int64
(** Indicates whether a floating-point numeral is a NaN. *)
val is_numeral_nan : context -> Expr.expr -> bool

1
src/api/ml/z3native.ml.pre
View file

@ -21,6 +21,7 @@ and solver_callback = ptr
and goal = ptr
and tactic = ptr
and params = ptr
and parser_context = ptr
and probe = ptr
and stats = ptr
and ast_vector = ptr

1
src/api/ml/z3native_stubs.c.pre
View file

@ -418,6 +418,7 @@ MK_PLUS_OBJ_NO_REF(constructor_list, 16)
MK_PLUS_OBJ_NO_REF(rcf_num, 16)
MK_PLUS_OBJ(params, 64)
MK_PLUS_OBJ(param_descrs, 64)
MK_PLUS_OBJ(parser_context, 64)
MK_PLUS_OBJ(model, 64)
MK_PLUS_OBJ(func_interp, 32)
MK_PLUS_OBJ(func_entry, 32)

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

@ -9192,6 +9192,25 @@ def _dict2darray(decls, ctx):
i = i + 1
return sz, _names, _decls
class ParserContext:
def __init__(self, ctx= None):
self.ctx = _get_ctx(ctx)
self.pctx = Z3_mk_parser_context(self.ctx.ref())
Z3_parser_context_inc_ref(self.ctx.ref(), self.pctx)
def __del__(self):
if self.ctx.ref() is not None and self.pctx is not None and Z3_parser_context_dec_ref is not None:
Z3_parser_context_dec_ref(self.ctx.ref(), self.pctx)
self.pctx = None
def add_sort(self, sort):
Z3_parser_context_add_sort(self.ctx.ref(), self.pctx, sort.as_ast())
def add_decl(self, decl):
Z3_parser_context_add_decl(self.ctx.ref(), self.pctx, decl.as_ast())
def from_string(self, s):
return AstVector(Z3_parser_context_from_string(self.ctx.ref(), self.pctx, s), self.ctx)
def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
"""Parse a string in SMT 2.0 format using the given sorts and decls.

7
src/api/python/z3/z3types.py
View file

@ -216,6 +216,13 @@ class ParamDescrs(ctypes.c_void_p):
def from_param(obj):
return obj
class ParserContextObj(ctypes.c_void_p):
def __init__(self, pc):
self._as_parameter_ = pc
def from_param(obj):
return obj
class FuncInterpObj(ctypes.c_void_p):
def __init__(self, f):

66
src/api/z3_api.h
View file

@ -20,6 +20,7 @@ DEFINE_TYPE(Z3_constructor);
DEFINE_TYPE(Z3_constructor_list);
DEFINE_TYPE(Z3_params);
DEFINE_TYPE(Z3_param_descrs);
DEFINE_TYPE(Z3_parser_context);
DEFINE_TYPE(Z3_goal);
DEFINE_TYPE(Z3_tactic);
DEFINE_TYPE(Z3_probe);
@ -58,6 +59,7 @@ DEFINE_TYPE(Z3_rcf_num);
- \c Z3_constructor_list: list of constructors for a (recursive) datatype.
- \c Z3_params: parameter set used to configure many components such as: simplifiers, tactics, solvers, etc.
- \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.
- \c Z3_parser_context: context for incrementally parsing strings. Declarations can be added incrementally to the parser state.
- \c Z3_model: model for the constraints asserted into the logical context.
- \c Z3_func_interp: interpretation of a function in a model.
- \c Z3_func_entry: representation of the value of a \c Z3_func_interp at a particular point.
@ -1413,6 +1415,7 @@ typedef enum
def_Type('CONSTRUCTOR_LIST', 'Z3_constructor_list', 'ConstructorList')
def_Type('SOLVER', 'Z3_solver', 'SolverObj')
def_Type('SOLVER_CALLBACK', 'Z3_solver_callback', 'SolverCallbackObj')
def_Type('PARSER_CONTEXT', 'Z3_parser_context', 'ParserContextObj')
def_Type('GOAL', 'Z3_goal', 'GoalObj')
def_Type('TACTIC', 'Z3_tactic', 'TacticObj')
def_Type('PARAMS', 'Z3_params', 'Params')
@ -1702,6 +1705,16 @@ extern "C" {
void Z3_API Z3_interrupt(Z3_context c);
/**
\brief use concurrency control for dec-ref.
Reference counting decrements are allowed in separate threads from the context.
If this setting is not invoked, reference counting decrements are not going to be thread safe.
def_API('Z3_enable_concurrent_dec_ref', VOID, (_in(CONTEXT),))
*/
void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c);
/**@}*/
/** @name Parameters */
@ -5827,6 +5840,55 @@ extern "C" {
Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str);
/**
\brief Create a parser context.
A parser context maintains state between calls to \c Z3_parser_context_parse_string
where the caller can pass in a set of SMTLIB2 commands.
It maintains all the declarations from previous calls together with
of sorts and function declarations (including 0-ary) that are added directly to the context.
def_API('Z3_mk_parser_context', PARSER_CONTEXT, (_in(CONTEXT),))
*/
Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c);
/**
\brief Increment the reference counter of the given \c Z3_parser_context object.
def_API('Z3_parser_context_inc_ref', VOID, (_in(CONTEXT), _in(PARSER_CONTEXT)))
*/
void Z3_API Z3_parser_context_inc_ref(Z3_context c, Z3_parser_context pc);
/**
\brief Decrement the reference counter of the given \c Z3_parser_context object.
def_API('Z3_parser_context_dec_ref', VOID, (_in(CONTEXT), _in(PARSER_CONTEXT)))
*/
void Z3_API Z3_parser_context_dec_ref(Z3_context c, Z3_parser_context pc);
/**
\brief Add a sort declaration.
def_API('Z3_parser_context_add_sort', VOID, (_in(CONTEXT), _in(PARSER_CONTEXT), _in(SORT)))
*/
void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s);
/**
\brief Add a function declaration.
def_API('Z3_parser_context_add_decl', VOID, (_in(CONTEXT), _in(PARSER_CONTEXT), _in(FUNC_DECL)))
*/
void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f);
/**
\brief Parse a string of SMTLIB2 commands. Return assertions.
def_API('Z3_parser_context_from_string', AST_VECTOR, (_in(CONTEXT), _in(PARSER_CONTEXT), _in(STRING)))
*/
Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string s);
/**@}*/
/** @name Error Handling */
@ -6811,7 +6873,7 @@ extern "C" {
/**
\brief register a callback when a new expression with a registered function is used by the solver
The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare.
The registered function appears at the top level and is created using \ref Z3_solver_propagate_declare.
def_API('Z3_solver_propagate_created', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_created_eh)))
*/
@ -6837,7 +6899,7 @@ extern "C" {
/**
Create uninterpreted function declaration for the user propagator.
When expressions using the function are created by the solver invoke a callback
to \ref \Z3_solver_progate_created with arguments
to \ref \Z3_solver_propagate_created with arguments
1. context and callback solve
2. declared_expr: expression using function that was used as the top-level symbol
3. declared_id: a unique identifier (unique within the current scope) to track the expression.

43
src/ast/ast.cpp
View file

@ -471,26 +471,31 @@ bool compare_nodes(ast const * n1, ast const * n2) {
return
to_var(n1)->get_idx() == to_var(n2)->get_idx() &&
to_var(n1)->get_sort() == to_var(n2)->get_sort();
case AST_QUANTIFIER:
case AST_QUANTIFIER: {
quantifier const* q1 = to_quantifier(n1);
quantifier const* q2 = to_quantifier(n2);
return
to_quantifier(n1)->get_kind() == to_quantifier(n2)->get_kind() &&
to_quantifier(n1)->get_num_decls() == to_quantifier(n2)->get_num_decls() &&
compare_arrays(to_quantifier(n1)->get_decl_sorts(),
to_quantifier(n2)->get_decl_sorts(),
to_quantifier(n1)->get_num_decls()) &&
compare_arrays(to_quantifier(n1)->get_decl_names(),
to_quantifier(n2)->get_decl_names(),
to_quantifier(n1)->get_num_decls()) &&
to_quantifier(n1)->get_expr() == to_quantifier(n2)->get_expr() &&
to_quantifier(n1)->get_weight() == to_quantifier(n2)->get_weight() &&
to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() &&
compare_arrays(to_quantifier(n1)->get_patterns(),
to_quantifier(n2)->get_patterns(),
to_quantifier(n1)->get_num_patterns()) &&
to_quantifier(n1)->get_num_no_patterns() == to_quantifier(n2)->get_num_no_patterns() &&
compare_arrays(to_quantifier(n1)->get_no_patterns(),
to_quantifier(n2)->get_no_patterns(),
to_quantifier(n1)->get_num_no_patterns());
q1->get_kind() == q2->get_kind() &&
q1->get_num_decls() == q2->get_num_decls() &&
compare_arrays(q1->get_decl_sorts(),
q2->get_decl_sorts(),
q1->get_num_decls()) &&
compare_arrays(q1->get_decl_names(),
q2->get_decl_names(),
q1->get_num_decls()) &&
q1->get_expr() == q2->get_expr() &&
q1->get_weight() == q2->get_weight() &&
q1->get_num_patterns() == q2->get_num_patterns() &&
((q1->get_qid().is_numerical() && q2->get_qid().is_numerical()) ||
(q1->get_qid() == q2->get_qid())) &&
compare_arrays(q1->get_patterns(),
q2->get_patterns(),
q1->get_num_patterns()) &&
q1->get_num_no_patterns() == q2->get_num_no_patterns() &&
compare_arrays(q1->get_no_patterns(),
q2->get_no_patterns(),
q1->get_num_no_patterns());
}
default:
UNREACHABLE();
}

37
src/ast/recfun_decl_plugin.cpp
View file

@ -67,6 +67,30 @@ namespace recfun {
m_decl = m.mk_func_decl(s, arity, domain, range, info);
}
def* def::copy(util& dst, ast_translation& tr) {
SASSERT(&dst.m() == &tr.to());
sort_ref_vector domain(tr.to());
sort_ref range(tr(m_range.get()), tr.to());
for (auto* s : m_domain)
domain.push_back(tr(s));
family_id fid = dst.get_family_id();
bool is_generated = m_decl->get_parameter(0).get_int() != 0;
def* r = alloc(def, tr.to(), fid, m_name, domain.size(), domain.data(), range, is_generated);
r->m_rhs = tr(m_rhs.get());
for (auto* v : m_vars)
r->m_vars.push_back(tr(v));
for (auto const& c1 : m_cases) {
r->m_cases.push_back(case_def(tr.to()));
auto& c2 = r->m_cases.back();
c2.m_pred = tr(c1.m_pred.get());
c2.m_guards = tr(c1.m_guards);
c2.m_rhs = tr(c1.m_rhs.get());
c2.m_def = r;
c2.m_immediate = c1.m_immediate;
}
return r;
}
bool def::contains_def(util& u, expr * e) {
struct def_find_p : public i_expr_pred {
util& u;
@ -415,6 +439,19 @@ namespace recfun {
return promise_def(&u(), d);
}
void plugin::inherit(decl_plugin* other, ast_translation& tr) {
for (auto [k, v] : static_cast<plugin*>(other)->m_defs) {
func_decl_ref f(tr(k), tr.to());
if (m_defs.contains(f))
continue;
def* d = v->copy(u(), tr);
m_defs.insert(f, d);
for (case_def & c : d->get_cases())
m_case_defs.insert(c.get_decl(), &c);
}
}
promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) {
def* d = u().decl_fun(name, n, params, range, is_generated);
erase_def(d->get_decl());

11
src/ast/recfun_decl_plugin.h
View file

@ -21,6 +21,7 @@ Revision History:
#include "ast/ast.h"
#include "ast/ast_pp.h"
#include "ast/ast_translation.h"
#include "util/obj_hashtable.h"
namespace recfun {
@ -62,6 +63,12 @@ namespace recfun {
def * m_def; //<! definition this is a part of
bool m_immediate; //<! does `rhs` contain no defined_fun/case_pred?
case_def(ast_manager& m):
m_pred(m),
m_guards(m),
m_rhs(m)
{}
case_def(ast_manager & m,
family_id fid,
def * d,
@ -132,6 +139,8 @@ namespace recfun {
bool is_fun_macro() const { return m_cases.size() == 1; }
bool is_fun_defined() const { return !is_fun_macro(); }
def* copy(util& dst, ast_translation& tr);
};
// definition to be complete (missing RHS)
@ -205,6 +214,8 @@ namespace recfun {
expr_ref redirect_ite(replace& subst, unsigned n, var * const* vars, expr * e);
void inherit(decl_plugin* other, ast_translation& tr) override;
};
}

36
src/ast/rewriter/char_rewriter.cpp
View file

@ -37,21 +37,57 @@ br_status char_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
case OP_CHAR_CONST:
break;
case OP_CHAR_LE:
st = mk_char_le(args[0], args[1], result);
break;
case OP_CHAR_TO_INT:
st = mk_char_to_int(args[0], result);
break;
case OP_CHAR_TO_BV:
st = mk_char_to_bv(args[0], result);
break;
case OP_CHAR_FROM_BV:
st = mk_char_from_bv(args[0], result);
break;
case OP_CHAR_IS_DIGIT:
st = mk_char_is_digit(args[0], result);
break;
}
return st;
}
br_status char_rewriter::mk_char_is_digit(expr* a, expr_ref& result) {
unsigned n;
if (!m_char->is_const_char(a, n))
return BR_FAILED;
result = m.mk_bool_val('0' <= n && n <= '9');
return BR_DONE;
}
br_status char_rewriter::mk_char_to_bv(expr* a, expr_ref& result) {
return BR_FAILED;
}
br_status char_rewriter::mk_char_le(expr* a, expr* b, expr_ref& result) {
unsigned na = 0, nb = 0;
if (m_char->is_const_char(a, na)) {
if (na == 0) {
result = m.mk_true();
return BR_DONE;
}
}
if (m_char->is_const_char(b, nb)) {
if (na != 0) {
result = m.mk_bool_val(na <= nb);
return BR_DONE;
}
if (nb == m_char->max_char()) {
result = m.mk_true();
return BR_DONE;
}
}
return BR_FAILED;
}
br_status char_rewriter::mk_char_from_bv(expr* e, expr_ref& result) {
bv_util bv(m);
rational n;

6
src/ast/rewriter/char_rewriter.h
View file

@ -35,6 +35,12 @@ class char_rewriter {
br_status mk_char_to_int(expr* e, expr_ref& result);
br_status mk_char_le(expr* a, expr* b, expr_ref& result);
br_status mk_char_is_digit(expr* a, expr_ref& result);
br_status mk_char_to_bv(expr* a, expr_ref& result);
public:
char_rewriter(ast_manager& m);

2
src/ast/rewriter/th_rewriter.cpp
View file

@ -78,7 +78,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
void updt_local_params(params_ref const & _p) {
rewriter_params p(_p);
m_flat = p.flat();
m_flat = true;
m_max_memory = megabytes_to_bytes(p.max_memory());
m_max_steps = p.max_steps();
m_pull_cheap_ite = p.pull_cheap_ite();

23
src/ast/seq_decl_plugin.cpp
View file

@ -532,7 +532,12 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
case _OP_STRING_FROM_CHAR: {
if (!(num_parameters == 1 && parameters[0].is_int()))
m.raise_exception("character literal expects integer parameter");
zstring zs(parameters[0].get_int());
int i = parameters[0].get_int();
if (i < 0)
m.raise_exception("character literal expects a non-negative integer parameter");
if (i > (int)m_char_plugin->max_char())
m.raise_exception("character literal is out of bounds");
zstring zs(i);
parameter p(zs);
return m.mk_const_decl(m_stringc_sym, m_string,func_decl_info(m_family_id, OP_STRING_CONST, 1, &p));
}
@ -966,6 +971,22 @@ bool seq_util::str::is_len_sub(expr const* s, expr*& l, expr*& u, rational& k) c
return false;
}
bool seq_util::str::is_concat_of_units(expr* s) const {
ptr_vector<expr> todo;
todo.push_back(s);
while (!todo.empty()) {
expr* e = todo.back();
todo.pop_back();
if (is_empty(e) || is_unit(e))
continue;
if (is_concat(e))
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
else
return false;
}
return true;
}
bool seq_util::str::is_unit_string(expr const* s, expr_ref& c) const {
zstring z;
expr* ch = nullptr;

1
src/ast/seq_decl_plugin.h
View file

@ -375,6 +375,7 @@ public:
bool is_to_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_TO_CODE); }
bool is_len_sub(expr const* n, expr*& l, expr*& u, rational& k) const;
bool is_concat_of_units(expr* n) const;
/*
tests if s is a single character string(c) or a unit (c)

29
src/cmd_context/basic_cmds.cpp
View file

@ -219,9 +219,8 @@ ATOMIC_CMD(get_proof_graph_cmd, "get-proof-graph", "retrieve proof and print it
pr = ctx.get_check_sat_result()->get_proof();
if (pr == 0)
throw cmd_exception("proof is not available");
if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) {
if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr))
throw cmd_exception("proof is not well sorted");
}
context_params& params = ctx.params();
const std::string& file = params.m_dot_proof_file;
@ -235,11 +234,11 @@ static void print_core(cmd_context& ctx) {
ctx.regular_stream() << "(";
bool first = true;
for (expr* e : core) {
if (first)
first = false;
else
ctx.regular_stream() << " ";
ctx.regular_stream() << mk_ismt2_pp(e, ctx.m());
if (first)
first = false;
else
ctx.regular_stream() << " ";
ctx.regular_stream() << mk_ismt2_pp(e, ctx.m());
}
ctx.regular_stream() << ")" << std::endl;
}
@ -260,9 +259,8 @@ ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset
return;
if (!ctx.produce_unsat_assumptions())
throw cmd_exception("unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)");
if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) {
if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat)
throw cmd_exception("unsat assumptions is not available");
}
print_core(ctx);
});
@ -410,6 +408,15 @@ class set_option_cmd : public set_get_option_cmd {
}
}
static void check_no_assertions(cmd_context & ctx, symbol const & opt_name) {
if (ctx.has_assertions()) {
std::string msg = "error setting '";
msg += opt_name.str();
msg += "', option value cannot be modified after assertions have been added";
throw cmd_exception(std::move(msg));
}
}
void set_param(cmd_context & ctx, char const * value) {
try {
gparams::set(m_option, value);
@ -437,11 +444,11 @@ class set_option_cmd : public set_get_option_cmd {
ctx.set_interactive_mode(to_bool(value));
}
else if (m_option == m_produce_proofs) {
check_not_initialized(ctx, m_produce_proofs);
check_no_assertions(ctx, m_produce_proofs);
ctx.set_produce_proofs(to_bool(value));
}
else if (m_option == m_produce_unsat_cores) {
check_not_initialized(ctx, m_produce_unsat_cores);
check_no_assertions(ctx, m_produce_unsat_cores);
ctx.set_produce_unsat_cores(to_bool(value));
}
else if (m_option == m_produce_unsat_assumptions) {

60
src/cmd_context/cmd_context.cpp
View file

@ -538,22 +538,9 @@ public:
cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_main_ctx(main_ctx),
m_logic(l),
m_interactive_mode(false),
m_global_decls(false),
m_print_success(m_params.m_smtlib2_compliant),
m_random_seed(0),
m_produce_unsat_cores(false),
m_produce_unsat_assumptions(false),
m_produce_assignments(false),
m_status(UNKNOWN),
m_numeral_as_real(false),
m_ignore_check(false),
m_exit_on_error(false),
m_manager(m),
m_own_manager(m == nullptr),
m_manager_initialized(false),
m_pmanager(nullptr),
m_sexpr_manager(nullptr),
m_regular("stdout", std::cout),
m_diagnostic("stderr", std::cerr) {
SASSERT(m != 0 || !has_manager());
@ -607,6 +594,7 @@ void cmd_context::global_params_updated() {
m_params.updt_params();
if (m_params.m_smtlib2_compliant)
m_print_success = true;
set_produce_proofs(m_params.m_proof);
if (m_solver) {
params_ref p;
if (!m_params.m_auto_config)
@ -626,13 +614,14 @@ void cmd_context::set_produce_models(bool f) {
void cmd_context::set_produce_unsat_cores(bool f) {
// can only be set before initialization
SASSERT(!has_manager());
SASSERT(!has_assertions());
m_params.m_unsat_core |= f;
}
void cmd_context::set_produce_proofs(bool f) {
// can only be set before initialization
SASSERT(!has_manager());
SASSERT(!has_assertions() || m_params.m_proof == f);
if (has_manager())
m().toggle_proof_mode(f ? PGM_ENABLED : PGM_DISABLED);
m_params.m_proof = f;
}
@ -835,15 +824,16 @@ bool cmd_context::set_logic(symbol const & s) {
TRACE("cmd_context", tout << s << "\n";);
if (has_logic())
throw cmd_exception("the logic has already been set");
if (has_manager() && m_main_ctx)
if (has_assertions() && m_main_ctx)
throw cmd_exception("logic must be set before initialization");
if (!smt_logics::supported_logic(s)) {
if (!smt_logics::supported_logic(s))
return false;
}
m_logic = s;
if (smt_logics::logic_has_reals_only(s)) {
if (m_solver)
mk_solver();
if (smt_logics::logic_has_reals_only(s))
m_numeral_as_real = true;
}
return true;
}
@ -1837,6 +1827,10 @@ void cmd_context::add_declared_functions(model& mdl) {
}
void cmd_context::display_sat_result(lbool r) {
if (has_manager() && m().has_trace_stream()) {
m().trace_stream().flush();
}
switch (r) {
case l_true:
regular_stream() << "sat" << std::endl;
@ -2203,22 +2197,25 @@ expr_ref_vector cmd_context::tracked_assertions() {
for (unsigned i = 0; i < assertions().size(); ++i) {
expr* an = assertion_names()[i];
expr* asr = assertions()[i];
if (an) {
if (an)
result.push_back(m().mk_implies(an, asr));
}
else {
else
result.push_back(asr);
}
}
}
else {
for (expr * e : assertions()) {
for (expr * e : assertions())
result.push_back(e);
}
}
return result;
}
void cmd_context::reset_tracked_assertions() {
m_assertion_names.reset();
for (expr* a : m_assertions)
m().dec_ref(a);
m_assertions.reset();
}
void cmd_context::display_assertions() {
if (!m_interactive_mode)
@ -2254,9 +2251,8 @@ format_ns::format * cmd_context::pp(sort * s) const {
}
cmd_context::pp_env & cmd_context::get_pp_env() const {
if (m_pp_env.get() == nullptr) {
if (m_pp_env.get() == nullptr)
const_cast<cmd_context*>(this)->m_pp_env = alloc(pp_env, *const_cast<cmd_context*>(this));
}
return *(m_pp_env.get());
}
@ -2314,9 +2310,8 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr
out << "(set-logic " << logic << ")" << std::endl;
// collect uninterpreted function declarations
decl_collector decls(m());
for (unsigned i = 0; i < num; i++) {
for (unsigned i = 0; i < num; i++)
decls.visit(assertions[i]);
}
// TODO: display uninterpreted sort decls, and datatype decls.
@ -2342,9 +2337,8 @@ void cmd_context::slow_progress_sample() {
svector<symbol> labels;
m_solver->get_labels(labels);
regular_stream() << "(labels";
for (symbol const& s : labels) {
for (symbol const& s : labels)
regular_stream() << " " << s;
}
regular_stream() << "))" << std::endl;
}

32
src/cmd_context/cmd_context.h
View file

@ -194,21 +194,21 @@ public:
protected:
ast_context_params m_params;
ast_context_params m_params;
bool m_main_ctx;
symbol m_logic;
bool m_interactive_mode;
bool m_global_decls;
bool m_interactive_mode = false;
bool m_global_decls = false;
bool m_print_success;
unsigned m_random_seed;
bool m_produce_unsat_cores;
bool m_produce_unsat_assumptions;
bool m_produce_assignments;
status m_status;
bool m_numeral_as_real;
bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
bool m_exit_on_error;
bool m_allow_duplicate_declarations { false };
unsigned m_random_seed = 0;
bool m_produce_unsat_cores = false;
bool m_produce_unsat_assumptions = false;
bool m_produce_assignments = false;
status m_status = UNKNOWN;
bool m_numeral_as_real = false;
bool m_ignore_check = false; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
bool m_exit_on_error = false;
bool m_allow_duplicate_declarations = false;
static std::ostringstream g_error_stream;
@ -216,9 +216,9 @@ protected:
sref_vector<generic_model_converter> m_mcs;
ast_manager * m_manager;
bool m_own_manager;
bool m_manager_initialized;
pdecl_manager * m_pmanager;
sexpr_manager * m_sexpr_manager;
bool m_manager_initialized = false;
pdecl_manager * m_pmanager = nullptr;
sexpr_manager * m_sexpr_manager = nullptr;
check_logic m_check_logic;
stream_ref m_regular;
stream_ref m_diagnostic;
@ -362,6 +362,7 @@ public:
bool produce_unsat_cores() const;
bool well_sorted_check_enabled() const;
bool validate_model_enabled() const;
bool has_assertions() const { return !m_assertions.empty(); }
void set_produce_models(bool flag);
void set_produce_unsat_cores(bool flag);
void set_produce_proofs(bool flag);
@ -485,6 +486,7 @@ public:
ptr_vector<expr> const& assertions() const { return m_assertions; }
ptr_vector<expr> const& assertion_names() const { return m_assertion_names; }
expr_ref_vector tracked_assertions();
void reset_tracked_assertions();
/**
\brief Hack: consume assertions if there are no scopes.

82
src/math/dd/dd_pdd.cpp
View file

@ -1291,6 +1291,88 @@ namespace dd {
return *this;
}
/**
* \brief substitute variable v by r.
* This base line implementation is simplistic and does not use operator caching.
*/
pdd pdd::subst_pdd(unsigned v, pdd const& r) const {
if (is_val())
return *this;
if (m.m_var2level[var()] < m.m_var2level[v])
return *this;
pdd l = lo().subst_pdd(v, r);
pdd h = hi().subst_pdd(v, r);
if (var() == v)
return r*h + l;
else if (l == lo() && h == hi())
return *this;
else
return m.mk_var(var())*h + l;
}
std::pair<unsigned_vector, pdd> pdd::var_factors() const {
if (is_val())
return { unsigned_vector(), *this };
unsigned v = var();
if (lo().is_val()) {
if (!lo().is_zero())
return { unsigned_vector(), *this };
auto [vars, p] = hi().var_factors();
vars.push_back(v);
return {vars, p};
}
auto [lo_vars, q] = lo().var_factors();
if (lo_vars.empty())
return { unsigned_vector(), *this };
unsigned_vector lo_and_hi;
auto merge = [&](unsigned_vector& lo_vars, unsigned_vector& hi_vars) {
unsigned ir = 0, jr = 0;
for (unsigned i = 0, j = 0; i < lo_vars.size() || j < hi_vars.size(); ) {
if (i == lo_vars.size())
hi_vars[jr++] = hi_vars[j++];
else if (j == hi_vars.size())
lo_vars[ir++] = lo_vars[i++];
else if (lo_vars[i] == hi_vars[j]) {
lo_and_hi.push_back(lo_vars[i]);
++i;
++j;
}
else if (m.m_var2level[lo_vars[i]] > m.m_var2level[hi_vars[j]])
hi_vars[jr++] = hi_vars[j++];
else
lo_vars[ir++] = lo_vars[i++];
}
lo_vars.shrink(ir);
hi_vars.shrink(jr);
};
auto mul = [&](unsigned_vector const& vars, pdd p) {
for (auto v : vars)
p *= m.mk_var(v);
return p;
};
auto [hi_vars, p] = hi().var_factors();
if (lo_vars.back() == v) {
lo_vars.pop_back();
merge(lo_vars, hi_vars);
lo_and_hi.push_back(v);
return { lo_and_hi, mul(lo_vars, q) + mul(hi_vars, p) };
}
if (hi_vars.empty())
return { unsigned_vector(), *this };
merge(lo_vars, hi_vars);
hi_vars.push_back(v);
if (lo_and_hi.empty())
return { unsigned_vector(), *this };
else
return { lo_and_hi, mul(lo_vars, q) + mul(hi_vars, p) };
}
std::ostream& operator<<(std::ostream& out, pdd const& b) { return b.display(out); }
void pdd_iterator::next() {

17
src/math/dd/dd_pdd.h
View file

@ -364,9 +364,20 @@ namespace dd {
bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); }
void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) { m.factor(*this, v, degree, lc, rest); }
/**
* \brief factor out variables
*/
std::pair<unsigned_vector, pdd> var_factors() const;
pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val(*this, s); }
pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
/**
* \brief substitute variable v by r.
*/
pdd subst_pdd(unsigned v, pdd const& r) const;
std::ostream& display(std::ostream& out) const { return m.display(out, *this); }
bool operator==(pdd const& other) const { return root == other.root; }
bool operator!=(pdd const& other) const { return root != other.root; }
@ -398,13 +409,17 @@ namespace dd {
inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); }
inline pdd operator-(int x, pdd const& b) { return rational(x) - b; }
inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }
inline pdd operator-(pdd const& b, rational const& r) { return b + (-r); }
inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; }
inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; }
inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; }
inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; }
inline pdd& operator-=(pdd & p, pdd const& q) { p = p - q; return p; }
inline pdd& operator+=(pdd & p, pdd const& q) { p = p + q; return p; }
inline pdd& operator+=(pdd & p, rational const& v) { p = p + v; return p; }
inline pdd& operator-=(pdd & p, rational const& v) { p = p - v; return p; }
inline pdd& operator*=(pdd & p, rational const& v) { p = p * v; return p; }
std::ostream& operator<<(std::ostream& out, pdd const& b);

34
src/math/dd/pdd_interval.h
View file

@ -27,7 +27,33 @@ typedef dep_intervals::with_deps_t w_dep;
class pdd_interval {
dep_intervals& m_dep_intervals;
std::function<void (unsigned, bool, scoped_dep_interval&)> m_var2interval;
// retrieve intervals after distributing multiplication over addition.
template <w_dep wd>
void get_interval_distributed(pdd const& p, scoped_dep_interval& i, scoped_dep_interval& ret) {
bool deps = wd == w_dep::with_deps;
if (p.is_val()) {
if (deps)
m_dep_intervals.mul<dep_intervals::with_deps>(p.val(), i, ret);
else
m_dep_intervals.mul<dep_intervals::without_deps>(p.val(), i, ret);
return;
}
scoped_dep_interval hi(m()), lo(m()), t(m()), a(m());
get_interval_distributed<wd>(p.lo(), i, lo);
m_var2interval(p.var(), deps, a);
if (deps) {
m_dep_intervals.mul<dep_intervals::with_deps>(a, i, t);
get_interval_distributed<wd>(p.hi(), t, hi);
m_dep_intervals.add<dep_intervals::with_deps>(hi, lo, ret);
}
else {
m_dep_intervals.mul<dep_intervals::without_deps>(a, i, t);
get_interval_distributed<wd>(p.hi(), t, hi);
m_dep_intervals.add<dep_intervals::without_deps>(hi, lo, ret);
}
}
public:
pdd_interval(dep_intervals& d): m_dep_intervals(d) {}
@ -57,5 +83,11 @@ public:
}
}
template <w_dep wd>
void get_interval_distributed(pdd const& p, scoped_dep_interval& ret) {
scoped_dep_interval i(m());
m_dep_intervals.set_interval_for_scalar(i, rational::one());
get_interval_distributed<wd>(p, i, ret);
}
};
}

35
src/math/grobner/grobner.cpp
View file

@ -116,10 +116,13 @@ void grobner::reset() {
}
void grobner::display_var(std::ostream & out, expr * var) const {
out << "#" << var->get_id();
#if 0
if (is_app(var) && to_app(var)->get_num_args() > 0)
out << mk_bounded_pp(var, m_manager);
else
out << mk_pp(var, m_manager);
#endif
}
void grobner::display_vars(std::ostream & out, unsigned num_vars, expr * const * vars) const {
@ -129,7 +132,7 @@ void grobner::display_vars(std::ostream & out, unsigned num_vars, expr * const *
}
}
void grobner::display_monomial(std::ostream & out, monomial const & m) const {
void grobner::display_monomial(std::ostream & out, monomial const & m, std::function<void(std::ostream&, expr*)>& display_var) const {
if (!m.m_coeff.is_one() || m.m_vars.empty()) {
out << m.m_coeff;
if (!m.m_vars.empty())
@ -162,7 +165,7 @@ void grobner::display_monomial(std::ostream & out, monomial const & m) const {
}
}
void grobner::display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials) const {
void grobner::display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials, std::function<void(std::ostream&, expr*)>& display_var) const {
bool first = true;
for (unsigned i = 0; i < num_monomials; i++) {
monomial const * m = monomials[i];
@ -170,26 +173,26 @@ void grobner::display_monomials(std::ostream & out, unsigned num_monomials, mono
first = false;
else
out << " + ";
display_monomial(out, *m);
display_monomial(out, *m, display_var);
}
}
void grobner::display_equation(std::ostream & out, equation const & eq) const {
display_monomials(out, eq.m_monomials.size(), eq.m_monomials.data());
void grobner::display_equation(std::ostream & out, equation const & eq, std::function<void(std::ostream&, expr*)>& display_var) const {
display_monomials(out, eq.m_monomials.size(), eq.m_monomials.data(), display_var);
out << " = 0\n";
}
void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const {
if (!v.empty()) {
out << header << "\n";
for (equation const* eq : v)
display_equation(out, *eq);
}
void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header, std::function<void(std::ostream&, expr*)>& display_var) const {
if (v.empty())
return;
out << header << "\n";
for (equation const* eq : v)
display_equation(out, *eq, display_var);
}
void grobner::display(std::ostream & out) const {
display_equations(out, m_processed, "processed:");
display_equations(out, m_to_process, "to process:");
void grobner::display(std::ostream & out, std::function<void(std::ostream&, expr*)>& display_var) const {
display_equations(out, m_processed, "processed:", display_var);
display_equations(out, m_to_process, "to process:", display_var);
}
void grobner::set_weight(expr * n, int weight) {
@ -525,7 +528,7 @@ bool grobner::is_subset(monomial const * m1, monomial const * m2, ptr_vector<exp
for (; i2 < sz2; i2++)
rest.push_back(m2->m_vars[i2]);
TRACE("grobner",
tout << "monomail: "; display_monomial(tout, *m1); tout << " is a subset of ";
tout << "monomial: "; display_monomial(tout, *m1); tout << " is a subset of ";
display_monomial(tout, *m2); tout << "\n";
tout << "rest: "; display_vars(tout, rest.size(), rest.data()); tout << "\n";);
return true;
@ -549,7 +552,7 @@ bool grobner::is_subset(monomial const * m1, monomial const * m2, ptr_vector<exp
}
}
// is not subset
TRACE("grobner", tout << "monomail: "; display_monomial(tout, *m1); tout << " is not a subset of ";
TRACE("grobner", tout << "monomial: "; display_monomial(tout, *m1); tout << " is not a subset of ";
display_monomial(tout, *m2); tout << "\n";);
return false;
}

32
src/math/grobner/grobner.h
View file

@ -120,9 +120,16 @@ protected:
void display_var(std::ostream & out, expr * var) const;
void display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials) const;
void display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials, std::function<void(std::ostream&, expr*)>& display_var) const;
void display_equations(std::ostream & out, equation_set const & v, char const * header) const;
void display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials) const {
std::function<void(std::ostream& out, expr* v)> _fn = [&](std::ostream& out, expr* v) { display_var(out, v); };
display_monomials(out, num_monomials, monomials, _fn);
}
void display_equations(std::ostream & out, equation_set const & v, char const * header, std::function<void(std::ostream&, expr*)>& display_var) const;
void del_equations(unsigned old_size);
@ -281,11 +288,26 @@ public:
void pop_scope(unsigned num_scopes);
void display_equation(std::ostream & out, equation const & eq) const;
void display_equation(std::ostream & out, equation const & eq) const {
std::function<void(std::ostream& out, expr* v)> _fn = [&](std::ostream& out, expr* v) { display_var(out, v); };
display_equation(out, eq, _fn);
}
void display_monomial(std::ostream & out, monomial const & m) const;
void display_monomial(std::ostream & out, monomial const & m) const {
std::function<void(std::ostream& out, expr* v)> _fn = [&](std::ostream& out, expr* v) { display_var(out, v); };
display_monomial(out, m, _fn);
}
void display_equation(std::ostream & out, equation const & eq, std::function<void(std::ostream&, expr*)>& display_var) const;
void display(std::ostream & out) const;
void display_monomial(std::ostream & out, monomial const & m, std::function<void(std::ostream&, expr*)>& display_var) const;
void display(std::ostream & out) const {
std::function<void(std::ostream& out, expr* v)> _fn = [&](std::ostream& out, expr* v) { display_var(out, v); };
display(out, _fn);
}
void display(std::ostream & out, std::function<void(std::ostream&, expr*)>& display_var) const;
};

2
src/math/grobner/pdd_simplifier.cpp
View file

@ -223,6 +223,8 @@ namespace dd {
for (unsigned i = 0; i < s.m_to_simplify.size(); ++i) {
equation* e = s.m_to_simplify[i];
pdd p = e->poly();
if (p.is_val())
continue;
if (!p.hi().is_val()) {
continue;
}

86
src/math/grobner/pdd_solver.cpp
View file

@ -11,9 +11,9 @@
--*/
#include "util/uint_set.h"
#include "math/grobner/pdd_solver.h"
#include "math/grobner/pdd_simplifier.h"
#include "util/uint_set.h"
#include <math.h>
@ -169,7 +169,7 @@ namespace dd {
/*
Use the given equation to simplify equations in set
*/
void solver::simplify_using(equation_vector& set, equation const& eq) {
void solver::simplify_using(equation_vector& set, std::function<bool(equation&, bool&)>& simplifier) {
struct scoped_update {
equation_vector& set;
unsigned i, j, sz;
@ -191,7 +191,7 @@ namespace dd {
equation& target = *set[sr.i];
bool changed_leading_term = false;
bool simplified = true;
simplified = !done() && try_simplify_using(target, eq, changed_leading_term);
simplified = !done() && simplifier(target, changed_leading_term);
if (simplified && is_trivial(target)) {
retire(&target);
@ -200,7 +200,6 @@ namespace dd {
// pushed to solved
}
else if (simplified && changed_leading_term) {
SASSERT(target.state() == processed);
push_equation(to_simplify, target);
if (!m_var2level.empty()) {
m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);
@ -210,6 +209,13 @@ namespace dd {
sr.nextj();
}
}
}
void solver::simplify_using(equation_vector& set, equation const& eq) {
std::function<bool(equation&, bool&)> simplifier = [&](equation& target, bool& changed_leading_term) {
return try_simplify_using(target, eq, changed_leading_term);
};
simplify_using(set, simplifier);
}
/*
@ -342,6 +348,7 @@ namespace dd {
for (equation* e : m_solved) dealloc(e);
for (equation* e : m_to_simplify) dealloc(e);
for (equation* e : m_processed) dealloc(e);
m_subst.reset();
m_solved.reset();
m_processed.reset();
m_to_simplify.reset();
@ -352,18 +359,54 @@ namespace dd {
}
void solver::add(pdd const& p, u_dependency * dep) {
if (p.is_zero()) return;
equation * eq = alloc(equation, p, dep);
if (check_conflict(*eq)) {
if (p.is_zero())
return;
equation * eq = alloc(equation, p, dep);
if (check_conflict(*eq))
return;
}
push_equation(to_simplify, eq);
if (!m_var2level.empty()) {
if (!m_var2level.empty())
m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1);
}
update_stats_max_degree_and_size(*eq);
}
}
void solver::add_subst(unsigned v, pdd const& p, u_dependency* dep) {
m_subst.push_back({v, p, dep});
if (!m_var2level.empty())
m_levelp1 = std::max(m_var2level[v]+1, std::max(m_var2level[p.var()]+1, m_levelp1));
std::function<bool(equation&, bool&)> simplifier = [&](equation& dst, bool& changed_leading_term) {
auto r = dst.poly().subst_pdd(v, p);
if (r == dst.poly())
return false;
if (is_too_complex(r)) {
m_too_complex = true;
return false;
}
changed_leading_term = m.different_leading_term(r, dst.poly());
dst = r;
dst = m_dep_manager.mk_join(dst.dep(), dep);
update_stats_max_degree_and_size(dst);
return true;
};
if (!done())
simplify_using(m_processed, simplifier);
if (!done())
simplify_using(m_to_simplify, simplifier);
if (!done())
simplify_using(m_solved, simplifier);
}
void solver::simplify(pdd& p, u_dependency*& d) {
for (auto const& [v, q, d2] : m_subst) {
pdd r = p.subst_pdd(v, q);
if (r != p) {
p = r;
d = m_dep_manager.mk_join(d, d2);
}
}
}
bool solver::canceled() {
return m_limit.is_canceled();
@ -446,9 +489,24 @@ namespace dd {
}
std::ostream& solver::display(std::ostream& out) const {
out << "solved\n"; for (auto e : m_solved) display(out, *e);
out << "processed\n"; for (auto e : m_processed) display(out, *e);
out << "to_simplify\n"; for (auto e : m_to_simplify) display(out, *e);
if (!m_solved.empty()) {
out << "solved\n"; for (auto e : m_solved) display(out, *e);
}
if (!m_processed.empty()) {
out << "processed\n"; for (auto e : m_processed) display(out, *e);
}
if (!m_to_simplify.empty()) {
out << "to_simplify\n"; for (auto e : m_to_simplify) display(out, *e);
}
if (!m_subst.empty()) {
out << "subst\n";
for (auto const& [v, p, d] : m_subst) {
out << "v" << v << " := " << p;
if (m_print_dep)
m_print_dep(d, out);
out << "\n";
}
}
return display_statistics(out);
}

5
src/math/grobner/pdd_solver.h
View file

@ -118,6 +118,7 @@ private:
equation_vector m_solved; // equations with solved variables, triangular
equation_vector m_processed;
equation_vector m_to_simplify;
vector<std::tuple<unsigned, pdd, u_dependency*>> m_subst;
mutable u_dependency_manager m_dep_manager;
equation_vector m_all_eqs;
equation* m_conflict;
@ -136,6 +137,9 @@ public:
void add(pdd const& p) { add(p, nullptr); }
void add(pdd const& p, u_dependency * dep);
void simplify(pdd& p, u_dependency*& dep);
void add_subst(unsigned v, pdd const& p, u_dependency* dep);
void simplify();
void saturate();
@ -160,6 +164,7 @@ private:
void simplify_using(equation& eq, equation_vector const& eqs);
void simplify_using(equation_vector& set, equation const& eq);
void simplify_using(equation & dst, equation const& src, bool& changed_leading_term);
void simplify_using(equation_vector& set, std::function<bool(equation&, bool&)>& simplifier);
bool try_simplify_using(equation& target, equation const& source, bool& changed_leading_term);
bool is_trivial(equation const& eq) const { return eq.poly().is_zero(); }

1
src/math/interval/dep_intervals.h
View file

@ -222,7 +222,6 @@ public:
template <enum with_deps_t wd>
void mul(const rational& r, const interval& a, interval& b) const {
if (r.is_zero()) return;
m_imanager.mul(r.to_mpq(), a, b);
if (wd == with_deps) {
auto lower_dep = a.m_lower_dep;

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

@ -34,6 +34,7 @@ z3_add_component(lp
nla_basics_lemmas.cpp
nla_common.cpp
nla_core.cpp
nla_grobner.cpp
nla_intervals.cpp
nla_monotone_lemmas.cpp
nla_order_lemmas.cpp

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

@ -40,7 +40,7 @@ bool horner::row_has_monomial_to_refine(const T& row) const {
template <typename T>
bool horner::row_is_interesting(const T& row) const {
TRACE("nla_solver_details", c().print_row(row, tout););
if (row.size() > c().m_nla_settings.horner_row_length_limit()) {
if (row.size() > c().m_nla_settings.horner_row_length_limit) {
TRACE("nla_solver_details", tout << "disregard\n";);
return false;
}
@ -98,7 +98,7 @@ bool horner::lemmas_on_row(const T& row) {
}
bool horner::horner_lemmas() {
if (!c().m_nla_settings.run_horner()) {
if (!c().m_nla_settings.run_horner) {
TRACE("nla_solver", tout << "not generating horner lemmas\n";);
return false;
}

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

@ -275,9 +275,6 @@ class lar_solver : public column_namer {
return m_column_buffer;
}
bool bound_is_integer_for_integer_column(unsigned j, const mpq & right_side) const;
inline unsigned get_base_column_in_row(unsigned row_index) const {
return m_mpq_lar_core_solver.m_r_solver.get_base_column_in_row(row_index);
}
inline lar_core_solver & get_core_solver() { return m_mpq_lar_core_solver; }
void catch_up_in_updating_int_solver();
var_index to_column(unsigned ext_j) const;
@ -357,6 +354,10 @@ public:
}
void set_value_for_nbasic_column(unsigned j, const impq& new_val);
inline unsigned get_base_column_in_row(unsigned row_index) const {
return m_mpq_lar_core_solver.m_r_solver.get_base_column_in_row(row_index);
}
// lp_assert(implied_bound_is_correctly_explained(ib, explanation)); }
constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side);
@ -630,6 +631,7 @@ public:
}
void round_to_integer_solution();
inline const row_strip<mpq> & get_row(unsigned i) const { return A_r().m_rows[i]; }
inline const row_strip<mpq> & basic2row(unsigned i) const { return A_r().m_rows[row_of_basic_column(i)]; }
inline const column_strip & get_column(unsigned i) const { return A_r().m_columns[i]; }
bool row_is_correct(unsigned i) const;
bool ax_is_correct() const;

8
src/math/lp/nla_common.cpp
View file

@ -71,11 +71,11 @@ void common::add_deps_of_fixed(lpvar j, u_dependency*& dep) {
// creates a nex expression for the coeff and var,
nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_dependency*& dep) {
SASSERT(!coeff.is_zero());
if (c().m_nla_settings.horner_subs_fixed() == 1 && c().var_is_fixed(j)) {
if (c().m_nla_settings.horner_subs_fixed == 1 && c().var_is_fixed(j)) {
add_deps_of_fixed(j, dep);
return cn.mk_scalar(coeff * c().m_lar_solver.column_lower_bound(j).x);
}
if (c().m_nla_settings.horner_subs_fixed() == 2 && c().var_is_fixed_to_zero(j)) {
if (c().m_nla_settings.horner_subs_fixed == 2 && c().var_is_fixed_to_zero(j)) {
add_deps_of_fixed(j, dep);
return cn.mk_scalar(rational(0));
}
@ -89,10 +89,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_depende
mf *= coeff;
u_dependency * initial_dep = dep;
for (lpvar k : m.vars()) {
if (c().m_nla_settings.horner_subs_fixed() && c().var_is_fixed(k)) {
if (c().m_nla_settings.horner_subs_fixed == 1 && c().var_is_fixed(k)) {
add_deps_of_fixed(k, dep);
mf *= c().m_lar_solver.column_lower_bound(k).x;
} else if (c().m_nla_settings.horner_subs_fixed() == 2 &&
} else if (c().m_nla_settings.horner_subs_fixed == 2 &&
c().var_is_fixed_to_zero(k)) {
dep = initial_dep;
add_deps_of_fixed(k, dep);

3738
src/math/lp/nla_core.cpp
View file

File diff suppressed because it is too large Load diff

83
src/math/lp/nla_core.h
View file

@ -18,15 +18,18 @@
#include "math/lp/nla_basics_lemmas.h"
#include "math/lp/nla_order_lemmas.h"
#include "math/lp/nla_monotone_lemmas.h"
#include "math/lp/nla_grobner.h"
#include "math/lp/emonics.h"
#include "math/lp/nla_settings.h"
#include "math/lp/nex.h"
#include "math/lp/horner.h"
#include "math/lp/monomial_bounds.h"
#include "math/lp/nla_intervals.h"
#include "math/grobner/pdd_solver.h"
#include "nlsat/nlsat_solver.h"
namespace nra {
class solver;
}
namespace nla {
@ -139,6 +142,20 @@ struct pp_factorization {
};
class core {
friend struct common;
friend class new_lemma;
friend class grobner;
friend class order;
friend struct basics;
friend struct tangents;
friend class monotone;
friend struct nla_settings;
friend class intervals;
friend class horner;
friend class solver;
friend class monomial_bounds;
friend class nra::solver;
struct stats {
unsigned m_nla_explanations;
unsigned m_nla_lemmas;
@ -148,16 +165,18 @@ class core {
memset(this, 0, sizeof(*this));
}
};
stats m_stats;
friend class new_lemma;
unsigned m_nlsat_delay { 50 };
unsigned m_nlsat_fails { 0 };
stats m_stats;
unsigned m_nlsat_delay = 50;
unsigned m_nlsat_fails = 0;
bool should_run_bounded_nlsat();
lbool bounded_nlsat();
public:
var_eqs<emonics> m_evars;
lp::lar_solver& m_lar_solver;
reslimit& m_reslim;
vector<lemma> * m_lemma_vec;
lp::u_set m_to_refine;
tangents m_tangents;
@ -166,24 +185,21 @@ public:
monotone m_monotone;
intervals m_intervals;
monomial_bounds m_monomial_bounds;
nla_settings m_nla_settings;
horner m_horner;
nla_settings m_nla_settings;
dd::pdd_manager m_pdd_manager;
dd::solver m_pdd_grobner;
private:
grobner m_grobner;
emonics m_emons;
svector<lpvar> m_add_buffer;
mutable lp::u_set m_active_var_set;
lp::u_set m_rows;
reslimit m_nra_lim;
public:
reslimit& m_reslim;
bool m_use_nra_model;
bool m_use_nra_model = false;
nra::solver m_nra;
private:
bool m_cautious_patching;
lpvar m_patched_var;
monic const* m_patched_monic;
bool m_cautious_patching = true;
lpvar m_patched_var = 0;
monic const* m_patched_monic = nullptr;
void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
@ -205,6 +221,8 @@ public:
m_active_var_set.resize(m_lar_solver.number_of_vars());
}
unsigned get_var_weight(lpvar) const;
reslimit& reslim() { return m_reslim; }
emonics& emons() { return m_emons; }
const emonics& emons() const { return m_emons; }
@ -243,12 +261,15 @@ public:
// returns true if the combination of the Horner's schema and Grobner Basis should be called
bool need_run_horner() const {
return m_nla_settings.run_horner() && lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0;
return m_nla_settings.run_horner && lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency == 0;
}
bool need_run_grobner() const {
return m_nla_settings.run_grobner() && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency() == 0;
return m_nla_settings.run_grobner && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency == 0;
}
void set_active_vars_weights(nex_creator&);
std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
void incremental_linearization(bool);
@ -450,31 +471,19 @@ public:
lpvar map_to_root(lpvar) const;
std::ostream& print_terms(std::ostream&) const;
std::ostream& print_term(const lp::lar_term&, std::ostream&) const;
template <typename T>
std::ostream& print_row(const T & row , std::ostream& out) const {
std::ostream& print_row(const T& row, std::ostream& out) const {
vector<std::pair<rational, lpvar>> v;
for (auto p : row) {
v.push_back(std::make_pair(p.coeff(), p.var()));
}
return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); },
out);
return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); }, out);
}
void run_grobner();
void find_nl_cluster();
void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);
std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
void display_matrix_of_m_rows(std::ostream & out) const;
void set_active_vars_weights(nex_creator&);
unsigned get_var_weight(lpvar) const;
void add_row_to_grobner(const vector<lp::row_cell<rational>> & row);
bool check_pdd_eq(const dd::solver::equation*);
const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
void set_level2var_for_grobner();
void configure_grobner();
bool influences_nl_var(lpvar) const;
bool is_nl_var(lpvar) const;
bool is_used_in_monic(lpvar) const;
void patch_monomials();
void patch_monomials_on_to_refine();

545
src/math/lp/nla_grobner.cpp Normal file
View file

@ -0,0 +1,545 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
nla_grobner.cpp
Author:
Lev Nachmanson (levnach)
Nikolaj Bjorner (nbjorner)
--*/
#include "util/uint_set.h"
#include "math/lp/nla_core.h"
#include "math/lp/factorization_factory_imp.h"
#include "math/lp/nex.h"
#include "math/grobner/pdd_solver.h"
#include "math/dd/pdd_interval.h"
#include "math/dd/pdd_eval.h"
namespace nla {
grobner::grobner(core* c):
common(c),
m_pdd_manager(m_core.m_lar_solver.number_of_vars()),
m_solver(m_core.m_reslim, m_pdd_manager),
m_lar_solver(m_core.m_lar_solver)
{}
lp::lp_settings& grobner::lp_settings() {
return c().lp_settings();
}
void grobner::operator()() {
unsigned& quota = c().m_nla_settings.grobner_quota;
if (quota == 1)
return;
lp_settings().stats().m_grobner_calls++;
find_nl_cluster();
configure();
m_solver.saturate();
if (is_conflicting())
return;
if (propagate_bounds())
return;
if (propagate_eqs())
return;
if (propagate_factorization())
return;
if (quota > 1)
quota--;
IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota << "\n");
IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
#if 0
// diagnostics: did we miss something
vector<dd::pdd> eqs;
for (auto eq : m_solver.equations())
eqs.push_back(eq->poly());
c().m_nra.check(eqs);
#endif
}
bool grobner::is_conflicting() {
unsigned conflicts = 0;
for (auto eq : m_solver.equations())
if (is_conflicting(*eq) && ++conflicts >= m_solver.number_of_conflicts_to_report())
break;
if (conflicts > 0)
lp_settings().stats().m_grobner_conflicts++;
TRACE("grobner", m_solver.display(tout));
IF_VERBOSE(2, if (conflicts > 0) verbose_stream() << "grobner conflict\n");
return conflicts > 0;
}
bool grobner::propagate_bounds() {
unsigned changed = 0;
for (auto eq : m_solver.equations())
if (propagate_bounds(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
return true;
return changed > 0;
}
bool grobner::propagate_eqs() {
unsigned changed = 0;
for (auto eq : m_solver.equations())
if (propagate_fixed(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
return true;
return changed > 0;
}
bool grobner::propagate_factorization() {
unsigned changed = 0;
for (auto eq : m_solver.equations())
if (propagate_factorization(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
return true;
return changed > 0;
}
/**
\brief detect equalities
- k*x = 0, that is x = 0
- ax + b = 0
*/
typedef lp::lar_term term;
bool grobner::propagate_fixed(const dd::solver::equation& eq) {
dd::pdd const& p = eq.poly();
//IF_VERBOSE(0, verbose_stream() << p << "\n");
if (p.is_unary()) {
unsigned v = p.var();
if (c().var_is_fixed(v))
return false;
ineq new_eq(v, llc::EQ, rational::zero());
if (c().ineq_holds(new_eq))
return false;
new_lemma lemma(c(), "pdd-eq");
add_dependencies(lemma, eq);
lemma |= new_eq;
return true;
}
if (p.is_offset()) {
unsigned v = p.var();
if (c().var_is_fixed(v))
return false;
rational a = p.hi().val();
rational b = -p.lo().val();
rational d = lcm(denominator(a), denominator(b));
a *= d;
b *= d;
ineq new_eq(term(a, v), llc::EQ, b);
if (c().ineq_holds(new_eq))
return false;
new_lemma lemma(c(), "pdd-eq");
add_dependencies(lemma, eq);
lemma |= new_eq;
return true;
}
return false;
}
/**
\brief detect simple factors
x*q = 0 => x = 0 or q = 0
*/
bool grobner::propagate_factorization(const dd::solver::equation& eq) {
dd::pdd const& p = eq.poly();
auto [vars, q] = p.var_factors();
if (vars.empty() || !q.is_linear())
return false;
// IF_VERBOSE(0, verbose_stream() << "factored " << q << " : " << vars << "\n");
term t;
while (!q.is_val()) {
t.add_monomial(q.hi().val(), q.var());
q = q.lo();
}
vector<ineq> ineqs;
for (auto v : vars)
ineqs.push_back(ineq(v, llc::EQ, rational::zero()));
ineqs.push_back(ineq(t, llc::EQ, -q.val()));
for (auto const& i : ineqs)
if (c().ineq_holds(i))
return false;
new_lemma lemma(c(), "pdd-factored");
add_dependencies(lemma, eq);
for (auto const& i : ineqs)
lemma |= i;
//lemma.display(verbose_stream());
return true;
}
void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) {
lp::explanation ex;
u_dependency_manager dm;
vector<unsigned, false> lv;
dm.linearize(eq.dep(), lv);
for (unsigned ci : lv)
ex.push_back(ci);
lemma &= ex;
}
void grobner::configure() {
m_solver.reset();
try {
set_level2var();
TRACE("grobner",
tout << "base vars: ";
for (lpvar j : c().active_var_set())
if (m_lar_solver.is_base(j))
tout << "j" << j << " ";
tout << "\n");
for (lpvar j : c().active_var_set()) {
if (m_lar_solver.is_base(j))
add_row(m_lar_solver.basic2row(j));
if (c().is_monic_var(j) && c().var_is_fixed(j))
add_fixed_monic(j);
}
}
catch (...) {
IF_VERBOSE(2, verbose_stream() << "pdd throw\n");
return;
}
TRACE("grobner", m_solver.display(tout));
#if 0
IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream()));
dd::pdd_eval eval(m_pdd_manager);
eval.var2val() = [&](unsigned j){ return val(j); };
for (auto* e : m_pdd_grobner.equations()) {
dd::pdd p = e->poly();
rational v = eval(p);
if (p.is_linear() && !eval(p).is_zero()) {
IF_VERBOSE(0, verbose_stream() << "violated linear constraint " << p << "\n");
}
}
#endif
struct dd::solver::config cfg;
cfg.m_max_steps = m_solver.equations().size();
cfg.m_max_simplified = c().m_nla_settings.grobner_max_simplified;
cfg.m_eqs_growth = c().m_nla_settings.grobner_eqs_growth;
cfg.m_expr_size_growth = c().m_nla_settings.grobner_expr_size_growth;
cfg.m_expr_degree_growth = c().m_nla_settings.grobner_expr_degree_growth;
cfg.m_number_of_conflicts_to_report = c().m_nla_settings.grobner_number_of_conflicts_to_report;
m_solver.set(cfg);
m_solver.adjust_cfg();
m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
}
std::ostream& grobner::diagnose_pdd_miss(std::ostream& out) {
// m_pdd_grobner.display(out);
dd::pdd_eval eval;
eval.var2val() = [&](unsigned j){ return val(j); };
for (auto* e : m_solver.equations()) {
dd::pdd p = e->poly();
rational v = eval(p);
if (!v.is_zero()) {
out << p << " := " << v << "\n";
}
}
for (unsigned j = 0; j < m_lar_solver.number_of_vars(); ++j) {
if (m_lar_solver.column_has_lower_bound(j) || m_lar_solver.column_has_upper_bound(j)) {
out << j << ": [";
if (m_lar_solver.column_has_lower_bound(j)) out << m_lar_solver.get_lower_bound(j);
out << "..";
if (m_lar_solver.column_has_upper_bound(j)) out << m_lar_solver.get_upper_bound(j);
out << "]\n";
}
}
return out;
}
bool grobner::is_conflicting(const dd::solver::equation& e) {
auto& di = c().m_intervals.get_dep_intervals();
dd::pdd_interval eval(di);
eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) {
if (deps) c().m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
else c().m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
};
scoped_dep_interval i(di), i_wd(di);
eval.get_interval<dd::w_dep::without_deps>(e.poly(), i);
if (!di.separated_from_zero(i)) {
TRACE("grobner", m_solver.display(tout << "not separated from 0 ", e) << "\n";
eval.get_interval_distributed<dd::w_dep::without_deps>(e.poly(), i);
tout << "separated from 0: " << di.separated_from_zero(i) << "\n";
for (auto j : e.poly().free_vars()) {
scoped_dep_interval a(di);
c().m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
c().m_intervals.display(tout << "j" << j << " ", a); tout << " ";
}
tout << "\n");
return false;
}
eval.get_interval<dd::w_dep::with_deps>(e.poly(), i_wd);
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
new_lemma lemma(m_core, "pdd");
lemma &= e;
};
if (di.check_interval_for_conflict_on_zero(i_wd, e.dep(), f)) {
TRACE("grobner", m_solver.display(tout << "conflict ", e) << "\n");
return true;
}
else {
TRACE("grobner", m_solver.display(tout << "no conflict ", e) << "\n");
return false;
}
}
bool grobner::propagate_bounds(const dd::solver::equation& e) {
return false;
// TODO
auto& di = c().m_intervals.get_dep_intervals();
dd::pdd_interval eval(di);
eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) {
if (deps) c().m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
else c().m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
};
scoped_dep_interval i(di), i_wd(di);
eval.get_interval<dd::w_dep::without_deps>(e.poly(), i);
return false;
}
void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar> & q) {
if (c().active_var_set_contains(j))
return;
c().insert_to_active_var_set(j);
if (c().is_monic_var(j)) {
const monic& m = c().emons()[j];
for (auto fcn : factorization_factory_imp(m, m_core))
for (const factor& fc: fcn)
q.push_back(var(fc));
}
if (c().var_is_fixed(j))
return;
const auto& matrix = m_lar_solver.A_r();
for (auto & s : matrix.m_columns[j]) {
unsigned row = s.var();
if (m_rows.contains(row))
continue;
m_rows.insert(row);
unsigned k = m_lar_solver.get_base_column_in_row(row);
if (m_lar_solver.column_is_free(k) && k != j)
continue;
CTRACE("grobner", matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit,
tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";);
if (matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit)
continue;
for (auto& rc : matrix.m_rows[row])
add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q);
}
}
const rational& grobner::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) {
unsigned lc, uc;
m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
dep = c().m_intervals.mk_join(dep, c().m_intervals.mk_leaf(lc));
dep = c().m_intervals.mk_join(dep, c().m_intervals.mk_leaf(uc));
return m_lar_solver.column_lower_bound(j).x;
}
dd::pdd grobner::pdd_expr(const rational& coeff, lpvar j, u_dependency*& dep) {
dd::pdd r = m_pdd_manager.mk_val(coeff);
sbuffer<lpvar> vars;
vars.push_back(j);
u_dependency* zero_dep = dep;
while (!vars.empty()) {
j = vars.back();
vars.pop_back();
if (c().m_nla_settings.grobner_subs_fixed > 0 && c().var_is_fixed_to_zero(j)) {
r = m_pdd_manager.mk_val(val_of_fixed_var_with_deps(j, zero_dep));
dep = zero_dep;
return r;
}
if (c().m_nla_settings.grobner_subs_fixed == 1 && c().var_is_fixed(j))
r *= val_of_fixed_var_with_deps(j, dep);
else if (!c().is_monic_var(j))
r *= m_pdd_manager.mk_var(j);
else
for (lpvar k : c().emons()[j].vars())
vars.push_back(k);
}
return r;
}
/**
\brief convert p == 0 into a solved form v == r, such that
v has bounds [lo, oo) iff r has bounds [lo', oo)
v has bounds (oo,hi] iff r has bounds (oo,hi']
The solved form allows the Grobner solver identify more bounds conflicts.
A bad leading term can miss bounds conflicts.
For example for x + y + z == 0 where x, y : [0, oo) and z : (oo,0]
we prefer to solve z == -x - y instead of x == -z - y
because the solution -z - y has neither an upper, nor a lower bound.
*/
bool grobner::is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r) {
if (!p.is_linear())
return false;
r = p;
unsigned num_lo = 0, num_hi = 0;
unsigned lo = 0, hi = 0;
rational lc, hc, c;
while (!r.is_val()) {
SASSERT(r.hi().is_val());
v = r.var();
rational val = r.hi().val();
switch (m_lar_solver.get_column_type(v)) {
case lp::column_type::lower_bound:
if (val > 0) num_lo++, lo = v, lc = val; else num_hi++, hi = v, hc = val;
break;
case lp::column_type::upper_bound:
if (val < 0) num_lo++, lo = v, lc = val; else num_hi++, hi = v, hc = val;
break;
case lp::column_type::fixed:
case lp::column_type::boxed:
break;
default:
return false;
}
if (num_lo > 1 && num_hi > 1)
return false;
r = r.lo();
}
if (num_lo == 1 && num_hi > 1) {
v = lo;
c = lc;
}
else if (num_hi == 1 && num_lo > 1) {
v = hi;
c = hc;
}
else
return false;
r = c*m_pdd_manager.mk_var(v) - p;
if (c != 1)
r = r * (1/c);
return true;
}
/**
\brief add an equality to grobner solver, convert it to solved form if available.
*/
void grobner::add_eq(dd::pdd& p, u_dependency* dep) {
unsigned v;
dd::pdd q(m_pdd_manager);
m_solver.simplify(p, dep);
if (is_solved(p, v, q))
m_solver.add_subst(v, q, dep);
else
m_solver.add(p, dep);
}
void grobner::add_fixed_monic(unsigned j) {
u_dependency* dep = nullptr;
dd::pdd r = m_pdd_manager.mk_val(rational(1));
for (lpvar k : c().emons()[j].vars())
r *= pdd_expr(rational::one(), k, dep);
r -= val_of_fixed_var_with_deps(j, dep);
add_eq(r, dep);
}
void grobner::add_row(const vector<lp::row_cell<rational>> & row) {
u_dependency *dep = nullptr;
rational val;
dd::pdd sum = m_pdd_manager.mk_val(rational(0));
for (const auto &p : row)
sum += pdd_expr(p.coeff(), p.var(), dep);
TRACE("grobner", c().print_row(row, tout) << " " << sum << "\n");
add_eq(sum, dep);
}
void grobner::find_nl_cluster() {
prepare_rows_and_active_vars();
svector<lpvar> q;
TRACE("grobner", for (lpvar j : c().m_to_refine) print_monic(c().emons()[j], tout) << "\n";);
for (lpvar j : c().m_to_refine)
q.push_back(j);
while (!q.empty()) {
lpvar j = q.back();
q.pop_back();
add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
}
TRACE("grobner", tout << "vars in cluster: ";
for (lpvar j : c().active_var_set()) tout << "j" << j << " "; tout << "\n";
display_matrix_of_m_rows(tout);
);
}
void grobner::prepare_rows_and_active_vars() {
m_rows.clear();
m_rows.resize(m_lar_solver.row_count());
c().clear_and_resize_active_var_set();
}
void grobner::display_matrix_of_m_rows(std::ostream & out) const {
const auto& matrix = m_lar_solver.A_r();
out << m_rows.size() << " rows" << "\n";
out << "the matrix\n";
for (const auto & r : matrix.m_rows)
c().print_row(r, out) << std::endl;
}
void grobner::set_level2var() {
unsigned n = m_lar_solver.column_count();
unsigned_vector sorted_vars(n), weighted_vars(n);
for (unsigned j = 0; j < n; j++) {
sorted_vars[j] = j;
weighted_vars[j] = c().get_var_weight(j);
}
#if 1
// potential update to weights
for (unsigned j = 0; j < n; j++) {
if (c().is_monic_var(j) && c().m_to_refine.contains(j)) {
for (lpvar k : c().m_emons[j].vars()) {
weighted_vars[k] += 6;
}
}
}
#endif
std::sort(sorted_vars.begin(), sorted_vars.end(), [&](unsigned a, unsigned b) {
unsigned wa = weighted_vars[a];
unsigned wb = weighted_vars[b];
return wa < wb || (wa == wb && a < b); });
unsigned_vector l2v(n);
for (unsigned j = 0; j < n; j++)
l2v[j] = sorted_vars[j];
m_pdd_manager.reset(l2v);
TRACE("grobner",
for (auto v : sorted_vars)
tout << "j" << v << " w:" << weighted_vars[v] << " ";
tout << "\n");
}
}

64
src/math/lp/nla_grobner.h Normal file
View file

@ -0,0 +1,64 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
--*/
#pragma once
#include "math/lp/nla_common.h"
#include "math/lp/nla_intervals.h"
#include "math/lp/nex.h"
#include "math/lp/cross_nested.h"
#include "math/lp/u_set.h"
#include "math/grobner/pdd_solver.h"
namespace nla {
class core;
class grobner : common {
dd::pdd_manager m_pdd_manager;
dd::solver m_solver;
lp::lar_solver& m_lar_solver;
lp::u_set m_rows;
lp::lp_settings& lp_settings();
// solving
bool is_conflicting();
bool is_conflicting(const dd::solver::equation& eq);
bool propagate_bounds();
bool propagate_bounds(const dd::solver::equation& eq);
bool propagate_eqs();
bool propagate_fixed(const dd::solver::equation& eq);
bool propagate_factorization();
bool propagate_factorization(const dd::solver::equation& eq);
void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq);
// setup
void configure();
void set_level2var();
void find_nl_cluster();
void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);
void add_row(const vector<lp::row_cell<rational>>& row);
void add_fixed_monic(unsigned j);
bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r);
void add_eq(dd::pdd& p, u_dependency* dep);
const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*& dep);
void display_matrix_of_m_rows(std::ostream& out) const;
std::ostream& diagnose_pdd_miss(std::ostream& out);
public:
grobner(core *core);
void operator()();
};
}

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

@ -19,7 +19,7 @@ typedef lp::lar_term term;
// a > b && c > 0 => ac > bc
void order::order_lemma() {
TRACE("nla_solver", );
if (!c().m_nla_settings.run_order()) {
if (!c().m_nla_settings.run_order) {
TRACE("nla_solver", tout << "not generating order lemmas\n";);
return;
}

116
src/math/lp/nla_settings.h
View file

@ -9,94 +9,38 @@ Author:
#pragma once
namespace nla {
class nla_settings {
bool m_run_order;
bool m_run_tangents;
bool m_run_horner;
// how often to call the horner heuristic
unsigned m_horner_frequency;
unsigned m_horner_row_length_limit;
unsigned m_horner_subs_fixed;
// grobner fields
bool m_run_grobner;
unsigned m_grobner_row_length_limit;
unsigned m_grobner_subs_fixed;
unsigned m_grobner_eqs_growth;
unsigned m_grobner_tree_size_growth;
unsigned m_grobner_expr_size_growth;
unsigned m_grobner_expr_degree_growth;
unsigned m_grobner_max_simplified;
unsigned m_grobner_number_of_conflicts_to_report;
unsigned m_grobner_quota;
unsigned m_grobner_frequency;
bool m_run_nra;
// expensive patching
bool m_expensive_patching;
public:
nla_settings() : m_run_order(true),
m_run_tangents(true),
m_run_horner(true),
m_horner_frequency(4),
m_horner_row_length_limit(10),
m_horner_subs_fixed(2),
m_run_grobner(true),
m_grobner_row_length_limit(50),
m_grobner_subs_fixed(false),
m_grobner_quota(0),
m_grobner_frequency(4),
m_run_nra(false),
m_expensive_patching(false)
{}
unsigned grobner_eqs_growth() const { return m_grobner_eqs_growth;}
unsigned& grobner_eqs_growth() { return m_grobner_eqs_growth;}
bool run_order() const { return m_run_order; }
bool& run_order() { return m_run_order; }
struct nla_settings {
bool run_order = true;
bool run_tangents = true;
// horner fields
bool run_horner = true;
unsigned horner_frequency = 4;
unsigned horner_row_length_limit = 10;
unsigned horner_subs_fixed = 2;
bool run_tangents() const { return m_run_tangents; }
bool& run_tangents() { return m_run_tangents; }
// grobner fields
bool run_grobner = true;
unsigned grobner_row_length_limit = 50;
unsigned grobner_subs_fixed = 1;
unsigned grobner_eqs_growth = 10;
unsigned grobner_tree_size_growth = 2;
unsigned grobner_expr_size_growth = 2;
unsigned grobner_expr_degree_growth = 2;
unsigned grobner_max_simplified = 10000;
unsigned grobner_number_of_conflicts_to_report = 1;
unsigned grobner_quota = 0;
unsigned grobner_frequency = 4;
bool expensive_patching() const { return m_expensive_patching; }
bool& expensive_patching() { return m_expensive_patching; }
bool run_horner() const { return m_run_horner; }
bool& run_horner() { return m_run_horner; }
unsigned horner_frequency() const { return m_horner_frequency; }
unsigned& horner_frequency() { return m_horner_frequency; }
unsigned horner_row_length_limit() const { return m_horner_row_length_limit; }
unsigned& horner_row_length_limit() { return m_horner_row_length_limit; }
unsigned horner_subs_fixed() const { return m_horner_subs_fixed; }
unsigned& horner_subs_fixed() { return m_horner_subs_fixed; }
bool run_grobner() const { return m_run_grobner; }
bool& run_grobner() { return m_run_grobner; }
unsigned grobner_frequency() const { return m_grobner_frequency; }
unsigned& grobner_frequency() { return m_grobner_frequency; }
bool run_nra() const { return m_run_nra; }
bool& run_nra() { return m_run_nra; }
unsigned grobner_row_length_limit() const { return m_grobner_row_length_limit; }
unsigned& grobner_row_length_limit() { return m_grobner_row_length_limit; }
unsigned grobner_subs_fixed() const { return m_grobner_subs_fixed; }
unsigned& grobner_subs_fixed() { return m_grobner_subs_fixed; }
unsigned grobner_tree_size_growth() const { return m_grobner_tree_size_growth; }
unsigned & grobner_tree_size_growth() { return m_grobner_tree_size_growth; }
unsigned grobner_expr_size_growth() const { return m_grobner_expr_size_growth; }
unsigned & grobner_expr_size_growth() { return m_grobner_expr_size_growth; }
unsigned grobner_expr_degree_growth() const { return m_grobner_expr_degree_growth; }
unsigned & grobner_expr_degree_growth() { return m_grobner_expr_degree_growth; }
unsigned grobner_max_simplified() const { return m_grobner_max_simplified; }
unsigned & grobner_max_simplified() { return m_grobner_max_simplified; }
unsigned grobner_number_of_conflicts_to_report() const { return m_grobner_number_of_conflicts_to_report; }
unsigned & grobner_number_of_conflicts_to_report() { return m_grobner_number_of_conflicts_to_report; }
unsigned& grobner_quota() { return m_grobner_quota; }
// nra fields
bool run_nra = false;
};
// expensive patching
bool expensive_patching = false;
nla_settings() {}
};
}

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

@ -186,7 +186,7 @@ tangents::tangents(core * c) : common(c) {}
void tangents::tangent_lemma() {
factorization bf(nullptr);
const monic* m = nullptr;
if (c().m_nla_settings.run_tangents() && c().find_bfc_to_refine(m, bf)) {
if (c().m_nla_settings.run_tangents && c().find_bfc_to_refine(m, bf)) {
lpvar j = m->var();
tangent_imp tangent(point(val(bf[0]), val(bf[1])), c().val(j), *m, bf, *this);
tangent();

108
src/math/lp/nra_solver.cpp
View file

@ -65,12 +65,10 @@ struct solver::imp {
}
// add polynomial definitions.
for (auto const& m : m_nla_core.emons()) {
for (auto const& m : m_nla_core.emons())
add_monic_eq(m);
}
for (unsigned i : m_term_set) {
for (unsigned i : m_term_set)
add_term(i);
}
// TBD: add variable bounds?
lbool r = l_undef;
@ -176,7 +174,103 @@ struct solver::imp {
lp_assert(false); // unreachable
}
m_nlsat->mk_clause(1, &lit, a);
}
}
lbool check(vector<dd::pdd> const& eqs) {
m_zero = nullptr;
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
m_zero = alloc(scoped_anum, am());
m_lp2nl.reset();
m_term_set.clear();
for (auto const& eq : eqs)
add_eq(eq);
for (auto const& [v, w] : m_lp2nl) {
auto& ls = m_nla_core.m_lar_solver;
if (ls.column_has_lower_bound(v))
add_lb(ls.get_lower_bound(v), w);
if (ls.column_has_upper_bound(v))
add_ub(ls.get_upper_bound(v), w);
}
lbool r = l_undef;
try {
r = m_nlsat->check();
}
catch (z3_exception&) {
if (m_limit.is_canceled()) {
r = l_undef;
}
else {
throw;
}
}
IF_VERBOSE(0, verbose_stream() << "check-nra " << r << "\n";
m_nlsat->display(verbose_stream());
for (auto const& [v, w] : m_lp2nl) {
auto& ls = m_nla_core.m_lar_solver;
if (ls.column_has_lower_bound(v))
verbose_stream() << w << " >= " << ls.get_lower_bound(v) << "\n";
if (ls.column_has_upper_bound(v))
verbose_stream() << w << " <= " << ls.get_upper_bound(v) << "\n";
});
return r;
}
void add_eq(dd::pdd const& eq) {
dd::pdd normeq = eq;
rational lc(1);
for (auto const& [c, m] : eq)
lc = lcm(denominator(c), lc);
if (lc != 1)
normeq *= lc;
polynomial::manager& pm = m_nlsat->pm();
polynomial::polynomial_ref p(pdd2polynomial(normeq), pm);
bool is_even[1] = { false };
polynomial::polynomial* ps[1] = { p };
nlsat::literal lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
m_nlsat->mk_clause(1, &lit, nullptr);
}
void add_lb(lp::impq const& b, unsigned w) {
add_bound(b.x, w, b.y <= 0, b.y > 0 ? nlsat::atom::kind::GT : nlsat::atom::kind::LT);
}
void add_ub(lp::impq const& b, unsigned w) {
add_bound(b.x, w, b.y >= 0, b.y < 0 ? nlsat::atom::kind::LT : nlsat::atom::kind::GT);
}
// w - bound < 0
// w - bound > 0
void add_bound(lp::mpq const& bound, unsigned w, bool neg, nlsat::atom::kind k) {
polynomial::manager& pm = m_nlsat->pm();
polynomial::polynomial_ref p1(pm.mk_polynomial(w), pm);
polynomial::polynomial_ref p2(pm.mk_const(bound), pm);
polynomial::polynomial_ref p(pm.sub(p1, p2), pm);
polynomial::polynomial* ps[1] = { p };
bool is_even[1] = { false };
nlsat::literal lit = m_nlsat->mk_ineq_literal(k, 1, ps, is_even);
if (neg)
lit.neg();
m_nlsat->mk_clause(1, &lit, nullptr);
}
polynomial::polynomial* pdd2polynomial(dd::pdd const& p) {
polynomial::manager& pm = m_nlsat->pm();
if (p.is_val())
return pm.mk_const(p.val());
polynomial::polynomial_ref lo(pdd2polynomial(p.lo()), pm);
polynomial::polynomial_ref hi(pdd2polynomial(p.hi()), pm);
unsigned w, v = p.var();
if (!m_lp2nl.find(v, w)) {
w = m_nlsat->mk_var(false);
m_lp2nl.insert(v, w);
}
polynomial::polynomial_ref vp(pm.mk_polynomial(w, 1), pm);
return pm.add(lo, pm.mul(vp, hi));
}
bool is_int(lp::var_index v) {
return s.var_is_int(v);
@ -265,6 +359,10 @@ lbool solver::check() {
return m_imp->check();
}
lbool solver::check(vector<dd::pdd> const& eqs) {
return m_imp->check(eqs);
}
bool solver::need_check() {
return m_imp->need_check();
}

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

@ -9,6 +9,7 @@
#include "util/rlimit.h"
#include "util/params.h"
#include "nlsat/nlsat_solver.h"
#include "math/dd/dd_pdd.h"
namespace lp {
class lar_solver;
@ -36,6 +37,11 @@ namespace nra {
*/
lbool check();
/**
\breif Check feasibility of equalities modulo bounds constraints on their variables.
*/
lbool check(vector<dd::pdd> const& eqs);
/*
\brief determine whether nra check is needed.
*/

1
src/opt/CMakeLists.txt
View file

@ -14,6 +14,7 @@ z3_add_component(opt
opt_solver.cpp
pb_sls.cpp
sortmax.cpp
totalizer.cpp
wmax.cpp
COMPONENT_DEPENDENCIES
sat_solver

45
src/opt/maxcore.cpp
View file

@ -13,6 +13,7 @@ Abstract:
- mus-mss: based on dual refinement of bounds.
- binary: binary version of maxres
- rc2: implementaion of rc2 heuristic using cardinality constraints
- rc2t: implementaion of rc2 heuristic using totalizerx
- rc2-binary: hybrid of rc2 and binary maxres. Perform one step of binary maxres.
If there are more than 16 soft constraints create a cardinality constraint.
@ -60,6 +61,7 @@ Notes:
#include "ast/ast_pp.h"
#include "ast/pb_decl_plugin.h"
#include "ast/ast_util.h"
#include "ast/ast_smt_pp.h"
#include "model/model_smt2_pp.h"
#include "solver/solver.h"
#include "solver/mus.h"
@ -71,6 +73,8 @@ Notes:
#include "opt/opt_cores.h"
#include "opt/maxsmt.h"
#include "opt/maxcore.h"
#include "opt/totalizer.h"
#include <iostream>
using namespace opt;
@ -131,6 +135,7 @@ private:
bool m_enable_lns = false; // enable LNS improvements
unsigned m_lns_conflicts = 1000; // number of conflicts used for LNS improvement
bool m_enable_core_rotate = false; // enable core rotation
bool m_use_totalizer = true; // use totalizer instead of cardinality encoding
std::string m_trace_id;
typedef ptr_vector<expr> exprs;
@ -169,7 +174,10 @@ public:
}
}
~maxcore() override {}
~maxcore() override {
for (auto& [k,t] : m_totalizers)
dealloc(t);
}
bool is_literal(expr* l) {
return
@ -780,8 +788,38 @@ public:
obj_map<expr, expr*> m_at_mostk;
obj_map<expr, bound_info> m_bounds;
rational m_unfold_upper;
obj_map<expr, totalizer*> m_totalizers;
expr* mk_atmost_tot(expr_ref_vector const& es, unsigned bound, rational const& weight) {
pb_util pb(m);
expr_ref am(pb.mk_at_most_k(es, 0), m);
totalizer* t = nullptr;
if (!m_totalizers.find(am, t)) {
m_trail.push_back(am);
t = alloc(totalizer, es);
m_totalizers.insert(am, t);
}
expr* at_least = t->at_least(bound + 1);
am = m.mk_not(at_least);
m_trail.push_back(am);
expr_ref_vector& clauses = t->clauses();
for (auto & clause : clauses) {
add(clause);
m_defs.push_back(clause);
}
clauses.reset();
auto& defs = t->defs();
for (auto & [v, d] : defs)
update_model(v, d);
defs.reset();
bound_info b(es, bound, weight);
m_bounds.insert(am, b);
return am;
}
expr* mk_atmost(expr_ref_vector const& es, unsigned bound, rational const& weight) {
if (m_use_totalizer)
return mk_atmost_tot(es, bound, weight);
pb_util pb(m);
expr_ref am(pb.mk_at_most_k(es, bound), m);
expr* r = nullptr;
@ -1024,6 +1062,7 @@ public:
m_enable_lns = p.enable_lns();
m_enable_core_rotate = p.enable_core_rotate();
m_lns_conflicts = p.lns_conflicts();
m_use_totalizer = p.rc2_totalizer();
if (m_c.num_objectives() > 1)
m_add_upper_bound_block = false;
}
@ -1040,6 +1079,9 @@ public:
m_unfold_upper = 0;
m_at_mostk.reset();
m_bounds.reset();
for (auto& [k,t] : m_totalizers)
dealloc(t);
m_totalizers.reset();
return l_true;
}
@ -1109,6 +1151,7 @@ opt::maxsmt_solver_base* opt::mk_rc2(
return alloc(maxcore, c, id, soft, maxcore::s_rc2);
}
opt::maxsmt_solver_base* opt::mk_rc2bin(
maxsat_context& c, unsigned id, vector<soft>& soft) {
return alloc(maxcore, c, id, soft, maxcore::s_primal_binary_rc2);

28
src/opt/opt_context.cpp
View file

@ -137,9 +137,6 @@ namespace opt {
m_model_fixed(),
m_objective_refs(m),
m_core(m),
m_enable_sat(false),
m_is_clausal(false),
m_pp_neat(false),
m_unknown("unknown")
{
params_ref p;
@ -196,6 +193,8 @@ namespace opt {
void context::add_hard_constraint(expr* f) {
if (m_calling_on_model) {
if (!m_incremental)
throw default_exception("Set opt.incremental = true to allow adding constraints during search");
get_solver().assert_expr(f);
for (auto const& [k, v] : m_maxsmts)
v->reset_upper();
@ -682,14 +681,11 @@ namespace opt {
void context::init_solver() {
setup_arith_solver();
m_sat_solver = nullptr;
m_opt_solver = alloc(opt_solver, m, m_params, *m_fm);
m_opt_solver->set_logic(m_logic);
m_solver = m_opt_solver.get();
m_opt_solver->ensure_pb();
//if (opt_params(m_params).priority() == symbol("pareto") ||
// (opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) {
//}
m_opt_solver->ensure_pb();
}
void context::setup_arith_solver() {
@ -708,6 +704,8 @@ namespace opt {
if (m_maxsat_engine != symbol("maxres") &&
m_maxsat_engine != symbol("rc2") &&
m_maxsat_engine != symbol("rc2tot") &&
m_maxsat_engine != symbol("rc2bin") &&
m_maxsat_engine != symbol("maxres-bin") &&
m_maxsat_engine != symbol("maxres-bin-delay") &&
m_maxsat_engine != symbol("pd-maxres") &&
@ -839,19 +837,14 @@ namespace opt {
}
goal_ref g(alloc(goal, m, true, !asms.empty()));
for (expr* fml : fmls) {
for (expr* fml : fmls)
g->assert_expr(fml);
}
for (expr * a : asms) {
for (expr * a : asms)
g->assert_expr(a, a);
}
tactic_ref tac0 =
and_then(mk_simplify_tactic(m, m_params),
mk_propagate_values_tactic(m),
mk_solve_eqs_tactic(m),
// NB: cannot ackermannize because max/min objectives would disappear
// mk_ackermannize_bv_tactic(m, m_params),
// NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m),
mk_simplify_tactic(m));
opt_params optp(m_params);
tactic_ref tac1, tac2, tac3, tac4;
@ -862,7 +855,7 @@ namespace opt {
m.linearize(core, deps);
has_dep |= !deps.empty();
}
if (optp.elim_01() && m_logic.is_null() && !has_dep) {
if (optp.elim_01() && m_logic.is_null() && !has_dep && !m_incremental) {
tac1 = mk_dt2bv_tactic(m);
tac2 = mk_lia2card_tactic(m);
tac3 = mk_eq2bv_tactic(m);
@ -1569,6 +1562,7 @@ namespace opt {
m_maxsat_engine = _p.maxsat_engine();
m_pp_neat = _p.pp_neat();
m_pp_wcnf = _p.pp_wcnf();
m_incremental = _p.incremental();
}
std::string context::to_string() {

11
src/opt/opt_context.h
View file

@ -194,11 +194,12 @@ namespace opt {
func_decl_ref_vector m_objective_refs;
expr_ref_vector m_core;
tactic_ref m_simplify;
bool m_enable_sat { true } ;
bool m_enable_sls { false };
bool m_is_clausal { false };
bool m_pp_neat { true };
bool m_pp_wcnf { false };
bool m_enable_sat = true;
bool m_enable_sls = false;
bool m_is_clausal = false;
bool m_pp_neat = false;
bool m_pp_wcnf = false;
bool m_incremental = false;
symbol m_maxsat_engine;
symbol m_logic;
svector<symbol> m_labels;

2
src/opt/opt_params.pyg
View file

@ -15,10 +15,12 @@ def_module_params('opt',
('enable_core_rotate', BOOL, False, 'enable core rotation to both sample cores and correction sets'),
('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
('elim_01', BOOL, True, 'eliminate 01 variables'),
('incremental', BOOL, False, 'set incremental mode. It disables pre-processing and enables adding constraints in model event handler'),
('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
('pp.wcnf', BOOL, False, 'print maxsat benchmark into wcnf format'),
('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
('rc2.totalizer', BOOL, True, 'use totalizer for rc2 encoding'),
('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
('maxres.max_num_cores', UINT, 200, 'maximal number of cores per round'),

119
src/opt/totalizer.cpp Normal file
View file

@ -0,0 +1,119 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
totalizer.cpp
Abstract:
Incremental totalizer for at least constraints
Author:
Nikolaj Bjorner (nbjorner) 2022-06-27
--*/
#include "opt/totalizer.h"
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include <iostream>
namespace opt {
void totalizer::ensure_bound(node* n, unsigned k) {
auto& lits = n->m_literals;
if (k > lits.size())
return;
auto* l = n->m_left;
auto* r = n->m_right;
if (l)
ensure_bound(l, k);
if (r)
ensure_bound(r, k);
expr_ref c(m), def(m);
expr_ref_vector ors(m), clause(m);
for (unsigned i = k; i > 0 && !lits.get(i - 1); --i) {
if (l->size() + r->size() < i) {
lits[i - 1] = m.mk_false();
continue;
}
c = m.mk_fresh_const("c", m.mk_bool_sort());
lits[i - 1] = c;
// >= 3
// r[2] => >= 3
// l[0] & r[1] => >= 3
// l[1] & r[0] => >= 3
// l[2] => >= 3
ors.reset();
for (unsigned j1 = 0; j1 <= i; ++j1) {
unsigned j2 = i - j1;
if (j1 > l->size())
continue;
if (j2 > r->size())
continue;
clause.reset();
if (0 < j1) {
expr* a = l->m_literals.get(j1 - 1);
clause.push_back(mk_not(m, a));
}
if (0 < j2) {
expr* b = r->m_literals.get(j2 - 1);
clause.push_back(mk_not(m, b));
}
if (clause.empty())
continue;
ors.push_back(mk_or(clause));
clause.push_back(c);
m_clauses.push_back(mk_or(clause));
}
def = mk_not(m, mk_and(ors));
m_defs.push_back(std::make_pair(c, def));
}
}
totalizer::totalizer(expr_ref_vector const& literals):
m(literals.m()),
m_literals(literals),
m_clauses(m) {
ptr_vector<node> trees;
for (expr* e : literals) {
expr_ref_vector ls(m);
ls.push_back(e);
trees.push_back(alloc(node, ls));
}
for (unsigned i = 0; i + 1 < trees.size(); i += 2) {
node* left = trees[i];
node* right = trees[i + 1];
expr_ref_vector ls(m);
ls.resize(left->size() + right->size());
node* n = alloc(node, ls);
n->m_left = left;
n->m_right = right;
trees.push_back(n);
}
m_root = trees.back();
}
totalizer::~totalizer() {
dealloc(m_root);
}
expr* totalizer::at_least(unsigned k) {
if (k == 0)
return m.mk_true();
if (m_root->size() < k)
return m.mk_false();
SASSERT(1 <= k && k <= m_root->size());
ensure_bound(m_root, k);
return m_root->m_literals.get(k - 1);
}
}

52
src/opt/totalizer.h Normal file
View file

@ -0,0 +1,52 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
totalizer.h
Abstract:
Incremental totalizer for at least constraints
Author:
Nikolaj Bjorner (nbjorner) 2022-06-27
--*/
#pragma once
#include "ast/ast.h"
namespace opt {
class totalizer {
struct node {
node* m_left = nullptr;
node* m_right = nullptr;
expr_ref_vector m_literals;
node(expr_ref_vector& l): m_literals(l) {}
~node() {
dealloc(m_left);
dealloc(m_right);
}
unsigned size() const { return m_literals.size(); }
};
ast_manager& m;
expr_ref_vector m_literals;
node* m_root = nullptr;
expr_ref_vector m_clauses;
vector<std::pair<expr_ref, expr_ref>> m_defs;
void ensure_bound(node* n, unsigned k);
public:
totalizer(expr_ref_vector const& literals);
~totalizer();
expr* at_least(unsigned k);
expr_ref_vector& clauses() { return m_clauses; }
vector<std::pair<expr_ref, expr_ref>>& defs() { return m_defs; }
};
}

1
src/params/rewriter_params.pyg
View file

@ -3,7 +3,6 @@ def_module_params('rewriter',
export=True,
params=(max_memory_param(),
max_steps_param(),
("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"),
("push_ite_arith", BOOL, False, "push if-then-else over arithmetic terms."),
("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."),
("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),

18
src/sat/sat_simplifier.cpp
View file

@ -1787,6 +1787,7 @@ namespace sat {
clause& c = it.curr();
if (!c.is_learned() && !c.was_removed()) {
r.push_back(clause_wrapper(c));
SASSERT(r.back().contains(l));
SASSERT(r.back().size() == c.size());
}
}
@ -1808,9 +1809,13 @@ namespace sat {
Return false if the result is a tautology
*/
bool simplifier::resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r) {
CTRACE("resolve_bug", !c1.contains(l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";);
CTRACE("resolve_bug", !c1.contains(l) || !c2.contains(~l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";);
if (m_visited.size() <= 2*s.num_vars())
m_visited.resize(2*s.num_vars(), false);
if (c1.was_removed())
return false;
if (c2.was_removed())
return false;
SASSERT(c1.contains(l));
SASSERT(c2.contains(~l));
bool res = true;
@ -1973,7 +1978,14 @@ namespace sat {
}
}
}
TRACE("sat_simplifier", tout << "eliminate " << v << ", before: " << before_clauses << " after: " << after_clauses << "\n";);
TRACE("sat_simplifier", tout << "eliminate " << v << ", before: " << before_clauses << " after: " << after_clauses << "\n";
tout << "pos\n";
for (auto & c : m_pos_cls)
tout << c << "\n";
tout << "neg\n";
for (auto & c : m_neg_cls)
tout << c << "\n";
);
m_elim_counter -= num_pos * num_neg + before_lits;
m_elim_counter -= num_pos * num_neg + before_lits;
@ -1988,6 +2000,8 @@ namespace sat {
m_elim_counter -= num_pos * num_neg + before_lits;
for (auto & c1 : m_pos_cls) {
if (c1.was_removed())
continue;
for (auto & c2 : m_neg_cls) {
m_new_cls.reset();
if (!resolve(c1, c2, pos_l, m_new_cls))

11
src/sat/sat_solver.cpp
View file

@ -2029,17 +2029,18 @@ namespace sat {
sort_watch_lits();
CASSERT("sat_simplify_bug", check_invariant());
m_probing();
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
m_asymm_branch(false);
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
if (m_ext) {
m_ext->clauses_modifed();
m_ext->simplify();
}
m_probing();
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
m_asymm_branch(false);
if (m_config.m_lookahead_simplify && !m_ext) {
lookahead lh(*this);
lh.simplify(true);

29
src/sat/smt/arith_axioms.cpp
View file

@ -128,6 +128,22 @@ namespace arith {
}
else {
expr_ref mone(a.mk_int(-1), m);
expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m);
literal eqz = mk_literal(m.mk_eq(q, zero));
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
literal mod_lt_q = mk_literal(a.mk_le(a.mk_sub(mod, abs_q), mone));
// q = 0 or p = (p mod q) + q * (p div q)
// q = 0 or (p mod q) >= 0
// q = 0 or (p mod q) < abs(q)
add_clause(eqz, eq);
add_clause(eqz, mod_ge_0);
add_clause(eqz, mod_lt_q);
#if 0
/*literal div_ge_0 = */ mk_literal(a.mk_ge(div, zero));
/*literal div_le_0 = */ mk_literal(a.mk_le(div, zero));
/*literal p_ge_0 = */ mk_literal(a.mk_ge(p, zero));
@ -139,6 +155,8 @@ namespace arith {
// q <= 0 or (p mod q) >= 0
// q <= 0 or (p mod q) < q
// q >= 0 or (p mod q) < -q
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
literal q_le_0 = mk_literal(a.mk_le(q, zero));
@ -148,6 +166,17 @@ namespace arith {
add_clause(q_le_0, mod_ge_0);
add_clause(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
add_clause(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
#endif
if (a.is_zero(p)) {
add_clause(eqz, mk_literal(m.mk_eq(mod, zero)));
add_clause(eqz, mk_literal(m.mk_eq(div, zero)));
}
else if (!a.is_numeral(q)) {
// (or (= y 0) (<= (* y (div x y)) x))
add_clause(eqz, mk_literal(a.mk_le(a.mk_mul(q, div), p)));
}
}
if (get_config().m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {

34
src/sat/smt/arith_internalize.cpp
View file

@ -69,23 +69,23 @@ namespace arith {
m_nla->push();
}
smt_params_helper prms(s().params());
m_nla->settings().run_order() = prms.arith_nl_order();
m_nla->settings().run_tangents() = prms.arith_nl_tangents();
m_nla->settings().run_horner() = prms.arith_nl_horner();
m_nla->settings().horner_subs_fixed() = prms.arith_nl_horner_subs_fixed();
m_nla->settings().horner_frequency() = prms.arith_nl_horner_frequency();
m_nla->settings().horner_row_length_limit() = prms.arith_nl_horner_row_length_limit();
m_nla->settings().run_grobner() = prms.arith_nl_grobner();
m_nla->settings().run_nra() = prms.arith_nl_nra();
m_nla->settings().grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed();
m_nla->settings().grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth();
m_nla->settings().grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth();
m_nla->settings().grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth();
m_nla->settings().grobner_max_simplified() = prms.arith_nl_grobner_max_simplified();
m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report();
m_nla->settings().grobner_quota() = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching() = false;
m_nla->settings().run_order = prms.arith_nl_order();
m_nla->settings().run_tangents = prms.arith_nl_tangents();
m_nla->settings().run_horner = prms.arith_nl_horner();
m_nla->settings().horner_subs_fixed = prms.arith_nl_horner_subs_fixed();
m_nla->settings().horner_frequency = prms.arith_nl_horner_frequency();
m_nla->settings().horner_row_length_limit = prms.arith_nl_horner_row_length_limit();
m_nla->settings().run_grobner = prms.arith_nl_grobner();
m_nla->settings().run_nra = prms.arith_nl_nra();
m_nla->settings().grobner_subs_fixed = prms.arith_nl_grobner_subs_fixed();
m_nla->settings().grobner_eqs_growth = prms.arith_nl_grobner_eqs_growth();
m_nla->settings().grobner_expr_size_growth = prms.arith_nl_grobner_expr_size_growth();
m_nla->settings().grobner_expr_degree_growth = prms.arith_nl_grobner_expr_degree_growth();
m_nla->settings().grobner_max_simplified = prms.arith_nl_grobner_max_simplified();
m_nla->settings().grobner_number_of_conflicts_to_report = prms.arith_nl_grobner_cnfl_to_report();
m_nla->settings().grobner_quota = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching = false;
}
}

1
src/sat/smt/bv_internalize.cpp
View file

@ -434,6 +434,7 @@ namespace bv {
SASSERT(bv.is_int2bv(n));
euf::enode* e = expr2enode(n);
mk_bits(e->get_th_var(get_id()));
get_var(e->get_arg(0));
assert_int2bv_axiom(n);
}

16
src/sat/smt/bv_solver.cpp
View file

@ -208,6 +208,22 @@ namespace bv {
if (is_bv(eq.v1())) {
m_find.merge(eq.v1(), eq.v2());
VERIFY(eq.is_eq());
return;
}
euf::enode* n1 = var2enode(eq.v1());
for (euf::enode* bv2int : euf::enode_class(n1)) {
if (!bv.is_bv2int(bv2int->get_expr()))
continue;
euf::enode* bv2int_arg = bv2int->get_arg(0);
for (euf::enode* p : euf::enode_parents(n1->get_root())) {
if (bv.is_int2bv(p->get_expr()) && p->get_sort() == bv2int_arg->get_sort() && p->get_root() != bv2int_arg->get_root()) {
euf::enode_pair_vector eqs;
eqs.push_back({ n1, p->get_arg(0) });
eqs.push_back({ n1, bv2int });
ctx.propagate(p, bv2int_arg, euf::th_explain::propagate(*this, eqs, p, bv2int_arg));
break;
}
}
}
}

38
src/sat/smt/dt_solver.cpp
View file

@ -506,7 +506,7 @@ namespace dt {
return m_nodes;
}
ptr_vector<euf::enode> const& solver::get_seq_args(enode* n) {
ptr_vector<euf::enode> const& solver::get_seq_args(enode* n, enode*& sibling) {
m_nodes.reset();
m_todo.reset();
auto add_todo = [&](enode* n) {
@ -515,9 +515,15 @@ namespace dt {
m_todo.push_back(n);
}
};
for (enode* sib : euf::enode_class(n))
add_todo(sib);
for (enode* sib : euf::enode_class(n)) {
if (m_sutil.str.is_concat_of_units(sib->get_expr())) {
add_todo(sib);
sibling = sib;
break;
}
}
for (unsigned i = 0; i < m_todo.size(); ++i) {
enode* n = m_todo[i];
@ -551,10 +557,10 @@ namespace dt {
// collect equalities on all children that may have been used.
bool found = false;
auto add = [&](enode* arg) {
if (arg->get_root() == child->get_root()) {
if (arg != child)
m_used_eqs.push_back(enode_pair(arg, child));
auto add = [&](enode* seq_arg) {
if (seq_arg->get_root() == child->get_root()) {
if (seq_arg != child)
m_used_eqs.push_back(enode_pair(seq_arg, child));
found = true;
}
};
@ -564,11 +570,14 @@ namespace dt {
if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s)))
for (enode* aarg : get_array_args(arg))
add(aarg);
}
sort* se;
if (m_sutil.is_seq(child->get_sort(), se) && dt.is_datatype(se)) {
for (enode* aarg : get_seq_args(child))
add(aarg);
sort* se;
if (m_sutil.is_seq(arg->get_sort(), se) && dt.is_datatype(se)) {
enode* sibling = nullptr;
for (enode* seq_arg : get_seq_args(arg, sibling))
add(seq_arg);
if (sibling && sibling != arg)
m_used_eqs.push_back(enode_pair(arg, sibling));
}
}
VERIFY(found);
@ -636,12 +645,13 @@ namespace dt {
// explore `arg` (with parent)
expr* earg = arg->get_expr();
sort* s = earg->get_sort(), *se;
enode* sibling;
if (dt.is_datatype(s)) {
m_parent.insert(arg->get_root(), parent);
oc_push_stack(arg);
}
else if (m_sutil.is_seq(s, se) && dt.is_datatype(se)) {
for (enode* sarg : get_seq_args(arg))
for (enode* sarg : get_seq_args(arg, sibling))
if (process_arg(sarg))
return true;
}

2
src/sat/smt/dt_solver.h
View file

@ -112,7 +112,7 @@ namespace dt {
void oc_push_stack(enode * n);
ptr_vector<enode> m_nodes, m_todo;
ptr_vector<enode> const& get_array_args(enode* n);
ptr_vector<enode> const& get_seq_args(enode* n);
ptr_vector<enode> const& get_seq_args(enode* n, enode*& sibling);
void pop_core(unsigned n) override;

116
src/sat/smt/pb_solver.cpp
View file

@ -34,7 +34,7 @@ namespace pb {
void solver::set_conflict(constraint& c, literal lit) {
m_stats.m_num_conflicts++;
TRACE("ba", display(tout, c, true); );
TRACE("pb", display(tout, c, true); );
if (!validate_conflict(c)) {
IF_VERBOSE(0, display(verbose_stream(), c, true));
UNREACHABLE();
@ -56,7 +56,7 @@ namespace pb {
default:
m_stats.m_num_propagations++;
m_num_propagations_since_pop++;
//TRACE("ba", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
//TRACE("pb", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
SASSERT(validate_unit_propagation(c, lit));
assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), c.cindex()));
break;
@ -69,7 +69,7 @@ namespace pb {
void solver::simplify(constraint& p) {
SASSERT(s().at_base_lvl());
if (p.lit() != sat::null_literal && value(p.lit()) == l_false) {
TRACE("ba", tout << "pb: flip sign " << p << "\n";);
TRACE("pb", tout << "pb: flip sign " << p << "\n";);
IF_VERBOSE(2, verbose_stream() << "sign is flipped " << p << "\n";);
return;
}
@ -280,7 +280,7 @@ namespace pb {
*/
lbool solver::add_assign(pbc& p, literal alit) {
BADLOG(display(verbose_stream() << "assign: " << alit << " watch: " << p.num_watch() << " size: " << p.size(), p, true));
TRACE("ba", display(tout << "assign: " << alit << "\n", p, true););
TRACE("pb", display(tout << "assign: " << alit << "\n", p, true););
SASSERT(!inconsistent());
unsigned sz = p.size();
unsigned bound = p.k();
@ -290,6 +290,7 @@ namespace pb {
SASSERT(p.lit() == sat::null_literal || value(p.lit()) == l_true);
SASSERT(num_watch <= sz);
SASSERT(num_watch > 0);
SASSERT(validate_watch(p, sat::null_literal));
unsigned index = 0;
m_a_max = 0;
m_pb_undef.reset();
@ -311,8 +312,6 @@ namespace pb {
return l_undef;
}
SASSERT(validate_watch(p, sat::null_literal));
// SASSERT(validate_watch(p, sat::null_literal));
SASSERT(index < num_watch);
unsigned index1 = index + 1;
@ -349,7 +348,7 @@ namespace pb {
SASSERT(validate_watch(p, sat::null_literal));
BADLOG(display(verbose_stream() << "conflict: " << alit << " watch: " << p.num_watch() << " size: " << p.size(), p, true));
SASSERT(bound <= slack);
TRACE("ba", tout << "conflict " << alit << "\n";);
TRACE("pb", tout << "conflict " << alit << "\n";);
set_conflict(p, alit);
return l_false;
}
@ -366,13 +365,14 @@ namespace pb {
p.swap(num_watch, index);
//
// slack >= bound, but slack - w(l) < bound
// l must be true.
//
if (slack < bound + m_a_max) {
BADLOG(verbose_stream() << "slack " << slack << " " << bound << " " << m_a_max << "\n";);
TRACE("ba", tout << p << "\n"; for(auto j : m_pb_undef) tout << j << " "; tout << "\n";);
TRACE("pb", tout << p << "\n"; for(auto j : m_pb_undef) tout << j << " "; tout << "\n";);
for (unsigned index1 : m_pb_undef) {
if (index1 == num_watch) {
index1 = index;
@ -389,7 +389,7 @@ namespace pb {
SASSERT(validate_watch(p, alit)); // except that alit is still watched.
TRACE("ba", display(tout << "assign: " << alit << "\n", p, true););
TRACE("pb", display(tout << "assign: " << alit << "\n", p, true););
BADLOG(verbose_stream() << "unwatch " << alit << " watch: " << p.num_watch() << " size: " << p.size() << " slack: " << p.slack() << " " << inconsistent() << "\n");
@ -547,7 +547,7 @@ namespace pb {
literal l = literal(v, c1 < 0);
c1 = std::abs(c1);
unsigned c = static_cast<unsigned>(c1);
// TRACE("ba", tout << l << " " << c << "\n";);
// TRACE("pb", tout << l << " " << c << "\n";);
m_overflow |= c != c1;
return wliteral(c, l);
}
@ -596,12 +596,13 @@ namespace pb {
s().reset_mark(v);
--m_num_marks;
}
if (idx == 0 && !_debug_conflict) {
if (idx == 0 && !_debug_conflict && m_num_marks > 0) {
_debug_conflict = true;
_debug_var2position.reserve(s().num_vars());
for (unsigned i = 0; i < lits.size(); ++i) {
_debug_var2position[lits[i].var()] = i;
}
IF_VERBOSE(0, verbose_stream() << "num marks: " << m_num_marks << "\n");
IF_VERBOSE(0,
active2pb(m_A);
uint64_t c = 0;
@ -617,20 +618,19 @@ namespace pb {
}
}
m_num_marks = 0;
resolve_conflict();
resolve_conflict();
exit(0);
}
--idx;
}
}
lbool solver::resolve_conflict() {
if (0 == m_num_propagations_since_pop) {
if (0 == m_num_propagations_since_pop)
return l_undef;
}
if (s().m_config.m_pb_resolve == sat::PB_ROUNDING) {
if (s().m_config.m_pb_resolve == sat::PB_ROUNDING)
return resolve_conflict_rs();
}
m_overflow = false;
reset_coeffs();
@ -638,7 +638,7 @@ namespace pb {
m_bound = 0;
literal consequent = s().m_not_l;
sat::justification js = s().m_conflict;
TRACE("ba", tout << consequent << " " << js << "\n";);
TRACE("pb", tout << consequent << " " << js << "\n";);
bool unique_max;
m_conflict_lvl = s().get_max_lvl(consequent, js, unique_max);
if (m_conflict_lvl == 0) {
@ -667,7 +667,7 @@ namespace pb {
}
DEBUG_CODE(TRACE("sat_verbose", display(tout, m_A);););
TRACE("ba", tout << "process consequent: " << consequent << " : "; s().display_justification(tout, js) << "\n";);
TRACE("pb", tout << "process consequent: " << consequent << " : "; s().display_justification(tout, js) << "\n";);
SASSERT(offset > 0);
DEBUG_CODE(justification2pb(js, consequent, offset, m_B););
@ -741,7 +741,7 @@ namespace pb {
inc_bound(offset);
inc_coeff(consequent, offset);
get_antecedents(consequent, p, m_lemma);
TRACE("ba", display(tout, p, true); tout << m_lemma << "\n";);
TRACE("pb", display(tout, p, true); tout << m_lemma << "\n";);
if (_debug_conflict) {
verbose_stream() << consequent << " ";
verbose_stream() << "antecedents: " << m_lemma << "\n";
@ -766,7 +766,7 @@ namespace pb {
active2pb(m_C);
VERIFY(validate_resolvent());
m_A = m_C;
TRACE("ba", display(tout << "conflict: ", m_A);););
TRACE("pb", display(tout << "conflict: ", m_A);););
cut();
@ -887,7 +887,7 @@ namespace pb {
}
}
ineq.divide(c);
TRACE("ba", display(tout << "var: " << v << " " << c << ": ", ineq, true););
TRACE("pb", display(tout << "var: " << v << " " << c << ": ", ineq, true););
}
void solver::round_to_one(bool_var w) {
@ -905,7 +905,7 @@ namespace pb {
SASSERT(validate_lemma());
divide(c);
SASSERT(validate_lemma());
TRACE("ba", active2pb(m_B); display(tout, m_B, true););
TRACE("pb", active2pb(m_B); display(tout, m_B, true););
}
void solver::divide(unsigned c) {
@ -935,14 +935,14 @@ namespace pb {
}
void solver::resolve_with(ineq const& ineq) {
TRACE("ba", display(tout, ineq, true););
TRACE("pb", display(tout, ineq, true););
inc_bound(ineq.m_k);
TRACE("ba", tout << "bound: " << m_bound << "\n";);
TRACE("pb", tout << "bound: " << m_bound << "\n";);
for (unsigned i = ineq.size(); i-- > 0; ) {
literal l = ineq.lit(i);
inc_coeff(l, static_cast<unsigned>(ineq.coeff(i)));
TRACE("ba", tout << "bound: " << m_bound << " lit: " << l << " coeff: " << ineq.coeff(i) << "\n";);
TRACE("pb", tout << "bound: " << m_bound << " lit: " << l << " coeff: " << ineq.coeff(i) << "\n";);
}
}
@ -995,11 +995,11 @@ namespace pb {
consequent.neg();
process_antecedent(consequent, 1);
}
TRACE("ba", tout << consequent << " " << js << "\n";);
TRACE("pb", tout << consequent << " " << js << "\n";);
unsigned idx = s().m_trail.size() - 1;
do {
TRACE("ba", s().display_justification(tout << "process consequent: " << consequent << " : ", js) << "\n";
TRACE("pb", s().display_justification(tout << "process consequent: " << consequent << " : ", js) << "\n";
if (consequent != sat::null_literal) { active2pb(m_A); display(tout, m_A, true); }
);
@ -1069,7 +1069,7 @@ namespace pb {
}
else {
SASSERT(k > c);
TRACE("ba", tout << "visited: " << l << "\n";);
TRACE("pb", tout << "visited: " << l << "\n";);
k -= c;
}
}
@ -1118,7 +1118,7 @@ namespace pb {
}
}
if (idx == 0) {
TRACE("ba", tout << "there is no consequent\n";);
TRACE("pb", tout << "there is no consequent\n";);
goto bail_out;
}
--idx;
@ -1131,7 +1131,7 @@ namespace pb {
js = s().m_justification[v];
}
while (m_num_marks > 0 && !m_overflow);
TRACE("ba", active2pb(m_A); display(tout, m_A, true););
TRACE("pb", active2pb(m_A); display(tout, m_A, true););
// TBD: check if this is useful
if (!m_overflow && consequent != sat::null_literal) {
@ -1143,7 +1143,7 @@ namespace pb {
}
bail_out:
TRACE("ba", tout << "bail " << m_overflow << "\n";);
TRACE("pb", tout << "bail " << m_overflow << "\n";);
if (m_overflow) {
++m_stats.m_num_overflow;
m_overflow = false;
@ -1199,23 +1199,23 @@ namespace pb {
}
}
if (slack >= 0) {
TRACE("ba", tout << "slack is non-negative\n";);
TRACE("pb", tout << "slack is non-negative\n";);
IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";);
return false;
}
if (m_overflow) {
TRACE("ba", tout << "overflow\n";);
TRACE("pb", tout << "overflow\n";);
return false;
}
if (m_lemma[0] == sat::null_literal) {
if (m_lemma.size() == 1) {
s().set_conflict(sat::justification(0));
}
TRACE("ba", tout << "no asserting literal\n";);
TRACE("pb", tout << "no asserting literal\n";);
return false;
}
TRACE("ba", tout << m_lemma << "\n";);
TRACE("pb", tout << m_lemma << "\n";);
if (get_config().m_drat && m_solver) {
s().m_drat.add(m_lemma, sat::status::th(true, get_id()));
@ -1224,7 +1224,7 @@ namespace pb {
s().m_lemma.reset();
s().m_lemma.append(m_lemma);
for (unsigned i = 1; i < m_lemma.size(); ++i) {
CTRACE("ba", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";);
CTRACE("pb", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";);
s().mark(m_lemma[i].var());
}
return true;
@ -1346,11 +1346,11 @@ namespace pb {
}
solver::solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id)
: euf::th_solver(m, symbol("ba"), id),
: euf::th_solver(m, symbol("pb"), id),
si(si), m_pb(m),
m_lookahead(nullptr),
m_constraint_id(0), m_ba(*this), m_sort(m_ba) {
TRACE("ba", tout << this << "\n";);
TRACE("pb", tout << this << "\n";);
m_num_propagations_since_pop = 0;
}
@ -1418,6 +1418,8 @@ namespace pb {
}
else if (lit == sat::null_literal) {
init_watch(*c);
if (c->is_pb())
validate_watch(c->to_pb(), sat::null_literal);
}
else {
if (m_solver) m_solver->set_external(lit.var());
@ -1569,7 +1571,7 @@ namespace pb {
}
void solver::get_antecedents(literal l, pbc const& p, literal_vector& r) {
TRACE("ba", display(tout << l << " level: " << s().scope_lvl() << " ", p, true););
TRACE("pb", display(tout << l << " level: " << s().scope_lvl() << " ", p, true););
SASSERT(p.lit() == sat::null_literal || value(p.lit()) == l_true);
if (p.lit() != sat::null_literal) {
@ -1621,7 +1623,7 @@ namespace pb {
if (j < p.num_watch()) {
j = p.num_watch();
}
CTRACE("ba", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true););
CTRACE("pb", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true););
if (_debug_conflict) {
IF_VERBOSE(0, verbose_stream() << "coeff " << coeff << "\n";);
@ -1672,7 +1674,7 @@ namespace pb {
for (unsigned i = 0; !found && i < c.k(); ++i) {
found = c[i] == l;
}
CTRACE("ba",!found, s().display(tout << l << ":" << c << "\n"););
CTRACE("pb",!found, s().display(tout << l << ":" << c << "\n"););
SASSERT(found););
VERIFY(c.lit() == sat::null_literal || value(c.lit()) != l_false);
@ -1712,7 +1714,7 @@ namespace pb {
}
void solver::remove_constraint(constraint& c, char const* reason) {
TRACE("ba", display(tout << "remove ", c, true) << " " << reason << "\n";);
TRACE("pb", display(tout << "remove ", c, true) << " " << reason << "\n";);
IF_VERBOSE(21, display(verbose_stream() << "remove " << reason << " ", c, true););
c.nullify_tracking_literal(*this);
clear_watch(c);
@ -1886,7 +1888,7 @@ namespace pb {
}
void solver::gc_half(char const* st_name) {
TRACE("ba", tout << "gc\n";);
TRACE("pb", tout << "gc\n";);
unsigned sz = m_learned.size();
unsigned new_sz = sz/2;
unsigned removed = 0;
@ -1933,7 +1935,7 @@ namespace pb {
// literal is assigned to false.
unsigned sz = c.size();
unsigned bound = c.k();
TRACE("ba", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << " " << c << "\n";);
TRACE("pb", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << " " << c << "\n";);
SASSERT(0 < bound && bound <= sz);
if (bound == sz) {
@ -1971,7 +1973,7 @@ namespace pb {
// conflict
if (bound != index && value(c[bound]) == l_false) {
TRACE("ba", tout << "conflict " << c[bound] << " " << alit << "\n";);
TRACE("pb", tout << "conflict " << c[bound] << " " << alit << "\n";);
if (c.lit() != sat::null_literal && value(c.lit()) == l_undef) {
if (index + 1 < bound) c.swap(index, bound - 1);
assign(c, ~c.lit());
@ -1985,7 +1987,7 @@ namespace pb {
c.swap(index, bound);
}
// TRACE("ba", tout << "no swap " << index << " " << alit << "\n";);
// TRACE("pb", tout << "no swap " << index << " " << alit << "\n";);
// there are no literals to swap with,
// prepare for unit propagation by swapping the false literal into
// position bound. Then literals in positions 0..bound-1 have to be
@ -2351,7 +2353,7 @@ namespace pb {
}
if (!all_units) {
TRACE("ba", tout << "replacing by pb: " << c << "\n";);
TRACE("pb", tout << "replacing by pb: " << c << "\n";);
m_wlits.reset();
for (unsigned i = 0; i < sz; ++i) {
m_wlits.push_back(wliteral(coeffs[i], c[i]));
@ -2914,13 +2916,13 @@ namespace pb {
SASSERT(&c1 != &c2);
if (subsumes(c1, c2, slit)) {
if (slit.empty()) {
TRACE("ba", tout << "subsume cardinality\n" << c1 << "\n" << c2 << "\n";);
TRACE("pb", tout << "subsume cardinality\n" << c1 << "\n" << c2 << "\n";);
remove_constraint(c2, "subsumed");
++m_stats.m_num_pb_subsumes;
set_non_learned(c1);
}
else {
TRACE("ba", tout << "self subsume cardinality\n";);
TRACE("pb", tout << "self subsume cardinality\n";);
IF_VERBOSE(11,
verbose_stream() << "self-subsume cardinality\n";
verbose_stream() << c1 << "\n";
@ -2952,7 +2954,7 @@ namespace pb {
// self-subsumption is TBD
}
else {
TRACE("ba", tout << "remove\n" << c1 << "\n" << c2 << "\n";);
TRACE("pb", tout << "remove\n" << c1 << "\n" << c2 << "\n";);
removed_clauses.push_back(&c2);
++m_stats.m_num_clause_subsumes;
set_non_learned(c1);
@ -3284,7 +3286,7 @@ namespace pb {
val += wl.first;
}
}
CTRACE("ba", val >= 0, active2pb(m_A); display(tout, m_A, true););
CTRACE("pb", val >= 0, active2pb(m_A); display(tout, m_A, true););
return val < 0;
}
@ -3297,7 +3299,7 @@ namespace pb {
if (!is_false(wl.second))
k += wl.first;
}
CTRACE("ba", k > 0, display(tout, ineq, true););
CTRACE("pb", k > 0, display(tout, ineq, true););
return k <= 0;
}
@ -3356,7 +3358,7 @@ namespace pb {
return nullptr;
}
constraint* c = add_pb_ge(sat::null_literal, m_wlits, m_bound, true);
TRACE("ba", if (c) display(tout, *c, true););
TRACE("pb", if (c) display(tout, *c, true););
++m_stats.m_num_lemmas;
return c;
}
@ -3587,7 +3589,7 @@ namespace pb {
s0.assign_scoped(l2);
s0.assign_scoped(l3);
lbool is_sat = s0.check();
TRACE("ba", s0.display(tout << "trying sat encoding"););
TRACE("pb", s0.display(tout << "trying sat encoding"););
if (is_sat == l_false) return true;
IF_VERBOSE(0,
@ -3698,11 +3700,11 @@ namespace pb {
bool solver::validate_conflict(literal_vector const& lits, ineq& p) {
for (literal l : lits) {
if (value(l) != l_false) {
TRACE("ba", tout << "literal " << l << " is not false\n";);
TRACE("pb", tout << "literal " << l << " is not false\n";);
return false;
}
if (!p.contains(l)) {
TRACE("ba", tout << "lemma contains literal " << l << " not in inequality\n";);
TRACE("pb", tout << "lemma contains literal " << l << " not in inequality\n";);
return false;
}
}
@ -3713,7 +3715,7 @@ namespace pb {
value += coeff;
}
}
CTRACE("ba", value >= p.m_k, tout << "slack: " << value << " bound " << p.m_k << "\n";
CTRACE("pb", value >= p.m_k, tout << "slack: " << value << " bound " << p.m_k << "\n";
display(tout, p);
tout << lits << "\n";);
return value < p.m_k;

2
src/sat/smt/recfun_solver.h
View file

@ -108,7 +108,7 @@ namespace recfun {
bool is_shared(euf::theory_var v) const override { return true; }
void init_search() override {}
bool should_research(sat::literal_vector const& core) override;
bool is_beta_redex(euf::enode* p, euf::enode* n) const;
bool is_beta_redex(euf::enode* p, euf::enode* n) const override;
void add_assumptions(sat::literal_set& assumptions) override;
bool tracking_assumptions() override { return true; }
};

4
src/sat/smt/sat_th.cpp
View file

@ -270,6 +270,10 @@ namespace euf {
return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), sat::null_literal, x, y, pma);
}
th_explain* th_explain::propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma) {
return mk(th, 0, nullptr, eqs.size(), eqs.data(), sat::null_literal, x, y, pma);
}
th_explain* th_explain::propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) {
return mk(th, 1, &lit, 0, nullptr, sat::null_literal, x, y);
}

1
src/sat/smt/sat_th.h
View file

@ -241,6 +241,7 @@ namespace euf {
static th_explain* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
static th_explain* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y);
static th_explain* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
static th_explain* propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma = nullptr);
static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, sat::proof_hint const* pma = nullptr);
static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma = nullptr);

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

@ -71,7 +71,7 @@ def_module_params(module_name='smt',
('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),

5
src/smt/smt_internalizer.cpp
View file

@ -1429,7 +1429,10 @@ namespace smt {
inc_ref(l2);
m_watches[(~l1).index()].insert_literal(l2);
m_watches[(~l2).index()].insert_literal(l1);
if (get_assignment(l2) == l_false) {
if (get_assignment(l1) == l_false) {
assign(l2, b_justification(~l1));
}
else if (get_assignment(l2) == l_false) {
assign(l1, b_justification(~l2));
}
m_clause_proof.add(l1, l2, k, j);

Some files were not shown because too many files have changed in this diff Show more