mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Merge branch 'unstable' into contrib

Browse source
This commit is contained in:
Leonardo de Moura 2012-12-22 14:36:30 -08:00
commit fbce816025
164 changed files with 2619 additions and 4128 deletions
Download patch file Download diff file Expand all files Collapse all files

25
RELEASE_NOTES
View file

@ -9,6 +9,8 @@ Version 4.3.2
- Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++.
- Added support for Python 3.x.
- Reverted to `(set-option :global-decls false)` as the default. In Z3 4.3.0 and Z3 4.3.1, this option was set to true.
Thanks to Julien Henry for reporting this problem.
@ -26,6 +28,29 @@ Version 4.3.2
- Fixed crash reported at http://z3.codeplex.com/workitem/10
- Removed auxiliary constants created by the nnf tactic from Z3 models.
- Fixed problem in the pretty printer. It was not introducing quotes for attribute names such as |foo:10|.
- Fixed bug when using assumptions (Thanks to Philippe Suter and Etienne Kneuss)
Consider the following example:
(assert F)
(check-sat a)
(check-sat)
If 'F' is unstatisfiable independently of the assumption 'a', and
the inconsistenty can be detected by just performing propagation,
Then, version <= 4.3.1 may return
unsat
sat
instead of
unsat
unsat
We say may because 'F' may have other unsatisfiable cores.
- Fixed bug reported at http://stackoverflow.com/questions/13923316/unprintable-solver-model
- Fixed timers on Linux and FreeBSD.
Version 4.3.1
=============

65
examples/c++/example.cpp
View file

@ -812,6 +812,68 @@ void tst_visit() {
visit(f);
}
void incremental_example1() {
std::cout << "incremental example1\n";
context c;
expr x = c.int_const("x");
solver s(c);
s.add(x > 0);
std::cout << s.check() << "\n";
// We can add more formulas to the solver
s.add(x < 0);
// and, invoke s.check() again...
std::cout << s.check() << "\n";
}
void incremental_example2() {
// In this example, we show how push() and pop() can be used
// to remove formulas added to the solver.
std::cout << "incremental example2\n";
context c;
expr x = c.int_const("x");
solver s(c);
s.add(x > 0);
std::cout << s.check() << "\n";
// push() creates a backtracking point (aka a snapshot).
s.push();
// We can add more formulas to the solver
s.add(x < 0);
// and, invoke s.check() again...
std::cout << s.check() << "\n";
// pop() will remove all formulas added between this pop() and the matching push()
s.pop();
// The context is satisfiable again
std::cout << s.check() << "\n";
// and contains only x > 0
std::cout << s << "\n";
}
void incremental_example3() {
// In this example, we show how to use assumptions to "remove"
// formulas added to a solver. Actually, we disable them.
std::cout << "incremental example3\n";
context c;
expr x = c.int_const("x");
solver s(c);
s.add(x > 0);
std::cout << s.check() << "\n";
// Now, suppose we want to add x < 0 to the solver, but we also want
// to be able to disable it later.
// To do that, we create an auxiliary Boolean variable
expr b = c.bool_const("b");
// and, assert (b implies x < 0)
s.add(implies(b, x < 0));
// Now, we check whether s is satisfiable under the assumption "b" is true.
expr_vector a1(c);
a1.push_back(b);
std::cout << s.check(a1) << "\n";
// To "disable" (x > 0), we may just ask with the assumption "not b" or not provide any assumption.
std::cout << s.check() << "\n";
expr_vector a2(c);
a2.push_back(!b);
std::cout << s.check(a2) << "\n";
}
int main() {
try {
demorgan(); std::cout << "\n";
@ -842,6 +904,9 @@ int main() {
tactic_example9(); std::cout << "\n";
tactic_qe(); std::cout << "\n";
tst_visit(); std::cout << "\n";
incremental_example1(); std::cout << "\n";
incremental_example2(); std::cout << "\n";
incremental_example3(); std::cout << "\n";
std::cout << "done\n";
}
catch (exception & ex) {

4
examples/python/example.py
View file

@ -4,5 +4,5 @@ x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print s.check()
print s.model()
print(s.check())
print(s.model())

263
scripts/mk_util.py
View file

@ -7,11 +7,6 @@
# Author: Leonardo de Moura (leonardo)
############################################
import sys
if sys.version >= "3":
print "ERROR: python 2.x required."
exit(1)
import os
import glob
import re
@ -75,6 +70,8 @@ VER_BUILD=None
VER_REVISION=None
PREFIX='/usr'
GMP=False
VS_PAR=False
VS_PAR_NUM=8
def is_windows():
return IS_WINDOWS
@ -132,8 +129,7 @@ def exec_cmd(cmd):
first = True
for e in cmd:
if first:
# Allow spaces in the executable name
first = False
first = False
new_cmd.append(e)
else:
if e != "":
@ -164,7 +160,7 @@ def exec_compiler_cmd(cmd):
def test_cxx_compiler(cc):
if is_verbose():
print "Testing %s..." % cc
print("Testing %s..." % cc)
t = TempFile('tst.cpp')
t.add('#include<iostream>\nint main() { return 0; }\n')
t.commit()
@ -172,7 +168,7 @@ def test_cxx_compiler(cc):
def test_c_compiler(cc):
if is_verbose():
print "Testing %s..." % cc
print("Testing %s..." % cc)
t = TempFile('tst.c')
t.add('#include<stdio.h>\nint main() { return 0; }\n')
t.commit()
@ -180,7 +176,7 @@ def test_c_compiler(cc):
def test_gmp(cc):
if is_verbose():
print "Testing GMP..."
print("Testing GMP...")
t = TempFile('tstgmp.cpp')
t.add('#include<gmp.h>\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n')
t.commit()
@ -188,7 +184,7 @@ def test_gmp(cc):
def test_openmp(cc):
if is_verbose():
print "Testing OpenMP..."
print("Testing OpenMP...")
t = TempFile('tstomp.cpp')
t.add('#include<omp.h>\nint main() { return omp_in_parallel() ? 1 : 0; }\n')
t.commit()
@ -199,12 +195,12 @@ def check_java():
t.add('public class Hello { public static void main(String[] args) { System.out.println("Hello, World"); }}\n')
t.commit()
if is_verbose():
print "Testing %s..." % JAVAC
print("Testing %s..." % JAVAC)
r = exec_cmd([JAVAC, 'Hello.java'])
if r != 0:
raise MKException('Failed testing Java compiler. Set environment variable JAVAC with the path to the Java compiler')
if is_verbose():
print "Testing %s..." % JAVA
print("Testing %s..." % JAVA)
r = exec_cmd([JAVA, 'Hello'])
rmf('Hello.class')
if r != 0:
@ -222,11 +218,11 @@ def find_java_home():
global JAVA_HOME
if JAVA_HOME != None:
if is_verbose():
print "Checking jni.h..."
print("Checking jni.h...")
if os.path.exists(os.path.join(JAVA_HOME, 'include', 'jni.h')):
return
if is_verbose():
print "Finding JAVA_HOME..."
print("Finding JAVA_HOME...")
t = TempFile('output')
null = open(os.devnull, 'wb')
try:
@ -240,17 +236,17 @@ def find_java_home():
m = open_pat.match(line)
if m:
# Remove last 3 directives from m.group(1)
print m.group(1)
print(m.group(1))
tmp = m.group(1).split(os.sep)
path = string.join(tmp[:len(tmp) - 3], os.sep)
if is_verbose():
print "Checking jni.h..."
print("Checking jni.h...")
jni_dir = find_jni_h(path)
if not jni_dir:
raise MKException("Failed to detect jni.h at '%s'.Possible solution: set JAVA_HOME with the path to JDK." % os.path.join(path, 'include'))
JAVA_HOME = os.path.split(jni_dir)[0]
if is_verbose():
print 'JAVA_HOME=%s' % JAVA_HOME
print('JAVA_HOME=%s' % JAVA_HOME)
return
raise MKException('Failed to find JAVA_HOME')
@ -259,7 +255,7 @@ def is64():
def check_ar():
if is_verbose():
print "Testing ar..."
print("Testing ar...")
if which('ar')== None:
raise MKException('ar (archive tool) was not found')
@ -320,7 +316,7 @@ def dos2unix(fname):
fout.close()
shutil.move(fname_new, fname)
if is_verbose():
print "dos2unix '%s'" % fname
print("dos2unix '%s'" % fname)
def dos2unix_tree_core(pattern, dir, files):
for filename in files:
@ -337,7 +333,7 @@ def check_eol():
# Linux/OSX/BSD check if the end-of-line is cr/lf
if is_cr_lf('LICENSE.txt'):
if is_verbose():
print "Fixing end of line..."
print("Fixing end of line...")
dos2unix_tree()
if os.name == 'nt':
@ -353,53 +349,55 @@ elif os.name == 'posix':
IS_LINUX=True
def display_help(exit_code):
print "mk_make.py: Z3 Makefile generator\n"
print "This script generates the Makefile for the Z3 theorem prover."
print "It must be executed from the Z3 root directory."
print "\nOptions:"
print " -h, --help display this message."
print " -s, --silent do not print verbose messages."
print("mk_make.py: Z3 Makefile generator\n")
print("This script generates the Makefile for the Z3 theorem prover.")
print("It must be executed from the Z3 root directory.")
print("\nOptions:")
print(" -h, --help display this message.")
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
print " -b <sudir>, --build=<subdir> subdirectory where Z3 will be built (default: build)."
print " -d, --debug compile Z3 in debug mode."
print " -t, --trace enable tracing in release mode."
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).")
print(" -d, --debug compile Z3 in debug mode.")
print(" -t, --trace enable tracing in release mode.")
if IS_WINDOWS:
print " -x, --x64 create 64 binary when using Visual Studio."
print " -m, --makefiles generate only makefiles."
print(" -x, --x64 create 64 binary when using Visual Studio.")
print(" -m, --makefiles generate only makefiles.")
if IS_WINDOWS:
print " -v, --vsproj generate Visual Studio Project Files."
print(" -v, --vsproj generate Visual Studio Project Files.")
if IS_WINDOWS:
print " -n, --nodotnet do not generate Microsoft.Z3.dll make rules."
print " -j, --java generate Java bindinds."
print " --staticlib build Z3 static library."
print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.")
print(" -j, --java generate Java bindinds.")
print(" --staticlib build Z3 static library.")
if not IS_WINDOWS:
print " -g, --gmp use GMP."
print ""
print "Some influential environment variables:"
print(" -g, --gmp use GMP.")
print("")
print("Some influential environment variables:")
if not IS_WINDOWS:
print " CXX C++ compiler"
print " CC C compiler"
print " LDFLAGS Linker flags, e.g., -L<lib dir> if you have libraries in a non-standard directory"
print " CPPFLAGS Preprocessor flags, e.g., -I<include dir> if you have header files in a non-standard directory"
print " CXXFLAGS C++ compiler flags"
print " JAVA Java virtual machine (only relevant if -j or --java option is provided)"
print " JAVAC Java compiler (only relevant if -j or --java option is provided)"
print " JAVA_HOME JDK installation directory (only relevant if -j or --java option is provided)"
print(" CXX C++ compiler")
print(" CC C compiler")
print(" LDFLAGS Linker flags, e.g., -L<lib dir> if you have libraries in a non-standard directory")
print(" CPPFLAGS Preprocessor flags, e.g., -I<include dir> if you have header files in a non-standard directory")
print(" CXXFLAGS C++ compiler flags")
print(" JAVA Java virtual machine (only relevant if -j or --java option is provided)")
print(" JAVAC Java compiler (only relevant if -j or --java option is provided)")
print(" JAVA_HOME JDK installation directory (only relevant if -j or --java option is provided)")
exit(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
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:dsxhmcvtnp:gjy:',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir='])
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir=', 'parallel='])
except:
print "ERROR: Invalid command line option"
print("ERROR: Invalid command line option")
display_help(1)
for opt, arg in options:
@ -429,8 +427,11 @@ def parse_options():
DOTNET_ENABLED = False
elif opt in ('--staticlib'):
STATIC_LIB = True
elif opt in ('-p', '--prefix'):
elif not IS_WINDOWS and opt in ('-p', '--prefix'):
PREFIX = arg
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)
@ -439,7 +440,7 @@ def parse_options():
elif opt in ('-j', '--java'):
JAVA_ENABLED = True
else:
print "ERROR: Invalid command line option '%s'" % opt
print("ERROR: Invalid command line option '%s'" % opt)
display_help(1)
# Return a list containing a file names included using '#include' in
@ -490,7 +491,7 @@ def set_z3py_dir(p):
raise MKException("Python bindings directory '%s' does not exist" % full)
Z3PY_SRC_DIR = full
if VERBOSE:
print "Python bindinds directory was detected."
print("Python bindinds directory was detected.")
_UNIQ_ID = 0
@ -656,8 +657,32 @@ class Component:
out.write(' -I%s' % get_component(dep).to_src_dir)
out.write('\n')
mk_dir(os.path.join(BUILD_DIR, self.build_dir))
for cppfile in get_cpp_files(self.src_dir):
self.add_cpp_rules(out, include_defs, cppfile)
if VS_PAR and IS_WINDOWS:
cppfiles = get_cpp_files(self.src_dir)
dependencies = set()
for cppfile in cppfiles:
dependencies.add(os.path.join(self.to_src_dir, cppfile))
self.add_rule_for_each_include(out, cppfile)
includes = extract_c_includes(os.path.join(self.src_dir, cppfile))
for include in includes:
owner = self.find_file(include, cppfile)
dependencies.add('%s.node' % os.path.join(owner.build_dir, include))
for cppfile in cppfiles:
out.write('%s$(OBJ_EXT) ' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]))
out.write(': ')
for dep in dependencies:
out.write(dep)
out.write(' ')
out.write('\n')
out.write('\t@$(CXX) $(CXXFLAGS) /MP%s $(%s)' % (VS_PAR_NUM, include_defs))
for cppfile in cppfiles:
out.write(' ')
out.write(os.path.join(self.to_src_dir, cppfile))
out.write('\n')
out.write('\tmove *.obj %s\n' % self.build_dir)
else:
for cppfile in get_cpp_files(self.src_dir):
self.add_cpp_rules(out, include_defs, cppfile)
# Return true if the component should be included in the all: rule
def main_component(self):
@ -750,7 +775,7 @@ def comp_components(c1, c2):
# Sort components based on (reverse) definition time
def sort_components(cnames):
return sorted(cnames, cmp=comp_components)
return sorted(cnames, key=lambda c: get_component(c).id, reverse=True)
class ExeComponent(Component):
def __init__(self, name, exe_name, path, deps, install):
@ -933,10 +958,8 @@ class DLLComponent(Component):
mk_dir(os.path.join(dist_path, 'bin'))
shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
'%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
if self.static:
mk_dir(os.path.join(dist_path, 'bin'))
shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name),
'%s.lib' % os.path.join(dist_path, 'bin', self.dll_name))
shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name),
'%s.lib' % os.path.join(dist_path, 'bin', self.dll_name))
class DotNetDLLComponent(Component):
def __init__(self, name, dll_name, path, deps, assembly_info_dir):
@ -1042,6 +1065,11 @@ class JavaDLLComponent(Component):
def main_component(self):
return is_java_enabled()
def mk_win_dist(self, build_path, dist_path):
if JAVA_ENABLED:
mk_dir(os.path.join(dist_path, 'bin'))
shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
'%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
class ExampleComponent(Component):
def __init__(self, name, path):
@ -1162,7 +1190,7 @@ class PythonExampleComponent(ExampleComponent):
for py in filter(lambda f: f.endswith('.py'), os.listdir(full)):
shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, py))
if is_verbose():
print "Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR)
print("Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR))
out.write('_ex_%s: \n\n' % self.name)
@ -1174,7 +1202,7 @@ def reg_component(name, c):
_ComponentNames.add(name)
_Name2Component[name] = c
if VERBOSE:
print "New component: '%s'" % name
print("New component: '%s'" % name)
def add_lib(name, deps=[], path=None, includes2install=[]):
c = LibComponent(name, path, deps, includes2install)
@ -1250,12 +1278,12 @@ def mk_config():
'SLINK_FLAGS=/nologo /LDd\n')
if not VS_X64:
config.write(
'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n'
'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n'
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
else:
config.write(
'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n'
'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n'
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
else:
@ -1281,11 +1309,11 @@ def mk_config():
# End of Windows VS config.mk
if is_verbose():
print '64-bit: %s' % is64()
print('64-bit: %s' % is64())
if is_java_enabled():
print 'Java Home: %s' % JAVA_HOME
print 'Java Compiler: %s' % JAVAC
print 'Java VM: %s' % JAVA
print('Java Home: %s' % JAVA_HOME)
print('Java Compiler: %s' % JAVAC)
print('Java VM: %s' % JAVA)
else:
global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS
ARITH = "internal"
@ -1367,17 +1395,17 @@ def mk_config():
config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS)
config.write('SLINK_OUT_FLAG=-o \n')
if is_verbose():
print 'Host platform: %s' % sysname
print 'C++ Compiler: %s' % CXX
print 'C Compiler : %s' % CC
print 'Arithmetic: %s' % ARITH
print 'OpenMP: %s' % HAS_OMP
print 'Prefix: %s' % PREFIX
print '64-bit: %s' % is64()
print('Host platform: %s' % sysname)
print('C++ Compiler: %s' % CXX)
print('C Compiler : %s' % CC)
print('Arithmetic: %s' % ARITH)
print('OpenMP: %s' % HAS_OMP)
print('Prefix: %s' % PREFIX)
print('64-bit: %s' % is64())
if is_java_enabled():
print 'Java Home: %s' % JAVA_HOME
print 'Java Compiler: %s' % JAVAC
print 'Java VM: %s' % JAVA
print('Java Home: %s' % JAVA_HOME)
print('Java Compiler: %s' % JAVAC)
print('Java VM: %s' % JAVA)
def mk_install(out):
out.write('install:\n')
@ -1403,7 +1431,7 @@ def mk_makefile():
mk_dir(BUILD_DIR)
mk_config()
if VERBOSE:
print "Writing %s" % os.path.join(BUILD_DIR, 'Makefile')
print("Writing %s" % os.path.join(BUILD_DIR, 'Makefile'))
out = open(os.path.join(BUILD_DIR, 'Makefile'), 'w')
out.write('# Automatically generated file.\n')
out.write('include config.mk\n')
@ -1431,24 +1459,24 @@ def mk_makefile():
mk_uninstall(out)
# Finalize
if VERBOSE:
print "Makefile was successfully generated."
print("Makefile was successfully generated.")
if not IS_WINDOWS:
print " python packages dir:", PYTHON_PACKAGE_DIR
print(" python packages dir: %s" % PYTHON_PACKAGE_DIR)
if DEBUG_MODE:
print " compilation mode: Debug"
print(" compilation mode: Debug")
else:
print " compilation mode: Release"
print(" compilation mode: Release")
if IS_WINDOWS:
if VS_X64:
print " platform: x64\n"
print "To build Z3, open a [Visual Studio x64 Command Prompt], then"
print(" platform: x64\n")
print("To build Z3, open a [Visual Studio x64 Command Prompt], then")
else:
print " platform: x86"
print "To build Z3, open a [Visual Studio Command Prompt], then"
print "type 'cd %s && nmake'\n" % os.path.join(os.getcwd(), BUILD_DIR)
print 'Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"'
print(" platform: x86")
print("To build Z3, open a [Visual Studio Command Prompt], then")
print("type 'cd %s && nmake'\n" % os.path.join(os.getcwd(), BUILD_DIR))
print('Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"')
else:
print "Type 'cd %s; make' to build Z3" % BUILD_DIR
print("Type 'cd %s; make' to build Z3" % BUILD_DIR)
# Generate automatically generated source code
def mk_auto_src():
@ -1543,7 +1571,7 @@ def def_module_params(module_name, export, params, class_name=None, description=
out.write('};\n')
out.write('#endif\n')
if is_verbose():
print "Generated '%s'" % hpp
print("Generated '%s'" % hpp)
def max_memory_param():
return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes')
@ -1557,6 +1585,10 @@ PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRI
'max_steps_param' : max_steps_param,
'def_module_params' : def_module_params }
def _execfile(file, globals=globals(), locals=locals()):
with open(file, "r") as fh:
exec(fh.read()+"\n", globals, locals)
# Execute python auxiliary scripts that generate extra code for Z3.
def exec_pyg_scripts():
global CURR_PYG
@ -1565,7 +1597,7 @@ def exec_pyg_scripts():
if f.endswith('.pyg'):
script = os.path.join(root, f)
CURR_PYG = script
execfile(script, PYG_GLOBALS)
_execfile(script, PYG_GLOBALS)
# TODO: delete after src/ast/pattern/expr_pattern_match
# database.smt ==> database.h
@ -1578,7 +1610,7 @@ def mk_pat_db():
fout.write('"%s\\n"\n' % line.strip('\n'))
fout.write(';\n')
if VERBOSE:
print "Generated '%s'" % os.path.join(c.src_dir, 'database.h')
print("Generated '%s'" % os.path.join(c.src_dir, 'database.h'))
# Update version numbers
def update_version():
@ -1603,7 +1635,7 @@ def mk_version_dot_h(major, minor, build, revision):
fout.write('#define Z3_BUILD_NUMBER %s\n' % build)
fout.write('#define Z3_REVISION_NUMBER %s\n' % revision)
if VERBOSE:
print "Generated '%s'" % os.path.join(c.src_dir, 'version.h')
print("Generated '%s'" % os.path.join(c.src_dir, 'version.h'))
# Update version number in AssemblyInfo.cs files
def update_all_assembly_infos(major, minor, build, revision):
@ -1652,13 +1684,13 @@ def update_assembly_info_version(assemblyinfo, major, minor, build, revision, is
else:
fout.write(line)
# if VERBOSE:
# print "%s version numbers updated at '%s'" % (num_updates, assemblyinfo)
# print("%s version numbers updated at '%s'" % (num_updates, assemblyinfo))
assert num_updates == 2, "unexpected number of version number updates"
fin.close()
fout.close()
shutil.move(tmp, assemblyinfo)
if VERBOSE:
print "Updated '%s'" % assemblyinfo
print("Updated '%s'" % assemblyinfo)
ADD_TACTIC_DATA=[]
ADD_PROBE_DATA=[]
@ -1700,7 +1732,7 @@ def mk_install_tactic_cpp(cnames, path):
added_include = True
fout.write('#include"%s"\n' % h_file)
try:
exec line.strip('\n ') in globals()
exec(line.strip('\n '), globals())
except:
raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line))
if probe_pat.match(line):
@ -1708,7 +1740,7 @@ def mk_install_tactic_cpp(cnames, path):
added_include = True
fout.write('#include"%s"\n' % h_file)
try:
exec line.strip('\n ') in globals()
exec(line.strip('\n '), globals())
except:
raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line))
# First pass will just generate the tactic factories
@ -1727,7 +1759,7 @@ def mk_install_tactic_cpp(cnames, path):
fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data)
fout.write('}\n')
if VERBOSE:
print "Generated '%s'" % fullname
print("Generated '%s'" % fullname)
def mk_all_install_tactic_cpps():
if not ONLY_MAKEFILES:
@ -1790,7 +1822,7 @@ def mk_mem_initializer_cpp(cnames, path):
fout.write('\n')
fout.write('}\n')
if VERBOSE:
print "Generated '%s'" % fullname
print("Generated '%s'" % fullname)
def mk_all_mem_initializer_cpps():
if not ONLY_MAKEFILES:
@ -1847,7 +1879,7 @@ def mk_gparams_register_modules(cnames, path):
fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr))
fout.write('}\n')
if VERBOSE:
print "Generated '%s'" % fullname
print("Generated '%s'" % fullname)
def mk_all_gparams_register_modules():
if not ONLY_MAKEFILES:
@ -1880,7 +1912,7 @@ def mk_def_file(c):
i = i + 1
num = num + 1
if VERBOSE:
print "Generated '%s'" % defname
print("Generated '%s'" % defname)
def mk_def_files():
if not ONLY_MAKEFILES:
@ -1900,7 +1932,7 @@ def cp_z3pyc_to_build():
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
print("Generated '%s'" % pyc)
def mk_bindings(api_files):
if not ONLY_MAKEFILES:
@ -1911,12 +1943,12 @@ def mk_bindings(api_files):
for api_file in api_files:
api_file_path = api.find_file(api_file, api.name)
new_api_files.append(os.path.join(api_file_path.src_dir, api_file))
g = {}
g = globals()
g["API_FILES"] = new_api_files
if is_java_enabled():
check_java()
mk_z3consts_java(api_files)
execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
_execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
cp_z3pyc_to_build()
# Extract enumeration types from API files, and add python definitions.
@ -1980,7 +2012,8 @@ def mk_z3consts_py(api_files):
if m:
name = words[1]
z3consts.write('# enum %s\n' % name)
for k, i in decls.iteritems():
for k in decls:
i = decls[k]
z3consts.write('%s = %s\n' % (k, i))
z3consts.write('\n')
mode = SEARCHING
@ -1994,7 +2027,7 @@ def mk_z3consts_py(api_files):
idx = idx + 1
linenum = linenum + 1
if VERBOSE:
print "Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py')
print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py'))
# Extract enumeration types from z3_api.h, and add .Net definitions
@ -2064,7 +2097,8 @@ def mk_z3consts_dotnet(api_files):
z3consts.write(' /// <summary>%s</summary>\n' % name)
z3consts.write(' public enum %s {\n' % name)
z3consts.write
for k, i in decls.iteritems():
for k in decls:
i = decls[k]
z3consts.write(' %s = %s,\n' % (k, i))
z3consts.write(' }\n\n')
mode = SEARCHING
@ -2079,7 +2113,7 @@ def mk_z3consts_dotnet(api_files):
linenum = linenum + 1
z3consts.write('}\n');
if VERBOSE:
print "Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs')
print("Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs'))
# Extract enumeration types from z3_api.h, and add Java definitions
@ -2153,7 +2187,8 @@ def mk_z3consts_java(api_files):
efile.write('public enum %s {\n' % name)
efile.write
first = True
for k, i in decls.iteritems():
for k in decls:
i = decls[k]
if first:
first = False
else:
@ -2184,7 +2219,7 @@ def mk_z3consts_java(api_files):
idx = idx + 1
linenum = linenum + 1
if VERBOSE:
print "Generated '%s'" % ('%s' % gendir)
print("Generated '%s'" % ('%s' % gendir))
def mk_gui_str(id):
return '4D2F40D8-E5F9-473B-B548-%012d' % id
@ -2271,7 +2306,7 @@ def mk_vs_proj(name, components):
f.write(' </ImportGroup>\n')
f.write('</Project>\n')
if is_verbose():
print "Generated '%s'" % proj_name
print("Generated '%s'" % proj_name)
def mk_win_dist(build_path, dist_path):
for c in get_components():

36
scripts/mk_win_dist.py
View file

@ -16,13 +16,15 @@ import subprocess
import zipfile
from mk_exception import *
from mk_project import *
import mk_util
BUILD_DIR='build-dist'
BUILD_X64_DIR='build-dist/x64'
BUILD_X86_DIR='build-dist/x86'
BUILD_X64_DIR=os.path.join('build-dist', 'x64')
BUILD_X86_DIR=os.path.join('build-dist', 'x86')
VERBOSE=True
DIST_DIR='dist'
FORCE_MK=False
JAVA_ENABLED=True
def set_verbose(flag):
global VERBOSE
@ -38,8 +40,8 @@ def mk_dir(d):
def set_build_dir(path):
global BUILD_DIR
BUILD_DIR = path
BUILD_X86_DIR = '%s/x86' % path
BUILD_X64_DIR = '%s/x64' % path
BUILD_X86_DIR = os.path.join(path, 'x86')
BUILD_X64_DIR = os.path.join(path, 'x64')
mk_dir(BUILD_X86_DIR)
mk_dir(BUILD_X64_DIR)
@ -52,16 +54,18 @@ def display_help():
print " -s, --silent do not print verbose messages."
print " -b <sudir>, --build=<subdir> subdirectory where x86 and x64 Z3 versions will be built (default: build-dist)."
print " -f, --force force script to regenerate Makefiles."
print " --nojava do not include Java bindings in the binary distribution files."
exit(0)
# Parse configuration option for mk_make script
def parse_options():
global FORCE_MK
global FORCE_MK, JAVA_ENABLED
path = BUILD_DIR
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
'help',
'silent',
'force'
'force',
'nojava'
])
for opt, arg in options:
if opt in ('-b', '--build'):
@ -74,18 +78,22 @@ def parse_options():
display_help()
elif opt in ('-f', '--force'):
FORCE_MK = True
elif opt == '--nojava':
JAVA_ENABLED = False
else:
raise MKException("Invalid command line option '%s'" % opt)
set_build_dir(path)
# Check whether build directory already exists or not
def check_build_dir(path):
return os.path.exists(path) and os.path.exists('%s/Makefile' % path)
return os.path.exists(path) and os.path.exists(os.path.join(path, 'Makefile'))
# Create a build directory using mk_make.py
def mk_build_dir(path, x64):
if not check_build_dir(path) or FORCE_MK:
opts = ["python", "scripts/mk_make.py", "-b", path]
opts = ["python", os.path.join('scripts', 'mk_make.py'), "-b", path]
if JAVA_ENABLED:
opts.append('--java')
if x64:
opts.append('-x')
if subprocess.call(opts) != 0:
@ -147,8 +155,12 @@ def mk_dist_dir_core(x64):
else:
platform = "x86"
build_path = BUILD_X86_DIR
dist_path = '%s/z3-%s.%s.%s-%s' % (DIST_DIR, major, minor, build, platform)
dist_path = os.path.join(DIST_DIR, 'z3-%s.%s.%s-%s' % (major, minor, build, platform))
mk_dir(dist_path)
if JAVA_ENABLED:
# HACK: Propagate JAVA_ENABLED flag to mk_util
# TODO: fix this hack
mk_util.JAVA_ENABLED = JAVA_ENABLED
mk_win_dist(build_path, dist_path)
if is_verbose():
print "Generated %s distribution folder at '%s'" % (platform, dist_path)
@ -225,7 +237,7 @@ def cp_vs_runtime_core(x64):
path = '%sredist\\%s' % (vcdir, platform)
VS_RUNTIME_FILES = []
os.path.walk(path, cp_vs_runtime_visitor, '*.dll')
bin_dist_path = '%s/%s/bin' % (DIST_DIR, get_dist_path(x64))
bin_dist_path = os.path.join(DIST_DIR, get_dist_path(x64), 'bin')
for f in VS_RUNTIME_FILES:
shutil.copy(f, bin_dist_path)
if is_verbose():
@ -236,8 +248,8 @@ def cp_vs_runtime():
cp_vs_runtime_core(False)
def cp_license():
shutil.copy("LICENSE.txt", "%s/%s" % (DIST_DIR, get_dist_path(True)))
shutil.copy("LICENSE.txt", "%s/%s" % (DIST_DIR, get_dist_path(False)))
shutil.copy("LICENSE.txt", os.path.join(DIST_DIR, get_dist_path(True)))
shutil.copy("LICENSE.txt", os.path.join(DIST_DIR, get_dist_path(False)))
# Entry point
def main():

