mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Merge branch 'unstable' into contrib

Browse source
This commit is contained in:
Leonardo de Moura 2012-12-31 13:48:44 -08:00
parent fbce816025 a51c6d125d
commit 6a6015e335
19 changed files with 267 additions and 207 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
.gitignore vendored
View file

@ -1,5 +1,8 @@
*~
*.pyc
*.pyo
# Ignore callgrind files
callgrind.out.*
# .hpp files are automatically generated
*.hpp
.z3-trace

18
README
View file

@ -17,22 +17,24 @@ Execute:
make
sudo make install
It will install z3 executable at /usr/bin, libraries at /usr/lib, and include files at /usr/include.
You can change the installation p
By default, it will install z3 executable at PREFIX/bin, libraries at PREFIX/lib, and include files at PREFIX/include,
where PREFIX is the installation prefix used for installing Python in your system.
It is usually /usr for most Linux distros, and /usr/local for FreeBSD.
Use the following commands to install in a different prefix (e.g., /home/leo)
Use the following commands to install in a different prefix (e.g., /home/leo), and the Z3 python
bindings in a different python package directory.
python scripts/mk_make.py --prefix=/home/leo --pydir=/home/leo/python
python scripts/mk_make.py --prefix=/home/leo
cd build
make
sudo make install
make install
In this example, the Z3 Python bindings will be stored at /home/leo/lib/pythonX.Y/dist-packages,
where X.Y corresponds to the python version in your system.
To uninstall Z3, use
sudo make uninstall
3) Building Z3 using clang and clang++ on Linux/OSX
4) Building Z3 using clang and clang++ on Linux/OSX
Remark: clang does not support OpenMP yet.
CXX=clang++ CC=clang python scripts/mk_make.py

2
RELEASE_NOTES
View file

@ -51,6 +51,8 @@ Version 4.3.2
- Fixed timers on Linux and FreeBSD.
- Fixed crash reported at http://z3.codeplex.com/workitem/11.
Version 4.3.1
=============

64
scripts/mk_util.py
View file

