mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

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

Browse source 
Conflicts:
	src/tactic/sls/sls_tactic.cpp

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-09-11 00:19:05 +01:00
parent fceaf97c95 dd62ca5eb3
commit 3660c617ea
125 changed files with 1759 additions and 657 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/tptp/tptp5.cpp
View file

@ -1630,10 +1630,8 @@ public:
unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0));
std::set<unsigned> const& hyps = m_proof_hypotheses.find(parent_id)->second;
print_hypotheses(out, hyps);
out << ").\n";
out << "))).\n";
break;
display_inference(out, "lemma", "thm", p);
break;
}
case Z3_OP_PR_UNIT_RESOLUTION:
display_inference(out, "unit_resolution", "thm", p);

180
scripts/mk_util.py
View file

@ -1,7 +1,7 @@
############################################
# Copyright (c) 2012 Microsoft Corporation
#
# Auxiliary scripts for generating Makefiles
#
# Auxiliary scripts for generating Makefiles
# and Visual Studio project files.
#
# Author: Leonardo de Moura (leonardo)
@ -42,7 +42,7 @@ BUILD_DIR='build'
REV_BUILD_DIR='..'
SRC_DIR='src'
EXAMPLE_DIR='examples'
# Required Components
# Required Components
Z3_DLL_COMPONENT='api_dll'
PATTERN_COMPONENT='pattern'
UTIL_COMPONENT='util'
@ -80,7 +80,7 @@ GPROF=False
GIT_HASH=False
def check_output(cmd):
return subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0].rstrip('\r\n')
return str(subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).rstrip('\r\n')
def git_hash():
try:
@ -222,7 +222,7 @@ def test_openmp(cc):
return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0
def find_jni_h(path):
for root, dirs, files in os.walk(path):
for root, dirs, files in os.walk(path):
for f in files:
if f == 'jni.h':
return root
@ -234,7 +234,7 @@ def check_java():
global JAR
JDK_HOME = getenv('JDK_HOME', None) # we only need to check this locally.
if is_verbose():
print("Finding javac ...")
@ -283,7 +283,7 @@ def check_java():
oo = TempFile('output')
eo = TempFile('errout')
try:
try:
subprocess.call([JAVAC, 'Hello.java', '-verbose'], stdout=oo.fname, stderr=eo.fname)
oo.commit()
eo.commit()
@ -298,7 +298,7 @@ def check_java():
if JNI_HOME != None:
if not os.path.exists(os.path.join(JNI_HOME, 'jni.h')):
raise MKException("Failed to detect jni.h '%s'; the environment variable JNI_HOME is probably set to the wrong path." % os.path.join(JNI_HOME))
else:
else:
# Search for jni.h in the library directories...
t = open('errout', 'r')
open_pat = re.compile("\[search path for class files: (.*)\]")
@ -314,22 +314,22 @@ def check_java():
# ... plus some heuristic ones.
extra_dirs = []
# For the libraries, even the JDK usually uses a JRE that comes with it. To find the
# For the libraries, even the JDK usually uses a JRE that comes with it. To find the
# headers we have to go a little bit higher up.
for dir in cdirs:
extra_dirs.append(os.path.abspath(os.path.join(dir, '..')))
if IS_OSX: # Apparently Apple knows best where to put stuff...
extra_dirs.append('/System/Library/Frameworks/JavaVM.framework/Headers/')
cdirs[len(cdirs):] = extra_dirs
for dir in cdirs:
q = find_jni_h(dir)
if q != False:
JNI_HOME = q
if JNI_HOME == None:
raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
@ -351,7 +351,7 @@ def find_cxx_compiler():
if test_cxx_compiler(cxx):
CXX = cxx
return CXX
raise MKException('C++ compiler was not found. Try to set the environment variable CXX with the C++ compiler available in your system.')
raise MKException('C++ compiler was not found. Try to set the environment variable CXX with the C++ compiler available in your system.')
def find_c_compiler():
global CC, C_COMPILERS
@ -362,7 +362,7 @@ def find_c_compiler():
if test_c_compiler(c):
CC = c
return CC
raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.')
raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.')
def set_version(major, minor, build, revision):
global VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION
@ -478,8 +478,8 @@ def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:df:sxhmcvtnp:gj',
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:df:sxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
'githash='])
@ -534,7 +534,7 @@ def parse_options():
elif opt == '--gprof':
GPROF = True
elif opt == '--githash':
GIT_HASH=arg
GIT_HASH=arg
else:
print("ERROR: Invalid command line option '%s'" % opt)
display_help(1)
@ -548,7 +548,7 @@ def extract_c_includes(fname):
system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
# We should generate and error for any occurrence of #include that does not match the previous pattern.
non_std_inc_pat = re.compile(".*#include.*")
f = open(fname, 'r')
linenum = 1
for line in f:
@ -622,7 +622,7 @@ def is_java_enabled():
return JAVA_ENABLED
def is_compiler(given, expected):
"""
"""
Return True if the 'given' compiler is the expected one.
>>> is_compiler('g++', 'g++')
True
@ -741,7 +741,7 @@ class Component:
self.add_rule_for_each_include(out, include)
include_node = '%s.node' % os.path.join(self.build_dir, include)
out.write('%s: ' % include_node)
self.add_cpp_h_deps(out, include)
self.add_cpp_h_deps(out, include)
out.write('\n')
out.write('\t@echo done > %s\n' % include_node)
@ -764,7 +764,7 @@ class Component:
out.write('\n')
mk_dir(os.path.join(BUILD_DIR, self.build_dir))
if VS_PAR and IS_WINDOWS:
cppfiles = get_cpp_files(self.src_dir)
cppfiles = list(get_cpp_files(self.src_dir))
dependencies = set()
for cppfile in cppfiles:
dependencies.add(os.path.join(self.to_src_dir, cppfile))
@ -801,7 +801,7 @@ class Component:
# Return true if the component needs builder to generate an install_tactics.cpp file
def require_install_tactics(self):
return False
# Return true if the component needs a def file
def require_def_file(self):
return False
@ -810,6 +810,9 @@ class Component:
def require_mem_initializer(self):
return False
def mk_install_deps(self, out):
return
def mk_install(self, out):
return
@ -818,7 +821,7 @@ class Component:
def is_example(self):
return False
# Invoked when creating a (windows) distribution package using components at build_path, and
# storing them at dist_path
def mk_win_dist(self, build_path, dist_path):
@ -853,10 +856,13 @@ class LibComponent(Component):
out.write('\n')
out.write('%s: %s\n\n' % (self.name, libfile))
def mk_install_dep(self, out):
out.write('%s' % libfile)
def mk_install(self, out):
for include in self.includes2install:
out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(PREFIX)', 'include', include)))
def mk_uninstall(self, out):
for include in self.includes2install:
out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'include', include))
@ -865,7 +871,7 @@ class LibComponent(Component):
mk_dir(os.path.join(dist_path, 'include'))
for include in self.includes2install:
shutil.copy(os.path.join(self.src_dir, include),
os.path.join(dist_path, 'include', include))
os.path.join(dist_path, 'include', include))
def mk_unix_dist(self, build_path, dist_path):
self.mk_win_dist(build_path, dist_path)
@ -935,11 +941,14 @@ class ExeComponent(Component):
def main_component(self):
return self.install
def mk_install_dep(self, out):
out.write('%s' % exefile)
def mk_install(self, out):
if self.install:
exefile = '%s$(EXE_EXT)' % self.exe_name
out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(PREFIX)', 'bin', exefile)))
def mk_uninstall(self, out):
exefile = '%s$(EXE_EXT)' % self.exe_name
out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'bin', exefile))
@ -1063,7 +1072,7 @@ class DLLComponent(Component):
out.write(' ')
out.write(obj)
out.write('\n')
def main_component(self):
return self.install
@ -1076,6 +1085,11 @@ class DLLComponent(Component):
def require_def_file(self):
return IS_WINDOWS and self.export_files
def mk_install_dep(self, out):
out.write('%s$(SO_EXT)' % self.dll_name)
if self.static:
out.write(' %s$(LIB_EXT)' % self.dll_name)
def mk_install(self, out):
if self.install:
dllfile = '%s$(SO_EXT)' % self.dll_name
@ -1084,7 +1098,7 @@ class DLLComponent(Component):
if self.static:
libfile = '%s$(LIB_EXT)' % self.dll_name
out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(PREFIX)', 'lib', libfile)))
def mk_uninstall(self, out):
dllfile = '%s$(SO_EXT)' % self.dll_name
@ -1118,7 +1132,7 @@ class DotNetDLLComponent(Component):
if assembly_info_dir == None:
assembly_info_dir = "."
self.dll_name = dll_name
self.assembly_info_dir = assembly_info_dir
self.assembly_info_dir = assembly_info_dir
def mk_makefile(self, out):
if DOTNET_ENABLED:
@ -1137,7 +1151,11 @@ class DotNetDLLComponent(Component):
out.write(' ')
out.write(cs_file)
out.write('\n')
out.write(' csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /define:DEBUG;TRACE /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /debug+ /debug:full /filealign:512 /optimize- /linkresource:%s.dll /out:%s.dll /target:library' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name))
out.write(' csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /filealign:512 /linkresource:%s.dll /out:%s.dll /target:library /doc:%s.xml' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name, self.dll_name))
if DEBUG_MODE:
out.write(' /define:DEBUG;TRACE /debug+ /debug:full /optimize-')
else:
out.write(' /optimize+')
if VS_X64:
out.write(' /platform:x64')
else:
@ -1147,7 +1165,7 @@ class DotNetDLLComponent(Component):
out.write('\n')
out.write('%s: %s\n\n' % (self.name, dllfile))
return
def main_component(self):
return DOTNET_ENABLED
@ -1160,6 +1178,13 @@ class DotNetDLLComponent(Component):
mk_dir(os.path.join(dist_path, 'bin'))
shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
'%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
'%s.xml' % os.path.join(dist_path, 'bin', self.dll_name))
if DEBUG_MODE:
shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
'%s.pdb' % os.path.join(dist_path, 'bin', self.dll_name))
def mk_unix_dist(self, build_path, dist_path):
# Do nothing
@ -1180,7 +1205,7 @@ class JavaDLLComponent(Component):
if is_java_enabled():
mk_dir(os.path.join(BUILD_DIR, 'api', 'java', 'classes'))
dllfile = '%s$(SO_EXT)' % self.dll_name
dllfile = '%s$(SO_EXT)' % self.dll_name
out.write('libz3java$(SO_EXT): libz3$(SO_EXT) %s\n' % os.path.join(self.to_src_dir, 'Native.cpp'))
t = '\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/java/Native$(OBJ_EXT) -I"%s" -I"%s/PLATFORM" -I%s %s/Native.cpp\n' % (JNI_HOME, JNI_HOME, get_component('api').to_src_dir, self.to_src_dir)
if IS_OSX:
@ -1211,16 +1236,16 @@ class JavaDLLComponent(Component):
JAR = '"%s"' % JAR
t = ('\t%s %s.java -d %s\n' % (JAVAC, os.path.join(self.to_src_dir, 'enumerations', '*'), os.path.join('api', 'java', 'classes')))
out.write(t)
t = ('\t%s -cp %s %s.java -d %s\n' % (JAVAC,
os.path.join('api', 'java', 'classes'),
os.path.join(self.to_src_dir, '*'),
t = ('\t%s -cp %s %s.java -d %s\n' % (JAVAC,
os.path.join('api', 'java', 'classes'),
os.path.join(self.to_src_dir, '*'),
os.path.join('api', 'java', 'classes')))
out.write(t)
out.write('\t%s cfm %s.jar %s -C %s .\n' % (JAR, self.package_name,
os.path.join(self.to_src_dir, 'manifest'),
out.write('\t%s cfm %s.jar %s -C %s .\n' % (JAR, self.package_name,
os.path.join(self.to_src_dir, 'manifest'),
os.path.join('api', 'java', 'classes')))
out.write('java: %s.jar\n\n' % self.package_name)
def main_component(self):
return is_java_enabled()
@ -1229,7 +1254,7 @@ class JavaDLLComponent(Component):
mk_dir(os.path.join(dist_path, 'bin'))
shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
'%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
shutil.copy(os.path.join(build_path, 'libz3java.dll'),
shutil.copy(os.path.join(build_path, 'libz3java.dll'),
os.path.join(dist_path, 'bin', 'libz3java.dll'))
shutil.copy(os.path.join(build_path, 'libz3java.lib'),
os.path.join(dist_path, 'bin', 'libz3java.lib'))
@ -1240,7 +1265,7 @@ class JavaDLLComponent(Component):
shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
'%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
so = get_so_ext()
shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
os.path.join(dist_path, 'bin', 'libz3java.%s' % so))
class ExampleComponent(Component):
@ -1296,7 +1321,7 @@ class CExampleComponent(CppExampleComponent):
def src_files(self):
return get_c_files(self.ex_dir)
class DotNetExampleComponent(ExampleComponent):
def __init__(self, name, path):
ExampleComponent.__init__(self, name, path)
@ -1577,7 +1602,7 @@ def mk_config():
config.write('CC=%s\n' % CC)
config.write('CXX=%s\n' % CXX)
config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS))
config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG)
config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG)
config.write('CXX_OUT_FLAG=-o \n')
config.write('OBJ_EXT=.o\n')
config.write('LIB_EXT=.a\n')
@ -1611,7 +1636,11 @@ def mk_config():
print('Java Compiler: %s' % JAVAC)
def mk_install(out):
out.write('install:\n')
out.write('install: ')
for c in get_components():
c.mk_install_deps(out)
out.write(' ')
out.write('\n')
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'bin'))
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'include'))
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'lib'))
@ -1632,7 +1661,7 @@ def mk_install(out):
out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' %
(os.path.join(PREFIX, 'lib'), LD_LIBRARY_PATH))
out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
out.write('\n')
out.write('\n')
def mk_uninstall(out):
out.write('uninstall:\n')
@ -1642,7 +1671,7 @@ def mk_uninstall(out):
out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
out.write('\t@echo Z3 was successfully uninstalled.\n')
out.write('\n')
out.write('\n')
# Generate the Z3 makefile
def mk_makefile():
@ -1697,7 +1726,7 @@ def mk_makefile():
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)
# Generate automatically generated source code
def mk_auto_src():
if not ONLY_MAKEFILES:
@ -1783,10 +1812,10 @@ def def_module_params(module_name, export, params, class_name=None, description=
# Generated accessors
for param in params:
if export:
out.write(' %s %s() const { return p.%s("%s", g, %s); }\n' %
out.write(' %s %s() const { return p.%s("%s", g, %s); }\n' %
(TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
else:
out.write(' %s %s() const { return p.%s("%s", %s); }\n' %
out.write(' %s %s() const { return p.%s("%s", %s); }\n' %
(TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
out.write('};\n')
out.write('#endif\n')
@ -1799,8 +1828,8 @@ def max_memory_param():
def max_steps_param():
return ('max_steps', UINT, UINT_MAX, 'maximum number of steps')
PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRING, 'SYMBOL' : SYMBOL,
'UINT_MAX' : UINT_MAX,
PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRING, 'SYMBOL' : SYMBOL,
'UINT_MAX' : UINT_MAX,
'max_memory_param' : max_memory_param,
'max_steps_param' : max_steps_param,
'def_module_params' : def_module_params }
@ -1815,7 +1844,7 @@ def _execfile(file, globals=globals(), locals=locals()):
# Execute python auxiliary scripts that generate extra code for Z3.
def exec_pyg_scripts():
global CURR_PYG
for root, dirs, files in os.walk('src'):
for root, dirs, files in os.walk('src'):
for f in files:
if f.endswith('.pyg'):
script = os.path.join(root, f)
@ -1831,7 +1860,7 @@ def mk_pat_db():
fout.write('char const * g_pattern_database =\n')
for line in fin:
fout.write('"%s\\n"\n' % line.strip('\n'))
fout.write(';\n')
fout.write(';\n')
if VERBOSE:
print("Generated '%s'" % os.path.join(c.src_dir, 'database.h'))
@ -1847,7 +1876,7 @@ def update_version():
mk_version_dot_h(major, minor, build, revision)
mk_all_assembly_infos(major, minor, build, revision)
mk_def_files()
# Update files with the version number
def mk_version_dot_h(major, minor, build, revision):
c = get_component(UTIL_COMPONENT)
@ -1870,8 +1899,8 @@ def mk_all_assembly_infos(major, minor, build, revision):
mk_assembly_info_version(assembly, major, minor, build, revision)
else:
raise MKException("Failed to find assembly info file 'AssemblyInfo' at '%s'" % os.path.join(c.src_dir, c.assembly_info_dir))
# Generate version number in the given 'AssemblyInfo.cs' file using 'AssemblyInfo' as a template.
def mk_assembly_info_version(assemblyinfo, major, minor, build, revision):
ver_pat = re.compile('[assembly: AssemblyVersion\("[\.\d]*"\) *')
@ -1936,7 +1965,7 @@ def mk_install_tactic_cpp(cnames, path):
if not added_include:
added_include = True
fout.write('#include"%s"\n' % h_file)
try:
try:
exec(line.strip('\n '), globals())
except:
raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line))
@ -1944,7 +1973,7 @@ def mk_install_tactic_cpp(cnames, path):
if not added_include:
added_include = True
fout.write('#include"%s"\n' % h_file)
try:
try:
exec(line.strip('\n '), globals())
except:
raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line))
@ -2128,7 +2157,7 @@ def mk_def_files():
def cp_z3py_to_build():
mk_dir(BUILD_DIR)
# Erase existing .pyc files
for root, dirs, files in os.walk(Z3PY_SRC_DIR):
for root, dirs, files in os.walk(Z3PY_SRC_DIR):
for f in files:
if f.endswith('.pyc'):
rmf(os.path.join(root, f))
@ -2171,7 +2200,7 @@ def mk_bindings(api_files):
mk_z3consts_java(api_files)
_execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
cp_z3py_to_build()
# Extract enumeration types from API files, and add python definitions.
def mk_z3consts_py(api_files):
if Z3PY_SRC_DIR == None:
@ -2208,7 +2237,7 @@ def mk_z3consts_py(api_files):
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
@ -2249,7 +2278,7 @@ def mk_z3consts_py(api_files):
linenum = linenum + 1
if VERBOSE:
print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py'))
# Extract enumeration types from z3_api.h, and add .Net definitions
def mk_z3consts_dotnet(api_files):
@ -2290,7 +2319,7 @@ def mk_z3consts_dotnet(api_files):
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
@ -2373,7 +2402,7 @@ def mk_z3consts_java(api_files):
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
@ -2411,7 +2440,7 @@ def mk_z3consts_java(api_files):
for k in decls:
i = decls[k]
if first:
first = False
first = False
else:
efile.write(',\n')
efile.write(' %s (%s)' % (k, i))
@ -2422,7 +2451,7 @@ def mk_z3consts_java(api_files):
efile.write(' }\n\n')
efile.write(' public static final %s fromInt(int v) {\n' % name)
efile.write(' for (%s k: values()) \n' % name)
efile.write(' if (k.intValue == v) return k;\n')
efile.write(' if (k.intValue == v) return k;\n')
efile.write(' return values()[0];\n')
efile.write(' }\n\n')
efile.write(' public final int toInt() { return this.intValue; }\n')
@ -2493,7 +2522,11 @@ def mk_vs_proj(name, components):
f.write(' <ClCompile>\n')
f.write(' <Optimization>Disabled</Optimization>\n')
f.write(' <PreprocessorDefinitions>WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
f.write(' <MinimalRebuild>true</MinimalRebuild>\n')
if VS_PAR:
f.write(' <MinimalRebuild>false</MinimalRebuild>\n')
f.write(' <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')
else:
f.write(' <MinimalRebuild>true</MinimalRebuild>\n')
f.write(' <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
f.write(' <WarningLevel>Level3</WarningLevel>\n')
f.write(' <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n')
@ -2527,7 +2560,11 @@ def mk_vs_proj(name, components):
f.write(' <ClCompile>\n')
f.write(' <Optimization>Disabled</Optimization>\n')
f.write(' <PreprocessorDefinitions>WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
f.write(' <MinimalRebuild>true</MinimalRebuild>\n')
if VS_PAR:
f.write(' <MinimalRebuild>false</MinimalRebuild>\n')
f.write(' <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')
else:
f.write(' <MinimalRebuild>true</MinimalRebuild>\n')
f.write(' <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
f.write(' <WarningLevel>Level3</WarningLevel>\n')
f.write(' <RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>\n')
@ -2573,16 +2610,17 @@ def mk_vs_proj(name, components):
def mk_win_dist(build_path, dist_path):
for c in get_components():
c.mk_win_dist(build_path, dist_path)
# Add Z3Py to lib directory
for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)):
# Add Z3Py to bin directory
print("Adding to %s\n" % dist_path)
for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
shutil.copy(os.path.join(build_path, pyc),
os.path.join(dist_path, 'bin', pyc))
def mk_unix_dist(build_path, dist_path):
for c in get_components():
c.mk_unix_dist(build_path, dist_path)
# Add Z3Py to lib directory
for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)):
# Add Z3Py to bin directory
for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
shutil.copy(os.path.join(build_path, pyc),
os.path.join(dist_path, 'bin', pyc))

2
scripts/update_api.py
View file

@ -420,7 +420,7 @@ def mk_dotnet():
NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
Unwrapped = [ 'Z3_del_context' ]
Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
def mk_dotnet_wrappers():
global Type2Str

94
src/api/api_interp.cpp
View file

@ -38,6 +38,7 @@ Revision History:
#include"iz3hash.h"
#include"iz3pp.h"
#include"iz3checker.h"
#include"scoped_proof.h"
using namespace stl_ext;
@ -290,6 +291,99 @@ extern "C" {
opts->map[name] = value;
}
Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p){
Z3_TRY;
LOG_Z3_get_interpolant(c, pf, pat, p);
RESET_ERROR_CODE();
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
mk_c(c)->save_object(v);
ast *_pf = to_ast(pf);
ast *_pat = to_ast(pat);
ptr_vector<ast> interp;
ptr_vector<ast> cnsts; // to throw away
ast_manager &_m = mk_c(c)->m();
iz3interpolate(_m,
_pf,
cnsts,
_pat,
interp,
(interpolation_options_struct *) 0 // ignore params for now
);
// copy result back
for(unsigned i = 0; i < interp.size(); i++){
v->m_ast_vector.push_back(interp[i]);
_m.dec_ref(interp[i]);
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);
}
Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp, __out Z3_model *model){
Z3_TRY;
LOG_Z3_compute_interpolant(c, pat, p, out_interp, model);
RESET_ERROR_CODE();
// params_ref &_p = to_params(p)->m_params;
params_ref _p;
_p.set_bool("proof", true); // this is currently useless
scoped_proof_mode spm(mk_c(c)->m(),PGM_FINE);
scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
m_solver.get()->updt_params(_p); // why do we have to do this?
ast *_pat = to_ast(pat);
ptr_vector<ast> interp;
ptr_vector<ast> cnsts; // to throw away
ast_manager &_m = mk_c(c)->m();
model_ref m;
lbool _status = iz3interpolate(_m,
*(m_solver.get()),
_pat,
cnsts,
interp,
m,
0 // ignore params for now
);
Z3_lbool status = of_lbool(_status);
Z3_ast_vector_ref *v = 0;
*model = 0;
if(_status == l_false){
// copy result back
v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
mk_c(c)->save_object(v);
for(unsigned i = 0; i < interp.size(); i++){
v->m_ast_vector.push_back(interp[i]);
_m.dec_ref(interp[i]);
}
}
else {
model_ref _m;
m_solver.get()->get_model(_m);
Z3_model_ref *crap = alloc(Z3_model_ref);
crap->m_model = _m.get();
mk_c(c)->save_object(crap);
*model = of_model(crap);
}
*out_interp = of_ast_vector(v);
return status;
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
};