9
scripts/trackall.sh Executable file
View file

@ -0,0 +1,9 @@
#!/bin/bash
# Script for "cloning" (and tracking) all branches at codeplex.
# On Windows, this script must be executed in the "git Bash" console.
for branch in `git branch -a | grep remotes | grep -v HEAD | grep -v master`; do
git branch --track ${branch##*/} $branch
done
git fetch --all
git pull --all

61
scripts/update_api.py
View file

@ -84,6 +84,19 @@ def lib():
raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
return _lib
def _to_ascii(s):
if isinstance(s, str):
return s.encode('ascii')
else:
return s
if sys.version < '3':
def _to_pystr(s):
return s
else:
def _to_pystr(s):
return s.decode('utf-8')
def init(PATH):
global _lib
_lib = ctypes.CDLL(PATH)
@ -146,20 +159,22 @@ next_type_id = FIRST_OBJ_ID
def def_Type(var, c_type, py_type):
global next_type_id
exec ('%s = %s' % (var, next_type_id)) in globals()
exec('%s = %s' % (var, next_type_id), globals())
Type2Str[next_type_id] = c_type
Type2PyStr[next_type_id] = py_type
next_type_id = next_type_id + 1
def def_Types():
pat1 = re.compile(" *def_Type.*")
import re
pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
for api_file in API_FILES:
api = open(api_file, 'r')
for line in api:
m = pat1.match(line)
if m:
eval(line)
for k, v in Type2Str.iteritems():
def_Type(m.group(1), m.group(2), m.group(3))
for k in Type2Str:
v = Type2Str[k]
if is_obj(k):
Type2Dotnet[k] = v
@ -258,7 +273,7 @@ def param2java(p):
elif param_type(p) == STRING:
return "StringPtr"
else:
print "ERROR: unreachable code"
print("ERROR: unreachable code")
assert(False)
exit(1)
if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
@ -313,6 +328,17 @@ def display_args(num):
core_py.write(", ")
core_py.write("a%s" % i)
def display_args_to_z3(params):
i = 0
for p in params:
if i > 0:
core_py.write(", ")
if param_type(p) == STRING:
core_py.write("_to_ascii(a%s)" % i)
else:
core_py.write("a%s" % i)
i = i + 1
def mk_py_wrappers():
core_py.write("\n")
for sig in _API2PY:
@ -327,13 +353,15 @@ def mk_py_wrappers():
core_py.write(" r = lib().%s(" % name)
else:
core_py.write(" lib().%s(" % name)
display_args(num)
display_args_to_z3(params)
core_py.write(")\n")
if len(params) > 0 and param_type(params[0]) == CONTEXT:
core_py.write(" err = lib().Z3_get_error_code(a0)\n")
core_py.write(" if err != Z3_OK:\n")
core_py.write(" raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))\n")
if result != VOID:
if result == STRING:
core_py.write(" return _to_pystr(r)\n")
elif result != VOID:
core_py.write(" return r\n")
core_py.write("\n")
@ -356,7 +384,8 @@ def mk_dotnet():
dotnet.write('#pragma warning disable 1591\n\n');
dotnet.write('namespace Microsoft.Z3\n')
dotnet.write('{\n')
for k, v in Type2Str.iteritems():
for k in Type2Str:
v = Type2Str[k]
if is_obj(k):
dotnet.write(' using %s = System.IntPtr;\n' % v)
dotnet.write('\n');
@ -579,7 +608,7 @@ def mk_java():
java_wrapper.write(' } \n\n')
java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n')
java_wrapper.write(' delete [] NEW; \n\n')
java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n')
java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n')
java_wrapper.write(' { \\\n')
java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n')
java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \\\n')
@ -702,7 +731,7 @@ def mk_java():
java_wrapper.write('}\n')
java_wrapper.write('#endif\n')
if is_verbose():
print "Generated '%s'" % java_nativef
print("Generated '%s'" % java_nativef)
def mk_log_header(file, name, params):
file.write("void log_%s(" % name)
@ -710,7 +739,7 @@ def mk_log_header(file, name, params):
for p in params:
if i > 0:
file.write(", ");
file.write("%s a%s" % (param2str(p), i))
file.write("%s a%s" % (param2str(p), i))
i = i + 1
file.write(")");
@ -981,8 +1010,8 @@ exe_c.close()
core_py.close()
if is_verbose():
print "Generated '%s'" % os.path.join(api_dir, 'api_log_macros.h')
print "Generated '%s'" % os.path.join(api_dir, 'api_log_macros.cpp')
print "Generated '%s'" % os.path.join(api_dir, 'api_commands.cpp')
print "Generated '%s'" % os.path.join(get_z3py_dir(), 'z3core.py')
print "Generated '%s'" % os.path.join(dotnet_dir, 'Native.cs')
print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.h'))
print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.cpp'))
print("Generated '%s'" % os.path.join(api_dir, 'api_commands.cpp'))
print("Generated '%s'" % os.path.join(get_z3py_dir(), 'z3core.py'))
print("Generated '%s'" % os.path.join(dotnet_dir, 'Native.cs'))

10
src/api/api_context.cpp
View file

@ -106,11 +106,11 @@ namespace api {
m_error_handler = &default_error_handler;
m_basic_fid = m().get_basic_family_id();
m_arith_fid = m().get_family_id("arith");
m_bv_fid = m().get_family_id("bv");
m_array_fid = m().get_family_id("array");
m_dt_fid = m().get_family_id("datatype");
m_datalog_fid = m().get_family_id("datalog_relation");
m_arith_fid = m().mk_family_id("arith");
m_bv_fid = m().mk_family_id("bv");
m_array_fid = m().mk_family_id("array");
m_dt_fid = m().mk_family_id("datatype");
m_datalog_fid = m().mk_family_id("datalog_relation");
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
if (!m_user_ref_count) {

1
src/api/api_datalog.h
View file

@ -55,6 +55,7 @@ namespace api {
std::string get_last_status();
std::string to_string(unsigned num_queries, expr*const* queries);
void cancel() { m_context.cancel(); }
void reset_cancel() { m_context.reset_cancel(); }
unsigned get_num_levels(func_decl* pred);
expr_ref get_cover_delta(int level, func_decl* pred);

74
src/api/api_parsers.cpp
View file

@ -252,42 +252,6 @@ extern "C" {
// ---------------
// Support for SMTLIB2
class z3_context_solver : public solver_na2as {
api::context & m_ctx;
smt::kernel & ctx() const { return m_ctx.get_smt_kernel(); }
public:
virtual ~z3_context_solver() {}
z3_context_solver(api::context& c) : m_ctx(c) {}
virtual void init_core(ast_manager & m, symbol const & logic) {}
virtual void collect_statistics(statistics & st) const {}
virtual void reset_core() { ctx().reset(); }
virtual void assert_expr(expr * t) { ctx().assert_expr(t); }
virtual void push_core() { ctx().push(); }
virtual void pop_core(unsigned n) { ctx().pop(n); }
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
return ctx().check(num_assumptions, assumptions);
}
virtual void get_unsat_core(ptr_vector<expr> & r) {
unsigned sz = ctx().get_unsat_core_size();
for (unsigned i = 0; i < sz; i++)
r.push_back(ctx().get_unsat_core_expr(i));
}
virtual void get_model(model_ref & m) { ctx().get_model(m); }
virtual proof * get_proof() { return ctx().get_proof(); }
virtual std::string reason_unknown() const { return ctx().last_failure_as_string(); }
virtual void get_labels(svector<symbol> & r) {
buffer<symbol> tmp;
ctx().get_relevant_labels(0, tmp);
r.append(tmp.size(), tmp.c_ptr());
}
// These are controlled by the main API
virtual void set_cancel(bool f) { }
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
virtual void set_progress_callback(progress_callback * callback) {}
};
Z3_ast parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is,
unsigned num_sorts,
Z3_symbol const sort_names[],
@ -298,9 +262,6 @@ extern "C" {
Z3_TRY;
cmd_context ctx(false, &(mk_c(c)->m()));
ctx.set_ignore_check(true);
if (exec) {
ctx.set_solver(alloc(z3_context_solver, *mk_c(c)));
}
for (unsigned i = 0; i < num_decls; ++i) {
ctx.insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
}
@ -353,39 +314,4 @@ extern "C" {
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_exec_smtlib2_string(Z3_context c, Z3_string str,
unsigned num_sorts,
Z3_symbol sort_names[],
Z3_sort sorts[],
unsigned num_decls,
Z3_symbol decl_names[],
Z3_func_decl decls[]) {
Z3_TRY;
cmd_context ctx(false, &(mk_c(c)->m()));
std::string s(str);
std::istringstream is(s);
// No logging for this one, since it private.
return parse_smtlib2_stream(true, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_exec_smtlib2_file(Z3_context c, Z3_string file_name,
unsigned num_sorts,
Z3_symbol sort_names[],
Z3_sort sorts[],
unsigned num_decls,
Z3_symbol decl_names[],
Z3_func_decl decls[]) {
Z3_TRY;
std::ifstream is(file_name);
if (!is) {
SET_ERROR_CODE(Z3_PARSER_ERROR);
return 0;
}
// No logging for this one, since it private.
return parse_smtlib2_stream(true, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
Z3_CATCH_RETURN(0);
}
};

56
src/api/api_solver.cpp
View file

@ -30,19 +30,20 @@ Revision History:
#include"scoped_timer.h"
#include"smt_strategic_solver.h"
#include"smt_solver.h"
#include"smt_implied_equalities.h"
extern "C" {
static void init_solver_core(Z3_context c, Z3_solver _s) {
ast_manager & m = mk_c(c)->m();
Z3_solver_ref * s = to_solver(_s);
mk_c(c)->params().init_solver_params(mk_c(c)->m(), *(s->m_solver), s->m_params);
s->m_solver->init(m, s->m_logic);
s->m_initialized = true;
bool proofs_enabled, models_enabled, unsat_core_enabled;
params_ref p = s->m_params;
mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
}
static void init_solver(Z3_context c, Z3_solver s) {
if (!to_solver(s)->m_initialized)
if (to_solver(s)->m_solver.get() == 0)
init_solver_core(c, s);
}
@ -50,8 +51,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_simple_solver(c);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref);
s->m_solver = mk_smt_solver();
Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_solver_factory());
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -62,8 +62,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_solver(c);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref);
s->m_solver = mk_smt_strategic_solver();
Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_strategic_solver_factory());
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -74,8 +73,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_solver_for_logic(c, logic);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref, to_symbol(logic));
s->m_solver = mk_smt_strategic_solver(true /* force solver to use tactics even when auto_config is disabled */);
Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_strategic_solver_factory(to_symbol(logic)));
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -86,8 +84,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_solver_from_tactic(c, t);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref);
s->m_solver = alloc(tactic2solver, to_tactic_ref(t));
Z3_solver_ref * s = alloc(Z3_solver_ref, mk_tactic2solver_factory(to_tactic_ref(t)));
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -100,7 +97,12 @@ extern "C" {
RESET_ERROR_CODE();
std::ostringstream buffer;
param_descrs descrs;
bool initialized = to_solver(s)->m_solver.get() != 0;
if (!initialized)
init_solver(c, s);
to_solver_ref(s)->collect_param_descrs(descrs);
if (!initialized)
to_solver(s)->m_solver = 0;
descrs.display(buffer);
return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN("");
@ -112,7 +114,12 @@ extern "C" {
RESET_ERROR_CODE();
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
mk_c(c)->save_object(d);
bool initialized = to_solver(s)->m_solver.get() != 0;
if (!initialized)
init_solver(c, s);
to_solver_ref(s)->collect_param_descrs(d->m_descrs);
if (!initialized)
to_solver(s)->m_solver = 0;
Z3_param_descrs r = of_param_descrs(d);
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
@ -122,7 +129,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_set_params(c, s, p);
RESET_ERROR_CODE();
if (to_solver(s)->m_initialized) {
if (to_solver(s)->m_solver) {
bool old_model = to_solver(s)->m_params.get_bool("model", true);
bool new_model = to_param_ref(p).get_bool("model", true);
if (old_model != new_model)
@ -176,8 +183,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_reset(c, s);
RESET_ERROR_CODE();
to_solver_ref(s)->reset();
to_solver(s)->m_initialized = false;
to_solver(s)->m_solver = 0;
Z3_CATCH;
}
@ -352,4 +358,22 @@ extern "C" {
return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN("");
}
Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
Z3_solver s,
unsigned num_terms,
Z3_ast const terms[],
unsigned class_ids[]) {
Z3_TRY;
LOG_Z3_get_implied_equalities(c, s, num_terms, terms, class_ids);
ast_manager& m = mk_c(c)->m();
RESET_ERROR_CODE();
CHECK_SEARCHING(c);
init_solver(c, s);
lbool result = smt::implied_equalities(m, *to_solver_ref(s), num_terms, to_exprs(terms), class_ids);
return static_cast<Z3_lbool>(result);
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
};

15
src/api/api_solver.h
View file

@ -22,17 +22,16 @@ Revision History:
#include"solver.h"
struct Z3_solver_ref : public api::object {
solver * m_solver;
params_ref m_params;
bool m_initialized;
symbol m_logic;
Z3_solver_ref():m_solver(0), m_initialized(false), m_logic(symbol::null) {}
Z3_solver_ref(symbol const & logic):m_solver(0), m_initialized(false), m_logic(logic) {}
virtual ~Z3_solver_ref() { dealloc(m_solver); }
scoped_ptr<solver_factory> m_solver_factory;
ref<solver> m_solver;
params_ref m_params;
symbol m_logic;
Z3_solver_ref(solver_factory * f):m_solver_factory(f), m_solver(0), m_logic(symbol::null) {}
virtual ~Z3_solver_ref() {}
};
inline Z3_solver_ref * to_solver(Z3_solver s) { return reinterpret_cast<Z3_solver_ref *>(s); }
inline Z3_solver of_solver(Z3_solver_ref * s) { return reinterpret_cast<Z3_solver>(s); }
inline solver * to_solver_ref(Z3_solver s) { return to_solver(s)->m_solver; }
inline solver * to_solver_ref(Z3_solver s) { return to_solver(s)->m_solver.get(); }
#endif

14
src/api/api_solver_old.cpp
View file

@ -22,7 +22,6 @@ Revision History:
#include"api_log_macros.h"
#include"api_context.h"
#include"api_model.h"
#include"smt_implied_equalities.h"
#include"cancel_eh.h"
extern "C" {
@ -112,19 +111,6 @@ extern "C" {
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
unsigned num_terms,
Z3_ast const terms[],
unsigned class_ids[]) {
Z3_TRY;
LOG_Z3_get_implied_equalities(c, num_terms, terms, class_ids);
RESET_ERROR_CODE();
CHECK_SEARCHING(c);
lbool result = smt::implied_equalities(mk_c(c)->get_smt_kernel(), num_terms, to_exprs(terms), class_ids);
return static_cast<Z3_lbool>(result);
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
Z3_lbool Z3_API Z3_check_assumptions(Z3_context c,
unsigned num_assumptions, Z3_ast const assumptions[],

2
src/api/ml/Makefile.build
View file

@ -13,7 +13,7 @@ XCDBG=-g $(CFLAGS)
XCOPT=-ccopt -Ox -ccopt -Oy- $(CFLAGS)
# ole32 is needed by camlidl (COM support)
XLIB=-cclib ole32.lib
AR=lib /nologo /LIBPATH:../../build ../../z3.lib /out:
AR=lib /nologo /LIBPATH:../../build ../../libz3.lib /out:
O=obj
A=lib
else

44
src/api/ml/README-linux
View file

@ -1,22 +1,22 @@
The OCaml API for Z3 was tested using OCaml 3.12.1.
You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- To build the OCaml API for Z3:
./build-lib.sh
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Remark: Building the OCaml API copies some pathnames into files,
so the OCaml API must be recompiled if the Z3 library files are moved.
See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3.
Acknowledgements:
The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg.
Many thanks to them!
The OCaml API for Z3 was tested using OCaml 3.12.1.
You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- To build the OCaml API for Z3:
./build-lib.sh
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Remark: Building the OCaml API copies some pathnames into files,
so the OCaml API must be recompiled if the Z3 library files are moved.
See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3.
Acknowledgements:
The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg.
Many thanks to them!

44
src/api/ml/README-osx
View file

@ -1,22 +1,22 @@
The OCaml API for Z3 was tested using OCaml 3.12.1.
You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- To build the OCaml API for Z3:
./build-lib.sh
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Remark: Building the OCaml API copies some pathnames into files,
so the OCaml API must be recompiled if the Z3 library files are moved.
See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3.
Acknowledgements:
The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg.
Many thanks to them!
The OCaml API for Z3 was tested using OCaml 3.12.1.
You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- To build the OCaml API for Z3:
./build-lib.sh
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Remark: Building the OCaml API copies some pathnames into files,
so the OCaml API must be recompiled if the Z3 library files are moved.
See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3.
Acknowledgements:
The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg.
Many thanks to them!

34
src/api/ml/README-test-linux
View file

@ -1,17 +1,17 @@
This directory contains scripts to build the test application using
OCaml. You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- One must build the OCaml library before compiling the example.
Go to directory ../ocaml
- Use 'build-test.sh' to build the test application using the OCaml compiler.
Remark: The OCaml and C compiler tool chains must be configured in your environment.
- Use 'exec.sh' to execute test_mlapi. The script sets LD_LIBRARY_PATH, and invokes test_mlapi.
This directory contains scripts to build the test application using
OCaml. You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- One must build the OCaml library before compiling the example.
Go to directory ../ocaml
- Use 'build-test.sh' to build the test application using the OCaml compiler.
Remark: The OCaml and C compiler tool chains must be configured in your environment.
- Use 'exec.sh' to execute test_mlapi. The script sets LD_LIBRARY_PATH, and invokes test_mlapi.

34
src/api/ml/README-test-osx
View file

@ -1,17 +1,17 @@
This directory contains scripts to build the test application using
OCaml. You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- One must build the OCaml library before compiling the example.
Go to directory ../ocaml
- Use 'build-test.sh' to build the test application using the OCaml compiler.
Remark: The OCaml and C compiler tool chains must be configured in your environment.
- Use 'exec.sh' to execute test_mlapi. The script sets DYLD_LIBRARY_PATH, and invokes test_mlapi.
This directory contains scripts to build the test application using
OCaml. You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- One must build the OCaml library before compiling the example.
Go to directory ../ocaml
- Use 'build-test.sh' to build the test application using the OCaml compiler.
Remark: The OCaml and C compiler tool chains must be configured in your environment.
- Use 'exec.sh' to execute test_mlapi. The script sets DYLD_LIBRARY_PATH, and invokes test_mlapi.

8
src/api/ml/exec.sh
View file

@ -1,4 +1,4 @@
#!/bin/sh
export LD_LIBRARY_PATH=../../lib:$LD_LIBRARY_PATH # for linux
export DYLD_LIBRARY_PATH=../../lib:$DYLD_LIBRARY_PATH # for osx
./test_mlapi
#!/bin/sh
export LD_LIBRARY_PATH=../../lib:$LD_LIBRARY_PATH # for linux
export DYLD_LIBRARY_PATH=../../lib:$DYLD_LIBRARY_PATH # for osx
./test_mlapi

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

@ -229,16 +229,6 @@ and param_kind =
| PK_OTHER
| PK_INVALID
and search_failure =
| NO_FAILURE
| UNKNOWN
| TIMEOUT
| MEMOUT_WATERMARK
| CANCELED
| NUM_CONFLICTS
| THEORY
| QUANTIFIERS
and ast_print_mode =
| PRINT_SMTLIB_FULL
| PRINT_LOW_LEVEL
@ -1596,6 +1586,9 @@ external stats_get_uint_value : context -> stats -> int -> int
external stats_get_double_value : context -> stats -> int -> float
= "camlidl_z3_Z3_stats_get_double_value"
external get_implied_equalities : context -> solver -> ast array -> lbool * int array
= "camlidl_z3_Z3_get_implied_equalities"
(* Internal auxiliary functions: *)
@ -3027,9 +3020,6 @@ external check : context -> lbool
external check_assumptions : context -> ast array -> int -> ast array -> lbool * model * ast * int * ast array
= "camlidl_z3V3_Z3_check_assumptions"
external get_implied_equalities : context -> ast array -> lbool * int array
= "camlidl_z3V3_Z3_get_implied_equalities"
external del_model : context -> model -> unit
= "camlidl_z3V3_Z3_del_model"

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

@ -229,16 +229,6 @@ and param_kind =
| PK_OTHER
| PK_INVALID
and search_failure =
| NO_FAILURE
| UNKNOWN
| TIMEOUT
| MEMOUT_WATERMARK
| CANCELED
| NUM_CONFLICTS
| THEORY
| QUANTIFIERS
and ast_print_mode =
| PRINT_SMTLIB_FULL
| PRINT_LOW_LEVEL
@ -1013,37 +1003,22 @@ and goal_prec =
- PK_INVALID invalid parameter.
*)
(**
{!search_failure}
The different kinds of search failure types.
- NO_FAILURE: The last search was successful
- UNKNOWN: Undocumented failure reason
- TIMEOUT: Timeout
- MEMOUT_WATERMAK: Search hit a memory high-watermak limit
- CANCELED: External cancel flag was set
- NUM_CONFLICTS: Maximum number of conflicts was reached
- THEORY: Theory is incomplete
- QUANTIFIERS: Logical context contains universal quantifiers
*)
(**
{!ast_print_mode}
{!ast_print_mode}
Z3 pretty printing modes (See {!set_ast_print_mode}).
- PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format.
- PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
- PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format.
- PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
- PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format.
- PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x compliant format.
*)
(**
{!error_code}
Z3 error codes
- OK: No error.
- SORT_ERROR: User tried to build an invalid (type incorrect) AST.
- IOB: Index out of bounds.
- INVALID_ARG: Invalid argument was provided.
- PARSER_ERROR: An error occurred when parsing a string or file.
- NO_PARSER: Parser output is not available, that is, user didn't invoke {!parse_smtlib_string} or {!parse_smtlib_file}.
{!error_code}
Z3 error codes
- OK: No error.
- SORT_ERROR: User tried to build an invalid (type incorrect) AST.
- IOB: Index out of bounds.
- INVALID_ARG: Invalid argument was provided.
- PARSER_ERROR: An error occurred when parsing a string or file.
- NO_PARSER: Parser output is not available, that is, user didn't invoke {!parse_smtlib_string} or {!parse_smtlib_file}.
- INVALID_PATTERN: Invalid pattern was used to build a quantifier.
- MEMOUT_FAIL: A memory allocation failure was encountered.
- FILE_ACCESS_ERRROR: A file could not be accessed.
@ -1054,17 +1029,16 @@ and goal_prec =
*)
(**
Definitions for update_api.py
def_Type('CONFIG', 'config', 'Config')
def_Type('CONTEXT', 'context', 'ContextObj')
def_Type('AST', 'ast', 'Ast')
def_Type('APP', 'app', 'Ast')
def_Type('SORT', 'sort', 'Sort')
def_Type('FUNC_DECL', 'func_decl', 'FuncDecl')
def_Type('PATTERN', 'pattern', 'Pattern')
def_Type('MODEL', 'model', 'Model')
def_Type('LITERALS', 'literals', 'Literals')
def_Type('CONSTRUCTOR', 'constructor', 'Constructor')
def_Type('CONFIG', 'config', 'Config')
def_Type('CONTEXT', 'context', 'ContextObj')
def_Type('AST', 'ast', 'Ast')
def_Type('APP', 'app', 'Ast')
def_Type('SORT', 'sort', 'Sort')
def_Type('FUNC_DECL', 'func_decl', 'FuncDecl')
def_Type('PATTERN', 'pattern', 'Pattern')
def_Type('MODEL', 'model', 'Model')
def_Type('LITERALS', 'literals', 'Literals')
def_Type('CONSTRUCTOR', 'constructor', 'Constructor')
def_Type('CONSTRUCTOR_LIST', 'constructor_list', 'ConstructorList')
def_Type('THEORY', 'theory', 'ctypes.c_void_p')
def_Type('THEORY_DATA', 'theory_data', 'ctypes.c_void_p')
@ -6050,6 +6024,30 @@ external stats_get_uint_value : context -> stats -> int -> int
external stats_get_double_value : context -> stats -> int -> float
= "camlidl_z3_Z3_stats_get_double_value"
(**
{2 {L Deprecated Constraints API}}
*)
(**
Summary: Retrieve congruence class representatives for terms.
The function can be used for relying on Z3 to identify equal terms under the current
set of assumptions. The array of terms and array of class identifiers should have
the same length. The class identifiers are numerals that are assigned to the same
value for their corresponding terms if the current context forces the terms to be
equal. You cannot deduce that terms corresponding to different numerals must be all different,
(especially when using non-convex theories).
All implied equalities are returned by this call.
This means that two terms map to the same class identifier if and only if
the current context implies that they are equal.
A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in.
The function return L_FALSE if the current assertions are not satisfiable.
- {b See also}: {!check_and_get_model}
- {b See also}: {!check}
@deprecated To be moved outside of API.
def_API('get_implied_equalities', UINT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
*)
external get_implied_equalities : context -> solver -> ast array -> lbool * int array
= "camlidl_z3_Z3_get_implied_equalities"
(**
{2 {L Legacy V3 API}}
@ -10595,32 +10593,6 @@ external check : context -> lbool
external check_assumptions : context -> ast array -> int -> ast array -> lbool * model * ast * int * ast array
= "camlidl_z3V3_Z3_check_assumptions"
(**
Summary: Retrieve congruence class representatives for terms.
The function can be used for relying on Z3 to identify equal terms under the current
set of assumptions. The array of terms and array of class identifiers should have
the same length. The class identifiers are numerals that are assigned to the same
value for their corresponding terms if the current context forces the terms to be
equal. You cannot deduce that terms corresponding to different numerals must be all different,
(especially when using non-convex theories).
All implied equalities are returned by this call.
This means that two terms map to the same class identifier if and only if
the current context implies that they are equal.
A side-effect of the function is a satisfiability check.
The function return L_FALSE if the current assertions are not satisfiable.
- {b See also}: {!check_and_get_model}
- {b See also}: {!check}
@deprecated Subsumed by solver API
def_API('get_implied_equalities', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _out_array(1, UINT)))
*)
external get_implied_equalities : context -> ast array -> lbool * int array
= "camlidl_z3V3_Z3_get_implied_equalities"
(**
Summary: Delete a model object.

132
src/api/ml/z3_stubs.c
View file

@ -605,30 +605,7 @@ value _v1;
return _v1;
}
int camlidl_transl_table_z3_enum_8[8] = {
Z3_NO_FAILURE,
Z3_UNKNOWN,
Z3_TIMEOUT,
Z3_MEMOUT_WATERMARK,
Z3_CANCELED,
Z3_NUM_CONFLICTS,
Z3_THEORY,
Z3_QUANTIFIERS,
};
void camlidl_ml2c_z3_Z3_search_failure(value _v1, Z3_search_failure * _c2, camlidl_ctx _ctx)
{
(*_c2) = camlidl_transl_table_z3_enum_8[Int_val(_v1)];
}
value camlidl_c2ml_z3_Z3_search_failure(Z3_search_failure * _c2, camlidl_ctx _ctx)
{
value _v1;
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_8, 8, "typedef Z3_search_failure: bad enum value");
return _v1;
}
int camlidl_transl_table_z3_enum_9[4] = {
int camlidl_transl_table_z3_enum_8[4] = {
Z3_PRINT_SMTLIB_FULL,
Z3_PRINT_LOW_LEVEL,
Z3_PRINT_SMTLIB_COMPLIANT,
@ -637,7 +614,7 @@ int camlidl_transl_table_z3_enum_9[4] = {
void camlidl_ml2c_z3_Z3_ast_print_mode(value _v1, Z3_ast_print_mode * _c2, camlidl_ctx _ctx)
{
(*_c2) = camlidl_transl_table_z3_enum_9[Int_val(_v1)];
(*_c2) = camlidl_transl_table_z3_enum_8[Int_val(_v1)];
}
value camlidl_c2ml_z3_Z3_ast_print_mode(Z3_ast_print_mode * _c2, camlidl_ctx _ctx)
@ -653,7 +630,7 @@ value _v1;
return _v1;
}
int camlidl_transl_table_z3_enum_10[13] = {
int camlidl_transl_table_z3_enum_9[13] = {
Z3_OK,
Z3_SORT_ERROR,
Z3_IOB,
@ -671,13 +648,13 @@ int camlidl_transl_table_z3_enum_10[13] = {
void camlidl_ml2c_z3_Z3_error_code(value _v1, Z3_error_code * _c2, camlidl_ctx _ctx)
{
(*_c2) = camlidl_transl_table_z3_enum_10[Int_val(_v1)];
(*_c2) = camlidl_transl_table_z3_enum_9[Int_val(_v1)];
}
value camlidl_c2ml_z3_Z3_error_code(Z3_error_code * _c2, camlidl_ctx _ctx)
{
value _v1;
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_10, 13, "typedef Z3_error_code: bad enum value");
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_9, 13, "typedef Z3_error_code: bad enum value");
return _v1;
}
@ -707,7 +684,7 @@ void check_error_code (Z3_context c)
void* error_handler_static = NULL;
int camlidl_transl_table_z3_enum_11[4] = {
int camlidl_transl_table_z3_enum_10[4] = {
Z3_GOAL_PRECISE,
Z3_GOAL_UNDER,
Z3_GOAL_OVER,
@ -716,7 +693,7 @@ int camlidl_transl_table_z3_enum_11[4] = {
void camlidl_ml2c_z3_Z3_goal_prec(value _v1, Z3_goal_prec * _c2, camlidl_ctx _ctx)
{
(*_c2) = camlidl_transl_table_z3_enum_11[Int_val(_v1)];
(*_c2) = camlidl_transl_table_z3_enum_10[Int_val(_v1)];
}
value camlidl_c2ml_z3_Z3_goal_prec(Z3_goal_prec * _c2, camlidl_ctx _ctx)
@ -11072,7 +11049,56 @@ check_error_code(c);
return _vres;
}
void caml_z3_error_handler(Z3_context c, Z3_error_code e) { static char buffer[128]; char * msg = Z3_get_error_msg_ex(c, e); if (strlen(msg) > 100) { failwith("Z3: error message is too big to fit in buffer"); } else { sprintf(buffer, "Z3: %s", msg); failwith(buffer); } }
value camlidl_z3_Z3_get_implied_equalities(
value _v_c,
value _v_s,
value _v_terms)
{
Z3_context c; /*in*/
Z3_solver s; /*in*/
unsigned int num_terms; /*in*/
Z3_ast const *terms; /*in*/
unsigned int *class_ids; /*out*/
Z3_lbool _res;
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
camlidl_ctx _ctx = &_ctxs;
mlsize_t _c1;
mlsize_t _c2;
value _v3;
mlsize_t _c4;
value _v5;
value _vresult;
value _vres[2] = { 0, 0, };
camlidl_ml2c_z3_Z3_context(_v_c, &c, _ctx);
camlidl_ml2c_z3_Z3_solver(_v_s, &s, _ctx);
_c1 = Wosize_val(_v_terms);
terms = camlidl_malloc(_c1 * sizeof(Z3_ast const ), _ctx);
for (_c2 = 0; _c2 < _c1; _c2++) {
_v3 = Field(_v_terms, _c2);
camlidl_ml2c_z3_Z3_ast(_v3, &terms[_c2], _ctx);
}
num_terms = _c1;
class_ids = camlidl_malloc(num_terms * sizeof(unsigned int ), _ctx);
_res = Z3_get_implied_equalities(c, s, num_terms, terms, class_ids);
Begin_roots_block(_vres, 2)
_vres[0] = camlidl_c2ml_z3_Z3_lbool(&_res, _ctx);
_vres[1] = camlidl_alloc(num_terms, 0);
for (_c4 = 0; _c4 < num_terms; _c4++) {
_v5 = Val_int(class_ids[_c4]);
modify(&Field(_vres[1], _c4), _v5);
}
_vresult = camlidl_alloc_small(2, 0);
Field(_vresult, 0) = _vres[0];
Field(_vresult, 1) = _vres[1];
End_roots()
camlidl_free(_ctx);
/* begin user-supplied deallocation sequence */
check_error_code(c);
/* end user-supplied deallocation sequence */
return _vresult;
}
void camlidl_ml2c_z3V3_Z3_symbol(value _v1, Z3_symbol * _c2, camlidl_ctx _ctx)
{
*_c2 = *((Z3_symbol *) Bp_val(_v1));
@ -18250,50 +18276,6 @@ value camlidl_z3V3_Z3_check_assumptions(
return _vresult;
}
value camlidl_z3V3_Z3_get_implied_equalities(
value _v_c,
value _v_terms)
{
Z3_context c; /*in*/
unsigned int num_terms; /*in*/
Z3_ast const *terms; /*in*/
unsigned int *class_ids; /*out*/
Z3_lbool _res;
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
camlidl_ctx _ctx = &_ctxs;
mlsize_t _c1;
mlsize_t _c2;
value _v3;
mlsize_t _c4;
value _v5;
value _vresult;
value _vres[2] = { 0, 0, };
camlidl_ml2c_z3V3_Z3_context(_v_c, &c, _ctx);
_c1 = Wosize_val(_v_terms);
terms = camlidl_malloc(_c1 * sizeof(Z3_ast const ), _ctx);
for (_c2 = 0; _c2 < _c1; _c2++) {
_v3 = Field(_v_terms, _c2);
camlidl_ml2c_z3V3_Z3_ast(_v3, &terms[_c2], _ctx);
}
num_terms = _c1;
class_ids = camlidl_malloc(num_terms * sizeof(unsigned int ), _ctx);
_res = Z3_get_implied_equalities(c, num_terms, terms, class_ids);
Begin_roots_block(_vres, 2)
_vres[0] = camlidl_c2ml_z3V3_Z3_lbool(&_res, _ctx);
_vres[1] = camlidl_alloc(num_terms, 0);
for (_c4 = 0; _c4 < num_terms; _c4++) {
_v5 = Val_int(class_ids[_c4]);
modify(&Field(_vres[1], _c4), _v5);
}
_vresult = camlidl_alloc_small(2, 0);
Field(_vresult, 0) = _vres[0];
Field(_vresult, 1) = _vres[1];
End_roots()
camlidl_free(_ctx);
return _vresult;
}
value camlidl_z3V3_Z3_del_model(
value _v_c,
value _v_m)

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

@ -37,15 +37,23 @@ Z3 exceptions:
... # the expression x + y is type incorrect
... n = x + y
... except Z3Exception as ex:
... print "failed:", ex
... print("failed: %s" % ex)
failed: 'sort mismatch'
"""
from z3core import *
from z3types import *
from z3consts import *
from z3printer import *
import sys
import io
if sys.version < '3':
def _is_int(v):
return isinstance(v, int) or isinstance(v, long)
else:
def _is_int(v):
return isinstance(v, int)
def enable_trace(msg):
Z3_enable_trace(msg)
@ -102,12 +110,12 @@ _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
# list of arguments.
def _get_args(args):
try:
if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
return args[0]
else:
return args
if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
return args[0]
else:
return args
except: # len is not necessarily defined when args is not a sequence (use reflection?)
return args
return args
def _Z3python_error_handler_core(c, e):
# Do nothing error handler, just avoid exit(0)
@ -140,7 +148,8 @@ class Context:
if __debug__:
_z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
conf = Z3_mk_config()
for key, value in kws.iteritems():
for key in kws:
value = kws[key]
Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
prev = None
for a in args:
@ -209,10 +218,12 @@ def set_param(*args, **kws):
if __debug__:
_z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
new_kws = {}
for k, v in kws.iteritems():
for k in kws:
v = kws[k]
if not set_pp_option(k, v):
new_kws[k] = v
for key, value in new_kws.iteritems():
for key in new_kws:
value = new_kws[key]
Z3_global_param_set(str(key).upper(), _to_param_value(value))
prev = None
for a in args:
@ -240,7 +251,7 @@ def get_param(name):
"""
ptr = (ctypes.c_char_p * 1)()
if Z3_global_param_get(str(name), ptr):
r = str(ptr[0])
r = z3core._to_pystr(ptr[0])
return r
raise Z3Exception("failed to retrieve value for '%s'" % name)
@ -899,11 +910,22 @@ def _coerce_exprs(a, b, ctx=None):
b = s.cast(b)
return (a, b)
def _reduce(f, l, a):
r = a
for e in l:
r = f(r, e)
return r
def _coerce_expr_list(alist, ctx=None):
if filter(is_expr, alist) == []:
alist = map(lambda a: _py2expr(a, ctx), alist)
s = reduce(_coerce_expr_merge, alist, None)
return map(lambda a: s.cast(a), alist)
has_expr = False
for a in alist:
if is_expr(a):
has_expr = True
break
if not has_expr:
alist = [ _py2expr(a, ctx) for a in alist ]
s = _reduce(_coerce_expr_merge, alist, None)
return [ s.cast(a) for a in alist ]
def is_expr(a):
"""Return `True` if `a` is a Z3 expression.
@ -1518,7 +1540,7 @@ def MultiPattern(*args):
"""
if __debug__:
_z3_assert(len(args) > 0, "At least one argument expected")
_z3_assert(all(map(is_expr, args)), "Z3 expressions expected")
_z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected")
ctx = args[0].ctx
args, sz = _to_ast_array(args)
return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
@ -1695,9 +1717,9 @@ def is_quantifier(a):
def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
if __debug__:
_z3_assert(is_bool(body), "Z3 expression expected")
_z3_assert(is_const(vs) or (len(vs) > 0 and all(map(is_const, vs))), "Invalid bounded variable(s)")
_z3_assert(all(map(lambda a: is_pattern(a) or is_expr(a), patterns)), "Z3 patterns expected")
_z3_assert(all(map(is_expr, no_patterns)), "no patterns are Z3 expressions")
_z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)")
_z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected")
_z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")
ctx = body.ctx
if is_app(vs):
vs = [vs]
@ -1706,7 +1728,7 @@ def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[],
for i in range(num_vars):
## TODO: Check if is constant
_vs[i] = vs[i].as_ast()
patterns = map(_to_pattern, patterns)
patterns = [ _to_pattern(p) for p in patterns ]
num_pats = len(patterns)
_pats = (Pattern * num_pats)()
for i in range(num_pats):
@ -2008,7 +2030,7 @@ class ArithRef(ExprRef):
def __truediv__(self, other):
"""Create the Z3 expression `other/self`."""
self.__div__(other)
return self.__div__(other)
def __rdiv__(self, other):
"""Create the Z3 expression `other/self`.
@ -2029,7 +2051,7 @@ class ArithRef(ExprRef):
def __rtruediv__(self, other):
"""Create the Z3 expression `other/self`."""
self.__rdiv__(other)
return self.__rdiv__(other)
def __mod__(self, other):
"""Create the Z3 expression `other%self`.
@ -2413,11 +2435,11 @@ class IntNumRef(ArithRef):
>>> v + 1
1 + 1
>>> v.as_long() + 1
2L
2
"""
if __debug__:
_z3_assert(self.is_int(), "Integer value expected")
return long(self.as_string())
return int(self.as_string())
def as_string(self):
"""Return a Z3 integer numeral as a Python string.
@ -2464,8 +2486,8 @@ class RatNumRef(ArithRef):
10000000000
>>> v + 1
10000000000 + 1
>>> v.numerator_as_long() + 1
10000000001L
>>> v.numerator_as_long() + 1 == 10000000001
True
"""
return self.numerator().as_long()
@ -2476,7 +2498,7 @@ class RatNumRef(ArithRef):
>>> v
1/3
>>> v.denominator_as_long()
3L
3
"""
return self.denominator().as_long()
@ -2529,7 +2551,7 @@ class AlgebraicNumRef(ArithRef):
def _py2expr(a, ctx=None):
if isinstance(a, bool):
return BoolVal(a, ctx)
if isinstance(a, int) or isinstance(a, long):
if _is_int(a):
return IntVal(a, ctx)
if isinstance(a, float):
return RealVal(a, ctx)
@ -2576,9 +2598,7 @@ def _to_int_str(val):
return "1"
else:
return "0"
elif isinstance(val, int):
return str(val)
elif isinstance(val, long):
elif _is_int(val):
return str(val)
elif isinstance(val, str):
return val
@ -2625,8 +2645,8 @@ def RatVal(a, b, ctx=None):
Real
"""
if __debug__:
_z3_assert(isinstance(a, int) or isinstance(a, str) or isinstance(a, long), "First argument cannot be converted into an integer")
_z3_assert(isinstance(b, int) or isinstance(b, str) or isinstance(a, long), "Second argument cannot be converted into an integer")
_z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
_z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
return simplify(RealVal(a, ctx)/RealVal(b, ctx))
def Q(a, b, ctx=None):
@ -3078,7 +3098,7 @@ class BitVecRef(ExprRef):
def __truediv__(self, other):
"""Create the Z3 expression (signed) division `self / other`."""
self.__div__(other)
return self.__div__(other)
def __rdiv__(self, other):
"""Create the Z3 expression (signed) division `other / self`.
@ -3098,7 +3118,7 @@ class BitVecRef(ExprRef):
def __rtruediv__(self, other):
"""Create the Z3 expression (signed) division `other / self`."""
self.__rdiv__(other)
return self.__rdiv__(other)
def __mod__(self, other):
"""Create the Z3 expression (signed) mod `self % other`.
@ -3218,9 +3238,9 @@ class BitVecRef(ExprRef):
>>> BitVecVal(4, 3)
4
>>> BitVecVal(4, 3).as_signed_long()
-4L
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2L
-2
>>> simplify(BitVecVal(4, 3) >> 1)
6
>>> simplify(LShR(BitVecVal(4, 3), 1))
@ -3284,32 +3304,32 @@ class BitVecNumRef(BitVecRef):
>>> v = BitVecVal(0xbadc0de, 32)
>>> v
195936478
>>> print "0x%.8x" % v.as_long()
>>> print("0x%.8x" % v.as_long())
0x0badc0de
"""
return long(self.as_string())
return int(self.as_string())
def as_signed_long(self):
"""Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign.
>>> BitVecVal(4, 3).as_signed_long()
-4L
-4
>>> BitVecVal(7, 3).as_signed_long()
-1L
-1
>>> BitVecVal(3, 3).as_signed_long()
3L
>>> BitVecVal(2L**32 - 1, 32).as_signed_long()
-1L
>>> BitVecVal(2L**64 - 1, 64).as_signed_long()
-1L
3
>>> BitVecVal(2**32 - 1, 32).as_signed_long()
-1
>>> BitVecVal(2**64 - 1, 64).as_signed_long()
-1
"""
sz = long(self.size())
sz = self.size()
val = self.as_long()
if val >= 2L**(sz - 1):
val = val - 2L**sz
if val < -2L**(sz - 1):
val = val + 2L**sz
return val
if val >= 2**(sz - 1):
val = val - 2**sz
if val < -2**(sz - 1):
val = val + 2**sz
return int(val)
def as_string(self):
return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
@ -3379,7 +3399,7 @@ def BitVecVal(val, bv, ctx=None):
>>> v = BitVecVal(10, 32)
>>> v
10
>>> print "0x%.8x" % v.as_long()
>>> print("0x%.8x" % v.as_long())
0x0000000a
"""
if is_bv_sort(bv):
@ -3440,12 +3460,12 @@ def Concat(*args):
Concat(Concat(1, 1 + 1), 1)
>>> simplify(Concat(v, v+1, v))
289
>>> print "%.3x" % simplify(Concat(v, v+1, v)).as_long()
>>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
121
"""
args = _get_args(args)
if __debug__:
_z3_assert(all(map(is_bv, args)), "All arguments must be Z3 bit-vector expressions.")
_z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
_z3_assert(len(args) >= 2, "At least two arguments expected.")
ctx = args[0].ctx
r = args[0]
@ -3615,9 +3635,9 @@ def LShR(a, b):
>>> BitVecVal(4, 3)
4
>>> BitVecVal(4, 3).as_signed_long()
-4L
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2L
-2
>>> simplify(BitVecVal(4, 3) >> 1)
6
>>> simplify(LShR(BitVecVal(4, 3), 1))
@ -3682,7 +3702,7 @@ def SignExt(n, a):
254
>>> v.size()
8
>>> print "%.x" % v.as_long()
>>> print("%.x" % v.as_long())
fe
"""
if __debug__:
@ -3727,12 +3747,12 @@ def RepeatBitVec(n, a):
>>> n.size()
32
>>> v0 = BitVecVal(10, 4)
>>> print "%.x" % v0.as_long()
>>> print("%.x" % v0.as_long())
a
>>> v = simplify(RepeatBitVec(4, v0))
>>> v.size()
16
>>> print "%.x" % v.as_long()
>>> print("%.x" % v.as_long())
aaaa
"""
if __debug__:
@ -4006,7 +4026,7 @@ def Map(f, *args):
if __debug__:
_z3_assert(len(args) > 0, "At least one Z3 array expression expected")
_z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
_z3_assert(all(map(is_array, args)), "Z3 array expected expected")
_z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
_z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
_args, sz = _to_ast_array(args)
ctx = f.ctx
@ -4100,7 +4120,7 @@ class Datatype:
if __debug__:
_z3_assert(isinstance(name, str), "String expected")
_z3_assert(isinstance(rec_name, str), "String expected")
_z3_assert(all(map(_valid_accessor, args)), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)")
_z3_assert(all([_valid_accessor(a) for a in args]), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)")
self.constructors.append((name, rec_name, args))
def declare(self, name, *args):
@ -4187,9 +4207,9 @@ def CreateDatatypes(*ds):
ds = _get_args(ds)
if __debug__:
_z3_assert(len(ds) > 0, "At least one Datatype must be specified")
_z3_assert(all(map(lambda d: isinstance(d, Datatype), ds)), "Arguments must be Datatypes")
_z3_assert(all(map(lambda d: d.ctx == ds[0].ctx, ds)), "Context mismatch")
_z3_assert(all(map(lambda d: d.constructors != [], ds)), "Non-empty Datatypes expected")
_z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
_z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
_z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
ctx = ds[0].ctx
num = len(ds)
names = (Symbol * num)()
@ -4355,7 +4375,7 @@ def EnumSort(name, values, ctx=None):
"""
if __debug__:
_z3_assert(isinstance(name, str), "Name must be a string")
_z3_assert(all(map(lambda v: isinstance(v, str), values)), "Eumeration sort values must be strings")
_z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
_z3_assert(len(values) > 0, "At least one value expected")
ctx = _get_ctx(ctx)
num = len(values)
@ -4369,7 +4389,7 @@ def EnumSort(name, values, ctx=None):
V = []
for i in range(num):
V.append(FuncDeclRef(_values[i], ctx))
V = map(lambda a: a(), V)
V = [a() for a in V]
return S, V
#########################################
@ -4432,7 +4452,8 @@ def args2params(arguments, keywords, ctx=None):
else:
r.set(prev, a)
prev = None
for k, v in keywords.iteritems():
for k in keywords:
v = keywords[k]
r.set(k, v)
return r
@ -4469,7 +4490,7 @@ class ParamDescrsRef:
return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
def __getitem__(self, arg):
if isinstance(arg, int) or isinstance(arg, long):
if _is_int(arg):
return self.get_name(arg)
else:
return self.get_kind(arg)
@ -5057,7 +5078,7 @@ class FuncEntry:
>>> try:
... e.arg_value(2)
... except IndexError:
... print "index error"
... print("index error")
index error
"""
if idx >= self.num_args():
@ -5122,7 +5143,10 @@ class FuncInterp(Z3PPObject):
Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
def else_value(self):
"""Return the `else` value for a function interpretation.
"""
Return the `else` value for a function interpretation.
Return None if Z3 did not specify the `else` value for
this object.
>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
@ -5135,7 +5159,11 @@ class FuncInterp(Z3PPObject):
>>> m[f].else_value()
1
"""
return _to_expr_ref(Z3_func_interp_get_else(self.ctx.ref(), self.f), self.ctx)
r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
if r:
return _to_expr_ref(r, self.ctx)
else:
return None
def num_entries(self):
"""Return the number of entries/points in the function interpretation `self`.
@ -5428,7 +5456,7 @@ class ModelRef(Z3PPObject):
1
>>> m[f]
[1 -> 0, else -> 0]
>>> for d in m: print "%s -> %s" % (d, m[d])
>>> for d in m: print("%s -> %s" % (d, m[d]))
x -> 1
f -> [1 -> 0, else -> 0]
"""
@ -5499,16 +5527,16 @@ class Statistics:
if in_html_mode():
out = io.StringIO()
even = True
out.write(u'<table border="1" cellpadding="2" cellspacing="0">')
out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
for k, v in self:
if even:
out.write(u'<tr style="background-color:#CFCFCF">')
out.write(u('<tr style="background-color:#CFCFCF">'))
even = False
else:
out.write(u'<tr>')
out.write(u('<tr>'))
even = True
out.write(u'<td>%s</td><td>%s</td></tr>' % (k, v))
out.write(u'</table>')
out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
out.write(u('</table>'))
return out.getvalue()
else:
return Z3_stats_to_string(self.ctx.ref(), self.stats)
@ -5806,7 +5834,7 @@ class Solver(Z3PPObject):
>>> s.assert_and_track(x > 0, 'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0, p3)
>>> print s.check()
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
@ -5954,7 +5982,7 @@ class Solver(Z3PPObject):
def help(self):
"""Display a string describing all available options."""
print Z3_solver_get_help(self.ctx.ref(), self.solver)
print(Z3_solver_get_help(self.ctx.ref(), self.solver))
def param_descrs(self):
"""Return the parameter description set."""
@ -6025,7 +6053,7 @@ class Fixedpoint(Z3PPObject):
else:
self.fixedpoint = fixedpoint
Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
self.vars = []
self.vars = []
def __del__(self):
if self.fixedpoint != None:
@ -6039,8 +6067,8 @@ class Fixedpoint(Z3PPObject):
def help(self):
"""Display a string describing all available options."""
print Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint)
print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
def param_descrs(self):
"""Return the parameter description set."""
return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
@ -6052,11 +6080,11 @@ class Fixedpoint(Z3PPObject):
for arg in args:
if isinstance(arg, Goal) or isinstance(arg, AstVector):
for f in arg:
f = self.abstract(f)
f = self.abstract(f)
Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
else:
arg = s.cast(arg)
arg = self.abstract(arg)
arg = self.abstract(arg)
Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
def add(self, *args):
@ -6072,38 +6100,38 @@ class Fixedpoint(Z3PPObject):
self.assert_exprs(*args)
def add_rule(self, head, body = None, name = None):
"""Assert rules defining recursive predicates to the fixedpoint solver.
"""Assert rules defining recursive predicates to the fixedpoint solver.
>>> a = Bool('a')
>>> b = Bool('b')
>>> b = Bool('b')
>>> s = Fixedpoint()
>>> s.register_relation(a.decl())
>>> s.register_relation(b.decl())
>>> s.fact(a)
>>> s.register_relation(a.decl())
>>> s.register_relation(b.decl())
>>> s.fact(a)
>>> s.rule(b, a)
>>> s.query(b)
sat
"""
if name == None:
name = ""
>>> s.query(b)
sat
"""
if name == None:
name = ""
name = to_symbol(name, self.ctx)
if body == None:
head = self.abstract(head)
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
else:
body = _get_args(body)
f = self.abstract(Implies(And(body),head))
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
if body == None:
head = self.abstract(head)
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
else:
body = _get_args(body)
f = self.abstract(Implies(And(body),head))
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def rule(self, head, body = None, name = None):
"""Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
self.add_rule(head, body, name)
"""Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
self.add_rule(head, body, name)
def fact(self, head, name = None):
"""Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
self.add_rule(head, None, name)
"""Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
self.add_rule(head, None, name)
def query(self, *query):
"""Query the fixedpoint engine whether formula is derivable.
"""Query the fixedpoint engine whether formula is derivable.
You can also pass an tuple or list of recursive predicates.
"""
query = _get_args(query)
@ -6134,17 +6162,17 @@ class Fixedpoint(Z3PPObject):
def update_rule(self, head, body, name):
"""update rule"""
if name == None:
name = ""
if name == None:
name = ""
name = to_symbol(name, self.ctx)
body = _get_args(body)
f = self.abstract(Implies(And(body),head))
Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def get_answer(self):
"""Retrieve answer from last query call."""
r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
return _to_expr_ref(r, self.ctx)
def get_answer(self):
"""Retrieve answer from last query call."""
r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
return _to_expr_ref(r, self.ctx)
def get_num_levels(self, predicate):
"""Retrieve number of levels used for predicate in PDR engine"""
@ -6160,40 +6188,40 @@ class Fixedpoint(Z3PPObject):
Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
def register_relation(self, *relations):
"""Register relation as recursive"""
relations = _get_args(relations)
for f in relations:
Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
"""Register relation as recursive"""
relations = _get_args(relations)
for f in relations:
Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
def set_predicate_representation(self, f, *representations):
"""Control how relation is represented"""
representations = _get_args(representations)
representations = map(to_symbol, representations)
sz = len(representations)
args = (Symbol * sz)()
for i in range(sz):
args[i] = representations[i]
Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
"""Control how relation is represented"""
representations = _get_args(representations)
representations = [to_symbol(s) for s in representations]
sz = len(representations)
args = (Symbol * sz)()
for i in range(sz):
args[i] = representations[i]
Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
def parse_string(self, s):
"""Parse rules and queries from a string"""
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
"""Parse rules and queries from a string"""
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
def parse_file(self, f):
"""Parse rules and queries from a file"""
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
"""Parse rules and queries from a file"""
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
def get_rules(self):
"""retrieve rules that have been added to fixedpoint context"""
return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
"""retrieve rules that have been added to fixedpoint context"""
return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
def get_assertions(self):
"""retrieve assertions that have been added to fixedpoint context"""
return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
"""retrieve assertions that have been added to fixedpoint context"""
return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
def __repr__(self):
"""Return a formatted string with all added rules and constraints."""
return self.sexpr()
return self.sexpr()
def sexpr(self):
"""Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
@ -6201,16 +6229,16 @@ class Fixedpoint(Z3PPObject):
return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
def to_string(self, queries):
"""Return a formatted string (in Lisp-like format) with all added constraints.
"""Return a formatted string (in Lisp-like format) with all added constraints.
We say the string is in s-expression format.
Include also queries.
Include also queries.
"""
args, len = _to_ast_array(queries)
args, len = _to_ast_array(queries)
return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
def statistics(self):
"""Return statistics for the last `query()`.
"""
"""
return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
def reason_unknown(self):
@ -6219,21 +6247,21 @@ class Fixedpoint(Z3PPObject):
return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
def declare_var(self, *vars):
"""Add variable or several variables.
The added variable or variables will be bound in the rules
and queries
"""
vars = _get_args(vars)
for v in vars:
self.vars += [v]
"""Add variable or several variables.
The added variable or variables will be bound in the rules
and queries
"""
vars = _get_args(vars)
for v in vars:
self.vars += [v]
def abstract(self, fml, is_forall=True):
if self.vars == []:
return fml
if is_forall:
return ForAll(self.vars, fml)
else:
return Exists(self.vars, fml)
if self.vars == []:
return fml
if is_forall:
return ForAll(self.vars, fml)
else:
return Exists(self.vars, fml)
#########################################
#
@ -6425,7 +6453,7 @@ class Tactic:
def help(self):
"""Display a string containing a description of the available options for the `self` tactic."""
print Z3_tactic_get_help(self.ctx.ref(), self.tactic)
print(Z3_tactic_get_help(self.ctx.ref(), self.tactic))
def param_descrs(self):
"""Return the parameter description set."""
@ -6521,7 +6549,7 @@ def ParOr(*ts, **ks):
if __debug__:
_z3_assert(len(ts) >= 2, "At least two arguments expected")
ctx = _get_ctx(ks.get('ctx', None))
ts = map(lambda t: _to_tactic(t, ctx), ts)
ts = [ _to_tactic(t, ctx) for t in ts ]
sz = len(ts)
_args = (TacticObj * sz)()
for i in range(sz):
@ -6566,7 +6594,7 @@ def Repeat(t, max=4294967295, ctx=None):
>>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
>>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
>>> r = t(c)
>>> for subgoal in r: print subgoal
>>> for subgoal in r: print(subgoal)
[x == 0, y == 0, x > y]
[x == 0, y == 1, x > y]
[x == 1, y == 0, x > y]
@ -6608,19 +6636,19 @@ def describe_tactics():
"""Display a (tabular) description of all available tactics in Z3."""
if in_html_mode():
even = True
print '<table border="1" cellpadding="2" cellspacing="0">'
print('<table border="1" cellpadding="2" cellspacing="0">')
for t in tactics():
if even:
print '<tr style="background-color:#CFCFCF">'
print('<tr style="background-color:#CFCFCF">')
even = False
else:
print '<tr>'
print('<tr>')
even = True
print '<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40))
print '</table>'
print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
print('</table>')
else:
for t in tactics():
print '%s : %s' % (t, tactic_description(t))
print('%s : %s' % (t, tactic_description(t)))
class Probe:
"""Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used."""
@ -6631,7 +6659,7 @@ class Probe:
self.probe = probe
elif isinstance(probe, float):
self.probe = Z3_probe_const(self.ctx.ref(), probe)
elif isinstance(probe, int) or isinstance(probe, long):
elif _is_int(probe):
self.probe = Z3_probe_const(self.ctx.ref(), float(probe))
elif isinstance(probe, bool):
if probe:
@ -6796,19 +6824,19 @@ def describe_probes():
"""Display a (tabular) description of all available probes in Z3."""
if in_html_mode():
even = True
print '<table border="1" cellpadding="2" cellspacing="0">'
print('<table border="1" cellpadding="2" cellspacing="0">')
for p in probes():
if even:
print '<tr style="background-color:#CFCFCF">'
print('<tr style="background-color:#CFCFCF">')
even = False
else:
print '<tr>'
print('<tr>')
even = True
print '<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40))
print '</table>'
print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
print('</table>')
else:
for p in probes():
print '%s : %s' % (p, probe_description(p))
print('%s : %s' % (p, probe_description(p)))
def _probe_nary(f, args, ctx):
if __debug__:
@ -6904,7 +6932,7 @@ def simplify(a, *arguments, **keywords):
def help_simplify():
"""Return a string describing all options available for Z3 `simplify` procedure."""
print Z3_simplify_get_help(main_ctx().ref())
print(Z3_simplify_get_help(main_ctx().ref()))
def simplify_param_descrs():
"""Return the set of parameter descriptions for Z3 `simplify` procedure."""
@ -6927,7 +6955,7 @@ def substitute(t, *m):
m = _get_args(m1)
if __debug__:
_z3_assert(is_expr(t), "Z3 expression expected")
_z3_assert(all(map(lambda p: isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()), m)), "Z3 invalid substitution, expression pairs expected.")
_z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
num = len(m)
_from = (Ast * num)()
_to = (Ast * num)()
@ -6949,7 +6977,7 @@ def substitute_vars(t, *m):
"""
if __debug__:
_z3_assert(is_expr(t), "Z3 expression expected")
_z3_assert(all(map(is_expr, m)), "Z3 invalid substitution, list of expressions expected.")
_z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
num = len(m)
_to = (Ast * num)()
for i in range(num):
@ -6976,7 +7004,7 @@ def Sum(*args):
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
args = _coerce_expr_list(args, ctx)
if is_bv(args[0]):
return reduce(lambda a, b: a + b, args, 0)
return _reduce(lambda a, b: a + b, args, 0)
else:
_args, sz = _to_ast_array(args)
return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)
@ -7001,7 +7029,7 @@ def Product(*args):
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
args = _coerce_expr_list(args, ctx)
if is_bv(args[0]):
return reduce(lambda a, b: a * b, args, 1)
return _reduce(lambda a, b: a * b, args, 1)
else:
_args, sz = _to_ast_array(args)
return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
@ -7021,18 +7049,18 @@ def solve(*args, **keywords):
s.set(**keywords)
s.add(*args)
if keywords.get('show', False):
print s
print(s)
r = s.check()
if r == unsat:
print "no solution"
print("no solution")
elif r == unknown:
print "failed to solve"
print("failed to solve")
try:
print s.model()
print(s.model())
except Z3Exception:
return
else:
print s.model()
print(s.model())
def solve_using(s, *args, **keywords):
"""Solve the constraints `*args` using solver `s`.
@ -7047,21 +7075,21 @@ def solve_using(s, *args, **keywords):
s.set(**keywords)
s.add(*args)
if keywords.get('show', False):
print "Problem:"
print s
print("Problem:")
print(s)
r = s.check()
if r == unsat:
print "no solution"
print("no solution")
elif r == unknown:
print "failed to solve"
print("failed to solve")
try:
print s.model()
print(s.model())
except Z3Exception:
return
else:
if keywords.get('show', False):
print "Solution:"
print s.model()
print("Solution:")
print(s.model())
def prove(claim, **keywords):
"""Try to prove the given claim.
@ -7079,16 +7107,16 @@ def prove(claim, **keywords):
s.set(**keywords)
s.add(Not(claim))
if keywords.get('show', False):
print s
print(s)
r = s.check()
if r == unsat:
print "proved"
print("proved")
elif r == unknown:
print "failed to prove"
print s.model()
print("failed to prove")
print(s.model())
else:
print "counterexample"
print s.model()
print("counterexample")
print(s.model())
def _solve_html(*args, **keywords):
"""Version of funcion `solve` used in RiSE4Fun."""
@ -7096,21 +7124,21 @@ def _solve_html(*args, **keywords):
s.set(**keywords)
s.add(*args)
if keywords.get('show', False):
print "<b>Problem:</b>"
print s
print("<b>Problem:</b>")
print(s)
r = s.check()
if r == unsat:
print "<b>no solution</b>"
print("<b>no solution</b>")
elif r == unknown:
print "<b>failed to solve</b>"
print("<b>failed to solve</b>")
try:
print s.model()
print(s.model())
except Z3Exception:
return
else:
if keywords.get('show', False):
print "<b>Solution:</b>"
print s.model()
print("<b>Solution:</b>")
print(s.model())
def _solve_using_html(s, *args, **keywords):
"""Version of funcion `solve_using` used in RiSE4Fun."""
@ -7119,21 +7147,21 @@ def _solve_using_html(s, *args, **keywords):
s.set(**keywords)
s.add(*args)
if keywords.get('show', False):
print "<b>Problem:</b>"
print s
print("<b>Problem:</b>")
print(s)
r = s.check()
if r == unsat:
print "<b>no solution</b>"
print("<b>no solution</b>")
elif r == unknown:
print "<b>failed to solve</b>"
print("<b>failed to solve</b>")
try:
print s.model()
print(s.model())
except Z3Exception:
return
else:
if keywords.get('show', False):
print "<b>Solution:</b>"
print s.model()
print("<b>Solution:</b>")
print(s.model())
def _prove_html(claim, **keywords):
"""Version of funcion `prove` used in RiSE4Fun."""
@ -7143,23 +7171,24 @@ def _prove_html(claim, **keywords):
s.set(**keywords)
s.add(Not(claim))
if keywords.get('show', False):
print s
print(s)
r = s.check()
if r == unsat:
print "<b>proved</b>"
print("<b>proved</b>")
elif r == unknown:
print "<b>failed to prove</b>"
print s.model()
print("<b>failed to prove</b>")
print(s.model())
else:
print "<b>counterexample</b>"
print s.model()
print("<b>counterexample</b>")
print(s.model())
def _dict2sarray(sorts, ctx):
sz = len(sorts)
_names = (Symbol * sz)()
_sorts = (Sort * sz) ()
i = 0
for k, v in sorts.iteritems():
for k in sorts:
v = sorts[k]
if __debug__:
_z3_assert(isinstance(k, str), "String expected")
_z3_assert(is_sort(v), "Z3 sort expected")
@ -7173,7 +7202,8 @@ def _dict2darray(decls, ctx):
_names = (Symbol * sz)()
_decls = (FuncDecl * sz) ()
i = 0
for k, v in decls.iteritems():
for k in decls:
v = decls[k]
if __debug__:
_z3_assert(isinstance(k, str), "String expected")
_z3_assert(is_func_decl(v) or is_const(v), "Z3 declaration or constant expected")

65
src/api/python/z3printer.py
View file

@ -74,6 +74,15 @@ def _is_add(k):
def _is_sub(k):
return k == Z3_OP_SUB or k == Z3_OP_BSUB
import sys
if sys.version < '3':
import codecs
def u(x):
return codecs.unicode_escape_decode(x)[0]
else:
def u(x):
return x
_z3_infix_compact = [ Z3_OP_MUL, Z3_OP_BMUL, Z3_OP_POWER, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_BSDIV, Z3_OP_BSMOD ]
_ellipses = '...'
@ -161,15 +170,19 @@ def _get_precedence(k):
return _z3_precedence.get(k, 100000)
_z3_html_op_to_str = {}
for _k, _v in _z3_op_to_str.iteritems():
for _k in _z3_op_to_str:
_v = _z3_op_to_str[_k]
_z3_html_op_to_str[_k] = _v
for _k, _v in _z3_pre_html_op_to_str.iteritems():
for _k in _z3_pre_html_op_to_str:
_v = _z3_pre_html_op_to_str[_k]
_z3_html_op_to_str[_k] = _v
_z3_html_precedence = {}
for _k, _v in _z3_precedence.iteritems():
for _k in _z3_precedence:
_v = _z3_precedence[_k]
_z3_html_precedence[_k] = _v
for _k, _v in _z3_pre_html_precedence.iteritems():
for _k in _z3_pre_html_precedence:
_v = _z3_pre_html_precedence[_k]
_z3_html_precedence[_k] = _v
_html_infix_map = {}
@ -237,7 +250,7 @@ class FormatObject:
class NAryFormatObject(FormatObject):
def __init__(self, fs):
assert all(map(lambda a: isinstance(a, FormatObject), fs))
assert all([isinstance(a, FormatObject) for a in fs])
self.children = fs
def children(self):
return self.children
@ -246,7 +259,7 @@ class ComposeFormatObject(NAryFormatObject):
def is_compose(sef):
return True
def as_tuple(self):
return ('compose', map(lambda a: a.as_tuple(), self.children))
return ('compose', [ a.as_tuple() for a in self.children ])
def space_upto_nl(self):
r = 0
for child in self.children:
@ -256,13 +269,13 @@ class ComposeFormatObject(NAryFormatObject):
return (r, True)
return (r, False)
def flat(self):
return compose(map(lambda a: a.flat(), self.children))
return compose([a.flat() for a in self.children ])
class ChoiceFormatObject(NAryFormatObject):
def is_choice(sef):
return True
def as_tuple(self):
return ('choice', map(lambda a: a.as_tuple(), self.children))
return ('choice', [ a.as_tuple() for a in self.children ])
def space_upto_nl(self):
return self.children[0].space_upto_nl()
def flat(self):
@ -388,11 +401,11 @@ class PP:
if not self.bounded or self.pos <= self.max_width:
sz = _len(f)
if self.bounded and self.pos + sz > self.max_width:
self.out.write(_ellipses)
self.out.write(u(_ellipses))
else:
self.pos = self.pos + sz
self.ribbon_pos = self.ribbon_pos + sz
self.out.write(unicode(f.string))
self.out.write(u(f.string))
def pp_compose(self, f, indent):
for c in f.children:
@ -410,11 +423,11 @@ class PP:
self.ribbon_pos = 0
self.line = self.line + 1
if self.line < self.max_lines:
self.out.write(unicode('\n'))
self.out.write(u('\n'))
for i in range(indent):
self.out.write(unicode(' '))
self.out.write(u(' '))
else:
self.out.write(unicode('\n...'))
self.out.write(u('\n...'))
raise StopPPException()
def pp(self, f, indent):
@ -791,7 +804,11 @@ class Formatter:
r.append(self.pp_ellipses())
break
if sz <= self.max_args:
else_pp = self.pp_expr(f.else_value(), 0, [])
else_val = f.else_value()
if else_val == None:
else_pp = to_format('#unspecified')
else:
else_pp = self.pp_expr(else_val, 0, [])
r.append(group(seq((to_format('else'), else_pp), self.pp_arrow())))
return seq3(r, '[', ']')
@ -953,23 +970,23 @@ def in_html_mode():
def pp(a):
if _support_pp(a):
print obj_to_string(a)
print(obj_to_string(a))
else:
print a
print(a)
def print_matrix(m):
z3._z3_assert(isinstance(m, list) or isinstance(m, tuple), "matrix expected")
if not in_html_mode():
print obj_to_string(m)
print(obj_to_string(m))
else:
print '<table cellpadding="2", cellspacing="0", border="1">'
print('<table cellpadding="2", cellspacing="0", border="1">')
for r in m:
z3._z3_assert(isinstance(r, list) or isinstance(r, tuple), "matrix expected")
print '<tr>'
print('<tr>')
for c in r:
print '<td>%s</td>' % c
print '</tr>'
print '</table>'
print('<td>%s</td>' % c)
print('</tr>')
print('</table>')
def insert_line_breaks(s, width):
"""Break s in lines of size width (approx)"""
@ -980,9 +997,9 @@ def insert_line_breaks(s, width):
w = 0
for i in range(sz):
if w > width and s[i] == ' ':
new_str.write(u'<br />')
new_str.write(u('<br />'))
w = 0
else:
new_str.write(unicode(s[i]))
new_str.write(u(s[i]))
w = w + 1
return new_str.getvalue()

18
src/api/z3_api.h
View file

@ -1080,6 +1080,7 @@ typedef enum {
Z3_PK_INVALID
} Z3_param_kind;
#ifdef CorML3
/**
\mlonly {!search_failure} \endmlonly \conly \brief
The different kinds of search failure types.
@ -1103,6 +1104,7 @@ typedef enum {
Z3_THEORY,
Z3_QUANTIFIERS
} Z3_search_failure;
#endif
/**
\mlonly {!ast_print_mode} \endmlonly \conly \brief
@ -6922,12 +6924,15 @@ END_MLAPI_EXCLUDE
);
/*@}*/
#endif
/**
@name Deprecated Constraints API
*/
/*@{*/
#ifdef CorML3
/**
\brief Set the SMTLIB logic to be used in the given logical context.
It is incorrect to invoke this function after invoking
@ -7109,7 +7114,9 @@ END_MLAPI_EXCLUDE
__out Z3_model * m, __out Z3_ast* proof,
__inout unsigned* core_size, __inout_ecount(num_assumptions) Z3_ast core[]
);
#endif
#ifdef CorML4
/**
\brief Retrieve congruence class representatives for terms.
@ -7123,23 +7130,26 @@ END_MLAPI_EXCLUDE
This means that two terms map to the same class identifier if and only if
the current context implies that they are equal.
A side-effect of the function is a satisfiability check.
A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in.
The function return Z3_L_FALSE if the current assertions are not satisfiable.
\sa Z3_check_and_get_model
\sa Z3_check
\deprecated Subsumed by Z3_solver API
\deprecated To be moved outside of API.
def_API('Z3_get_implied_equalities', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _out_array(1, UINT)))
def_API('Z3_get_implied_equalities', UINT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
*/
Z3_lbool Z3_API Z3_get_implied_equalities(
__in Z3_context c,
__in Z3_solver s,
__in unsigned num_terms,
__in_ecount(num_terms) Z3_ast const terms[],
__out_ecount(num_terms) unsigned class_ids[]
);
#endif
#ifdef CorML3
/**
\brief Delete a model object.

32
src/api/z3_private.h
View file

@ -36,38 +36,6 @@ extern "C" {
Z3_bool Z3_API Z3_get_numeral_rational(__in Z3_context c, __in Z3_ast a, rational& r);
/**
\brief \mlh exec_smtlib2_string c str \endmlh
Parse the given string using the SMT-LIB2 parser and execute its commands.
It returns a formula comprising of the conjunction of assertions in the scope
(up to push/pop) at the end of the string.
The returned formula is also asserted to the logical context on return.
*/
Z3_ast Z3_API Z3_exec_smtlib2_string(__in Z3_context c,
__in Z3_string str,
__in unsigned num_sorts,
__in_ecount(num_sorts) Z3_symbol sort_names[],
__in_ecount(num_sorts) Z3_sort sorts[],
__in unsigned num_decls,
__in_ecount(num_decls) Z3_symbol decl_names[],
__in_ecount(num_decls) Z3_func_decl decls[]
);
/**
\brief Similar to #Z3_exec_smtlib2_string, but reads the commands from a file.
*/
Z3_ast Z3_API Z3_exec_smtlib2_file(__in Z3_context c,
__in Z3_string file_name,
__in unsigned num_sorts,
__in_ecount(num_sorts) Z3_symbol sort_names[],
__in_ecount(num_sorts) Z3_sort sorts[],
__in unsigned num_decls,
__in_ecount(num_decls) Z3_symbol decl_names[],
__in_ecount(num_decls) Z3_func_decl decls[]
);
#ifndef CAMLIDL
#ifdef __cplusplus
};

24
src/ast/arith_decl_plugin.cpp
View file

@ -573,18 +573,7 @@ expr * arith_decl_plugin::get_some_value(sort * s) {
return mk_numeral(rational(0), s == m_int_decl);
}
arith_util::arith_util(ast_manager & m):
m_manager(m),
m_afid(m.get_family_id("arith")),
m_plugin(0) {
}
void arith_util::init_plugin() {
SASSERT(m_plugin == 0);
m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
}
bool arith_util::is_numeral(expr const * n, rational & val, bool & is_int) const {
bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int) const {
if (!is_app_of(n, m_afid, OP_NUM))
return false;
func_decl * decl = to_app(n)->get_decl();
@ -593,6 +582,17 @@ bool arith_util::is_numeral(expr const * n, rational & val, bool & is_int) const
return true;
}
arith_util::arith_util(ast_manager & m):
arith_recognizers(m.mk_family_id("arith")),
m_manager(m),
m_plugin(0) {
}
void arith_util::init_plugin() {
SASSERT(m_plugin == 0);
m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
}
bool arith_util::is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val) {
if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM))
return false;

69
src/ast/arith_decl_plugin.h
View file

@ -187,36 +187,24 @@ public:
virtual void set_cancel(bool f);
};
class arith_util {
ast_manager & m_manager;
/**
\brief Procedures for recognizing arithmetic expressions.
We don't need access to ast_manager, and operations can be simultaneously
executed in different threads.
*/
class arith_recognizers {
protected:
family_id m_afid;
arith_decl_plugin * m_plugin;
void init_plugin();
arith_decl_plugin & plugin() const {
if (!m_plugin) const_cast<arith_util*>(this)->init_plugin();
SASSERT(m_plugin != 0);
return *m_plugin;
}
public:
arith_util(ast_manager & m);
arith_recognizers(family_id id):m_afid(id) {}
ast_manager & get_manager() const { return m_manager; }
family_id get_family_id() const { return m_afid; }
algebraic_numbers::manager & am() {
return plugin().am();
}
bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; }
bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
bool is_numeral(expr const * n, rational & val, bool & is_int) const;
bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); }
bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); }
bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
bool is_zero(expr const * n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
bool is_minus_one(expr * n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
// return true if \c n is a term of the form (* -1 r)
@ -227,6 +215,7 @@ public:
}
return false;
}
bool is_le(expr const * n) const { return is_app_of(n, m_afid, OP_LE); }
bool is_ge(expr const * n) const { return is_app_of(n, m_afid, OP_GE); }
bool is_lt(expr const * n) const { return is_app_of(n, m_afid, OP_LT); }
@ -245,14 +234,13 @@ public:
bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); }
bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
bool is_int(expr const * n) const { return is_int(m_manager.get_sort(n)); }
bool is_int(expr const * n) const { return is_int(get_sort(n)); }
bool is_real(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); }
bool is_real(expr const * n) const { return is_real(m_manager.get_sort(n)); }
bool is_real(expr const * n) const { return is_real(get_sort(n)); }
bool is_int_real(sort const * s) const { return s->get_family_id() == m_afid; }
bool is_int_real(expr const * n) const { return is_int_real(m_manager.get_sort(n)); }
bool is_int_real(expr const * n) const { return is_int_real(get_sort(n)); }
MATCH_UNARY(is_uminus);
MATCH_BINARY(is_sub);
MATCH_BINARY(is_add);
MATCH_BINARY(is_mul);
@ -265,6 +253,34 @@ public:
MATCH_BINARY(is_div);
MATCH_BINARY(is_idiv);
bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
};
class arith_util : public arith_recognizers {
ast_manager & m_manager;
arith_decl_plugin * m_plugin;
void init_plugin();
arith_decl_plugin & plugin() const {
if (!m_plugin) const_cast<arith_util*>(this)->init_plugin();
SASSERT(m_plugin != 0);
return *m_plugin;
}
public:
arith_util(ast_manager & m);
ast_manager & get_manager() const { return m_manager; }
algebraic_numbers::manager & am() {
return plugin().am();
}
bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); }
sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); }
@ -320,9 +336,6 @@ public:
app * mk_acosh(expr * arg) { return m_manager.mk_app(m_afid, OP_ACOSH, arg); }
app * mk_atanh(expr * arg) { return m_manager.mk_app(m_afid, OP_ATANH, arg); }
bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
app * mk_pi() { return plugin().mk_pi(); }
app * mk_e() { return plugin().mk_e(); }