@ -68,7 +68,7 @@ VER_MAJOR=None
VER_MINOR=None
VER_BUILD=None
VER_REVISION=None
PREFIX='/usr'
PREFIX=os.path.split(os.path.split(os.path.split(PYTHON_PACKAGE_DIR)[0])[0])[0]
GMP=False
VS_PAR=False
VS_PAR_NUM=8
@ -357,7 +357,6 @@ def display_help(exit_code):
print(" -s, --silent do not print verbose messages.")
if not IS_WINDOWS:
print(" -p <dir>, --prefix=<dir> installation prefix (default: %s)." % PREFIX)
print(" -y <dir>, --pydir=<dir> installation prefix for Z3 python bindings (default: %s)." % PYTHON_PACKAGE_DIR)
else:
print(" --parallel=num use cl option /MP with 'num' parallel processes")
print(" -b <sudir>, --build=<subdir> subdirectory where Z3 will be built (default: build).")
@ -393,9 +392,9 @@ def parse_options():
global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:dsxhmcvtnp:gjy:',
'b:dsxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir=', 'parallel='])
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel='])
except:
print("ERROR: Invalid command line option")
display_help(1)
@ -429,12 +428,13 @@ def parse_options():
STATIC_LIB = True
elif not IS_WINDOWS and opt in ('-p', '--prefix'):
PREFIX = arg
PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages')
mk_dir(PYTHON_PACKAGE_DIR)
if sys.version >= "3":
mk_dir(os.path.join(PYTHON_PACKAGE_DIR, '__pycache__'))
elif IS_WINDOWS and opt == '--parallel':
VS_PAR = True
VS_PAR_NUM = int(arg)
elif opt in ('-y', '--pydir'):
PYTHON_PACKAGE_DIR = arg
mk_dir(PYTHON_PACKAGE_DIR)
elif opt in ('-g', '--gmp'):
GMP = True
elif opt in ('-j', '--java'):
@ -1402,6 +1402,7 @@ def mk_config():
print('OpenMP: %s' % HAS_OMP)
print('Prefix: %s' % PREFIX)
print('64-bit: %s' % is64())
print('Python version: %s' % distutils.sysconfig.get_python_version())
if is_java_enabled():
print('Java Home: %s' % JAVA_HOME)
print('Java Compiler: %s' % JAVAC)
@ -1414,15 +1415,30 @@ def mk_install(out):
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'lib'))
for c in get_components():
c.mk_install(out)
out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR)
out.write('\t@cp z3*.py %s\n' % PYTHON_PACKAGE_DIR)
if sys.version >= "3":
out.write('\t@cp %s*.pyc %s\n' % (os.path.join('__pycache__', 'z3'),
os.path.join(PYTHON_PACKAGE_DIR, '__pycache__')))
else:
out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR)
out.write('\t@echo Z3 was successfully installed.\n')
if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
if os.uname()[0] == 'Darwin':
LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH"
else:
LD_LIBRARY_PATH = "LD_LIBRARY_PATH"
out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' %
(os.path.join(PREFIX, 'lib'), LD_LIBRARY_PATH))
out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
out.write('\n')
def mk_uninstall(out):
out.write('uninstall:\n')
for c in get_components():
c.mk_uninstall(out)
out.write('\t@rm -f %s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
out.write('\t@echo Z3 was successfully uninstalled.\n')
out.write('\n')
@ -1441,6 +1457,8 @@ def mk_makefile():
if c.main_component():
out.write(' %s' % c.name)
out.write('\n\t@echo Z3 was successfully built.\n')
out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % BUILD_DIR)
out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be also executed if \'%s\' directory is added to the PYTHONPATH environment variable.\"\n" % BUILD_DIR)
if not IS_WINDOWS:
out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
out.write('\t@echo " sudo make install"\n')
@ -1920,19 +1938,35 @@ def mk_def_files():
if c.require_def_file():
mk_def_file(c)
def cp_z3pyc_to_build():
def cp_z3py_to_build():
mk_dir(BUILD_DIR)
# Erase existing .pyc files
for root, dirs, files in os.walk(Z3PY_SRC_DIR):
for f in files:
if f.endswith('.pyc'):
rmf(os.path.join(root, f))
# Compile Z3Py files
if compileall.compile_dir(Z3PY_SRC_DIR, force=1) != 1:
raise MKException("failed to compile Z3Py sources")
# Copy sources to build
for py in filter(lambda f: f.endswith('.py'), os.listdir(Z3PY_SRC_DIR)):
shutil.copyfile(os.path.join(Z3PY_SRC_DIR, py), os.path.join(BUILD_DIR, py))
if is_verbose():
print("Copied '%s'" % py)
# Python 2.x support
for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(Z3PY_SRC_DIR)):
try:
os.remove(os.path.join(BUILD_DIR, pyc))
except:
pass
shutil.copyfile(os.path.join(Z3PY_SRC_DIR, pyc), os.path.join(BUILD_DIR, pyc))
os.remove(os.path.join(Z3PY_SRC_DIR, pyc))
if is_verbose():
print("Generated '%s'" % pyc)
# Python 3.x support
src_pycache = os.path.join(Z3PY_SRC_DIR, '__pycache__')
if os.path.exists(src_pycache):
for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)):
target_pycache = os.path.join(BUILD_DIR, '__pycache__')
mk_dir(target_pycache)
shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc))
if is_verbose():
print("Generated '%s'" % pyc)
def mk_bindings(api_files):
if not ONLY_MAKEFILES:
@ -1949,7 +1983,7 @@ def mk_bindings(api_files):
check_java()
mk_z3consts_java(api_files)
_execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
cp_z3pyc_to_build()
cp_z3py_to_build()
# Extract enumeration types from API files, and add python definitions.
def mk_z3consts_py(api_files):

2
src/api/api_context.h
View file