3
src/api/api_model.cpp
View file

@ -60,6 +60,7 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
mk_c(c)->save_ast_trail(r);
RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(0);
}
@ -263,6 +264,7 @@ extern "C" {
RESET_ERROR_CODE();
CHECK_NON_NULL(f, 0);
expr * e = to_func_interp_ref(f)->get_else();
mk_c(c)->save_ast_trail(e);
RETURN_Z3(of_expr(e));
Z3_CATCH_RETURN(0);
}
@ -301,6 +303,7 @@ extern "C" {
LOG_Z3_func_entry_get_value(c, e);
RESET_ERROR_CODE();
expr * v = to_func_entry_ref(e)->get_result();
mk_c(c)->save_ast_trail(v);
RETURN_Z3(of_expr(v));
Z3_CATCH_RETURN(0);
}

1
src/api/api_solver.cpp
View file

@ -40,6 +40,7 @@ extern "C" {
params_ref p = s->m_params;
mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
s->m_solver->updt_params(p);
}
static void init_solver(Z3_context c, Z3_solver s) {

4
src/api/dotnet/Context.cs
View file

@ -3523,7 +3523,7 @@ namespace Microsoft.Z3
/// </summary>
/// <remarks>
/// The list of all configuration parameters can be obtained using the Z3 executable:
/// <c>z3.exe -ini?</c>
/// <c>z3.exe -p</c>
/// Only a few configuration parameters are mutable once the context is created.
/// An exception is thrown when trying to modify an immutable parameter.
/// </remarks>
@ -3646,7 +3646,7 @@ namespace Microsoft.Z3
internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
internal uint refCount = 0;
internal long refCount = 0;
/// <summary>
/// Finalizer.

39
src/api/dotnet/Fixedpoint.cs
View file

@ -269,6 +269,14 @@ namespace Microsoft.Z3
AST.ArrayLength(queries), AST.ArrayToNative(queries));
}
BoolExpr[] ToBoolExprs(ASTVector v) {
uint n = v.Size;
BoolExpr[] res = new BoolExpr[n];
for (uint i = 0; i < n; i++)
res[i] = new BoolExpr(Context, v[i].NativeObject);
return res;
}
/// <summary>
/// Retrieve set of rules added to fixedpoint context.
/// </summary>
@ -278,12 +286,7 @@ namespace Microsoft.Z3
{
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
uint n = v.Size;
BoolExpr[] res = new BoolExpr[n];
for (uint i = 0; i < n; i++)
res[i] = new BoolExpr(Context, v[i].NativeObject);
return res;
return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)));
}
}
@ -296,15 +299,27 @@ namespace Microsoft.Z3
{
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
uint n = v.Size;
BoolExpr[] res = new BoolExpr[n];
for (uint i = 0; i < n; i++)
res[i] = new BoolExpr(Context, v[i].NativeObject);
return res;
return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)));
}
}
/// <summary>
/// Parse an SMT-LIB2 file with fixedpoint rules.
/// Add the rules to the current fixedpoint context.
/// Return the set of queries in the file.
/// </summary>
public BoolExpr[] ParseFile(string file) {
return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)));
}
/// <summary>
/// Similar to ParseFile. Instead it takes as argument a string.
/// </summary>
public BoolExpr[] ParseString(string s) {
return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)));
}
#region Internal
internal Fixedpoint(Context ctx, IntPtr obj)

8
src/api/dotnet/Z3Object.cs
View file

