mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-11-09 09:49:48 -08:00
parent 0909832cbf e0066df6a9
commit 865c0c0109
13 changed files with 245 additions and 148 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
CMakeLists.txt
View file

@ -32,9 +32,9 @@ project(Z3 C CXX)
# Project version
################################################################################
set(Z3_VERSION_MAJOR 4)
set(Z3_VERSION_MINOR 4)
set(Z3_VERSION_PATCH 2)
set(Z3_VERSION_TWEAK 1)
set(Z3_VERSION_MINOR 5)
set(Z3_VERSION_PATCH 1)
set(Z3_VERSION_TWEAK 0)
set(Z3_FULL_VERSION 0)
set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
message(STATUS "Z3 version ${Z3_VERSION}")

28
examples/python/example.py
View file

@ -1,4 +1,30 @@
# Copyright (c) Microsoft Corporation 2015
# Copyright (c) Microsoft Corporation 2015, 2016
# The Z3 Python API requires libz3.dll/.so/.dylib in the
# PATH/LD_LIBRARY_PATH/DYLD_LIBRARY_PATH
# environment variable and the PYTHON_PATH environment variable
# needs to point to the `python' directory that contains `z3/z3.py'
# (which is at bin/python in our binary releases).
# If you obtained example.py as part of our binary release zip files,
# which you unzipped into a directory called `MYZ3', then follow these
# instructions to run the example:
# Running this example on Windows:
# set PATH=%PATH%;MYZ3\bin
# set PYTHONPATH=MYZ3\bin\python
# python example.py
# Running this example on Linux:
# export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:MYZ3/bin
# export PYTHONPATH=MYZ3/bin/python
# python example.py
# Running this example on OSX:
# export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:MYZ3/bin
# export PYTHONPATH=MYZ3/bin/python
# python example.py
from z3 import *

3
scripts/mk_project.py
View file

@ -9,7 +9,7 @@ from mk_util import *
# Z3 Project definition
def init_project_def():
set_version(4, 4, 2, 1)
set_version(4, 5, 1, 0)
add_lib('util', [])
add_lib('polynomial', ['util'], 'math/polynomial')
add_lib('sat', ['util'])
@ -94,6 +94,7 @@ def init_project_def():
add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml')
add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
set_z3py_dir('api/python')
add_python(_libz3Component)
add_python_install(_libz3Component)
# Examples
add_cpp_example('cpp_example', 'c++')

10
scripts/mk_unix_dist.py
View file

@ -26,6 +26,7 @@ DOTNET_ENABLED=True
DOTNET_KEY_FILE=None
JAVA_ENABLED=True
GIT_HASH=False
PYTHON_ENABLED=True
def set_verbose(flag):
global VERBOSE
@ -55,6 +56,7 @@ def display_help():
print(" --nodotnet do not include .NET bindings in the binary distribution files.")
print(" --dotnet-key=<file> sign the .NET assembly with the private key in <file>.")
print(" --nojava do not include Java bindings in the binary distribution files.")
print(" --nopython do not include Python bindings in the binary distribution files.")
print(" --githash include git hash in the Zip file.")
exit(0)
@ -69,7 +71,8 @@ def parse_options():
'nojava',
'nodotnet',
'dotnet-key=',
'githash'
'githash',
'nopython'
])
for opt, arg in options:
if opt in ('-b', '--build'):
@ -84,6 +87,8 @@ def parse_options():
FORCE_MK = True
elif opt == '--nodotnet':
DOTNET_ENABLED = False
elif opt == '--nopython':
PYTHON_ENABLED = False
elif opt == '--dotnet-key':
DOTNET_KEY_FILE = arg
elif opt == '--nojava':
@ -111,6 +116,8 @@ def mk_build_dir(path):
if GIT_HASH:
opts.append('--githash=%s' % mk_util.git_hash())
opts.append('--git-describe')
if PYTHON_ENABLED:
opts.append('--python')
if subprocess.call(opts) != 0:
raise MKException("Failed to generate build directory at '%s'" % path)
@ -181,6 +188,7 @@ def mk_dist_dir():
mk_util.DOTNET_ENABLED = DOTNET_ENABLED
mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE
mk_util.JAVA_ENABLED = JAVA_ENABLED
mk_util.PYTHON_ENABLED = PYTHON_ENABLED
mk_unix_dist(build_path, dist_path)
if is_verbose():
print("Generated distribution folder at '%s'" % dist_path)

53
scripts/mk_util.py
View file