10
src/ast/array_decl_plugin.cpp
View file

@ -542,6 +542,16 @@ bool array_decl_plugin::is_fully_interp(sort const * s) const {
return m_manager->is_fully_interp(get_array_range(s));
}
func_decl * array_recognizers::get_as_array_func_decl(app * n) const {
SASSERT(is_as_array(n));
return to_func_decl(n->get_decl()->get_parameter(0).get_ast());
}
array_util::array_util(ast_manager& m):
array_recognizers(m.mk_family_id("array")),
m_manager(m) {
}
bool array_util::is_as_array_tree(expr * n) {
ptr_buffer<expr, 32> todo;
todo.push_back(n);

23
src/ast/array_decl_plugin.h
View file

@ -129,27 +129,34 @@ class array_decl_plugin : public decl_plugin {
virtual bool is_fully_interp(sort const * s) const;
};
class array_util {
ast_manager & m_manager;
family_id m_fid;
class array_recognizers {
protected:
family_id m_fid;
public:
array_util(ast_manager& m): m_manager(m), m_fid(m.get_family_id("array")) {}
ast_manager & get_manager() const { return m_manager; }
array_recognizers(family_id fid):m_fid(fid) {}
family_id get_family_id() const { return m_fid; }
bool is_array(sort* s) const { return is_sort_of(s, m_fid, ARRAY_SORT);}
bool is_array(expr* n) const { return is_array(m_manager.get_sort(n)); }
bool is_array(expr* n) const { return is_array(get_sort(n)); }
bool is_select(expr* n) const { return is_app_of(n, m_fid, OP_SELECT); }
bool is_store(expr* n) const { return is_app_of(n, m_fid, OP_STORE); }
bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
bool is_as_array_tree(expr * n);
bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
func_decl * get_as_array_func_decl(app * n) const { SASSERT(is_as_array(n)); return to_func_decl(n->get_decl()->get_parameter(0).get_ast()); }
func_decl * get_as_array_func_decl(app * n) const;
};
class array_util : public array_recognizers {
ast_manager & m_manager;
public:
array_util(ast_manager& m);
ast_manager & get_manager() const { return m_manager; }
bool is_as_array_tree(expr * n);
app * mk_store(unsigned num_args, expr * const * args) {
return m_manager.mk_app(m_fid, OP_STORE, 0, 0, num_args, args);

77
src/ast/ast.cpp
View file

@ -137,7 +137,7 @@ void display_parameters(std::ostream & out, unsigned n, parameter const * p) {
//
// -----------------------------------
family_id family_manager::get_family_id(symbol const & s) {
family_id family_manager::mk_family_id(symbol const & s) {
family_id r;
if (m_families.find(s, r)) {
return r;
@ -149,7 +149,15 @@ family_id family_manager::get_family_id(symbol const & s) {
return r;
}
bool family_manager::has_family(symbol const & s) {
family_id family_manager::get_family_id(symbol const & s) const {
family_id r;
if (m_families.find(s, r))
return r;
else
return null_family_id;
}
bool family_manager::has_family(symbol const & s) const {
return m_families.contains(s);
}
@ -374,6 +382,31 @@ quantifier::quantifier(bool forall, unsigned num_decls, sort * const * decl_sort
memcpy(const_cast<expr **>(get_no_patterns()), no_patterns, sizeof(expr *) * num_no_patterns);
}
// -----------------------------------
//
// Auxiliary functions
//
// -----------------------------------
sort * get_sort(expr const * n) {
while (true) {
switch(n->get_kind()) {
case AST_APP:
return to_app(n)->get_decl()->get_range();
case AST_VAR:
return to_var(n)->get_sort();
case AST_QUANTIFIER:
// The sort of the quantifier is the sort of the nested expression.
// This code assumes the given expression is well-sorted.
n = to_quantifier(n)->get_expr();
break;
default:
UNREACHABLE();
return 0;
}
}
}
// -----------------------------------
//
// AST hash-consing
@ -1048,6 +1081,16 @@ expr * basic_decl_plugin::get_some_value(sort * s) {
return 0;
}
bool basic_recognizers::is_ite(expr const * n, expr * & t1, expr * & t2, expr * & t3) const {
if (is_ite(n)) {
t1 = to_app(n)->get_arg(0);
t2 = to_app(n)->get_arg(1);
t3 = to_app(n)->get_arg(2);
return true;
}
return false;
}
// -----------------------------------
//
// label_decl_plugin
@ -1262,12 +1305,12 @@ void ast_manager::init() {
m_expr_id_gen.reset(0);
m_decl_id_gen.reset(c_first_decl_id);
m_some_value_proc = 0;
m_basic_family_id = get_family_id("basic");
m_label_family_id = get_family_id("label");
m_pattern_family_id = get_family_id("pattern");
m_model_value_family_id = get_family_id("model-value");
m_user_sort_family_id = get_family_id("user-sort");
m_arith_family_id = get_family_id("arith");
m_basic_family_id = mk_family_id("basic");
m_label_family_id = mk_family_id("label");
m_pattern_family_id = mk_family_id("pattern");
m_model_value_family_id = mk_family_id("model-value");
m_user_sort_family_id = mk_family_id("user-sort");
m_arith_family_id = mk_family_id("arith");
basic_decl_plugin * plugin = alloc(basic_decl_plugin);
register_plugin(m_basic_family_id, plugin);
m_bool_sort = plugin->mk_bool_sort();
@ -1400,7 +1443,7 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
<< ", target has_family: " << m_family_manager.has_family(fid) << "\n";
if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
if (!m_family_manager.has_family(fid)) {
family_id new_fid = get_family_id(fid_name);
family_id new_fid = mk_family_id(fid_name);
TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
}
TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
@ -1437,7 +1480,7 @@ void ast_manager::set_next_expr_id(unsigned id) {
unsigned ast_manager::get_node_size(ast const * n) { return ::get_node_size(n); }
void ast_manager::register_plugin(symbol const & s, decl_plugin * plugin) {
family_id id = m_family_manager.get_family_id(s);
family_id id = m_family_manager.mk_family_id(s);
SASSERT(is_format_manager() || s != symbol("format"));
register_plugin(id, plugin);
}
@ -1495,20 +1538,6 @@ void ast_manager::register_plugin(family_id id, decl_plugin * plugin) {
plugin->set_manager(this, id);
}
sort * ast_manager::get_sort(expr const * n) const {
switch(n->get_kind()) {
case AST_APP:
return to_app(n)->get_decl()->get_range();
case AST_VAR:
return to_var(n)->get_sort();
case AST_QUANTIFIER:
return m_bool_sort;
default:
UNREACHABLE();
return 0;
}
}
bool ast_manager::is_bool(expr const * n) const {
return get_sort(n) == m_bool_sort;
}

77
src/ast/ast.h
View file

@ -188,10 +188,20 @@ class family_manager {
svector<symbol> m_names;
public:
family_manager():m_next_id(0) {}
/**
\brief Return the family_id for s, a new id is created if !has_family(s)
If has_family(s), then this method is equivalent to get_family_id(s)
*/
family_id mk_family_id(symbol const & s);
/**
\brief Return the family_id for s, return null_family_id if s was not registered in the manager.
*/
family_id get_family_id(symbol const & s) const;
family_id get_family_id(symbol const & s);
bool has_family(symbol const & s);
bool has_family(symbol const & s) const;
void get_dom(svector<symbol>& dom) const { m_families.get_dom(dom); }
@ -1287,6 +1297,55 @@ inline bool has_labels(expr const * n) {
else return false;
}
sort * get_sort(expr const * n);
class basic_recognizers {
family_id m_fid;
public:
basic_recognizers(family_id fid):m_fid(fid) {}
bool is_bool(sort const * s) const { return is_sort_of(s, m_fid, BOOL_SORT); }
bool is_bool(expr const * n) const { return is_bool(get_sort(n)); }
bool is_or(expr const * n) const { return is_app_of(n, m_fid, OP_OR); }
bool is_implies(expr const * n) const { return is_app_of(n, m_fid, OP_IMPLIES); }
bool is_and(expr const * n) const { return is_app_of(n, m_fid, OP_AND); }
bool is_not(expr const * n) const { return is_app_of(n, m_fid, OP_NOT); }
bool is_eq(expr const * n) const { return is_app_of(n, m_fid, OP_EQ); }
bool is_oeq(expr const * n) const { return is_app_of(n, m_fid, OP_OEQ); }
bool is_distinct(expr const * n) const { return is_app_of(n, m_fid, OP_DISTINCT); }
bool is_iff(expr const * n) const { return is_app_of(n, m_fid, OP_IFF); }
bool is_xor(expr const * n) const { return is_app_of(n, m_fid, OP_XOR); }
bool is_ite(expr const * n) const { return is_app_of(n, m_fid, OP_ITE); }
bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); }
bool is_true(expr const * n) const { return is_app_of(n, m_fid, OP_TRUE); }
bool is_false(expr const * n) const { return is_app_of(n, m_fid, OP_FALSE); }
bool is_complement_core(expr const * n1, expr const * n2) const {
return (is_true(n1) && is_false(n2)) || (is_not(n1) && to_app(n1)->get_arg(0) == n2);
}
bool is_complement(expr const * n1, expr const * n2) const { return is_complement_core(n1, n2) || is_complement_core(n2, n1); }
bool is_or(func_decl const * d) const { return is_decl_of(d, m_fid, OP_OR); }
bool is_implies(func_decl const * d) const { return is_decl_of(d, m_fid, OP_IMPLIES); }
bool is_and(func_decl const * d) const { return is_decl_of(d, m_fid, OP_AND); }
bool is_not(func_decl const * d) const { return is_decl_of(d, m_fid, OP_NOT); }
bool is_eq(func_decl const * d) const { return is_decl_of(d, m_fid, OP_EQ); }
bool is_iff(func_decl const * d) const { return is_decl_of(d, m_fid, OP_IFF); }
bool is_xor(func_decl const * d) const { return is_decl_of(d, m_fid, OP_XOR); }
bool is_ite(func_decl const * d) const { return is_decl_of(d, m_fid, OP_ITE); }
bool is_term_ite(func_decl const * d) const { return is_ite(d) && !is_bool(d->get_range()); }
bool is_distinct(func_decl const * d) const { return is_decl_of(d, m_fid, OP_DISTINCT); }
MATCH_UNARY(is_not);
MATCH_BINARY(is_eq);
MATCH_BINARY(is_iff);
MATCH_BINARY(is_implies);
MATCH_BINARY(is_and);
MATCH_BINARY(is_or);
MATCH_BINARY(is_xor);
MATCH_TERNARY(is_and);
MATCH_TERNARY(is_or);
bool is_ite(expr const * n, expr * & t1, expr * & t2, expr * & t3) const;
};
// -----------------------------------
//
// Get Some Value functor
@ -1404,6 +1463,8 @@ public:
// propagate cancellation signal to decl_plugins
void set_cancel(bool f);
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
bool has_trace_stream() const { return m_trace_stream != 0; }
std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }
@ -1432,8 +1493,10 @@ public:
small_object_allocator & get_allocator() { return m_alloc; }
family_id get_family_id(symbol const & s) const { return const_cast<ast_manager*>(this)->m_family_manager.get_family_id(s); }
family_id mk_family_id(symbol const & s) { return m_family_manager.mk_family_id(s); }
family_id mk_family_id(char const * s) { return mk_family_id(symbol(s)); }
family_id get_family_id(symbol const & s) const { return m_family_manager.get_family_id(s); }
family_id get_family_id(char const * s) const { return get_family_id(symbol(s)); }
symbol const & get_family_name(family_id fid) const { return m_family_manager.get_name(fid); }
@ -1456,7 +1519,7 @@ public:
bool has_plugin(family_id fid) const { return get_plugin(fid) != 0; }
bool has_plugin(symbol const & s) const { return has_plugin(get_family_id(s)); }
bool has_plugin(symbol const & s) const { return m_family_manager.has_family(s) && has_plugin(m_family_manager.get_family_id(s)); }
void get_dom(svector<symbol> & dom) const { m_family_manager.get_dom(dom); }
@ -1546,7 +1609,7 @@ protected:
}
public:
sort * get_sort(expr const * n) const;
sort * get_sort(expr const * n) const { return ::get_sort(n); }
void check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const;
void check_sorts_core(ast const * n) const;
bool check_sorts(ast const * n) const;

9
src/ast/ast_smt2_pp.cpp
View file

@ -501,7 +501,12 @@ class smt2_printer {
}
format * pp_simple_attribute(char const * attr, symbol const & s) {
return mk_compose(m(), mk_string(m(), attr), mk_string(m(), s.str().c_str()));
std::string str;
if (is_smt2_quoted_symbol(s))
str = mk_smt2_quoted_symbol(s);
else
str = s.str();
return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str()));
}
format * pp_labels(bool is_pos, buffer<symbol> const & names, format * f) {
@ -851,7 +856,7 @@ class smt2_printer {
buf.push_back(pp_simple_attribute(":weight ", q->get_weight()));
}
if (q->get_skid() != symbol::null) {
buf.push_back(pp_simple_attribute(":skid ", q->get_skid()));
buf.push_back(pp_simple_attribute(":skolemid ", q->get_skid()));
}
if (q->get_qid() != symbol::null) {
#if 0

12
src/ast/ast_smt_pp.cpp
View file

@ -795,11 +795,11 @@ public:
m_simplify_implies(simplify_implies)
{
m_basic_fid = m.get_basic_family_id();
m_label_fid = m.get_family_id("label");
m_bv_fid = m.get_family_id("bv");
m_arith_fid = m.get_family_id("arith");
m_array_fid = m.get_family_id("array");
m_dt_fid = m.get_family_id("datatype");
m_label_fid = m.mk_family_id("label");
m_bv_fid = m.mk_family_id("bv");
m_arith_fid = m.mk_family_id("arith");
m_array_fid = m.mk_family_id("array");
m_dt_fid = m.mk_family_id("datatype");
}
void operator()(expr* n) {
@ -1009,7 +1009,7 @@ ast_smt_pp::ast_smt_pp(ast_manager& m):
m_status("unknown"),
m_category(),
m_logic(),
m_dt_fid(m.get_family_id("datatype")),
m_dt_fid(m.mk_family_id("datatype")),
m_is_declared(&m_is_declared_default),
m_simplify_implies(true)
{}

181
src/ast/bv_decl_plugin.cpp
View file

@ -41,26 +41,6 @@ bv_decl_plugin::bv_decl_plugin():
m_int_sort(0) {
}
void bv_decl_plugin::mk_table_upto(unsigned n) {
if (m_powers.empty()) {
m_powers.push_back(rational(1));
}
unsigned sz = m_powers.size();
rational curr = m_powers[sz - 1];
rational two(2);
for (unsigned i = sz; i <= n; i++) {
curr *= two;
m_powers.push_back(curr);
}
}
rational bv_decl_plugin::power_of_two(unsigned n) const {
if (n >= m_powers.size()) {
const_cast<bv_decl_plugin*>(this)->mk_table_upto(n + 1);
}
return m_powers[n];
}
void bv_decl_plugin::set_manager(ast_manager * m, family_id id) {
decl_plugin::set_manager(m, id);
@ -79,7 +59,7 @@ void bv_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_xor3 = m_manager->mk_func_decl(symbol("xor3"), 3, d, b, func_decl_info(m_family_id, OP_XOR3));
m_manager->inc_ref(m_xor3);
m_int_sort = m_manager->mk_sort(m_manager->get_family_id("arith"), INT_SORT);
m_int_sort = m_manager->mk_sort(m_manager->mk_family_id("arith"), INT_SORT);
SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before bv_decl_plugin.
m_manager->inc_ref(m_int_sort);
}
@ -169,7 +149,7 @@ void bv_decl_plugin::mk_bv_sort(unsigned bv_size) {
sz = sort_size::mk_very_big();
}
else {
sz = sort_size(power_of_two(bv_size));
sz = sort_size(rational::power_of_two(bv_size));
}
m_bv_sorts[bv_size] = m_manager->mk_sort(symbol("bv"), sort_info(m_family_id, BV_SORT, sz, 1, &p));
m_manager->inc_ref(m_bv_sorts[bv_size]);
@ -436,7 +416,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
// This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
// After SMT-COMP, I should find all offending modules.
// For now, I will just simplify the numeral here.
parameter p0(mod(parameters[0].get_rational(), power_of_two(bv_size)));
parameter p0(mod(parameters[0].get_rational(), rational::power_of_two(bv_size)));
parameter ps[2] = { p0, parameters[1] };
sort * bv = get_bv_sort(bv_size);
return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
@ -621,7 +601,7 @@ void bv_decl_plugin::get_offset_term(app * a, expr * & t, rational & offset) con
offset = decl->get_parameter(0).get_rational();
sz = decl->get_parameter(1).get_int();
t = a->get_arg(1);
offset = mod(offset, power_of_two(sz));
offset = mod(offset, rational::power_of_two(sz));
}
else {
t = a;
@ -729,37 +709,104 @@ expr * bv_decl_plugin::get_some_value(sort * s) {
return m_manager->mk_app(m_family_id, OP_BV_NUM, 2, p, 0, 0);
}
bv_util::bv_util(ast_manager & m):
m_manager(m) {
SASSERT(m.has_plugin(symbol("bv")));
m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.get_family_id("bv")));
}
rational bv_util::norm(rational const & val, unsigned bv_size, bool is_signed) const {
rational r = mod(val, power_of_two(bv_size));
rational bv_recognizers::norm(rational const & val, unsigned bv_size, bool is_signed) const {
rational r = mod(val, rational::power_of_two(bv_size));
SASSERT(!r.is_neg());
if (is_signed) {
if (r >= power_of_two(bv_size - 1)) {
r -= power_of_two(bv_size);
if (r >= rational::power_of_two(bv_size - 1)) {
r -= rational::power_of_two(bv_size);
}
if (r < -power_of_two(bv_size - 1)) {
r += power_of_two(bv_size);
if (r < -rational::power_of_two(bv_size - 1)) {
r += rational::power_of_two(bv_size);
}
}
return r;
}
bool bv_util::has_sign_bit(rational const & n, unsigned bv_size) const {
bool bv_recognizers::has_sign_bit(rational const & n, unsigned bv_size) const {
SASSERT(bv_size > 0);
rational m = norm(n, bv_size, false);
rational p = power_of_two(bv_size - 1);
rational p = rational::power_of_two(bv_size - 1);
return m >= p;
}
bool bv_util::is_bv_sort(sort const * s) const {
bool bv_recognizers::is_bv_sort(sort const * s) const {
return (s->get_family_id() == get_fid() && s->get_decl_kind() == BV_SORT && s->get_num_parameters() == 1);
}
bool bv_recognizers::is_numeral(expr const * n, rational & val, unsigned & bv_size) const {
if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
return false;
}
func_decl * decl = to_app(n)->get_decl();
val = decl->get_parameter(0).get_rational();
bv_size = decl->get_parameter(1).get_int();
return true;
}
bool bv_recognizers::is_allone(expr const * e) const {
rational r;
unsigned bv_size;
if (!is_numeral(e, r, bv_size)) {
return false;
}
bool result = (r == rational::power_of_two(bv_size) - rational(1));
TRACE("is_allone", tout << r << " " << result << "\n";);
return result;
}
bool bv_recognizers::is_zero(expr const * n) const {
if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
return false;
}
func_decl * decl = to_app(n)->get_decl();
return decl->get_parameter(0).get_rational().is_zero();
}
bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) {
if (!is_extract(e)) return false;
low = get_extract_low(e);
high = get_extract_high(e);
b = to_app(e)->get_arg(0);
return true;
}
bool bv_recognizers::is_bv2int(expr const* e, expr*& r) {
if (!is_bv2int(e)) return false;
r = to_app(e)->get_arg(0);
return true;
}
bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational & result) {
if (n.is_one()) {
result = n;
return true;
}
if (!mod(n, rational(2)).is_one()) {
return false;
}
rational g;
rational x;
rational y;
g = gcd(n, rational::power_of_two(bv_size), x, y);
if (x.is_neg()) {
x = mod(x, rational::power_of_two(bv_size));
}
SASSERT(x.is_pos());
SASSERT(mod(x * n, rational::power_of_two(bv_size)).is_one());
result = x;
return true;
}
bv_util::bv_util(ast_manager & m):
bv_recognizers(m.mk_family_id(symbol("bv"))),
m_manager(m) {
SASSERT(m.has_plugin(symbol("bv")));
m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv")));
}
app * bv_util::mk_numeral(rational const & val, sort* s) {
if (!is_bv_sort(s)) {
return 0;
@ -774,67 +821,13 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) {
return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0);
}
bool bv_util::is_numeral(expr const * n, rational & val, unsigned & bv_size) const {
if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
return false;
}
func_decl * decl = to_app(n)->get_decl();
val = decl->get_parameter(0).get_rational();
bv_size = decl->get_parameter(1).get_int();
return true;
}
bool bv_util::is_allone(expr const * e) const {
rational r;
unsigned bv_size;
if (!is_numeral(e, r, bv_size)) {
return false;
}
bool result = (r == power_of_two(bv_size) - rational(1));
TRACE("is_allone", tout << r << " " << result << "\n";);
return result;
}
bool bv_util::is_zero(expr const * n) const {
if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
return false;
}
func_decl * decl = to_app(n)->get_decl();
return decl->get_parameter(0).get_rational().is_zero();
}
sort * bv_util::mk_sort(unsigned bv_size) {
parameter p[1] = { parameter(bv_size) };
return m_manager.mk_sort(get_fid(), BV_SORT, 1, p);
}
bool bv_util::mult_inverse(rational const & n, unsigned bv_size, rational & result) {
if (n.is_one()) {
result = n;
return true;
}
if (!mod(n, rational(2)).is_one()) {
return false;
}
rational g;
rational x;
rational y;
g = gcd(n, power_of_two(bv_size), x, y);
if (x.is_neg()) {
x = mod(x, power_of_two(bv_size));
}
SASSERT(x.is_pos());
SASSERT(mod(x * n, power_of_two(bv_size)).is_one());
result = x;
return true;
}
app * bv_util::mk_bv2int(expr* e) {
sort* s = m_manager.mk_sort(m_manager.get_family_id("arith"), INT_SORT);
sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT);
parameter p(s);
return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
}

142
src/ast/bv_decl_plugin.h
View file

@ -127,9 +127,6 @@ inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) {
class bv_decl_plugin : public decl_plugin {
protected:
vector<rational> m_powers;
void mk_table_upto(unsigned n);
symbol m_bv_sym;
symbol m_concat_sym;
symbol m_sign_extend_sym;
@ -245,8 +242,6 @@ protected:
public:
bv_decl_plugin();
rational power_of_two(unsigned n) const;
virtual ~bv_decl_plugin() {}
virtual void finalize();
@ -273,7 +268,70 @@ public:
virtual expr * get_some_value(sort * s);
};
class bv_util {
class bv_recognizers {
family_id m_afid;
public:
bv_recognizers(family_id fid):m_afid(fid) {}
family_id get_fid() const { return m_afid; }
family_id get_family_id() const { return get_fid(); }
bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
bool is_numeral(expr const * n) const { return is_app_of(n, get_fid(), OP_BV_NUM); }
bool is_allone(expr const * e) const;
bool is_zero(expr const * e) const;
bool is_bv_sort(sort const * s) const;
bool is_bv(expr const* e) const { return is_bv_sort(get_sort(e)); }
bool is_concat(expr const * e) const { return is_app_of(e, get_fid(), OP_CONCAT); }
bool is_extract(func_decl const * f) const { return is_decl_of(f, get_fid(), OP_EXTRACT); }
bool is_extract(expr const * e) const { return is_app_of(e, get_fid(), OP_EXTRACT); }
unsigned get_extract_high(func_decl const * f) const { return f->get_parameter(0).get_int(); }
unsigned get_extract_low(func_decl const * f) const { return f->get_parameter(1).get_int(); }
unsigned get_extract_high(expr const * n) { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
unsigned get_extract_low(expr const * n) { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b);
bool is_bv2int(expr const * e, expr * & r);
bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); }
bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); }
bool is_bv_mul(expr const * e) const { return is_app_of(e, get_fid(), OP_BMUL); }
bool is_bv_neg(expr const * e) const { return is_app_of(e, get_fid(), OP_BNEG); }
bool is_bv_sdiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BSDIV); }
bool is_bv_udiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BUDIV); }
bool is_bv_srem(expr const * e) const { return is_app_of(e, get_fid(), OP_BSREM); }
bool is_bv_urem(expr const * e) const { return is_app_of(e, get_fid(), OP_BUREM); }
bool is_bv_smod(expr const * e) const { return is_app_of(e, get_fid(), OP_BSMOD); }
bool is_bv_and(expr const * e) const { return is_app_of(e, get_fid(), OP_BAND); }
bool is_bv_or(expr const * e) const { return is_app_of(e, get_fid(), OP_BOR); }
bool is_bv_xor(expr const * e) const { return is_app_of(e, get_fid(), OP_BXOR); }
bool is_bv_nand(expr const * e) const { return is_app_of(e, get_fid(), OP_BNAND); }
bool is_bv_nor(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOR); }
bool is_bv_not(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOT); }
bool is_bv_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); }
bool is_bv_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); }
bool is_bit2bool(expr const * e) const { return is_app_of(e, get_fid(), OP_BIT2BOOL); }
bool is_bv2int(expr const* e) const { return is_app_of(e, get_fid(), OP_BV2INT); }
bool is_int2bv(expr const* e) const { return is_app_of(e, get_fid(), OP_INT2BV); }
bool is_mkbv(expr const * e) const { return is_app_of(e, get_fid(), OP_MKBV); }
bool is_bv_ashr(expr const * e) const { return is_app_of(e, get_fid(), OP_BASHR); }
bool is_bv_lshr(expr const * e) const { return is_app_of(e, get_fid(), OP_BLSHR); }
bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); }
bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); }
MATCH_BINARY(is_bv_add);
MATCH_BINARY(is_bv_mul);
MATCH_BINARY(is_bv_sle);
MATCH_BINARY(is_bv_ule);
MATCH_BINARY(is_bv_shl);
rational norm(rational const & val, unsigned bv_size, bool is_signed) const ;
rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
bool has_sign_bit(rational const & n, unsigned bv_size) const;
bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
};
class bv_util : public bv_recognizers {
ast_manager & m_manager;
bv_decl_plugin * m_plugin;
@ -282,29 +340,10 @@ public:
ast_manager & get_manager() const { return m_manager; }
family_id get_fid() const { return m_plugin->get_family_id(); }
family_id get_family_id() const { return get_fid(); }
rational power_of_two(unsigned n) const { return m_plugin->power_of_two(n); }
rational norm(rational const & val, unsigned bv_size, bool is_signed) const ;
rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
bool has_sign_bit(rational const & n, unsigned bv_size) const;
app * mk_numeral(rational const & val, sort* s);
app * mk_numeral(rational const & val, unsigned bv_size);
app * mk_numeral(uint64 u, unsigned bv_size) { return mk_numeral(rational(u, rational::ui64()), bv_size); }
sort * mk_sort(unsigned bv_size);
bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
bool is_numeral(expr const * n) const {
return is_app_of(n, get_fid(), OP_BV_NUM);
}
bool is_allone(expr const * e) const;
bool is_zero(expr const * e) const;
bool is_bv_sort(sort const * s) const;
bool is_bv(expr const* e) const {
return is_bv_sort(m_manager.get_sort(e));
}
unsigned get_bv_size(sort const * s) const {
SASSERT(is_bv_sort(s));
@ -348,59 +387,6 @@ public:
app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); }
bool is_concat(expr const * e) const { return is_app_of(e, get_fid(), OP_CONCAT); }
bool is_extract(func_decl const * f) const { return is_decl_of(f, get_fid(), OP_EXTRACT); }
bool is_extract(expr const * e) const { return is_app_of(e, get_fid(), OP_EXTRACT); }
unsigned get_extract_high(func_decl const * f) const { return f->get_parameter(0).get_int(); }
unsigned get_extract_low(func_decl const * f) const { return f->get_parameter(1).get_int(); }
unsigned get_extract_high(expr const * n) { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
unsigned get_extract_low(expr const * n) { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
bool is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) {
if (!is_extract(e)) return false;
low = get_extract_low(e);
high = get_extract_high(e);
b = to_app(e)->get_arg(0);
return true;
}
bool is_bv2int(expr const* e, expr*& r) {
if (!is_bv2int(e)) return false;
r = to_app(e)->get_arg(0);
return true;
}
bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); }
bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); }
bool is_bv_mul(expr const * e) const { return is_app_of(e, get_fid(), OP_BMUL); }
bool is_bv_neg(expr const * e) const { return is_app_of(e, get_fid(), OP_BNEG); }
bool is_bv_sdiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BSDIV); }
bool is_bv_udiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BUDIV); }
bool is_bv_srem(expr const * e) const { return is_app_of(e, get_fid(), OP_BSREM); }
bool is_bv_urem(expr const * e) const { return is_app_of(e, get_fid(), OP_BUREM); }
bool is_bv_smod(expr const * e) const { return is_app_of(e, get_fid(), OP_BSMOD); }
bool is_bv_and(expr const * e) const { return is_app_of(e, get_fid(), OP_BAND); }
bool is_bv_or(expr const * e) const { return is_app_of(e, get_fid(), OP_BOR); }
bool is_bv_xor(expr const * e) const { return is_app_of(e, get_fid(), OP_BXOR); }
bool is_bv_nand(expr const * e) const { return is_app_of(e, get_fid(), OP_BNAND); }
bool is_bv_nor(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOR); }
bool is_bv_not(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOT); }
bool is_bv_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); }
bool is_bv_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); }
bool is_bit2bool(expr const * e) const { return is_app_of(e, get_fid(), OP_BIT2BOOL); }
bool is_bv2int(expr const* e) const { return is_app_of(e, get_fid(), OP_BV2INT); }
bool is_int2bv(expr const* e) const { return is_app_of(e, get_fid(), OP_INT2BV); }
bool is_mkbv(expr const * e) const { return is_app_of(e, get_fid(), OP_MKBV); }
bool is_bv_ashr(expr const * e) const { return is_app_of(e, get_fid(), OP_BASHR); }
bool is_bv_lshr(expr const * e) const { return is_app_of(e, get_fid(), OP_BLSHR); }
bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); }
bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); }
MATCH_BINARY(is_bv_add);
MATCH_BINARY(is_bv_mul);
MATCH_BINARY(is_bv_sle);
MATCH_BINARY(is_bv_ule);
MATCH_BINARY(is_bv_shl);
bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
};
#endif /* _BV_DECL_PLUGIN_H_ */

