From a5e3713c2c5e1065510d927a9c07ab240b3bf870 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Jun 2014 05:47:42 -0700 Subject: [PATCH 01/25] fix unmatched parenthsis and code odor Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index d0e174914..00d03a8b0 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -1630,10 +1630,8 @@ public: unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0)); std::set 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); From 1ed7643d3223c88f80e72135553e6cb5743158e5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Jun 2014 09:52:59 -0700 Subject: [PATCH 02/25] Add option to control explosion of cofactor-term-ite following example by Anvesh Signed-off-by: Nikolaj Bjorner --- src/tactic/core/cofactor_elim_term_ite.cpp | 54 ++++++++++++-------- src/tactic/core/cofactor_elim_term_ite.h | 2 +- src/tactic/core/cofactor_term_ite_tactic.cpp | 3 +- 3 files changed, 34 insertions(+), 25 deletions(-) diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index d81b4fa13..bba6db2b6 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -29,14 +29,15 @@ struct cofactor_elim_term_ite::imp { ast_manager & m; params_ref m_params; unsigned long long m_max_memory; - volatile bool m_cancel; + bool m_cofactor_equalities; + volatile bool m_cancel; void checkpoint() { cooperate("cofactor ite"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); if (m_cancel) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + throw tactic_exception(TACTIC_CANCELED_MSG); } // Collect atoms that contain term if-then-else @@ -111,7 +112,7 @@ struct cofactor_elim_term_ite::imp { frame & fr = m_frame_stack.back(); expr * t = fr.m_t; bool form_ctx = fr.m_form_ctx; - TRACE("cofactor_ite_analyzer", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";); + TRACE("cofactor", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";); m_owner.checkpoint(); @@ -150,7 +151,7 @@ struct cofactor_elim_term_ite::imp { } if (i < num_args) { m_has_term_ite.mark(t); - TRACE("cofactor_ite_analyzer", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";); + TRACE("cofactor", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";); save_candidate(t, form_ctx); } } @@ -167,6 +168,7 @@ struct cofactor_elim_term_ite::imp { }; expr * get_first(expr * t) { + TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";); typedef std::pair frame; expr_fast_mark1 visited; sbuffer stack; @@ -225,6 +227,7 @@ struct cofactor_elim_term_ite::imp { \brief Fuctor for selecting the term if-then-else condition with the most number of occurrences. */ expr * get_best(expr * t) { + TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";); typedef std::pair frame; obj_map occs; expr_fast_mark1 visited; @@ -299,12 +302,17 @@ struct cofactor_elim_term_ite::imp { } } visited.reset(); - CTRACE("cofactor_ite_get_best", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";); + CTRACE("cofactor", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";); return best; } void updt_params(params_ref const & p) { m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_cofactor_equalities = p.get_bool("cofactor_equalities", true); + } + + void collect_param_descrs(param_descrs & r) { + r.insert("cofactor_equalities", CPK_BOOL, "(default: true) use equalities to rewrite bodies of ite-expressions. This is potentially expensive."); } void set_cancel(bool f) { @@ -354,16 +362,16 @@ struct cofactor_elim_term_ite::imp { m_term = 0; expr * lhs; expr * rhs; - if (m.is_eq(t, lhs, rhs)) { + if (m_owner.m_cofactor_equalities && m.is_eq(t, lhs, rhs)) { if (m.is_unique_value(lhs)) { m_term = rhs; m_value = to_app(lhs); - TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";); + TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";); } else if (m.is_unique_value(rhs)) { m_term = lhs; m_value = to_app(rhs); - TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";); + TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";); } } // TODO: bounds @@ -467,7 +475,7 @@ struct cofactor_elim_term_ite::imp { m_cofactor.set_cofactor_atom(neg_c); m_cofactor(curr, neg_cofactor); curr = m.mk_ite(c, pos_cofactor, neg_cofactor); - TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";); + TRACE("cofactor", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";); } } return false; @@ -522,7 +530,7 @@ struct cofactor_elim_term_ite::imp { void cofactor(expr * t, expr_ref & r) { unsigned step = 0; - TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";); + TRACE("cofactor", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";); expr_ref curr(m); curr = t; while (true) { @@ -543,21 +551,20 @@ struct cofactor_elim_term_ite::imp { m_cofactor(curr, neg_cofactor); if (pos_cofactor == neg_cofactor) { curr = pos_cofactor; - TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";); - continue; } - if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) { + else if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) { curr = c; - TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";); - continue; } - if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) { + else if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) { curr = neg_c; - TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";); - continue; } - curr = m.mk_ite(c, pos_cofactor, neg_cofactor); - TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";); + else { + curr = m.mk_ite(c, pos_cofactor, neg_cofactor); + } + TRACE("cofactor", + tout << "cofactor_ite step: " << step << "\n"; + tout << "co-factor: " << mk_ismt2_pp(c, m) << "\n"; + tout << mk_ismt2_pp(curr, m) << "\n";); } } @@ -570,6 +577,7 @@ struct cofactor_elim_term_ite::imp { void operator()(expr * t, expr_ref & r) { ptr_vector new_args; + SASSERT(m_frames.empty()); m_frames.push_back(frame(t, true)); while (!m_frames.empty()) { m_owner.checkpoint(); @@ -649,7 +657,8 @@ struct cofactor_elim_term_ite::imp { imp(ast_manager & _m, params_ref const & p): m(_m), - m_params(p) { + m_params(p), + m_cofactor_equalities(true) { m_cancel = false; updt_params(p); } @@ -686,7 +695,8 @@ void cofactor_elim_term_ite::updt_params(params_ref const & p) { m_imp->updt_params(p); } -void cofactor_elim_term_ite::get_param_descrs(param_descrs & r) { +void cofactor_elim_term_ite::collect_param_descrs(param_descrs & r) { + m_imp->collect_param_descrs(r); } void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) { diff --git a/src/tactic/core/cofactor_elim_term_ite.h b/src/tactic/core/cofactor_elim_term_ite.h index 9b325b1f0..ce2f31ea0 100644 --- a/src/tactic/core/cofactor_elim_term_ite.h +++ b/src/tactic/core/cofactor_elim_term_ite.h @@ -31,7 +31,7 @@ public: virtual ~cofactor_elim_term_ite(); void updt_params(params_ref const & p); - static void get_param_descrs(param_descrs & r); + void collect_param_descrs(param_descrs & r); void operator()(expr * t, expr_ref & r); diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index 16b4d1ad4..bc719a85e 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -52,8 +52,7 @@ public: virtual ~cofactor_term_ite_tactic() {} virtual void updt_params(params_ref const & p) { m_params = p; m_elim_ite.updt_params(p); } - static void get_param_descrs(param_descrs & r) { cofactor_elim_term_ite::get_param_descrs(r); } - virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } + virtual void collect_param_descrs(param_descrs & r) { m_elim_ite.collect_param_descrs(r); } virtual void operator()(goal_ref const & g, goal_ref_buffer & result, From 103e49d9b4906237a9f520d27861675e222f2c7d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Jun 2014 09:53:47 -0700 Subject: [PATCH 03/25] Add option to control explosion of cofactor-term-ite following example by Anvesh Signed-off-by: Nikolaj Bjorner --- src/tactic/core/cofactor_elim_term_ite.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index bba6db2b6..1f560ef62 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -563,7 +563,7 @@ struct cofactor_elim_term_ite::imp { } TRACE("cofactor", tout << "cofactor_ite step: " << step << "\n"; - tout << "co-factor: " << mk_ismt2_pp(c, m) << "\n"; + tout << "cofactor: " << mk_ismt2_pp(c, m) << "\n"; tout << mk_ismt2_pp(curr, m) << "\n";); } } From a26ae624e0d33a738707d86afd819cca668f2429 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 19 Jun 2014 15:50:18 +0100 Subject: [PATCH 04/25] Fixed dependencies of install target in Makefile Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 89cabe87e..423898ad8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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 @@ -853,6 +856,9 @@ 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))) @@ -935,6 +941,9 @@ 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 @@ -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 @@ -1611,7 +1625,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')) From 91b32206fde2cf0ab6fc85ff3452370d24cd22f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Jun 2014 13:59:35 -0700 Subject: [PATCH 05/25] fix(scripts/mk_make): python3 compatibility Signed-off-by: Leonardo de Moura --- scripts/mk_util.py | 124 ++++++++++++++++++++++----------------------- 1 file changed, 62 insertions(+), 62 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 423898ad8..653e4588b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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) @@ -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 @@ -821,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): @@ -862,7 +862,7 @@ class LibComponent(Component): 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)) @@ -871,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) @@ -948,7 +948,7 @@ class ExeComponent(Component): 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)) @@ -1072,7 +1072,7 @@ class DLLComponent(Component): out.write(' ') out.write(obj) out.write('\n') - + def main_component(self): return self.install @@ -1098,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 @@ -1132,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: @@ -1161,7 +1161,7 @@ class DotNetDLLComponent(Component): out.write('\n') out.write('%s: %s\n\n' % (self.name, dllfile)) return - + def main_component(self): return DOTNET_ENABLED @@ -1194,7 +1194,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: @@ -1225,16 +1225,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() @@ -1243,7 +1243,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')) @@ -1254,7 +1254,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): @@ -1310,7 +1310,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) @@ -1591,7 +1591,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') @@ -1650,7 +1650,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') @@ -1660,7 +1660,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(): @@ -1715,7 +1715,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: @@ -1801,10 +1801,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') @@ -1817,8 +1817,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 } @@ -1833,7 +1833,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) @@ -1849,7 +1849,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')) @@ -1865,7 +1865,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) @@ -1888,8 +1888,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]*"\) *') @@ -1954,7 +1954,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)) @@ -1962,7 +1962,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)) @@ -2146,7 +2146,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)) @@ -2189,7 +2189,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: @@ -2226,7 +2226,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: @@ -2267,7 +2267,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): @@ -2308,7 +2308,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: @@ -2391,7 +2391,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: @@ -2429,7 +2429,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)) @@ -2440,7 +2440,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') From 000db81b4f6811328fb9309c7af1a5d702eb1291 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 23 Jun 2014 15:47:47 +0100 Subject: [PATCH 06/25] Fixed bug where the random seed wasn't passed through to theory_arith. Thanks to Carsten! (Stackoverflow #24327987) Signed-off-by: Christoph M. Wintersteiger --- src/smt/params/theory_arith_params.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 7281a5daa..7287cac2f 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -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(p.arith_solver()); m_nl_arith = p.arith_nl(); m_nl_arith_gb = p.arith_nl_gb(); From 3209cd2ded8bfd952cfd99d0398b4c0bd4a0c04d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 23 Jun 2014 16:40:49 +0100 Subject: [PATCH 07/25] Disabled construction of partial model on theory failure as it caused buggy behavior. Thanks to parno (Codeplex Issue #117)! Signed-off-by: Christoph M. Wintersteiger --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 02ee06985..4f3c73ce6 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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; } From 7158e814d1dc22eabaace0f8da6f8950e9bca1d9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 25 Jun 2014 13:25:23 +0100 Subject: [PATCH 08/25] Bugfix for quasi-macros, many thanks to Nuno Lopez finding this bug and for suggesting a fix! Signed-off-by: Christoph M. Wintersteiger --- src/ast/macros/quasi_macros.cpp | 17 +++++++++++------ src/ast/macros/quasi_macros.h | 1 + 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index 084a33ebf..b26b7faba 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -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; diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h index c5e6b6d4f..64e72e348 100644 --- a/src/ast/macros/quasi_macros.h +++ b/src/ast/macros/quasi_macros.h @@ -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; From 311fed47602fbd10e4e8313081328f0864215060 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 1 Jul 2014 13:12:10 +0100 Subject: [PATCH 09/25] Changed python distribution to include *.py files to enable use with Python 2.7 and 3.4 out of the box. Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 653e4588b..6a9ace762 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2591,16 +2591,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)) From 3533a090105a5e26064bae50635e3f52a0c7846a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Jul 2014 23:48:49 +0200 Subject: [PATCH 10/25] bit2bool bug reported by Sagar Chaki Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_bit_blast.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 112541541..90d410ab1 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -88,11 +88,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); } } From d6de73a2d10135d5fb036787888380352c2bc3a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Jul 2014 18:11:57 +0200 Subject: [PATCH 11/25] fix model converter in inliner. Bug reported by Sagar Chaki Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 3 ++- src/muz/base/dl_util.cpp | 2 +- src/muz/transforms/dl_mk_rule_inliner.cpp | 5 +++++ 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index b29a9c87d..94e20eceb 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5668,7 +5668,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))) */ diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index 218f9906a..a6647a1d2 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -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"; }); diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index d9dad5c56..712c82feb 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -423,6 +423,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) { From 4f7d872d591cf1f9d23807898026e4516b686dc3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Jul 2014 11:21:19 +0200 Subject: [PATCH 12/25] fix model transformation bug in bit blaster rule transformer, reported by Sagar Chaki Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_bit_blast.cpp | 2 +- src/tactic/filter_model_converter.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 90d410ab1..15d3b2f5f 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -71,7 +71,7 @@ namespace datalog { unsigned arity_p = p->get_arity(); unsigned arity_q = q->get_arity(); SASSERT(0 < arity_p); - model->register_decl(p, f); + model->register_decl(p, f->copy()); func_interp* g = alloc(func_interp, m, arity_q); if (f) { diff --git a/src/tactic/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp index da4c71e54..ba6ee4f0d 100644 --- a/src/tactic/filter_model_converter.cpp +++ b/src/tactic/filter_model_converter.cpp @@ -43,6 +43,7 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx if (fs.is_marked(f)) continue; func_interp * fi = old_model->get_func_interp(f); + SASSERT(fi); new_model->register_decl(f, fi->copy()); } new_model->copy_usort_interps(*old_model); From e4dedbbefca8ac3fcf21e9f4dac0cf2018b8100a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Jul 2014 15:38:22 +0200 Subject: [PATCH 13/25] fix quantifier elimination bugs reported by Berdine and Bornat Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/qe/qe.cpp | 115 ++++++++++++++++++++------- src/qe/qe_arith_plugin.cpp | 73 ++++++++++------- src/smt/theory_bv.cpp | 5 +- src/tactic/arith/bv2int_rewriter.cpp | 2 + 5 files changed, 137 insertions(+), 60 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index b040efc0c..e67300970 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -704,7 +704,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul } // propagate mod inside only if not all arguments are not already mod. - if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { + if (false && m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";); unsigned num_args = to_app(arg1)->get_num_args(); unsigned i; diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index d63f0ae00..770a49c07 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -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 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 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_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 m_plugins; diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 7bf0978f6..83c7b79d8 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -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"; ); } } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index a338be50a..44715c37a 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -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); @@ -1210,11 +1211,11 @@ namespace smt { } } } - else if (m_params.m_bv_enable_int2bv2int && m_util.is_bv2int(n)) { + else if (/*m_params.m_bv_enable_int2bv2int &&*/ m_util.is_bv2int(n)) { ctx.mark_as_relevant(n->get_arg(0)); assert_bv2int_axiom(n); } - else if (m_params.m_bv_enable_int2bv2int && m_util.is_int2bv(n)) { + else if (/*m_params.m_bv_enable_int2bv2int &&*/ m_util.is_int2bv(n)) { ctx.mark_as_relevant(n->get_arg(0)); assert_int2bv_axiom(n); } diff --git a/src/tactic/arith/bv2int_rewriter.cpp b/src/tactic/arith/bv2int_rewriter.cpp index 872981283..00d2f53ad 100644 --- a/src/tactic/arith/bv2int_rewriter.cpp +++ b/src/tactic/arith/bv2int_rewriter.cpp @@ -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; } From dd786bb5bf4babb7eef988ad3487d627fee13ce4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Jul 2014 15:41:03 +0200 Subject: [PATCH 14/25] fix quantifier elimination bugs reported by Berdine and Bornat Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 44715c37a..8b3021573 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1211,11 +1211,11 @@ namespace smt { } } } - else if (/*m_params.m_bv_enable_int2bv2int &&*/ m_util.is_bv2int(n)) { + else if (m_params.m_bv_enable_int2bv2int && m_util.is_bv2int(n)) { ctx.mark_as_relevant(n->get_arg(0)); assert_bv2int_axiom(n); } - else if (/*m_params.m_bv_enable_int2bv2int &&*/ m_util.is_int2bv(n)) { + else if (m_params.m_bv_enable_int2bv2int && m_util.is_int2bv(n)) { ctx.mark_as_relevant(n->get_arg(0)); assert_int2bv_axiom(n); } From 752a6b2e33c954eba65a2d88d3b8e6ef82a251e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Jul 2014 16:46:27 +0200 Subject: [PATCH 15/25] fix quantifier elimination bugs reported by Berdine and Bornat Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index e67300970..b040efc0c 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -704,7 +704,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul } // propagate mod inside only if not all arguments are not already mod. - if (false && m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { + if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";); unsigned num_args = to_app(arg1)->get_num_args(); unsigned i; From 72fe197bda0d89674a1056def7640bd20e237b4f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Jul 2014 17:06:36 +0200 Subject: [PATCH 16/25] fix model generation bug reported by Saga Chaki Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_bit_blast.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 15d3b2f5f..fd1dbb205 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -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,10 +68,16 @@ 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); + SASSERT(f); model->register_decl(p, f->copy()); func_interp* g = alloc(func_interp, m, arity_q); From 4957e71408ebfa96545f767b665e37390512092e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Jul 2014 17:12:39 +0200 Subject: [PATCH 17/25] make get_vars populate all indices with sorts even if variable does not occur in rule. This makes the use of get_vars less prone to callers having to double check for null pointers Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_rule.cpp | 5 +++-- src/muz/base/dl_rule.h | 2 +- src/muz/bmc/dl_bmc_engine.cpp | 10 +++++----- src/muz/transforms/dl_mk_array_blast.cpp | 2 +- src/muz/transforms/dl_mk_coalesce.cpp | 6 +++--- src/muz/transforms/dl_mk_quantifier_instantiation.cpp | 5 +---- src/muz/transforms/dl_mk_rule_inliner.cpp | 5 +---- src/muz/transforms/dl_mk_scale.cpp | 2 +- 8 files changed, 16 insertions(+), 21 deletions(-) diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 184a5fa02..017bac724 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -978,13 +978,14 @@ namespace datalog { } } - void rule::get_vars(ptr_vector& sorts) const { + void rule::get_vars(ast_manager& m, ptr_vector& 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()); } } diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 1c31dc6b4..7104bae1f 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -304,7 +304,7 @@ namespace datalog { void norm_vars(rule_manager & rm); - void get_vars(ptr_vector& sorts) const; + void get_vars(ast_manager& m, ptr_vector& sorts) const; void to_formula(expr_ref& result) const; diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 0dcbf4644..51b1a5295 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -148,7 +148,7 @@ namespace datalog { void mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) { ptr_vector 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 rule_vars; expr_ref_vector args(m), conjs(m); - r.get_vars(rule_vars); + r.get_vars(m, rule_vars); obj_hashtable 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 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 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 sorts; - r.get_vars(sorts); + r.get_vars(m, sorts); // populate substitution of bound variables. sub.reset(); sub.resize(sorts.size()); diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index 9303181b6..641d40779 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -87,7 +87,7 @@ namespace datalog { else { if (m_next_var == 0) { ptr_vector 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)); diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp index 8c7f1d5b4..ac7a58d8d 100644 --- a/src/muz/transforms/dl_mk_coalesce.cpp +++ b/src/muz/transforms/dl_mk_coalesce.cpp @@ -62,7 +62,7 @@ namespace datalog { rule_ref r(const_cast(&rl), rm); ptr_vector sorts; expr_ref_vector revsub(m), conjs(m); - rl.get_vars(sorts); + rl.get_vars(m, sorts); revsub.resize(sorts.size()); svector 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 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) { diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 9c55ca658..fcb8d7b85 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -199,7 +199,7 @@ namespace datalog { expr_ref fml(m), cnst(m); var_ref var(m); ptr_vector 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); diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 712c82feb..522bd2e86 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -143,11 +143,8 @@ namespace datalog { expr_ref_vector result(m); ptr_vector 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); diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index 9ada7be20..271bf5f62 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -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))); From 44751c0ef8212bc78400aac42432e4fc7db3fa15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Jul 2014 15:27:24 -0700 Subject: [PATCH 18/25] Add missing .NET API functions for parsing rules into fixedpoint object Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Fixedpoint.cs | 39 +++++++++++++++++++++++++----------- 1 file changed, 27 insertions(+), 12 deletions(-) diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 8c6e6c4c6..3f40b220b 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -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; + } + /// /// Retrieve set of rules added to fixedpoint context. /// @@ -278,12 +286,7 @@ namespace Microsoft.Z3 { Contract.Ensures(Contract.Result() != 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() != 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))); } } + /// + /// Parse an SMT-LIB2 file with fixedpoint rules. + /// Add the rules to the current fixedpoint context. + /// Return the set of queries in the file. + /// + public BoolExpr[] ParseFile(string file) { + return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file))); + } + + /// + /// Similar to ParseFile. Instead it takes as argument a string. + /// + + 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) From 5b1a98a15587ff49ca023f93bba20fb3c1672790 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 24 Jul 2014 13:53:56 +0100 Subject: [PATCH 19/25] Bugfix for Python 3 --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 6a9ace762..16393d2b8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2592,7 +2592,7 @@ def mk_win_dist(build_path, dist_path): for c in get_components(): c.mk_win_dist(build_path, dist_path) # Add Z3Py to bin directory - print "Adding to %s\n" % dist_path + 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)) From 1abf3beaba62d5a426ce5e76a9a7b356f1b99506 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 24 Jul 2014 16:52:32 +0100 Subject: [PATCH 20/25] bugfix for Python 3 Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 16393d2b8..b73f7a7a8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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)) From 24961dc5f16645b345f99c13cb30b5b46764040a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jul 2014 14:42:00 -0700 Subject: [PATCH 21/25] feat(ast/ast_smt_pp): display quantifier QID when printing proofs, feature requested by Dan Rosen Signed-off-by: Leonardo de Moura --- src/ast/ast_smt_pp.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index f684879ae..59e5c04b9 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -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 << ")"; From 1944283253dbdd7c27f0586eabaa2456e9aef76b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 28 Jul 2014 19:36:11 +0100 Subject: [PATCH 22/25] FPA unified function names --- src/ast/float_decl_plugin.cpp | 2 +- src/ast/float_decl_plugin.h | 11 +++++++---- src/ast/rewriter/float_rewriter.cpp | 21 ++++++++++----------- 3 files changed, 18 insertions(+), 16 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 1adedb2d7..df26422c8 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -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; diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 3786b76ee..58c37080d 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -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); diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index ecd06ff38..a4212d579 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -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()); From b423418810e1f8099e2e575464668b9ac974dd9a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 28 Jul 2014 19:37:58 +0100 Subject: [PATCH 23/25] FPA fixed omissions reported by user xor88 (codeplex discussion 554193) Signed-off-by: Christoph M. Wintersteiger --- src/ast/fpa/fpa2bv_converter.cpp | 96 +++++++++++++++++++++++++------- src/ast/fpa/fpa2bv_converter.h | 8 ++- src/ast/fpa/fpa2bv_rewriter.h | 10 +++- 3 files changed, 90 insertions(+), 24 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 20925a0f9..d6f362902 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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(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)); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 2ccdac6a9..dcb508ffd 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -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 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); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index b2e3da939..225aad668 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -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; } From 06a4a3599da0fd89479f30e30f4aaea46bff47f9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 29 Jul 2014 18:04:54 +0100 Subject: [PATCH 24/25] Added git hashcode information to (get-info :version) Signed-off-by: Christoph M. Wintersteiger --- src/cmd_context/basic_cmds.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 527230e16..836ade9ce 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -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; From 39646bac3e58d8a28c0c5abc818d28b054b3a4bb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 31 Jul 2014 16:32:25 +0100 Subject: [PATCH 25/25] added operator[] to obj_map for convenience Signed-off-by: Christoph M. Wintersteiger --- src/util/obj_hashtable.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 603898af8..8ff5f8e8f 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -165,6 +165,14 @@ public: SASSERT(e); return e->get_data().m_value; } + + value const & operator[](key * k) const { + return find(k); + } + + value & operator[](key * k) { + return find(k); + } iterator find_iterator(Key * k) const { return m_table.find(key_data(k));