@ -63,6 +63,7 @@ DOTNET_COMPONENT='dotnet'
JAVA_COMPONENT='java'
ML_COMPONENT='ml'
CPP_COMPONENT='cpp'
PYTHON_COMPONENT='python'
#####################
IS_WINDOWS=False
IS_LINUX=False
@ -81,6 +82,7 @@ ONLY_MAKEFILES = False
Z3PY_SRC_DIR=None
VS_PROJ = False
TRACE = False
PYTHON_ENABLED=False
DOTNET_ENABLED=False
DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None)
JAVA_ENABLED=False
@ -675,7 +677,7 @@ def display_help(exit_code):
# Parse configuration option for mk_make script
def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED
global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
@ -748,6 +750,7 @@ def parse_options():
elif opt in ('', '--noomp'):
USE_OMP = False
elif opt in ('--python'):
PYTHON_ENABLED = True
PYTHON_INSTALL_ENABLED = True
else:
print("ERROR: Invalid command line option '%s'" % opt)
@ -844,6 +847,9 @@ def is_ml_enabled():
def is_dotnet_enabled():
return DOTNET_ENABLED
def is_python_enabled():
return PYTHON_ENABLED
def is_python_install_enabled():
return PYTHON_INSTALL_ENABLED
@ -1382,6 +1388,32 @@ class DLLComponent(Component):
shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
'%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
class PythonComponent(Component):
def __init__(self, name, libz3Component):
assert isinstance(libz3Component, DLLComponent)
global PYTHON_ENABLED
Component.__init__(self, name, None, [])
self.libz3Component = libz3Component
def main_component(self):
return False
def mk_win_dist(self, build_path, dist_path):
if not is_python_enabled():
return
src = os.path.join(build_path, 'python', 'z3')
dst = os.path.join(dist_path, INSTALL_BIN_DIR, 'python', 'z3')
if os.path.exists(dst):
shutil.rmtree(dst)
shutil.copytree(src, dst)
def mk_unix_dist(self, build_path, dist_path):
self.mk_win_dist(build_path, dist_path)
def mk_makefile(self, out):
return
class PythonInstallComponent(Component):
def __init__(self, name, libz3Component):
assert isinstance(libz3Component, DLLComponent)
@ -1484,6 +1516,7 @@ class PythonInstallComponent(Component):
os.path.join('python', 'z3', '*.pyc'),
os.path.join(self.pythonPkgDir,'z3'),
in_prefix=self.in_prefix_install)
if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
@ -2173,6 +2206,15 @@ class PythonExampleComponent(ExampleComponent):
print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python')))
out.write('_ex_%s: \n\n' % self.name)
def mk_win_dist(self, build_path, dist_path):
full = os.path.join(EXAMPLE_DIR, self.path)
py = 'example.py'
shutil.copyfile(os.path.join(full, py),
os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py))
def mk_unix_dist(self, build_path, dist_path):
self.mk_win_dist(build_path, dist_path)
def reg_component(name, c):
global _Id, _Components, _ComponentNames, _Name2Component
@ -2213,6 +2255,10 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man
c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps)
reg_component(name, c)
def add_python(libz3Component):
name = 'python'
reg_component(name, PythonComponent(name, libz3Component))
def add_python_install(libz3Component):
name = 'python_install'
reg_component(name, PythonInstallComponent(name, libz3Component))
@ -3230,11 +3276,6 @@ def mk_vs_proj_dll(name, components):
def mk_win_dist(build_path, dist_path):
for c in get_components():
c.mk_win_dist(build_path, dist_path)
# Add Z3Py to bin directory
print("Adding to %s\n" % dist_path)
for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
shutil.copy(os.path.join(build_path, pyc),
os.path.join(dist_path, INSTALL_BIN_DIR, pyc))
def mk_unix_dist(build_path, dist_path):
for c in get_components():

12
scripts/mk_win_dist.py
View file