2
src/ast/datatype_decl_plugin.cpp
View file

@ -673,7 +673,7 @@ bool datatype_decl_plugin::is_value(app * e) const {
datatype_util::datatype_util(ast_manager & m):
m_manager(m),
m_family_id(m.get_family_id("datatype")),
m_family_id(m.mk_family_id("datatype")),
m_asts(m) {
}

2
src/ast/decl_collector.cpp
View file

@ -45,7 +45,7 @@ decl_collector::decl_collector(ast_manager & m, bool preds):
m_manager(m),
m_sep_preds(preds) {
m_basic_fid = m_manager.get_basic_family_id();
m_dt_fid = m_manager.get_family_id("datatype");
m_dt_fid = m_manager.mk_family_id("datatype");
}
void decl_collector::visit(ast* n) {

2
src/ast/dl_decl_plugin.cpp
View file

@ -629,7 +629,7 @@ namespace datalog {
m(m),
m_arith(m),
m_bv(m),
m_fid(m.get_family_id(symbol("datalog_relation")))
m_fid(m.mk_family_id(symbol("datalog_relation")))
{}
// create a constant belonging to a given finite domain.

6
src/ast/float_decl_plugin.cpp
View file

@ -31,7 +31,7 @@ float_decl_plugin::float_decl_plugin():
void float_decl_plugin::set_manager(ast_manager * m, family_id id) {
decl_plugin::set_manager(m, id);
family_id aid = m_manager->get_family_id("arith");
family_id aid = m_manager->mk_family_id("arith");
m_real_sort = m_manager->mk_sort(aid, REAL_SORT);
SASSERT(m_real_sort != 0); // arith_decl_plugin must be installed before float_decl_plugin.
m_manager->inc_ref(m_real_sort);
@ -42,7 +42,7 @@ void float_decl_plugin::set_manager(ast_manager * m, family_id id) {
if (m_manager->has_plugin(symbol("bv"))) {
// bv plugin is optional, so m_bv_plugin may be 0
m_bv_fid = m_manager->get_family_id("bv");
m_bv_fid = m_manager->mk_family_id("bv");
m_bv_plugin = static_cast<bv_decl_plugin*>(m_manager->get_plugin(m_bv_fid));
}
}
@ -512,7 +512,7 @@ bool float_decl_plugin::is_value(app * e) const {
float_util::float_util(ast_manager & m):
m_manager(m),
m_fid(m.get_family_id("float")),
m_fid(m.mk_family_id("float")),
m_a_util(m) {
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m_fid));
}

2
src/ast/format.cpp
View file

@ -103,7 +103,7 @@ namespace format_ns {
symbol f("format");
if (!fm(m).has_plugin(f))
fm(m).register_plugin(f, alloc(format_decl_plugin));
return fm(m).get_family_id(f);
return fm(m).mk_family_id(f);
}
static family_id fid(ast_manager & m) {

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

@ -41,7 +41,7 @@ macro_util::macro_util(ast_manager & m, simplifier & s):
arith_simplifier_plugin * macro_util::get_arith_simp() const {
if (m_arith_simp == 0) {
const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.get_family_id("arith")));
const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("arith")));
}
SASSERT(m_arith_simp != 0);
return m_arith_simp;
@ -49,7 +49,7 @@ arith_simplifier_plugin * macro_util::get_arith_simp() const {
bv_simplifier_plugin * macro_util::get_bv_simp() const {
if (m_bv_simp == 0) {
const_cast<macro_util*>(this)->m_bv_simp = static_cast<bv_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.get_family_id("bv")));
const_cast<macro_util*>(this)->m_bv_simp = static_cast<bv_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("bv")));
}
SASSERT(m_bv_simp != 0);
return m_bv_simp;

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

