mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'master' into sls

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-11 09:56:46 -07:00
commit 5d9d134151
406 changed files with 17512 additions and 8359 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ackermannization/ackr_bound_probe.cpp
View file

@ -60,8 +60,6 @@ class ackr_bound_probe : public probe {
};
public:
ackr_bound_probe() {}
result operator()(goal const & g) override {
proc p(g.m());
unsigned sz = g.size();

2
src/ackermannization/lackr_model_constructor.cpp
View file

@ -41,8 +41,6 @@ public:
, m_ackr_helper(m)
{}
~imp() { }
//
// Returns true iff model was successfully constructed.
// Conflicts are saved as a side effect.

17
src/api/api_opt.cpp
View file

@ -459,6 +459,21 @@ extern "C" {
Z3_CATCH;
}
void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast var, Z3_ast value) {
Z3_TRY;
LOG_Z3_optimize_set_initial_value(c, o, var, value);
RESET_ERROR_CODE();
if (to_expr(var)->get_sort() != to_expr(value)->get_sort()) {
SET_ERROR_CODE(Z3_INVALID_USAGE, "variable and value should have same sort");
return;
}
ast_manager& m = mk_c(c)->m();
if (!m.is_value(to_expr(value))) {
SET_ERROR_CODE(Z3_INVALID_USAGE, "a proper value was not supplied");
return;
}
to_optimize_ptr(o)->initialize_value(to_expr(var), to_expr(value));
Z3_CATCH;
}
};

18
src/api/api_solver.cpp
View file

@ -1143,5 +1143,23 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast var, Z3_ast value) {
Z3_TRY;
LOG_Z3_solver_set_initial_value(c, s, var, value);
RESET_ERROR_CODE();
if (to_expr(var)->get_sort() != to_expr(value)->get_sort()) {
SET_ERROR_CODE(Z3_INVALID_USAGE, "variable and value should have same sort");
return;
}
ast_manager& m = mk_c(c)->m();
if (!m.is_value(to_expr(value))) {
SET_ERROR_CODE(Z3_INVALID_USAGE, "a proper value was not supplied");
return;
}
to_solver_ref(s)->user_propagate_initialize_value(to_expr(var), to_expr(value));
Z3_CATCH;
}
};

30
src/api/c++/z3++.h
View file