@ -28,6 +28,7 @@ DOTNET_ENABLED=True
DOTNET_KEY_FILE=None
JAVA_ENABLED=True
GIT_HASH=False
PYTHON_ENABLED=True
def set_verbose(flag):
global VERBOSE
@ -60,12 +61,13 @@ def display_help():
print(" --nodotnet do not include .NET bindings in the binary distribution files.")
print(" --dotnet-key=<file> sign the .NET assembly with the private key in <file>.")
print(" --nojava do not include Java bindings in the binary distribution files.")
print(" --nopython do not include Python bindings in the binary distribution files.")
print(" --githash include git hash in the Zip file.")
exit(0)
# Parse configuration option for mk_make script
def parse_options():
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED
path = BUILD_DIR
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
'help',
@ -74,7 +76,8 @@ def parse_options():
'nojava',
'nodotnet',
'dotnet-key=',
'githash'
'githash',
'nopython'
])
for opt, arg in options:
if opt in ('-b', '--build'):
@ -89,6 +92,8 @@ def parse_options():
FORCE_MK = True
elif opt == '--nodotnet':
DOTNET_ENABLED = False
elif opt == '--nopython':
PYTHON_ENABLED = False
elif opt == '--dotnet-key':
DOTNET_KEY_FILE = arg
elif opt == '--nojava':
@ -118,6 +123,8 @@ def mk_build_dir(path, x64):
if GIT_HASH:
opts.append('--githash=%s' % mk_util.git_hash())
opts.append('--git-describe')
if PYTHON_ENABLED:
opts.append('--python')
if subprocess.call(opts) != 0:
raise MKException("Failed to generate build directory at '%s'" % path)
@ -192,6 +199,7 @@ def mk_dist_dir_core(x64):
mk_util.DOTNET_ENABLED = DOTNET_ENABLED
mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE
mk_util.JAVA_ENABLED = JAVA_ENABLED
mk_util.PYTHON_ENABLED = PYTHON_ENABLED
mk_win_dist(build_path, dist_path)
if is_verbose():
print("Generated %s distribution folder at '%s'" % (platform, dist_path))

4
src/api/api_datalog.cpp
View file