@ -17,11 +17,67 @@ Revision History:
--*/
#include"defined_names.h"
#include"obj_hashtable.h"
#include"used_vars.h"
#include"var_subst.h"
#include"ast_smt2_pp.h"
#include"ast_pp.h"
struct defined_names::impl {
typedef obj_map<expr, app *> expr2name;
typedef obj_map<expr, proof *> expr2proof;
ast_manager & m_manager;
symbol m_z3name;
/**
\brief Mapping from expressions to their names. A name is an application.
If the expression does not have free variables, then the name is just a constant.
*/
expr2name m_expr2name;
/**
\brief Mapping from expressions to the apply-def proof.
That is, for each expression e, m_expr2proof[e] is the
proof e and m_expr2name[2] are observ. equivalent.
This mapping is not used if proof production is disabled.
*/
expr2proof m_expr2proof;
/**
\brief Domain of m_expr2name. It is used to keep the expressions
alive and for backtracking
*/
expr_ref_vector m_exprs;
expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive.
proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive.
unsigned_vector m_lims; //!< Backtracking support.
impl(ast_manager & m, char const * prefix);
virtual ~impl();
app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
void cache_new_name(expr * e, app * name);
void cache_new_name_intro_proof(expr * e, proof * pr);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result);
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
void push_scope();
void pop_scope(unsigned num_scopes);
void reset();
unsigned get_num_names() const { return m_names.size(); }
func_decl * get_name_decl(unsigned i) const { return to_app(m_names.get(i))->get_decl(); }
};
struct defined_names::pos_impl : public defined_names::impl {
pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
};
defined_names::impl::impl(ast_manager & m, char const * prefix):
m_manager(m),
m_exprs(m),
@ -222,5 +278,50 @@ void defined_names::impl::reset() {
m_lims.reset();
}
defined_names::defined_names(ast_manager & m, char const * fresh_prefix) {
m_impl = alloc(impl, m, fresh_prefix);
m_pos_impl = alloc(pos_impl, m, fresh_prefix);
}
defined_names::~defined_names() {
dealloc(m_impl);
dealloc(m_pos_impl);
}
bool defined_names::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
return m_impl->mk_name(e, new_def, new_def_pr, n, pr);
}
bool defined_names::mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
return m_pos_impl->mk_name(e, new_def, new_def_pr, n, pr);
}
void defined_names::push() {
m_impl->push_scope();
m_pos_impl->push_scope();
}
void defined_names::pop(unsigned num_scopes) {
m_impl->pop_scope(num_scopes);
m_pos_impl->pop_scope(num_scopes);
}
void defined_names::reset() {
m_impl->reset();
m_pos_impl->reset();
}
unsigned defined_names::get_num_names() const {
return m_impl->get_num_names() + m_pos_impl->get_num_names();
}
func_decl * defined_names::get_name_decl(unsigned i) const {
SASSERT(i < get_num_names());
unsigned n1 = m_impl->get_num_names();
return i < n1 ? m_impl->get_name_decl(i) : m_pos_impl->get_name_decl(i - n1);
}

