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

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-12-26 11:31:09 -08:00
parent bc77a97e92 2a286541e0
commit 8b8fb74fd6
111 changed files with 1263 additions and 1079 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
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.
@ -30,7 +32,7 @@ Version 4.3.2
- 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)
- Fixed bug when using assumptions (Thanks to Philippe Suter and Etienne Kneuss)
Consider the following example:
(assert F)
(check-sat a)
@ -45,6 +47,12 @@ Version 4.3.2
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.
- Fixed crash reported at http://z3.codeplex.com/workitem/11.
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())

209
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
@ -134,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 != "":
@ -166,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()
@ -174,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()
@ -182,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()
@ -190,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()
@ -201,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:
@ -224,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:
@ -242,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')
@ -261,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')
@ -322,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:
@ -339,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':
@ -355,42 +349,42 @@ 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(" -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."
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
@ -403,7 +397,7 @@ def parse_options():
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
'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:
@ -446,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
@ -497,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
@ -781,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):
@ -1196,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)
@ -1208,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)
@ -1315,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"
@ -1401,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')
@ -1437,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')
@ -1465,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():
@ -1577,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')
@ -1591,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
@ -1599,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
@ -1612,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():
@ -1637,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):
@ -1686,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=[]
@ -1734,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):
@ -1742,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
@ -1761,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:
@ -1824,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:
@ -1881,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:
@ -1914,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:
@ -1934,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:
@ -1945,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.
@ -2014,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
@ -2028,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
@ -2098,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
@ -2113,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
@ -2187,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:
@ -2218,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
@ -2305,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():

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);

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
@ -1598,6 +1588,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: *)
(*
@ -2988,9 +2981,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"

71
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
@ -866,23 +856,9 @@ and goal_prec =
- PK_OTHER all internal parameter kinds which are not exposed in the API.
- 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}
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_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format.
@ -891,7 +867,6 @@ and goal_prec =
(**
{!error_code}
Z3 error codes
- OK: No error.
- SORT_ERROR: User tried to build an invalid (type incorrect) AST.
- IOB: Index out of bounds.
@ -908,7 +883,6 @@ and goal_prec =
*)
(**
Definitions for update_api.py
def_Type('CONFIG', 'config', 'Config')
def_Type('CONTEXT', 'context', 'ContextObj')
def_Type('AST', 'ast', 'Ast')
@ -5043,6 +5017,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}}
@ -8941,27 +8939,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.
- {b See also}: {!check_and_get_model}

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

@ -594,30 +594,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,
@ -626,7 +603,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)
@ -642,7 +619,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,
@ -660,13 +637,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;
}
@ -698,7 +675,7 @@ void check_error_code (Z3_context c)
/* Disable default error handler, all error checking is done by check_error_code */
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,
@ -707,7 +684,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)
@ -11110,6 +11087,56 @@ check_error_code(c);
return _vres;
}
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));
@ -18321,50 +18348,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()