@ -189,7 +189,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, unsigned __int64 size) {
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, __uint64 size) {
Z3_TRY;
LOG_Z3_mk_finite_domain_sort(c, name, size);
RESET_ERROR_CODE();
@ -199,7 +199,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, unsigned __int64 * out) {
Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, __uint64 * out) {
Z3_TRY;
if (out) {
*out = 0;

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

@ -4,6 +4,7 @@ import shutil
import platform
import subprocess
import multiprocessing
import re
from setuptools import setup
from distutils.errors import LibError
from distutils.command.build import build as _build
@ -43,6 +44,16 @@ def _clean_bins():
shutil.rmtree(BINS_DIR, ignore_errors=True)
shutil.rmtree(HEADERS_DIR, ignore_errors=True)
def _z3_version():
fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py')
if os.path.exists(fn):
with open(fn) as f:
for line in f:
n = re.match(".*set_version\((.*), (.*), (.*), (.*)\).*", line)
if not n is None:
return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4)
return "?.?.?.?"
def _configure_z3():
# bail out early if we don't need to do this - it forces a rebuild every time otherwise
if os.path.exists(BUILD_DIR):
@ -139,7 +150,7 @@ class sdist(_sdist):
setup(
name='z3-solver',
version='4.4.2.1',
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, compiliation, or installation, please submit issues to https://github.com/angr/angr-z3',
author="The Z3 Theorem Prover Project",

12
src/api/z3_api.h
View file

@ -1807,7 +1807,7 @@ extern "C" {
def_API('Z3_mk_finite_domain_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT64)))
*/
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, unsigned __int64 size);
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, __uint64 size);
/**
\brief Create an array type.
@ -3143,14 +3143,14 @@ extern "C" {
/**
\brief Create a numeral of a int, bit-vector, or finite-domain sort.
This function can be use to create numerals that fit in a machine unsigned __int64 integer.
This function can be use to create numerals that fit in a machine __uint64 integer.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\sa Z3_mk_numeral
def_API('Z3_mk_unsigned_int64', AST, (_in(CONTEXT), _in(UINT64), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, unsigned __int64 v, Z3_sort ty);
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, __uint64 v, Z3_sort ty);
/*@}*/
@ -3722,7 +3722,7 @@ extern "C" {
def_API('Z3_get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64)))
*/
Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, unsigned __int64* r);
Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, __uint64* r);
/**
\brief Return the domain of the given array sort.
@ -4288,7 +4288,7 @@ extern "C" {
/**
\brief Similar to #Z3_get_numeral_string, but only succeeds if
the value can fit in a machine unsigned __int64 int. Return Z3_TRUE if the call succeeded.
the value can fit in a machine __uint64 int. Return Z3_TRUE if the call succeeded.
\pre Z3_get_ast_kind(c, v) == Z3_NUMERAL_AST
@ -4296,7 +4296,7 @@ extern "C" {
def_API('Z3_get_numeral_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
*/
Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned __int64* u);
Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, __uint64* u);
/**
\brief Similar to #Z3_get_numeral_string, but only succeeds if

118
src/ast/macros/macro_util.cpp
View file

@ -34,7 +34,7 @@ macro_util::macro_util(ast_manager & m, simplifier & s):
m_simplifier(s),
m_arith_simp(0),
m_bv_simp(0),
m_basic_simp(0),
m_basic_simp(0),
m_forbidden_set(0),
m_curr_clause(0) {
}
@ -64,23 +64,23 @@ basic_simplifier_plugin * macro_util::get_basic_simp() const {
}
bool macro_util::is_bv(expr * n) const {
return get_bv_simp()->is_bv(n);
return get_bv_simp()->is_bv(n);
}
bool macro_util::is_bv_sort(sort * s) const {
return get_bv_simp()->is_bv_sort(s);
return get_bv_simp()->is_bv_sort(s);
}
bool macro_util::is_add(expr * n) const {
return get_arith_simp()->is_add(n) || get_bv_simp()->is_add(n);
return get_arith_simp()->is_add(n) || get_bv_simp()->is_add(n);
}
bool macro_util::is_times_minus_one(expr * n, expr * & arg) const {
return get_arith_simp()->is_times_minus_one(n, arg) || get_bv_simp()->is_times_minus_one(n, arg);
}
bool macro_util::is_le(expr * n) const {
return get_arith_simp()->is_le(n) || get_bv_simp()->is_le(n);
bool macro_util::is_le(expr * n) const {
return get_arith_simp()->is_le(n) || get_bv_simp()->is_le(n);
}
bool macro_util::is_le_ge(expr * n) const {
@ -130,7 +130,7 @@ void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_r
/**
\brief Return true if \c n is an application of the form
(f x_{k_1}, ..., x_{k_n})
where f is uninterpreted
@ -147,7 +147,7 @@ bool macro_util::is_macro_head(expr * n, unsigned num_decls) const {
var2pos.resize(num_decls, -1);
for (unsigned i = 0; i < num_decls; i++) {
expr * c = to_app(n)->get_arg(i);
if (!is_var(c))
if (!is_var(c))
return false;
unsigned idx = to_var(c)->get_idx();
if (idx >= num_decls || var2pos[idx] != -1)
@ -161,12 +161,12 @@ bool macro_util::is_macro_head(expr * n, unsigned num_decls) const {
/**
\brief Return true if n is of the form
(= (f x_{k_1}, ..., x_{k_n}) t) OR
(iff (f x_{k_1}, ..., x_{k_n}) t)
(iff (f x_{k_1}, ..., x_{k_n}) t)
where
is_macro_head((f x_{k_1}, ..., x_{k_n})) returns true AND
t does not contain f AND
f is not in forbidden_set
@ -180,7 +180,8 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
if (m_manager.is_eq(n) || m_manager.is_iff(n)) {
expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1);
if (is_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) && !occurs(to_app(lhs)->get_decl(), rhs)) {
if (is_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) &&
!occurs(to_app(lhs)->get_decl(), rhs)) {
head = to_app(lhs);
def = rhs;
return true;
@ -192,12 +193,12 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
/**
\brief Return true if n is of the form
(= t (f x_{k_1}, ..., x_{k_n})) OR
(iff t (f x_{k_1}, ..., x_{k_n}))
where
is_macro_head((f x_{k_1}, ..., x_{k_n})) returns true AND
t does not contain f AND
f is not in forbidden_set
@ -211,7 +212,8 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h
if (m_manager.is_eq(n) || m_manager.is_iff(n)) {
expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1);
if (is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) && !occurs(to_app(rhs)->get_decl(), lhs)) {
if (is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) &&
!occurs(to_app(rhs)->get_decl(), lhs)) {
head = to_app(rhs);
def = lhs;
return true;
@ -254,7 +256,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
if (!as->is_numeral(rhs))
return false;
inv = false;
ptr_buffer<expr> args;
expr * h = 0;
@ -271,15 +273,15 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
for (unsigned i = 0; i < lhs_num_args; i++) {
expr * arg = lhs_args[i];
expr * neg_arg;
if (h == 0 &&
is_macro_head(arg, num_decls) &&
!is_forbidden(to_app(arg)->get_decl()) &&
if (h == 0 &&
is_macro_head(arg, num_decls) &&
!is_forbidden(to_app(arg)->get_decl()) &&
!poly_contains_head(lhs, to_app(arg)->get_decl(), arg)) {
h = arg;
}
else if (h == 0 && as->is_times_minus_one(arg, neg_arg) &&
is_macro_head(neg_arg, num_decls) &&
!is_forbidden(to_app(neg_arg)->get_decl()) &&
is_macro_head(neg_arg, num_decls) &&
!is_forbidden(to_app(neg_arg)->get_decl()) &&
!poly_contains_head(lhs, to_app(neg_arg)->get_decl(), arg)) {
h = neg_arg;
inv = true;
@ -304,7 +306,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
\brief Auxiliary function for is_pseudo_predicate_macro. It detects the pattern (= (f X) t)
*/
bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t) {
if (!m_manager.is_eq(n))
if (!m_manager.is_eq(n))
return false;
expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1);
@ -331,7 +333,7 @@ bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, ap
/**
\brief Returns true if n if of the form (forall (X) (iff (= (f X) t) def[X]))
where t is a ground term, (f X) is the head.
where t is a ground term, (f X) is the head.
*/
bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def) {
if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
@ -343,14 +345,14 @@ bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t
return false;
expr * lhs = to_app(body)->get_arg(0);
expr * rhs = to_app(body)->get_arg(1);
if (is_pseudo_head(lhs, num_decls, head, t) &&
!is_forbidden(head->get_decl()) &&
if (is_pseudo_head(lhs, num_decls, head, t) &&
!is_forbidden(head->get_decl()) &&
!occurs(head->get_decl(), rhs)) {
def = rhs;
return true;
}
if (is_pseudo_head(rhs, num_decls, head, t) &&
!is_forbidden(head->get_decl()) &&
if (is_pseudo_head(rhs, num_decls, head, t) &&
!is_forbidden(head->get_decl()) &&
!occurs(head->get_decl(), lhs)) {
def = lhs;
return true;
@ -361,7 +363,7 @@ bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t
/**
\brief A quasi-macro head is of the form f[X_1, ..., X_n],
where n == num_decls, f[X_1, ..., X_n] is a term starting with symbol f, f is uninterpreted,
contains all universally quantified variables as arguments.
contains all universally quantified variables as arguments.
Note that, some arguments of f[X_1, ..., X_n] may not be variables.
Examples of quasi-macros:
@ -477,16 +479,16 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
else
var_mapping.setx(max_var_idx - i, v);
}
for (unsigned i = num_args; i <= max_var_idx; i++)
// CMW: Won't be used, but dictates a larger binding size,
// CMW: Won't be used, but dictates a larger binding size,
// so that the indexes between here and in the rewriter match.
// It's possible that we don't see the true max idx of all vars here.
var_mapping.setx(max_var_idx - i, 0);
var_mapping.setx(max_var_idx - i, 0);
if (changed) {
// REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution.
var_subst subst(m_manager, true);
var_subst subst(m_manager, true);
TRACE("macro_util_bug",
tout << "head: " << mk_pp(head, m_manager) << "\n";
tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n";
@ -503,8 +505,8 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
// -----------------------------
//
// "Hint" support
// See comment at is_hint_atom
// "Hint" support
// See comment at is_hint_atom
// for a definition of what a hint is.
//
// -----------------------------
@ -516,7 +518,7 @@ bool is_hint_head(expr * n, ptr_buffer<var> & vars) {
return false;
unsigned num_args = to_app(n)->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(n)->get_arg(i);
expr * arg = to_app(n)->get_arg(i);
if (is_var(arg))
vars.push_back(to_var(arg));
}
@ -552,7 +554,7 @@ bool vars_of_is_subset(expr * n, ptr_buffer<var> const & vars) {
}
}
else {
SASSERT(is_quantifier(curr));
SASSERT(is_quantifier(curr));
return false; // do no support nested quantifier... being conservative.
}
}
@ -560,7 +562,7 @@ bool vars_of_is_subset(expr * n, ptr_buffer<var> const & vars) {
}
/**
\brief (= lhs rhs) is a hint atom if
\brief (= lhs rhs) is a hint atom if
lhs is of the form (f t_1 ... t_n)
and all variables occurring in rhs are direct arguments of lhs.
*/
@ -598,7 +600,7 @@ void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref
/**
\brief Return true if n can be viewed as a polynomial "hint" based on head.
That is, n (but the monomial exception) only uses the variables in head, and does not use
head->get_decl().
head->get_decl().
is_hint_head(head, vars) must also return true
*/
bool macro_util::is_poly_hint(expr * n, app * head, expr * exception) {
@ -630,7 +632,7 @@ bool macro_util::is_poly_hint(expr * n, app * head, expr * exception) {
}
TRACE("macro_util_hint", tout << "succeeded\n";);
return true;
}
// -----------------------------
@ -681,7 +683,7 @@ void macro_util::insert_macro(app * head, expr * def, expr * cond, bool ineq, bo
r.insert(head->get_decl(), norm_def.get(), norm_cond.get(), ineq, satisfy_atom, hint);
}
void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom,
void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom,
bool hint, macro_candidates & r) {
if (!is_macro_head(head, head->get_num_args())) {
app_ref new_head(m_manager);
@ -783,8 +785,8 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a
if (!is_app(arg))
continue;
func_decl * f = to_app(arg)->get_decl();
bool _is_arith_macro =
bool _is_arith_macro =
is_quasi_macro_head(arg, num_decls) &&
!is_forbidden(f) &&
!poly_contains_head(lhs, f, arg) &&
@ -805,14 +807,14 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a
}
else if (is_times_minus_one(arg, neg_arg) && is_app(neg_arg)) {
f = to_app(neg_arg)->get_decl();
bool _is_arith_macro =
bool _is_arith_macro =
is_quasi_macro_head(neg_arg, num_decls) &&
!is_forbidden(f) &&
!poly_contains_head(lhs, f, arg) &&
!occurs(f, rhs) &&
!rest_contains_decl(f, atom);
bool _is_poly_hint = !_is_arith_macro && is_poly_hint(lhs, to_app(neg_arg), arg);
if (_is_arith_macro || _is_poly_hint) {
collect_poly_args(lhs, arg, args);
expr_ref rest(m_manager);
@ -842,34 +844,34 @@ void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls,
/**
\brief Collect macro candidates for atom \c atom.
The candidates are stored in \c r.
The following post-condition holds:
for each i in [0, r.size() - 1]
we have a conditional macro of the form
r.get_cond(i) IMPLIES f(x_1, ..., x_n) = r.get_def(i)
where
f == r.get_fs(i) .., x_n), f is uninterpreted and x_1, ..., x_n are variables.
r.get_cond(i) and r.get_defs(i) do not contain f or variables not in {x_1, ..., x_n}
The idea is to use r.get_defs(i) as the interpretation for f in a model M whenever r.get_cond(i)
Given a model M and values { v_1, ..., v_n }
Given a model M and values { v_1, ..., v_n }
Let M' be M{x_1 -> v_1, ..., v_n -> v_n}
Note that M'(f(x_1, ..., x_n)) = M(f)(v_1, ..., v_n)
Then, IF we have that M(f)(v_1, ..., v_n) = M'(r.get_def(i)) AND
M'(r.get_cond(i)) = true
THEN M'(atom) = true
That is, if the conditional macro is used then the atom is satisfied when M'(r.get_cond(i)) = true
IF r.is_ineq(i) = false, then
M(f)(v_1, ..., v_n) ***MUST BE*** M'(r.get_def(i)) whenever M'(r.get_cond(i)) = true
IF r.satisfy_atom(i) = true, then we have the stronger property:
Then, IF we have that (M'(r.get_cond(i)) = true IMPLIES M(f)(v_1, ..., v_n) = M'(r.get_def(i)))
@ -878,8 +880,8 @@ void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls,
void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls, macro_candidates & r) {
expr* lhs, *rhs;
if (m_manager.is_eq(atom, lhs, rhs) || m_manager.is_iff(atom, lhs, rhs)) {
if (is_quasi_macro_head(lhs, num_decls) &&
!is_forbidden(to_app(lhs)->get_decl()) &&
if (is_quasi_macro_head(lhs, num_decls) &&
!is_forbidden(to_app(lhs)->get_decl()) &&
!occurs(to_app(lhs)->get_decl(), rhs) &&
!rest_contains_decl(to_app(lhs)->get_decl(), atom)) {
expr_ref cond(m_manager);
@ -889,9 +891,9 @@ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls,
else if (is_hint_atom(lhs, rhs)) {
insert_quasi_macro(to_app(lhs), num_decls, rhs, 0, false, true, true, r);
}
if (is_quasi_macro_head(rhs, num_decls) &&
!is_forbidden(to_app(rhs)->get_decl()) &&
if (is_quasi_macro_head(rhs, num_decls) &&
!is_forbidden(to_app(rhs)->get_decl()) &&
!occurs(to_app(rhs)->get_decl(), lhs) &&
!rest_contains_decl(to_app(rhs)->get_decl(), atom)) {
expr_ref cond(m_manager);

3
src/cmd_context/cmd_context.cpp
View file

@ -1568,6 +1568,9 @@ void cmd_context::validate_model() {
// If r contains as_array/store/map/const expressions, then we do not generate the error.
// TODO: improve evaluator for model expressions.
// Note that, if "a" evaluates to false, then the error will be generated.
if (has_quantifiers(r)) {
continue;
}
try {
for_each_expr(contains_array, r);
}

97
src/smt/smt_quantifier.cpp
View file

@ -27,7 +27,7 @@ Revision History:
#include"ast_smt2_pp.h"
namespace smt {
quantifier_manager_plugin * mk_default_plugin();
struct quantifier_manager::imp {
@ -40,7 +40,7 @@ namespace smt {
ptr_vector<quantifier> m_quantifiers;
scoped_ptr<quantifier_manager_plugin> m_plugin;
unsigned m_num_instances;
imp(quantifier_manager & wrapper, context & ctx, smt_params & p, quantifier_manager_plugin * plugin):
m_wrapper(wrapper),
m_context(ctx),
@ -85,7 +85,7 @@ namespace smt {
out << max_generation << " : " << max_cost << "\n";
}
}
void del(quantifier * q) {
if (m_params.m_qi_profile) {
display_stats(verbose_stream(), q);
@ -99,15 +99,15 @@ namespace smt {
}
bool is_shared(enode * n) const {
return m_plugin->is_shared(n);
return m_plugin->is_shared(n);
}
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
ptr_vector<enode> & used_enodes) {
max_generation = std::max(max_generation, get_generation(q));
if (m_num_instances > m_params.m_qi_max_instances)
@ -136,7 +136,7 @@ namespace smt {
}
return false;
}
void init_search_eh() {
m_num_instances = 0;
ptr_vector<quantifier>::iterator it2 = m_quantifiers.begin();
@ -149,7 +149,7 @@ namespace smt {
m_plugin->init_search_eh();
TRACE("smt_params", m_params.display(tout); );
}
void assign_eh(quantifier * q) {
m_plugin->assign_eh(q);
}
@ -175,7 +175,7 @@ namespace smt {
m_plugin->pop(num_scopes);
m_qi_queue.pop_scope(num_scopes);
}
bool can_propagate() {
return m_qi_queue.has_work() || m_plugin->can_propagate();
}
@ -184,7 +184,7 @@ namespace smt {
m_plugin->propagate();
m_qi_queue.instantiate();
}
bool check_quantifier(quantifier* q) {
return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // TBD: && !m_context->get_manager().is_rec_fun_def(q);
}
@ -251,7 +251,7 @@ namespace smt {
quantifier_manager::~quantifier_manager() {
dealloc(m_imp);
}
context & quantifier_manager::get_context() const {
return m_imp->m_context;
}
@ -285,16 +285,16 @@ namespace smt {
return m_imp->get_generation(q);
}
bool quantifier_manager::add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
bool quantifier_manager::add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
ptr_vector<enode> & used_enodes) {
return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_generation, used_enodes);
}
bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) {
ptr_vector<enode> tmp;
return add_instance(q, 0, num_bindings, bindings, generation, generation, generation, tmp);
@ -347,7 +347,7 @@ namespace smt {
quantifier_manager::check_model_result quantifier_manager::check_model(proto_model * m, obj_map<enode, app *> const & root2value) {
return m_imp->check_model(m, root2value);
}
void quantifier_manager::push() {
m_imp->push();
}
@ -367,7 +367,7 @@ namespace smt {
plugin->set_manager(*this);
}
}
void quantifier_manager::display(std::ostream & out) const {
}
@ -382,12 +382,12 @@ namespace smt {
m_imp->display_stats(out, q);
}
ptr_vector<quantifier>::const_iterator quantifier_manager::begin_quantifiers() const {
return m_imp->m_quantifiers.begin();
ptr_vector<quantifier>::const_iterator quantifier_manager::begin_quantifiers() const {
return m_imp->m_quantifiers.begin();
}
ptr_vector<quantifier>::const_iterator quantifier_manager::end_quantifiers() const {
return m_imp->m_quantifiers.end();
ptr_vector<quantifier>::const_iterator quantifier_manager::end_quantifiers() const {
return m_imp->m_quantifiers.end();
}
// The default plugin uses E-matching, MBQI and quick-checker
@ -404,13 +404,13 @@ namespace smt {
bool m_active;
public:
default_qm_plugin():
m_qm(0),
m_context(0),
m_new_enode_qhead(0),
m_qm(0),
m_context(0),
m_new_enode_qhead(0),
m_lazy_matching_idx(0),
m_active(false) {
}
virtual ~default_qm_plugin() {
}
@ -434,20 +434,18 @@ namespace smt {
virtual bool model_based() const { return m_fparams->m_mbqi; }
virtual bool mbqi_enabled(quantifier *q) const {
if(!m_fparams->m_mbqi_id) return true;
virtual bool mbqi_enabled(quantifier *q) const {
if (!m_fparams->m_mbqi_id) return true;
const symbol &s = q->get_qid();
size_t len = strlen(m_fparams->m_mbqi_id);
if(s == symbol::null || s.is_numerical())
if (s == symbol::null || s.is_numerical())
return len == 0;
return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0;
}
return strncmp(s.bare_str(), m_fparams->m_mbqi_id, len) == 0;
}
/* Quantifier id's must begin with the prefix specified by
parameter mbqi.id to be instantiated with MBQI. The default
value is the empty string, so all quantifiers are
instantiated.
*/
/* Quantifier id's must begin with the prefix specified by parameter
mbqi.id to be instantiated with MBQI. The default value is the
empty string, so all quantifiers are instantiated. */
virtual void add(quantifier * q) {
if (m_fparams->m_mbqi && mbqi_enabled(q)) {
m_active = true;
@ -455,8 +453,7 @@ namespace smt {
}
}
virtual void del(quantifier * q) {
}
virtual void del(quantifier * q) { }
virtual void push() {
m_mam->push_scope();
@ -465,7 +462,7 @@ namespace smt {
m_model_finder->push_scope();
}
}
virtual void pop(unsigned num_scopes) {
m_mam->pop_scope(num_scopes);
m_lazy_mam->pop_scope(num_scopes);
@ -473,7 +470,7 @@ namespace smt {
m_model_finder->pop_scope(num_scopes);
}
}
virtual void init_search_eh() {
m_lazy_matching_idx = 0;
if (m_fparams->m_mbqi) {
@ -516,7 +513,7 @@ namespace smt {
}
}
}
bool use_ematching() const {
return m_fparams->m_ematching && !m_qm->empty();
}
@ -538,7 +535,7 @@ namespace smt {
}
virtual void restart_eh() {
if (m_fparams->m_mbqi) {
if (m_fparams->m_mbqi) {
m_model_finder->restart_eh();
m_model_checker->restart_eh();
}
@ -613,7 +610,7 @@ namespace smt {
}
return FC_DONE;
}
};
quantifier_manager_plugin * mk_default_plugin() {

34
src/smt/smt_quantifier.h
View file

@ -37,7 +37,7 @@ namespace smt {
public:
quantifier_manager(context & ctx, smt_params & fp, params_ref const & p);
~quantifier_manager();
context & get_context() const;
void set_plugin(quantifier_manager_plugin * plugin);
@ -51,12 +51,12 @@ namespace smt {
quantifier_stat * get_stat(quantifier * q) const;
unsigned get_generation(quantifier * q) const;
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
ptr_vector<enode> & used_enodes);
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
@ -78,11 +78,11 @@ namespace smt {
bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
void adjust_model(proto_model * m);
check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value);
void push();
void pop(unsigned num_scopes);
void reset();
void display(std::ostream & out) const;
void display_stats(std::ostream & out, quantifier * q) const;
@ -97,7 +97,7 @@ namespace smt {
public:
quantifier_manager_plugin() {}
virtual ~quantifier_manager_plugin() {}
virtual void set_manager(quantifier_manager & qm) = 0;
virtual quantifier_manager_plugin * mk_fresh() = 0;
@ -106,7 +106,7 @@ namespace smt {
virtual void del(quantifier * q) = 0;
virtual bool is_shared(enode * n) const = 0;
/**
\brief This method is invoked whenever q is assigned to true.
*/
@ -131,9 +131,9 @@ namespace smt {
\brief This method is invoked whenever the solver restarts.
*/
virtual void restart_eh() = 0;
/**
\brief Return true if the quantifier_manager can propagate information
\brief Return true if the quantifier_manager can propagate information
information back into the core.
*/
virtual bool can_propagate() const = 0;
@ -143,11 +143,11 @@ namespace smt {
\brief Return true if the plugin is "model based"
*/
virtual bool model_based() const = 0;
/**
\brief Is "model based" instantiate allowed to instantiate this quantifier?
*/
virtual bool mbqi_enabled(quantifier *q) const {return true;}
virtual bool mbqi_enabled(quantifier *q) const {return true;}
/**
\brief Give a change to the plugin to adjust the interpretation of unintepreted functions.
@ -161,10 +161,10 @@ namespace smt {
It also provides a mapping from enodes to their interpretations.
*/
virtual quantifier_manager::check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value) = 0;
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;
};
};