88
src/ast/normal_forms/defined_names.h
View file

@ -21,7 +21,6 @@ Revision History:
#define _DEFINED_NAMES_H_
#include"ast.h"
#include"obj_hashtable.h"
/**
\brief Mapping from expressions to skolem functions that are used to name them.
@ -29,62 +28,13 @@ Revision History:
The mapping supports backtracking using the methods #push_scope and #pop_scope.
*/
class defined_names {
struct impl {
typedef obj_map<expr, app *> expr2name;
typedef obj_map<expr, proof *> expr2proof;
ast_manager & m_manager;
symbol m_z3name;
/**
\brief Mapping from expressions to their names. A name is an application.
If the expression does not have free variables, then the name is just a constant.
*/
expr2name m_expr2name;
/**
\brief Mapping from expressions to the apply-def proof.
That is, for each expression e, m_expr2proof[e] is the
proof e and m_expr2name[2] are observ. equivalent.
This mapping is not used if proof production is disabled.
*/
expr2proof m_expr2proof;
/**
\brief Domain of m_expr2name. It is used to keep the expressions
alive and for backtracking
*/
expr_ref_vector m_exprs;
expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive.
proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive.
unsigned_vector m_lims; //!< Backtracking support.
impl(ast_manager & m, char const * prefix);
virtual ~impl();
app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
void cache_new_name(expr * e, app * name);
void cache_new_name_intro_proof(expr * e, proof * pr);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result);
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
void push_scope();
void pop_scope(unsigned num_scopes);
void reset();
};
struct pos_impl : public impl {
pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
};
impl m_impl;
pos_impl m_pos_impl;
struct impl;
struct pos_impl;
impl * m_impl;
pos_impl * m_pos_impl;
public:
defined_names(ast_manager & m, char const * fresh_prefix = "z3name"):m_impl(m, fresh_prefix), m_pos_impl(m, fresh_prefix) {}
defined_names(ast_manager & m, char const * fresh_prefix = "z3name");
~defined_names();
// -----------------------------------
//
@ -113,9 +63,7 @@ public:
Remark: the definitions are closed with an universal quantifier if e contains free variables.
*/
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
return m_impl.mk_name(e, new_def, new_def_pr, n, pr);
}
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
/**
\brief Create a name for a positive occurrence of the expression \c e.
@ -127,24 +75,14 @@ public:
Remark: the definitions are closed with an universal quantifier if e contains free variables.
*/
bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
return m_pos_impl.mk_name(e, new_def, new_def_pr, n, pr);
}
bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
void push_scope() {
m_impl.push_scope();
m_pos_impl.push_scope();
}
void push();
void pop(unsigned num_scopes);
void reset();
void pop_scope(unsigned num_scopes) {
m_impl.pop_scope(num_scopes);
m_pos_impl.pop_scope(num_scopes);
}
void reset() {
m_impl.reset();
m_pos_impl.reset();
}
unsigned get_num_names() const;
func_decl * get_name_decl(unsigned i) const;
};
#endif /* _DEFINED_NAMES_H_ */

2
src/ast/pattern/pattern_inference.cpp
View file

@ -91,7 +91,7 @@ pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params &
simplifier(m),
m_params(params),
m_bfid(m.get_basic_family_id()),
m_afid(m.get_family_id("arith")),
m_afid(m.mk_family_id("arith")),
m_le(m),
m_nested_arith_only(true),
m_block_loop_patterns(params.m_pi_block_loop_patterns),

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

@ -150,7 +150,7 @@ class pattern_inference : public simplifier {
void save_candidate(expr * n, unsigned delta);
void reset();
public:
collect(ast_manager & m, pattern_inference & o):m_manager(m), m_owner(o), m_afid(m.get_family_id("arith")) {}
collect(ast_manager & m, pattern_inference & o):m_manager(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
void operator()(expr * n, unsigned num_bindings);
};

2
src/ast/proof_checker/proof_checker.cpp
View file

@ -85,7 +85,7 @@ proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pi
if (!m.has_plugin(fam_name)) {
m.register_plugin(fam_name, alloc(hyp_decl_plugin));
}
m_hyp_fid = m.get_family_id(fam_name);
m_hyp_fid = m.mk_family_id(fam_name);
// m_spc_fid = m.get_family_id("spc");
m_nil = m.mk_const(m_hyp_fid, OP_NIL);
}

14
src/ast/reg_decl_plugins.cpp
View file