@ -1603,10 +1603,10 @@ namespace z3 {
unsigned i;
public:
iterator(expr& e, unsigned i): e(e), i(i) {}
bool operator==(iterator const& other) noexcept {
bool operator==(iterator const& other) const noexcept {
return i == other.i;
}
bool operator!=(iterator const& other) noexcept {
bool operator!=(iterator const& other) const noexcept {
return i != other.i;
}
expr operator*() const { return e.arg(i); }
@ -2865,6 +2865,17 @@ namespace z3 {
check_error();
return result;
}
void set_initial_value(expr const& var, expr const& value) {
Z3_solver_set_initial_value(ctx(), m_solver, var, value);
check_error();
}
void set_initial_value(expr const& var, int i) {
set_initial_value(var, ctx().num_val(i, var.get_sort()));
}
void set_initial_value(expr const& var, bool b) {
set_initial_value(var, ctx().bool_val(b));
}
expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
friend std::ostream & operator<<(std::ostream & out, solver const & s);
@ -2946,10 +2957,10 @@ namespace z3 {
expr_vector const * operator->() const { return &(operator*()); }
expr_vector const& operator*() const noexcept { return m_cube; }
bool operator==(cube_iterator const& other) noexcept {
bool operator==(cube_iterator const& other) const noexcept {
return other.m_end == m_end;
};
bool operator!=(cube_iterator const& other) noexcept {
bool operator!=(cube_iterator const& other) const noexcept {
return other.m_end != m_end;
};
@ -3330,6 +3341,17 @@ namespace z3 {
handle add(expr const& e, unsigned weight) {
return add_soft(e, weight);
}
void set_initial_value(expr const& var, expr const& value) {
Z3_optimize_set_initial_value(ctx(), m_opt, var, value);
check_error();
}
void set_initial_value(expr const& var, int i) {
set_initial_value(var, ctx().num_val(i, var.get_sort()));
}
void set_initial_value(expr const& var, bool b) {
set_initial_value(var, ctx().bool_val(b));
}
handle maximize(expr const& e) {
return handle(Z3_optimize_maximize(ctx(), m_opt, e));
}

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

File diff suppressed because it is too large Load diff

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

@ -29,7 +29,7 @@
"clean": "rimraf build 'src/**/*.__GENERATED__.*'",
"lint": "prettier -c '{./,src/,scripts/,examples/}**/*.{js,ts}'",
"format": "prettier --write '{./,src/,scripts/}**/*.{js,ts}'",
"test": "jest",
"test": "node --expose-gc ./node_modules/.bin/jest",
"docs": "typedoc",
"check-engine": "check-engine"
},

2
src/api/js/scripts/build-wasm.ts
View file

@ -69,7 +69,7 @@ const fns = JSON.stringify(exportedFuncs());
const methods = '["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]';
const libz3a = path.normalize('../../../build/libz3.a');
spawnSync(
`emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=1GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`,
`emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=2GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`,
);
fs.rmSync(ccWrapperPath);

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

@ -4,6 +4,12 @@ import { init, killThreads } from '../jest';
import { Arith, Bool, Model, Quantifier, Z3AssertionError, Z3HighLevel, AstVector } from './types';
import { expectType } from 'ts-expect';
// this should not be necessary but there may be a Jest bug
// https://github.com/jestjs/jest/issues/7874
afterEach(() => {
global.gc && global.gc();
});
/**
* Generate all possible solutions from given assumptions.
*
@ -355,6 +361,7 @@ describe('high-level', () => {
});
});
describe('bitvectors', () => {
it('can do simple proofs', async () => {
const { BitVec, Concat, Implies, isBitVecVal } = api.Context('main');
@ -373,7 +380,7 @@ describe('high-level', () => {
const y = BitVec.const('y', 32);
await prove(Implies(Concat(x, y).eq(Concat(y, x)), x.eq(y)));
});
}, 10_000 /* timeout ms */);
it('finds x and y such that: x ^ y - 103 == x * y', async () => {
const { BitVec, isBitVecVal } = api.Context('main');
@ -393,6 +400,7 @@ describe('high-level', () => {
});
});
describe('arrays', () => {
it('Example 1', async () => {
const Z3 = api.Context('main');
@ -447,7 +455,7 @@ describe('high-level', () => {
await prove(Eq(arr2.select(0), FIVE_VAL));
await prove(Not(Eq(arr2.select(0), BitVec.val(6, 256))));
await prove(Eq(arr2.store(idx, val).select(idx), constArr.store(idx, val).select(idx)));
});
}, 10_000 /* timeout ms */);
it('Finds arrays that differ but that sum to the same', async () => {
const Z3 = api.Context('main');

4
src/api/julia/README.md
View file

@ -1,6 +1,8 @@
# Julia bindings
The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) provides and interface to Z3 by exposing its C++ API via [CxxWrap.jl](https://github.com/JuliaInterop/CxxWrap.jl). The bindings therefore consist of a [C++ part](z3jl.cpp) and a [Julia part](https://github.com/ahumenberger/Z3.jl). The C++ part defines the Z3 types/methods which are exposed. The resulting library is loaded in the Julia part via CxxWrap.jl which creates the corresponding Julia types/methods.
The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) provides and interface to Z3 by exposing its C API.
A previous version exposed the C++ API via [CxxWrap.jl](https://github.com/JuliaInterop/CxxWrap.jl). The bindings therefore consisted of a [C++ part](z3jl.cpp) and a [Julia part](https://github.com/ahumenberger/Z3.jl). The C++ part defines the Z3 types/methods which are exposed. The resulting library is loaded in the Julia part via CxxWrap.jl which creates the corresponding Julia types/methods.
## Building the C++ part

2
src/api/python/pyproject.toml
View file

@ -1,3 +1,3 @@
[build-system]
requires = ["setuptools>=46.4.0", "wheel", "cmake"]
requires = ["setuptools>=70", "cmake"]
build-backend = "setuptools.build_meta"

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

@ -7,18 +7,17 @@ import multiprocessing
import re
import glob
from setuptools import setup
from distutils.util import get_platform
from distutils.errors import LibError
from distutils.command.build import build as _build
from distutils.command.sdist import sdist as _sdist
from distutils.command.clean import clean as _clean
from setuptools.command.build import build as _build
from setuptools.command.sdist import sdist as _sdist
from setuptools.command.bdist_wheel import bdist_wheel as _bdist_wheel
from setuptools.command.develop import develop as _develop
from setuptools.command.bdist_egg import bdist_egg as _bdist_egg
class LibError(Exception):
pass
build_env = dict(os.environ)
build_env['PYTHON'] = sys.executable
build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -std=c++17"
build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -std=c++20"
# determine where we're building and where sources are
ROOT_DIR = os.path.abspath(os.path.dirname(__file__))
@ -33,6 +32,8 @@ if RELEASE_DIR is None:
HEADER_DIRS = [os.path.join(SRC_DIR, 'src', 'api'), os.path.join(SRC_DIR, 'src', 'api', 'c++')]
RELEASE_METADATA = None
BUILD_PLATFORM = sys.platform
BUILD_ARCH = os.environ.get("Z3_CROSS_COMPILING", platform.machine())
BUILD_OS_VERSION = platform.mac_ver()[0].split(".")
else:
if not os.path.isdir(RELEASE_DIR):
raise Exception("RELEASE_DIR (%s) is not a directory!" % RELEASE_DIR)
@ -43,6 +44,11 @@ else:
raise Exception("RELEASE_DIR (%s) must be in the format z3-version-arch-os[-osversion] so we can extract metadata from it. Sorry!" % RELEASE_DIR)
RELEASE_METADATA.pop(0)
BUILD_PLATFORM = RELEASE_METADATA[2]
BUILD_ARCH = RELEASE_METADATA[1]
if len(RELEASE_METADATA) == 4:
BUILD_OS_VERSION = RELEASE_METADATA[3].split(".")
else:
BUILD_OS_VERSION = None
# determine where destinations are
LIBS_DIR = os.path.join(ROOT_DIR, 'z3', 'lib')
@ -50,7 +56,7 @@ HEADERS_DIR = os.path.join(ROOT_DIR, 'z3', 'include')
BINS_DIR = os.path.join(ROOT_DIR, 'bin')
# determine platform-specific filenames
if BUILD_PLATFORM in ('darwin', 'osx'):
if BUILD_PLATFORM in ('sequoia','darwin', 'osx'):
LIBRARY_FILE = "libz3.dylib"
EXECUTABLE_FILE = "z3"
elif BUILD_PLATFORM in ('win32', 'cygwin', 'win'):
@ -193,7 +199,7 @@ def _copy_bins():
link_name = None
if BUILD_PLATFORM in ('win32', 'cygwin', 'win'):
pass # TODO: When windows VMs work on M1, fill this in
elif BUILD_PLATFORM in ('darwin', 'osx'):
elif BUILD_PLATFORM in ('sequoia', 'darwin', 'osx'):
split = LIBRARY_FILE.split('.')
link_name = split[0] + '.' + major_minor + '.' + split[1]
else:
@ -238,111 +244,41 @@ class develop(_develop):
self.execute(_copy_bins, (), msg="Copying binaries")
_develop.run(self)
class bdist_egg(_bdist_egg):
def run(self):
self.run_command('build')
_bdist_egg.run(self)
class sdist(_sdist):
def run(self):
self.execute(_clean_bins, (), msg="Cleaning binary files and headers")
self.execute(_copy_sources, (), msg="Copying source files")
_sdist.run(self)
class clean(_clean):
def run(self):
self.execute(_clean_bins, (), msg="Cleaning binary files and headers")
self.execute(_clean_native_build, (), msg="Cleaning native build")
_clean.run(self)
class bdist_wheel(_bdist_wheel):
def finalize_options(self):
if BUILD_ARCH is not None and BUILD_PLATFORM is not None:
os_version_tag = '_'.join(BUILD_OS_VERSION[:2]) if BUILD_OS_VERSION is not None else 'xxxxxx'
TAGS = {
# linux tags cannot be deployed - they must be auditwheel'd to pick the right compatibility tag based on imported libc symbol versions
("linux", "x86_64"): "linux_x86_64",
("linux", "aarch64"): "linux_aarch64",
# windows arm64 is not supported by pypi yet
("win", "x64"): "win_amd64",
("win", "x86"): "win32",
("osx", "x64"): f"macosx_{os_version_tag}_x86_64",
("osx", "arm64"): f"macosx_{os_version_tag}_arm64",
("darwin", "x86_64"): f"macosx_{os_version_tag}_x86_64",
("darwin", "x64"): f"macosx_{os_version_tag}_x86_64",
("darwin", "arm64"): f"macosx_{os_version_tag}_arm64",
("sequoia", "x64"): f"macosx_{os_version_tag}_x86_64",
("sequoia", "x86_64"): f"macosx_{os_version_tag}_x86_64",
("sequoia", "arm64"): f"macosx_{os_version_tag}_arm64",
} # type: dict[tuple[str, str], str]
self.plat_name = TAGS[(BUILD_PLATFORM, BUILD_ARCH)]
return super().finalize_options()
# the build directory needs to exist
#try: os.makedirs(os.path.join(ROOT_DIR, 'build'))
#except OSError: pass
# platform.freedesktop_os_release was added in 3.10
os_id = ''
if hasattr(platform, 'freedesktop_os_release'):
try:
osr = platform.freedesktop_os_release()
print(osr)
os_id = osr['ID']
except OSError:
pass
if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
if RELEASE_DIR is None:
name = get_platform()
if 'linux' in name:
# linux_* platform tags are disallowed because the python ecosystem is fubar
# linux builds should be built in the centos 5 vm for maximum compatibility
# see https://github.com/pypa/manylinux
# see also https://github.com/angr/angr-dev/blob/master/admin/bdist.py
plat_name = 'manylinux_2_28_' + platform.machine()
elif 'mingw' in name:
if platform.architecture()[0] == '64bit':
plat_name = 'win_amd64'
else:
plat_name ='win32'
else:
# https://www.python.org/dev/peps/pep-0425/
plat_name = name.replace('.', '_').replace('-', '_')
else:
# extract the architecture of the release from the directory name
arch = RELEASE_METADATA[1]
distos = RELEASE_METADATA[2]
if distos in ('debian', 'ubuntu'):
raise Exception(
"Linux binary distributions must be built on centos to conform to PEP 513 or alpine if targeting musl"
)
elif distos == 'glibc':
if arch == 'x64':
plat_name = 'manylinux_2_28_x86_64'
elif arch == 'arm64' or arch == 'aarch64':
# context on why are we match on arm64
# but use aarch64 on the plat_name is
# due to a workaround current python
# legacy build doesn't support aarch64
# so using the currently supported arm64
# build and simply rename it to aarch64
# see full context on #7148
plat_name = 'manylinux_2_28_aarch64'
else:
plat_name = 'manylinux_2_28_i686'
elif distos == 'linux' and os_id == 'alpine':
if arch == 'x64':
plat_name = 'musllinux_1_1_x86_64'
else:
plat_name = 'musllinux_1_1_i686'
elif distos == 'win':
if arch == 'x64':
plat_name = 'win_amd64'
else:
plat_name = 'win32'
elif distos == 'osx':
osver = RELEASE_METADATA[3]
if osver.count('.') > 1:
osver = '.'.join(osver.split('.')[:2])
if osver.startswith("11"):
osver = "11_0"
if arch == 'x64':
plat_name ='macosx_%s_x86_64' % osver.replace('.', '_')
elif arch == 'arm64':
plat_name ='macosx_%s_arm64' % osver.replace('.', '_')
else:
raise Exception(f"idk how os {distos} {osver} works. what goes here?")
else:
raise Exception(f"idk how to translate between this z3 release os {distos} and the python naming scheme")
idx = sys.argv.index('bdist_wheel') + 1
sys.argv.insert(idx, '--plat-name')
sys.argv.insert(idx + 1, plat_name)
sys.argv.insert(idx + 2, '--universal') # supports py2+py3. if --plat-name is not specified this will also mean that the package can be installed on any machine regardless of architecture, so watch out!
setup(
name='z3-solver',
version=_z3_version(),
description='an efficient SMT solver library',
long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compilation, or installation, please submit issues to https://github.com/z3prover/z3.git',
long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html',
author="The Z3 Theorem Prover Project",
maintainer="Audrey Dutcher and Nikolaj Bjorner",
maintainer_email="audrey@rhelmot.io",
@ -356,5 +292,5 @@ setup(
'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')]
},
data_files=[('bin',[os.path.join('bin',EXECUTABLE_FILE)])],
cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg, 'clean': clean},
cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_wheel': bdist_wheel},
)

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

@ -6798,7 +6798,7 @@ class Statistics:
sat
>>> st = s.statistics()
>>> len(st)
6
7
"""
return int(Z3_stats_size(self.ctx.ref(), self.stats))
@ -6812,11 +6812,11 @@ class Statistics:
sat
>>> st = s.statistics()
>>> len(st)
6
7
>>> st[0]
('nlsat propagations', 2)
>>> st[1]
('nlsat stages', 2)
('nlsat restarts', 1)
"""
if idx >= len(self):
raise IndexError
@ -7353,6 +7353,13 @@ class Solver(Z3PPObject):
Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
return trail, levels
def set_initial_value(self, var, value):
"""initialize the solver's state by setting the initial value of var to value
"""
s = var.sort()
value = s.cast(value)
Z3_solver_set_initial_value(self.ctx.ref(), self.solver, var.ast, value.ast)
def trail(self):
"""Return trail of the solver state after a check() call.
"""
@ -7926,9 +7933,12 @@ _on_model_eh = on_model_eh_type(_global_on_model)
class Optimize(Z3PPObject):
"""Optimize API provides methods for solving using objective functions and weighted soft constraints"""
def __init__(self, ctx=None):
def __init__(self, optimize=None, ctx=None):
self.ctx = _get_ctx(ctx)
self.optimize = Z3_mk_optimize(self.ctx.ref())
if optimize is None:
self.optimize = Z3_mk_optimize(self.ctx.ref())
else:
self.optimize = optimize
self._on_models_id = None
Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
@ -8029,6 +8039,13 @@ class Optimize(Z3PPObject):
return [asoft(a) for a in arg]
return asoft(arg)
def set_initial_value(self, var, value):
"""initialize the solver's state by setting the initial value of var to value
"""
s = var.sort()
value = s.cast(value)
Z3_optimize_set_initial_value(self.ctx.ref(), self.optimize, var.ast, value.ast)
def maximize(self, arg):
"""Add objective function to maximize."""
return OptimizeObjective(
@ -10220,7 +10237,7 @@ def FPs(names, fpsort, ctx=None):
>>> x.ebits()
8
>>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
x + y * z
(x + y) * z
"""
ctx = _get_ctx(ctx)
if isinstance(names, str):

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

@ -1412,8 +1412,10 @@ class HTMLFormatter(Formatter):
ys_pp = group(seq(ys))
if a.is_forall():
header = "&forall;"
else:
elif a.is_exists():
header = "&exist;"
else:
header = "&lambda;"
return group(compose(to_format(header, 1),
indent(1, compose(ys_pp, to_format(" :"), line_break(), body_pp))))

12
src/api/z3_api.h
View file

@ -7241,6 +7241,18 @@ extern "C" {
bool Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const* fixed, unsigned num_eqs, Z3_ast const* eq_lhs, Z3_ast const* eq_rhs, Z3_ast conseq);
/**
\brief provide an initialization hint to the solver. The initialization hint is used to calibrate an initial value of the expression that
represents a variable. If the variable is Boolean, the initial phase is set according to \c value. If the variable is an integer or real,
the initial Simplex tableau is recalibrated to attempt to follow the value assignment.
def_API('Z3_solver_set_initial_value', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST), _in(AST)))
*/
void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast v, Z3_ast val);
/**
\brief Check whether the assertions in a given solver are consistent or not.

12
src/api/z3_optimization.h
View file

@ -139,6 +139,18 @@ extern "C" {
*/
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d);
/**
\brief provide an initialization hint to the solver.
The initialization hint is used to calibrate an initial value of the expression that
represents a variable. If the variable is Boolean, the initial phase is set
according to \c value. If the variable is an integer or real,
the initial Simplex tableau is recalibrated to attempt to follow the value assignment.
def_API('Z3_optimize_set_initial_value', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(AST)))
*/
void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast v, Z3_ast val);
/**
\brief Check consistency and produce optimal values.
\param c - context

3
src/ast/arith_decl_plugin.cpp
View file

@ -34,9 +34,6 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
m_nums(m_amanager) {
}
~algebraic_numbers_wrapper() {
}
unsigned mk_id(algebraic_numbers::anum const & val) {
SASSERT(!m_amanager.is_rational(val));
unsigned idx = m_id_gen.mk();

2
src/ast/array_decl_plugin.cpp
View file

@ -577,9 +577,9 @@ void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol
void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
op_names.push_back(builtin_name("store",OP_STORE));
op_names.push_back(builtin_name("select",OP_SELECT));
op_names.push_back(builtin_name("const",OP_CONST_ARRAY)); // github issue #7383
if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) {
// none of the SMT2 logics support these extensions
op_names.push_back(builtin_name("const",OP_CONST_ARRAY));
op_names.push_back(builtin_name("map",OP_ARRAY_MAP));
op_names.push_back(builtin_name("default",OP_ARRAY_DEFAULT));
op_names.push_back(builtin_name("union",OP_SET_UNION));

9
src/ast/ast.cpp
View file

@ -58,7 +58,7 @@ parameter::parameter(parameter const& other) : m_val(other.m_val) {
}
void parameter::init_eh(ast_manager & m) {
if (is_ast()) {
if (is_ast()) {
m.inc_ref(get_ast());
}
}
@ -1008,7 +1008,8 @@ sort* basic_decl_plugin::join(unsigned n, expr* const* es) {
}
sort* basic_decl_plugin::join(sort* s1, sort* s2) {
if (s1 == s2) return s1;
if (s1 == s2)
return s1;
if (s1->get_family_id() == arith_family_id &&
s2->get_family_id() == arith_family_id) {
if (s1->get_decl_kind() == REAL_SORT) {
@ -1016,6 +1017,10 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
}
return s2;
}
if (s1 == m_bool_sort && s2->get_family_id() == arith_family_id)
return s2;
if (s2 == m_bool_sort && s1->get_family_id() == arith_family_id)
return s1;
std::ostringstream buffer;
buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
throw ast_exception(buffer.str());

2
src/ast/ast_pp_dot.cpp
View file

@ -45,8 +45,6 @@ struct ast_pp_dot_st {
m_printed(),
m_to_print(),
m_first(true) {}
~ast_pp_dot_st() {};
void push_term(const expr * a) { m_to_print.push_back(a); }

13
src/ast/ast_smt_pp.cpp
View file

@ -31,6 +31,7 @@ Revision History:
#include "ast/datatype_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/fpa_decl_plugin.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/for_each_ast.h"
#include "ast/decl_collector.h"
#include "math/polynomial/algebraic_numbers.h"
@ -1000,6 +1001,18 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
}
}
vector<std::pair<func_decl*, expr*>> recfuns;
recfun::util u(m);
for (auto f : decls.get_rec_decls())
recfuns.push_back({f, u.get_def(f).get_rhs()});
if (!recfuns.empty()) {
smt2_pp_environment_dbg env(m);
ast_smt2_pp_recdefs(strm, recfuns, env);
}
#endif
for (expr* a : m_assumptions) {

3
src/ast/ast_trail.h
View file

@ -33,8 +33,7 @@ class ast2ast_trailmap {
public:
ast2ast_trailmap(ast_manager& m):
m_domain(m),
m_range(m),
m_map()
m_range(m)
{}
bool find(S* s, T*& t) {

4
src/ast/bv_decl_plugin.cpp
View file

@ -927,7 +927,7 @@ sort * bv_util::mk_sort(unsigned bv_size) {
}
unsigned bv_util::get_int2bv_size(parameter const& p) {
int sz;
int sz = 0;
VERIFY(m_plugin->get_int2bv_size(1, &p, sz));
return static_cast<unsigned>(sz);
}
@ -951,4 +951,4 @@ app* bv_util::mk_bv_rotate_left(expr* arg, unsigned n) {
app* bv_util::mk_bv_rotate_right(expr* arg, unsigned n) {
parameter p(n);
return m_manager.mk_app(get_fid(), OP_ROTATE_RIGHT, 1, &p, 1, &arg);
}
}

49
src/ast/converters/generic_model_converter.cpp
View file

@ -22,6 +22,7 @@ Notes:
#include "ast/for_each_expr.h"
#include "ast/ast_util.h"
#include "ast/occurs.h"
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/converters/generic_model_converter.h"
@ -130,6 +131,54 @@ generic_model_converter * generic_model_converter::copy(ast_translation & transl
return res;
}
void generic_model_converter::convert_initialize_value(vector<std::pair<expr_ref, expr_ref>> & var2value) {
if (var2value.empty() || m_entries.empty())
return;
for (unsigned i = 0; i < var2value.size(); ++i) {
auto& [var, value] = var2value[i];
for (auto const& e : m_entries) {
switch (e.m_instruction) {
case HIDE:
break;
case ADD:
if (is_uninterp_const(var) && e.m_f == to_app(var)->get_decl())
convert_initialize_value(e.m_def, i, var2value);
break;
}
}
}
}
void generic_model_converter::convert_initialize_value(expr* def, unsigned i, vector<std::pair<expr_ref, expr_ref>>& var2value) {
// var = if(c, th, el) = value
// th = value => c = true
// el = value => c = false
expr* c = nullptr, *th = nullptr, *el = nullptr;
auto& [var, value] = var2value[i];
if (m.is_ite(def, c, th, el)) {
if (value == th) {
var = c;
value = m.mk_true();
return;
}
if (value == el) {
var = c;
value = m.mk_false();
return;
}
}
// var = def = value
// => def = value
if (is_uninterp(def)) {
var = def;
return;
}
}
void generic_model_converter::set_env(ast_pp_util* visitor) {
if (!visitor) {

3
src/ast/converters/generic_model_converter.h
View file

@ -37,6 +37,7 @@ private:
vector<entry> m_entries;
expr_ref simplify_def(entry const& e);
void convert_initialize_value(expr* def, unsigned i, vector<std::pair<expr_ref, expr_ref>>& var2value);
public:
generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {}
@ -61,6 +62,8 @@ public:
model_converter * translate(ast_translation & translator) override { return copy(translator); }
void convert_initialize_value(vector<std::pair<expr_ref, expr_ref>>& var2value) override;
generic_model_converter* copy(ast_translation & translator);
void set_env(ast_pp_util* visitor) override;

6
src/ast/converters/model_converter.cpp
View file

@ -107,6 +107,12 @@ public:
m_c2->get_units(fmls);
m_c1->get_units(fmls);
}
void convert_initialize_value(vector<std::pair<expr_ref, expr_ref>>& var2value) override {
m_c2->convert_initialize_value(var2value);
m_c1->convert_initialize_value(var2value);
}
char const * get_name() const override { return "concat-model-converter"; }

5
src/ast/converters/model_converter.h
View file

@ -71,9 +71,6 @@ protected:
void display_del(std::ostream& out, func_decl* f) const;
void display_add(std::ostream& out, ast_manager& m);
public:
model_converter() {}
void set_completion(bool f) { m_completion = f; }
virtual void operator()(model_ref & m) = 0;
@ -86,6 +83,8 @@ public:
virtual void set_env(ast_pp_util* visitor);
virtual void convert_initialize_value(vector<std::pair<expr_ref, expr_ref>> & var2value) { }
/**
\brief we are adding a formula to the context of the model converter.
The operator has as side effect of adding definitions as assertions to the

112
src/ast/datatype_decl_plugin.cpp
View file

@ -220,17 +220,33 @@ namespace datatype {
}
namespace decl {
plugin::~plugin() {
finalize();
}
void plugin::finalize() {
for (auto& kv : m_defs) {
dealloc(kv.m_value);
}
for (auto& kv : m_defs)
dealloc(kv.m_value);
m_defs.reset();
m_util = nullptr; // force deletion
reset();
}
void plugin::reset() {
m_datatype2constructors.reset();
m_datatype2nonrec_constructor.reset();
m_constructor2accessors.reset();
m_constructor2recognizer.reset();
m_recognizer2constructor.reset();
m_accessor2constructor.reset();
m_is_recursive.reset();
m_is_enum.reset();
std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
m_vectors.reset();
dealloc(m_asts);
m_asts = nullptr;
++m_start;
}
util & plugin::u() const {
@ -578,6 +594,7 @@ namespace datatype {
if (m_defs.find(s, d))
dealloc(d);
m_defs.remove(s);
reset();
}
bool plugin::is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const {
@ -799,7 +816,7 @@ namespace datatype {
for (unsigned i = 0; i < n; ++i) {
sort* ps = get_datatype_parameter_sort(s, i);
sz = get_sort_size(params, ps);
m_refs.push_back(sz);
plugin().m_refs.push_back(sz);
S.insert(d.params().get(i), sz);
}
auto ss = d.sort_size();
@ -896,7 +913,7 @@ namespace datatype {
}
TRACE("datatype", tout << "set sort size " << s << "\n";);
d.set_sort_size(param_size::size::mk_plus(s_add));
m_refs.reset();
plugin().m_refs.reset();
}
}
@ -1008,9 +1025,7 @@ namespace datatype {
util::util(ast_manager & m):
m(m),
m_family_id(null_family_id),
m_plugin(nullptr),
m_asts(m),
m_start(0) {
m_plugin(nullptr) {
}
@ -1025,26 +1040,21 @@ namespace datatype {
return m_family_id;
}
util::~util() {
std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
}
ptr_vector<func_decl> const * util::get_datatype_constructors(sort * ty) {
SASSERT(is_datatype(ty));
ptr_vector<func_decl> * r = nullptr;
if (m_datatype2constructors.find(ty, r))
if (plugin().m_datatype2constructors.find(ty, r))
return r;
r = alloc(ptr_vector<func_decl>);
m_asts.push_back(ty);
m_vectors.push_back(r);
m_datatype2constructors.insert(ty, r);
plugin().add_ast(ty);
plugin().m_vectors.push_back(r);
plugin().m_datatype2constructors.insert(ty, r);
if (!is_declared(ty))
m.raise_exception("datatype constructors have not been created");
def const& d = get_def(ty);
for (constructor const* c : d) {
func_decl_ref f = c->instantiate(ty);
m_asts.push_back(f);
plugin().add_ast(f);
r->push_back(f);
}
return r;
@ -1053,13 +1063,13 @@ namespace datatype {
ptr_vector<func_decl> const * util::get_constructor_accessors(func_decl * con) {
SASSERT(is_constructor(con));
ptr_vector<func_decl> * res = nullptr;
if (m_constructor2accessors.find(con, res)) {
if (plugin().m_constructor2accessors.find(con, res)) {
return res;
}
res = alloc(ptr_vector<func_decl>);
m_asts.push_back(con);
m_vectors.push_back(res);
m_constructor2accessors.insert(con, res);
plugin().add_ast(con);
plugin().m_vectors.push_back(res);
plugin().m_constructor2accessors.insert(con, res);
sort * datatype = con->get_range();
def const& d = get_def(datatype);
for (constructor const* c : d) {
@ -1067,7 +1077,7 @@ namespace datatype {
for (accessor const* a : *c) {
func_decl_ref fn = a->instantiate(datatype);
res->push_back(fn);
m_asts.push_back(fn);
plugin().add_ast(fn);
}
break;
}
@ -1086,7 +1096,7 @@ namespace datatype {
func_decl * util::get_constructor_recognizer(func_decl * con) {
SASSERT(is_constructor(con));
func_decl * d = nullptr;
if (m_constructor2recognizer.find(con, d))
if (plugin().m_constructor2recognizer.find(con, d))
return d;
sort * datatype = con->get_range();
def const& dd = get_def(datatype);
@ -1097,9 +1107,9 @@ namespace datatype {
parameter ps[2] = { parameter(con), parameter(r) };
d = m.mk_func_decl(fid(), OP_DT_RECOGNISER, 2, ps, 1, &datatype);
SASSERT(d);
m_asts.push_back(con);
m_asts.push_back(d);
m_constructor2recognizer.insert(con, d);
plugin().add_ast(con);
plugin().add_ast(d);
plugin().m_constructor2recognizer.insert(con, d);
return d;
}
@ -1120,10 +1130,10 @@ namespace datatype {
bool util::is_recursive(sort * ty) {
SASSERT(is_datatype(ty));
bool r = false;
if (!m_is_recursive.find(ty, r)) {
if (!plugin().m_is_recursive.find(ty, r)) {
r = is_recursive_core(ty);
m_is_recursive.insert(ty, r);
m_asts.push_back(ty);
plugin().m_is_recursive.insert(ty, r);
plugin().add_ast(ty);
}
return r;
}
@ -1147,21 +1157,21 @@ namespace datatype {
if (!is_datatype(s))
return false;
bool r = false;
if (m_is_enum.find(s, r))
if (plugin().m_is_enum.find(s, r))
return r;
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
r = true;
for (unsigned i = 0; r && i < cnstrs.size(); ++i)
r = cnstrs[i]->get_arity() == 0;
m_is_enum.insert(s, r);
m_asts.push_back(s);
plugin().m_is_enum.insert(s, r);
plugin().add_ast(s);
return r;
}
func_decl * util::get_accessor_constructor(func_decl * accessor) {
SASSERT(is_accessor(accessor));
func_decl * r = nullptr;
if (m_accessor2constructor.find(accessor, r))
if (plugin().m_accessor2constructor.find(accessor, r))
return r;
sort * datatype = accessor->get_domain(0);
symbol c_id = accessor->get_parameter(1).get_symbol();
@ -1174,26 +1184,15 @@ namespace datatype {
}
}
r = fn;
m_accessor2constructor.insert(accessor, r);
m_asts.push_back(accessor);
m_asts.push_back(r);
plugin().m_accessor2constructor.insert(accessor, r);
plugin().add_ast(accessor);
plugin().add_ast(r);
return r;
}
void util::reset() {
m_datatype2constructors.reset();
m_datatype2nonrec_constructor.reset();
m_constructor2accessors.reset();
m_constructor2recognizer.reset();
m_recognizer2constructor.reset();
m_accessor2constructor.reset();
m_is_recursive.reset();
m_is_enum.reset();
std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
m_vectors.reset();
m_asts.reset();
++m_start;
plugin().reset();
}
@ -1205,7 +1204,7 @@ namespace datatype {
func_decl * util::get_non_rec_constructor(sort * ty) {
SASSERT(is_datatype(ty));
cnstr_depth cd;
if (m_datatype2nonrec_constructor.find(ty, cd))
if (plugin().m_datatype2nonrec_constructor.find(ty, cd))
return cd.first;
ptr_vector<sort> forbidden_set;
forbidden_set.push_back(ty);
@ -1222,7 +1221,7 @@ namespace datatype {
each T_i is not a datatype or it is a datatype t not in forbidden_set,
and get_non_rec_constructor_core(T_i, forbidden_set union { T_i })
*/
util::cnstr_depth util::get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set) {
cnstr_depth util::get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set) {
// We must select a constructor c(T_1, ..., T_n):T such that
// 1) T_i's are not recursive
// If there is no such constructor, then we select one that
@ -1231,7 +1230,7 @@ namespace datatype {
ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty);
array_util autil(m);
cnstr_depth result(nullptr, 0);
if (m_datatype2nonrec_constructor.find(ty, result))
if (plugin().m_datatype2nonrec_constructor.find(ty, result))
return result;
TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n";
tout << "forbidden: ";
@ -1273,9 +1272,9 @@ namespace datatype {
}
}
if (result.first) {
m_asts.push_back(result.first);
m_asts.push_back(ty);
m_datatype2nonrec_constructor.insert(ty, result);
plugin().add_ast(result.first);
plugin().add_ast(ty);
plugin().m_datatype2nonrec_constructor.insert(ty, result);
}
return result;
}
@ -1291,6 +1290,7 @@ namespace datatype {
IF_VERBOSE(0, verbose_stream() << f->get_name() << "\n");
for (constructor* c : d)
IF_VERBOSE(0, verbose_stream() << "!= " << c->name() << "\n");
return UINT_MAX;
SASSERT(false);
UNREACHABLE();
return 0;

42
src/ast/datatype_decl_plugin.h
View file

@ -198,6 +198,8 @@ namespace datatype {
def* translate(ast_translation& tr, util& u);
};
typedef std::pair<func_decl*, unsigned> cnstr_depth;
namespace decl {
class plugin : public decl_plugin {
@ -213,6 +215,7 @@ namespace datatype {
void log_axiom_definitions(symbol const& s, sort * new_sort);
public:
plugin(): m_id_counter(0), m_class_id(0), m_has_nested_rec(false) {}
~plugin() override;
@ -259,6 +262,25 @@ namespace datatype {
bool has_nested_rec() const { return m_has_nested_rec; }
void reset();
obj_map<sort, ptr_vector<func_decl>*> m_datatype2constructors;
obj_map<sort, cnstr_depth> m_datatype2nonrec_constructor;
obj_map<func_decl, ptr_vector<func_decl>*> m_constructor2accessors;
obj_map<func_decl, func_decl*> m_constructor2recognizer;
obj_map<func_decl, func_decl*> m_recognizer2constructor;
obj_map<func_decl, func_decl*> m_accessor2constructor;
obj_map<sort, bool> m_is_recursive;
obj_map<sort, bool> m_is_enum;
mutable obj_map<sort, bool> m_is_fully_interp;
mutable ast_ref_vector* m_asts = nullptr;
sref_vector<param_size::size> m_refs;
ptr_vector<ptr_vector<func_decl> > m_vectors;
unsigned m_start = 0;
mutable ptr_vector<sort> m_fully_interp_trail;
void add_ast(ast* a) const { if (!m_asts) m_asts = alloc(ast_ref_vector, *m_manager); m_asts->push_back(a); }
private:
bool is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const;
bool is_value_aux(bool unique, app * arg) const;
@ -295,25 +317,10 @@ namespace datatype {
ast_manager & m;
mutable family_id m_family_id;
mutable decl::plugin* m_plugin;
typedef std::pair<func_decl*, unsigned> cnstr_depth;
family_id fid() const;
obj_map<sort, ptr_vector<func_decl> *> m_datatype2constructors;
obj_map<sort, cnstr_depth> m_datatype2nonrec_constructor;
obj_map<func_decl, ptr_vector<func_decl> *> m_constructor2accessors;
obj_map<func_decl, func_decl *> m_constructor2recognizer;
obj_map<func_decl, func_decl *> m_recognizer2constructor;
obj_map<func_decl, func_decl *> m_accessor2constructor;
obj_map<sort, bool> m_is_recursive;
obj_map<sort, bool> m_is_enum;
mutable obj_map<sort, bool> m_is_fully_interp;
mutable ast_ref_vector m_asts;
sref_vector<param_size::size> m_refs;
ptr_vector<ptr_vector<func_decl> > m_vectors;
unsigned m_start;
mutable ptr_vector<sort> m_fully_interp_trail;
cnstr_depth get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
friend class decl::plugin;
@ -331,7 +338,6 @@ namespace datatype {
public:
util(ast_manager & m);
~util();
ast_manager & get_manager() const { return m; }
// sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params);
bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); }

6
src/ast/euf/euf_ac_plugin.cpp
View file

@ -440,8 +440,9 @@ namespace euf {
TRACE("plugin", tout << "propagate " << eq_id << ": " << eq_pp(*this, m_eqs[eq_id]) << "\n");
// simplify eq using processed
for (auto other_eq : backward_iterator(eq_id))
TRACE("plugin", tout << "backward iterator " << eq_id << " vs " << other_eq << " " << is_processed(other_eq) << "\n");
TRACE("plugin",
for (auto other_eq : backward_iterator(eq_id))
tout << "backward iterator " << eq_id << " vs " << other_eq << " " << is_processed(other_eq) << "\n");
for (auto other_eq : backward_iterator(eq_id))
if (is_processed(other_eq) && backward_simplify(eq_id, other_eq))
goto loop_start;
@ -907,7 +908,6 @@ namespace euf {
m_dst_r.reset();
m_dst_r.append(monomial(dst.r).m_nodes);
unsigned src_r_size = m_src_r.size();
unsigned dst_r_size = m_dst_r.size();
SASSERT(src_r_size == monomial(src.r).size());
// dst_r contains C
// src_r contains E

6
src/ast/euf/euf_ac_plugin.h
View file

@ -47,7 +47,6 @@ namespace euf {
unsigned_vector eqs; // equality occurrences
unsigned root_id() const { return root->n->get_id(); }
~node() {}
static node* mk(region& r, enode* n);
};
@ -62,8 +61,7 @@ namespace euf {
node* operator*() { return m_first; }
iterator& operator++() { if (!m_last) m_last = m_first; m_first = m_first->next; return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& other) const { return m_last == other.m_last && m_first == other.m_first; }
bool operator!=(iterator const& other) const { return !(*this == other); }
bool operator!=(iterator const& other) const { return m_last != other.m_last || m_first != other.m_first; }
};
equiv(node& _n) :n(_n) {}
equiv(node* _n) :n(*_n) {}
@ -270,8 +268,6 @@ namespace euf {
ac_plugin(egraph& g, unsigned fid, unsigned op);
ac_plugin(egraph& g, func_decl* f);
~ac_plugin() override {}
theory_id get_id() const override { return m_fid; }

2
src/ast/euf/euf_arith_plugin.h
View file

@ -33,8 +33,6 @@ namespace euf {
public:
arith_plugin(egraph& g);
~arith_plugin() override {}
theory_id get_id() const override { return a.get_family_id(); }
void register_node(enode* n) override;

2
src/ast/euf/euf_bv_plugin.h
View file

@ -95,8 +95,6 @@ namespace euf {
public:
bv_plugin(egraph& g);
~bv_plugin() override {}
theory_id get_id() const override { return bv.get_family_id(); }
void register_node(enode* n) override;

4
src/ast/euf/euf_egraph.cpp
View file

@ -107,8 +107,8 @@ namespace euf {
void egraph::update_children(enode* n) {
for (enode* child : enode_args(n))
child->get_root()->add_parent(n);
for (enode* child : enode_args(n))
SASSERT(child->get_root()->m_parents.back() == n);
DEBUG_CODE(for (enode* child : enode_args(n))
SASSERT(child->get_root()->m_parents.back() == n););
m_updates.push_back(update_record(n, update_record::update_children()));
}

6
src/ast/euf/euf_enode.h
View file

@ -280,8 +280,7 @@ namespace euf {
enode* operator*() { return m_first; }
iterator& operator++() { if (!m_last) m_last = m_first; m_first = m_first->m_next; return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& other) const { return m_last == other.m_last && m_first == other.m_first; }
bool operator!=(iterator const& other) const { return !(*this == other); }
bool operator!=(iterator const& other) const { return m_last != other.m_last || m_first != other.m_first; }
};
enode_class(enode & _n):n(_n) {}
enode_class(enode * _n):n(*_n) {}
@ -300,8 +299,7 @@ namespace euf {
th_var_list const& operator*() { return *m_th_vars; }
iterator& operator++() { m_th_vars = m_th_vars->get_next(); return *this; }
iterator operator++(int) { iterator tmp = *this; ++* this; return tmp; }
bool operator==(iterator const& other) const { return m_th_vars == other.m_th_vars; }
bool operator!=(iterator const& other) const { return !(*this == other); }
bool operator!=(iterator const& other) const { return m_th_vars != other.m_th_vars; }
};
enode_th_vars(enode& _n) :n(_n) {}
enode_th_vars(enode* _n) :n(*_n) {}

2
src/ast/euf/euf_specrel_plugin.h
View file

@ -34,8 +34,6 @@ namespace euf {
public:
specrel_plugin(egraph& g);
~specrel_plugin() override {}
theory_id get_id() const override { return sp.get_family_id(); }

3
src/ast/expr2polynomial.cpp
View file

@ -504,9 +504,6 @@ default_expr2polynomial::default_expr2polynomial(ast_manager & am, polynomial::m
expr2polynomial(am, pm, nullptr) {
}
default_expr2polynomial::~default_expr2polynomial() {
}
bool default_expr2polynomial::is_int(polynomial::var x) const {
return m_is_int[x];
}

1
src/ast/expr2polynomial.h
View file

@ -102,7 +102,6 @@ class default_expr2polynomial : public expr2polynomial {
bool_vector m_is_int;
public:
default_expr2polynomial(ast_manager & am, polynomial::manager & pm);
~default_expr2polynomial() override;
bool is_int(polynomial::var x) const override;
protected:
polynomial::var mk_var(bool is_int) override;

24
src/ast/for_each_expr.cpp
View file

@ -146,20 +146,16 @@ subterms::iterator& subterms::iterator::operator++() {
return *this;
}
bool subterms::iterator::operator==(iterator const& other) const {
bool subterms::iterator::operator!=(iterator const& other) const {
// ignore state of visited
if (other.m_esp->size() != m_esp->size()) {
return false;
return true;
}
for (unsigned i = m_esp->size(); i-- > 0; ) {
if (m_esp->get(i) != other.m_esp->get(i))
return false;
return true;
}
return true;
}
bool subterms::iterator::operator!=(iterator const& other) const {
return !(*this == other);
return false;
}
@ -216,18 +212,14 @@ subterms_postorder::iterator& subterms_postorder::iterator::operator++() {
return *this;
}
bool subterms_postorder::iterator::operator==(iterator const& other) const {
bool subterms_postorder::iterator::operator!=(iterator const& other) const {
// ignore state of visited
if (other.m_es.size() != m_es.size()) {
return false;
return true;
}
for (unsigned i = m_es.size(); i-- > 0; ) {
if (m_es.get(i) != other.m_es.get(i))
return false;
return true;
}
return true;
}
bool subterms_postorder::iterator::operator!=(iterator const& other) const {
return !(*this == other);
return false;
}

2
src/ast/for_each_expr.h
View file

@ -190,7 +190,6 @@ public:
expr* operator*();
iterator operator++(int);
iterator& operator++();
bool operator==(iterator const& other) const;
bool operator!=(iterator const& other) const;
};
@ -220,7 +219,6 @@ public:
expr* operator*();
iterator operator++(int);
iterator& operator++();
bool operator==(iterator const& other) const;
bool operator!=(iterator const& other) const;
};
static subterms_postorder all(expr_ref_vector const& es) { return subterms_postorder(es, true); }

2
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -2692,7 +2692,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
SASSERT(tmp_rat.is_int32());
SASSERT(sz == 3);
mpf_rounding_mode mrm;
mpf_rounding_mode mrm = MPF_ROUND_TOWARD_ZERO;
switch ((BV_RM_VAL)tmp_rat.get_unsigned()) {
case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break;
case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break;

3
src/ast/fpa/fpa2bv_rewriter.h
View file

@ -36,9 +36,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p);
~fpa2bv_rewriter_cfg() {
}
void cleanup_buffers() {
m_out.finalize();
}

6
src/ast/fpa_decl_plugin.cpp
View file

@ -47,9 +47,6 @@ void fpa_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_bv_plugin = static_cast<bv_decl_plugin*>(m_manager->get_plugin(m_bv_fid));
}
fpa_decl_plugin::~fpa_decl_plugin() {
}
unsigned fpa_decl_plugin::mk_id(mpf const & v) {
unsigned new_id = m_id_gen.mk();
m_values.reserve(new_id+1);
@ -961,9 +958,6 @@ fpa_util::fpa_util(ast_manager & m):
m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m_fid));
}
fpa_util::~fpa_util() {
}
sort * fpa_util::mk_float_sort(unsigned ebits, unsigned sbits) {
parameter ps[2] = { parameter(ebits), parameter(sbits) };
return m().mk_sort(m_fid, FLOATING_POINT_SORT, 2, ps);

2
src/ast/fpa_decl_plugin.h
View file

@ -175,7 +175,6 @@ public:
bool is_float_sort(sort * s) const { return is_sort_of(s, m_family_id, FLOATING_POINT_SORT); }
bool is_rm_sort(sort * s) const { return is_sort_of(s, m_family_id, ROUNDING_MODE_SORT); }
~fpa_decl_plugin() override;
void finalize() override;
decl_plugin * mk_fresh() override;
@ -216,7 +215,6 @@ class fpa_util {
public:
fpa_util(ast_manager & m);
~fpa_util();
ast_manager & m() const { return m_manager; }
mpf_manager & fm() const { return m_plugin->fm(); }

3
src/ast/has_free_vars.cpp
View file

@ -30,7 +30,7 @@ class contains_vars::imp {
void visit(expr * n, unsigned delta, bool & visited) {
expr_delta_pair e(n, delta);
if (!m_cache.contains(e)) {
if (!is_ground(n) && !m_cache.contains(e)) {
m_todo.push_back(e);
visited = false;
}
@ -74,6 +74,7 @@ public:
m_todo.push_back(expr_delta_pair(n, begin));
while (!m_todo.empty()) {
expr_delta_pair e = m_todo.back();
if (visit_children(e.m_node, e.m_delta)) {
m_cache.insert(e);
m_todo.pop_back();

5
src/ast/macros/cond_macro.h
View file

@ -39,10 +39,7 @@ public:
m_weight(weight) {
SASSERT(!m_hint || !m_cond);
}
~cond_macro() {
}
func_decl * get_f() const { return m_f; }
expr * get_def() const { return m_def; }

3
src/ast/macros/macro_finder.cpp
View file

@ -269,9 +269,6 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
m_autil(m) {
}
macro_finder::~macro_finder() {
}
bool macro_finder::expand_macros(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
TRACE("macro_finder", tout << "starting expand_macros:\n";
m_macro_manager.display(tout););

1
src/ast/macros/macro_finder.h
View file

@ -43,7 +43,6 @@ class macro_finder {
public:
macro_finder(ast_manager & m, macro_manager & mm);
~macro_finder();
void operator()(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
void operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
};

3
src/ast/macros/macro_manager.cpp
View file

@ -41,9 +41,6 @@ macro_manager::macro_manager(ast_manager & m):
m_util.set_forbidden_set(&m_forbidden_set);
}
macro_manager::~macro_manager() {
}
void macro_manager::push_scope() {
m_scopes.push_back(scope());
scope & s = m_scopes.back();

1
src/ast/macros/macro_manager.h
View file

@ -64,7 +64,6 @@ class macro_manager {
public:
macro_manager(ast_manager & m);
~macro_manager();
void copy_to(macro_manager& dst);
ast_manager & get_manager() const { return m; }
macro_util & get_util() { return m_util; }

3
src/ast/macros/quasi_macros.cpp
View file

@ -31,9 +31,6 @@ quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) :
m_new_qsorts(m) {
}
quasi_macros::~quasi_macros() {
}
void quasi_macros::find_occurrences(expr * e) {
unsigned j;
m_todo.reset();

1
src/ast/macros/quasi_macros.h
View file

@ -60,7 +60,6 @@ class quasi_macros {
public:
quasi_macros(ast_manager & m, macro_manager & mm);
~quasi_macros();
/**
\brief Find pure function macros and apply them.

5
src/ast/normal_forms/defined_names.cpp
View file

@ -57,7 +57,7 @@ struct defined_names::impl {
unsigned_vector m_lims; //!< Backtracking support.
impl(ast_manager & m, char const * prefix);
virtual ~impl();
virtual ~impl() = default;
app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
void cache_new_name(expr * e, app * name);
@ -90,9 +90,6 @@ defined_names::impl::impl(ast_manager & m, char const * prefix):
m_z3name = prefix;
}
defined_names::impl::~impl() {
}
/**
\brief Given an expression \c e that may contain free variables, return an application (sk x_1 ... x_n),
where sk is a fresh variable name, and x_i's are the free variables of \c e.

5
src/ast/normal_forms/nnf.cpp
View file

@ -69,6 +69,7 @@ class skolemizer {
typedef act_cache cache;
ast_manager & m;
var_subst m_subst;
symbol m_sk_hack;
bool m_sk_hack_enabled;
cache m_cache;
@ -128,7 +129,6 @@ class skolemizer {
//
// (VAR 0) should be in the last position of substitution.
//
var_subst s(m);
SASSERT(is_well_sorted(m, q->get_expr()));
expr_ref tmp(m);
expr * body = q->get_expr();
@ -146,7 +146,7 @@ class skolemizer {
}
}
}
r = s(body, substitution);
r = m_subst(body, substitution);
p = nullptr;
if (m_proofs_enabled) {
if (q->get_kind() == forall_k)
@ -159,6 +159,7 @@ class skolemizer {
public:
skolemizer(ast_manager & m):
m(m),
m_subst(m),
m_sk_hack("sk_hack"),
m_sk_hack_enabled(false),
m_cache(m),

3
src/ast/pattern/expr_pattern_match.cpp
View file

@ -41,9 +41,6 @@ expr_pattern_match::expr_pattern_match(ast_manager & manager):
m_manager(manager), m_precompiled(manager) {
}
expr_pattern_match::~expr_pattern_match() {
}
bool
expr_pattern_match::match_quantifier(quantifier* qf, app_ref_vector& patterns, unsigned& weight) {
if (m_regs.empty()) {

1
src/ast/pattern/expr_pattern_match.h
View file

@ -116,7 +116,6 @@ class expr_pattern_match {
public:
expr_pattern_match(ast_manager & manager);
~expr_pattern_match();
bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight);
bool match_quantifier_index(quantifier* qf, app_ref_vector & patterns, unsigned& index);
unsigned initialize(quantifier* qf);

6
src/ast/pattern/pattern_inference.h
View file

@ -114,9 +114,9 @@ class pattern_inference_cfg : public default_rewriter_cfg {
//
class collect {
struct entry {
expr * m_node;
unsigned m_delta;
entry():m_node(nullptr), m_delta(0) {}
expr * m_node = nullptr;
unsigned m_delta = 0;
entry() = default;
entry(expr * n, unsigned d):m_node(n), m_delta(d) {}
unsigned hash() const {
return hash_u_u(m_node->get_id(), m_delta);

2
src/ast/proofs/proof_utils.h
View file

@ -230,7 +230,7 @@ public:
<< "New pf: " << mk_pp(newp, m) << "\n";);
}
proof *r;
proof *r = nullptr;
VERIFY(cache.find(pr, r));
DEBUG_CODE(

22
src/ast/recfun_decl_plugin.cpp
View file

@ -170,8 +170,6 @@ namespace recfun {
vector<branch> m_branches;
public:
case_state() : m_reg(), m_branches() {}
bool empty() const { return m_branches.empty(); }
branch pop_branch() {
@ -242,23 +240,18 @@ namespace recfun {
{
VERIFY(m_cases.empty() && "cases cannot already be computed");
SASSERT(n_vars == m_domain.size());
TRACEFN("compute cases " << mk_pp(rhs, m));
unsigned case_idx = 0;
std::string name("case-");
name.append(m_name.str());
m_vars.append(n_vars, vars);
m_rhs = rhs;
if (!is_macro)
for (expr* e : subterms::all(m_rhs))
if (is_lambda(e))
throw default_exception("recursive definitions with lambdas are not supported");
unsigned case_idx = 0;
expr_ref_vector conditions(m);
m_vars.append(n_vars, vars);
m_rhs = rhs;
// is the function a macro (unconditional body)?
if (is_macro || n_vars == 0 || !contains_ite(u, rhs)) {
@ -267,7 +260,6 @@ namespace recfun {
return;
}
// analyze control flow of `rhs`, accumulating guards and
// rebuilding a `ite`-free RHS on the fly for each path in `rhs`.
@ -368,9 +360,6 @@ namespace recfun {
m_plugin(dynamic_cast<decl::plugin*>(m.get_plugin(m_fid))) {
}
util::~util() {
}
def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range, bool is_generated) {
return alloc(def, m(), m_fid, name, n, domain, range, is_generated);
}
@ -419,7 +408,6 @@ namespace recfun {
}
namespace decl {
plugin::plugin() : decl_plugin(), m_defs(), m_case_defs() {}
plugin::~plugin() { finalize(); }
void plugin::finalize() {

2
src/ast/recfun_decl_plugin.h
View file

@ -173,7 +173,6 @@ namespace recfun {
void compute_scores(expr* e, obj_map<expr, unsigned>& scores);
public:
plugin();
~plugin() override;
void finalize() override;
@ -238,7 +237,6 @@ namespace recfun {
public:
util(ast_manager &m);
~util();
ast_manager & m() { return m_manager; }
family_id get_family_id() const { return m_fid; }

128
src/ast/rewriter/bv_rewriter.cpp
View file

@ -109,17 +109,20 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
break;
case OP_BNEG_OVFL:
SASSERT(num_args == 1);
return mk_bvneg_overflow(args[0], result);
st = mk_bvneg_overflow(args[0], result);
break;
case OP_BSHL:
SASSERT(num_args == 2);
return mk_bv_shl(args[0], args[1], result);
st = mk_bv_shl(args[0], args[1], result);
break;
case OP_BLSHR:
SASSERT(num_args == 2);
return mk_bv_lshr(args[0], args[1], result);
st = mk_bv_lshr(args[0], args[1], result);
break;
case OP_BASHR:
SASSERT(num_args == 2);
return mk_bv_ashr(args[0], args[1], result);
st = mk_bv_ashr(args[0], args[1], result);
break;
case OP_BSDIV:
SASSERT(num_args == 2);
return mk_bv_sdiv(args[0], args[1], result);
@ -151,13 +154,16 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
SASSERT(num_args == 2);
return mk_bv_smod_i(args[0], args[1], result);
case OP_CONCAT:
return mk_concat(num_args, args, result);
st = mk_concat(num_args, args, result);
break;
case OP_EXTRACT:
SASSERT(num_args == 1);
return mk_extract(m_util.get_extract_high(f), m_util.get_extract_low(f), args[0], result);
st = mk_extract(m_util.get_extract_high(f), m_util.get_extract_low(f), args[0], result);
break;
case OP_REPEAT:
SASSERT(num_args == 1);
return mk_repeat(f->get_parameter(0).get_int(), args[0], result);
st = mk_repeat(f->get_parameter(0).get_int(), args[0], result);
break;
case OP_ZERO_EXT:
SASSERT(num_args == 1);
return mk_zero_extend(f->get_parameter(0).get_int(), args[0], result);
@ -596,28 +602,45 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
//
// a <=_u #x000f
//
unsigned bv_sz = m_util.get_bv_size(b);
unsigned i = bv_sz;
unsigned first_non_zero = UINT_MAX;
while (i > 0) {
--i;
if (!is_zero_bit(b, i)) {
first_non_zero = i;
break;
}
}
unsigned bv_sz = m_util.get_bv_size(a);
auto last_non_zero = [&](expr* x) {
for (unsigned i = bv_sz; i-- > 0; )
if (!is_zero_bit(x, i))
return i;
return UINT_MAX;
};
unsigned lnz = last_non_zero(b);
if (first_non_zero == UINT_MAX) {
if (lnz == UINT_MAX) {
// all bits are zero
result = m.mk_eq(a, mk_zero(bv_sz));
return BR_REWRITE1;
}
else if (first_non_zero < bv_sz - 1 && m_le2extract) {
result = m.mk_and(m.mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), mk_zero(bv_sz - first_non_zero - 1)),
m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b)));
else if (lnz < bv_sz - 1 && m_le2extract) {
// a[sz-1:lnz+1] = 0 & a[lnz:0] <= b[lnz:0]
result = m.mk_and(m.mk_eq(m_mk_extract(bv_sz - 1, lnz + 1, a), mk_zero(bv_sz - lnz - 1)),
m_util.mk_ule(m_mk_extract(lnz, 0, a), m_mk_extract(lnz, 0, b)));
return BR_REWRITE3;
}
lnz = last_non_zero(a);
if (lnz == UINT_MAX) {
// all bits are zero
result = m.mk_true();
return BR_DONE;
}
else if (lnz < bv_sz - 1 && m_le2extract) {
// use the equivalence to simplify:
// #x000f <=_u b <=> b[sz-1:lnz+1] != 0 or #xf <= b[lnz:0])
result = m.mk_implies(m.mk_eq(m_mk_extract(bv_sz - 1, lnz + 1, b), mk_zero(bv_sz - lnz - 1)),
m_util.mk_ule(m_mk_extract(lnz, 0, a), m_mk_extract(lnz, 0, b)));
return BR_REWRITE_FULL;
}
}
#endif
@ -1422,19 +1445,50 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
br_status bv_rewriter::mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result) {
numeral val;
bool is_int;
expr* x;
if (m_autil.is_numeral(arg, val, is_int)) {
val = m_util.norm(val, bv_size);
result = mk_numeral(val, bv_size);
return BR_DONE;
}
// (int2bv (bv2int x)) --> x
if (m_util.is_bv2int(arg) && bv_size == get_bv_size(to_app(arg)->get_arg(0))) {
result = to_app(arg)->get_arg(0);
// int2bv (bv2int x) --> x
if (m_util.is_bv2int(arg, x) && bv_size == get_bv_size(x)) {
result = x;
return BR_DONE;
}
// int2bv (bv2int x) --> 0000x
if (m_util.is_bv2int(arg, x) && bv_size > get_bv_size(x)) {
mk_zero_extend(bv_size - get_bv_size(x), x, result);
return BR_REWRITE1;
}
// int2bv (bv2int x) --> x[sz-1:0]
if (m_util.is_bv2int(arg, x) && bv_size < get_bv_size(x)) {
result = m_mk_extract(bv_size - 1, 0, x);
return BR_REWRITE1;
}
#if 0
// int2bv (a + b) --> int2bv(a) + int2bv(b)
if (m_autil.is_add(arg)) {
expr_ref_vector args(m);
for (expr* e : *to_app(arg))
args.push_back(m_util.mk_int2bv(bv_size, e));
result = m_util.mk_bv_add(args);
return BR_REWRITE3;
}
// int2bv (a * b) --> int2bv(a) * int2bv(b)
if (m_autil.is_mul(arg)) {
expr_ref_vector args(m);
for (expr* e : *to_app(arg))
args.push_back(m_util.mk_int2bv(bv_size, e));
result = m_util.mk_bv_mul(args);
return BR_REWRITE3;
}
#endif
return BR_FAILED;
}
@ -2717,6 +2771,27 @@ bool bv_rewriter::is_urem_any(expr * e, expr * & dividend, expr * & divisor) {
return true;
}
br_status bv_rewriter::mk_eq_bv2int(expr* lhs, expr* rhs, expr_ref& result) {
rational r;
expr* x, *y;
if (m_autil.is_numeral(lhs))
std::swap(lhs, rhs);
if (m_autil.is_numeral(rhs, r) && m_util.is_bv2int(lhs, x)) {
unsigned bv_size = m_util.get_bv_size(x);
if (0 <= r && r < rational::power_of_two(bv_size))
result = m.mk_eq(m_util.mk_numeral(r, bv_size), x);
else
result = m.mk_false();
return BR_REWRITE1;
}
if (m_util.is_bv2int(lhs, x) && m_util.is_bv2int(rhs, y)) {
result = m.mk_eq(x, y);
return BR_REWRITE1;
}
return BR_FAILED;
}
br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
if (lhs == rhs) {
result = m.mk_true();
@ -2760,6 +2835,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
return st;
}
if (m_blast_eq_value) {
st = mk_blast_eq_value(lhs, rhs, result);
if (st != BR_FAILED)

1
src/ast/rewriter/bv_rewriter.h
View file

@ -203,6 +203,7 @@ public:
bool is_urem_any(expr * e, expr * & dividend, expr * & divisor);
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
br_status mk_eq_bv2int(expr* lhs, expr* rhs, expr_ref& result);
br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
br_status mk_distinct(unsigned num_args, expr * const * args, expr_ref & result);

10
src/ast/rewriter/factor_equivs.h
View file

@ -103,11 +103,10 @@ public:
m_first = false;
return *this;
}
bool operator==(const iterator& o) {
bool operator!=(const iterator& o) const {
SASSERT(&m_ouf == &o.m_ouf);
return m_first == o.m_first && m_curr_id == o.m_curr_id;
return m_first != o.m_first || m_curr_id != o.m_curr_id;
}
bool operator!=(const iterator& o) {return !(*this == o);}
};
iterator begin(OBJ*o) {
@ -152,11 +151,10 @@ public:
m_ouf.m_uf.is_root(m_rootnb) != true);
return *this;
}
bool operator==(const equiv_iterator& o) {
bool operator!=(const equiv_iterator& o) const {
SASSERT(&m_ouf == &o.m_ouf);
return m_rootnb == o.m_rootnb;
return m_rootnb != o.m_rootnb;
}
bool operator!=(const equiv_iterator& o) {return !(*this == o);}
};
equiv_iterator begin() {return equiv_iterator(*this, 0);}

1
src/ast/rewriter/inj_axiom.cpp
View file

@ -74,6 +74,7 @@ bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
}
}
if (found_vars && !has_free_vars(q)) {
(void)num_vars;
TRACE("inj_axiom",
tout << "Cadidate for simplification:\n" << mk_ll_pp(q, m) << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n" <<
mk_pp(var1, m) << "\n" << mk_pp(var2, m) << "\nnum_vars: " << num_vars << "\n";);

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

@ -26,8 +26,6 @@ label_rewriter::label_rewriter(ast_manager & m) :
m_label_fid(m.get_label_family_id()),
m_rwr(m, false, *this) {}
label_rewriter::~label_rewriter() {}
br_status label_rewriter::reduce_app(
func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr) {

1
src/ast/rewriter/label_rewriter.h
View file

@ -27,7 +27,6 @@ class label_rewriter : public default_rewriter_cfg {
rewriter_tpl<label_rewriter> m_rwr;
public:
label_rewriter(ast_manager & m);
~label_rewriter();
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr);

2
src/ast/rewriter/rewriter.h
View file

@ -346,8 +346,6 @@ public:
ast_manager & m() const { return this->m_manager; }
Config & cfg() { return m_cfg; }
Config const & cfg() const { return m_cfg; }
~rewriter_tpl() override {};
void reset();
void cleanup();

4
src/ast/rewriter/seq_rewriter.cpp
View file

@ -2060,6 +2060,10 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(a->get_sort()), c);
return BR_REWRITE2;
}
if (str().is_empty(a) && str().is_empty(c)) {
result = a;
return BR_DONE;
}
zstring s1, s2;
expr_ref_vector strs(m());
if (str().is_string(a, s1) && str().is_string(b, s2)) {

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

@ -59,6 +59,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
bv_util m_bv_util;
der m_der;
expr_safe_replace m_rep;
unused_vars_eliminator m_elim_unused_vars;
expr_ref_vector m_pinned;
// substitution support
expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions
@ -685,9 +686,18 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
st = m_seq_rw.mk_eq_core(a, b, result);
if (st != BR_FAILED)
return st;
st = extended_bv_eq(a, b, result);
if (st != BR_FAILED)
return st;
return apply_tamagotchi(a, b, result);
}
br_status extended_bv_eq(expr* a, expr* b, expr_ref& result) {
if (m_bv_util.is_bv2int(a) || m_bv_util.is_bv2int(b))
return m_bv_rw.mk_eq_bv2int(a, b, result);
return BR_FAILED;
}
expr_ref mk_eq(expr* a, expr* b) {
expr_ref result(m());
br_status st = reduce_eq(a, b, result);
@ -820,8 +830,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
}
SASSERT(old_q->get_sort() == q1->get_sort());
result = elim_unused_vars(m(), q1, params_ref());
result = m_elim_unused_vars(q1);
result_pr = nullptr;
@ -878,6 +887,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_bv_util(m),
m_der(m),
m_rep(m),
m_elim_unused_vars(m, params_ref()),
m_pinned(m),
m_used_dependencies(m) {
updt_local_params(p);

18
src/ast/rewriter/var_subst.cpp
View file

@ -52,6 +52,24 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args)
rep(n, result);
return result;
}
if (is_app(n) && all_of(*to_app(n), [&](expr* arg) { return is_ground(arg) || is_var(arg); })) {
ptr_buffer<expr> new_args;
for (auto arg : *to_app(n)) {
if (is_ground(arg))
new_args.push_back(arg);
else {
unsigned idx = to_var(arg)->get_idx();
expr* new_arg = nullptr;
if (idx < num_args)
new_arg = m_std_order ? args[num_args - idx - 1] : args[idx];
if (!new_arg)
new_arg = arg;
new_args.push_back(new_arg);
}
}
result = m.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.data());
return result;
}
SASSERT(is_well_sorted(result.m(), n));
m_reducer.reset();
if (m_std_order)

2
src/ast/rewriter/var_subst.h
View file

@ -94,7 +94,7 @@ class expr_free_vars {
ptr_vector<sort> m_sorts;
ptr_vector<expr> m_todo;
public:
expr_free_vars() {}
expr_free_vars() = default;
expr_free_vars(expr* e) { (*this)(e); }
void reset();
void operator()(expr* e);

2
src/ast/seq_decl_plugin.h
View file

@ -446,7 +446,7 @@ public:
/*
Default constructor of invalid info.
*/
info() {}
info() = default;
/*
Used for constructing either an invalid info that is only used to indicate uninitialized entry, or valid but unknown info value.

4
src/ast/simplifiers/dominator_simplifier.cpp
View file

@ -187,8 +187,8 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
}
expr_ref dominator_simplifier::simplify_not(app * e) {
expr *ee;
ENSURE(m.is_not(e, ee));
expr *ee = nullptr;
VERIFY(m.is_not(e, ee));
unsigned old_lvl = scope_level();
expr_ref t = simplify_rec(ee);
local_pop(scope_level() - old_lvl);

2
src/ast/simplifiers/linear_equation.h
View file

@ -35,7 +35,7 @@ private:
mpz * m_as; // precise coefficients
double * m_approx_as; // approximated coefficients
var * m_xs; // var ids
linear_equation() {}
linear_equation() = default;
public:
unsigned size() const { return m_size; }
mpz const & a(unsigned idx) const { SASSERT(idx < m_size); return m_as[idx]; }

2
src/ast/simplifiers/reduce_args_simplifier.cpp
View file

@ -375,8 +375,6 @@ public:
m_bv(m)
{}
~reduce_args_simplifier() override {}
char const* name() const override { return "reduce-args"; }
void collect_statistics(statistics& st) const override {

4
src/ast/sls/bvsls_opt_engine.cpp
View file

@ -28,10 +28,6 @@ bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) :
m_best_model = alloc(model, m);
}
bvsls_opt_engine::~bvsls_opt_engine()
{
}
bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
expr_ref const & objective,
model_ref initial_model,

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

@ -31,7 +31,6 @@ class bvsls_opt_engine : public sls_engine {
public:
bvsls_opt_engine(ast_manager & m, params_ref const & p);
~bvsls_opt_engine();
class optimization_result {
public:

2
src/ast/sls/sls_bv_valuation.h
View file

@ -31,7 +31,7 @@ namespace sls {
unsigned nw = 0;
unsigned mask = 0;
bvect() {}
bvect() = default;
bvect(unsigned sz) : svector(sz, (unsigned)0) {}
void set_bw(unsigned bw);

17
src/cmd_context/basic_cmds.cpp
View file

@ -318,6 +318,22 @@ UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING,
else
ctx.regular_stream() << arg << std::endl;);
class set_initial_value_cmd : public cmd {
expr* m_var = nullptr, *m_value = nullptr;
public:
set_initial_value_cmd(): cmd("set-initial-value") {}
char const* get_usage() const override { return "<var> <value>"; }
char const* get_descr(cmd_context& ctx) const override { return "set an initial value for search as a hint to the solver"; }
unsigned get_arity() const override { return 2; }
void prepare(cmd_context& ctx) override { m_var = m_value = nullptr; }
cmd_arg_kind next_arg_kind(cmd_context& ctx) const override { return CPK_EXPR; }
void set_next_arg(cmd_context& ctx, expr* e) override { if (m_var) m_value = e; else m_var = e; }
void execute(cmd_context& ctx) override {
SASSERT(m_var && m_value);
ctx.set_initial_value(m_var, m_value);
}
};
class set_get_option_cmd : public cmd {
protected:
symbol m_true;
@ -893,6 +909,7 @@ void install_basic_cmds(cmd_context & ctx) {
ctx.insert(alloc(get_option_cmd));
ctx.insert(alloc(get_info_cmd));
ctx.insert(alloc(set_info_cmd));
ctx.insert(alloc(set_initial_value_cmd));
ctx.insert(alloc(get_consequences_cmd));
ctx.insert(alloc(builtin_cmd, "assert", "<term>", "assert term."));
ctx.insert(alloc(builtin_cmd, "check-sat", "<boolean-constants>*", "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true."));

30
src/cmd_context/cmd_context.cpp
View file

@ -33,7 +33,6 @@ Notes:
#include "ast/fpa_decl_plugin.h"
#include "ast/special_relations_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/var_subst.h"
#include "ast/pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h"
@ -52,6 +51,7 @@ Notes:
#include "solver/smt_logics.h"
#include "cmd_context/basic_cmds.h"
#include "cmd_context/cmd_context.h"
#include "solver/slice_solver.h"
#include <iostream>
func_decls::func_decls(ast_manager & m, func_decl * f):
@ -406,8 +406,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma
recfun::promise_def d = p.ensure_def(s, arity, domain, t->get_sort(), false);
// recursive functions have opposite calling convention from macros!
var_subst sub(m(), true);
expr_ref tt = sub(t, rvars);
expr_ref tt = std_subst()(t, rvars);
p.set_definition(replace, d, true, vars.size(), vars.data(), tt);
register_fun(s, d.get_def()->get_decl());
}
@ -461,7 +460,6 @@ bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, exp
if (eq) {
t = d.m_body;
t = sub(t);
verbose_stream() << "macro " << t << "\n";
ptr_buffer<sort> domain;
for (unsigned i = 0; i < n; ++i)
domain.push_back(args[i]->get_sort());
@ -629,6 +627,7 @@ cmd_context::~cmd_context() {
finalize_cmds();
finalize_tactic_manager();
m_proof_cmds = nullptr;
m_var2values.reset();
reset(true);
m_mcs.reset();
m_solver = nullptr;
@ -654,6 +653,8 @@ void cmd_context::set_opt(opt_wrapper* opt) {
m_opt = opt;
for (unsigned i = 0; i < m_scopes.size(); ++i)
m_opt->push();
for (auto const& [var, value] : m_var2values)
m_opt->initialize_value(var, value);
m_opt->set_logic(m_logic);
}
@ -1254,9 +1255,8 @@ bool cmd_context::try_mk_macro_app(symbol const & s, unsigned num_args, expr * c
tout << "s: " << s << "\n";
tout << "body:\n" << mk_ismt2_pp(_t, m()) << "\n";
tout << "args:\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n" << mk_pp(args[i]->get_sort(), m()) << "\n";);
var_subst subst(m(), false);
scoped_rlimit no_limit(m().limit(), 0);
result = subst(_t, coerced_args);
result = rev_subst()(_t, coerced_args);
if (well_sorted_check_enabled() && !is_well_sorted(m(), result))
throw cmd_exception("invalid macro application, sort mismatch ", s);
return true;
@ -1515,12 +1515,15 @@ void cmd_context::reset(bool finalize) {
m_opt = nullptr;
m_pp_env = nullptr;
m_dt_eh = nullptr;
m_std_subst = nullptr;
m_rev_subst = nullptr;
if (m_manager) {
dealloc(m_pmanager);
m_pmanager = nullptr;
if (m_own_manager) {
dealloc(m_manager);
m_manager = nullptr;
m_manager_initialized = false;
}
else {
@ -1874,6 +1877,17 @@ void cmd_context::display_dimacs() {
}
}
void cmd_context::set_initial_value(expr* var, expr* value) {
if (get_opt()) {
get_opt()->initialize_value(var, value);
return;
}
if (get_solver())
get_solver()->user_propagate_initialize_value(var, value);
m_var2values.push_back({expr_ref(var, m()), expr_ref(value, m())});
}
void cmd_context::display_model(model_ref& mdl) {
if (mdl) {
if (mc0()) (*mc0())(mdl);
@ -2244,6 +2258,7 @@ void cmd_context::mk_solver() {
params_ref p;
m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled);
m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
m_solver = mk_slice_solver(m_solver.get());
}
@ -2450,9 +2465,6 @@ cmd_context::dt_eh::dt_eh(cmd_context & owner):
m_dt_util(owner.m()) {
}
cmd_context::dt_eh::~dt_eh() {
}
void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";);
for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) {

12
src/cmd_context/cmd_context.h
View file

@ -33,6 +33,7 @@ Notes:
#include "ast/datatype_decl_plugin.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/var_subst.h"
#include "ast/converters/generic_model_converter.h"
#include "solver/solver.h"
#include "solver/check_logic.h"
@ -47,7 +48,7 @@ class func_decls {
bool signatures_collide(func_decl* f, func_decl* g) const;
bool signatures_collide(unsigned n, sort*const* domain, sort* range, func_decl* g) const;
public:
func_decls() {}
func_decls() = default;
func_decls(ast_manager & m, func_decl * f);
void finalize(ast_manager & m);
bool contains(func_decl * f) const;
@ -173,6 +174,8 @@ public:
virtual void set_logic(symbol const& s) = 0;
virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
virtual void updt_params(params_ref const& p) = 0;
virtual void initialize_value(expr* var, expr* value) = 0;
};
class ast_context_params : public context_params {
@ -260,6 +263,7 @@ protected:
scoped_ptr_vector<builtin_decl> m_extra_builtin_decls; // make sure that dynamically allocated builtin_decls are deleted
dictionary<object_ref*> m_object_refs; // anything that can be named.
dictionary<sexpr*> m_user_tactic_decls;
vector<std::pair<expr_ref, expr_ref>> m_var2values;
dictionary<func_decls> m_func_decls;
obj_map<func_decl, symbol> m_func_decl2alias;
@ -277,6 +281,7 @@ protected:
ptr_vector<expr> m_assertions;
std::vector<std::string> m_assertion_strings;
ptr_vector<expr> m_assertion_names; // named assertions are represented using boolean variables.
scoped_ptr<var_subst> m_std_subst, m_rev_subst;
struct scope {
unsigned m_func_decls_stack_lim;
@ -302,7 +307,6 @@ protected:
public:
void reset() { m_dt_util.reset(); }
dt_eh(cmd_context & owner);
~dt_eh() override;
void operator()(sort * dt, pdecl* pd) override;
};
@ -315,6 +319,9 @@ protected:
scoped_ptr<pp_env> m_pp_env;
pp_env & get_pp_env() const;
var_subst& std_subst() { if (!m_std_subst) m_std_subst = alloc(var_subst, m(), true); return *m_std_subst; }
var_subst& rev_subst() { if (!m_rev_subst) m_rev_subst = alloc(var_subst, m(), false); return *m_rev_subst; }
void register_builtin_sorts(decl_plugin * p);
void register_builtin_ops(decl_plugin * p);
void load_plugin(symbol const & name, bool install_names, svector<family_id>& fids);
@ -419,6 +426,7 @@ public:
solver* get_solver() { return m_solver.get(); }
void set_solver(solver* s) { m_solver = s; }
void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; }
void set_initial_value(expr* var, expr* value);
void set_solver_factory(solver_factory * s);
void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }

4
src/cmd_context/tactic_cmds.cpp
View file

@ -27,7 +27,6 @@ Notes:
#include "ast/ast_smt2_pp.h"
#include "tactic/tactic.h"
#include "tactic/tactical.h"
#include "tactic/probe.h"
#include "solver/check_sat_result.h"
#include "cmd_context/cmd_context_to_goal.h"
#include "cmd_context/echo_tactic.h"
@ -38,9 +37,6 @@ probe_info::probe_info(symbol const & n, char const * d, probe * p):
m_probe(p) {
}
probe_info::~probe_info() {
}
class declare_tactic_cmd : public cmd {
symbol m_name;
sexpr * m_decl;

3
src/cmd_context/tactic_cmds.h
View file

@ -18,12 +18,12 @@ Notes:
#pragma once
#include "ast/ast.h"
#include "tactic/probe.h"
#include "util/params.h"
#include "util/cmd_context_types.h"
#include "util/ref.h"
class tactic;
class probe;
typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&);
@ -52,7 +52,6 @@ class probe_info {
ref<probe> m_probe;
public:
probe_info(symbol const & n, char const * d, probe * p);
~probe_info();
symbol get_name() const { return m_name; }
char const * get_descr() const { return m_descr; }

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

@ -571,8 +571,7 @@ namespace dd {
pdd_monomial const* operator->() const { return &m_mono; }
pdd_iterator& operator++() { next(); return *this; }
pdd_iterator operator++(int) { auto tmp = *this; next(); return tmp; }
bool operator==(pdd_iterator const& other) const { return m_nodes == other.m_nodes; }
bool operator!=(pdd_iterator const& other) const { return !operator==(other); }
bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; }
};
class pdd_linear_iterator {
@ -591,7 +590,6 @@ namespace dd {
pointer operator->() const { return &m_mono; }
pdd_linear_iterator& operator++() { next(); return *this; }
pdd_linear_iterator operator++(int) { auto tmp = *this; next(); return tmp; }
bool operator==(pdd_linear_iterator const& other) const { return m_next == other.m_next; }
bool operator!=(pdd_linear_iterator const& other) const { return m_next != other.m_next; }
};

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

@ -48,7 +48,7 @@ public:
friend class grobner;
friend struct monomial_lt;
monomial() {}
monomial() = default;
public:
rational const & get_coeff() const { return m_coeff; }
unsigned get_degree() const { return m_vars.size(); }
@ -63,7 +63,7 @@ public:
ptr_vector<monomial> m_monomials; //!< sorted monomials
v_dependency * m_dep; //!< justification for the equality
friend class grobner;
equation() {}
equation() = default;
public:
unsigned get_num_monomials() const { return m_monomials.size(); }
monomial const * get_monomial(unsigned idx) const { return m_monomials[idx]; }

1
src/math/hilbert/heap_trie.h
View file

@ -369,7 +369,6 @@ public:
}
iterator& operator++() { fwd(); return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& it) const {return m_count == it.m_count; }
bool operator!=(iterator const& it) const {return m_count != it.m_count; }
private:

2
src/math/hilbert/hilbert_basis.cpp
View file

@ -455,7 +455,6 @@ public:
offset_t operator*() const { return p.m_passive[m_idx]; }
iterator& operator++() { ++m_idx; fwd(); return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& it) const {return m_idx == it.m_idx; }
bool operator!=(iterator const& it) const {return m_idx != it.m_idx; }
};
@ -614,7 +613,6 @@ public:
offset_t sos() const { return (p.hb.vec(pas()).weight().is_pos()?p.m_neg_sos:p.m_pos_sos)[p.m_psos[m_idx]]; }
iterator& operator++() { ++m_idx; fwd(); return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& it) const {return m_idx == it.m_idx; }
bool operator!=(iterator const& it) const {return m_idx != it.m_idx; }
};

1
src/math/hilbert/hilbert_basis.h
View file

@ -115,7 +115,6 @@ class hilbert_basis {
offset_t operator*() const { return hb.m_basis[m_idx]; }
iterator& operator++() { ++m_idx; return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& it) const {return m_idx == it.m_idx; }
bool operator!=(iterator const& it) const {return m_idx != it.m_idx; }
};

4
src/math/interval/mod_interval.h
View file

@ -26,7 +26,7 @@ namespace bv {
bool tight = true;
interval_tpl(T const& l, T const& h, unsigned sz, bool tight = false): l(l), h(h), sz(sz), tight(tight) {}
interval_tpl() {}
interval_tpl() = default;
bool invariant() const {
return
@ -167,7 +167,7 @@ namespace bv {
iinterval i;
rinterval r;
interval() {}
interval() = default;
interval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
if (sz <= 64) {

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

@ -21,7 +21,5 @@ Revision History:
#include "math/lp/core_solver_pretty_printer_def.h"
template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out);
template void lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::print();
template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::~core_solver_pretty_printer();
template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> > &, std::ostream & out);
template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::~core_solver_pretty_printer();
template void lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::print();

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

@ -66,7 +66,6 @@ public:
void init_costs();
~core_solver_pretty_printer();
void init_rs_width();
T current_column_norm();

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

@ -67,8 +67,6 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_co
}
template <typename T, typename X> core_solver_pretty_printer<T, X>::~core_solver_pretty_printer() {
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_rs_width() {
m_rs_width = static_cast<unsigned>(T_to_string(m_core_solver.get_cost()).size());
for (unsigned i = 0; i < nrows(); i++) {

7
src/math/lp/emonics.h
View file

@ -51,9 +51,8 @@ class emonics {
unsigned m_index;
};
struct head_tail {
head_tail(): m_head(nullptr), m_tail(nullptr) {}
cell* m_head;
cell* m_tail;
cell* m_head = nullptr;
cell* m_tail = nullptr;
};
struct hash_canonical {
emonics& em;
@ -205,7 +204,6 @@ public:
monic & operator*() { return m.m_monics[m_cell->m_index]; }
iterator& operator++() { m_touched = true; m_cell = m_cell->m_next; return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& other) const { return m_cell == other.m_cell && m_touched == other.m_touched; }
bool operator!=(iterator const& other) const { return m_cell != other.m_cell || m_touched != other.m_touched; }
};
@ -239,7 +237,6 @@ public:
}
pf_iterator& operator++() { ++m_it; fast_forward(); return *this; }
pf_iterator operator++(int) { pf_iterator tmp = *this; ++*this; return tmp; }
bool operator==(pf_iterator const& other) const { return m_it == other.m_it; }
bool operator!=(pf_iterator const& other) const { return m_it != other.m_it; }
};

7
src/math/lp/explanation.h
View file

@ -29,7 +29,7 @@ class explanation {
vector<std::pair<constraint_index, mpq>> m_vector;
ci_set m_set;
public:
explanation() {}
explanation() = default;
template <typename T>
explanation(const T& t) {
@ -106,11 +106,10 @@ public:
iterator(bool run_on_vector, pair_vec::const_iterator vi, ci_set::iterator cii) :
m_run_on_vector(run_on_vector), m_vi(vi), m_ci(cii)
{}
bool operator==(const iterator &other) const {
bool operator!=(const iterator &other) const {
SASSERT(m_run_on_vector == other.m_run_on_vector);
return m_run_on_vector? m_vi == other.m_vi : m_ci == other.m_ci;
return m_run_on_vector ? m_vi != other.m_vi : m_ci != other.m_ci;
}
bool operator!=(const iterator &other) const { return !(*this == other); }
};
iterator begin() const {

12
src/math/lp/factorization.cpp
View file

@ -97,14 +97,12 @@ const_iterator_mon::const_iterator_mon(const bool_vector& mask, const factorizat
m_ff(f) ,
m_full_factorization_returned(false)
{}
bool const_iterator_mon::operator==(const const_iterator_mon::self_type &other) const {
return
m_full_factorization_returned == other.m_full_factorization_returned &&
m_mask == other.m_mask;
}
bool const_iterator_mon::operator!=(const const_iterator_mon::self_type &other) const { return !(*this == other); }
bool const_iterator_mon::operator!=(const const_iterator_mon::self_type &other) const {
return
m_full_factorization_returned != other.m_full_factorization_returned ||
m_mask != other.m_mask;
}
factorization const_iterator_mon::create_binary_factorization(factor j, factor k) const {
factorization f(nullptr);

5
src/math/lp/factorization.h
View file

@ -24,7 +24,7 @@ class factor {
factor_type m_type = factor_type::VAR;
bool m_sign = false;
public:
factor() { }
factor() = default;
explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t) {}
unsigned var() const { return m_var; }
factor_type type() const { return m_type; }
@ -88,8 +88,7 @@ struct const_iterator_mon {
self_type operator++(int);
const_iterator_mon(const bool_vector& mask, const factorization_factory *f);
bool operator==(const self_type &other) const;
bool operator!=(const self_type &other) const;
factorization create_binary_factorization(factor j, factor k) const;

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

@ -180,7 +180,7 @@ public:
m_column_permutation.transpose_from_left(j, k);
}
general_matrix(){}
general_matrix() = default;
general_matrix(unsigned n) :
m_row_permutation(n),
m_column_permutation(n),

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

@ -527,7 +527,7 @@ public:
has_small_cut = true;
add_cut(cc.m_t, cc.m_k, cc.m_dep);
if (lia.settings().get_cancel_flag())
return lia_move::undef;
return lia_move::cancelled;
}
if (big_cuts.size()) {
@ -544,6 +544,9 @@ public:
if (!_check_feasible())
return lia_move::conflict;
if (lra.get_status() == lp_status::CANCELLED)
return lia_move::cancelled;
if (!lia.has_inf_int())
return lia_move::sat;

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

@ -19,8 +19,7 @@ namespace lp {
lia(lia),
lra(lia.lra),
m_settings(lia.settings()),
m_abs_max(zero_of_type<mpq>()),
m_var_register() {}
m_abs_max(zero_of_type<mpq>()) {}
bool hnf_cutter::is_full() const {
return

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

@ -44,7 +44,7 @@ class implied_bound {
k = static_cast<lconstraint_kind>(k / 2);
return k;
}
implied_bound(){}
implied_bound() = default;
implied_bound(const mpq & a,
unsigned j,
bool is_lower_bound,

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