11
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.
@ -7140,7 +7147,9 @@ END_MLAPI_EXCLUDE
__in_ecount(num_terms) Z3_ast const terms[],
__out_ecount(num_terms) unsigned class_ids[]
);
#endif
#ifdef CorML3
/**
\brief Delete a model object.

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(); }

23
src/ast/array_decl_plugin.cpp
View file

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

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;

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));
}
}

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

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

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());

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;
}

9
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) {
@ -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)

3
src/cmd_context/cmd_context.h
View file

@ -249,6 +249,9 @@ protected:
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);

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.

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,

2
src/muz_qe/proof_utils.cpp
View file

@ -450,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)

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); }
};

2
src/smt/proto_model/array_factory.cpp
View file

@ -34,7 +34,7 @@ func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) {
}
array_factory::array_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.get_family_id("array"), md) {
struct_factory(m, m.mk_family_id("array"), md) {
}
/**

2
src/smt/proto_model/datatype_factory.cpp
View file

@ -22,7 +22,7 @@ Revision History:
#include"ast_ll_pp.h"
datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.get_family_id("datatype"), md),
struct_factory(m, m.mk_family_id("datatype"), md),
m_util(m) {
}

4
src/smt/proto_model/numeral_factory.cpp
View file

@ -24,7 +24,7 @@ app * arith_factory::mk_value_core(rational const & val, sort * s) {
}
arith_factory::arith_factory(ast_manager & m):
numeral_factory(m, m.get_family_id("arith")),
numeral_factory(m, m.mk_family_id("arith")),
m_util(m) {
}
@ -36,7 +36,7 @@ app * arith_factory::mk_value(rational const & val, bool is_int) {
}
bv_factory::bv_factory(ast_manager & m):
numeral_factory(m, m.get_family_id("bv")),
numeral_factory(m, m.mk_family_id("bv")),
m_util(m) {
}

2
src/smt/proto_model/proto_model.cpp
View file

@ -31,7 +31,7 @@ proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p):
model_core(m),
m_asts(m),
m_simplifier(s),
m_afid(m.get_family_id(symbol("array"))) {
m_afid(m.mk_family_id(symbol("array"))) {
register_factory(alloc(basic_factory, m));
m_user_sort_factory = alloc(user_sort_factory, m);
register_factory(m_user_sort_factory);

2
src/smt/proto_model/value_factory.cpp
View file

@ -51,7 +51,7 @@ expr * basic_factory::get_fresh_value(sort * s) {
}
user_sort_factory::user_sort_factory(ast_manager & m):
simple_factory<unsigned>(m, m.get_family_id("user-sort")) {
simple_factory<unsigned>(m, m.mk_family_id("user-sort")) {
}
void user_sort_factory::freeze_universe(sort * s) {

2
src/smt/smt_kernel.cpp
View file

@ -253,12 +253,10 @@ namespace smt {
}
lbool kernel::setup_and_check() {
set_cancel(false);
return m_imp->setup_and_check();
}
lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) {
set_cancel(false);
lbool r = m_imp->check(num_assumptions, assumptions);
TRACE("smt_kernel", tout << "check result: " << r << "\n";);
return r;

4
src/smt/smt_model_finder.cpp
View file

@ -454,8 +454,8 @@ namespace smt {
m_model(0),
m_eval_cache_range(m),
m_new_constraints(0) {
m_asimp = static_cast<arith_simplifier_plugin*>(s.get_plugin(m.get_family_id("arith")));
m_bvsimp = static_cast<bv_simplifier_plugin*>(s.get_plugin(m.get_family_id("bv")));
m_asimp = static_cast<arith_simplifier_plugin*>(s.get_plugin(m.mk_family_id("arith")));
m_bvsimp = static_cast<bv_simplifier_plugin*>(s.get_plugin(m.mk_family_id("bv")));
}
~auf_solver() {

2
src/smt/smt_model_finder.h
View file

@ -33,7 +33,7 @@ Abstract:
Lugano, Switzerland, 2010.
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software
Development, Leonardo de Moura, Nikolaj Bjørner, IJCAR,
Development, Leonardo de Moura, Nikolaj Bjorner, IJCAR,
Edinburgh, Scotland, 2010.
Author:

6
src/smt/smt_setup.cpp
View file

@ -692,7 +692,7 @@ namespace smt {
void setup::setup_arith() {
switch(m_params.m_arith_mode) {
case AS_NO_ARITH:
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.get_family_id("arith"), "no arithmetic"));
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
break;
case AS_DIFF_LOGIC:
if (m_params.m_arith_fixnum) {
@ -734,7 +734,7 @@ namespace smt {
void setup::setup_bv() {
switch(m_params.m_bv_mode) {
case BS_NO_BV:
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.get_family_id("bv"), "no bit-vector"));
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("bv"), "no bit-vector"));
break;
case BS_BLASTER:
m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params));
@ -745,7 +745,7 @@ namespace smt {
void setup::setup_arrays() {
switch(m_params.m_array_mode) {
case AR_NO_ARRAY:
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.get_family_id("array"), "no array"));
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("array"), "no array"));
break;
case AR_SIMPLE:
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));

2
src/smt/theory_arith_core.h
View file

@ -1294,7 +1294,7 @@ namespace smt {
template<typename Ext>
theory_arith<Ext>::theory_arith(ast_manager & m, theory_arith_params & params):
theory(m.get_family_id("arith")),
theory(m.mk_family_id("arith")),
m_params(params),
m_util(m),
m_arith_eq_solver(m),

2
src/smt/theory_array_base.cpp
View file

@ -27,7 +27,7 @@ Revision History:
namespace smt {
theory_array_base::theory_array_base(ast_manager & m):
theory(m.get_family_id("array")),
theory(m.mk_family_id("array")),
m_found_unsupported_op(false)
{
}

2
src/smt/theory_bv.cpp
View file

@ -1239,7 +1239,7 @@ namespace smt {
}
theory_bv::theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params):
theory(m.get_family_id("bv")),
theory(m.mk_family_id("bv")),
m_params(params),
m_util(m),
m_autil(m),

2
src/smt/theory_datatype.cpp
View file

@ -454,7 +454,7 @@ namespace smt {
}
theory_datatype::theory_datatype(ast_manager & m, theory_datatype_params & p):
theory(m.get_family_id("datatype")),
theory(m.mk_family_id("datatype")),
m_params(p),
m_util(m),
m_find(*this),

2
src/smt/theory_dense_diff_logic_def.h
View file

@ -28,7 +28,7 @@ namespace smt {
template<typename Ext>
theory_dense_diff_logic<Ext>::theory_dense_diff_logic(ast_manager & m, theory_arith_params & p):
theory(m.get_family_id("arith")),
theory(m.mk_family_id("arith")),
m_params(p),
m_autil(m),
m_arith_eq_adapter(*this, p, m_autil),

2
src/smt/theory_diff_logic.h
View file

@ -306,7 +306,7 @@ namespace smt {
public:
theory_diff_logic(ast_manager& m, smt_params & params):
theory(m.get_family_id("arith")),
theory(m.mk_family_id("arith")),
m_params(params),
m_util(m),
m_arith_eq_adapter(*this, params, m_util),

4
src/smt/theory_dl.cpp
View file

@ -88,7 +88,7 @@ namespace smt {
m_th.get_rep(s, r, v);
app_ref rep_of(m_th.m());
rep_of = m_th.m().mk_app(r, m_node->get_owner());
theory_id bv_id = m_th.m().get_family_id("bv");
theory_id bv_id = m_th.m().mk_family_id("bv");
theory_bv* th_bv = dynamic_cast<theory_bv*>(ctx.get_theory(bv_id));
SASSERT(th_bv);
rational val;
@ -106,7 +106,7 @@ namespace smt {
public:
theory_dl(ast_manager& m):
theory(m.get_family_id("datalog_relation")),
theory(m.mk_family_id("datalog_relation")),
m_util(m),
m_bv(m),
m_trail(m)

2
src/smt/theory_seq_empty.h
View file

@ -32,7 +32,7 @@ namespace smt {
virtual theory* mk_fresh(context*) { return alloc(theory_seq_empty, get_manager()); }
virtual char const * get_name() const { return "seq-empty"; }
public:
theory_seq_empty(ast_manager& m):theory(m.get_family_id("seq")), m_used(false) {}
theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
};
};

2
src/smt/user_plugin/user_smt_theory.cpp
View file

@ -646,7 +646,7 @@ namespace smt {
context & ctx = _s.get_context(); // HACK
symbol _name(name);
ast_manager & m = ctx.get_manager();
family_id fid = m.get_family_id(_name);
family_id fid = m.mk_family_id(_name);
user_decl_plugin * dp = alloc(user_decl_plugin);
m.register_plugin(fid, dp);
simplifier & s = ctx.get_simplifier();

2
src/tactic/arith/bv2int_rewriter.cpp
View file

@ -544,7 +544,7 @@ bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
m_bv.is_extract(e2, lo1, hi1, e3) &&
lo1 == 0 && hi1 == hi-1 &&
m_arith.is_numeral(t2, k, is_int) && is_int &&
k == m_bv.power_of_two(hi)
k == rational::power_of_two(hi)
) {
s = e3;
return true;

2
src/tactic/arith/nla2bv_tactic.cpp
View file

@ -253,7 +253,7 @@ class nla2bv_tactic : public tactic {
s_bv = m_arith.mk_sub(m_arith.mk_numeral(*up, true), s_bv);
}
else {
s_bv = m_arith.mk_sub(s_bv, m_arith.mk_numeral(m_bv.power_of_two(num_bits-1), true));
s_bv = m_arith.mk_sub(s_bv, m_arith.mk_numeral(rational::power_of_two(num_bits-1), true));
}
m_trail.push_back(s_bv);

4
src/tactic/arith/pb2bv_tactic.cpp
View file

@ -583,7 +583,7 @@ private:
return false; // size must be even
// I implemented only the easy (and very common) case, where a_i = 2^{n-i-1} and c = 2^n - 1
unsigned n = sz/2;
if (c != m_bv_util.power_of_two(n) - numeral(1))
if (c != rational::power_of_two(n) - numeral(1))
return false;
for (unsigned i = 0; i < n; i++) {
monomial const & m1 = p[i*2];
@ -592,7 +592,7 @@ private:
return false;
if (m1.m_a != m2.m_a)
return false;
if (m1.m_a != m_bv_util.power_of_two(n - i - 1))
if (m1.m_a != rational::power_of_two(n - i - 1))
return false;
}
return true;

6
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -647,9 +647,9 @@ class elim_uncnstr_tactic : public tactic {
unsigned bv_sz = m_bv_util.get_bv_size(arg1);
rational MAX;
if (is_signed)
MAX = m_bv_util.power_of_two(bv_sz - 1) - rational(1);
MAX = rational::power_of_two(bv_sz - 1) - rational(1);
else
MAX = m_bv_util.power_of_two(bv_sz) - rational(1);
MAX = rational::power_of_two(bv_sz) - rational(1);
app * u;
bool is_new = mk_fresh_uncnstr_var_for(f, arg1, arg2, u);
app * r = m().mk_or(u, m().mk_eq(t, m_bv_util.mk_numeral(MAX, bv_sz)));
@ -666,7 +666,7 @@ class elim_uncnstr_tactic : public tactic {
unsigned bv_sz = m_bv_util.get_bv_size(arg1);
rational MIN;
if (is_signed)
MIN = -m_bv_util.power_of_two(bv_sz - 1);
MIN = -rational::power_of_two(bv_sz - 1);
else
MIN = rational(0);
app * u;

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

@ -32,7 +32,7 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m_mpz_manager(m_mpf_manager.mpz_manager()),
m_bv_util(m),
extra_assertions(m) {
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.get_family_id("float")));
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.mk_family_id("float")));
}
fpa2bv_converter::~fpa2bv_converter() {

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