@ -27,25 +27,25 @@ Revision History:
#include"float_decl_plugin.h"
void reg_decl_plugins(ast_manager & m) {
if (!m.get_plugin(m.get_family_id(symbol("arith")))) {
if (!m.get_plugin(m.mk_family_id(symbol("arith")))) {
m.register_plugin(symbol("arith"), alloc(arith_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("bv")))) {
if (!m.get_plugin(m.mk_family_id(symbol("bv")))) {
m.register_plugin(symbol("bv"), alloc(bv_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("array")))) {
if (!m.get_plugin(m.mk_family_id(symbol("array")))) {
m.register_plugin(symbol("array"), alloc(array_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("datatype")))) {
if (!m.get_plugin(m.mk_family_id(symbol("datatype")))) {
m.register_plugin(symbol("datatype"), alloc(datatype_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("datalog_relation")))) {
if (!m.get_plugin(m.mk_family_id(symbol("datalog_relation")))) {
m.register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("seq")))) {
if (!m.get_plugin(m.mk_family_id(symbol("seq")))) {
m.register_plugin(symbol("seq"), alloc(seq_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("float")))) {
if (!m.get_plugin(m.mk_family_id(symbol("float")))) {
m.register_plugin(symbol("float"), alloc(float_decl_plugin));
}
}

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

@ -36,7 +36,7 @@ public:
bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, basic_simplifier_plugin & _s);
ast_manager & m() const { return m_util.get_manager(); }
numeral power(unsigned n) const { return m_util.power_of_two(n); }
numeral power(unsigned n) const { return rational::power_of_two(n); }
void mk_xor(expr * a, expr * b, expr_ref & r) { s.mk_xor(a, b, r); }
void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r);
void mk_carry(expr * a, expr * b, expr * c, expr_ref & r);

2
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -32,7 +32,7 @@ struct blaster_cfg {
blaster_cfg(bool_rewriter & r, bv_util & u):m_rewriter(r), m_util(u) {}
ast_manager & m() const { return m_util.get_manager(); }
numeral power(unsigned n) const { return m_util.power_of_two(n); }
numeral power(unsigned n) const { return rational::power_of_two(n); }
void mk_xor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_xor(a, b, r); }
void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r) {
expr_ref tmp(m());

3
src/ast/rewriter/bool_rewriter.cpp
View file

@ -27,6 +27,7 @@ void bool_rewriter::updt_params(params_ref const & _p) {
m_local_ctx = p.local_ctx();
m_local_ctx_limit = p.local_ctx_limit();
m_blast_distinct = p.blast_distinct();
m_blast_distinct_threshold = p.blast_distinct_threshold();
m_ite_extra_rules = p.ite_extra_rules();
}
@ -746,7 +747,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
return BR_DONE;
}
if (m_blast_distinct) {
if (m_blast_distinct && num_args < m_blast_distinct_threshold) {
ptr_buffer<expr> new_diseqs;
for (unsigned i = 0; i < num_args; i++) {
for (unsigned j = i + 1; j < num_args; j++)

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

@ -55,6 +55,7 @@ class bool_rewriter {
bool m_local_ctx;
bool m_elim_and;
bool m_blast_distinct;
unsigned m_blast_distinct_threshold;
bool m_ite_extra_rules;
unsigned m_local_ctx_limit;
unsigned m_local_ctx_cost;

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

@ -6,4 +6,6 @@ def_module_params(module_name='rewriter',
("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"),
("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"),
("local_ctx_limit", UINT, UINT_MAX, "limit for applying local context simplifier"),
("blast_distinct", BOOL, False, "expand a distinct predicate into a quadratic number of disequalities")))
("blast_distinct", BOOL, False, "expand a distinct predicate into a quadratic number of disequalities"),
("blast_distinct_threshold", UINT, UINT_MAX, "when blast_distinct is true, only distinct expressions with less than this number of arguments are blasted")
))

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

@ -283,12 +283,12 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
if (is_num1 || is_num2) {
if (is_signed) {
lower = - m_util.power_of_two(sz - 1);
upper = m_util.power_of_two(sz - 1) - numeral(1);
lower = - rational::power_of_two(sz - 1);
upper = rational::power_of_two(sz - 1) - numeral(1);
}
else {
lower = numeral(0);
upper = m_util.power_of_two(sz) - numeral(1);
upper = rational::power_of_two(sz) - numeral(1);
}
}
@ -387,14 +387,14 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
if (is_numeral(arg, v, sz)) {
sz = high - low + 1;
if (v.is_neg())
mod(v, m_util.power_of_two(sz), v);
mod(v, rational::power_of_two(sz), v);
if (v.is_uint64()) {
uint64 u = v.get_uint64();
uint64 e = shift_right(u, low) & (shift_left(1ull, sz) - 1ull);
result = mk_numeral(numeral(e, numeral::ui64()), sz);
return BR_DONE;
}
div(v, m_util.power_of_two(low), v);
div(v, rational::power_of_two(low), v);
result = mk_numeral(v, sz);
return BR_DONE;
}
@ -519,7 +519,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
SASSERT(r2 < numeral(bv_size));
SASSERT(r2.is_unsigned());
r1 = m_util.norm(r1 * m_util.power_of_two(r2.get_unsigned()), bv_size);
r1 = m_util.norm(r1 * rational::power_of_two(r2.get_unsigned()), bv_size);
result = mk_numeral(r1, bv_size);
return BR_DONE;
}
@ -567,7 +567,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
SASSERT(r2.is_unsigned());
unsigned sh = r2.get_unsigned();
div(r1, m_util.power_of_two(sh), r1);
div(r1, rational::power_of_two(sh), r1);
result = mk_numeral(r1, bv_size);
return BR_DONE;
}
@ -626,7 +626,7 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
if (is_num1 && is_num2 && numeral(bv_size) <= r2) {
if (m_util.has_sign_bit(r1, bv_size))
result = mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size);
result = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
else
result = mk_numeral(0, bv_size);
return BR_DONE;
@ -635,7 +635,7 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
if (is_num1 && is_num2) {
SASSERT(r2 < numeral(bv_size));
bool sign = m_util.has_sign_bit(r1, bv_size);
div(r1, m_util.power_of_two(r2.get_unsigned()), r1);
div(r1, rational::power_of_two(r2.get_unsigned()), r1);
if (sign) {
// pad ones.
numeral p(1);
@ -697,7 +697,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
// The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff)
result = m().mk_ite(m().mk_app(get_fid(), OP_SLT, arg1, mk_numeral(0, bv_size)),
mk_numeral(1, bv_size),
mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size));
mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size));
return BR_REWRITE2;
}
}
@ -746,7 +746,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
}
else {
// The "hardware interpretation" for (bvudiv x 0) is #xffff
result = mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size);
result = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
return BR_DONE;
}
@ -845,7 +845,7 @@ bool bv_rewriter::is_minus_one_core(expr * arg) const {
numeral r;
unsigned bv_size;
if (is_numeral(arg, r, bv_size)) {
return r == (m_util.power_of_two(bv_size) - numeral(1));
return r == (rational::power_of_two(bv_size) - numeral(1));
}
return false;
}
@ -924,7 +924,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
if (is_x_minus_one(arg1, x) && x == arg2) {
bv_size = get_bv_size(arg1);
expr * x_minus_1 = arg1;
expr * minus_one = mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size);
expr * minus_one = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
result = m().mk_ite(m().mk_eq(x, mk_numeral(0, bv_size)),
m().mk_app(get_fid(), OP_BUREM0, minus_one),
x_minus_1);
@ -1068,7 +1068,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
if (i > 0)
prev = new_args.back();
if (is_numeral(arg, v1, sz1) && prev != 0 && is_numeral(prev, v2, sz2)) {
v2 *= m_util.power_of_two(sz1);
v2 *= rational::power_of_two(sz1);
v2 += v1;
new_args.pop_back();
new_args.push_back(mk_numeral(v2, sz1+sz2));
@ -1137,7 +1137,7 @@ br_status bv_rewriter::mk_sign_extend(unsigned n, expr * arg, expr_ref & result)
if (is_numeral(arg, r, bv_size)) {
unsigned result_bv_size = bv_size + n;
r = m_util.norm(r, bv_size, true);
mod(r, m_util.power_of_two(result_bv_size), r);
mod(r, rational::power_of_two(result_bv_size), r);
result = mk_numeral(r, result_bv_size);
return BR_DONE;
}
@ -1213,7 +1213,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
if (m_util.is_bv_not(arg)) {
expr * atom = to_app(arg)->get_arg(0);
if (pos_args.is_marked(atom)) {
result = mk_numeral(m_util.power_of_two(sz) - numeral(1), sz);
result = mk_numeral(rational::power_of_two(sz) - numeral(1), sz);
return BR_DONE;
}
else if (neg_args.is_marked(atom)) {
@ -1229,7 +1229,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
continue;
}
else if (neg_args.is_marked(arg)) {
result = mk_numeral(m_util.power_of_two(sz) - numeral(1), sz);
result = mk_numeral(rational::power_of_two(sz) - numeral(1), sz);
return BR_DONE;
}
pos_args.mark(arg, true);
@ -1237,7 +1237,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
}
}
if (v1 == m_util.power_of_two(sz) - numeral(1)) {
if (v1 == rational::power_of_two(sz) - numeral(1)) {
result = mk_numeral(v1, sz);
return BR_DONE;
}
@ -1294,7 +1294,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
}
if (i != low) {
unsigned num_sz = i - low;
exs.push_back(m_util.mk_numeral(m_util.power_of_two(num_sz) - numeral(1), num_sz));
exs.push_back(m_util.mk_numeral(rational::power_of_two(num_sz) - numeral(1), num_sz));
low = i;
}
while (i < sz && mod(v1, two).is_zero()) {
@ -1385,7 +1385,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
else if (pos_args.is_marked(atom)) {
pos_args.mark(atom, false);
merged = true;
v1 = bitwise_xor(v1, m_util.power_of_two(sz) - numeral(1));
v1 = bitwise_xor(v1, rational::power_of_two(sz) - numeral(1));
}
else {
neg_args.mark(atom, true);
@ -1399,7 +1399,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
else if (neg_args.is_marked(arg)) {
neg_args.mark(arg, false);
merged = true;
v1 = bitwise_xor(v1, m_util.power_of_two(sz) - numeral(1));
v1 = bitwise_xor(v1, rational::power_of_two(sz) - numeral(1));
}
else {
pos_args.mark(arg, true);
@ -1455,7 +1455,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
return BR_REWRITE3;
}
if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (m_util.power_of_two(sz) - numeral(1)))))
if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1)))))
return BR_FAILED;
ptr_buffer<expr> new_args;
@ -1611,7 +1611,7 @@ br_status bv_rewriter::mk_bv_redand(expr * arg, expr_ref & result) {
numeral r;
unsigned bv_size;
if (is_numeral(arg, r, bv_size)) {
result = (r == m_util.power_of_two(bv_size) - numeral(1)) ? mk_numeral(1, 1) : mk_numeral(0, 1);
result = (r == rational::power_of_two(bv_size) - numeral(1)) ? mk_numeral(1, 1) : mk_numeral(0, 1);
return BR_DONE;
}
return BR_FAILED;
@ -1707,7 +1707,7 @@ bool bv_rewriter::is_zero_bit(expr * x, unsigned idx) {
if (is_numeral(x, val, bv_size)) {
if (val.is_zero())
return true;
div(val, m_util.power_of_two(idx), val);
div(val, rational::power_of_two(idx), val);
return (val % numeral(2)).is_zero();
}
if (m_util.is_concat(x)) {

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

@ -443,4 +443,4 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result
br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) {
return BR_FAILED;
}
}

2
src/ast/simplifier/bv_elim.cpp
View file

@ -15,7 +15,7 @@ void bv_elim::elim(quantifier* q, quantifier_ref& r) {
expr_ref new_body(m_manager);
expr* old_body = q->get_expr();
unsigned num_decls = q->get_num_decls();
family_id bfid = m_manager.get_family_id("bv");
family_id bfid = m_manager.mk_family_id("bv");
//
// Traverse sequence of bound variables to eliminate

40
src/ast/simplifier/bv_simplifier_plugin.cpp
View file

@ -76,9 +76,9 @@ app * bv_simplifier_plugin::mk_numeral(numeral const & n) {
}
app * bv_simplifier_plugin::mk_numeral(numeral const& n, unsigned bv_size) {
numeral r = mod(n, m_util.power_of_two(bv_size));
numeral r = mod(n, rational::power_of_two(bv_size));
SASSERT(!r.is_neg());
SASSERT(r < m_util.power_of_two(bv_size));
SASSERT(r < rational::power_of_two(bv_size));
return m_util.mk_numeral(r, bv_size);
}
@ -225,7 +225,7 @@ inline uint64 bv_simplifier_plugin::to_uint64(const numeral & n, unsigned bv_siz
SASSERT(bv_size <= 64);
numeral tmp = n;
if (tmp.is_neg()) {
tmp = mod(tmp, m_util.power_of_two(bv_size));
tmp = mod(tmp, rational::power_of_two(bv_size));
}
SASSERT(tmp.is_nonneg());
SASSERT(tmp.is_uint64());
@ -235,7 +235,7 @@ inline uint64 bv_simplifier_plugin::to_uint64(const numeral & n, unsigned bv_siz
#define MK_BV_OP(_oper_,_binop_) \
rational bv_simplifier_plugin::mk_bv_ ## _oper_(numeral const& a0, numeral const& b0, unsigned sz) { \
rational r(0), a(a0), b(b0); \
numeral p64 = m_util.power_of_two(64); \
numeral p64 = rational::power_of_two(64); \
numeral mul(1); \
while (sz > 0) { \
numeral a1 = a % p64; \
@ -260,7 +260,7 @@ MK_BV_OP(xor,^)
rational bv_simplifier_plugin::mk_bv_not(numeral const& a0, unsigned sz) {
rational r(0), a(a0), mul(1);
numeral p64 = m_util.power_of_two(64);
numeral p64 = rational::power_of_two(64);
while (sz > 0) {
numeral a1 = a % p64;
uint64 u = ~a1.get_uint64();
@ -320,12 +320,12 @@ void bv_simplifier_plugin::mk_leq_core(bool is_signed, expr * arg1, expr * arg2,
if (is_num1 || is_num2) {
if (is_signed) {
lower = - m_util.power_of_two(bv_size - 1);
upper = m_util.power_of_two(bv_size - 1) - numeral(1);
lower = - rational::power_of_two(bv_size - 1);
upper = rational::power_of_two(bv_size - 1) - numeral(1);
}
else {
lower = numeral(0);
upper = m_util.power_of_two(bv_size) - numeral(1);
upper = rational::power_of_two(bv_size) - numeral(1);
}
}
@ -509,7 +509,7 @@ bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * ar
if (m_util.is_numeral(a, r, num_bits)) {
if (r.is_neg()) {
r = mod(r, m_util.power_of_two(sz));
r = mod(r, rational::power_of_two(sz));
}
SASSERT(r.is_nonneg());
if (r.is_uint64()) {
@ -520,7 +520,7 @@ bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * ar
result = mk_numeral(numeral(e, numeral::ui64()), sz);
return true;
}
result = mk_numeral(div(r, m_util.power_of_two(low)), sz);
result = mk_numeral(div(r, rational::power_of_two(low)), sz);
return true;
}
// (extract[high:low] (extract[high2:low2] x)) == (extract[high+low2 : low+low2] x)
@ -902,7 +902,7 @@ void bv_simplifier_plugin::mk_concat(unsigned num_args, expr * const * args, exp
--i;
expr * arg = args[i];
if (is_numeral(arg, arg_val)) {
arg_val *= m_util.power_of_two(shift);
arg_val *= rational::power_of_two(shift);
val += arg_val;
shift += get_bv_size(arg);
TRACE("bv_simplifier_plugin",
@ -1203,7 +1203,7 @@ bool bv_simplifier_plugin::is_minus_one_core(expr * arg) const {
unsigned bv_size;
if (m_util.is_numeral(arg, r, bv_size)) {
numeral minus_one(-1);
minus_one = mod(minus_one, m_util.power_of_two(bv_size));
minus_one = mod(minus_one, rational::power_of_two(bv_size));
return r == minus_one;
}
return false;
@ -1295,7 +1295,7 @@ void bv_simplifier_plugin::mk_sign_extend(unsigned n, expr * arg, expr_ref & res
if (m_util.is_numeral(arg, r, bv_size)) {
unsigned result_bv_size = bv_size + n;
r = norm(r, bv_size, true);
r = mod(r, m_util.power_of_two(result_bv_size));
r = mod(r, rational::power_of_two(result_bv_size));
result = mk_numeral(r, result_bv_size);
TRACE("mk_sign_extend", tout << "n: " << n << "\n";
ast_ll_pp(tout, m_manager, arg); tout << "====>\n";
@ -1373,7 +1373,7 @@ void bv_simplifier_plugin::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result
else if (is_num1 && is_num2) {
SASSERT(r2 < rational(bv_size));
SASSERT(r2.is_unsigned());
result = mk_numeral(r1 * m_util.power_of_two(r2.get_unsigned()), bv_size);
result = mk_numeral(r1 * rational::power_of_two(r2.get_unsigned()), bv_size);
}
//
@ -1423,7 +1423,7 @@ void bv_simplifier_plugin::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & resul
else if (is_num1 && is_num2) {
SASSERT(r2.is_unsigned());
unsigned sh = r2.get_unsigned();
r1 = div(r1, m_util.power_of_two(sh));
r1 = div(r1, rational::power_of_two(sh));
result = mk_numeral(r1, bv_size);
}
//
@ -1804,8 +1804,8 @@ void bv_simplifier_plugin::mk_bv_rotate_left_core(unsigned shift, numeral r, uns
result = mk_numeral(r, bv_size);
}
else {
rational r1 = div(r, m_util.power_of_two(bv_size - shift)); // shift right
rational r2 = (r * m_util.power_of_two(shift)) % m_util.power_of_two(bv_size); // shift left
rational r1 = div(r, rational::power_of_two(bv_size - shift)); // shift right
rational r2 = (r * rational::power_of_two(shift)) % rational::power_of_two(bv_size); // shift left
result = mk_numeral(r1 + r2, bv_size);
}
}
@ -1831,8 +1831,8 @@ void bv_simplifier_plugin::mk_bv_rotate_right_core(unsigned shift, numeral r, un
result = mk_numeral(r, bv_size);
}
else {
rational r1 = div(r, m_util.power_of_two(shift)); // shift right
rational r2 = (r * m_util.power_of_two(bv_size - shift)) % m_util.power_of_two(bv_size); // shift left
rational r1 = div(r, rational::power_of_two(shift)); // shift right
rational r2 = (r * rational::power_of_two(bv_size - shift)) % rational::power_of_two(bv_size); // shift left
result = mk_numeral(r1 + r2, bv_size);
}
}
@ -1935,7 +1935,7 @@ void bv_simplifier_plugin::mk_bv_ashr(expr* arg1, expr* arg2, expr_ref& result)
else if (is_num1 && is_num2) {
SASSERT(r2 < rational(bv_size));
bool sign = has_sign_bit(r1, bv_size);
r1 = div(r1, m_util.power_of_two(r2.get_unsigned()));
r1 = div(r1, rational::power_of_two(r2.get_unsigned()));
if (sign) {
// pad ones.
rational p(1);

2
src/ast/simplifier/bv_simplifier_plugin.h
View file

@ -172,7 +172,7 @@ public:
app * mk_numeral(rational const & n, unsigned bv_size);
app * mk_numeral(uint64 n, unsigned bv_size) { return mk_numeral(numeral(n, numeral::ui64()), bv_size); }
app* mk_bv0(unsigned bv_size) { return m_util.mk_numeral(numeral(0), bv_size); }
rational mk_allone(unsigned bv_size) { return m_util.power_of_two(bv_size) - numeral(1); }
rational mk_allone(unsigned bv_size) { return rational::power_of_two(bv_size) - numeral(1); }
bool is_minus_one_core(expr * arg) const;
bool is_x_minus_one(expr * arg, expr * & x);
void mk_int2bv(expr * arg, sort* range, expr_ref & result);

2
src/ast/simplifier/simplifier_plugin.h
View file

@ -37,7 +37,7 @@ protected:
void set_reduce_invoked() { m_reduce_invoked = true; }
public:
simplifier_plugin(symbol const & fname, ast_manager & m):m_manager(m), m_fid(m.get_family_id(fname)), m_presimp(false), m_reduce_invoked(false) {}
simplifier_plugin(symbol const & fname, ast_manager & m):m_manager(m), m_fid(m.mk_family_id(fname)), m_presimp(false), m_reduce_invoked(false) {}
bool reduce_invoked() const { return m_reduce_invoked; }

4
src/ast/static_features.cpp
View file

@ -23,8 +23,8 @@ static_features::static_features(ast_manager & m):
m_manager(m),
m_autil(m),
m_bfid(m.get_basic_family_id()),
m_afid(m.get_family_id("arith")),
m_lfid(m.get_family_id("label")),
m_afid(m.mk_family_id("arith")),
m_lfid(m.mk_family_id("label")),
m_label_sym("label"),
m_pattern_sym("pattern"),
m_expr_list_sym("expr-list") {

2
src/cmd_context/basic_cmds.cpp
View file

@ -643,7 +643,7 @@ public:
family_id get_array_fid(cmd_context & ctx) {
if (m_array_fid == null_family_id) {
m_array_fid = ctx.m().get_family_id("array");
m_array_fid = ctx.m().mk_family_id("array");
}
return m_array_fid;
}

30
src/cmd_context/cmd_context.cpp
View file

@ -343,6 +343,13 @@ cmd_context::~cmd_context() {
m_check_sat_result = 0;
}
void cmd_context::set_cancel(bool f) {
if (m_solver)
m_solver->set_cancel(f);
if (has_manager())
m().set_cancel(f);
}
void cmd_context::global_params_updated() {
m_params.updt_params();
if (m_solver) {
@ -582,8 +589,8 @@ void cmd_context::init_manager_core(bool new_manager) {
// it prevents clashes with builtin types.
insert(pm().mk_plist_decl());
}
if (m_solver) {
init_solver_options(m_solver.get());
if (m_solver_factory) {
mk_solver();
}
m_check_logic.set_logic(m(), m_logic);
}
@ -1119,7 +1126,7 @@ void cmd_context::reset(bool finalize) {
reset_func_decls();
restore_assertions(0);
if (m_solver)
m_solver->reset();
m_solver = 0;
m_pp_env = 0;
m_dt_eh = 0;
if (m_manager) {
@ -1379,7 +1386,7 @@ void cmd_context::set_diagnostic_stream(char const * name) {
struct contains_array_op_proc {
struct found {};
family_id m_array_fid;
contains_array_op_proc(ast_manager & m):m_array_fid(m.get_family_id("array")) {}
contains_array_op_proc(ast_manager & m):m_array_fid(m.mk_family_id("array")) {}
void operator()(var * n) {}
void operator()(app * n) {
if (n->get_family_id() != m_array_fid)
@ -1441,17 +1448,18 @@ void cmd_context::validate_model() {
}
}
void cmd_context::init_solver_options(solver * s) {
void cmd_context::mk_solver() {
bool proofs_enabled, models_enabled, unsat_core_enabled;
params_ref p;
m_params.init_solver_params(m(), *m_solver, p);
m_solver->init(m(), m_logic);
m_params.get_solver_params(m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
}
void cmd_context::set_solver(solver * s) {
void cmd_context::set_solver_factory(solver_factory * f) {
m_solver_factory = f;
m_check_sat_result = 0;
m_solver = s;
if (has_manager() && s != 0) {
init_solver_options(s);
if (has_manager() && f != 0) {
mk_solver();
// assert formulas and create scopes in the new solver.
unsigned lim = 0;
svector<scope>::iterator it = m_scopes.begin();

9
src/cmd_context/cmd_context.h
View file

@ -185,6 +185,7 @@ protected:
};
svector<scope> m_scopes;
scoped_ptr<solver_factory> m_solver_factory;
ref<solver> m_solver;
ref<check_sat_result> m_check_sat_result;
@ -243,11 +244,14 @@ protected:
void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;}
void init_solver_options(solver * s);
void mk_solver();
public:
cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
~cmd_context();
void set_cancel(bool f);
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
context_params & params() { return m_params; }
void global_params_updated(); // this method should be invoked when global (and module) params are updated.
void set_logic(symbol const & s);
@ -289,8 +293,7 @@ public:
pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
void set_solver(solver * s);
solver * get_solver() const { return m_solver.get(); }
void set_solver_factory(solver_factory * s);
void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
check_sat_state cs_state() const;

10
src/cmd_context/context_params.cpp
View file

@ -131,11 +131,11 @@ params_ref context_params::merge_default_params(params_ref const & p) {
}
}
void context_params::init_solver_params(ast_manager & m, solver & s, params_ref const & p) {
s.set_produce_proofs(m.proofs_enabled() && m_proof);
s.set_produce_models(p.get_bool("model", m_model));
s.set_produce_unsat_cores(p.get_bool("unsat_core", m_unsat_core));
s.updt_params(merge_default_params(p));
void context_params::get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) {
proofs_enabled = m.proofs_enabled() && p.get_bool("proof", m_proof);
models_enabled = p.get_bool("model", m_model);
unsat_core_enabled = p.get_bool("unsat_core", m_unsat_core);
p = merge_default_params(p);
}
ast_manager * context_params::mk_ast_manager() {

9
src/cmd_context/context_params.h
View file

@ -22,7 +22,6 @@ Notes:
#include"params.h"
class ast_manager;
class solver;
class context_params {
void set_bool(bool & opt, char const * param, char const * value);
@ -50,13 +49,9 @@ public:
*/
/**
\brief Goodie for updating the solver params
based on the configuration of the context_params object.
This method is used when creating solvers from the
cmd_context and API.
\brief Goodies for extracting parameters for creating a solver object.
*/
void init_solver_params(ast_manager & m, solver & s, params_ref const & p);
void get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled);
/**
\brief Include in p parameters derived from this context_params.

2
src/cmd_context/pdecl.cpp
View file

@ -765,7 +765,7 @@ pdecl_manager::pdecl_manager(ast_manager & m):
m_allocator(m.get_allocator()),
m_new_dt_eh(0) {
m_list = 0;
m_datatype_fid = m.get_family_id("datatype");
m_datatype_fid = m.mk_family_id("datatype");
}
pdecl_manager::~pdecl_manager() {

42
src/math/polynomial/algebraic_numbers.cpp
View file

@ -2796,72 +2796,58 @@ namespace algebraic_numbers {
}
void manager::del(numeral & a) {
set_cancel(false);
return m_imp->del(a);
}
void manager::reset(numeral & a) {
set_cancel(false);
return m_imp->reset(a);
}
bool manager::is_zero(numeral const & a) {
set_cancel(false);
return m_imp->is_zero(const_cast<numeral&>(a));
}
bool manager::is_pos(numeral const & a) {
set_cancel(false);
return m_imp->is_pos(const_cast<numeral&>(a));
}
bool manager::is_neg(numeral const & a) {
set_cancel(false);
return m_imp->is_neg(const_cast<numeral&>(a));
}
bool manager::is_rational(numeral const & a) {
set_cancel(false);
return m_imp->is_rational(const_cast<numeral&>(a));
}
bool manager::is_int(numeral const & a) {
set_cancel(false);
return m_imp->is_int(const_cast<numeral&>(a));
}
unsigned manager::degree(numeral const & a) {
set_cancel(false);
return m_imp->degree(const_cast<numeral&>(a));
}
void manager::to_rational(numeral const & a, mpq & r) {
set_cancel(false);
return m_imp->to_rational(const_cast<numeral&>(a), r);
}
void manager::to_rational(numeral const & a, rational & r) {
set_cancel(false);
return m_imp->to_rational(const_cast<numeral&>(a), r);
}
void manager::swap(numeral & a, numeral & b) {
set_cancel(false);
return m_imp->swap(a, b);
}
void manager::int_lt(numeral const & a, numeral & b) {
set_cancel(false);
m_imp->int_lt(const_cast<numeral&>(a), b);
}
void manager::int_gt(numeral const & a, numeral & b) {
set_cancel(false);
m_imp->int_gt(const_cast<numeral&>(a), b);
}
void manager::select(numeral const & prev, numeral const & curr, numeral & result) {
set_cancel(false);
m_imp->select(const_cast<numeral&>(prev), const_cast<numeral&>(curr), result);
}
@ -2878,55 +2864,45 @@ namespace algebraic_numbers {
}
void manager::set(numeral & a, mpq const & n) {
set_cancel(false);
m_imp->set(a, n);
}
void manager::set(numeral & a, numeral const & n) {
set_cancel(false);
m_imp->set(a, n);
}
void manager::isolate_roots(polynomial_ref const & p, numeral_vector & roots) {
set_cancel(false);
m_imp->isolate_roots(p, roots);
}
void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots) {
set_cancel(false);
m_imp->isolate_roots(p, x2v, roots);
}
void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<int> & signs) {
set_cancel(false);
m_imp->isolate_roots(p, x2v, roots, signs);
}
void manager::mk_root(polynomial_ref const & p, unsigned i, numeral & r) {
set_cancel(false);
m_imp->mk_root(p, i, r);
}
void manager::mk_root(sexpr const * p, unsigned i, numeral & r) {
set_cancel(false);
m_imp->mk_root(p, i, r);
}
void manager::root(numeral const & a, unsigned k, numeral & b) {
set_cancel(false);
m_imp->root(const_cast<numeral&>(a), k, b);
}
void manager::power(numeral const & a, unsigned k, numeral & b) {
TRACE("anum_detail", display_root(tout, a); tout << "^" << k << "\n";);
set_cancel(false);
m_imp->power(const_cast<numeral&>(a), k, b);
TRACE("anum_detail", tout << "^ result: "; display_root(tout, b); tout << "\n";);
}
void manager::add(numeral const & a, numeral const & b, numeral & c) {
TRACE("anum_detail", display_root(tout, a); tout << " + "; display_root(tout, b); tout << "\n";);
set_cancel(false);
m_imp->add(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
TRACE("anum_detail", tout << "+ result: "; display_root(tout, c); tout << "\n";);
}
@ -2939,45 +2915,37 @@ namespace algebraic_numbers {
void manager::sub(numeral const & a, numeral const & b, numeral & c) {
TRACE("anum_detail", display_root(tout, a); tout << " - "; display_root(tout, b); tout << "\n";);
set_cancel(false);
m_imp->sub(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
TRACE("anum_detail", tout << "- result: "; display_root(tout, c); tout << "\n";);
}
void manager::mul(numeral const & a, numeral const & b, numeral & c) {
TRACE("anum_detail", display_root(tout, a); tout << " * "; display_root(tout, b); tout << "\n";);
set_cancel(false);
m_imp->mul(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
TRACE("anum_detail", tout << "* result: "; display_root(tout, c); tout << "\n";);
}
void manager::div(numeral const & a, numeral const & b, numeral & c) {
set_cancel(false);
m_imp->div(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
}
void manager::neg(numeral & a) {
set_cancel(false);
m_imp->neg(a);
}
void manager::inv(numeral & a) {
set_cancel(false);
m_imp->inv(a);
}
int manager::compare(numeral const & a, numeral const & b) {
set_cancel(false);
return m_imp->compare(const_cast<numeral&>(a), const_cast<numeral&>(b));
}
bool manager::eq(numeral const & a, numeral const & b) {
set_cancel(false);
return m_imp->eq(const_cast<numeral&>(a), const_cast<numeral&>(b));
}
bool manager::eq(numeral const & a, mpq const & b) {
set_cancel(false);
return m_imp->eq(const_cast<numeral&>(a), b);
}
@ -2988,12 +2956,10 @@ namespace algebraic_numbers {
}
bool manager::lt(numeral const & a, numeral const & b) {
set_cancel(false);
return m_imp->lt(const_cast<numeral&>(a), const_cast<numeral&>(b));
}
bool manager::lt(numeral const & a, mpq const & b) {
set_cancel(false);
return m_imp->lt(const_cast<numeral&>(a), b);
}
@ -3004,7 +2970,6 @@ namespace algebraic_numbers {
}
bool manager::gt(numeral const & a, mpq const & b) {
set_cancel(false);
return m_imp->gt(const_cast<numeral&>(a), b);
}
@ -3073,38 +3038,31 @@ namespace algebraic_numbers {
}
int manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
set_cancel(false);
SASSERT(&(x2v.m()) == this);
return m_imp->eval_sign_at(p, x2v);
}
void manager::display_interval(std::ostream & out, numeral const & a) const {
const_cast<manager*>(this)->set_cancel(false);
m_imp->display_interval(out, a);
}
void manager::display_decimal(std::ostream & out, numeral const & a, unsigned precision) const {
const_cast<manager*>(this)->set_cancel(false);
m_imp->display_decimal(out, a, precision);
}
void manager::display_root(std::ostream & out, numeral const & a) const {
const_cast<manager*>(this)->set_cancel(false);
m_imp->display_root(out, a);
}
void manager::display_mathematica(std::ostream & out, numeral const & a) const {
const_cast<manager*>(this)->set_cancel(false);
m_imp->display_mathematica(out, a);
}
void manager::display_root_smt2(std::ostream & out, numeral const & a) const {
const_cast<manager*>(this)->set_cancel(false);
m_imp->display_root_smt2(out, a);
}
void manager::reset_statistics() {
set_cancel(false);
m_imp->reset_statistics();
}

2
src/math/polynomial/algebraic_numbers.h
View file

@ -64,8 +64,8 @@ namespace algebraic_numbers {
static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
void set_cancel(bool f);
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
void updt_params(params_ref const & p);

1
src/math/polynomial/polynomial.cpp
View file

@ -2368,7 +2368,6 @@ namespace polynomial {
void checkpoint() {
if (m_cancel) {
set_cancel(false);
throw polynomial_exception("canceled");
}
cooperate("polynomial");

1
src/math/polynomial/polynomial.h
View file

@ -220,6 +220,7 @@ namespace polynomial {
void set_cancel(bool f);
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
/**
\brief Abstract event handler.

2
src/math/polynomial/polynomial_factorization.cpp
View file

@ -16,7 +16,7 @@ Author:
Notes:
[1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal,
46(8-10):1853<EFBFBD>1859, 1967.
46(8-10):1853-1859, 1967.
[2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third
edition, 1997.
[3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993.

2
src/math/polynomial/polynomial_factorization.h
View file

@ -16,7 +16,7 @@ Author:
Notes:
[1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal,
46(8-10):1853<EFBFBD>1859, 1967.
46(8-10):1853-1859, 1967.
[2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third
edition, 1997.
[3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993.

2
src/math/polynomial/upolynomial_factorization.cpp
View file

@ -16,7 +16,7 @@ Author:
Notes:
[1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal,
46(8-10):1853<EFBFBD>1859, 1967.
46(8-10):1853-1859, 1967.
[2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third
edition, 1997.
[3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993.

2
src/math/polynomial/upolynomial_factorization.h
View file

@ -16,7 +16,7 @@ Author:
Notes:
[1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal,
46(8-10):1853<EFBFBD>1859, 1967.
46(8-10):1853-1859, 1967.
[2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third
edition, 1997.
[3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993.

2
src/math/polynomial/upolynomial_factorization_int.h
View file

@ -17,7 +17,7 @@ Author:
Notes:
[1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal,
46(8-10):1853<EFBFBD>1859, 1967.
46(8-10):1853-1859, 1967.
[2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third
edition, 1997.
[3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993.

4
src/model/model_evaluator.cpp
View file

@ -244,10 +244,10 @@ unsigned model_evaluator::get_num_steps() const {
return m_imp->get_num_steps();
}
void model_evaluator::cancel() {
void model_evaluator::set_cancel(bool f) {
#pragma omp critical (model_evaluator)
{
m_imp->cancel();
m_imp->set_cancel(f);
}
}

4
src/model/model_evaluator.h
View file

@ -41,7 +41,9 @@ public:
void operator()(expr * t, expr_ref & r);
void cancel();
void set_cancel(bool f);
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
void cleanup(params_ref const & p = params_ref());
void reset(params_ref const & p = params_ref());

2
src/muz_qe/dl_bmc_engine.cpp
View file

@ -963,7 +963,7 @@ namespace datalog {
sort_ref_vector new_sorts(m);
family_id dfid = m.get_family_id("datatype");
family_id dfid = m.mk_family_id("datatype");
datatype_decl_plugin* dtp = static_cast<datatype_decl_plugin*>(m.get_plugin(dfid));
VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts));

2
src/muz_qe/dl_cmds.cpp
View file

@ -75,7 +75,7 @@ struct dl_context {
if (!m_decl_plugin) {
symbol name("datalog_relation");
if (m.has_plugin(name)) {
m_decl_plugin = static_cast<datalog::dl_decl_plugin*>(m_cmd.m().get_plugin(m.get_family_id(name)));
m_decl_plugin = static_cast<datalog::dl_decl_plugin*>(m_cmd.m().get_plugin(m.mk_family_id(name)));
}
else {
m_decl_plugin = alloc(datalog::dl_decl_plugin);

1
src/muz_qe/dl_context.h
View file

@ -349,6 +349,7 @@ namespace datalog {
void cancel();
void cleanup();
void reset_cancel() { cleanup(); }
/**
\brief check if query 'q' is satisfied under asserted rules and background.

2
src/muz_qe/dl_mk_extract_quantifiers2.cpp
View file

@ -332,7 +332,7 @@ namespace datalog {
smt::quantifier_manager* qm = ctx.get_quantifier_manager();
qm->get_plugin()->set_instance_plugin(alloc(instance_plugin, *this));
#endif
lbool res = solver.check();
solver.check();
for (unsigned i = 0; i < m_bindings.size(); ++i) {
expr_ref_vector& binding = m_bindings[i];

6
src/muz_qe/dl_relation_manager.h
View file

@ -3,7 +3,7 @@ Copyright (c) 2006 Microsoft Corporation
Module Name:
dl_remation_manager.h
dl_relation_manager.h
Abstract:
@ -316,7 +316,7 @@ namespace datalog {
oldTgt:=tgt.clone();
tgt:=tgt \union src
if(tgt!=oldTgt) {
delta:=delta \union src //also “delta \union tgt” would work
delta:=delta \union src //also ?delta \union tgt? would work
}
}
@ -488,7 +488,7 @@ namespace datalog {
oldTgt:=tgt.clone();
tgt:=tgt \union src
if(tgt!=oldTgt) {
delta:=delta \union src //also “delta \union tgt” would work
delta:=delta \union src //also ?delta \union tgt? would work
}
}

2
src/muz_qe/dl_rule.cpp
View file

@ -74,7 +74,7 @@ namespace datalog {
class remove_label_cfg : public default_rewriter_cfg {
family_id m_label_fid;
public:
remove_label_cfg(ast_manager& m): m_label_fid(m.get_family_id("label")) {}
remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
virtual ~remove_label_cfg() {}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,

6
src/muz_qe/pdr_util.cpp
View file

@ -1129,7 +1129,11 @@ namespace pdr {
if (a.is_numeral(lhs) || a.is_numeral(rhs)) {
return test_ineq(e);
}
return test_term(lhs) && test_term(rhs);
return
test_term(lhs) &&
test_term(rhs) &&
!a.is_mul(lhs) &&
!a.is_mul(rhs);
}
bool test_term(expr* e) const {

7
src/muz_qe/proof_utils.cpp
View file

@ -312,9 +312,10 @@ public:
};
void proof_utils::reduce_hypotheses(proof_ref& pr) {
class reduce_hypotheses reduce(pr.get_manager());
ast_manager& m = pr.get_manager();
class reduce_hypotheses reduce(m);
reduce(pr);
SASSERT(is_closed(pr.get_manager(), pr));
CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
}
class proof_is_closed {
@ -449,7 +450,7 @@ static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>
parameter const* params = thLemma->get_decl()->get_parameters();
unsigned num_params = thLemma->get_decl()->get_num_parameters();
SASSERT(params[0].is_symbol());
family_id tid = m.get_family_id(params[0].get_symbol());
family_id tid = m.mk_family_id(params[0].get_symbol());
SASSERT(tid != null_family_id);
prNew = m.mk_th_lemma(tid, m.get_fact(pr),
premises.size(), premises.c_ptr(), num_params-1, params+1);

4
src/muz_qe/qe_arith_plugin.cpp
View file

@ -1512,7 +1512,7 @@ public:
public:
arith_plugin(i_solver_context& ctx, ast_manager& m, smt_params& p):
qe_solver_plugin(m, m.get_family_id("arith"), ctx),
qe_solver_plugin(m, m.mk_family_id("arith"), ctx),
m_util(m, p, ctx),
m_trail(m)
{}
@ -2403,7 +2403,7 @@ public:
bool m_produce_models;
public:
nlarith_plugin(i_solver_context& ctx, ast_manager& m, bool produce_models) :
qe_solver_plugin(m, m.get_family_id("arith"), ctx),
qe_solver_plugin(m, m.mk_family_id("arith"), ctx),
m_rewriter(m),
m_util(m),
m_replacer(mk_default_expr_replacer(m)),

2
src/muz_qe/qe_array_plugin.cpp
View file

@ -16,7 +16,7 @@ namespace qe {
public:
array_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.get_family_id("array"), ctx),
qe_solver_plugin(m, m.mk_family_id("array"), ctx),
m_replace(mk_default_expr_replacer(m))
{
}

2
src/muz_qe/qe_bv_plugin.cpp
View file

@ -32,7 +32,7 @@ namespace qe {
bv_util m_bv;
public:
bv_plugin(i_solver_context& ctx, ast_manager& m):
qe_solver_plugin(m, m.get_family_id("bv"), ctx),
qe_solver_plugin(m, m.mk_family_id("bv"), ctx),
m_replace(mk_default_expr_replacer(m)),
m_bv(m)
{}

2
src/muz_qe/qe_datatype_plugin.cpp
View file

@ -422,7 +422,7 @@ namespace qe {
public:
datatype_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.get_family_id("datatype"), ctx),
qe_solver_plugin(m, m.mk_family_id("datatype"), ctx),
m_datatype_util(m),
m_replace(mk_default_expr_replacer(m)),
m_trail(m)

2
src/muz_qe/qe_dl_plugin.cpp
View file

@ -45,7 +45,7 @@ namespace qe {
public:
dl_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.get_family_id("datalog_relation"), ctx),
qe_solver_plugin(m, m.mk_family_id("datalog_relation"), ctx),
m_replace(mk_default_expr_replacer(m)),
m_util(m),
m_trail(m)

259
src/muz_qe/qe_lite.cpp
View file

@ -35,7 +35,7 @@ Revision History:
#include "dl_util.h"
#include "for_each_expr.h"
#include "expr_safe_replace.h"
#include "cooperate.h"
class is_variable_proc {
public:
@ -91,6 +91,7 @@ namespace eq {
expr_ref_vector m_subst_map;
expr_ref_buffer m_new_args;
th_rewriter m_rewriter;
volatile bool m_cancel;
void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
order.reset();
@ -530,6 +531,7 @@ namespace eq {
// Find all definitions
for (unsigned i = 0; i < num_args; i++) {
checkpoint();
if (is_var_def(is_exists, args[i], v, t)) {
unsigned idx = v->get_idx();
if(m_map.get(idx, 0) == 0) {
@ -569,8 +571,14 @@ namespace eq {
return false;
}
void checkpoint() {
cooperate("der");
if (m_cancel)
throw tactic_exception(TACTIC_CANCELED_MSG);
}
public:
der(ast_manager & m): m(m), a(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m) {}
der(ast_manager & m): m(m), a(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m), m_cancel(false) {}
void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
@ -588,6 +596,7 @@ namespace eq {
r = q;
// Keep applying reduce_quantifier1 until r doesn't change anymore
do {
checkpoint();
proof_ref curr_pr(m);
q = to_quantifier(r);
reduce_quantifier1(q, r, curr_pr);
@ -605,6 +614,12 @@ namespace eq {
}
ast_manager& get_manager() const { return m; }
void set_cancel(bool f) {
m_rewriter.set_cancel(f);
m_cancel = f;
}
};
}; // namespace eq
@ -618,6 +633,7 @@ namespace ar {
is_variable_proc* m_is_variable;
ptr_vector<expr> m_todo;
expr_mark m_visited;
volatile bool m_cancel;
bool is_variable(expr * e) const {
return (*m_is_variable)(e);
@ -723,13 +739,19 @@ namespace ar {
return false;
}
void checkpoint() {
cooperate("der");
if (m_cancel)
throw tactic_exception(TACTIC_CANCELED_MSG);
}
public:
der(ast_manager& m): m(m), a(m), m_is_variable(0) {}
der(ast_manager& m): m(m), a(m), m_is_variable(0), m_cancel(false) {}
void operator()(expr_ref_vector& fmls) {
for (unsigned i = 0; i < fmls.size(); ++i) {
checkpoint();
solve_select(fmls, i, fmls[i].get());
solve_neq_select(fmls, i, fmls[i].get());
}
@ -738,6 +760,10 @@ namespace ar {
void operator()(expr* e) {}
void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
void set_cancel(bool f) {
m_cancel = f;
}
};
}; // namespace ar
@ -866,7 +892,6 @@ namespace fm {
unsigned m_fm_cutoff2;
unsigned m_fm_extra;
bool m_fm_occ;
unsigned long long m_max_memory;
unsigned m_counter;
bool m_inconsistent;
expr_dependency_ref m_inconsistent_core;
@ -1243,7 +1268,7 @@ namespace fm {
//
// ---------------------------
fm(ast_manager & _m, params_ref const & p):
fm(ast_manager & _m):
m(_m),
m_allocator("fm-elim"),
m_util(m),
@ -1251,7 +1276,6 @@ namespace fm {
m_var2expr(m),
m_new_fmls(m),
m_inconsistent_core(m) {
updt_params(p);
m_cancel = false;
}
@ -1259,14 +1283,13 @@ namespace fm {
reset_constraints();
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_fm_real_only = p.get_bool("fm_real_only", true);
m_fm_limit = p.get_uint("fm_limit", 5000000);
m_fm_cutoff1 = p.get_uint("fm_cutoff1", 8);
m_fm_cutoff2 = p.get_uint("fm_cutoff2", 256);
m_fm_extra = p.get_uint("fm_extra", 0);
m_fm_occ = p.get_bool("fm_occ", false);
void updt_params() {
m_fm_real_only = true;
m_fm_limit = 5000000;
m_fm_cutoff1 = 8;
m_fm_cutoff2 = 256;
m_fm_extra = 0;
m_fm_occ = false;
}
void set_cancel(bool f) {
@ -2010,11 +2033,9 @@ namespace fm {
}
void checkpoint() {
// cooperate("fm");
cooperate("fm");
if (m_cancel)
throw tactic_exception(TACTIC_CANCELED_MSG);
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
}
public:
@ -2083,11 +2104,56 @@ namespace fm {
} // namespace fm
class qe_lite::impl {
public:
struct elim_cfg : public default_rewriter_cfg {
impl& m_imp;
ast_manager& m;
public:
elim_cfg(impl& i): m_imp(i), m(i.m) {}
bool reduce_quantifier(quantifier * q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
result = new_body;
if (is_forall(q)) {
result = m.mk_not(result);
}
uint_set indices;
for (unsigned i = 0; i < q->get_num_decls(); ++i) {
indices.insert(i);
}
m_imp(indices, true, result);
if (is_forall(q)) {
result = m.mk_not(result);
}
result = m.update_quantifier(
q,
q->get_num_patterns(), new_patterns,
q->get_num_no_patterns(), new_no_patterns, result);
m_imp.m_rewriter(result);
return true;
}
};
class elim_star : public rewriter_tpl<elim_cfg> {
elim_cfg m_cfg;
public:
elim_star(impl& i):
rewriter_tpl<elim_cfg>(i.m, false, m_cfg),
m_cfg(i)
{}
};
private:
ast_manager& m;
params_ref m_params;
eq::der m_der;
fm::fm m_fm;
ar::der m_array_der;
elim_star m_elim_star;
th_rewriter m_rewriter;
bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) {
index = fmls.size();
@ -2106,7 +2172,13 @@ class qe_lite::impl {
}
public:
impl(ast_manager& m): m(m), m_der(m), m_fm(m, m_params), m_array_der(m) {}
impl(ast_manager& m):
m(m),
m_der(m),
m_fm(m),
m_array_der(m),
m_elim_star(*this),
m_rewriter(m) {}
void operator()(app_ref_vector& vars, expr_ref& fml) {
if (vars.empty()) {
@ -2145,14 +2217,12 @@ public:
else {
fml = tmp;
}
}
}
void operator()(expr_ref& fml, proof_ref& pr) {
// TODO apply der everywhere as a rewriting rule.
// TODO add cancel method.
if (is_quantifier(fml)) {
m_der(to_quantifier(fml), fml, pr);
}
expr_ref tmp(m);
m_elim_star(fml, tmp, pr);
fml = tmp;
}
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
@ -2195,6 +2265,14 @@ public:
TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
}
void set_cancel(bool f) {
m_der.set_cancel(f);
m_array_der.set_cancel(f);
m_fm.set_cancel(f);
m_elim_star.set_cancel(f);
m_rewriter.set_cancel(f);
}
};
qe_lite::qe_lite(ast_manager& m) {
@ -2209,6 +2287,10 @@ void qe_lite::operator()(app_ref_vector& vars, expr_ref& fml) {
(*m_impl)(vars, fml);
}
void qe_lite::set_cancel(bool f) {
m_impl->set_cancel(f);
}
void qe_lite::operator()(expr_ref& fml, proof_ref& pr) {
(*m_impl)(fml, pr);
}
@ -2220,3 +2302,130 @@ void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_re
void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) {
(*m_impl)(index_set, index_of_bound, fmls);
}
class qe_lite_tactic : public tactic {
struct imp {
ast_manager& m;
qe_lite m_qe;
volatile bool m_cancel;
imp(ast_manager& m, params_ref const& p):
m(m),
m_qe(m),
m_cancel(false)
{}
void set_cancel(bool f) {
m_cancel = f;
m_qe.set_cancel(f);
}
void checkpoint() {
if (m_cancel)
throw tactic_exception(TACTIC_CANCELED_MSG);
cooperate("qe-lite");
}
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
tactic_report report("qe-lite", *g);
proof_ref new_pr(m);
expr_ref new_f(m);
bool produce_proofs = g->proofs_enabled();
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
checkpoint();
if (g->inconsistent())
break;
expr * f = g->form(i);
if (!has_quantifiers(f))
continue;
new_f = f;
m_qe(new_f, new_pr);
if (produce_proofs) {
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
}
g->update(i, new_f, new_pr, g->dep(i));
}
g->inc_depth();
result.push_back(g.get());
TRACE("qe", g->display(tout););
SASSERT(g->is_well_sorted());
}
};
params_ref m_params;
imp * m_imp;
public:
qe_lite_tactic(ast_manager & m, params_ref const & p):
m_params(p) {
m_imp = alloc(imp, m, p);
}
virtual tactic * translate(ast_manager & m) {
return alloc(qe_lite_tactic, m, m_params);
}
virtual ~qe_lite_tactic() {
dealloc(m_imp);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
// m_imp->updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {
// m_imp->collect_param_descrs(r);
}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
}
virtual void collect_statistics(statistics & st) const {
// m_imp->collect_statistics(st);
}
virtual void reset_statistics() {
// m_imp->reset_statistics();
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
};
tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
return alloc(qe_lite_tactic, m, p);
}
template class rewriter_tpl<qe_lite::impl::elim_cfg>;

10
src/muz_qe/qe_lite.h
View file

@ -23,6 +23,9 @@ Revision History:
#include "ast.h"
#include "uint_set.h"
#include "params.h"
class tactic;
class qe_lite {
class impl;
@ -56,6 +59,13 @@ public:
\brief full rewriting based light-weight quantifier elimination round.
*/
void operator()(expr_ref& fml, proof_ref& pr);
void set_cancel(bool f);
};
tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)")
*/
#endif

37
src/nlsat/nlsat_explain.cpp
View file

@ -981,6 +981,14 @@ namespace nlsat {
bool atom_val = a->get_kind() == atom::EQ;
bool lit_val = l.sign() ? !atom_val : atom_val;
new_lit = lit_val ? true_literal : false_literal;
if (!info.m_lc_const) {
// We have essentially shown the current factor must be zero If the leading coefficient is not zero.
// Note that, if the current factor is zero, then the whole polynomial is zero.
// The atom is true if it is an equality, and false otherwise.
// The sign of the leading coefficient (info.m_lc) of info.m_eq doesn't matter.
// However, we have to store the fact it is not zero.
info.add_lc_diseq();
}
return;
}
else if (s == -1 && !is_even) {
@ -1341,3 +1349,32 @@ namespace nlsat {
}
};
#ifdef Z3DEBUG
void pp(nlsat::explain::imp & ex, unsigned num, nlsat::literal const * ls) {
ex.display(std::cout, num, ls);
}
void pp(nlsat::explain::imp & ex, nlsat::scoped_literal_vector & ls) {
ex.display(std::cout, ls);
}
void pp(nlsat::explain::imp & ex, polynomial_ref const & p) {
ex.display(std::cout, p);
std::cout << std::endl;
}
void pp(nlsat::explain::imp & ex, polynomial::polynomial * p) {
polynomial_ref _p(p, ex.m_pm);
ex.display(std::cout, _p);
std::cout << std::endl;
}
void pp(nlsat::explain::imp & ex, polynomial_ref_vector const & ps) {
ex.display(std::cout, ps);
}
void pp_var(nlsat::explain::imp & ex, nlsat::var x) {
ex.display(std::cout, x);
std::cout << std::endl;
}
void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
ex.display(std::cout, l);
std::cout << std::endl;
}
#endif

2
src/nlsat/nlsat_explain.h
View file

@ -27,7 +27,9 @@ namespace nlsat {
class evaluator;
class explain {
public:
struct imp;
private:
imp * m_imp;
public:
explain(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,

2
src/parsers/smt/smtlib_solver.cpp
View file

@ -86,7 +86,7 @@ namespace smtlib {
benchmark.add_formula(m_ast_manager.mk_true());
}
m_ctx = alloc(cmd_context, true, &m_ast_manager, benchmark.get_logic());
m_ctx->set_solver(mk_smt_strategic_solver(false));
m_ctx->set_solver_factory(mk_smt_strategic_solver_factory());
theory::expr_iterator fit = benchmark.begin_formulas();
theory::expr_iterator fend = benchmark.end_formulas();
for (; fit != fend; ++fit)

12
src/parsers/smt/smtparser.cpp
View file

@ -483,13 +483,13 @@ public:
class array_sort : public builtin_sort_builder {
public:
array_sort(ast_manager& m) :
builtin_sort_builder(m, m.get_family_id("array"), ARRAY_SORT) {}
builtin_sort_builder(m, m.mk_family_id("array"), ARRAY_SORT) {}
};
class bv_sort : public builtin_sort_builder {
public:
bv_sort(ast_manager& m) :
builtin_sort_builder(m, m.get_family_id("bv"), BV_SORT) {}
builtin_sort_builder(m, m.mk_family_id("bv"), BV_SORT) {}
};
class user_sort : public sort_builder {
@ -538,7 +538,7 @@ class smtparser : public parser {
public:
add_plugins(ast_manager& m) {
#define REGISTER_PLUGIN(NAME, MK) { \
family_id fid = m.get_family_id(symbol(NAME)); \
family_id fid = m.mk_family_id(symbol(NAME)); \
if (!m.has_plugin(fid)) { \
m.register_plugin(fid, MK); \
} \
@ -681,7 +681,7 @@ public:
smtlib::symtable* table = m_benchmark.get_symtable();
symbol arith("arith");
family_id afid = m_manager.get_family_id(arith);
family_id afid = m_manager.mk_family_id(arith);
m_arith_fid = afid;
add_builtin_type("Int", afid, INT_SORT);
@ -694,7 +694,7 @@ public:
add_builtins(afid);
symbol bv("bv");
family_id bfid = m_manager.get_family_id(bv);
family_id bfid = m_manager.mk_family_id(bv);
m_bv_fid = bfid;
add_builtins(bfid);
@ -702,7 +702,7 @@ public:
add_builtin_type("BitVec", bfid, BV_SORT);
symbol array("array");
afid = m_manager.get_family_id(array);
afid = m_manager.mk_family_id(array);
m_array_fid = afid;
add_builtins(afid);

1
src/parsers/smt2/smt2parser.cpp
View file

@ -390,6 +390,7 @@ namespace smt2 {
void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
void error(unsigned line, unsigned pos, char const * msg) {
m_ctx.reset_cancel();
if (use_vs_format()) {
m_ctx.diagnostic_stream() << "Z3(" << line << ", " << pos << "): ERROR: " << msg;
if (msg[strlen(msg)-1] != '\n')

3
src/parsers/util/pattern_validation.h
View file

@ -32,11 +32,10 @@ class pattern_validator {
public:
pattern_validator(ast_manager const & m):
m_bfid(m.get_basic_family_id()),
m_lfid(m.get_family_id("label")) {
m_lfid(m.get_label_family_id()) {
}
bool operator()(unsigned num_bindings, unsigned num_new_bindings, expr * n);
bool operator()(unsigned num_new_bindings, expr * n) { return operator()(UINT_MAX, num_new_bindings, n); }
};

6
src/shell/smtlib_frontend.cpp
View file

@ -30,9 +30,6 @@ Revision History:
#include"subpaving_cmds.h"
#include"smt_strategic_solver.h"
#include"tactic2solver.h"
#include"qfnra_nlsat_tactic.h"
extern bool g_display_statistics;
extern void display_config();
static clock_t g_start_time;
@ -98,8 +95,7 @@ unsigned read_smtlib2_commands(char const * file_name) {
signal(SIGINT, on_ctrl_c);
cmd_context ctx;
solver * s = mk_smt_strategic_solver(false);
ctx.set_solver(s);
ctx.set_solver_factory(mk_smt_strategic_solver_factory());
install_dl_cmds(ctx);
install_dbg_cmds(ctx);

11
src/smt/asserted_formulas.cpp
View file

@ -189,7 +189,7 @@ void asserted_formulas::push_scope() {
s.m_asserted_formulas_lim = m_asserted_formulas.size();
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead);
s.m_inconsistent_old = m_inconsistent;
m_defined_names.push_scope();
m_defined_names.push();
m_bv_sharing.push_scope();
commit();
}
@ -201,7 +201,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) {
unsigned new_lvl = m_scopes.size() - num_scopes;
scope & s = m_scopes[new_lvl];
m_inconsistent = s.m_inconsistent_old;
m_defined_names.pop_scope(num_scopes);
m_defined_names.pop(num_scopes);
m_asserted_formulas.shrink(s.m_asserted_formulas_lim);
if (m_manager.proofs_enabled())
m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim);
@ -439,6 +439,8 @@ void asserted_formulas::nnf_cnf() {
expr_ref r1(m_manager);
proof_ref pr1(m_manager);
CASSERT("well_sorted",is_well_sorted(m_manager, n));
push_todo.reset();
push_todo_prs.reset();
apply_nnf(n, push_todo, push_todo_prs, r1, pr1);
CASSERT("well_sorted",is_well_sorted(m_manager, r1));
pr = m_manager.mk_modus_ponens(pr, pr1);
@ -855,3 +857,8 @@ void asserted_formulas::max_bv_sharing() {
}
#ifdef Z3DEBUG
void pp(asserted_formulas & f) {
f.display(std::cout);
}
#endif

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