diff --git a/CMakeLists.txt b/CMakeLists.txt
index 0ab59f18f..60531ca94 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -2,7 +2,7 @@
cmake_minimum_required(VERSION 3.16)
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.12.3.0 LANGUAGES CXX)
+project(Z3 VERSION 4.12.5.0 LANGUAGES CXX)
################################################################################
# Project version
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index f46f32a1a..9a7bc1856 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -9,7 +9,16 @@ Version 4.next
- polysat
- native word level bit-vector solving.
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
- - Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT.
+
+Version 4.12.5
+==============
+
+Version 4.12.4
+==============
+- Re-release fixing a few issues with 4.12:
+ - Python dependency on importlib.resources vs importlib_resources break automatic pypi installations. Supposedly fixed by conditioning dependency on Python 3.9 where the feature is built-in.
+ - Missing release of arm64 for Ubuntu.
+ - Futile attempt to streamline adding readme.md file as part of Nuget distribution. Nuget.org now requires a readme file. I was able to integrate the readme with the cmake build, but the cross-platform repackage in scripts/mk_nuget_task.py does not ingest a similar readme file with the CI pipelines.
Version 4.12.3
==============
@@ -23,6 +32,12 @@ Version 4.12.3
- Various (ongoing) performance fixes and improvements to smt.arith.solver=6
- A working version of solver.proof.trim=true option. Proofs logs created when using sat.smt=true may be trimmed by running z3
on the generated proof log using the option solver.proof.trim=true.
+- Optimizations LIA and NIA (linear integer arithmetic and non-linear integer (and real) arithmetic reasoning).
+ smt.arith.solver=6 is the default for most use cases. It trails smt.arith.solver=2 in some scenarios and the gap has been either removed or reduced.
+ smt.arith.solver=6 is complete for integrations of non-linear real arithmetic and theories, smt.arith.solver=2 is not.
+- qel: Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT.
+- added real-closed fields features to C API, exposed more RCF over OCaml API
+- fixes to FP
Version 4.12.2
==============
diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py
index cf7140e5e..d3f402773 100644
--- a/scripts/mk_nuget_task.py
+++ b/scripts/mk_nuget_task.py
@@ -24,13 +24,16 @@ def mk_dir(d):
os_info = { 'ubuntu-latest' : ('so', 'linux-x64'),
'ubuntu-18' : ('so', 'linux-x64'),
'ubuntu-20' : ('so', 'linux-x64'),
- 'x64-glibc-2.31' : ('so', 'linux-x64'),
+ 'x64-glibc-2.35' : ('so', 'linux-x64'),
'x64-win' : ('dll', 'win-x64'),
'x86-win' : ('dll', 'win-x86'),
'x64-osx' : ('dylib', 'osx-x64'),
- 'arm64-osx' : ('dylib', 'osx-arm64'),
'debian' : ('so', 'linux-x64') }
+# Nuget not supported for ARM
+#'arm-glibc-2.35' : ('so', 'linux-arm64'),
+#'arm64-osx' : ('dylib', 'osx-arm64'),
+
def classify_package(f, arch):
@@ -85,6 +88,8 @@ def mk_targets(source_root):
def mk_icon(source_root):
mk_dir("out/content")
shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg")
+ shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md")
+
def create_nuget_spec(version, repo, branch, commit, symbols, arch):
@@ -104,6 +109,7 @@ Linux Dependencies:
© Microsoft Corporation. All rights reserved.
smt constraint solver theorem prover
content/icon.jpg
+ content/README.md
https://github.com/Z3Prover/z3
MIT
@@ -113,6 +119,10 @@ Linux Dependencies:
+
+
+
+
""".format(version, repo, branch, commit, arch)
print(contents)
sym = "sym." if symbols else ""
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 876e0fd21..77bb1b680 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -8,7 +8,7 @@
from mk_util import *
def init_version():
- set_version(4, 12, 3, 0) # express a default build version or pick up ci build version
+ set_version(4, 12, 5, 0) # express a default build version or pick up ci build version
# Z3 Project definition
def init_project_def():
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 3d3996792..0728c2cb7 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1736,6 +1736,7 @@ class DotNetDLLComponent(Component):
true
Microsoft
Microsoft
+ README.md
false
Z3 is a satisfiability modulo theories solver from Microsoft Research.
Copyright Microsoft Corporation. All rights reserved.
@@ -1745,9 +1746,10 @@ class DotNetDLLComponent(Component):
+
-""" % (version, key, self.to_src_dir)
+""" % (version, key, self.to_src_dir, self.to_src_dir)
mk_dir(os.path.join(BUILD_DIR, 'dotnet'))
csproj = os.path.join('dotnet', 'z3.csproj')
diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml
index eebff5803..2b1b4ca3d 100644
--- a/scripts/nightly.yaml
+++ b/scripts/nightly.yaml
@@ -1,7 +1,7 @@
variables:
Major: '4'
Minor: '12'
- Patch: '3'
+ Patch: '5'
AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName)
diff --git a/scripts/release.yml b/scripts/release.yml
index b400860a7..76f8a8a57 100644
--- a/scripts/release.yml
+++ b/scripts/release.yml
@@ -6,7 +6,7 @@
trigger: none
variables:
- ReleaseVersion: '4.12.3'
+ ReleaseVersion: '4.12.5'
stages:
@@ -504,7 +504,7 @@ stages:
displayName: "Download Ubuntu Arm64"
inputs:
artifactName: 'UbuntuArm64'
- targetPath: tmp
+ path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: "Download Doc"
inputs:
@@ -583,7 +583,7 @@ stages:
# Enable on release:
- job: PyPIPublish
- condition: eq(1,0)
+ condition: eq(1,1)
displayName: "Publish to PyPI"
pool:
vmImage: "ubuntu-latest"
diff --git a/scripts/update_api.py b/scripts/update_api.py
index ddfb31f26..7d3d8899f 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1,4 +1,4 @@
-# - !/usr/bin/env python
+#!/usr/bin/env python
############################################
# Copyright (c) 2012 Microsoft Corporation
#
@@ -1831,7 +1831,10 @@ import atexit
import sys, os
import contextlib
import ctypes
-import importlib_resources
+if sys.version_info >= (3, 9):
+ import importlib.resources as importlib_resources
+else:
+ import importlib_resources
from .z3types import *
from .z3consts import *
diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in
index 85ab98b38..ec136809d 100644
--- a/src/api/dotnet/Microsoft.Z3.csproj.in
+++ b/src/api/dotnet/Microsoft.Z3.csproj.in
@@ -7,6 +7,8 @@
Microsoft.Z3
Microsoft.Z3
+ README.md
+
Z3 .NET Interface
Z3 .NET Interface
@@ -15,8 +17,8 @@
Z3 is a satisfiability modulo theories solver from Microsoft Research.
.NET Interface to the Z3 Theorem Prover
- Copyright (C) 2006-2019 Microsoft Corporation
- Copyright (C) 2006-2019 Microsoft Corporation
+ Copyright (C) 2006- Microsoft Corporation
+ Copyright (C) 2006- Microsoft Corporation
Microsoft Corporation
Microsoft Corporation
@@ -65,6 +67,11 @@
${Z3_DOTNET_COMPILE_ITEMS}
+
+
+
+
+
diff --git a/src/api/dotnet/README.md b/src/api/dotnet/README.md
new file mode 100644
index 000000000..fe614782f
--- /dev/null
+++ b/src/api/dotnet/README.md
@@ -0,0 +1,3 @@
+# Z3 Nuget Package
+
+For more information see [the Z3 github page](https://github.com/z3prover/z3.git)
diff --git a/src/api/python/setup.py b/src/api/python/setup.py
index 1837b5bec..325fb4230 100644
--- a/src/api/python/setup.py
+++ b/src/api/python/setup.py
@@ -18,7 +18,7 @@ from setuptools.command.bdist_egg import bdist_egg as _bdist_egg
build_env = dict(os.environ)
build_env['PYTHON'] = sys.executable
-build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -std=c++11"
+build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -std=c++17"
# determine where we're building and where sources are
ROOT_DIR = os.path.abspath(os.path.dirname(__file__))
@@ -313,6 +313,8 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
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':
@@ -339,6 +341,7 @@ setup(
license='MIT License',
keywords=['z3', 'smt', 'sat', 'prover', 'theorem'],
packages=['z3'],
+ install_requires = ['importlib-resources'],
include_package_data=True,
package_data={
'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')]
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index f7a99f1c2..18d3abc9d 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1572,7 +1572,12 @@ class BoolRef(ExprRef):
return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
def __add__(self, other):
- return If(self, 1, 0) + If(other, 1, 0)
+ if isinstance(other, BoolRef):
+ other = If(other, 1, 0)
+ return If(self, 1, 0) + other
+
+ def __radd__(self, other):
+ return self + other
def __rmul__(self, other):
return self * other
@@ -1593,6 +1598,9 @@ class BoolRef(ExprRef):
def __or__(self, other):
return Or(self, other)
+
+ def __xor__(self, other):
+ return Xor(self, other)
def __invert__(self):
return Not(self)
diff --git a/src/ast/polymorphism_inst.cpp b/src/ast/polymorphism_inst.cpp
index 4da83ee10..aa9b1e5fe 100644
--- a/src/ast/polymorphism_inst.cpp
+++ b/src/ast/polymorphism_inst.cpp
@@ -94,7 +94,10 @@ namespace polymorphism {
t.push(value_trail(m_decl_qhead));
for (; m_decl_qhead < num_decls; ++m_decl_qhead) {
func_decl* p = m_decl_queue.get(m_decl_qhead);
- for (expr* e : m_occurs[m.poly_root(p)])
+ func_decl* r = m.poly_root(p);
+ if (!m_occurs.contains(r))
+ continue;
+ for (expr* e : m_occurs[r])
instantiate(p, e, instances);
}
}
diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index 9a9e4566b..5d0e664f2 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -611,4 +611,19 @@ void emonics::set_propagated(monic const& m) {
m_u_f_stack.push(set_unpropagated(*this, m.var()));
}
+void emonics::set_bound_propagated(monic const& m) {
+ struct set_bound_unpropagated : public trail {
+ emonics& em;
+ unsigned var;
+ public:
+ set_bound_unpropagated(emonics& em, unsigned var): em(em), var(var) {}
+ void undo() override {
+ em[var].set_bound_propagated(false);
+ }
+ };
+ SASSERT(!m.is_bound_propagated());
+ (*this)[m.var()].set_bound_propagated(true);
+ m_u_f_stack.push(set_bound_unpropagated(*this, m.var()));
+}
+
}
diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h
index fe0b19117..55086515d 100644
--- a/src/math/lp/emonics.h
+++ b/src/math/lp/emonics.h
@@ -143,6 +143,7 @@ public:
void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
void set_propagated(monic const& m);
+ void set_bound_propagated(monic const& m);
// this method is required by union_find
trail_stack & get_trail_stack() { return m_u_f_stack; }
diff --git a/src/math/lp/monic.h b/src/math/lp/monic.h
index d981b2042..19137cd31 100644
--- a/src/math/lp/monic.h
+++ b/src/math/lp/monic.h
@@ -59,6 +59,7 @@ class monic: public mon_eq {
bool m_rsign;
mutable unsigned m_visited;
bool m_propagated = false;
+ bool m_bound_propagated = false;
public:
// constructors
monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx):
@@ -77,6 +78,8 @@ public:
void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); }
void set_propagated(bool p) { m_propagated = p; }
bool is_propagated() const { return m_propagated; }
+ void set_bound_propagated(bool p) { m_bound_propagated = p; }
+ bool is_bound_propagated() const { return m_bound_propagated; }
svector::const_iterator begin() const { return vars().begin(); }
svector::const_iterator end() const { return vars().end(); }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 96f1b4a30..f36fab52e 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1517,6 +1517,9 @@ void core::add_bounds() {
for (lpvar j : m.vars()) {
if (!var_is_free(j))
continue;
+ if (m.is_bound_propagated())
+ continue;
+ m_emons.set_bound_propagated(m);
// split the free variable (j <= 0, or j > 0), and return
m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
TRACE("nla_solver", print_ineq(m_literals.back(), tout) << "\n");
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index baf27a5bb..f9974b41c 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -59,21 +59,20 @@ namespace nla {
if (m_delay_base > 0)
--m_delay_base;
- if (is_conflicting())
- return;
-
try {
- if (propagate_bounds())
+
+ if (is_conflicting())
return;
if (propagate_eqs())
return;
-
+
if (propagate_factorization())
return;
-
+
if (propagate_linear_equations())
return;
+
}
catch (...) {
@@ -111,17 +110,9 @@ namespace nla {
return false;
}
- 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())
+ for (auto eq : m_solver.equations())
if (propagate_fixed(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
return true;
return changed > 0;
@@ -129,7 +120,7 @@ namespace nla {
bool grobner::propagate_factorization() {
unsigned changed = 0;
- for (auto eq : m_solver.equations())
+ for (auto eq : m_solver.equations())
if (propagate_factorization(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
return true;
return changed > 0;
@@ -165,19 +156,12 @@ namespace nla {
rational d = lcm(denominator(a), denominator(b));
a *= d;
b *= d;
-#if 0
- c().lra.update_column_type_and_bound(v, lp::lconstraint_kind::EQ, b/a, eq.dep());
- lp::explanation exp;
- explain(eq, exp);
- c().add_fixed_equality(c().lra.column_to_reported_index(v), b/a, exp);
-#else
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;
-#endif
return true;
}
@@ -377,73 +361,18 @@ namespace nla {
}
}
- 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(j, a);
- else c().m_intervals.set_var_interval(j, a);
- };
- scoped_dep_interval i(di), i_wd(di);
- eval.get_interval(e.poly(), i);
- return false;
- }
-
bool grobner::propagate_linear_equations() {
unsigned changed = 0;
m_mon2var.clear();
for (auto const& m : c().emons())
m_mon2var[m.vars()] = m.var();
+
for (auto eq : m_solver.equations())
if (propagate_linear_equations(*eq))
++changed;
-#if 0
- for (auto eq : m_solver.equations())
- if (check_missed_bound(*eq))
- return true;
-#endif
return changed > 0;
}
-
- bool grobner::check_missed_bound(dd::solver::equation const& e) {
- auto& di = c().m_intervals.get_dep_intervals();
- auto set_var_interval = [&](lpvar j, scoped_dep_interval& a) {
- c().m_intervals.set_var_interval(j, a);
- };
- scoped_dep_interval i(di), t(di), s(di), u(di);
- di.set_value(i, rational::zero());
-
- for (auto const& [coeff, vars] : e.poly()) {
- if (vars.empty())
- di.add(coeff, i);
- else {
- di.set_value(t, coeff);
- for (auto v : vars) {
- set_var_interval(v, s);
- di.mul(t, s, t);
- }
- if (m_mon2var.find(vars) != m_mon2var.end()) {
- auto v = m_mon2var.find(vars)->second;
- set_var_interval(v, u);
- di.mul(coeff, u, u);
- di.intersect(t, u, t);
- }
- di.add(i, t, i);
- }
- }
- if (!di.separated_from_zero(i))
- return false;
-// m_solver.display(verbose_stream() << "missed bound\n", e);
-// exit(1);
- std::function f = [this](const lp::explanation& e) {
- new_lemma lemma(m_core, "pdd");
- lemma &= e;
- };
- return di.check_interval_for_conflict_on_zero(i, e.dep(), f);
- }
-
+
bool grobner::propagate_linear_equations(dd::solver::equation const& e) {
if (equation_is_true(e))
return false;
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index e70b5473d..be5f06136 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -35,20 +35,14 @@ namespace nla {
bool is_conflicting();
bool is_conflicting(dd::solver::equation const& eq);
- bool propagate_bounds();
- bool propagate_bounds(dd::solver::equation const& eq);
-
bool propagate_eqs();
bool propagate_fixed(dd::solver::equation const& eq);
bool propagate_factorization();
bool propagate_factorization(dd::solver::equation const& eq);
-
bool propagate_linear_equations();
bool propagate_linear_equations(dd::solver::equation const& eq);
-
- bool check_missed_bound(dd::solver::equation const& eq);
void add_dependencies(new_lemma& lemma, dd::solver::equation const& eq);
void explain(dd::solver::equation const& eq, lp::explanation& exp);
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 3a437855e..0361fc157 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -164,7 +164,7 @@ namespace sat {
unsigned m_rephase_inc;
backoff m_rephase;
backoff m_reorder;
- var_queue m_case_split_queue;
+ var_queue m_case_split_queue;
unsigned m_qhead;
unsigned m_scope_lvl;
unsigned m_search_lvl;
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index d1216c171..cfc1f06f2 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -509,10 +509,10 @@ namespace smt {
// Assuming `app` is equal to a constructor term, return the constructor enode
inline enode * theory_datatype::oc_get_cstor(enode * app) {
theory_var v = app->get_root()->get_th_var(get_id());
- SASSERT(v != null_theory_var);
+ if (v == null_theory_var)
+ return nullptr;
v = m_find.find(v);
var_data * d = m_var_data[v];
- SASSERT(d->m_constructor);
return d->m_constructor;
}
@@ -802,8 +802,9 @@ namespace smt {
return false;
func_decl* con = m_util.get_accessor_constructor(f);
for (enode* app : ctx.enodes_of(f)) {
- enode* arg = app->get_arg(0)->get_root();
- if (is_constructor(arg) && arg->get_decl() != con)
+ enode* arg = app->get_arg(0);
+ enode* arg_con = oc_get_cstor(arg);
+ if (arg_con && is_constructor(arg_con) && arg_con->get_decl() != con)
return true;
}
return false;
diff --git a/src/util/dlist.h b/src/util/dlist.h
index e5c95b8cf..07aefa97e 100644
--- a/src/util/dlist.h
+++ b/src/util/dlist.h
@@ -223,6 +223,16 @@ public:
}
};
+template
+class dll_elements {
+ T const* m_list;
+public:
+ dll_elements(T const* list) : m_list(list) {}
+ dll_iterator begin() const { return dll_iterator::mk_begin(m_list); }
+ dll_iterator end() const { return dll_iterator::mk_end(m_list); }
+};
+
+
template < typename T
, typename U = std::enable_if_t, T>> // should only match if T actually inherits from dll_base
>
diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp
index 324750cfa..f90843e36 100644
--- a/src/util/mpq.cpp
+++ b/src/util/mpq.cpp
@@ -316,6 +316,12 @@ unsigned mpq_manager::prev_power_of_two(mpq const & a) {
return prev_power_of_two(_tmp);
}
+template
+unsigned mpq_manager::next_power_of_two(mpq const & a) {
+ _scoped_numeral > _tmp(*this);
+ ceil(a, _tmp);
+ return next_power_of_two(_tmp);
+}
template
template
diff --git a/src/util/mpq.h b/src/util/mpq.h
index e254ade69..1bdf8f31b 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -848,6 +848,14 @@ public:
unsigned prev_power_of_two(mpz const & a) { return mpz_manager::prev_power_of_two(a); }
unsigned prev_power_of_two(mpq const & a);
+ /**
+ \brief Return the smallest k s.t. a <= 2^k.
+
+ \remark Return 0 if a is not positive.
+ */
+ unsigned next_power_of_two(mpz const & a) { return mpz_manager::next_power_of_two(a); }
+ unsigned next_power_of_two(mpq const & a);
+
bool is_int_perfect_square(mpq const & a, mpq & r) {
SASSERT(is_int(a));
reset_denominator(r);
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index c3ba30161..296b4426e 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -2288,6 +2288,19 @@ unsigned mpz_manager::bitsize(mpz const & a) {
return mlog2(a) + 1;
}
+template
+unsigned mpz_manager::next_power_of_two(mpz const & a) {
+ if (is_nonpos(a))
+ return 0;
+ if (is_one(a))
+ return 0;
+ unsigned shift;
+ if (is_power_of_two(a, shift))
+ return shift;
+ else
+ return log2(a) + 1;
+}
+
template
bool mpz_manager::is_perfect_square(mpz const & a, mpz & root) {
if (is_neg(a))
diff --git a/src/util/mpz.h b/src/util/mpz.h
index a1bb19395..bb1141ea7 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -692,6 +692,13 @@ public:
\remark Return 0 if a is not positive.
*/
unsigned prev_power_of_two(mpz const & a) { return log2(a); }
+
+ /**
+ \brief Return the smallest k s.t. a <= 2^k.
+
+ \remark Return 0 if a is not positive.
+ */
+ unsigned next_power_of_two(mpz const & a);
/**
\brief Return true if a^{1/n} is an integer, and store the result in a.
diff --git a/src/util/rational.h b/src/util/rational.h
index f47fddefe..88a0552ba 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -55,7 +55,7 @@ public:
explicit rational(double z) { UNREACHABLE(); }
explicit rational(char const * v) { m().set(m_val, v); }
-
+
explicit rational(unsigned const * v, unsigned sz) { m().set(m_val, sz, v); }
struct i64 {};
@@ -489,6 +489,18 @@ public:
return get_num_digits(rational(10));
}
+ /**
+ * \brief Return the biggest k s.t. 2^k <= a.
+ * \remark Return 0 if a is not positive.
+ */
+ unsigned prev_power_of_two() const { return m().prev_power_of_two(m_val); }
+
+ /**
+ * \brief Return the smallest k s.t. a <= 2^k.
+ * \remark Return 0 if a is not positive.
+ */
+ unsigned next_power_of_two() const { return m().next_power_of_two(m_val); }
+
bool get_bit(unsigned index) const {
return m().get_bit(m_val, index);
}
@@ -501,6 +513,15 @@ public:
return k;
}
+ /** Number of trailing zeros in an N-bit representation */
+ unsigned parity(unsigned num_bits) const {
+ SASSERT(!is_neg());
+ SASSERT(*this < rational::power_of_two(num_bits));
+ if (is_zero())
+ return num_bits;
+ return trailing_zeros();
+ }
+
static bool limit_denominator(rational &num, rational const& limit);
};
@@ -649,3 +670,7 @@ inline rational gcd(rational const & r1, rational const & r2, rational & a, rati
rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val);
return result;
}
+
+inline void swap(rational& r1, rational& r2) {
+ r1.swap(r2);
+}
diff --git a/src/util/var_queue.h b/src/util/var_queue.h
index 7245153ca..0af4de3b8 100644
--- a/src/util/var_queue.h
+++ b/src/util/var_queue.h
@@ -21,20 +21,20 @@ Revision History:
#include "util/heap.h"
-
+template
class var_queue {
typedef unsigned var;
struct lt {
- svector & m_activity;
- lt(svector & act):m_activity(act) {}
+ ActivityVector & m_activity;
+ lt(ActivityVector & act):m_activity(act) {}
bool operator()(var v1, var v2) const { return m_activity[v1] > m_activity[v2]; }
};
heap m_queue;
-public:
+public:
- var_queue(svector & act):m_queue(128, lt(act)) {}
+ var_queue(ActivityVector & act):m_queue(128, lt(act)) {}
void activity_increased_eh(var v) {
if (m_queue.contains(v))
@@ -68,6 +68,8 @@ public:
void reset() {
m_queue.reset();
}
+
+ bool contains(var v) const { return m_queue.contains(v); }
bool empty() const { return m_queue.empty(); }
@@ -90,11 +92,12 @@ public:
return out;
}
- using const_iterator = decltype(m_queue)::const_iterator;
+ using const_iterator = const int *;
const_iterator begin() const { return m_queue.begin(); }
const_iterator end() const { return m_queue.end(); }
};
-inline std::ostream& operator<<(std::ostream& out, var_queue const& queue) {
+template
+inline std::ostream& operator<<(std::ostream& out, var_queue const& queue) {
return queue.display(out);
}