@ -54,7 +54,7 @@ namespace api {
datalog::dl_decl_util m_datalog_util;
// Support for old solver API
smt_params m_fparams;
smt_params m_fparams;
smt::kernel * m_solver; // General purpose solver for backward compatibility
// -------------------------------

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

@ -44,6 +44,7 @@ from z3core import *
from z3types import *
from z3consts import *
from z3printer import *
from fractions import Fraction
import sys
import io
@ -2523,6 +2524,15 @@ class RatNumRef(ArithRef):
"""
return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
def as_fraction(self):
"""Return a Z3 rational as a Python Fraction object.
>>> v = RealVal("1/5")
>>> v.as_fraction()
Fraction(1, 5)
"""
return Fraction(self.numerator_as_long(), self.denominator_as_long())
class AlgebraicNumRef(ArithRef):
"""Algebraic irrational values."""

9
src/api/python/z3num.py
View file

@ -8,6 +8,7 @@
from z3 import *
from z3core import *
from z3printer import *
from fractions import Fraction
def _to_numeral(num, ctx=None):
if isinstance(num, Numeral):
@ -170,6 +171,14 @@ class Numeral:
assert(self.is_integer())
return long(Z3_get_numeral_string(self.ctx_ref(), self.as_ast()))
def as_fraction(self):
""" Return a numeral (that is a rational) as a Python Fraction.
>>> Numeral("1/5").as_fraction()
Fraction(1, 5)
"""
assert(self.is_rational())
return Fraction(self.numerator().as_long(), self.denominator().as_long())
def approx(self, precision=10):
"""Return a numeral that approximates the numeral `self`.
The result `r` is such that |r - self| <= 1/10^precision

53
src/ast/arith_decl_plugin.cpp
View file

@ -206,6 +206,21 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
func_decl * e_decl = m->mk_const_decl(symbol("euler"), r, func_decl_info(id, OP_E));
m_e = m->mk_const(e_decl);
m->inc_ref(m_e);
func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT));
m_0_pw_0_int = m->mk_const(z_pw_z_int);
m->inc_ref(m_0_pw_0_int);
func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL));
m_0_pw_0_real = m->mk_const(z_pw_z_real);
m->inc_ref(m_0_pw_0_real);
MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r);
MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r);
MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i);
MK_UNARY(m_mod_0_decl, "mod0", OP_MOD_0, i);
MK_UNARY(m_u_asin_decl, "asin-u", OP_U_ASIN, r);
MK_UNARY(m_u_acos_decl, "acos-u", OP_U_ACOS, r);
}
arith_decl_plugin::arith_decl_plugin():
@ -253,7 +268,15 @@ arith_decl_plugin::arith_decl_plugin():
m_acosh_decl(0),
m_atanh_decl(0),
m_pi(0),
m_e(0) {
m_e(0),
m_0_pw_0_int(0),
m_0_pw_0_real(0),
m_neg_root_decl(0),
m_div_0_decl(0),
m_idiv_0_decl(0),
m_mod_0_decl(0),
m_u_asin_decl(0),
m_u_acos_decl(0) {
}
arith_decl_plugin::~arith_decl_plugin() {
@ -303,6 +326,14 @@ void arith_decl_plugin::finalize() {
DEC_REF(m_atanh_decl);
DEC_REF(m_pi);
DEC_REF(m_e);
DEC_REF(m_0_pw_0_int);
DEC_REF(m_0_pw_0_real);
DEC_REF(m_neg_root_decl);
DEC_REF(m_div_0_decl);
DEC_REF(m_idiv_0_decl);
DEC_REF(m_mod_0_decl);
DEC_REF(m_u_asin_decl);
DEC_REF(m_u_acos_decl);
m_manager->dec_array_ref(m_small_ints.size(), m_small_ints.c_ptr());
m_manager->dec_array_ref(m_small_reals.size(), m_small_reals.c_ptr());
}
@ -347,6 +378,14 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
case OP_ATANH: return m_atanh_decl;
case OP_PI: return m_pi->get_decl();
case OP_E: return m_e->get_decl();
case OP_0_PW_0_INT: return m_0_pw_0_int->get_decl();
case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl();
case OP_NEG_ROOT: return m_neg_root_decl;
case OP_DIV_0: return m_div_0_decl;
case OP_IDIV_0: return m_idiv_0_decl;
case OP_MOD_0: return m_mod_0_decl;
case OP_U_ASIN: return m_u_asin_decl;
case OP_U_ACOS: return m_u_acos_decl;
default: return 0;
}
}
@ -426,12 +465,20 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args
return true;
return false;
}
static bool is_const_op(decl_kind k) {
return
k == OP_PI ||
k == OP_E ||
k == OP_0_PW_0_INT ||
k == OP_0_PW_0_REAL;
}
func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (k == OP_NUM)
return mk_num_decl(num_parameters, parameters, arity);
if (arity == 0 && k != OP_PI && k != OP_E) {
if (arity == 0 && !is_const_op(k)) {
m_manager->raise_exception("no arguments supplied to arithmetical operator");
return 0;
}
@ -448,7 +495,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
unsigned num_args, expr * const * args, sort * range) {
if (k == OP_NUM)
return mk_num_decl(num_parameters, parameters, num_args);
if (num_args == 0 && k != OP_PI && k != OP_E) {
if (num_args == 0 && !is_const_op(k)) {
m_manager->raise_exception("no arguments supplied to arithmetical operator");
return 0;
}

34
src/ast/arith_decl_plugin.h
View file

@ -35,6 +35,7 @@ enum arith_sort_kind {
enum arith_op_kind {
OP_NUM, // rational & integers
OP_IRRATIONAL_ALGEBRAIC_NUM, // irrationals that are roots of polynomials with integer coefficients
//
OP_LE,
OP_GE,
OP_LT,
@ -67,6 +68,15 @@ enum arith_op_kind {
// constants
OP_PI,
OP_E,
// under-specified symbols
OP_0_PW_0_INT, // 0^0 for integers
OP_0_PW_0_REAL, // 0^0 for reals
OP_NEG_ROOT, // x^n when n is even and x is negative
OP_DIV_0, // x/0
OP_IDIV_0, // x div 0
OP_MOD_0, // x mod 0
OP_U_ASIN, // asin(x) for x < -1 or x > 1
OP_U_ACOS, // acos(x) for x < -1 or x > 1
LAST_ARITH_OP
};
@ -126,7 +136,16 @@ protected:
app * m_pi;
app * m_e;
app * m_0_pw_0_int;
app * m_0_pw_0_real;
func_decl * m_neg_root_decl;
func_decl * m_div_0_decl;
func_decl * m_idiv_0_decl;
func_decl * m_mod_0_decl;
func_decl * m_u_asin_decl;
func_decl * m_u_acos_decl;
ptr_vector<app> m_small_ints;
ptr_vector<app> m_small_reals;
@ -182,6 +201,10 @@ public:
app * mk_e() const { return m_e; }
app * mk_0_pw_0_int() const { return m_0_pw_0_int; }
app * mk_0_pw_0_real() const { return m_0_pw_0_real; }
virtual expr * get_some_value(sort * s);
virtual void set_cancel(bool f);
@ -339,6 +362,15 @@ public:
app * mk_pi() { return plugin().mk_pi(); }
app * mk_e() { return plugin().mk_e(); }
app * mk_0_pw_0_int() { return plugin().mk_0_pw_0_int(); }
app * mk_0_pw_0_real() { return plugin().mk_0_pw_0_real(); }
app * mk_div0(expr * arg) { return m_manager.mk_app(m_afid, OP_DIV_0, arg); }
app * mk_idiv0(expr * arg) { return m_manager.mk_app(m_afid, OP_IDIV_0, arg); }
app * mk_mod0(expr * arg) { return m_manager.mk_app(m_afid, OP_MOD_0, arg); }
app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); }
app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); }
app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); }
/**
\brief Return the equality (= lhs rhs), but it makes sure that
if one of the arguments is a numeral, then it will be in the right-hand-side;

13
src/ast/array_decl_plugin.cpp
View file

@ -113,15 +113,14 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const *
m_manager->raise_exception("invalid const array definition, invalid domain size");
return 0;
}
unsigned num_parameters = s->get_num_parameters();
if (num_parameters == 0) {
m_manager->raise_exception("parameter mismatch");
if (!is_array_sort(s)) {
m_manager->raise_exception("invalid const array definition, parameter is not an array sort");
return 0;
}
if (!m_manager->compatible_sorts(get_array_range(s), domain[0])) {
m_manager->raise_exception("invalid const array definition, sort mismatch between array range and argument");
return 0;
}
// TBD check that range sort corresponds to last parameter.
parameter param(s);
func_decl_info info(m_family_id, OP_CONST_ARRAY, 1, &param);
info.m_private_parameters = true;

9
src/ast/rewriter/array_rewriter.cpp
View file

@ -292,7 +292,14 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
}
expr * fv = m().mk_app(f, values.size(), values.c_ptr());
parameter p(m().get_sort(args[0]));
sort * in_s = get_sort(args[0]);
ptr_vector<sort> domain;
unsigned domain_sz = get_array_arity(in_s);
for (unsigned i = 0; i < domain_sz; i++)
domain.push_back(get_array_domain(in_s, i));
sort_ref out_s(m());
out_s = m_util.mk_array_sort(domain_sz, domain.c_ptr(), f->get_range());
parameter p(out_s.get());
result = m().mk_app(get_fid(), OP_CONST_ARRAY, 1, &p, 1, &fv);
return BR_REWRITE2;
}

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

@ -63,6 +63,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
m_blast_eq_value = p.blast_eq_value();
m_split_concat_eq = p.split_concat_eq();
m_udiv2mul = p.udiv2mul();
m_bvnot2arith = p.bvnot2arith();
m_mkbv2num = _p.get_bool("mkbv2num", false);
}
@ -1527,6 +1528,14 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
}
#endif
if (m_bvnot2arith) {
// (bvnot x) --> (bvsub -1 x)
bv_size = get_bv_size(arg);
rational minus_one = (rational::power_of_two(bv_size) - numeral(1));
result = m_util.mk_bv_sub(m_util.mk_numeral(minus_one, bv_size), arg);
return BR_REWRITE1;
}
return BR_FAILED;
}

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

@ -67,6 +67,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
bool m_mkbv2num;
bool m_split_concat_eq;
bool m_udiv2mul;
bool m_bvnot2arith;
bool is_zero_bit(expr * x, unsigned idx);

4
src/ast/rewriter/bv_rewriter_params.pyg
View file

@ -7,4 +7,6 @@ def_module_params(module_name='rewriter',
("blast_eq_value", BOOL, False, "blast (some) Bit-vector equalities into bits"),
("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"),
("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation")))
("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)")
))

68
src/muz_qe/dl_mk_slice.cpp
View file

@ -429,6 +429,29 @@ namespace datalog {
}
}
void mk_slice::filter_unique_vars(rule& r) {
//
// Variables that occur in multiple uinterpreted predicates are not sliceable.
//
uint_set used_vars;
for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) {
app* p = r.get_tail(j);
for (unsigned i = 0; i < p->get_num_args(); ++i) {
expr* v = p->get_arg(i);
if (is_var(v)) {
unsigned vi = to_var(v)->get_idx();
add_var(vi);
if (used_vars.contains(vi)) {
m_var_is_sliceable[vi] = false;
}
else {
used_vars.insert(vi);
}
}
}
}
}
void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) {
expr_ref_vector conjs = get_tail_conjs(r);
for (unsigned j = 0; j < conjs.size(); ++j) {
@ -475,6 +498,7 @@ namespace datalog {
}
}
}
filter_unique_vars(r);
//
// Collect the set of variables that are solved.
// Collect the occurrence count of the variables per conjunct.
@ -750,51 +774,11 @@ namespace datalog {
m_solved_vars.reset();
#if 0
uint_set used_vars;
expr_ref b(m);
TBD: buggy code:
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
if (is_eq(e, v, b)) {
if (v >= m_solved_vars.size()) {
m_solved_vars.resize(v+1);
}
if (v < sorts.size() && sorts[v]) {
TRACE("dl", tout << "already bound " << mk_pp(e, m) << "\n";);
add_free_vars(used_vars, e);
}
else if (m_solved_vars[v].get()) {
TRACE("dl", tout << "already solved " << mk_pp(e, m) << "\n";);
add_free_vars(used_vars, e);
add_free_vars(used_vars, m_solved_vars[v].get());
used_vars.insert(v);
}
else {
TRACE("dl", tout << "new solution " << mk_pp(e, m) << "\n";);
m_solved_vars[v] = b;
}
}
else {
TRACE("dl", tout << "not solved " << mk_pp(e, m) << "\n";);
add_free_vars(used_vars, e);
}
tail.push_back(to_app(e));
}
#endif
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
#if 0
if (false && is_eq(e, v, b) && m_solved_vars[v].get() && !used_vars.contains(v)) {
TRACE("dl", tout << "removing conjunct: " << mk_pp(e, m) << "\n";);
// skip conjunct
}
#endif
tail.push_back(to_app(e));
}
new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0);
rm.fix_unbound_vars(new_rule, false);

2
src/muz_qe/dl_mk_slice.h
View file

@ -89,6 +89,8 @@ namespace datalog {
void update_predicate(app* p, app_ref& q);
void filter_unique_vars(rule& r);
void solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars);
public:

56
src/muz_qe/qe_lite.cpp
View file

@ -971,15 +971,15 @@ namespace fm {
}
bool is_linear_ineq(expr * t) const {
bool result = false;
m.is_not(t, t);
expr * lhs, * rhs;
TRACE("is_occ_bug", tout << mk_pp(t, m) << "\n";);
if (m_util.is_le(t, lhs, rhs) || m_util.is_ge(t, lhs, rhs)) {
if (!m_util.is_numeral(rhs))
return false;
return is_linear_pol(lhs);
result = m_util.is_numeral(rhs) && is_linear_pol(lhs);
}
return false;
TRACE("qe_lite", tout << mk_pp(t, m) << " " << (result?"true":"false") << "\n";);
return result;
}
bool is_occ(expr * t) {
@ -1049,7 +1049,7 @@ namespace fm {
cnstr->m_xs = reinterpret_cast<var*>(mem_xs);
cnstr->m_as = reinterpret_cast<rational*>(mem_as);
for (unsigned i = 0; i < num_vars; i++) {
TRACE("mk_constraint_bug", tout << "xs[" << i << "]: " << xs[i] << "\n";);
TRACE("qe_lite", tout << "xs[" << i << "]: " << xs[i] << "\n";);
cnstr->m_xs[i] = xs[i];
new (cnstr->m_as + i) rational(as[i]);
}
@ -1241,7 +1241,7 @@ namespace fm {
if (c2->m_dead)
continue;
if (subsumes(c, *c2)) {
TRACE("fm_subsumption", display(tout, c); tout << "\nsubsumed:\n"; display(tout, *c2); tout << "\n";);
TRACE("qe_lite", display(tout, c); tout << "\nsubsumed:\n"; display(tout, *c2); tout << "\n";);
c2->m_dead = true;
continue;
}
@ -1284,12 +1284,12 @@ namespace fm {
}
void updt_params() {
m_fm_real_only = true;
m_fm_real_only = false;
m_fm_limit = 5000000;
m_fm_cutoff1 = 8;
m_fm_cutoff2 = 256;
m_fm_extra = 0;
m_fm_occ = false;
m_fm_occ = true;
}
void set_cancel(bool f) {
@ -1318,7 +1318,7 @@ namespace fm {
expr * f = g[i];
if (is_occ(f))
continue;
TRACE("is_occ_bug", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";);
TRACE("qe_lite", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";);
quick_for_each_expr(proc, visited, f);
}
}
@ -1447,6 +1447,7 @@ namespace fm {
SASSERT(m_uppers.size() == m_is_int.size());
SASSERT(m_forbidden.size() == m_is_int.size());
SASSERT(m_var2pos.size() == m_is_int.size());
TRACE("qe_lite", tout << mk_pp(t,m) << " |-> " << x << " forbidden: " << forbidden << "\n";);
return x;
}
@ -1468,7 +1469,7 @@ namespace fm {
x = mk_var(t);
SASSERT(m_expr2var.contains(t));
SASSERT(m_var2expr.get(x) == t);
TRACE("to_var_bug", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";);
TRACE("qe_lite", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";);
return x;
}
@ -1488,6 +1489,7 @@ namespace fm {
void add_constraint(expr * f, expr_dependency * dep) {
TRACE("qe_lite", tout << mk_pp(f, m) << "\n";);
SASSERT(!m.is_or(f) || m_fm_occ);
sbuffer<literal> lits;
sbuffer<var> xs;
@ -1524,7 +1526,7 @@ namespace fm {
neg = !neg;
expr * lhs = to_app(l)->get_arg(0);
expr * rhs = to_app(l)->get_arg(1);
m_util.is_numeral(rhs, c);
VERIFY (m_util.is_numeral(rhs, c));
if (neg)
c.neg();
unsigned num_mons;
@ -1567,7 +1569,7 @@ namespace fm {
}
}
TRACE("to_var_bug", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";);
TRACE("qe_lite", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";);
constraint * new_c = mk_constraint(lits.size(),
lits.c_ptr(),
@ -1578,7 +1580,7 @@ namespace fm {
strict,
dep);
TRACE("to_var_bug", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";);
TRACE("qe_lite", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";);
VERIFY(register_constraint(new_c));
}
@ -1591,7 +1593,7 @@ namespace fm {
if (is_false(*c)) {
del_constraint(c);
m_inconsistent = true;
TRACE("add_constraint_bug", tout << "is false "; display(tout, *c); tout << "\n";);
TRACE("qe_lite", tout << "is false "; display(tout, *c); tout << "\n";);
return false;
}
@ -1614,7 +1616,7 @@ namespace fm {
return true;
}
else {
TRACE("add_constraint_bug", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";);
TRACE("qe_lite", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";);
m_new_fmls.push_back(to_expr(*c));
del_constraint(c);
return false;
@ -1668,7 +1670,7 @@ namespace fm {
}
// x_cost_lt is not a total order on variables
std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int));
TRACE("fm",
TRACE("qe_lite",
svector<x_cost>::iterator it2 = x_cost_vector.begin();
svector<x_cost>::iterator end2 = x_cost_vector.end();
for (; it2 != end2; ++it2) {
@ -1854,7 +1856,7 @@ namespace fm {
if (new_xs.empty() && (new_c.is_pos() || (!new_strict && new_c.is_zero()))) {
// literal is true
TRACE("fm", tout << "resolution " << x << " consequent literal is always true: \n";
TRACE("qe_lite", tout << "resolution " << x << " consequent literal is always true: \n";
display(tout, l);
tout << "\n";
display(tout, u); tout << "\n";);
@ -1898,7 +1900,7 @@ namespace fm {
}
if (tautology) {
TRACE("fm", tout << "resolution " << x << " tautology: \n";
TRACE("qe_lite", tout << "resolution " << x << " tautology: \n";
display(tout, l);
tout << "\n";
display(tout, u); tout << "\n";);
@ -1908,7 +1910,7 @@ namespace fm {
expr_dependency * new_dep = m.mk_join(l.m_dep, u.m_dep);
if (new_lits.empty() && new_xs.empty() && (new_c.is_neg() || (new_strict && new_c.is_zero()))) {
TRACE("fm", tout << "resolution " << x << " inconsistent: \n";
TRACE("qe_lite", tout << "resolution " << x << " inconsistent: \n";
display(tout, l);
tout << "\n";
display(tout, u); tout << "\n";);
@ -1926,7 +1928,7 @@ namespace fm {
new_strict,
new_dep);
TRACE("fm", tout << "resolution " << x << "\n";
TRACE("qe_lite", tout << "resolution " << x << "\n";
display(tout, l);
tout << "\n";
display(tout, u);
@ -1949,7 +1951,7 @@ namespace fm {
if (l.empty() || u.empty()) {
// easy case
mark_constraints_dead(x);
TRACE("fm", tout << "variable was eliminated (trivial case)\n";);
TRACE("qe_lite", tout << "variable was eliminated (trivial case)\n";);
return true;
}
@ -1967,7 +1969,7 @@ namespace fm {
m_counter += num_lowers * num_uppers;
TRACE("fm_bug", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n";
TRACE("qe_lite", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n";
display_constraints(tout, l); tout << "uppers:\n"; display_constraints(tout, u););
unsigned num_old_cnstrs = num_uppers + num_lowers;
@ -1977,7 +1979,7 @@ namespace fm {
for (unsigned i = 0; i < num_lowers; i++) {
for (unsigned j = 0; j < num_uppers; j++) {
if (m_inconsistent || num_new_cnstrs > limit) {
TRACE("fm", tout << "too many new constraints: " << num_new_cnstrs << "\n";);
TRACE("qe_lite", tout << "too many new constraints: " << num_new_cnstrs << "\n";);
del_constraints(new_constraints.size(), new_constraints.c_ptr());
return false;
}
@ -2002,7 +2004,7 @@ namespace fm {
backward_subsumption(*c);
register_constraint(c);
}
TRACE("fm", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";);
TRACE("qe_lite", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";);
return true;
}
@ -2018,7 +2020,7 @@ namespace fm {
if (!c->m_dead) {
c->m_dead = true;
expr * new_f = to_expr(*c);
TRACE("fm_bug", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";);
TRACE("qe_lite", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";);
m_new_fmls.push_back(new_f);
}
}
@ -2049,7 +2051,7 @@ namespace fm {
m_new_fmls.push_back(m.mk_false());
}
else {
TRACE("fm", display(tout););
TRACE("qe_lite", display(tout););
subsume();
var_vector candidates;

112
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -99,93 +99,15 @@ Rules
(mod t1 t2) --> k2 | same constraints as above
*/
struct purify_arith_decls {
ast_manager & m;
func_decl * m_int_0_pw_0_decl; // decl for: int 0^0
func_decl * m_real_0_pw_0_decl; // decl for: rel 0^0
func_decl * m_neg_root_decl; // decl for: even root of negative (real) number
func_decl * m_div_0_decl; // decl for: x/0
func_decl * m_idiv_0_decl; // decl for: div(x, 0)
func_decl * m_mod_0_decl; // decl for: mod(x, 0)
func_decl * m_asin_u_decl; // decl for: asin(x) when x < -1 or x > 1
func_decl * m_acos_u_decl; // decl for: acos(x) when x < -1 or x > 1
void inc_refs() {
m.inc_ref(m_int_0_pw_0_decl);
m.inc_ref(m_real_0_pw_0_decl);
m.inc_ref(m_neg_root_decl);
m.inc_ref(m_div_0_decl);
m.inc_ref(m_idiv_0_decl);
m.inc_ref(m_mod_0_decl);
m.inc_ref(m_asin_u_decl);
m.inc_ref(m_acos_u_decl);
}
void dec_refs() {
m.dec_ref(m_int_0_pw_0_decl);
m.dec_ref(m_real_0_pw_0_decl);
m.dec_ref(m_neg_root_decl);
m.dec_ref(m_div_0_decl);
m.dec_ref(m_idiv_0_decl);
m.dec_ref(m_mod_0_decl);
m.dec_ref(m_asin_u_decl);
m.dec_ref(m_acos_u_decl);
}
purify_arith_decls(arith_util & u):
m(u.get_manager()) {
sort * i = u.mk_int();
sort * r = u.mk_real();
m_int_0_pw_0_decl = m.mk_const_decl(symbol("0^0-int"), i);
m_real_0_pw_0_decl = m.mk_const_decl(symbol("0^0-real"), r);
sort * rr[2] = { r, r };
m_neg_root_decl = m.mk_func_decl(symbol("neg-root"), 2, rr, r);
m_div_0_decl = m.mk_func_decl(symbol("/0"), 1, &r, r);
m_idiv_0_decl = m.mk_func_decl(symbol("div0"), 1, &i, i);
m_mod_0_decl = m.mk_func_decl(symbol("mod0"), 1, &i, i);
m_asin_u_decl = m.mk_func_decl(symbol("asin-u"), 1, &r, r);
m_acos_u_decl = m.mk_func_decl(symbol("acos-u"), 1, &r, r);
inc_refs();
}
purify_arith_decls(ast_manager & _m,
func_decl * int_0_pw_0,
func_decl * real_0_pw_0,
func_decl * neg_root,
func_decl * div_0,
func_decl * idiv_0,
func_decl * mod_0,
func_decl * asin_u,
func_decl * acos_u
):
m(_m),
m_int_0_pw_0_decl(int_0_pw_0),
m_real_0_pw_0_decl(real_0_pw_0),
m_neg_root_decl(neg_root),
m_div_0_decl(div_0),
m_idiv_0_decl(idiv_0),
m_mod_0_decl(mod_0),
m_asin_u_decl(asin_u),
m_acos_u_decl(acos_u) {
inc_refs();
}
~purify_arith_decls() {
dec_refs();
}
};
struct purify_arith_proc {
arith_util & m_util;
purify_arith_decls & m_aux_decls;
bool m_produce_proofs;
bool m_elim_root_objs;
bool m_elim_inverses;
bool m_complete;
purify_arith_proc(arith_util & u, purify_arith_decls & d, bool produce_proofs, bool elim_root_objs, bool elim_inverses, bool complete):
purify_arith_proc(arith_util & u, bool produce_proofs, bool elim_root_objs, bool elim_inverses, bool complete):
m_util(u),
m_aux_decls(d),
m_produce_proofs(produce_proofs),
m_elim_root_objs(elim_root_objs),
m_elim_inverses(elim_inverses),
@ -247,15 +169,6 @@ struct purify_arith_proc {
expr * mk_fresh_int_var() { return mk_fresh_var(true); }
func_decl * div0_decl() { return m_owner.m_aux_decls.m_div_0_decl; }
func_decl * idiv0_decl() { return m_owner.m_aux_decls.m_idiv_0_decl; }
func_decl * mod0_decl() { return m_owner.m_aux_decls.m_mod_0_decl; }
func_decl * int_0_pw_0_decl() { return m_owner.m_aux_decls.m_int_0_pw_0_decl; }
func_decl * real_0_pw_0_decl() { return m_owner.m_aux_decls.m_real_0_pw_0_decl; }
func_decl * neg_root_decl() { return m_owner.m_aux_decls.m_neg_root_decl; }
func_decl * asin_u_decl() { return m_owner.m_aux_decls.m_asin_u_decl; }
func_decl * acos_u_decl() { return m_owner.m_aux_decls.m_acos_u_decl; }
expr * mk_int_zero() { return u().mk_numeral(rational(0), true); }
expr * mk_real_zero() { return u().mk_numeral(rational(0), false); }
@ -332,7 +245,7 @@ struct purify_arith_proc {
if (complete()) {
// y != 0 \/ k = div-0(x)
push_cnstr(OR(NOT(EQ(y, mk_real_zero())),
EQ(k, m().mk_app(div0_decl(), x))));
EQ(k, u().mk_div0(x))));
push_cnstr_pr(result_pr);
}
}
@ -380,10 +293,10 @@ struct purify_arith_proc {
push_cnstr_pr(mod_pr);
if (complete()) {
push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, m().mk_app(idiv0_decl(), x))));
push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv0(x))));
push_cnstr_pr(result_pr);
push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, m().mk_app(mod0_decl(), x))));
push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod0(x))));
push_cnstr_pr(mod_pr);
}
}
@ -445,8 +358,7 @@ struct purify_arith_proc {
push_cnstr(OR(EQ(x, zero), EQ(k, one)));
push_cnstr_pr(result_pr);
if (complete()) {
func_decl * z_pw_z = is_int ? int_0_pw_0_decl() : real_0_pw_0_decl();
push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, m().mk_const(z_pw_z))));
push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real())));
push_cnstr_pr(result_pr);
}
}
@ -470,7 +382,7 @@ struct purify_arith_proc {
push_cnstr_pr(result_pr);
if (complete()) {
push_cnstr(OR(u().mk_ge(x, zero),
EQ(k, m().mk_app(neg_root_decl(), x, u().mk_numeral(n, false)))));
EQ(k, u().mk_neg_root(x, u().mk_numeral(n, false)))));
push_cnstr_pr(result_pr);
}
}
@ -561,10 +473,10 @@ struct purify_arith_proc {
// x < -1 implies k = asin_u(x)
// x > 1 implies k = asin_u(x)
push_cnstr(OR(u().mk_ge(x, mone),
EQ(k, m().mk_app(asin_u_decl(), x))));
EQ(k, u().mk_u_asin(x))));
push_cnstr_pr(result_pr);
push_cnstr(OR(u().mk_le(x, one),
EQ(k, m().mk_app(asin_u_decl(), x))));
EQ(k, u().mk_u_asin(x))));
push_cnstr_pr(result_pr);
}
return BR_DONE;
@ -603,10 +515,10 @@ struct purify_arith_proc {
// x < -1 implies k = acos_u(x)
// x > 1 implies k = acos_u(x)
push_cnstr(OR(u().mk_ge(x, mone),
EQ(k, m().mk_app(acos_u_decl(), x))));
EQ(k, u().mk_u_acos(x))));
push_cnstr_pr(result_pr);
push_cnstr(OR(u().mk_le(x, one),
EQ(k, m().mk_app(acos_u_decl(), x))));
EQ(k, u().mk_u_acos(x))));
push_cnstr_pr(result_pr);
}
return BR_DONE;
@ -835,12 +747,10 @@ struct purify_arith_proc {
class purify_arith_tactic : public tactic {
arith_util m_util;
purify_arith_decls m_aux_decls;
params_ref m_params;
public:
purify_arith_tactic(ast_manager & m, params_ref const & p):
m_util(m),
m_aux_decls(m_util),
m_params(p) {
}
@ -879,7 +789,7 @@ public:
bool elim_root_objs = m_params.get_bool("elim_root_objects", true);
bool elim_inverses = m_params.get_bool("elim_inverses", true);
bool complete = m_params.get_bool("complete", true);
purify_arith_proc proc(m_util, m_aux_decls, produce_proofs, elim_root_objs, elim_inverses, complete);
purify_arith_proc proc(m_util, produce_proofs, elim_root_objs, elim_inverses, complete);
proc(*(g.get()), mc, produce_models);

5
src/util/params.cpp
View file

@ -933,3 +933,8 @@ void params::set_sym(char const * k, symbol const & v) {
SET_SYM_VALUE();
}
#ifdef Z3DEBUG
void pp(params_ref const & p) {
std::cout << p << std::endl;
}
#endif