@ -19,6 +19,7 @@ Notes:
using System;
using System.Diagnostics.Contracts;
using System.Threading;
namespace Microsoft.Z3
{
@ -50,8 +51,7 @@ namespace Microsoft.Z3
if (m_ctx != null)
{
m_ctx.refCount--;
if (m_ctx.refCount == 0)
if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
GC.ReRegisterForFinalize(m_ctx);
m_ctx = null;
}
@ -77,7 +77,7 @@ namespace Microsoft.Z3
{
Contract.Requires(ctx != null);
ctx.refCount++;
Interlocked.Increment(ref ctx.refCount);
m_ctx = ctx;
}
@ -85,7 +85,7 @@ namespace Microsoft.Z3
{
Contract.Requires(ctx != null);
ctx.refCount++;
Interlocked.Increment(ref ctx.refCount);
m_ctx = ctx;
IncRef(obj);
m_n_obj = obj;

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

@ -899,6 +899,7 @@ def _coerce_expr_merge(s, a):
return s
else:
if __debug__:
_z3_assert(s1.ctx == s.ctx, "context mismatch")
_z3_assert(False, "sort mismatch")
else:
return s
@ -1459,9 +1460,18 @@ def And(*args):
>>> And(P)
And(p__0, p__1, p__2, p__3, p__4)
"""
args = _get_args(args)
ctx = _ctx_from_ast_arg_list(args)
last_arg = None
if len(args) > 0:
last_arg = args[len(args)-1]
if isinstance(last_arg, Context):
ctx = args[len(args)-1]
args = args[:len(args)-1]
else:
ctx = main_ctx()
args = _get_args(args)
ctx_args = _ctx_from_ast_arg_list(args, ctx)
if __debug__:
_z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
if _has_probe(args):
return _probe_and(args, ctx)
@ -1480,9 +1490,18 @@ def Or(*args):
>>> Or(P)
Or(p__0, p__1, p__2, p__3, p__4)
"""
args = _get_args(args)
ctx = _ctx_from_ast_arg_list(args)
last_arg = None
if len(args) > 0:
last_arg = args[len(args)-1]
if isinstance(last_arg, Context):
ctx = args[len(args)-1]
args = args[:len(args)-1]
else:
ctx = main_ctx()
args = _get_args(args)
ctx_args = _ctx_from_ast_arg_list(args, ctx)
if __debug__:
_z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
if _has_probe(args):
return _probe_or(args, ctx)
@ -4128,6 +4147,7 @@ class Datatype:
"""
if __debug__:
_z3_assert(isinstance(name, str), "String expected")
_z3_assert(name != "", "Constructor name cannot be empty")
return self.declare_core(name, "is_" + name, *args)
def __repr__(self):
@ -7233,3 +7253,128 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
dsz, dnames, ddecls = _dict2darray(decls, ctx)
return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
def Interp(a,ctx=None):
"""Create an interpolation operator.
The argument is an interpolation pattern (see tree_interpolant).
>>> x = Int('x')
>>> print Interp(x>0)
interp(x > 0)
"""
ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
s = BoolSort(ctx)
a = s.cast(a)
return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx)
def tree_interpolant(pat,p=None,ctx=None):
"""Compute interpolant for a tree of formulas.
The input is an interpolation pattern over a set of formulas C.
The pattern pat is a formula combining the formulas in C using
logical conjunction and the "interp" operator (see Interp). This
interp operator is logically the identity operator. It marks the
sub-formulas of the pattern for which interpolants should be
computed. The interpolant is a map sigma from marked subformulas
to formulas, such that, for each marked subformula phi of pat
(where phi sigma is phi with sigma(psi) substituted for each
subformula psi of phi such that psi in dom(sigma)):
1) phi sigma implies sigma(phi), and
2) sigma(phi) is in the common uninterpreted vocabulary between
the formulas of C occurring in phi and those not occurring in
phi
and moreover pat sigma implies false. In the simplest case
an interpolant for the pattern "(and (interp A) B)" maps A
to an interpolant for A /\ B.
The return value is a vector of formulas representing sigma. This
vector contains sigma(phi) for each marked subformula of pat, in
pre-order traversal. This means that subformulas of phi occur before phi
in the vector. Also, subformulas that occur multiply in pat will
occur multiply in the result vector.
If pat is satisfiable, raises an object of class ModelRef
that represents a model of pat.
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
>>> x = Int('x')
>>> y = Int('y')
>>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y))
[Not(x >= 0), Not(y <= 2)]
>>> g = And(Interp(x<0),x<2)
>>> try:
... print tree_interpolant(g).sexpr()
... except ModelRef as m:
... print m.sexpr()
(define-fun x () Int
(- 1))
"""
f = pat
ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
ptr = (AstVectorObj * 1)()
mptr = (Model * 1)()
if p == None:
p = ParamsRef(ctx)
res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
if res == Z3_L_FALSE:
return AstVector(ptr[0],ctx)
raise ModelRef(mptr[0], ctx)
def binary_interpolant(a,b,p=None,ctx=None):
"""Compute an interpolant for a binary conjunction.
If a & b is unsatisfiable, returns an interpolant for a & b.
This is a formula phi such that
1) a implies phi
2) b implies not phi
3) All the uninterpreted symbols of phi occur in both a and b.
If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a &b.
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
>>> x = Int('x')
>>> print binary_interpolant(x<0,x>2)
x <= 2
"""
f = And(Interp(a),b)
return tree_interpolant(f,p,ctx)[0]
def sequence_interpolant(v,p=None,ctx=None):
"""Compute interpolant for a sequence of formulas.
If len(v) == N, and if the conjunction of the formulas in v is
unsatisfiable, the interpolant is a sequence of formulas w
such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
and v[i+1]..v[n]
Requires len(v) >= 1.
If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a & b.
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
>>> x = Int('x')
>>> y = Int('y')
>>> print sequence_interpolant([x < 0, y == x , y > 2])
[Not(x >= 0), Not(y >= 0)]
"""
f = v[0]
for i in range(1,len(v)):
f = And(Interp(f),v[i])
return tree_interpolant(f,p,ctx)

1
src/api/python/z3types.py
View file

@ -109,3 +109,4 @@ class FuncEntryObj(ctypes.c_void_p):
class RCFNumObj(ctypes.c_void_p):
def __init__(self, e): self._as_parameter_ = e
def from_param(obj): return obj

115
src/api/z3_api.h
View file

@ -1375,6 +1375,16 @@ extern "C" {
although some parameters can be changed using #Z3_update_param_value.
All main interaction with Z3 happens in the context of a \c Z3_context.
In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects
are determined by the scope level of #Z3_push and #Z3_pop.
In other words, a Z3_ast object remains valid until there is a
call to Z3_pop that takes the current scope below the level where
the object was created.
Note that all other reference counted objects, including Z3_model,
Z3_solver, Z3_func_interp have to be managed by the caller.
Their reference counts are not handled by the context.
\conly \sa Z3_del_context
\conly \deprecated Use #Z3_mk_context_rc
@ -5668,7 +5678,8 @@ END_MLAPI_EXCLUDE
Each conjunct encodes values of the bound variables of the query that are satisfied.
In PDR mode, the returned answer is a single conjunction.
The previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.
def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
@ -7698,6 +7709,108 @@ END_MLAPI_EXCLUDE
Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
/** Compute an interpolant from a refutation. This takes a proof of
"false" from a set of formulas C, and an interpolation
pattern. The pattern pat is a formula combining the formulas in C
using logical conjunction and the "interp" operator (see
#Z3_mk_interp). This interp operator is logically the identity
operator. It marks the sub-formulas of the pattern for which interpolants should
be computed. The interpolant is a map sigma from marked subformulas to
formulas, such that, for each marked subformula phi of pat (where phi sigma
is phi with sigma(psi) substituted for each subformula psi of phi such that
psi in dom(sigma)):
1) phi sigma implies sigma(phi), and
2) sigma(phi) is in the common uninterpreted vocabulary between
the formulas of C occurring in phi and those not occurring in
phi
and moreover pat sigma implies false. In the simplest case
an interpolant for the pattern "(and (interp A) B)" maps A
to an interpolant for A /\ B.
The return value is a vector of formulas representing sigma. The
vector contains sigma(phi) for each marked subformula of pat, in
pre-order traversal. This means that subformulas of phi occur before phi
in the vector. Also, subformulas that occur multiply in pat will
occur multiply in the result vector.
In particular, calling Z3_get_interpolant on a pattern of the
form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will
result in a sequence interpolant for A_1, A_2,... A_N.
Neglecting interp markers, the pattern must be a conjunction of
formulas in C, the set of premises of the proof. Otherwise an
error is flagged.
Any premises of the proof not present in the pattern are
treated as "background theory". Predicate and function symbols
occurring in the background theory are treated as interpreted and
thus always allowed in the interpolant.
Interpolant may not necessarily be computable from all
proofs. To be sure an interpolant can be computed, the proof
must be generated by an SMT solver for which interpoaltion is
supported, and the premises must be expressed using only
theories and operators for which interpolation is supported.
Currently, the only SMT solver that is supported is the legacy
SMT solver. Such a solver is available as the default solver in
#Z3_context objects produced by #Z3_mk_interpolation_context.
Currently, the theories supported are equality with
uninterpreted functions, linear integer arithmetic, and the
theory of arrays (in SMT-LIB terms, this is AUFLIA).
Quantifiers are allowed. Use of any other operators (including
"labels") may result in failure to compute an interpolant from a
proof.
Parameters:
\param c logical context.
\param pf a refutation from premises (assertions) C
\param pat an interpolation pattern over C
\param p parameters
def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
*/
Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
/* Compute an interpolant for an unsatisfiable conjunction of formulas.
This takes as an argument an interpolation pattern as in
#Z3_get_interpolant. This is a conjunction, some subformulas of
which are marked with the "interp" operator (see #Z3_mk_interp).
The conjunction is first checked for unsatisfiability. The result
of this check is returned in the out parameter "status". If the result
is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
and returned as a vector of formulas. Otherwise the return value is
an empty formula.
See #Z3_get_interpolant for a discussion of supported theories.
The advantage of this function over #Z3_get_interpolant is that
it is not necessary to create a suitable SMT solver and generate
a proof. The disadvantage is that it is not possible to use the
solver incrementally.
Parameters:
\param c logical context.
\param pat an interpolation pattern
\param p parameters for solver creation
\param status returns the status of the sat check
\param model returns model if satisfiable
Return value: status of SAT check
def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
*/
Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model);
/** Constant reprepresenting a root of a formula tree for tree interpolation */
#define IZ3_ROOT SHRT_MAX

10
src/ast/ast_smt_pp.cpp
View file

@ -569,8 +569,8 @@ class smt_printer {
m_out << ")";
}
if (m_is_smt2 && q->get_num_patterns() > 0) {
m_out << "(!";
if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
m_out << "(! ";
}
{
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_is_smt2, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
@ -609,7 +609,11 @@ class smt_printer {
m_out << "}";
}
}
if (m_is_smt2 && q->get_num_patterns() > 0) {
if (q->get_qid() != symbol::null)
m_out << " :qid " << q->get_qid();
if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
m_out << ")";
}
m_out << ")";

18
src/ast/dl_decl_plugin.cpp
View file

@ -599,7 +599,23 @@ namespace datalog {
return 0;
}
result = mk_compare(OP_DL_LT, m_lt_sym, domain);
break;
break;
case OP_DL_REP: {
if (!check_domain(0, 0, num_parameters) ||
!check_domain(1, 1, arity)) return 0;
func_decl_info info(m_family_id, k, 0, 0);
result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info);
break;
}
case OP_DL_ABS: {
if (!check_domain(0, 0, num_parameters) ||
!check_domain(1, 1, arity)) return 0;
func_decl_info info(m_family_id, k, 0, 0);
result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info);
break;
}
default:
m_manager->raise_exception("operator not recognized");

2
src/ast/dl_decl_plugin.h
View file

@ -48,6 +48,8 @@ namespace datalog {
OP_RA_CLONE,
OP_DL_CONSTANT,
OP_DL_LT,
OP_DL_REP,
OP_DL_ABS,
LAST_RA_OP
};

2
src/ast/float_decl_plugin.cpp
View file

@ -106,7 +106,7 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
return false;
}
bool float_decl_plugin::is_rm(expr * n, mpf_rounding_mode & val) {
bool float_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) {
if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_AWAY)) {
val = MPF_ROUND_NEAREST_TAWAY;
return true;

11
src/ast/float_decl_plugin.h
View file

@ -169,7 +169,8 @@ public:
app * mk_value(mpf const & v);
bool is_value(expr * n) { return is_app_of(n, m_family_id, OP_FLOAT_VALUE); }
bool is_value(expr * n, mpf & val);
bool is_rm(expr * n, mpf_rounding_mode & val);
bool is_rm_value(expr * n, mpf_rounding_mode & val);
bool is_rm_value(expr * n) { mpf_rounding_mode t; return is_rm_value(n, t); }
mpf const & get_value(unsigned id) const {
SASSERT(m_value_table.contains(id));
@ -198,7 +199,9 @@ public:
sort * mk_float_sort(unsigned ebits, unsigned sbits);
sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); }
bool is_float(sort * s) { return is_sort_of(s, m_fid, FLOAT_SORT); }
bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
bool is_float(expr * e) { return is_float(m_manager.get_sort(e)); }
bool is_rm(expr * e) { return is_rm(m_manager.get_sort(e)); }
unsigned get_ebits(sort * s);
unsigned get_sbits(sort * s);
@ -217,8 +220,8 @@ public:
app * mk_value(mpf const & v) { return m_plugin->mk_value(v); }
bool is_value(expr * n) { return m_plugin->is_value(n); }
bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }
bool is_rm(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm(n, v); }
bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }
bool is_rm_value(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm_value(n, v); }
app * mk_pzero(unsigned ebits, unsigned sbits);
app * mk_nzero(unsigned ebits, unsigned sbits);

96
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -28,9 +28,10 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m(m),
m_simp(m),
m_util(m),
m_mpf_manager(m_util.fm()),
m_mpz_manager(m_mpf_manager.mpz_manager()),
m_bv_util(m),
m_arith_util(m),
m_mpf_manager(m_util.fm()),
m_mpz_manager(m_mpf_manager.mpz_manager()),
extra_assertions(m) {
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.mk_family_id("float")));
}
@ -268,7 +269,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
result = r;
}
else {
SASSERT(is_rm_sort(f->get_range()));
SASSERT(is_rm(f->get_range()));
result = m.mk_fresh_const(
#ifdef Z3DEBUG
@ -281,6 +282,10 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
expr_ref rcc(m);
rcc = bu().mk_ule(result, bu().mk_numeral(4, 3));
extra_assertions.push_back(rcc);
}
}
@ -1847,6 +1852,55 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
// Just keep it here, as there will be something else that uses it.
mk_triple(args[0], args[1], args[2], result);
}
else if (num == 3 &&
m_bv_util.is_bv(args[0]) &&
m_arith_util.is_numeral(args[1]) &&
m_arith_util.is_numeral(args[2]))
{
// Three arguments, some of them are not numerals.
SASSERT(m_util.is_float(f->get_range()));
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr * rm = args[0];
rational q;
if (!m_arith_util.is_numeral(args[1], q))
NOT_IMPLEMENTED_YET();
rational e;
if (!m_arith_util.is_numeral(args[2], e))
NOT_IMPLEMENTED_YET();
SASSERT(e.is_int64());
SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1));
mpf nte, nta, tp, tn, tz;
m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator());
m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator());
m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator());
m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator());
m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator());
app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m);
a_nte = m_plugin->mk_value(nte);
a_nta = m_plugin->mk_value(nta);
a_tp = m_plugin->mk_value(tp);
a_tn = m_plugin->mk_value(tn);
a_tz = m_plugin->mk_value(tz);
expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m);
mk_value(a_nte->get_decl(), 0, 0, bv_nte);
mk_value(a_nta->get_decl(), 0, 0, bv_nta);
mk_value(a_tp->get_decl(), 0, 0, bv_tp);
mk_value(a_tn->get_decl(), 0, 0, bv_tn);
mk_value(a_tz->get_decl(), 0, 0, bv_tz);
mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tn, bv_tz, result);
mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tp, result, result);
mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), bv_nta, result, result);
mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), bv_nte, result, result);
}
else if (num == 1 && m_bv_util.is_bv(args[0])) {
sort * s = f->get_range();
unsigned to_sbits = m_util.get_sbits(s);
@ -1862,7 +1916,9 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
result);
}
else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) {
else if (num == 2 &&
is_app(args[1]) &&
m_util.is_float(m.get_sort(args[1]))) {
// We also support float to float conversion
sort * s = f->get_range();
expr_ref rm(m), x(m);
@ -2015,23 +2071,24 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
mk_ite(c2, v2, result, result);
mk_ite(c1, v1, result, result);
}
}
else {
}
else if (num == 2 &&
m_util.is_rm(args[0]),
m_arith_util.is_real(args[1])) {
// .. other than that, we only support rationals for asFloat
SASSERT(num == 2);
SASSERT(m_util.is_float(f->get_range()));
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(m_bv_util.is_numeral(args[0]));
rational tmp_rat; unsigned sz;
m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz);
unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(m_bv_util.is_numeral(args[0]));
rational tmp_rat; unsigned sz;
m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz);
SASSERT(tmp_rat.is_int32());
SASSERT(sz == 3);
BV_RM_VAL bv_rm = (BV_RM_VAL) tmp_rat.get_unsigned();
BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned();
mpf_rounding_mode rm;
switch(bv_rm)
switch (bv_rm)
{
case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break;
case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break;
@ -2042,22 +2099,23 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
}
SASSERT(m_util.au().is_numeral(args[1]));
rational q;
SASSERT(m_util.au().is_numeral(args[1]));
m_util.au().is_numeral(args[1], q);
mpf v;
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
expr * sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1);
expr * s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits-1);
expr * s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
expr * e = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
mk_triple(sgn, s, e, result);
m_util.fm().del(v);
}
else
UNREACHABLE();
SASSERT(is_well_sorted(m, result));
}

8
src/ast/fpa/fpa2bv_converter.h
View file

@ -45,9 +45,10 @@ class fpa2bv_converter {
ast_manager & m;
basic_simplifier_plugin m_simp;
float_util m_util;
bv_util m_bv_util;
arith_util m_arith_util;
mpf_manager & m_mpf_manager;
unsynch_mpz_manager & m_mpz_manager;
bv_util m_bv_util;
unsynch_mpz_manager & m_mpz_manager;
float_decl_plugin * m_plugin;
obj_map<func_decl, expr*> m_const2bv;
@ -64,8 +65,9 @@ public:
bool is_float(sort * s) { return m_util.is_float(s); }
bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); }
bool is_rm(expr * e) { return m_util.is_rm(e); }
bool is_rm(sort * s) { return m_util.is_rm(s); }
bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }
bool is_rm_sort(sort * s) { return m_util.is_rm(s); }
void mk_triple(expr * sign, expr * significand, expr * exponent, expr_ref & result) {
SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);

10
src/ast/fpa/fpa2bv_rewriter.h
View file

@ -78,17 +78,23 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
return BR_DONE;
}
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) {
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
m_conv.mk_rm_const(f, result);
return BR_DONE;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
if (m_conv.is_float(args[0])) {
SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
sort * ds = f->get_domain()[0];
if (m_conv.is_float(ds)) {
m_conv.mk_eq(args[0], args[1], result);
return BR_DONE;
}
else if (m_conv.is_rm(ds)) {
result = m().mk_eq(args[0], args[1]);
return BR_DONE;
}
return BR_FAILED;
}

17
src/ast/macros/quasi_macros.cpp
View file

@ -41,7 +41,7 @@ void quasi_macros::find_occurrences(expr * e) {
// we remember whether we have seen an expr once, or more than once;
// when we see it the second time, we don't have to visit it another time,
// as we are only intersted in finding unique function applications.
// as we are only interested in finding unique function applications.
m_visited_once.reset();
m_visited_more.reset();
@ -61,7 +61,7 @@ void quasi_macros::find_occurrences(expr * e) {
case AST_VAR: break;
case AST_QUANTIFIER: m_todo.push_back(to_quantifier(cur)->get_expr()); break;
case AST_APP:
if (is_uninterp(cur) && !is_ground(cur)) {
if (is_non_ground_uninterp(cur)) {
func_decl * f = to_app(cur)->get_decl();
m_occurrences.insert_if_not_there(f, 0);
occurrences_map::iterator it = m_occurrences.find_iterator(f);
@ -76,6 +76,10 @@ void quasi_macros::find_occurrences(expr * e) {
}
};
bool quasi_macros::is_non_ground_uninterp(expr const * e) const {
return is_non_ground(e) && is_uninterp(e);
}
bool quasi_macros::is_unique(func_decl * f) const {
return m_occurrences.find(f) == 1;
}
@ -149,6 +153,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
// Our definition of a quasi-macro:
// Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted,
// f[X] contains all universally quantified variables, and f does not occur in T[X].
TRACE("quasi_macros", tout << "Checking for quasi macro: " << mk_pp(e, m_manager) << std::endl;);
if (is_quantifier(e) && to_quantifier(e)->is_forall()) {
quantifier * q = to_quantifier(e);
@ -157,23 +162,23 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
expr * lhs = to_app(qe)->get_arg(0);
expr * rhs = to_app(qe)->get_arg(1);
if (is_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
!depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
a = to_app(lhs);
t = rhs;
return true;
} else if (is_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
} else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
!depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {
a = to_app(rhs);
t = lhs;
return true;
}
} else if (m_manager.is_not(qe) && is_uninterp(to_app(qe)->get_arg(0)) &&
} else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) &&
is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false
a = to_app(to_app(qe)->get_arg(0));
t = m_manager.mk_false();
return true;
} else if (is_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
} else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
a = to_app(qe);
t = m_manager.mk_true();
return true;

1
src/ast/macros/quasi_macros.h
View file

@ -45,6 +45,7 @@ class quasi_macros {
expr_mark m_visited_more;
bool is_unique(func_decl * f) const;
bool is_non_ground_uninterp(expr const * e) const;
bool fully_depends_on(app * a, quantifier * q) const;
bool depends_on(expr * e, func_decl * f) const;

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

@ -323,6 +323,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
TRACE("bit_blaster", tout << f->get_name() << " ";
for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " ";
tout << "\n";);
if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) {
mk_const(f, result);
return BR_DONE;

10
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -828,6 +828,12 @@ void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * cons
template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_rotate_left(unsigned sz, expr * const * a_bits, unsigned n, expr_ref_vector & out_bits) {
TRACE("bit_blaster", tout << n << ": " << sz << " ";
for (unsigned i = 0; i < sz; ++i) {
tout << mk_pp(a_bits[i], m()) << " ";
}
tout << "\n";
);
n = n % sz;
for (unsigned i = sz - n; i < sz; i++)
out_bits.push_back(a_bits[i]);
@ -974,7 +980,7 @@ void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * co
mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out);
out = new_out;
}
TRACE("bit_blaster_tpl<Cfg>", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
out_bits.set(sz - i - 1, out);
}
}
@ -1004,7 +1010,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
out = a_bits[i];
for (unsigned j = 1; j < sz; j++) {
expr_ref new_out(m());
unsigned src = (Left ? (i - j) : (i + j)) % sz;
unsigned src = (Left ? (sz + i - j) : (i + j)) % sz;
mk_ite(eqs.get(j), a_bits[src], out, new_out);
out = new_out;
}

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

@ -21,6 +21,7 @@ Notes:
#include"poly_rewriter_def.h"
#include"ast_smt2_pp.h"
mk_extract_proc::mk_extract_proc(bv_util & u):
m_util(u),
m_high(0),

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

@ -82,7 +82,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
if (num_args == 2) {
mpf_rounding_mode rm;
if (!m_util.is_rm(args[0], rm))
if (!m_util.is_rm_value(args[0], rm))
return BR_FAILED;
rational q;
@ -109,12 +109,12 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
return BR_FAILED;
}
else if (num_args == 3 &&
m_util.is_rm(m().get_sort(args[0])) &&
m_util.is_rm(args[0]) &&
m_util.au().is_real(args[1]) &&
m_util.au().is_int(args[2])) {
mpf_rounding_mode rm;
if (!m_util.is_rm(args[0], rm))
if (!m_util.is_rm_value(args[0], rm))
return BR_FAILED;
rational q;
@ -129,8 +129,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
mpf v;
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
result = m_util.mk_value(v);
m_util.fm().del(v);
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
m_util.fm().del(v);
return BR_DONE;
}
else {
@ -140,7 +139,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) {
if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm());
if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
scoped_mpf t(m_util.fm());
@ -161,7 +160,7 @@ br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref
br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) {
if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm());
if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
scoped_mpf t(m_util.fm());
@ -176,7 +175,7 @@ br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref
br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) {
if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm());
if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
scoped_mpf t(m_util.fm());
@ -287,7 +286,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) {
if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm());
if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3) && m_util.is_value(arg4, v4)) {
scoped_mpf t(m_util.fm());
@ -302,7 +301,7 @@ br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, exp
br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) {
if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm());
if (m_util.is_value(arg2, v2)) {
scoped_mpf t(m_util.fm());
@ -317,7 +316,7 @@ br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
br_status float_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) {
if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm());
if (m_util.is_value(arg2, v2)) {
scoped_mpf t(m_util.fm());

2
src/ast/scoped_proof.h
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifndef _SCOPED_PROOF__H_
#define _SCOPED_PROOF_H_
#define _SCOPED_PROOF__H_
#include "ast.h"

9
src/cmd_context/basic_cmds.cpp
View file

@ -547,6 +547,9 @@ public:
}
};
#define STRINGIZE(x) #x
#define STRINGIZE_VALUE_OF(x) STRINGIZE(x)
class get_info_cmd : public cmd {
symbol m_error_behavior;
symbol m_name;
@ -584,7 +587,11 @@ public:
ctx.regular_stream() << "(:authors \"Leonardo de Moura and Nikolaj Bjorner\")" << std::endl;
}
else if (opt == m_version) {
ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "\")" << std::endl;
ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER
#ifdef Z3GITHASH
<< " - build hashcode " << STRINGIZE_VALUE_OF(Z3GITHASH)
#endif
<< "\")" << std::endl;
}
else if (opt == m_status) {
ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl;

10
src/cmd_context/cmd_context.cpp
View file

@ -346,8 +346,14 @@ cmd_context::~cmd_context() {
}
void cmd_context::set_cancel(bool f) {
if (m_solver)
m_solver->set_cancel(f);
if (m_solver) {
if (f) {
m_solver->cancel();
}
else {
m_solver->reset_cancel();
}
}
if (has_manager())
m().set_cancel(f);
}

3
src/cmd_context/interpolant_cmds.cpp
View file

@ -33,6 +33,7 @@ Notes:
#include"iz3checker.h"
#include"iz3profiling.h"
#include"interp_params.hpp"
#include"scoped_proof.h"
static void show_interpolant_and_maybe_check(cmd_context & ctx,
ptr_vector<ast> &cnsts,
@ -153,7 +154,7 @@ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, par
ast_manager &_m = ctx.m();
// TODO: the following is a HACK to enable proofs in the old smt solver
// When we stop using that solver, this hack can be removed
_m.toggle_proof_mode(PGM_FINE);
scoped_proof_mode spm(_m,PGM_FINE);
ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
p.set_bool("proof", true);
scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());

2
src/cmd_context/pdecl.cpp
View file

@ -189,7 +189,7 @@ class psort_app : public psort {
m.inc_ref(d);
m.inc_ref(num_args, args);
SASSERT(num_args == m_decl->get_num_params() || m_decl->has_var_params());
DEBUG_CODE(for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this););
DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); });
}
virtual void finalize(pdecl_manager & m) {

30
src/duality/duality.h
View file

@ -29,7 +29,7 @@ using namespace stl_ext;
namespace Duality {
class implicant_solver;
struct implicant_solver;
/* Generic operations on Z3 formulas */
@ -253,6 +253,27 @@ protected:
}
void assert_axiom(const expr &axiom){
#if 1
// HACK: large "distict" predicates can kill the legacy SMT solver.
// encode them with a UIF
if(axiom.is_app() && axiom.decl().get_decl_kind() == Distinct)
if(axiom.num_args() > 10){
sort s = axiom.arg(0).get_sort();
std::vector<sort> sv;
sv.push_back(s);
int nargs = axiom.num_args();
std::vector<expr> args(nargs);
func_decl f = ctx->fresh_func_decl("@distinct",sv,ctx->int_sort());
for(int i = 0; i < nargs; i++){
expr a = axiom.arg(i);
expr new_cnstr = f(a) == ctx->int_val(i);
args[i] = new_cnstr;
}
expr cnstr = ctx->make(And,args);
islvr->AssertInterpolationAxiom(cnstr);
return;
}
#endif
islvr->AssertInterpolationAxiom(axiom);
}
@ -1131,6 +1152,13 @@ protected:
virtual void LearnFrom(Solver *old_solver) = 0;
/** Return true if the solution be incorrect due to recursion bounding.
That is, the returned "solution" might contain all derivable facts up to the
given recursion bound, but not be actually a fixed point.
*/
virtual bool IsResultRecursionBounded() = 0;
virtual ~Solver(){}
static Solver *Create(const std::string &solver_class, RPFP *rpfp);

85
src/duality/duality_solver.cpp
View file

@ -100,6 +100,7 @@ namespace Duality {
};
Reporter *CreateStdoutReporter(RPFP *rpfp);
Reporter *CreateConjectureFileReporter(RPFP *rpfp, const std::string &fname);
/** Object we throw in case of catastrophe. */
@ -125,6 +126,7 @@ namespace Duality {
{
rpfp = _rpfp;
reporter = 0;
conj_reporter = 0;
heuristic = 0;
unwinding = 0;
FullExpand = false;
@ -274,6 +276,7 @@ namespace Duality {
RPFP *rpfp; // the input RPFP
Reporter *reporter; // object for logging
Reporter *conj_reporter; // object for logging conjectures
Heuristic *heuristic; // expansion heuristic
context &ctx; // Z3 context
solver &slvr; // Z3 solver
@ -297,6 +300,7 @@ namespace Duality {
int last_decisions;
hash_set<Node *> overapproxes;
std::vector<Proposer *> proposers;
std::string ConjectureFile;
#ifdef BOUNDED
struct Counter {
@ -310,6 +314,7 @@ namespace Duality {
/** Solve the problem. */
virtual bool Solve(){
reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp);
conj_reporter = ConjectureFile.empty() ? 0 : CreateConjectureFileReporter(rpfp,ConjectureFile);
#ifndef LOCALIZE_CONJECTURES
heuristic = !cex.get_tree() ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex);
#else
@ -340,6 +345,8 @@ namespace Duality {
delete heuristic;
// delete unwinding; // keep the unwinding for future mining of predicates
delete reporter;
if(conj_reporter)
delete conj_reporter;
for(unsigned i = 0; i < proposers.size(); i++)
delete proposers[i];
return res;
@ -449,6 +456,9 @@ namespace Duality {
if(option == "recursion_bound"){
return SetIntOption(RecursionBound,value);
}
if(option == "conjecture_file"){
ConjectureFile = value;
}
return false;
}
@ -728,6 +738,13 @@ namespace Duality {
return ctx.constant(name.c_str(),ctx.bool_sort());
}
/** Make a boolean variable to act as a "marker" for a pair of nodes. */
expr NodeMarker(Node *node1, Node *node2){
std::string name = std::string("@m_") + string_of_int(node1->number);
name += std::string("_") + string_of_int(node2->number);
return ctx.constant(name.c_str(),ctx.bool_sort());
}
/** Union the annotation of dst into src. If with_markers is
true, we conjoin the annotation formula of dst with its
marker. This allows us to discover which disjunct is
@ -751,6 +768,29 @@ namespace Duality {
annot.Simplify();
}
bool recursionBounded;
/** See if the solution might be bounded. */
void TestRecursionBounded(){
recursionBounded = false;
if(RecursionBound == -1)
return;
for(unsigned i = 0; i < nodes.size(); i++){
Node *node = nodes[i];
std::vector<Node *> &insts = insts_of_node[node];
for(unsigned j = 0; j < insts.size(); j++)
if(indset->Contains(insts[j]))
if(NodePastRecursionBound(insts[j])){
recursionBounded = true;
return;
}
}
}
bool IsResultRecursionBounded(){
return recursionBounded;
}
/** Generate a proposed solution of the input RPFP from
the unwinding, by unioning the instances of each node. */
void GenSolutionFromIndSet(bool with_markers = false){
@ -1009,6 +1049,7 @@ namespace Duality {
timer_stop("ProduceCandidatesForExtension");
if(candidates.empty()){
GenSolutionFromIndSet();
TestRecursionBounded();
return true;
}
Candidate cand = candidates.front();
@ -1136,19 +1177,19 @@ namespace Duality {
}
void GenNodeSolutionWithMarkersAux(Node *node, RPFP::Transformer &annot, expr &marker_disjunction){
void GenNodeSolutionWithMarkersAux(Node *node, RPFP::Transformer &annot, expr &marker_disjunction, Node *other_node){
#ifdef BOUNDED
if(RecursionBound >= 0 && NodePastRecursionBound(node))
return;
#endif
RPFP::Transformer temp = node->Annotation;
expr marker = NodeMarker(node);
expr marker = (!other_node) ? NodeMarker(node) : NodeMarker(node, other_node);
temp.Formula = (!marker || temp.Formula);
annot.IntersectWith(temp);
marker_disjunction = marker_disjunction || marker;
}
bool GenNodeSolutionWithMarkers(Node *node, RPFP::Transformer &annot, bool expanded_only = false){
bool GenNodeSolutionWithMarkers(Node *node, RPFP::Transformer &annot, bool expanded_only = false, Node *other_node = 0){
bool res = false;
annot.SetFull();
expr marker_disjunction = ctx.bool_val(false);
@ -1156,7 +1197,7 @@ namespace Duality {
for(unsigned j = 0; j < insts.size(); j++){
Node *node = insts[j];
if(indset->Contains(insts[j])){
GenNodeSolutionWithMarkersAux(node, annot, marker_disjunction); res = true;
GenNodeSolutionWithMarkersAux(node, annot, marker_disjunction, other_node); res = true;
}
}
annot.Formula = annot.Formula && marker_disjunction;
@ -1253,7 +1294,7 @@ namespace Duality {
Node *inst = insts[k];
if(indset->Contains(inst)){
if(checker->Empty(node) ||
eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){
eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst,node)),ctx.bool_val(true))){
candidate.Children.push_back(inst);
goto next_child;
}
@ -1336,7 +1377,7 @@ namespace Duality {
for(unsigned j = 0; j < edge->Children.size(); j++){
Node *oc = edge->Children[j];
Node *nc = gen_cands_edge->Children[j];
GenNodeSolutionWithMarkers(oc,nc->Annotation,true);
GenNodeSolutionWithMarkers(oc,nc->Annotation,true,nc);
}
checker->AssertEdge(gen_cands_edge,1,true);
return root;
@ -1462,6 +1503,8 @@ namespace Duality {
bool Update(Node *node, const RPFP::Transformer &fact, bool eager=false){
if(!node->Annotation.SubsetEq(fact)){
reporter->Update(node,fact,eager);
if(conj_reporter)
conj_reporter->Update(node,fact,eager);
indset->Update(node,fact);
updated_nodes.insert(node->map);
node->Annotation.IntersectWith(fact);
@ -2201,7 +2244,7 @@ namespace Duality {
#endif
int expand_max = 1;
if(0&&duality->BatchExpand){
int thing = stack.size() * 0.1;
int thing = stack.size() / 10; // * 0.1;
expand_max = std::max(1,thing);
if(expand_max > 1)
std::cout << "foo!\n";
@ -3043,6 +3086,7 @@ namespace Duality {
};
};
static int stop_event = -1;
class StreamReporter : public Reporter {
std::ostream &s;
@ -3052,6 +3096,9 @@ namespace Duality {
int event;
int depth;
void ev(){
if(stop_event == event){
std::cout << "stop!\n";
}
s << "[" << event++ << "]" ;
}
virtual void Extend(RPFP::Node *node){
@ -3129,4 +3176,28 @@ namespace Duality {
Reporter *CreateStdoutReporter(RPFP *rpfp){
return new StreamReporter(rpfp, std::cout);
}
class ConjectureFileReporter : public Reporter {
std::ofstream s;
public:
ConjectureFileReporter(RPFP *_rpfp, const std::string &fname)
: Reporter(_rpfp), s(fname.c_str()) {}
virtual void Update(RPFP::Node *node, const RPFP::Transformer &update, bool eager){
s << "(define-fun " << node->Name.name() << " (";
for(unsigned i = 0; i < update.IndParams.size(); i++){
if(i != 0)
s << " ";
s << "(" << update.IndParams[i] << " " << update.IndParams[i].get_sort() << ")";
}
s << ") Bool \n";
s << update.Formula << ")\n";
s << std::endl;
}
};
Reporter *CreateConjectureFileReporter(RPFP *rpfp, const std::string &fname){
return new ConjectureFileReporter(rpfp, fname);
}
}

5
src/duality/duality_wrapper.h
View file

@ -397,6 +397,11 @@ namespace Duality {
sort array_domain() const;
sort array_range() const;
friend std::ostream & operator<<(std::ostream & out, sort const & m){
m.ctx().print_expr(out,m);
return out;
}
};

11
src/interp/iz3base.cpp
View file

@ -260,7 +260,7 @@ void iz3base::check_interp(const std::vector<ast> &itps, std::vector<ast> &theor
#endif
}
bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof){
bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof, std::vector<ast> &vars){
params_ref p;
p.set_bool("proof", true); // this is currently useless
@ -277,6 +277,15 @@ bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof){
::ast *proof = s.get_proof();
_proof = cook(proof);
}
else if(vars.size()) {
model_ref(_m);
s.get_model(_m);
for(unsigned i = 0; i < vars.size(); i++){
expr_ref r(m());
_m.get()->eval(to_expr(vars[i].raw()),r,true);
vars[i] = cook(r.get());
}
}
dealloc(m_solver);
return res != l_false;
}

2
src/interp/iz3base.h
View file

@ -113,7 +113,7 @@ class iz3base : public iz3mgr, public scopes {
void check_interp(const std::vector<ast> &itps, std::vector<ast> &theory);
/** For convenience -- is this formula SAT? */
bool is_sat(const std::vector<ast> &consts, ast &_proof);
bool is_sat(const std::vector<ast> &consts, ast &_proof, std::vector<ast> &vars);
/** Interpolator for clauses, to be implemented */
virtual void interpolate_clause(std::vector<ast> &lits, std::vector<ast> &itps){

4
src/interp/iz3hash.h
View file

@ -29,6 +29,10 @@ Revision History:
#ifndef IZ3_HASH_H
#define IZ3_HASH_H
#ifdef _WINDOWS
#pragma warning(disable:4267)
#endif
#include <string>
#include <vector>
#include <iterator>

9
src/interp/iz3interp.cpp
View file

@ -41,6 +41,7 @@ Revision History:
#include "iz3hash.h"
#include "iz3interp.h"
#include"scoped_proof.h"
using namespace stl_ext;
@ -347,8 +348,10 @@ public:
// get the interps for the tree positions
std::vector<ast> _interps = interps;
interps.resize(pos_map.size());
for(unsigned i = 0; i < pos_map.size(); i++)
interps[i] = i < _interps.size() ? _interps[i] : mk_false();
for(unsigned i = 0; i < pos_map.size(); i++){
unsigned j = pos_map[i];
interps[i] = j < _interps.size() ? _interps[j] : mk_false();
}
}
bool has_interp(hash_map<ast,bool> &memo, const ast &t){
@ -501,6 +504,8 @@ lbool iz3interpolate(ast_manager &_m_manager,
return res;
}
void interpolation_options_struct::apply(iz3base &b){
for(stl_ext::hash_map<std::string,std::string>::iterator it = map.begin(), en = map.end();
it != en;

2
src/interp/iz3interp.h
View file

@ -76,6 +76,7 @@ void iz3interpolate(ast_manager &_m_manager,
ptr_vector<ast> &interps,
interpolation_options_struct * options);
/* Compute an interpolant from an ast representing an interpolation
problem, if unsat, else return a model (if enabled). Uses the
given solver to produce the proof/model. Also returns a vector
@ -90,4 +91,5 @@ lbool iz3interpolate(ast_manager &_m_manager,
model_ref &m,
interpolation_options_struct * options);
#endif

5
src/interp/iz3mgr.h
View file

@ -387,10 +387,13 @@ class iz3mgr {
return UnknownTheory;
}
enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,UnknownKind};
enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,ArithMysteryKind,UnknownKind};
lemma_kind get_theory_lemma_kind(const ast &proof){
symb s = sym(proof);
if(s->get_num_parameters() < 2) {
return ArithMysteryKind; // Bad -- Z3 hasn't told us
}
::symbol p0;
bool ok = s->get_parameter(1).is_symbol(p0);
if(!ok) return UnknownKind;

97
src/interp/iz3proof_itp.cpp
View file

@ -607,7 +607,29 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
}
ast distribute_coeff(const ast &coeff, const ast &s){
if(sym(s) == sum){
if(sym(arg(s,2)) == sum)
return make(sum,
distribute_coeff(coeff,arg(s,0)),
make_int(rational(1)),
distribute_coeff(make(Times,coeff,arg(s,1)), arg(s,2)));
else
return make(sum,
distribute_coeff(coeff,arg(s,0)),
make(Times,coeff,arg(s,1)),
arg(s,2));
}
if(op(s) == Leq && arg(s,1) == make_int(rational(0)) && arg(s,2) == make_int(rational(0)))
return s;
return make(sum,make(Leq,make_int(rational(0)),make_int(rational(0))),coeff,s);
}
ast simplify_sum(std::vector<ast> &args){
if(args[1] != make_int(rational(1))){
if(sym(args[2]) == sum)
return make(sum,args[0],make_int(rational(1)),distribute_coeff(args[1],args[2]));
}
ast Aproves = mk_true(), Bproves = mk_true();
ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves);
if(!is_normal_ineq(ineq)) throw cannot_simplify();
@ -757,6 +779,22 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast Bcond = my_implies(Bproves1,my_and(Aproves1,z3_simplify(ineq2)));
// if(!is_true(Aproves1) || !is_true(Bproves1))
// std::cout << "foo!\n";;
if(y == make_int(rational(0)) && op(x) == Plus && num_args(x) == 2){
if(get_term_type(arg(x,0)) == LitA){
ast iter = z3_simplify(make(Plus,arg(x,0),get_ineq_rhs(xleqy)));
ast rewrite1 = make_rewrite(LitA,pos_add(0,top_pos),Acond,make(Equal,arg(x,0),iter));
iter = make(Plus,iter,arg(x,1));
ast rewrite2 = make_rewrite(LitB,top_pos,Bcond,make(Equal,iter,y));
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
}
if(get_term_type(arg(x,1)) == LitA){
ast iter = z3_simplify(make(Plus,arg(x,1),get_ineq_rhs(xleqy)));
ast rewrite1 = make_rewrite(LitA,pos_add(1,top_pos),Acond,make(Equal,arg(x,1),iter));
iter = make(Plus,arg(x,0),iter);
ast rewrite2 = make_rewrite(LitB,top_pos,Bcond,make(Equal,iter,y));
return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
}
}
if(get_term_type(x) == LitA){
ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy)));
ast rewrite1 = make_rewrite(LitA,top_pos,Acond,make(Equal,x,iter));
@ -1014,6 +1052,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
coeff = argpos ? make_int(rational(-1)) : make_int(rational(1));
break;
case Not:
coeff = make_int(rational(-1));
case Plus:
break;
case Times:
@ -2568,12 +2607,17 @@ class iz3proof_itp_impl : public iz3proof_itp {
break;
default: { // mixed equality
if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed){
// std::cerr << "WARNING: mixed term in leq2eq\n";
std::vector<ast> lits;
lits.push_back(con);
lits.push_back(make(Not,xleqy));
lits.push_back(make(Not,yleqx));
return make_axiom(lits);
if(y == make_int(rational(0)) && op(x) == Plus && num_args(x) == 2){
// std::cerr << "WARNING: untested case in leq2eq\n";
}
else {
// std::cerr << "WARNING: mixed term in leq2eq\n";
std::vector<ast> lits;
lits.push_back(con);
lits.push_back(make(Not,xleqy));
lits.push_back(make(Not,yleqx));
return make_axiom(lits);
}
}
std::vector<ast> conjs; conjs.resize(3);
conjs[0] = mk_not(con);
@ -2655,8 +2699,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
};
std::vector<LocVar> localization_vars; // localization vars in order of creation
hash_map<ast,ast> localization_map; // maps terms to their localization vars
hash_map<ast,ast> localization_pf_map; // maps terms to proofs of their localizations
struct locmaps {
hash_map<ast,ast> localization_map; // maps terms to their localization vars
hash_map<ast,ast> localization_pf_map; // maps terms to proofs of their localizations
};
hash_map<prover::range,locmaps> localization_maps_per_range;
/* "localize" a term e to a given frame range, creating new symbols to
represent non-local subterms. This returns the localized version e_l,
@ -2677,7 +2726,24 @@ class iz3proof_itp_impl : public iz3proof_itp {
return make(Equal,x,y);
}
bool range_is_global(const prover::range &r){
if(pv->range_contained(r,rng))
return false;
if(!pv->ranges_intersect(r,rng))
return false;
return true;
}
ast localize_term(ast e, const prover::range &rng, ast &pf){
// we need to memoize this function separately for A, B and global
prover::range map_range = rng;
if(range_is_global(map_range))
map_range = pv->range_full();
locmaps &maps = localization_maps_per_range[map_range];
hash_map<ast,ast> &localization_map = maps.localization_map;
hash_map<ast,ast> &localization_pf_map = maps.localization_pf_map;
ast orig_e = e;
pf = make_refl(e); // proof that e = e
@ -2764,6 +2830,21 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast bar = make_assumption(frame,foo);
pf = make_transitivity(new_var,e,orig_e,bar,pf);
localization_pf_map[orig_e] = pf;
// HACK: try to bias this term in the future
if(!pv->range_is_full(rng)){
prover::range rf = pv->range_full();
locmaps &fmaps = localization_maps_per_range[rf];
hash_map<ast,ast> &flocalization_map = fmaps.localization_map;
hash_map<ast,ast> &flocalization_pf_map = fmaps.localization_pf_map;
// if(flocalization_map.find(orig_e) == flocalization_map.end())
{
flocalization_map[orig_e] = new_var;
flocalization_pf_map[orig_e] = pf;
}
}
return new_var;
}

25
src/interp/iz3scopes.h
View file

@ -23,6 +23,7 @@ Revision History:
#include <vector>
#include <limits.h>
#include "iz3hash.h"
class scopes {
@ -63,6 +64,11 @@ class scopes {
return rng.hi < rng.lo;
}
/** is this range full? */
bool range_is_full(const range &rng){
return rng.lo == SHRT_MIN && rng.hi == SHRT_MAX;
}
/** return an empty range */
range range_empty(){
range res;
@ -194,4 +200,23 @@ class scopes {
};
// let us hash on ranges
#ifndef FULL_TREE
namespace hash_space {
template <>
class hash<scopes::range> {
public:
size_t operator()(const scopes::range &p) const {
return (size_t)p.lo + (size_t)p.hi;
}
};
}
inline bool operator==(const scopes::range &x, const scopes::range &y){
return x.lo == y.lo && x.hi == y.hi;
}
#endif
#endif

218
src/interp/iz3translate.cpp
View file

@ -1058,36 +1058,66 @@ public:
}
rational get_first_coefficient(const ast &t, ast &v){
if(op(t) == Plus){
unsigned best_id = UINT_MAX;
rational best_coeff(0);
int nargs = num_args(t);
for(int i = 0; i < nargs; i++)
if(op(arg(t,i)) != Numeral){
ast lv = get_linear_var(arg(t,i));
unsigned id = ast_id(lv);
if(id < best_id) {
v = lv;
best_id = id;
best_coeff = get_coeff(arg(t,i));
}
}
return best_coeff;
}
else
if(op(t) != Numeral)
return(get_coeff(t));
return rational(0);
}
ast divide_inequalities(const ast &x, const ast&y){
std::vector<rational> xcoeffs,ycoeffs;
get_linear_coefficients(arg(x,1),xcoeffs);
get_linear_coefficients(arg(y,1),ycoeffs);
if(xcoeffs.size() != ycoeffs.size() || xcoeffs.size() == 0)
ast xvar, yvar;
rational xcoeff = get_first_coefficient(arg(x,0),xvar);
rational ycoeff = get_first_coefficient(arg(y,0),yvar);
if(xcoeff == rational(0) || ycoeff == rational(0) || xvar != yvar)
throw "bad assign-bounds lemma";
rational ratio = xcoeff/ycoeff;
if(denominator(ratio) != rational(1))
throw "bad assign-bounds lemma";
rational ratio = xcoeffs[0]/ycoeffs[0];
return make_int(ratio); // better be integer!
}
ast AssignBounds2Farkas(const ast &proof, const ast &con){
std::vector<ast> farkas_coeffs;
get_assign_bounds_coeffs(proof,farkas_coeffs);
std::vector<ast> lits;
int nargs = num_args(con);
if(nargs != (int)(farkas_coeffs.size()))
throw "bad assign-bounds theory lemma";
#if 0
for(int i = 1; i < nargs; i++)
lits.push_back(mk_not(arg(con,i)));
ast sum = sum_inequalities(farkas_coeffs,lits);
ast conseq = rhs_normalize_inequality(arg(con,0));
ast d = divide_inequalities(sum,conseq);
std::vector<ast> my_coeffs;
my_coeffs.push_back(d);
for(unsigned i = 0; i < farkas_coeffs.size(); i++)
my_coeffs.push_back(farkas_coeffs[i]);
if(farkas_coeffs[0] != make_int(rational(1)))
farkas_coeffs[0] = make_int(rational(1));
#else
std::vector<ast> my_coeffs;
std::vector<ast> lits, lit_coeffs;
for(int i = 1; i < nargs; i++){
lits.push_back(mk_not(arg(con,i)));
lit_coeffs.push_back(farkas_coeffs[i]);
}
ast sum = normalize_inequality(sum_inequalities(lit_coeffs,lits));
ast conseq = normalize_inequality(arg(con,0));
ast d = divide_inequalities(sum,conseq);
#if 0
if(d != farkas_coeffs[0])
std::cout << "wow!\n";
#endif
farkas_coeffs[0] = d;
#endif
std::vector<ast> my_coeffs;
std::vector<ast> my_cons;
for(int i = 1; i < nargs; i++){
my_cons.push_back(mk_not(arg(con,i)));
@ -1107,10 +1137,27 @@ public:
ast AssignBoundsRule2Farkas(const ast &proof, const ast &con, std::vector<Iproof::node> prems){
std::vector<ast> farkas_coeffs;
get_assign_bounds_rule_coeffs(proof,farkas_coeffs);
std::vector<ast> lits;
int nargs = num_prems(proof)+1;
if(nargs != (int)(farkas_coeffs.size()))
throw "bad assign-bounds theory lemma";
#if 0
if(farkas_coeffs[0] != make_int(rational(1)))
farkas_coeffs[0] = make_int(rational(1));
#else
std::vector<ast> lits, lit_coeffs;
for(int i = 1; i < nargs; i++){
lits.push_back(conc(prem(proof,i-1)));
lit_coeffs.push_back(farkas_coeffs[i]);
}
ast sum = normalize_inequality(sum_inequalities(lit_coeffs,lits));
ast conseq = normalize_inequality(con);
ast d = divide_inequalities(sum,conseq);
#if 0
if(d != farkas_coeffs[0])
std::cout << "wow!\n";
#endif
farkas_coeffs[0] = d;
#endif
std::vector<ast> my_coeffs;
std::vector<ast> my_cons;
for(int i = 1; i < nargs; i++){
@ -1278,6 +1325,17 @@ public:
return make(Plus,args);
}
void get_sum_as_vector(const ast &t, std::vector<rational> &coeffs, std::vector<ast> &vars){
if(!(op(t) == Plus)){
coeffs.push_back(get_coeff(t));
vars.push_back(get_linear_var(t));
}
else {
int nargs = num_args(t);
for(int i = 0; i < nargs; i++)
get_sum_as_vector(arg(t,i),coeffs,vars);
}
}
ast replace_summands_with_fresh_vars(const ast &t, hash_map<ast,ast> &map){
if(op(t) == Plus){
@ -1294,6 +1352,99 @@ public:
return map[t];
}
rational lcd(const std::vector<rational> &rats){
rational res = rational(1);
for(unsigned i = 0; i < rats.size(); i++){
res = lcm(res,denominator(rats[i]));
}
return res;
}
Iproof::node reconstruct_farkas_with_dual(const std::vector<ast> &prems, const std::vector<Iproof::node> &pfs, const ast &con){
int nprems = prems.size();
std::vector<ast> npcons(nprems);
hash_map<ast,ast> pain_map; // not needed
for(int i = 0; i < nprems; i++){
npcons[i] = painfully_normalize_ineq(conc(prems[i]),pain_map);
if(op(npcons[i]) == Lt){
ast constval = z3_simplify(make(Sub,arg(npcons[i],1),make_int(rational(1))));
npcons[i] = make(Leq,arg(npcons[i],0),constval);
}
}
ast ncon = painfully_normalize_ineq(mk_not(con),pain_map);
npcons.push_back(ncon);
hash_map<ast,ast> dual_map;
std::vector<ast> cvec, vars_seen;
ast rhs = make_real(rational(0));
for(unsigned i = 0; i < npcons.size(); i++){
ast c= mk_fresh_constant("@c",real_type());
cvec.push_back(c);
ast lhs = arg(npcons[i],0);
std::vector<rational> coeffs;
std::vector<ast> vars;
get_sum_as_vector(lhs,coeffs,vars);
for(unsigned j = 0; j < coeffs.size(); j++){
rational coeff = coeffs[j];
ast var = vars[j];
if(dual_map.find(var) == dual_map.end()){
dual_map[var] = make_real(rational(0));
vars_seen.push_back(var);
}
ast foo = make(Plus,dual_map[var],make(Times,make_real(coeff),c));
dual_map[var] = foo;
}
rhs = make(Plus,rhs,make(Times,c,arg(npcons[i],1)));
}
std::vector<ast> cnstrs;
for(unsigned i = 0; i < vars_seen.size(); i++)
cnstrs.push_back(make(Equal,dual_map[vars_seen[i]],make_real(rational(0))));
cnstrs.push_back(make(Leq,rhs,make_real(rational(0))));
for(unsigned i = 0; i < cvec.size() - 1; i++)
cnstrs.push_back(make(Geq,cvec[i],make_real(rational(0))));
cnstrs.push_back(make(Equal,cvec.back(),make_real(rational(1))));
ast new_proof;
// greedily reduce the core
for(unsigned i = 0; i < cvec.size() - 1; i++){
std::vector<ast> dummy;
cnstrs.push_back(make(Equal,cvec[i],make_real(rational(0))));
if(!is_sat(cnstrs,new_proof,dummy))
cnstrs.pop_back();
}
std::vector<ast> vals = cvec;
if(!is_sat(cnstrs,new_proof,vals))
throw "Proof error!";
std::vector<rational> rat_farkas_coeffs;
for(unsigned i = 0; i < cvec.size(); i++){
ast bar = vals[i];
rational r;
if(is_numeral(bar,r))
rat_farkas_coeffs.push_back(r);
else
throw "Proof error!";
}
rational the_lcd = lcd(rat_farkas_coeffs);
std::vector<ast> farkas_coeffs;
std::vector<Iproof::node> my_prems;
std::vector<ast> my_pcons;
for(unsigned i = 0; i < prems.size(); i++){
ast fc = make_int(rat_farkas_coeffs[i] * the_lcd);
if(!(fc == make_int(rational(0)))){
farkas_coeffs.push_back(fc);
my_prems.push_back(pfs[i]);
my_pcons.push_back(conc(prems[i]));
}
}
farkas_coeffs.push_back(make_int(the_lcd));
my_prems.push_back(iproof->make_hypothesis(mk_not(con)));
my_pcons.push_back(mk_not(con));
Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
return res;
}
ast painfully_normalize_ineq(const ast &ineq, hash_map<ast,ast> &map){
ast res = normalize_inequality(ineq);
ast lhs = arg(res,0);
@ -1318,7 +1469,8 @@ public:
npcons.push_back(ncon);
// ast assumps = make(And,pcons);
ast new_proof;
if(is_sat(npcons,new_proof))
std::vector<ast> dummy;
if(is_sat(npcons,new_proof,dummy))
throw "Proof error!";
pfrule dk = pr(new_proof);
int nnp = num_prems(new_proof);
@ -1334,7 +1486,7 @@ public:
farkas_coeffs.push_back(make_int(rational(1)));
}
else
throw "cannot reconstruct farkas proof";
return reconstruct_farkas_with_dual(prems,pfs,con);
for(int i = 0; i < nnp; i++){
ast p = conc(prem(new_proof,i));
@ -1348,7 +1500,7 @@ public:
my_pcons.push_back(mk_not(con));
}
else
throw "cannot reconstruct farkas proof";
return reconstruct_farkas_with_dual(prems,pfs,con);
}
Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
return res;
@ -1378,7 +1530,8 @@ public:
npcons.push_back(ncon);
// ast assumps = make(And,pcons);
ast new_proof;
if(is_sat(npcons,new_proof))
std::vector<ast> dummy;
if(is_sat(npcons,new_proof,dummy))
throw "Proof error!";
pfrule dk = pr(new_proof);
int nnp = num_prems(new_proof);
@ -1408,7 +1561,7 @@ public:
my_pcons.push_back(mk_not(con));
}
else
throw "cannot reconstruct farkas proof";
return painfully_reconstruct_farkas(prems,pfs,con);
}
Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
return res;
@ -1433,6 +1586,12 @@ public:
return res;
}
ast ArithMysteryRule(const ast &con, const std::vector<ast> &prems, const std::vector<Iproof::node> &args){
// Hope for the best!
Iproof::node guess = reconstruct_farkas(prems,args,con);
return guess;
}
struct CannotCombineEqPropagate {};
void CombineEqPropagateRec(const ast &proof, std::vector<ast> &prems, std::vector<Iproof::node> &args, ast &eqprem){
@ -1552,6 +1711,13 @@ public:
if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or)
std::cout << "foo!\n";
// no idea why this shows up
if(dk == PR_MODUS_PONENS_OEQ)
if(conc(prem(proof,0)) == con){
res = translate_main(prem(proof,0),expect_clause);
return res;
}
#if 0
if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
Iproof::node clause = translate_main(prem(proof,0),true);
@ -1737,6 +1903,14 @@ public:
res = EqPropagate(con,prems,args);
break;
}
case ArithMysteryKind: {
// Z3 hasn't told us what kind of lemma this is -- maybe we can guess
std::vector<ast> prems(nprems);
for(unsigned i = 0; i < nprems; i++)
prems[i] = prem(proof,i);
res = ArithMysteryRule(con,prems,args);
break;
}
default:
throw unsupported();
}

4
src/model/model.cpp
View file

@ -133,7 +133,9 @@ bool model::eval(expr * e, expr_ref & result, bool model_completion) {
ev(e, result);
return true;
}
catch (model_evaluator_exception &) {
catch (model_evaluator_exception & ex) {
(void)ex;
TRACE("model_evaluator", tout << ex.msg() << "\n";);
return false;
}
}

9
src/muz/base/dl_context.h
View file

@ -53,6 +53,7 @@ namespace datalog {
MEMOUT,
INPUT_ERROR,
APPROX,
BOUNDED,
CANCELED
};
@ -278,6 +279,12 @@ namespace datalog {
void register_variable(func_decl* var);
/*
Replace constants that have been registered as
variables by de-Bruijn indices and corresponding
universal (if is_forall is true) or existential
quantifier.
*/
expr_ref bind_variables(expr* fml, bool is_forall);
/**
@ -298,6 +305,8 @@ namespace datalog {
\brief Retrieve predicates
*/
func_decl_set const& get_predicates() const { return m_preds; }
ast_ref_vector const &get_pinned() const {return m_pinned; }
bool is_predicate(func_decl* pred) const { return m_preds.contains(pred); }
bool is_predicate(expr * e) const { return is_app(e) && is_predicate(to_app(e)->get_decl()); }

5
src/muz/base/dl_rule.cpp
View file

@ -978,13 +978,14 @@ namespace datalog {
}
}
void rule::get_vars(ptr_vector<sort>& sorts) const {
void rule::get_vars(ast_manager& m, ptr_vector<sort>& sorts) const {
sorts.reset();
used_vars used;
get_used_vars(used);
unsigned sz = used.get_max_found_var_idx_plus_1();
for (unsigned i = 0; i < sz; ++i) {
sorts.push_back(used.get(i));
sort* s = used.get(i);
sorts.push_back(s?s:m.mk_bool_sort());
}
}

2
src/muz/base/dl_rule.h
View file

@ -304,7 +304,7 @@ namespace datalog {
void norm_vars(rule_manager & rm);
void get_vars(ptr_vector<sort>& sorts) const;
void get_vars(ast_manager& m, ptr_vector<sort>& sorts) const;
void to_formula(expr_ref& result) const;

2
src/muz/base/dl_util.cpp
View file

@ -290,7 +290,7 @@ namespace datalog {
}
}
TRACE("dl_dr",
tout << r.get_decl()->get_name() << "\n";
tout << mk_pp(r.get_head(), m) << " :- \n";
for (unsigned i = 0; i < body.size(); ++i) {
tout << mk_pp(body[i].get(), m) << "\n";
});

1
src/muz/base/fixedpoint_params.pyg
View file

@ -77,6 +77,7 @@ def_module_params('fixedpoint',
('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'),
('batch_expand', BOOL, False, 'DUALITY: use batch expansion'),
('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
('conjecture_file', STRING, '', 'DUALITY: save conjectures to file'),
))

10
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -148,7 +148,7 @@ namespace datalog {
void mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) {
ptr_vector<sort> sorts;
r.get_vars(sorts);
r.get_vars(m, sorts);
// populate substitution of bound variables.
sub.reset();
sub.resize(sorts.size());
@ -421,7 +421,7 @@ namespace datalog {
ptr_vector<sort> rule_vars;
expr_ref_vector args(m), conjs(m);
r.get_vars(rule_vars);
r.get_vars(m, rule_vars);
obj_hashtable<expr> used_vars;
unsigned num_vars = 0;
for (unsigned i = 0; i < r.get_decl()->get_arity(); ++i) {
@ -514,7 +514,7 @@ namespace datalog {
unsigned sz = r->get_uninterpreted_tail_size();
ptr_vector<sort> rule_vars;
r->get_vars(rule_vars);
r->get_vars(m, rule_vars);
args.append(prop->get_num_args(), prop->get_args());
expr_ref_vector sub = mk_skolem_binding(*r, rule_vars, args);
if (sub.empty() && sz == 0) {
@ -803,7 +803,7 @@ namespace datalog {
func_decl* p = r.get_decl();
ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m.get_sort(path));
// populate substitution of bound variables.
r.get_vars(sorts);
r.get_vars(m, sorts);
sub.reset();
sub.resize(sorts.size());
for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) {
@ -1327,7 +1327,7 @@ namespace datalog {
void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub) {
ptr_vector<sort> sorts;
r.get_vars(sorts);
r.get_vars(m, sorts);
// populate substitution of bound variables.
sub.reset();
sub.resize(sorts.size());

76
src/muz/duality/duality_dl_interface.cpp
View file

@ -35,6 +35,8 @@ Revision History:
#include "model_smt2_pp.h"
#include "model_v2_pp.h"
#include "fixedpoint_params.hpp"
#include "used_vars.h"
#include "func_decl_dependencies.h"
// template class symbol_table<family_id>;
@ -164,6 +166,20 @@ lbool dl_interface::query(::expr * query) {
clauses.push_back(e);
}
std::vector<sort> b_sorts;
std::vector<symbol> b_names;
used_vars uv;
uv.process(query);
unsigned nuv = uv.get_max_found_var_idx_plus_1();
for(int i = nuv-1; i >= 0; i--){ // var indices are backward
::sort * s = uv.get(i);
if(!s)
s = _d->ctx.m().mk_bool_sort(); // missing var, whatever
b_sorts.push_back(sort(_d->ctx,s));
b_names.push_back(symbol(_d->ctx,::symbol(i))); // names?
}
#if 0
// turn the query into a clause
expr q(_d->ctx,m_ctx.bind_variables(query,false));
@ -177,6 +193,9 @@ lbool dl_interface::query(::expr * query) {
}
q = q.arg(0);
}
#else
expr q(_d->ctx,query);
#endif
expr qc = implies(q,_d->ctx.bool_val(false));
qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc);
@ -189,6 +208,46 @@ lbool dl_interface::query(::expr * query) {
_d->rpfp->AssertAxiom(e);
}
// make sure each predicate is the head of at least one clause
func_decl_set heads;
for(unsigned i = 0; i < clauses.size(); i++){
expr cl = clauses[i];
while(true){
if(cl.is_app()){
decl_kind k = cl.decl().get_decl_kind();
if(k == Implies)
cl = cl.arg(1);
else {
heads.insert(cl.decl());
break;
}
}
else if(cl.is_quantifier())
cl = cl.body();
else break;
}
}
ast_ref_vector const &pinned = m_ctx.get_pinned();
for(unsigned i = 0; i < pinned.size(); i++){
::ast *fa = pinned[i];
if(is_func_decl(fa)){
::func_decl *fd = to_func_decl(fa);
if(m_ctx.is_predicate(fd)) {
func_decl f(_d->ctx,fd);
if(!heads.contains(fd)){
int arity = f.arity();
std::vector<expr> args;
for(int j = 0; j < arity; j++)
args.push_back(_d->ctx.fresh_func_decl("X",f.domain(j))());
expr c = implies(_d->ctx.bool_val(false),f(args));
c = _d->ctx.make_quant(Forall,args,c);
clauses.push_back(c);
}
}
}
}
// creates 1-1 map between clauses and rpfp edges
_d->rpfp->FromClauses(clauses);
@ -211,6 +270,7 @@ lbool dl_interface::query(::expr * query) {
rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0");
rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file());
unsigned rb = m_ctx.get_params().recursion_bound();
if(rb != UINT_MAX){
std::ostringstream os; os << rb;
@ -246,7 +306,19 @@ lbool dl_interface::query(::expr * query) {
// dealloc(rs); this is now owned by data
// true means the RPFP problem is SAT, so the query is UNSAT
return ans ? l_false : l_true;
// but we return undef if the UNSAT result is bounded
if(ans){
if(rs->IsResultRecursionBounded()){
#if 0
m_ctx.set_status(datalog::BOUNDED);
return l_undef;
#else
return l_false;
#endif
}
return l_false;
}
return l_true;
}
expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) {
@ -350,7 +422,9 @@ void dl_interface::display_certificate_non_const(std::ostream& out) {
if(_d->status == StatusModel){
ast_manager &m = m_ctx.get_manager();
model_ref md = get_model();
out << "(fixedpoint \n";
model_smt2_pp(out, m, *md.get(), 0);
out << ")\n";
}
else if(_d->status == StatusRefutation){
out << "(derivation\n";

5
src/muz/fp/dl_cmds.cpp
View file

@ -252,6 +252,11 @@ public:
print_certificate(ctx);
break;
case l_undef:
if(dlctx.get_status() == datalog::BOUNDED){
ctx.regular_stream() << "bounded\n";
print_certificate(ctx);
break;
}
ctx.regular_stream() << "unknown\n";
switch(dlctx.get_status()) {
case datalog::INPUT_ERROR:

68
src/muz/pdr/pdr_context.cpp
View file

@ -47,6 +47,7 @@ Notes:
#include "dl_boogie_proof.h"
#include "qe_util.h"
#include "scoped_proof.h"
#include "expr_safe_replace.h"
namespace pdr {
@ -736,6 +737,11 @@ namespace pdr {
m_closed = true;
}
void model_node::reopen() {
SASSERT(m_closed);
m_closed = false;
}
static bool is_ini(datalog::rule const& r) {
return r.get_uninterpreted_tail_size() == 0;
}
@ -745,6 +751,7 @@ namespace pdr {
return const_cast<datalog::rule*>(m_rule);
}
// only initial states are not set by the PDR search.
SASSERT(m_model.get());
datalog::rule const& rl1 = pt().find_rule(*m_model);
if (is_ini(rl1)) {
set_rule(&rl1);
@ -864,9 +871,10 @@ namespace pdr {
}
void model_search::add_leaf(model_node& n) {
unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value;
++count;
if (count == 1 || is_repeated(n)) {
model_nodes ns;
model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value;
nodes.push_back(&n);
if (nodes.size() == 1 || is_repeated(n)) {
set_leaf(n);
}
else {
@ -875,7 +883,7 @@ namespace pdr {
}
void model_search::set_leaf(model_node& n) {
erase_children(n);
erase_children(n, true);
SASSERT(n.is_open());
enqueue_leaf(n);
}
@ -897,7 +905,7 @@ namespace pdr {
set_leaf(*root);
}
obj_map<expr, unsigned>& model_search::cache(model_node const& n) {
obj_map<expr, ptr_vector<model_node> >& model_search::cache(model_node const& n) {
unsigned l = n.orig_level();
if (l >= m_cache.size()) {
m_cache.resize(l + 1);
@ -905,7 +913,7 @@ namespace pdr {
return m_cache[l];
}
void model_search::erase_children(model_node& n) {
void model_search::erase_children(model_node& n, bool backtrack) {
ptr_vector<model_node> todo, nodes;
todo.append(n.children());
erase_leaf(n);
@ -916,13 +924,20 @@ namespace pdr {
nodes.push_back(m);
todo.append(m->children());
erase_leaf(*m);
remove_node(*m);
remove_node(*m, backtrack);
}
std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>());
}
void model_search::remove_node(model_node& n) {
if (0 == --cache(n).find(n.state())) {
void model_search::remove_node(model_node& n, bool backtrack) {
model_nodes& nodes = cache(n).find(n.state());
nodes.erase(&n);
if (nodes.size() > 0 && n.is_open() && backtrack) {
for (unsigned i = 0; i < nodes.size(); ++i) {
nodes[i]->reopen();
}
}
if (nodes.empty()) {
cache(n).remove(n.state());
}
}
@ -1048,10 +1063,7 @@ namespace pdr {
predicates.pop_back();
for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) {
subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
dctx.get_rewriter()(tmp);
if (!m.is_true(tmp)) {
constraints.push_back(tmp);
}
constraints.push_back(tmp);
}
for (unsigned i = 0; i < constraints.size(); ++i) {
max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
@ -1074,7 +1086,28 @@ namespace pdr {
children.append(n->children());
}
return pm.mk_and(constraints);
expr_safe_replace repl(m);
for (unsigned i = 0; i < constraints.size(); ++i) {
expr* e = constraints[i].get(), *e1, *e2;
if (m.is_eq(e, e1, e2) && is_var(e1) && is_ground(e2)) {
repl.insert(e1, e2);
}
else if (m.is_eq(e, e1, e2) && is_var(e2) && is_ground(e1)) {
repl.insert(e2, e1);
}
}
expr_ref_vector result(m);
for (unsigned i = 0; i < constraints.size(); ++i) {
expr_ref tmp(m);
tmp = constraints[i].get();
repl(tmp);
dctx.get_rewriter()(tmp);
if (!m.is_true(tmp)) {
result.push_back(tmp);
}
}
return pm.mk_and(result);
}
proof_ref model_search::get_proof_trace(context const& ctx) {
@ -1203,10 +1236,11 @@ namespace pdr {
void model_search::reset() {
if (m_root) {
erase_children(*m_root);
remove_node(*m_root);
erase_children(*m_root, false);
remove_node(*m_root, false);
dealloc(m_root);
m_root = 0;
m_cache.reset();
}
}
@ -1240,7 +1274,7 @@ namespace pdr {
m_pm(m_fparams, params.max_num_contexts(), m),
m_query_pred(m),
m_query(0),
m_search(m_params.bfs_model_search()),
m_search(m_params.bfs_model_search(), m),
m_last_result(l_undef),
m_inductive_lvl(0),
m_expanded_lvl(0),

13
src/muz/pdr/pdr_context.h
View file

@ -231,6 +231,7 @@ namespace pdr {
}
void set_closed();
void reopen();
void set_pre_closed() { m_closed = true; }
void reset() { m_children.reset(); }
@ -243,19 +244,21 @@ namespace pdr {
};
class model_search {
typedef ptr_vector<model_node> model_nodes;
ast_manager& m;
bool m_bfs;
model_node* m_root;
std::deque<model_node*> m_leaves;
vector<obj_map<expr, unsigned> > m_cache;
vector<obj_map<expr, model_nodes > > m_cache;
obj_map<expr, unsigned>& cache(model_node const& n);
void erase_children(model_node& n);
obj_map<expr, model_nodes>& cache(model_node const& n);
void erase_children(model_node& n, bool backtrack);
void erase_leaf(model_node& n);
void remove_node(model_node& n);
void remove_node(model_node& n, bool backtrack);
void enqueue_leaf(model_node& n); // add leaf to priority queue.
void update_models();
public:
model_search(bool bfs): m_bfs(bfs), m_root(0) {}
model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {}
~model_search();
void reset();

2
src/muz/transforms/dl_mk_array_blast.cpp
View file

@ -87,7 +87,7 @@ namespace datalog {
else {
if (m_next_var == 0) {
ptr_vector<sort> vars;
r.get_vars(vars);
r.get_vars(m, vars);
m_next_var = vars.size() + 1;
}
v = m.mk_var(m_next_var, m.get_sort(e));

14
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -26,6 +26,7 @@ Revision History:
#include "dl_mk_interp_tail_simplifier.h"
#include "fixedpoint_params.hpp"
#include "scoped_proof.h"
#include "model_v2_pp.h"
namespace datalog {
@ -67,11 +68,17 @@ namespace datalog {
func_decl* p = m_new_funcs[i].get();
func_decl* q = m_old_funcs[i].get();
func_interp* f = model->get_func_interp(p);
if (!f) continue;
expr_ref body(m);
unsigned arity_p = p->get_arity();
unsigned arity_q = q->get_arity();
TRACE("dl",
model_v2_pp(tout, *model);
tout << mk_pp(p, m) << "\n";
tout << mk_pp(q, m) << "\n";);
SASSERT(0 < arity_p);
model->register_decl(p, f);
SASSERT(f);
model->register_decl(p, f->copy());
func_interp* g = alloc(func_interp, m, arity_q);
if (f) {
@ -88,11 +95,12 @@ namespace datalog {
for (unsigned j = 0; j < arity_q; ++j) {
sort* s = q->get_domain(j);
arg = m.mk_var(j, s);
expr* t = arg;
if (m_bv.is_bv_sort(s)) {
expr* args[1] = { arg };
unsigned sz = m_bv.get_bv_size(s);
for (unsigned k = 0; k < sz; ++k) {
proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, args);
parameter p(k);
proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &t);
sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj);
}
}

6
src/muz/transforms/dl_mk_coalesce.cpp
View file

@ -62,7 +62,7 @@ namespace datalog {
rule_ref r(const_cast<rule*>(&rl), rm);
ptr_vector<sort> sorts;
expr_ref_vector revsub(m), conjs(m);
rl.get_vars(sorts);
rl.get_vars(m, sorts);
revsub.resize(sorts.size());
svector<bool> valid(sorts.size(), true);
for (unsigned i = 0; i < sub.size(); ++i) {
@ -117,8 +117,8 @@ namespace datalog {
rule_ref res(rm);
bool_rewriter bwr(m);
svector<bool> is_neg;
tgt->get_vars(sorts1);
src.get_vars(sorts2);
tgt->get_vars(m, sorts1);
src.get_vars(m, sorts2);
mk_pred(head, src.get_head(), tgt->get_head());
for (unsigned i = 0; i < src.get_uninterpreted_tail_size(); ++i) {

17
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -200,7 +200,22 @@ namespace datalog {
func_decl_set::iterator it = pruned_preds.begin();
extension_model_converter* mc0 = alloc(extension_model_converter, m);
for (; it != end; ++it) {
mc0->insert(*it, m.mk_true());
const rule_vector& rules = source.get_predicate_rules(*it);
expr_ref_vector fmls(m);
for (unsigned i = 0; i < rules.size(); ++i) {
app* head = rules[i]->get_head();
expr_ref_vector conj(m);
for (unsigned j = 0; j < head->get_num_args(); ++j) {
expr* arg = head->get_arg(j);
if (!is_var(arg)) {
conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg));
}
}
fmls.push_back(m.mk_and(conj.size(), conj.c_ptr()));
}
expr_ref fml(m);
fml = m.mk_or(fmls.size(), fmls.c_ptr());
mc0->insert(*it, fml);
}
m_context.add_model_converter(mc0);
}

5
src/muz/transforms/dl_mk_quantifier_instantiation.cpp
View file

@ -199,7 +199,7 @@ namespace datalog {
expr_ref fml(m), cnst(m);
var_ref var(m);
ptr_vector<sort> sorts;
r.get_vars(sorts);
r.get_vars(m, sorts);
m_uf.reset();
m_terms.reset();
m_var2cnst.reset();
@ -207,9 +207,6 @@ namespace datalog {
fml = m.mk_and(conjs.size(), conjs.c_ptr());
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
var = m.mk_var(i, sorts[i]);
cnst = m.mk_fresh_const("C", sorts[i]);
m_var2cnst.insert(var, cnst);

10
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -143,11 +143,8 @@ namespace datalog {
expr_ref_vector result(m);
ptr_vector<sort> sorts;
expr_ref v(m), w(m);
r.get_vars(sorts);
r.get_vars(m, sorts);
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
v = m.mk_var(i, sorts[i]);
m_subst.apply(2, m_deltas, expr_offset(v, is_tgt?0:1), w);
result.push_back(w);
@ -423,6 +420,11 @@ namespace datalog {
}
TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules; );
for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
rule* r = m_inlined_rules.get_rule(i);
datalog::del_rule(m_mc, *r);
}
}
bool mk_rule_inliner::transform_rule(rule_set const& orig, rule * r0, rule_set& tgt) {

2
src/muz/transforms/dl_mk_scale.cpp
View file

@ -141,7 +141,7 @@ namespace datalog {
m_cache.reset();
m_trail.reset();
m_eqs.reset();
r.get_vars(vars);
r.get_vars(m, vars);
unsigned num_vars = vars.size();
for (unsigned j = 0; j < utsz; ++j) {
tail.push_back(mk_pred(num_vars, r.get_tail(j)));

115
src/qe/qe.cpp
View file

@ -1120,6 +1120,7 @@ namespace qe {
st->init(fml);
st->m_vars.append(m_vars.size(), m_vars.c_ptr());
SASSERT(invariant());
TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(fml, m) << "\n";);
return st;
}
@ -1133,6 +1134,7 @@ namespace qe {
m_branch_index.insert(branch_id, index);
st->m_vars.append(m_vars.size(), m_vars.c_ptr());
SASSERT(invariant());
//TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(st->fml(), m) << "\n";);
return st;
}
@ -1164,6 +1166,16 @@ namespace qe {
}
}
expr_ref abstract_variable(app* x, expr* fml) const {
expr_ref result(m);
expr* y = x;
expr_abstract(m, 0, 1, &y, fml, result);
symbol X(x->get_decl()->get_name());
sort* s = m.get_sort(x);
result = m.mk_exists(1, &s, &X, result);
return result;
}
void display_validate(std::ostream& out) const {
if (m_children.empty()) {
return;
@ -1171,25 +1183,53 @@ namespace qe {
expr_ref q(m);
expr* x = m_var;
if (x) {
expr_abstract(m, 0, 1, &x, m_fml, q);
ptr_vector<expr> fmls;
q = abstract_variable(m_var, m_fml);
expr_ref_vector fmls(m);
expr_ref fml(m);
for (unsigned i = 0; i < m_children.size(); ++i) {
expr* fml = m_children[i]->fml();
search_tree const& child = *m_children[i];
fml = child.fml();
if (fml) {
// abstract free variables in children.
ptr_vector<app> child_vars, new_vars;
child_vars.append(child.m_vars.size(), child.m_vars.c_ptr());
if (child.m_var) {
child_vars.push_back(child.m_var);
}
for (unsigned j = 0; j < child_vars.size(); ++j) {
if (!m_vars.contains(child_vars[j]) &&
!new_vars.contains(child_vars[j])) {
fml = abstract_variable(child_vars[j], fml);
new_vars.push_back(child_vars[j]);
}
}
fmls.push_back(fml);
}
}
symbol X(m_var->get_decl()->get_name());
sort* s = m.get_sort(x);
q = m.mk_exists(1, &s, &X, q);
expr_ref tmp(m);
bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), tmp);
expr_ref f(m.mk_not(m.mk_iff(q, tmp)), m);
bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), fml);
fml = m.mk_not(m.mk_iff(q, fml));
ast_smt_pp pp(m);
out << "(echo " << m_var->get_decl()->get_name() << ")\n";
out << "; eliminate " << mk_pp(m_var, m) << "\n";
out << "(push)\n";
pp.display_smt2(out, f);
pp.display_smt2(out, fml);
out << "(pop)\n\n";
DEBUG_CODE(
smt_params params;
params.m_simplify_bit2int = true;
params.m_arith_enum_const_mod = true;
params.m_bv_enable_int2bv2int = true;
params.m_relevancy_lvl = 0;
smt::kernel ctx(m, params);
ctx.assert_expr(fml);
lbool is_sat = ctx.check();
if (is_sat == l_true) {
std::cout << "; Validation failed:\n";
std::cout << mk_pp(fml, m) << "\n";
}
);
}
for (unsigned i = 0; i < m_children.size(); ++i) {
if (m_children[i]->fml()) {
@ -1410,13 +1450,9 @@ namespace qe {
m_solver.assert_expr(m_fml);
if (assumption) m_solver.assert_expr(assumption);
bool is_sat = false;
while (l_false != m_solver.check()) {
while (l_true == m_solver.check()) {
is_sat = true;
model_ref model;
m_solver.get_model(model);
TRACE("qe", model_v2_pp(tout, *model););
model_evaluator model_eval(*model);
final_check(model_eval);
final_check();
}
if (!is_sat) {
@ -1466,14 +1502,30 @@ namespace qe {
private:
void final_check(model_evaluator& model_eval) {
TRACE("qe", tout << "\n";);
while (can_propagate_assignment(model_eval)) {
propagate_assignment(model_eval);
}
VERIFY(CHOOSE_VAR == update_current(model_eval, true));
SASSERT(m_current->fml());
pop(model_eval);
void final_check() {
model_ref model;
m_solver.get_model(model);
scoped_ptr<model_evaluator> model_eval = alloc(model_evaluator, *model);
while (true) {
TRACE("qe", model_v2_pp(tout, *model););
while (can_propagate_assignment(*model_eval)) {
propagate_assignment(*model_eval);
}
VERIFY(CHOOSE_VAR == update_current(*model_eval, true));
SASSERT(m_current->fml());
if (l_true != m_solver.check()) {
return;
}
m_solver.get_model(model);
model_eval = alloc(model_evaluator, *model);
search_tree* st = m_current;
update_current(*model_eval, false);
if (st == m_current) {
break;
}
}
pop(*model_eval);
}
ast_manager& get_manager() { return m; }
@ -1633,6 +1685,7 @@ namespace qe {
nb = m_current->get_num_branches();
expr_ref fml(m_current->fml(), m);
if (!eval(model_eval, b, branch) || branch >= nb) {
TRACE("qe", tout << "evaluation failed: setting branch to 0\n";);
branch = rational::zero();
}
SASSERT(!branch.is_neg());
@ -1694,11 +1747,12 @@ namespace qe {
}
//
// The current state is satisfiable
// and the closed portion of the formula
// can be used as the quantifier-free portion.
// The closed portion of the formula
// can be used as the quantifier-free portion,
// unless the current state is unsatisfiable.
//
if (m.is_true(fml_mixed)) {
SASSERT(l_true == m_solver.check());
m_current = m_current->add_child(fml_closed);
for (unsigned i = 0; m_defs && i < m_current->num_free_vars(); ++i) {
expr_ref val(m);
@ -1708,6 +1762,7 @@ namespace qe {
if (val == x) {
model_ref model;
lbool is_sat = m_solver.check();
if (is_sat == l_undef) return;
m_solver.get_model(model);
SASSERT(is_sat == l_true);
model_evaluator model_eval2(*model);
@ -1890,7 +1945,7 @@ namespace qe {
vars.reset();
closed = closed && (r != l_undef);
}
TRACE("qe", tout << mk_ismt2_pp(fml, m) << "\n";);
TRACE("qe", tout << mk_pp(fml, m) << "\n";);
m_current->add_child(fml)->reset_free_vars();
block_assignment();
}
@ -1959,7 +2014,7 @@ namespace qe {
class quant_elim_new : public quant_elim {
ast_manager& m;
smt_params& m_fparams;
smt_params& m_fparams;
expr_ref m_assumption;
bool m_produce_models;
ptr_vector<quant_elim_plugin> m_plugins;

73
src/qe/qe_arith_plugin.cpp
View file

@ -31,6 +31,7 @@ Revision History:
#include "obj_pair_hashtable.h"
#include "nlarith_util.h"
#include "model_evaluator.h"
#include "smt_kernel.h"
namespace qe {
@ -80,9 +81,9 @@ namespace qe {
ast_manager& m;
i_solver_context& m_ctx;
public:
arith_util m_arith; // initialize before m_zero_i, etc.
arith_util m_arith; // initialize before m_zero_i, etc.
th_rewriter simplify;
private:
th_rewriter m_rewriter;
arith_eq_solver m_arith_solver;
bv_util m_bv;
@ -102,7 +103,7 @@ namespace qe {
m(m),
m_ctx(ctx),
m_arith(m),
m_rewriter(m),
simplify(m),
m_arith_solver(m),
m_bv(m),
m_zero_i(m_arith.mk_numeral(numeral(0), true), m),
@ -434,7 +435,6 @@ namespace qe {
expr_ref tmp(e, m);
simplify(tmp);
m_arith_rewriter.mk_le(tmp, mk_zero(e), result);
TRACE("qe_verbose", tout << "mk_le " << mk_pp(result, m) << "\n";);
}
void mk_lt(expr* e, expr_ref& result) {
@ -521,7 +521,8 @@ namespace qe {
expr_ref result1(m), result2(m);
// a*s + b*t <= 0
expr_ref as_bt_le_0(result, m), tmp2(m), tmp3(m), tmp4(m);
expr_ref as_bt_le_0(result, m), tmp2(m), asz_bt_le_0(m), tmp3(m), tmp4(m);
expr_ref b_divides_sz(m);
// a*s + b*t + (a-1)(b-1) <= 0
tmp2 = m_arith.mk_add(as_bt, slack);
@ -560,30 +561,36 @@ namespace qe {
sz = m_arith.mk_uminus(sz);
}
tmp4 = mk_add(mk_mul(a1, sz), bt);
mk_le(tmp4, tmp3);
mk_le(tmp4, asz_bt_le_0);
if (to_app(tmp3)->get_arg(0) == x &&
m_arith.is_zero(to_app(tmp3)->get_arg(1))) {
if (to_app(asz_bt_le_0)->get_arg(0) == x &&
m_arith.is_zero(to_app(asz_bt_le_0)->get_arg(1))) {
// exists z in [0 .. |b|-2] . |b| | (z + s) && z <= 0
// <=>
// |b| | s
mk_divides(abs_b, s, tmp2);
}
else {
mk_divides(abs_b, sz, tmp2);
mk_and(tmp2, tmp3, tmp4);
mk_big_or(abs_b - numeral(2), x, tmp4, tmp2);
mk_divides(abs_b, sz, b_divides_sz);
mk_and(b_divides_sz, asz_bt_le_0, tmp4);
mk_big_or(abs_b - numeral(2), x, tmp4, tmp2);
TRACE("qe",
tout << "b | s + z: " << mk_pp(b_divides_sz, m) << "\n";
tout << "a(s+z) + bt <= 0: " << mk_pp(asz_bt_le_0, m) << "\n";
);
}
mk_flat_and(as_bt_le_0, tmp2, result2);
mk_or(result1, result2, result);
simplify(result);
// a*s + b*t + (a-1)(b-1) <= 0
// or exists z in [0 .. |b|-2] . |b| | (z + s) && a*n_sign(b)(s + z) + |b|t <= 0
}
TRACE("qe",
{
expr_ref_vector trail(m);
tout << "is_strict: " << (is_strict?"true":"false") << "\n";
tout << (is_strict?"strict":"non-strict") << "\n";
bound(m, a, t, false).pp(tout, x);
tout << "\n";
bound(m, b, s, false).pp(tout, x);
@ -592,10 +599,6 @@ namespace qe {
});
}
void simplify(expr_ref& p) {
m_rewriter(p);
}
struct mul_lt {
arith_util& u;
mul_lt(arith_qe_util& u): u(u.m_arith) {}
@ -1052,7 +1055,6 @@ namespace qe {
}
bool reduce_equation(expr* p, expr* fml) {
TRACE("qe", tout << mk_pp(p, m) << "\n";);
numeral k;
if (m_arith.is_numeral(p, k) && k.is_zero()) {
@ -1555,9 +1557,10 @@ public:
mk_non_resolve(bounds, true, is_lower, result);
mk_non_resolve(bounds, false, is_lower, result);
m_util.simplify(result);
add_cache(x, fml, v, result, x_t.get_coeff(), x_t.get_term());
TRACE("qe",
tout << vl << " " << mk_pp(x, m) << "\n";
tout << vl << " " << mk_pp(x, m) << " infinite case\n";
tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";);
return;
@ -1591,19 +1594,22 @@ public:
SASSERT(index < bounds.size(is_strict, is_lower));
expr_ref t(bounds.exprs(is_strict, is_lower)[index], m);
rational a = bounds.coeffs(is_strict, is_lower)[index];
t = x_t.mk_term(a, t);
a = x_t.mk_coeff(a);
mk_bounds(bounds, x, true, is_eq, is_strict, is_lower, index, a, t, result);
mk_bounds(bounds, x, false, is_eq, is_strict, is_lower, index, a, t, result);
t = x_t.mk_term(a, t);
a = x_t.mk_coeff(a);
mk_resolve(bounds, x, x_t, true, is_eq, is_strict, is_lower, index, a, t, result);
mk_resolve(bounds, x, x_t, false, is_eq, is_strict, is_lower, index, a, t, result);
m_util.simplify(result);
add_cache(x, fml, v, result, x_t.get_coeff(), x_t.get_term());
TRACE("qe",
{
tout << vl << " " << mk_pp(x, m) << "\n";
tout << vl << " " << mk_pp(bounds.atoms(is_strict, is_lower)[index],m) << "\n";
tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";
}
@ -2225,6 +2231,12 @@ public:
}
}
m_util.simplify(result);
TRACE("qe",
tout << (is_strict?"strict":"non-strict") << "\n";
tout << (is_lower?"is-lower":"is-upper") << "\n";
tout << "a: " << a << " " << mk_pp(t, m) << "\n";
tout << "b: " << b << " " << mk_pp(s, m) << "\n";
tout << mk_pp(result, m) << "\n";);
}
//
@ -2245,10 +2257,12 @@ public:
void mk_bounds(bounds_proc& bounds,
app* x, bool is_strict, bool is_eq_ctx, bool is_strict_ctx, bool is_lower, unsigned index,
app* x, bool is_strict, bool is_eq_ctx,
bool is_strict_ctx, bool is_lower, unsigned index,
rational const& a, expr* t,
expr_ref& result)
{
TRACE("qe", tout << mk_pp(t, m) << "\n";);
SASSERT(!is_eq_ctx || !is_strict_ctx);
unsigned sz = bounds.size(is_strict, is_lower);
expr_ref tmp(m), eq(m);
@ -2258,13 +2272,14 @@ public:
for (unsigned i = 0; i < sz; ++i) {
app* e = bounds.atoms(is_strict, is_lower)[i];
expr* s = bounds.exprs(is_strict, is_lower)[i];
expr_ref s(bounds.exprs(is_strict, is_lower)[i], m);
rational b = bounds.coeffs(is_strict, is_lower)[i];
if (same_strict && i == index) {
if (non_strict_real) {
m_util.mk_eq(a, x, t, eq);
TRACE("qe", tout << "a:" << a << " x: " << mk_pp(x, m) << " t: " << mk_pp(t, m) << " eq: " << mk_pp(eq, m) << "\n";);
TRACE("qe", tout << "a:" << a << " x: " << mk_pp(x, m) << "t: " <<
mk_pp(t, m) << " eq: " << mk_pp(eq, m) << "\n";);
if (is_eq_ctx) {
m_ctx.add_constraint(true, eq);
}
@ -2292,6 +2307,7 @@ public:
(non_strict_real && is_eq_ctx && is_strict) ||
(same_strict && i < index);
mk_bound(result_is_strict, is_lower, a, t, b, s, tmp);
m_util.m_replace.apply_substitution(e, tmp.get(), result);
@ -2330,14 +2346,17 @@ public:
s = x_t.mk_term(b, s);
b = x_t.mk_coeff(b);
m_util.mk_resolve(x, strict_resolve, a, t, b, s, tmp);
expr_ref save_result(result);
m_util.m_replace.apply_substitution(e, tmp.get(), result);
m_ctx.add_constraint(true, mk_not(e), tmp);
TRACE("qe_verbose",
tout << mk_pp(atm, m) << " ";
tout << mk_pp(e, m) << " ==> ";
tout << mk_pp(e, m) << " ==>\n";
tout << mk_pp(tmp, m) << "\n";
tout << "old fml: " << mk_pp(save_result, m) << "\n";
tout << "new fml: " << mk_pp(result, m) << "\n";
);
}
}

2
src/qe/qe_sat_tactic.cpp
View file

@ -226,7 +226,7 @@ namespace qe {
return alloc(sat_tactic, m);
}
~sat_tactic() {
virtual ~sat_tactic() {
for (unsigned i = 0; i < m_solvers.size(); ++i) {
dealloc(m_solvers[i]);
}

1
src/smt/params/preprocessor_params.cpp
View file

@ -23,6 +23,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
m_macro_finder = p.macro_finder();
m_pull_nested_quantifiers = p.pull_nested_quantifiers();
m_refine_inj_axiom = p.refine_inj_axioms();
}
void preprocessor_params::updt_params(params_ref const & p) {

1
src/smt/params/smt_params_helper.pyg
View file

@ -14,6 +14,7 @@ def_module_params(module_name='smt',
('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),

1
src/smt/params/theory_arith_params.cpp
View file

@ -22,6 +22,7 @@ Revision History:
void theory_arith_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
m_arith_random_initial_value = p.arith_random_initial_value();
m_arith_random_seed = p.random_seed();
m_arith_mode = static_cast<arith_solver_id>(p.arith_solver());
m_nl_arith = p.arith_nl();
m_nl_arith_gb = p.arith_nl_gb();

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

@ -20,6 +20,7 @@ Revision History:
#include"proto_model.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"expr_functors.h"
datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.mk_family_id("datatype"), md),
@ -47,8 +48,10 @@ expr * datatype_factory::get_some_value(sort * s) {
*/
expr * datatype_factory::get_last_fresh_value(sort * s) {
expr * val = 0;
if (m_last_fresh_value.find(s, val))
if (m_last_fresh_value.find(s, val)) {
TRACE("datatype_factory", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
return val;
}
value_set * set = get_value_set(s);
if (set->empty())
val = get_some_value(s);
@ -59,6 +62,17 @@ expr * datatype_factory::get_last_fresh_value(sort * s) {
return val;
}
bool datatype_factory::is_subterm_of_last_value(app* e) {
expr* last;
if (!m_last_fresh_value.find(m_manager.get_sort(e), last)) {
return false;
}
contains_app contains(m_manager, e);
bool result = contains(last);
TRACE("datatype_factory", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";);
return result;
}
/**
\brief Create an almost fresh value. If s is recursive, then the result is not 0.
It also updates m_last_fresh_value
@ -105,11 +119,18 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
}
}
if (recursive || found_fresh_arg) {
expr * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
app * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
SASSERT(!found_fresh_arg || !set->contains(new_value));
register_value(new_value);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, new_value);
if (m_util.is_recursive(s)) {
if (is_subterm_of_last_value(new_value)) {
new_value = static_cast<app*>(m_last_fresh_value.find(s));
}
else {
m_last_fresh_value.insert(s, new_value);
}
}
TRACE("datatype_factory", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";);
return new_value;
}
}
@ -170,8 +191,10 @@ expr * datatype_factory::get_fresh_value(sort * s) {
// Approach 2)
// For recursive datatypes.
// search for constructor...
unsigned num_iterations = 0;
if (m_util.is_recursive(s)) {
while(true) {
++num_iterations;
TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
ptr_vector<func_decl>::const_iterator it = constructors->begin();
@ -181,12 +204,26 @@ expr * datatype_factory::get_fresh_value(sort * s) {
expr_ref_vector args(m_manager);
bool found_sibling = false;
unsigned num = constructor->get_arity();
TRACE("datatype_factory", tout << "checking constructor: " << constructor->get_name() << "\n";);
for (unsigned i = 0; i < num; i++) {
sort * s_arg = constructor->get_domain(i);
TRACE("datatype_factory", tout << mk_pp(s, m_manager) << " "
<< mk_pp(s_arg, m_manager) << " are_siblings "
<< m_util.are_siblings(s, s_arg) << " is_datatype "
<< m_util.is_datatype(s_arg) << " found_sibling "
<< found_sibling << "\n";);
if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
found_sibling = true;
expr * maybe_new_arg = get_almost_fresh_value(s_arg);
expr * maybe_new_arg = 0;
if (num_iterations <= 1) {
maybe_new_arg = get_almost_fresh_value(s_arg);
}
else {
maybe_new_arg = get_fresh_value(s_arg);
}
if (!maybe_new_arg) {
TRACE("datatype_factory",
tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
maybe_new_arg = m_model.get_some_value(s_arg);
found_sibling = false;
}
@ -202,6 +239,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
if (found_sibling) {
expr_ref new_value(m_manager);
new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
m_last_fresh_value.insert(s, new_value);
if (!set->contains(new_value)) {
register_value(new_value);

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

@ -29,6 +29,8 @@ class datatype_factory : public struct_factory {
expr * get_last_fresh_value(sort * s);
expr * get_almost_fresh_value(sort * s);
bool is_subterm_of_last_value(app* e);
public:
datatype_factory(ast_manager & m, proto_model & md);
virtual ~datatype_factory() {}

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

@ -247,6 +247,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
new_t = mk_some_interp_for(f);
}
else {
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
is_ok = false;
}
}
@ -294,6 +295,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
// f is an uninterpreted function, there is no need to use m_simplifier.mk_app
new_t = m_manager.mk_app(f, num_args, args.c_ptr());
trail.push_back(new_t);
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
is_ok = false;
}
}
@ -326,6 +328,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
todo.pop_back();
break;
case AST_QUANTIFIER:
TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";);
is_ok = false; // evaluator does not handle quantifiers.
SASSERT(a != 0);
eval_cache.insert(a, a);

2
src/smt/smt_context.cpp
View file

@ -3945,7 +3945,7 @@ namespace smt {
m_fingerprints.display(tout);
);
failure fl = get_last_search_failure();
if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) {
if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == THEORY) {
// don't generate model.
return;
}

21
src/smt/smt_model_finder.cpp
View file

@ -396,7 +396,7 @@ namespace smt {
// Support for evaluating expressions in the current model.
proto_model * m_model;
obj_map<expr, expr *> m_eval_cache;
obj_map<expr, expr *> m_eval_cache[2];
expr_ref_vector m_eval_cache_range;
ptr_vector<node> m_root_nodes;
@ -409,7 +409,8 @@ namespace smt {
}
void reset_eval_cache() {
m_eval_cache.reset();
m_eval_cache[0].reset();
m_eval_cache[1].reset();
m_eval_cache_range.reset();
}
@ -468,6 +469,7 @@ namespace smt {
~auf_solver() {
flush_nodes();
reset_eval_cache();
}
void set_context(context * ctx) {
@ -547,7 +549,7 @@ namespace smt {
for (obj_map<expr, unsigned>::iterator it = elems.begin(); it != elems.end(); it++) {
expr * n = it->m_key;
expr * n_val = eval(n, true);
if (!m_manager.is_value(n_val))
if (!n_val || !m_manager.is_value(n_val))
to_delete.push_back(n);
}
for (ptr_vector<expr>::iterator it = to_delete.begin(); it != to_delete.end(); it++) {
@ -569,16 +571,19 @@ namespace smt {
virtual expr * eval(expr * n, bool model_completion) {
expr * r = 0;
if (m_eval_cache.find(n, r)) {
if (m_eval_cache[model_completion].find(n, r)) {
return r;
}
expr_ref tmp(m_manager);
if (!m_model->eval(n, tmp, model_completion))
if (!m_model->eval(n, tmp, model_completion)) {
r = 0;
else
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n-----> null\n";);
}
else {
r = tmp;
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
m_eval_cache.insert(n, r);
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
}
m_eval_cache[model_completion].insert(n, r);
m_eval_cache_range.push_back(r);
return r;
}

2
src/smt/smt_model_generator.cpp
View file

@ -102,6 +102,7 @@ namespace smt {
if (th && th->build_models()) {
if (r->get_th_var(th->get_id()) != null_theory_var) {
proc = th->mk_value(r, *this);
SASSERT(proc);
}
else {
TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
@ -110,6 +111,7 @@ namespace smt {
}
else {
proc = mk_model_value(r);
SASSERT(proc);
}
}
SASSERT(proc);

1
src/smt/theory_arith.h
View file

@ -85,6 +85,7 @@ namespace smt {
typedef typename Ext::numeral numeral;
typedef typename Ext::inf_numeral inf_numeral;
typedef vector<numeral> numeral_vector;
typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
static const int dead_row_id = -1;
protected:

3
src/smt/theory_arith_core.h
View file

@ -2780,7 +2780,6 @@ namespace smt {
*/
template<typename Ext>
void theory_arith<Ext>::refine_epsilon() {
typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
while (true) {
rational2var mapping;
theory_var num = get_num_vars();
@ -2788,6 +2787,8 @@ namespace smt {
for (theory_var v = 0; v < num; v++) {
if (is_int(v))
continue;
if (!get_context().is_shared(get_enode(v)))
continue;
inf_numeral const & val = get_value(v);
rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
theory_var v2;

2
src/smt/theory_arith_eq.h
View file

@ -193,7 +193,7 @@ namespace smt {
return true;
}
if (!r.get_base_var() == x && x > y) {
if (r.get_base_var() != x && x > y) {
std::swap(x, y);
k.neg();
}

12
src/smt/theory_arith_nl.h
View file

@ -654,6 +654,7 @@ namespace smt {
}
return get_value(v, computed_epsilon) == val;
}
/**
\brief Return true if for every monomial x_1 * ... * x_n,
@ -2309,8 +2310,9 @@ namespace smt {
if (m_nl_monomials.empty())
return FC_DONE;
if (check_monomial_assignments())
if (check_monomial_assignments()) {
return FC_DONE;
}
if (!m_params.m_nl_arith)
return FC_GIVEUP;
@ -2338,9 +2340,10 @@ namespace smt {
if (!max_min_nl_vars())
return FC_CONTINUE;
if (check_monomial_assignments())
if (check_monomial_assignments()) {
return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
}
svector<theory_var> vars;
get_non_linear_cluster(vars);
@ -2391,8 +2394,9 @@ namespace smt {
}
while (m_nl_strategy_idx != old_idx);
if (check_monomial_assignments())
if (check_monomial_assignments()) {
return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
}
TRACE("non_linear", display(tout););

1
src/smt/theory_bv.cpp
View file

@ -1198,6 +1198,7 @@ namespace smt {
void theory_bv::relevant_eh(app * n) {
ast_manager & m = get_manager();
context & ctx = get_context();
TRACE("bv", tout << "relevant: " << mk_pp(n, m) << "\n";);
if (m.is_bool(n)) {
bool_var v = ctx.get_bool_var(n);
atom * a = get_bv2a(v);

7
src/smt/theory_dl.cpp
View file

@ -162,7 +162,7 @@ namespace smt {
m.register_factory(alloc(dl_factory, m_util, m.get_model()));
}
virtual smt::model_value_proc * mk_value(smt::enode * n) {
virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) {
return alloc(dl_value_proc, *this, n);
}
@ -201,9 +201,8 @@ namespace smt {
if(!m_reps.find(s, r) || !m_vals.find(s,v)) {
SASSERT(!m_reps.contains(s));
sort* bv = b().mk_sort(64);
// TBD: filter these from model.
r = m().mk_fresh_func_decl("rep",1, &s,bv);
v = m().mk_fresh_func_decl("val",1, &bv,s);
r = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_REP, 0, 0, 1, &s, bv);
v = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_ABS, 0, 0, 1, &bv, s);
m_reps.insert(s, r);
m_vals.insert(s, v);
add_trail(r);

10
src/solver/combined_solver.cpp
View file

@ -218,8 +218,14 @@ public:
}
virtual void set_cancel(bool f) {
m_solver1->set_cancel(f);
m_solver2->set_cancel(f);
if (f) {
m_solver1->cancel();
m_solver2->cancel();
}
else {
m_solver1->reset_cancel();
m_solver2->reset_cancel();
}
}
virtual void set_progress_callback(progress_callback * callback) {

4
src/solver/solver.h
View file

@ -99,7 +99,6 @@ public:
*/
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
virtual void set_cancel(bool f) {}
/**
\brief Interrupt this solver.
*/
@ -130,6 +129,9 @@ public:
\brief Display the content of this solver.
*/
virtual void display(std::ostream & out) const;
protected:
virtual void set_cancel(bool f) = 0;
};
#endif

2
src/solver/solver_na2as.cpp
View file

@ -82,7 +82,7 @@ void solver_na2as::pop(unsigned n) {
}
void solver_na2as::restore_assumptions(unsigned old_sz) {
SASSERT(old_sz == 0);
// SASSERT(old_sz == 0);
for (unsigned i = old_sz; i < m_assumptions.size(); i++) {
m_manager.dec_ref(m_assumptions[i]);
}

8
src/solver/tactic2solver.cpp
View file

@ -173,8 +173,12 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
}
void tactic2solver::set_cancel(bool f) {
if (m_tactic.get())
m_tactic->set_cancel(f);
if (m_tactic.get()) {
if (f)
m_tactic->cancel();
else
m_tactic->reset_cancel();
}
}
void tactic2solver::collect_statistics(statistics & st) const {

2
src/tactic/aig/aig.h
View file

@ -73,8 +73,6 @@ public:
void display(std::ostream & out, aig_ref const & r) const;
void display_smt2(std::ostream & out, aig_ref const & r) const;
unsigned get_num_aigs() const;
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
void set_cancel(bool f);
};

10
src/tactic/arith/add_bounds_tactic.cpp
View file

@ -172,18 +172,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
d = m_imp;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
protected:

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

@ -218,6 +218,7 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_urem(s1, t1));
TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";);
return BR_DONE;
}
@ -232,6 +233,7 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
u1 = mk_bv_add(s1, u1, false);
align_sizes(u1, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_urem(u1, t1));
TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";);
return BR_DONE;
}

10
src/tactic/arith/degree_shift_tactic.cpp
View file

@ -319,18 +319,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m);
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
protected:

13
src/tactic/arith/diff_neq_tactic.cpp
View file

@ -398,20 +398,13 @@ public:
}
virtual void cleanup() {
unsigned num_conflicts = m_imp->m_num_conflicts;
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m, m_params);
d->m_num_conflicts = m_imp->m_num_conflicts;
#pragma omp critical (tactic_cancel)
{
d = m_imp;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
m_imp->m_num_conflicts = num_conflicts;
}
protected:

10
src/tactic/arith/factor_tactic.cpp
View file

@ -333,18 +333,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
virtual void set_cancel(bool f) {

10
src/tactic/arith/fix_dl_var_tactic.cpp
View file

@ -338,18 +338,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
virtual void set_cancel(bool f) {

10
src/tactic/arith/fm_tactic.cpp
View file

@ -1682,18 +1682,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
virtual void operator()(goal_ref const & in,

10
src/tactic/arith/lia2pb_tactic.cpp
View file

@ -345,18 +345,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
d = m_imp;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
protected:

9
src/tactic/arith/normalize_bounds_tactic.cpp
View file

@ -191,17 +191,12 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
d = m_imp;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
protected:

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

@ -1002,17 +1002,12 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
d = m_imp;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
protected:

10
src/tactic/arith/propagate_ineqs_tactic.cpp
View file

@ -548,16 +548,10 @@ void propagate_ineqs_tactic::set_cancel(bool f) {
}
void propagate_ineqs_tactic::cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
d = m_imp;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}

10
src/tactic/arith/recover_01_tactic.cpp
View file

@ -425,18 +425,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
d = m_imp;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
protected:

10
src/tactic/bv/bit_blaster_tactic.cpp
View file

@ -140,18 +140,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m(), m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
unsigned get_num_steps() const {

10
src/tactic/bv/bv1_blaster_tactic.cpp
View file

@ -465,18 +465,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m(), m_params);
#pragma omp critical (tactic_cancel)
{
d = m_imp;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
unsigned get_num_steps() const {

10
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -392,17 +392,11 @@ void bv_size_reduction_tactic::set_cancel(bool f) {
}
void bv_size_reduction_tactic::cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m);
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}

10
src/tactic/bv/max_bv_sharing_tactic.cpp
View file

@ -311,18 +311,12 @@ public:
}
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = m_imp;
imp * d = alloc(imp, m_imp->m(), m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
std::swap(d, m_imp);
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
virtual void set_cancel(bool f) {

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