From db8782e7e78ab7bdbdb8afb311da14f47219ba66 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Oct 2012 19:27:19 -0700 Subject: [PATCH 01/16] New default behavior in the strategic_solver: invoke tactics when incremental solver returns unknown. Signed-off-by: Leonardo de Moura --- lib/strategic_solver.cpp | 36 ++++++++++++++++++++++++++---------- lib/strategic_solver.h | 16 ++++++++++++++-- 2 files changed, 40 insertions(+), 12 deletions(-) diff --git a/lib/strategic_solver.cpp b/lib/strategic_solver.cpp index fe976c138..c8d5c6fcb 100644 --- a/lib/strategic_solver.cpp +++ b/lib/strategic_solver.cpp @@ -33,7 +33,7 @@ strategic_solver::strategic_solver(): m_check_sat_executed(false), m_inc_solver(0), m_inc_solver_timeout(UINT_MAX), - m_tactic_if_undef(false), + m_inc_unknown_behavior(IUB_USE_TACTIC_IF_QF), m_default_fct(0), m_curr_tactic(0), m_proof(0), @@ -56,6 +56,29 @@ strategic_solver::~strategic_solver() { m().dec_ref(m_proof); } +bool strategic_solver::has_quantifiers() const { + unsigned sz = get_num_assertions(); + for (unsigned i = 0; i < sz; i++) { + if (::has_quantifiers(get_assertion(i))) + return true; + } + return false; +} + +/** + \brief Return true if a tactic should be used when the incremental solver returns unknown. +*/ +bool strategic_solver::use_tactic_when_undef() const { + switch (m_inc_unknown_behavior) { + case IUB_RETURN_UNDEF: return false; + case IUB_USE_TACTIC_IF_QF: return !has_quantifiers(); + case IUB_USE_TACTIC: return true; + default: + UNREACHABLE(); + return false; + } +} + void strategic_solver::set_inc_solver(solver * s) { SASSERT(m_inc_solver == 0); SASSERT(m_num_scopes == 0); @@ -86,13 +109,6 @@ void strategic_solver::set_inc_solver_timeout(unsigned timeout) { m_inc_solver_timeout = timeout; } -/** - \brief Use tactic when the incremental solver return undef. -*/ -void strategic_solver::use_tactic_if_undef(bool f) { - m_tactic_if_undef = f; -} - /** \brief Set the default tactic factory. It is used if there is no tactic for a given logic. @@ -285,7 +301,7 @@ lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assum IF_VERBOSE(PS_VB_LVL, verbose_stream() << "using incremental solver (without a timeout).\n";); m_use_inc_solver_results = true; lbool r = m_inc_solver->check_sat(0, 0); - if (r != l_undef || factory == 0 || !m_tactic_if_undef) { + if (r != l_undef || factory == 0 || !use_tactic_when_undef()) { m_use_inc_solver_results = true; return r; } @@ -299,7 +315,7 @@ lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assum scoped_timer timer(m_inc_solver_timeout, &eh); r = m_inc_solver->check_sat(0, 0); } - if ((r != l_undef || !m_tactic_if_undef) && !eh.m_canceled) { + if ((r != l_undef || !use_tactic_when_undef()) && !eh.m_canceled) { m_use_inc_solver_results = true; return r; } diff --git a/lib/strategic_solver.h b/lib/strategic_solver.h index 811fcaa95..b145da5f7 100644 --- a/lib/strategic_solver.h +++ b/lib/strategic_solver.h @@ -26,6 +26,15 @@ class progress_callback; struct front_end_params; class strategic_solver : public solver { +public: + // Behavior when the incremental solver returns unknown. + enum inc_unknown_behavior { + IUB_RETURN_UNDEF, // just return unknown + IUB_USE_TACTIC_IF_QF, // invoke tactic if problem is quantifier free + IUB_USE_TACTIC // invoke tactic + }; + +private: ast_manager * m_manager; front_end_params * m_fparams; symbol m_logic; @@ -34,7 +43,7 @@ class strategic_solver : public solver { bool m_check_sat_executed; scoped_ptr m_inc_solver; unsigned m_inc_solver_timeout; - bool m_tactic_if_undef; + inc_unknown_behavior m_inc_unknown_behavior; scoped_ptr m_default_fct; dictionary m_logic2fct; @@ -63,6 +72,9 @@ class strategic_solver : public solver { struct mk_tactic; + bool has_quantifiers() const; + bool use_tactic_when_undef() const; + public: strategic_solver(); ~strategic_solver(); @@ -73,7 +85,7 @@ public: void set_inc_solver_timeout(unsigned timeout); void set_default_tactic(tactic_factory * fct); void set_tactic_for(symbol const & logic, tactic_factory * fct); - void use_tactic_if_undef(bool f); + void set_inc_unknown_behavior(inc_unknown_behavior b) { m_inc_unknown_behavior = b; } void force_tactic(bool f) { m_force_tactic = f; } virtual void set_front_end_params(front_end_params & p) { m_fparams = &p; } From 12882f865fb8a35823312761de6a1130a8f367d6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Oct 2012 21:06:07 -0700 Subject: [PATCH 02/16] Fixed z3test.py. Execute z3test.py during Z3Py installation. Signed-off-by: Leonardo de Moura --- Makefile.in | 1 + python/z3test.py | 11 ++++------- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/Makefile.in b/Makefile.in index 9aef78a13..a24bb823d 100644 --- a/Makefile.in +++ b/Makefile.in @@ -361,6 +361,7 @@ install-python: $(BIN_DIR)/lib$(Z3).@SO_EXT@ @cp python/z3tactics.pyc $(PYTHON_PACKAGE_DIR) @cp python/z3printer.pyc $(PYTHON_PACKAGE_DIR) @cp $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(PYTHON_PACKAGE_DIR) + @if python python/z3test.py; then echo "Z3Py was successfully installed."; else echo "Failed to execute Z3Py regressions..."; exit 1; fi uninstall-python: @if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi diff --git a/python/z3test.py b/python/z3test.py index b57fa89dd..9b894d7ad 100644 --- a/python/z3test.py +++ b/python/z3test.py @@ -1,9 +1,6 @@ import z3, doctest -import sys, re -if re.compile("64 bit").search(sys.version): - z3.init("..\\x64\\external_64\\z3.dll") -else: - z3.init("..\\external\\z3.dll") - -doctest.testmod(z3) +r = doctest.testmod(z3) +if r.failed != 0: + exit(1) + From 44a98920d17b46a8e9e9d7b016bb19c303cdc109 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Oct 2012 21:34:36 -0700 Subject: [PATCH 03/16] improved z3py installation Signed-off-by: Leonardo de Moura --- Makefile.in | 4 ++-- dll/z3.def | 8 ++++---- dll/z3_dbg.def | 8 ++++---- lib/api.py | 5 ++--- python/README-linux.txt | 26 -------------------------- python/README-osx.txt | 24 ------------------------ python/README-win.txt | 16 ---------------- python/README.txt | 23 +++++++++++++++++++---- python/exec-linux.sh | 2 -- python/exec-osx.sh | 2 -- python/run-linux.sh | 2 -- python/run-osx.sh | 2 -- python/run.sh | 2 -- python/z3core.py | 5 ++--- 14 files changed, 33 insertions(+), 96 deletions(-) delete mode 100644 python/README-linux.txt delete mode 100644 python/README-osx.txt delete mode 100644 python/README-win.txt delete mode 100644 python/exec-linux.sh delete mode 100644 python/exec-osx.sh delete mode 100644 python/run-linux.sh delete mode 100644 python/run-osx.sh delete mode 100644 python/run.sh diff --git a/Makefile.in b/Makefile.in index a24bb823d..fd4366d13 100644 --- a/Makefile.in +++ b/Makefile.in @@ -350,7 +350,7 @@ uninstall: @rm -f $(PREFIX)/include/z3_macros.h @rm -f $(PREFIX)/include/z3++.h -install-python: $(BIN_DIR)/lib$(Z3).@SO_EXT@ +install-z3py: $(BIN_DIR)/lib$(Z3).@SO_EXT@ @if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi @echo "Installing Python bindings at $(PYTHON_PACKAGE_DIR)." @$(PYTHON) python/example.py > /dev/null @@ -363,7 +363,7 @@ install-python: $(BIN_DIR)/lib$(Z3).@SO_EXT@ @cp $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(PYTHON_PACKAGE_DIR) @if python python/z3test.py; then echo "Z3Py was successfully installed."; else echo "Failed to execute Z3Py regressions..."; exit 1; fi -uninstall-python: +uninstall-z3py: @if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi @echo "Uninstalling Python bindings from $(PYTHON_PACKAGE_DIR)." @rm -f $(PYTHON_PACKAGE_DIR)/z3.pyc diff --git a/dll/z3.def b/dll/z3.def index c663ed5c4..d56875d92 100644 --- a/dll/z3.def +++ b/dll/z3.def @@ -232,10 +232,10 @@ EXPORTS Z3_get_quantifier_pattern_ast @230 Z3_get_quantifier_num_no_patterns @231 Z3_get_quantifier_no_pattern_ast @232 - Z3_get_quantifier_bound_name @233 - Z3_get_quantifier_bound_sort @234 - Z3_get_quantifier_body @235 - Z3_get_quantifier_num_bound @236 + Z3_get_quantifier_num_bound @233 + Z3_get_quantifier_bound_name @234 + Z3_get_quantifier_bound_sort @235 + Z3_get_quantifier_body @236 Z3_simplify @237 Z3_simplify_ex @238 Z3_simplify_get_help @239 diff --git a/dll/z3_dbg.def b/dll/z3_dbg.def index 0d70389ee..0c830c94e 100644 --- a/dll/z3_dbg.def +++ b/dll/z3_dbg.def @@ -232,10 +232,10 @@ EXPORTS Z3_get_quantifier_pattern_ast @230 Z3_get_quantifier_num_no_patterns @231 Z3_get_quantifier_no_pattern_ast @232 - Z3_get_quantifier_bound_name @233 - Z3_get_quantifier_bound_sort @234 - Z3_get_quantifier_body @235 - Z3_get_quantifier_num_bound @236 + Z3_get_quantifier_num_bound @233 + Z3_get_quantifier_bound_name @234 + Z3_get_quantifier_bound_sort @235 + Z3_get_quantifier_body @236 Z3_simplify @237 Z3_simplify_ex @238 Z3_simplify_get_help @239 diff --git a/lib/api.py b/lib/api.py index 1382a9a18..71449f43b 100644 --- a/lib/api.py +++ b/lib/api.py @@ -57,10 +57,9 @@ def _find_lib(): _dir = os.path.dirname(os.path.abspath(__file__)) libs = ['z3.dll', 'libz3.so', 'libz3.dylib'] if sys.maxsize > 2**32: - winlibdir = 'x64' + locs = [_dir, '%s%s..%sx64%sexternal' % (_dir, os.sep, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] else: - winlibdir = 'bin' - locs = [_dir, '%s%s..%s%s' % (_dir, os.sep, os.sep, winlibdir), '%s%s..%slib' % (_dir, os.sep, os.sep), '%s%s..%sexternal' % (_dir, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] + locs = [_dir, '%s%s..%sexternal' % (_dir, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] for loc in locs: for lib in libs: f = '%s%s%s' % (loc, os.sep, lib) diff --git a/python/README-linux.txt b/python/README-linux.txt deleted file mode 100644 index 037e609cc..000000000 --- a/python/README-linux.txt +++ /dev/null @@ -1,26 +0,0 @@ -In your Python application you should include: - - from z3 import * - -Installing the Z3 Python bindings - -Option 1: Install Z3 Python bindings in your python distribution ----------------------------------------------------------------- - -To install the Z3 python bindings in your system, use - sudo make install-python -in the Z3 root directory. -After installing the Z3 python bindings, you can try the example application - python example.py - -Option 2: Set PYTHONPATH ------------------------- - -You may also use Z3Py by including this directory in your PYTHONPATH. -Z3Py searches for libz3.so in set of predefined places that includes the directory where Z3Py is stored. -You may also manually initialize Z3Py using the command z3.init(path-to-libz3.so) - -Learn more about Z3Py at: -http://rise4fun.com/Z3Py/tutorial/guide - - diff --git a/python/README-osx.txt b/python/README-osx.txt deleted file mode 100644 index b3fd134aa..000000000 --- a/python/README-osx.txt +++ /dev/null @@ -1,24 +0,0 @@ -In your Python application you should include: - - from z3 import * - -Installing the Z3 Python bindings - -Option 1: Install Z3 Python bindings in your python distribution ----------------------------------------------------------------- - -To install the Z3 python bindings in your system, use - sudo make install-python -in the Z3 root directory. -After installing the Z3 python bindings, you can try the example application - python example.py - -Option 2: Set PYTHONPATH ------------------------- - -You may also use Z3Py by including this directory in your PYTHONPATH. -Z3Py searches for libz3.dylib in set of predefined places that includes the directory where Z3Py is stored. -You may also manually initialize Z3Py using the command z3.init(path-to-libz3.dylib) - -Learn more about Z3Py at: -http://rise4fun.com/Z3Py/tutorial/guide diff --git a/python/README-win.txt b/python/README-win.txt deleted file mode 100644 index 7ff47a2e4..000000000 --- a/python/README-win.txt +++ /dev/null @@ -1,16 +0,0 @@ -To run the test script execute: -python example.py - -To create scripts using Z3Py, the Z3 python directory must be in your PYTHONPATH. -If you copy the z3*.py files to a different directory, you must also copy the z3.dll. -Remark: if you are using python 32-bit, you must copy the z3.dll in the bin directory. -If you are using python 64-bit, you must copy the z3.dll in the x64 directory. - -You may also manually initialize Z3Py using the command z3.init(path-to-z3.dll) - -In your Python application you should include: - - from z3 import * - -Learn more about Z3Py at: -http://rise4fun.com/Z3Py/tutorial/guide diff --git a/python/README.txt b/python/README.txt index 04791f5f7..9831c6fc6 100644 --- a/python/README.txt +++ b/python/README.txt @@ -1,5 +1,20 @@ -To run the test script execute: -python example.py - -Learn more about Z3Py at: +You can learn more about Z3Py at: http://rise4fun.com/Z3Py/tutorial/guide + +On Windows, you must build Z3 before using Z3Py. +To build Z3, you should executed the following command +in the Z3 root directory at the Visual Studio Command Prompt + + msbuild /p:configuration=external + +If you are using a 64-bit Python interpreter, you should use + + msbuild /p:configuration=external /p:platform=x64 + + +On Linux and OSX, you must install Z3Py, before trying example.py. +To install Z3Py on Linux and OSX, you should execute the following +command in the Z3 root directory + + sudo make install-z3py + diff --git a/python/exec-linux.sh b/python/exec-linux.sh deleted file mode 100644 index 6a775a767..000000000 --- a/python/exec-linux.sh +++ /dev/null @@ -1,2 +0,0 @@ -export PYTHONPATH=../../python:$PYTHONPATH -python example.py \ No newline at end of file diff --git a/python/exec-osx.sh b/python/exec-osx.sh deleted file mode 100644 index c32d0884f..000000000 --- a/python/exec-osx.sh +++ /dev/null @@ -1,2 +0,0 @@ -export PYTHONPATH=../../python:$PYTHONPATH -python example.py diff --git a/python/run-linux.sh b/python/run-linux.sh deleted file mode 100644 index dc0e24d2c..000000000 --- a/python/run-linux.sh +++ /dev/null @@ -1,2 +0,0 @@ -export LD_LIBRARY_PATH=. -python example.py diff --git a/python/run-osx.sh b/python/run-osx.sh deleted file mode 100644 index dc0e24d2c..000000000 --- a/python/run-osx.sh +++ /dev/null @@ -1,2 +0,0 @@ -export LD_LIBRARY_PATH=. -python example.py diff --git a/python/run.sh b/python/run.sh deleted file mode 100644 index dc0e24d2c..000000000 --- a/python/run.sh +++ /dev/null @@ -1,2 +0,0 @@ -export LD_LIBRARY_PATH=. -python example.py diff --git a/python/z3core.py b/python/z3core.py index 90894e9ff..588e9fa86 100644 --- a/python/z3core.py +++ b/python/z3core.py @@ -8,10 +8,9 @@ def _find_lib(): _dir = os.path.dirname(os.path.abspath(__file__)) libs = ['z3.dll', 'libz3.so', 'libz3.dylib'] if sys.maxsize > 2**32: - winlibdir = 'x64' + locs = [_dir, '%s%s..%sx64%sexternal' % (_dir, os.sep, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] else: - winlibdir = 'bin' - locs = [_dir, '%s%s..%s%s' % (_dir, os.sep, os.sep, winlibdir), '%s%s..%slib' % (_dir, os.sep, os.sep), '%s%s..%sexternal' % (_dir, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] + locs = [_dir, '%s%s..%sexternal' % (_dir, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] for loc in locs: for lib in libs: f = '%s%s%s' % (loc, os.sep, lib) From ad107bfc42ee770850b73149be375223d917d9a4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Oct 2012 21:47:46 -0700 Subject: [PATCH 04/16] fixed typos Signed-off-by: Leonardo de Moura --- configure.in | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/configure.in b/configure.in index 8236334a4..421c9a3c0 100644 --- a/configure.in +++ b/configure.in @@ -150,9 +150,10 @@ Z3 was configured with success. Host platform: $PLATFORM Arithmetic: $ARITH Python Support: $HAS_PYTHON_MSG -Pyyhon: $PYTHON +Python: $PYTHON +Prefix: $prefix Type 'make' to compile Z3. Type 'sudo make install' to install Z3. -Type 'sudo make install-python' to install Z3 Python bindings. +Type 'sudo make install-z3py' to install Z3 Python (Z3Py) bindings. EOF From 4dc834d5ee30e7853a5beebae7bbd19ac5488b4a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Oct 2012 21:59:09 -0700 Subject: [PATCH 05/16] making sure that Z3 can be compiled with cygwin/g++ Signed-off-by: Leonardo de Moura --- configure.in | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/configure.in b/configure.in index 421c9a3c0..2b403a421 100644 --- a/configure.in +++ b/configure.in @@ -47,7 +47,15 @@ AS_IF([test "$host_os" = "Darwin"], [ SLIBFLAGS="-shared -fopenmp" COMP_VERSIONS= STATIC_FLAGS=-static -], [ +], [test "${host_os:0:6}" = "CYGWIN"], [ + PLATFORM=win + SO_EXT=dll + LDFLAGS= + SLIBFLAGS="-shared -fopenmp" + COMP_VERSIONS= + STATIC_FLAGS=-static +], +[ AC_MSG_ERROR([Unknown host platform: $host_os]) ]) AC_SUBST(PLATFORM) From 1f61381172121b58821fcd9ed5cb3e8945d8c429 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Oct 2012 00:07:16 -0700 Subject: [PATCH 06/16] trying to compile Z3 using cygwin/gcc... Signed-off-by: Leonardo de Moura --- configure.in | 1 + lib/dimacs.cpp | 2 ++ lib/dl_context.h | 4 ++++ lib/hash.h | 2 -- lib/pdr_context.h | 4 ++++ lib/scoped_timer.cpp | 16 ++++++++++------ lib/stopwatch.h | 2 +- lib/trace.h | 5 +++++ 8 files changed, 27 insertions(+), 9 deletions(-) diff --git a/configure.in b/configure.in index 2b403a421..fc0e55e1e 100644 --- a/configure.in +++ b/configure.in @@ -54,6 +54,7 @@ AS_IF([test "$host_os" = "Darwin"], [ SLIBFLAGS="-shared -fopenmp" COMP_VERSIONS= STATIC_FLAGS=-static + CPPFLAGS+=" -D_CYGWIN" ], [ AC_MSG_ERROR([Unknown host platform: $host_os]) diff --git a/lib/dimacs.cpp b/lib/dimacs.cpp index 51b964dd3..3aa8591f9 100644 --- a/lib/dimacs.cpp +++ b/lib/dimacs.cpp @@ -17,6 +17,8 @@ Revision History: --*/ #include"dimacs.h" +#undef max +#undef min #include"sat_solver.h" class stream_buffer { diff --git a/lib/dl_context.h b/lib/dl_context.h index 5db3c22b7..462e83ede 100644 --- a/lib/dl_context.h +++ b/lib/dl_context.h @@ -19,6 +19,10 @@ Revision History: #ifndef _DL_CONTEXT_H_ #define _DL_CONTEXT_H_ +#ifdef _CYGWIN +#undef min +#undef max +#endif #include"arith_decl_plugin.h" #include"front_end_params.h" #include"map.h" diff --git a/lib/hash.h b/lib/hash.h index 581f8e4d2..3c7e50a6c 100644 --- a/lib/hash.h +++ b/lib/hash.h @@ -21,11 +21,9 @@ Revision History: #include -#ifndef _WINDOWS #ifndef __fallthrough #define __fallthrough #endif -#endif #define mix(a,b,c) \ { \ diff --git a/lib/pdr_context.h b/lib/pdr_context.h index e0ac2c53d..801ee6103 100644 --- a/lib/pdr_context.h +++ b/lib/pdr_context.h @@ -20,6 +20,10 @@ Revision History: #ifndef _PDR_CONTEXT_H_ #define _PDR_CONTEXT_H_ +#ifdef _CYGWIN +#undef min +#undef max +#endif #include #include "pdr_manager.h" #include "dl_base.h" diff --git a/lib/scoped_timer.cpp b/lib/scoped_timer.cpp index 008529308..c2583921d 100644 --- a/lib/scoped_timer.cpp +++ b/lib/scoped_timer.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include"z3_exception.h" #include"z3_omp.h" -#ifdef _WINDOWS +#if defined(_WINDOWS) || defined(_CYGWIN) // Windows #include #elif defined(__APPLE__) && defined(__MACH__) @@ -40,12 +40,16 @@ Revision History: #endif #include"scoped_timer.h" +#ifdef _CYGWIN +#undef min +#undef max +#endif #include"util.h" #include struct scoped_timer::imp { event_handler * m_eh; -#ifdef _WINDOWS +#if defined(_WINDOWS) || defined(_CYGWIN) HANDLE m_timer; bool m_first; #elif defined(__APPLE__) && defined(__MACH__) @@ -62,7 +66,7 @@ struct scoped_timer::imp { timer_t m_timerid; #endif -#ifdef _WINDOWS +#if defined(_WINDOWS) || defined(_CYGWIN) static void CALLBACK abort_proc(PVOID param, BOOLEAN timer_or_wait_fired) { imp * obj = static_cast(param); if (obj->m_first) { @@ -117,7 +121,7 @@ struct scoped_timer::imp { imp(unsigned ms, event_handler * eh): m_eh(eh) { -#ifdef _WINDOWS +#if defined(_WINDOWS) || defined(_CYGWIN) m_first = true; CreateTimerQueueTimer(&m_timer, NULL, @@ -167,7 +171,7 @@ struct scoped_timer::imp { } ~imp() { -#ifdef _WINDOWS +#if defined(_WINDOWS) || defined(_CYGWIN) DeleteTimerQueueTimer(NULL, m_timer, INVALID_HANDLE_VALUE); @@ -191,7 +195,7 @@ struct scoped_timer::imp { }; -#ifdef _WINDOWS +#if defined(_WINDOWS) || defined(_CYGWIN) #elif defined(__APPLE__) && defined(__MACH__) // Mac OS X #else diff --git a/lib/stopwatch.h b/lib/stopwatch.h index e27141924..661d3762b 100644 --- a/lib/stopwatch.h +++ b/lib/stopwatch.h @@ -20,7 +20,7 @@ Revision History: #ifndef _STOPWATCH_H_ #define _STOPWATCH_H_ -#ifdef _WINDOWS +#if defined(_WINDOWS) || defined(_CYGWIN) // Does this redefinition work? #define ARRAYSIZE_TEMP ARRAYSIZE diff --git a/lib/trace.h b/lib/trace.h index ac87dbb7a..941520f87 100644 --- a/lib/trace.h +++ b/lib/trace.h @@ -19,6 +19,11 @@ Revision History: #ifndef _TRACE_H_ #define _TRACE_H_ + +#ifdef _CYGWIN +#undef max +#undef min +#endif #include #ifdef _TRACE From 6c475660d8fb6fafa40510b0703c3aafbcf79072 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 12 Oct 2012 15:12:21 +0100 Subject: [PATCH 07/16] Removed support for signed assemblies. Users are advised to build their own assemblies from the source code, which they can sign using their own private keys. Signed-off-by: Christoph M. Wintersteiger --- Microsoft.Z3/Microsoft.Z3.csproj | 8 +++--- Microsoft.Z3/z3.snk | Bin 596 -> 0 bytes Microsoft.Z3V3/AssemblyInfo.cpp | 14 +++++----- Microsoft.Z3V3/Microsoft.Z3V3.vcxproj | 36 +++++++++++++++++--------- Microsoft.Z3V3/z3.snk | Bin 596 -> 0 bytes 5 files changed, 34 insertions(+), 24 deletions(-) delete mode 100644 Microsoft.Z3/z3.snk delete mode 100644 Microsoft.Z3V3/z3.snk diff --git a/Microsoft.Z3/Microsoft.Z3.csproj b/Microsoft.Z3/Microsoft.Z3.csproj index 9ca28df75..62ec169b0 100644 --- a/Microsoft.Z3/Microsoft.Z3.csproj +++ b/Microsoft.Z3/Microsoft.Z3.csproj @@ -208,10 +208,11 @@ true - true + false - z3.snk + + false @@ -293,9 +294,6 @@ - - - diff --git a/Microsoft.Z3/z3.snk b/Microsoft.Z3/z3.snk deleted file mode 100644 index 1c1ac87139db582e9021fd69893f32c23450bc67..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 596 zcmV-a0;~N80ssI2Bme+XQ$aES1ONa50097ZdN^E`fV9($I`dn<1f}a+1i;_!$y;J4 zee;lDbzQFm79@J~Ur^w}{$f#z2?xqAj>XryfQ*x%kO4Cl)u^c0HB!a{bvPi?)i8iv zfIOQ{?t#eU5G(LC{DMJ7?Yfb}*D0r<0RC%R3_qZ=Dz~^8!WLVA67o=R^5!ctR?E5r zTZTnWM3seP-F7UD=c-9e^wfVQrSDO_|F(yHd1Bi}9*{u0P5bXD-4|d?GB!uf5dL6D zA@1Iy352^5cF^X1u9ob7yioyvp%rI31-q*Z{P_7~oJ*&An4NRDD-@o-``1PLAWHZ< z<@D<3OD2z@fg*XSeCl2cQN{4XIW5m=ajoGS;Zfb6lN_Ff@*0vkeA}cfGrqL%0IlIw z`)!pN!Wc?1${pgpA0^pS(kzGn1#`S=5RamF3XZsCQ0+AJ+JS&{RP$uvs?*qkWrUxo+PV zgx9qdq7iY6(QhyrK;^KOslOqAWXw=mb`m(|xeT+xFTyojbY+%->2=77E*~oQtZN>S zq9xdu!RmBGMdK0RfJ6YMBHDi%@3`wydNE*iYSuEg@V?E=f0CG iozI4Z`K&(xgd3HMachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -282,7 +283,8 @@ MachineX64 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -306,7 +308,8 @@ MachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -330,7 +333,8 @@ MachineX64 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -354,7 +358,8 @@ MachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -377,7 +382,8 @@ MachineX64 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -401,7 +407,8 @@ MachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -426,7 +433,8 @@ true - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -450,7 +458,8 @@ MachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)35MSSharedLib1024.snk" + + @@ -475,7 +484,8 @@ true - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -499,14 +509,16 @@ MachineX64 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)35MSSharedLib1024.snk" + + - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + diff --git a/Microsoft.Z3V3/z3.snk b/Microsoft.Z3V3/z3.snk deleted file mode 100644 index 1c1ac87139db582e9021fd69893f32c23450bc67..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 596 zcmV-a0;~N80ssI2Bme+XQ$aES1ONa50097ZdN^E`fV9($I`dn<1f}a+1i;_!$y;J4 zee;lDbzQFm79@J~Ur^w}{$f#z2?xqAj>XryfQ*x%kO4Cl)u^c0HB!a{bvPi?)i8iv zfIOQ{?t#eU5G(LC{DMJ7?Yfb}*D0r<0RC%R3_qZ=Dz~^8!WLVA67o=R^5!ctR?E5r zTZTnWM3seP-F7UD=c-9e^wfVQrSDO_|F(yHd1Bi}9*{u0P5bXD-4|d?GB!uf5dL6D zA@1Iy352^5cF^X1u9ob7yioyvp%rI31-q*Z{P_7~oJ*&An4NRDD-@o-``1PLAWHZ< z<@D<3OD2z@fg*XSeCl2cQN{4XIW5m=ajoGS;Zfb6lN_Ff@*0vkeA}cfGrqL%0IlIw z`)!pN!Wc?1${pgpA0^pS(kzGn1#`S=5RamF3XZsCQ0+AJ+JS&{RP$uvs?*qkWrUxo+PV zgx9qdq7iY6(QhyrK;^KOslOqAWXw=mb`m(|xeT+xFTyojbY+%->2=77E*~oQtZN>S zq9xdu!RmBGMdK0RfJ6YMBHDi%@3`wydNE*iYSuEg@V?E=f0CG iozI4Z`K&(xgd3H Date: Fri, 12 Oct 2012 15:13:38 +0100 Subject: [PATCH 08/16] Formatting and build configuration fixes. Signed-off-by: Christoph M. Wintersteiger --- Microsoft.Z3/Log.cs | 88 +++++++++++++++++++++--------------------- Microsoft.Z3/Solver.cs | 28 ++++++++------ z3-prover.sln | 10 ++++- 3 files changed, 68 insertions(+), 58 deletions(-) diff --git a/Microsoft.Z3/Log.cs b/Microsoft.Z3/Log.cs index 9058f73f5..f8b2ea88b 100644 --- a/Microsoft.Z3/Log.cs +++ b/Microsoft.Z3/Log.cs @@ -22,58 +22,58 @@ using System.Diagnostics.Contracts; namespace Microsoft.Z3 { - /// - /// Interaction logging for Z3. - /// - /// - /// Note that this is a global, static log and if multiple Context - /// objects are created, it logs the interaction with all of them. - /// + /// + /// Interaction logging for Z3. + /// + /// + /// Note that this is a global, static log and if multiple Context + /// objects are created, it logs the interaction with all of them. + /// [ContractVerification(true)] public static class Log - { - private static bool m_is_open = false; - - /// - /// Open an interaction log file. - /// - /// the name of the file to open - /// True if opening the log file succeeds, false otherwise. - public static bool Open(string filename) { - m_is_open = true; - return Native.Z3_open_log(filename) == 1; - } + private static bool m_is_open = false; - /// - /// Closes the interaction log. - /// - public static void Close() - { - m_is_open = false; - Native.Z3_close_log(); - } + /// + /// Open an interaction log file. + /// + /// the name of the file to open + /// True if opening the log file succeeds, false otherwise. + public static bool Open(string filename) + { + m_is_open = true; + return Native.Z3_open_log(filename) == 1; + } - /// - /// Appends the user-provided string to the interaction log. - /// - public static void Append(string s) - { - Contract.Requires(isOpen()); + /// + /// Closes the interaction log. + /// + public static void Close() + { + m_is_open = false; + Native.Z3_close_log(); + } - if (!m_is_open) - throw new Z3Exception("Log cannot be closed."); - Native.Z3_append_log(s); - } + /// + /// Appends the user-provided string to the interaction log. + /// + public static void Append(string s) + { + Contract.Requires(isOpen()); - /// - /// Checks whether the interaction log is opened. - /// - /// True if the interaction log is open, false otherwise. + if (!m_is_open) + throw new Z3Exception("Log cannot be closed."); + Native.Z3_append_log(s); + } + + /// + /// Checks whether the interaction log is opened. + /// + /// True if the interaction log is open, false otherwise. [Pure] public static bool isOpen() - { - return m_is_open; + { + return m_is_open; + } } - } } diff --git a/Microsoft.Z3/Solver.cs b/Microsoft.Z3/Solver.cs index 2403108c1..6450a8cbc 100644 --- a/Microsoft.Z3/Solver.cs +++ b/Microsoft.Z3/Solver.cs @@ -33,10 +33,12 @@ namespace Microsoft.Z3 /// public string Help { - get { + get + { Contract.Ensures(Contract.Result() != null); - return Native.Z3_solver_get_help(Context.nCtx, NativeObject); } + return Native.Z3_solver_get_help(Context.nCtx, NativeObject); + } } /// @@ -56,13 +58,13 @@ namespace Microsoft.Z3 /// /// Retrieves parameter descriptions for solver. /// - ParamDescrs ParameterDescriptions - { - get - { - return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); - } - } + public ParamDescrs ParameterDescriptions + { + get + { + return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); + } + } /// @@ -250,10 +252,12 @@ namespace Microsoft.Z3 /// public Statistics Statistics { - get { + get + { Contract.Ensures(Contract.Result() != null); - return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject)); } + return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject)); + } } /// @@ -282,7 +286,7 @@ namespace Microsoft.Z3 { Native.Z3_solver_dec_ref(ctx.nCtx, obj); } - }; + }; internal override void IncRef(IntPtr o) { diff --git a/z3-prover.sln b/z3-prover.sln index 7823930ae..1b016a5e9 100644 --- a/z3-prover.sln +++ b/z3-prover.sln @@ -276,6 +276,7 @@ Global {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|Mixed Platforms.ActiveCfg = external|Win32 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|Mixed Platforms.Build.0 = external|Win32 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|Win32.ActiveCfg = Release|Win32 + {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|Win32.Build.0 = Release|Win32 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|x64.ActiveCfg = external|x64 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|x64.Build.0 = external|x64 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|x86.ActiveCfg = Release|Win32 @@ -326,6 +327,7 @@ Global {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|Mixed Platforms.ActiveCfg = external|Win32 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|Mixed Platforms.Build.0 = external|Win32 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|Win32.ActiveCfg = external|Win32 + {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|Win32.Build.0 = external|Win32 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|x64.ActiveCfg = external|x64 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|x64.Build.0 = external|x64 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|x86.ActiveCfg = external|x64 @@ -374,6 +376,7 @@ Global {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|Mixed Platforms.ActiveCfg = external|Win32 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|Mixed Platforms.Build.0 = external|Win32 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|Win32.ActiveCfg = external|Win32 + {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|Win32.Build.0 = external|Win32 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|x64.ActiveCfg = external|x64 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|x64.Build.0 = external|x64 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|x86.ActiveCfg = external|x64 @@ -422,6 +425,7 @@ Global {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|Mixed Platforms.ActiveCfg = external|Win32 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|Mixed Platforms.Build.0 = external|Win32 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|Win32.ActiveCfg = external|Win32 + {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|Win32.Build.0 = external|Win32 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|x64.ActiveCfg = external|x64 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|x64.Build.0 = external|x64 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|x86.ActiveCfg = external|x64 @@ -469,7 +473,8 @@ Global {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Any CPU.ActiveCfg = external|Any CPU {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Mixed Platforms.ActiveCfg = external|Any CPU {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Mixed Platforms.Build.0 = external|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Win32.ActiveCfg = external|x64 + {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Win32.ActiveCfg = external|Any CPU + {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Win32.Build.0 = external|Any CPU {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|x64.ActiveCfg = external|x64 {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|x64.Build.0 = external|x64 {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|x86.ActiveCfg = external|x64 @@ -517,7 +522,8 @@ Global {D350BC78-8455-45D3-9759-073394378BF2}.external|Any CPU.ActiveCfg = Release|x64 {D350BC78-8455-45D3-9759-073394378BF2}.external|Mixed Platforms.ActiveCfg = Release|x86 {D350BC78-8455-45D3-9759-073394378BF2}.external|Mixed Platforms.Build.0 = Release|x86 - {D350BC78-8455-45D3-9759-073394378BF2}.external|Win32.ActiveCfg = Release|x64 + {D350BC78-8455-45D3-9759-073394378BF2}.external|Win32.ActiveCfg = Release|Any CPU + {D350BC78-8455-45D3-9759-073394378BF2}.external|Win32.Build.0 = Release|Any CPU {D350BC78-8455-45D3-9759-073394378BF2}.external|x64.ActiveCfg = Release|x64 {D350BC78-8455-45D3-9759-073394378BF2}.external|x64.Build.0 = Release|x64 {D350BC78-8455-45D3-9759-073394378BF2}.external|x86.ActiveCfg = Release|x64 From b0a2d8488d53a0591011913af78a20ec982c5b48 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Oct 2012 07:47:55 -0700 Subject: [PATCH 09/16] added repr method to ParamDescrs Signed-off-by: Leonardo de Moura --- python/z3.py | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/python/z3.py b/python/z3.py index 9d9d03e55..dea752a87 100644 --- a/python/z3.py +++ b/python/z3.py @@ -43,6 +43,7 @@ from z3types import * from z3consts import * from z3tactics import * from z3printer import * +import io # We use _z3_assert instead of the assert command because we want to # produce nice error messages in Z3Py at rise4fun.com @@ -4419,6 +4420,20 @@ class ParamDescrsRef: else: return self.get_kind(arg) + def __repr__(self): + r = io.StringIO() + first = True + r.write(u'(') + for i in range(self.size()): + if first: + first = False + else: + r.write(u' ') + r.write(u'%s' % self.get_name(i)) + r.write(u')') + return r.getvalue() + + ######################################### # # Goals From 42c27b7a46aff7e6442b52f3a2909db9d2aa673e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 12 Oct 2012 16:44:46 +0100 Subject: [PATCH 10/16] Added ParamDescr.ToString() Formatting Signed-off-by: Christoph M. Wintersteiger --- Microsoft.Z3/Context.cs | 76 ++++++++++++++++++------------------- Microsoft.Z3/Fixedpoint.cs | 38 +++++++++---------- Microsoft.Z3/ParamDescrs.cs | 23 ++++++++++- Microsoft.Z3/Solver.cs | 5 +-- Microsoft.Z3/Tactic.cs | 26 ++++++------- 5 files changed, 90 insertions(+), 78 deletions(-) diff --git a/Microsoft.Z3/Context.cs b/Microsoft.Z3/Context.cs index 597b9b7c6..27bbf6d42 100644 --- a/Microsoft.Z3/Context.cs +++ b/Microsoft.Z3/Context.cs @@ -50,7 +50,7 @@ namespace Microsoft.Z3 Contract.Requires(settings != null); IntPtr cfg = Native.Z3_mk_config(); - foreach(KeyValuePair kv in settings) + foreach (KeyValuePair kv in settings) Native.Z3_set_param_value(cfg, kv.Key, kv.Value); m_ctx = Native.Z3_mk_context_rc(cfg); Native.Z3_del_config(cfg); @@ -88,7 +88,7 @@ namespace Microsoft.Z3 /// internal Symbol[] MkSymbols(string[] names) { - Contract.Ensures(names == null || Contract.Result() != null); + Contract.Ensures(names == null || Contract.Result() != null); Contract.Ensures(names != null || Contract.Result() == null); Contract.Ensures(Contract.Result() == null || Contract.Result().Length == names.Length); Contract.Ensures(Contract.Result() == null || Contract.ForAll(Contract.Result(), s => s != null)); @@ -129,7 +129,7 @@ namespace Microsoft.Z3 if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort; } } - + /// /// Retrieves the Real sort of the context. @@ -204,7 +204,7 @@ namespace Microsoft.Z3 Contract.Requires(domain != null); Contract.Requires(range != null); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(domain); CheckContextMatch(range); return new ArraySort(this, domain, range); @@ -392,9 +392,9 @@ namespace Microsoft.Z3 Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays"); CheckContextMatch(constructor); cla[i] = new ConstructorList(this, constructor); - n_constr[i] = cla[i].NativeObject; + n_constr[i] = cla[i].NativeObject; } - IntPtr[] n_res = new IntPtr[n]; + IntPtr[] n_res = new IntPtr[n]; Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr); DatatypeSort[] res = new DatatypeSort[n]; for (uint i = 0; i < n; i++) @@ -526,7 +526,7 @@ namespace Microsoft.Z3 CheckContextMatch(range); return new FuncDecl(this, MkSymbol(name), null, range); - } + } /// /// Creates a fresh constant function declaration with a name prefixed with . @@ -728,7 +728,7 @@ namespace Microsoft.Z3 CheckContextMatch(f); CheckContextMatch(args); return Expr.Create(this, f, args); - } + } #region Propositional /// @@ -800,7 +800,7 @@ namespace Microsoft.Z3 CheckContextMatch(a); return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject)); } - + /// /// Create an expression representing an if-then-else: ite(t1, t2, t3). /// @@ -895,7 +895,7 @@ namespace Microsoft.Z3 /// public ArithExpr MkAdd(params ArithExpr[] t) { - Contract.Requires(t != null); + Contract.Requires(t != null); Contract.Requires(Contract.ForAll(t, a => a != null)); Contract.Ensures(Contract.Result() != null); @@ -1167,7 +1167,7 @@ namespace Microsoft.Z3 Contract.Requires(t1 != null); Contract.Requires(t2 != null); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(t1); CheckContextMatch(t2); return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject)); @@ -1634,8 +1634,8 @@ namespace Microsoft.Z3 { Contract.Requires(t1 != null); Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); - + Contract.Ensures(Contract.Result() != null); + CheckContextMatch(t1); CheckContextMatch(t2); return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject)); @@ -1658,7 +1658,7 @@ namespace Microsoft.Z3 Contract.Requires(t1 != null); Contract.Requires(t2 != null); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(t1); CheckContextMatch(t2); return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject)); @@ -1683,7 +1683,7 @@ namespace Microsoft.Z3 Contract.Requires(t1 != null); Contract.Requires(t2 != null); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(t1); CheckContextMatch(t2); return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject)); @@ -1700,7 +1700,7 @@ namespace Microsoft.Z3 { Contract.Requires(t != null); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject)); } @@ -2147,7 +2147,7 @@ namespace Microsoft.Z3 { Contract.Requires(args != null); Contract.Requires(Contract.ForAll(args, a => a != null)); - + CheckContextMatch(args); return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } @@ -2213,7 +2213,7 @@ namespace Microsoft.Z3 Contract.Requires(arg1 != null); Contract.Requires(arg2 != null); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(arg1); CheckContextMatch(arg2); return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject)); @@ -2538,7 +2538,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(names, n => n != null)); Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); - + Contract.Ensures(Contract.Result() != null); return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); @@ -2607,7 +2607,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(names, n => n != null)); Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); - + Contract.Ensures(Contract.Result() != null); if (universal) @@ -2626,7 +2626,7 @@ namespace Microsoft.Z3 Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null)); Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); - + Contract.Ensures(Contract.Result() != null); if (universal) @@ -2702,10 +2702,10 @@ namespace Microsoft.Z3 uint cdn = Symbol.ArrayLength(declNames); uint cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); + throw new Z3Exception("Argument size mismatch"); Native.Z3_parse_smtlib_string(nCtx, str, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); + AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); } /// @@ -2722,7 +2722,7 @@ namespace Microsoft.Z3 throw new Z3Exception("Argument size mismatch"); Native.Z3_parse_smtlib_file(nCtx, fileName, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); + AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); } /// @@ -2811,7 +2811,7 @@ namespace Microsoft.Z3 res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i)); return res; } - } + } /// /// Parse the given string using the SMT-LIB2 parser. @@ -2965,7 +2965,7 @@ namespace Microsoft.Z3 Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(t1); CheckContextMatch(t2); CheckContextMatch(ts); @@ -2982,7 +2982,7 @@ namespace Microsoft.Z3 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last); return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last)); } - else + else return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject)); } @@ -3313,7 +3313,7 @@ namespace Microsoft.Z3 Contract.Requires(p1 != null); Contract.Requires(p2 != null); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(p1); CheckContextMatch(p2); return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject)); @@ -3328,7 +3328,7 @@ namespace Microsoft.Z3 Contract.Requires(p1 != null); Contract.Requires(p2 != null); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(p1); CheckContextMatch(p2); return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject)); @@ -3343,7 +3343,7 @@ namespace Microsoft.Z3 Contract.Requires(p1 != null); Contract.Requires(p2 != null); Contract.Ensures(Contract.Result() != null); - + CheckContextMatch(p1); CheckContextMatch(p2); return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject)); @@ -3423,7 +3423,7 @@ namespace Microsoft.Z3 /// /// Create a Fixedpoint context. /// - public Fixedpoint MkFixedpoint() + public Fixedpoint MkFixedpoint() { Contract.Ensures(Contract.Result() != null); @@ -3464,7 +3464,7 @@ namespace Microsoft.Z3 { return a.NativeObject; } - + /// /// Return a string describing all available parameters to Expr.Simplify. /// @@ -3478,14 +3478,10 @@ namespace Microsoft.Z3 /// /// Retrieves parameter descriptions for simplifier. /// - public ParamDescrs SimplifyParameterDescriptions - { - get - { - return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); - } - } - + public ParamDescrs SimplifyParameterDescriptions + { + get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); } + } /// /// Enable/disable printing of warning messages to the console. diff --git a/Microsoft.Z3/Fixedpoint.cs b/Microsoft.Z3/Fixedpoint.cs index ae94c4d24..3e04e6169 100644 --- a/Microsoft.Z3/Fixedpoint.cs +++ b/Microsoft.Z3/Fixedpoint.cs @@ -34,10 +34,11 @@ namespace Microsoft.Z3 /// public string Help { - get { + get + { Contract.Ensures(Contract.Result() != null); - return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject); - } + return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject); + } } /// @@ -56,13 +57,10 @@ namespace Microsoft.Z3 /// /// Retrieves parameter descriptions for Fixedpoint solver. /// - public ParamDescrs ParameterDescriptions - { - get - { - return new ParamDescrs(Context, Native.Z3_fixedpoint_get_param_descrs(Context.nCtx, NativeObject)); - } - } + public ParamDescrs ParameterDescriptions + { + get { return new ParamDescrs(Context, Native.Z3_fixedpoint_get_param_descrs(Context.nCtx, NativeObject)); } + } /// @@ -146,7 +144,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null)); Context.CheckContextMatch(relations); - Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject, + Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject, AST.ArrayLength(relations), AST.ArrayToNative(relations)); switch (r) { @@ -179,7 +177,7 @@ namespace Microsoft.Z3 /// /// Update named rule into in the fixedpoint solver. /// - public void UpdateRule(BoolExpr rule, Symbol name) + public void UpdateRule(BoolExpr rule, Symbol name) { Contract.Requires(rule != null); @@ -210,18 +208,18 @@ namespace Microsoft.Z3 /// /// Retrieve the number of levels explored for a given predicate. /// - public uint GetNumLevels(FuncDecl predicate) - { - return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject); - } + public uint GetNumLevels(FuncDecl predicate) + { + return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject); + } /// /// Retrieve the cover of a predicate. /// public Expr GetCoverDelta(int level, FuncDecl predicate) { - IntPtr res = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject); - return (res == IntPtr.Zero) ? null : Expr.Create(Context, res); + IntPtr res = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject); + return (res == IntPtr.Zero) ? null : Expr.Create(Context, res); } /// @@ -230,7 +228,7 @@ namespace Microsoft.Z3 /// public void AddCover(int level, FuncDecl predicate, Expr property) { - Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject); + Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject); } /// @@ -259,7 +257,7 @@ namespace Microsoft.Z3 public string ToString(BoolExpr[] queries) { - return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, + return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, AST.ArrayLength(queries), AST.ArrayToNative(queries)); } diff --git a/Microsoft.Z3/ParamDescrs.cs b/Microsoft.Z3/ParamDescrs.cs index f93d449a4..961bceeff 100644 --- a/Microsoft.Z3/ParamDescrs.cs +++ b/Microsoft.Z3/ParamDescrs.cs @@ -23,7 +23,7 @@ using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// - /// A ParameterSet represents a configuration in the form of Symbol/value pairs. + /// A ParamDescrs describes a set of parameters. /// [ContractVerification(true)] public class ParamDescrs : Z3Object @@ -62,6 +62,27 @@ namespace Microsoft.Z3 } } + /// + /// The size of the ParamDescrs. + /// + public uint Size + { + get { return Native.Z3_param_descrs_size(Context.nCtx, NativeObject); } + } + + /// + /// Retrieves a string representation of the ParamDescrs. + /// + public override string ToString() + { + String res = ""; + Symbol[] n = Names; + if (n.Length > 0) res = n[0].ToString(); + for (uint i = 1; i < n.Length; i++) + res += " " + n[i].ToString(); + return res; + } + #region Internal internal ParamDescrs(Context ctx, IntPtr obj) : base(ctx, obj) diff --git a/Microsoft.Z3/Solver.cs b/Microsoft.Z3/Solver.cs index 6450a8cbc..dc261bfd8 100644 --- a/Microsoft.Z3/Solver.cs +++ b/Microsoft.Z3/Solver.cs @@ -60,10 +60,7 @@ namespace Microsoft.Z3 /// public ParamDescrs ParameterDescriptions { - get - { - return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); - } + get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); } } diff --git a/Microsoft.Z3/Tactic.cs b/Microsoft.Z3/Tactic.cs index 62d9015f8..6340c9b41 100644 --- a/Microsoft.Z3/Tactic.cs +++ b/Microsoft.Z3/Tactic.cs @@ -39,21 +39,19 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - - return Native.Z3_tactic_get_help(Context.nCtx, NativeObject); } + + return Native.Z3_tactic_get_help(Context.nCtx, NativeObject); + } } /// /// Retrieves parameter descriptions for Tactics. /// - public ParamDescrs ParameterDescriptions - { - get - { - return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); - } - } + public ParamDescrs ParameterDescriptions + { + get { return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); } + } /// @@ -83,7 +81,7 @@ namespace Microsoft.Z3 { Contract.Requires(g != null); Contract.Ensures(Contract.Result() != null); - + return Apply(g); } } @@ -103,11 +101,13 @@ namespace Microsoft.Z3 } #region Internal - internal Tactic(Context ctx, IntPtr obj) : base(ctx, obj) + internal Tactic(Context ctx, IntPtr obj) + : base(ctx, obj) { Contract.Requires(ctx != null); } - internal Tactic(Context ctx, string name) : base(ctx, Native.Z3_mk_tactic(ctx.nCtx, name)) + internal Tactic(Context ctx, string name) + : base(ctx, Native.Z3_mk_tactic(ctx.nCtx, name)) { Contract.Requires(ctx != null); } @@ -123,7 +123,7 @@ namespace Microsoft.Z3 { Native.Z3_tactic_dec_ref(ctx.nCtx, obj); } - }; + }; internal override void IncRef(IntPtr o) { From f7bcd40137ed2f5d1d5c96d0771575997b9157f9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Oct 2012 09:13:04 -0700 Subject: [PATCH 11/16] Added API Z3_param_descrs_to_string Signed-off-by: Leonardo de Moura --- Microsoft.Z3/Native.cs | 11 + dll/z3.def | 989 +++++++++++++++++++++-------------------- dll/z3_dbg.def | 989 +++++++++++++++++++++-------------------- lib/api.py | 1 + lib/api_commands.cpp | 238 +++++----- lib/api_log_macros.cpp | 238 +++++----- lib/api_log_macros.h | 2 + lib/api_params.cpp | 17 + lib/z3_api.h | 6 + python/z3.py | 13 +- python/z3core.py | 9 + 11 files changed, 1281 insertions(+), 1232 deletions(-) diff --git a/Microsoft.Z3/Native.cs b/Microsoft.Z3/Native.cs index b923cce35..0c0349a78 100644 --- a/Microsoft.Z3/Native.cs +++ b/Microsoft.Z3/Native.cs @@ -1132,6 +1132,9 @@ namespace Microsoft.Z3 [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] public extern static IntPtr Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, uint a2); + [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] + public extern static IntPtr Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1); + [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)] public extern static void Z3_interrupt(Z3_context a0); @@ -4293,6 +4296,14 @@ namespace Microsoft.Z3 return r; } + public static string Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1) { + IntPtr r = LIB.Z3_param_descrs_to_string(a0, a1); + Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0); + if (err != Z3_error_code.Z3_OK) + throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err))); + return Marshal.PtrToStringAnsi(r); + } + public static void Z3_interrupt(Z3_context a0) { LIB.Z3_interrupt(a0); Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0); diff --git a/dll/z3.def b/dll/z3.def index d56875d92..e65e8b225 100644 --- a/dll/z3.def +++ b/dll/z3.def @@ -25,497 +25,498 @@ EXPORTS Z3_param_descrs_get_kind @23 Z3_param_descrs_size @24 Z3_param_descrs_get_name @25 - Z3_mk_int_symbol @26 - Z3_mk_string_symbol @27 - Z3_mk_uninterpreted_sort @28 - Z3_mk_bool_sort @29 - Z3_mk_int_sort @30 - Z3_mk_real_sort @31 - Z3_mk_bv_sort @32 - Z3_mk_finite_domain_sort @33 - Z3_mk_array_sort @34 - Z3_mk_tuple_sort @35 - Z3_mk_enumeration_sort @36 - Z3_mk_list_sort @37 - Z3_mk_constructor @38 - Z3_del_constructor @39 - Z3_mk_datatype @40 - Z3_mk_constructor_list @41 - Z3_del_constructor_list @42 - Z3_mk_datatypes @43 - Z3_query_constructor @44 - Z3_mk_func_decl @45 - Z3_mk_app @46 - Z3_mk_const @47 - Z3_mk_fresh_func_decl @48 - Z3_mk_fresh_const @49 - Z3_mk_true @50 - Z3_mk_false @51 - Z3_mk_eq @52 - Z3_mk_distinct @53 - Z3_mk_not @54 - Z3_mk_ite @55 - Z3_mk_iff @56 - Z3_mk_implies @57 - Z3_mk_xor @58 - Z3_mk_and @59 - Z3_mk_or @60 - Z3_mk_add @61 - Z3_mk_mul @62 - Z3_mk_sub @63 - Z3_mk_unary_minus @64 - Z3_mk_div @65 - Z3_mk_mod @66 - Z3_mk_rem @67 - Z3_mk_power @68 - Z3_mk_lt @69 - Z3_mk_le @70 - Z3_mk_gt @71 - Z3_mk_ge @72 - Z3_mk_int2real @73 - Z3_mk_real2int @74 - Z3_mk_is_int @75 - Z3_mk_bvnot @76 - Z3_mk_bvredand @77 - Z3_mk_bvredor @78 - Z3_mk_bvand @79 - Z3_mk_bvor @80 - Z3_mk_bvxor @81 - Z3_mk_bvnand @82 - Z3_mk_bvnor @83 - Z3_mk_bvxnor @84 - Z3_mk_bvneg @85 - Z3_mk_bvadd @86 - Z3_mk_bvsub @87 - Z3_mk_bvmul @88 - Z3_mk_bvudiv @89 - Z3_mk_bvsdiv @90 - Z3_mk_bvurem @91 - Z3_mk_bvsrem @92 - Z3_mk_bvsmod @93 - Z3_mk_bvult @94 - Z3_mk_bvslt @95 - Z3_mk_bvule @96 - Z3_mk_bvsle @97 - Z3_mk_bvuge @98 - Z3_mk_bvsge @99 - Z3_mk_bvugt @100 - Z3_mk_bvsgt @101 - Z3_mk_concat @102 - Z3_mk_extract @103 - Z3_mk_sign_ext @104 - Z3_mk_zero_ext @105 - Z3_mk_repeat @106 - Z3_mk_bvshl @107 - Z3_mk_bvlshr @108 - Z3_mk_bvashr @109 - Z3_mk_rotate_left @110 - Z3_mk_rotate_right @111 - Z3_mk_ext_rotate_left @112 - Z3_mk_ext_rotate_right @113 - Z3_mk_int2bv @114 - Z3_mk_bv2int @115 - Z3_mk_bvadd_no_overflow @116 - Z3_mk_bvadd_no_underflow @117 - Z3_mk_bvsub_no_overflow @118 - Z3_mk_bvsub_no_underflow @119 - Z3_mk_bvsdiv_no_overflow @120 - Z3_mk_bvneg_no_overflow @121 - Z3_mk_bvmul_no_overflow @122 - Z3_mk_bvmul_no_underflow @123 - Z3_mk_select @124 - Z3_mk_store @125 - Z3_mk_const_array @126 - Z3_mk_map @127 - Z3_mk_array_default @128 - Z3_mk_set_sort @129 - Z3_mk_empty_set @130 - Z3_mk_full_set @131 - Z3_mk_set_add @132 - Z3_mk_set_del @133 - Z3_mk_set_union @134 - Z3_mk_set_intersect @135 - Z3_mk_set_difference @136 - Z3_mk_set_complement @137 - Z3_mk_set_member @138 - Z3_mk_set_subset @139 - Z3_mk_numeral @140 - Z3_mk_real @141 - Z3_mk_int @142 - Z3_mk_unsigned_int @143 - Z3_mk_int64 @144 - Z3_mk_unsigned_int64 @145 - Z3_mk_pattern @146 - Z3_mk_bound @147 - Z3_mk_forall @148 - Z3_mk_exists @149 - Z3_mk_quantifier @150 - Z3_mk_quantifier_ex @151 - Z3_mk_forall_const @152 - Z3_mk_exists_const @153 - Z3_mk_quantifier_const @154 - Z3_mk_quantifier_const_ex @155 - Z3_get_symbol_kind @156 - Z3_get_symbol_int @157 - Z3_get_symbol_string @158 - Z3_get_sort_name @159 - Z3_get_sort_id @160 - Z3_sort_to_ast @161 - Z3_is_eq_sort @162 - Z3_get_sort_kind @163 - Z3_get_bv_sort_size @164 - Z3_get_finite_domain_sort_size @165 - Z3_get_array_sort_domain @166 - Z3_get_array_sort_range @167 - Z3_get_tuple_sort_mk_decl @168 - Z3_get_tuple_sort_num_fields @169 - Z3_get_tuple_sort_field_decl @170 - Z3_get_datatype_sort_num_constructors @171 - Z3_get_datatype_sort_constructor @172 - Z3_get_datatype_sort_recognizer @173 - Z3_get_datatype_sort_constructor_accessor @174 - Z3_get_relation_arity @175 - Z3_get_relation_column @176 - Z3_func_decl_to_ast @177 - Z3_is_eq_func_decl @178 - Z3_get_func_decl_id @179 - Z3_get_decl_name @180 - Z3_get_decl_kind @181 - Z3_get_domain_size @182 - Z3_get_arity @183 - Z3_get_domain @184 - Z3_get_range @185 - Z3_get_decl_num_parameters @186 - Z3_get_decl_parameter_kind @187 - Z3_get_decl_int_parameter @188 - Z3_get_decl_double_parameter @189 - Z3_get_decl_symbol_parameter @190 - Z3_get_decl_sort_parameter @191 - Z3_get_decl_ast_parameter @192 - Z3_get_decl_func_decl_parameter @193 - Z3_get_decl_rational_parameter @194 - Z3_app_to_ast @195 - Z3_get_app_decl @196 - Z3_get_app_num_args @197 - Z3_get_app_arg @198 - Z3_is_eq_ast @199 - Z3_get_ast_id @200 - Z3_get_ast_hash @201 - Z3_get_sort @202 - Z3_is_well_sorted @203 - Z3_get_bool_value @204 - Z3_get_ast_kind @205 - Z3_is_app @206 - Z3_is_numeral_ast @207 - Z3_is_algebraic_number @208 - Z3_to_app @209 - Z3_to_func_decl @210 - Z3_get_numeral_string @211 - Z3_get_numeral_decimal_string @212 - Z3_get_numerator @213 - Z3_get_denominator @214 - Z3_get_numeral_small @215 - Z3_get_numeral_int @216 - Z3_get_numeral_uint @217 - Z3_get_numeral_uint64 @218 - Z3_get_numeral_int64 @219 - Z3_get_numeral_rational_int64 @220 - Z3_get_algebraic_number_lower @221 - Z3_get_algebraic_number_upper @222 - Z3_pattern_to_ast @223 - Z3_get_pattern_num_terms @224 - Z3_get_pattern @225 - Z3_get_index_value @226 - Z3_is_quantifier_forall @227 - Z3_get_quantifier_weight @228 - Z3_get_quantifier_num_patterns @229 - Z3_get_quantifier_pattern_ast @230 - Z3_get_quantifier_num_no_patterns @231 - Z3_get_quantifier_no_pattern_ast @232 - Z3_get_quantifier_num_bound @233 - Z3_get_quantifier_bound_name @234 - Z3_get_quantifier_bound_sort @235 - Z3_get_quantifier_body @236 - Z3_simplify @237 - Z3_simplify_ex @238 - Z3_simplify_get_help @239 - Z3_simplify_get_param_descrs @240 - Z3_update_term @241 - Z3_substitute @242 - Z3_substitute_vars @243 - Z3_translate @244 - Z3_model_inc_ref @245 - Z3_model_dec_ref @246 - Z3_model_eval @247 - Z3_model_get_const_interp @248 - Z3_model_get_func_interp @249 - Z3_model_get_num_consts @250 - Z3_model_get_const_decl @251 - Z3_model_get_num_funcs @252 - Z3_model_get_func_decl @253 - Z3_model_get_num_sorts @254 - Z3_model_get_sort @255 - Z3_model_get_sort_universe @256 - Z3_is_as_array @257 - Z3_get_as_array_func_decl @258 - Z3_func_interp_inc_ref @259 - Z3_func_interp_dec_ref @260 - Z3_func_interp_get_num_entries @261 - Z3_func_interp_get_entry @262 - Z3_func_interp_get_else @263 - Z3_func_interp_get_arity @264 - Z3_func_entry_inc_ref @265 - Z3_func_entry_dec_ref @266 - Z3_func_entry_get_value @267 - Z3_func_entry_get_num_args @268 - Z3_func_entry_get_arg @269 - Z3_open_log @270 - Z3_append_log @271 - Z3_close_log @272 - Z3_toggle_warning_messages @273 - Z3_set_ast_print_mode @274 - Z3_ast_to_string @275 - Z3_pattern_to_string @276 - Z3_sort_to_string @277 - Z3_func_decl_to_string @278 - Z3_model_to_string @279 - Z3_benchmark_to_smtlib_string @280 - Z3_parse_smtlib2_string @281 - Z3_parse_smtlib2_file @282 - Z3_parse_smtlib_string @283 - Z3_parse_smtlib_file @284 - Z3_get_smtlib_num_formulas @285 - Z3_get_smtlib_formula @286 - Z3_get_smtlib_num_assumptions @287 - Z3_get_smtlib_assumption @288 - Z3_get_smtlib_num_decls @289 - Z3_get_smtlib_decl @290 - Z3_get_smtlib_num_sorts @291 - Z3_get_smtlib_sort @292 - Z3_get_smtlib_error @293 - Z3_parse_z3_string @294 - Z3_parse_z3_file @295 - Z3_get_error_code @296 - Z3_set_error_handler @297 - Z3_set_error @298 - Z3_get_error_msg @299 - Z3_get_error_msg_ex @300 - Z3_get_version @301 - Z3_reset_memory @302 - Z3_mk_theory @303 - Z3_theory_get_ext_data @304 - Z3_theory_mk_sort @305 - Z3_theory_mk_value @306 - Z3_theory_mk_constant @307 - Z3_theory_mk_func_decl @308 - Z3_theory_get_context @309 - Z3_set_delete_callback @310 - Z3_set_reduce_app_callback @311 - Z3_set_reduce_eq_callback @312 - Z3_set_reduce_distinct_callback @313 - Z3_set_new_app_callback @314 - Z3_set_new_elem_callback @315 - Z3_set_init_search_callback @316 - Z3_set_push_callback @317 - Z3_set_pop_callback @318 - Z3_set_restart_callback @319 - Z3_set_reset_callback @320 - Z3_set_final_check_callback @321 - Z3_set_new_eq_callback @322 - Z3_set_new_diseq_callback @323 - Z3_set_new_assignment_callback @324 - Z3_set_new_relevant_callback @325 - Z3_theory_assert_axiom @326 - Z3_theory_assume_eq @327 - Z3_theory_enable_axiom_simplification @328 - Z3_theory_get_eqc_root @329 - Z3_theory_get_eqc_next @330 - Z3_theory_get_num_parents @331 - Z3_theory_get_parent @332 - Z3_theory_is_value @333 - Z3_theory_is_decl @334 - Z3_theory_get_num_elems @335 - Z3_theory_get_elem @336 - Z3_theory_get_num_apps @337 - Z3_theory_get_app @338 - Z3_mk_fixedpoint @339 - Z3_fixedpoint_inc_ref @340 - Z3_fixedpoint_dec_ref @341 - Z3_fixedpoint_add_rule @342 - Z3_fixedpoint_add_fact @343 - Z3_fixedpoint_assert @344 - Z3_fixedpoint_query @345 - Z3_fixedpoint_query_relations @346 - Z3_fixedpoint_get_answer @347 - Z3_fixedpoint_get_reason_unknown @348 - Z3_fixedpoint_update_rule @349 - Z3_fixedpoint_get_num_levels @350 - Z3_fixedpoint_get_cover_delta @351 - Z3_fixedpoint_add_cover @352 - Z3_fixedpoint_get_statistics @353 - Z3_fixedpoint_register_relation @354 - Z3_fixedpoint_set_predicate_representation @355 - Z3_fixedpoint_simplify_rules @356 - Z3_fixedpoint_set_params @357 - Z3_fixedpoint_get_help @358 - Z3_fixedpoint_get_param_descrs @359 - Z3_fixedpoint_to_string @360 - Z3_fixedpoint_push @361 - Z3_fixedpoint_pop @362 - Z3_fixedpoint_init @363 - Z3_fixedpoint_set_reduce_assign_callback @364 - Z3_fixedpoint_set_reduce_app_callback @365 - Z3_mk_ast_vector @366 - Z3_ast_vector_inc_ref @367 - Z3_ast_vector_dec_ref @368 - Z3_ast_vector_size @369 - Z3_ast_vector_get @370 - Z3_ast_vector_set @371 - Z3_ast_vector_resize @372 - Z3_ast_vector_push @373 - Z3_ast_vector_translate @374 - Z3_ast_vector_to_string @375 - Z3_mk_ast_map @376 - Z3_ast_map_inc_ref @377 - Z3_ast_map_dec_ref @378 - Z3_ast_map_contains @379 - Z3_ast_map_find @380 - Z3_ast_map_insert @381 - Z3_ast_map_erase @382 - Z3_ast_map_reset @383 - Z3_ast_map_size @384 - Z3_ast_map_keys @385 - Z3_ast_map_to_string @386 - Z3_mk_goal @387 - Z3_goal_inc_ref @388 - Z3_goal_dec_ref @389 - Z3_goal_precision @390 - Z3_goal_assert @391 - Z3_goal_inconsistent @392 - Z3_goal_depth @393 - Z3_goal_reset @394 - Z3_goal_size @395 - Z3_goal_formula @396 - Z3_goal_num_exprs @397 - Z3_goal_is_decided_sat @398 - Z3_goal_is_decided_unsat @399 - Z3_goal_translate @400 - Z3_goal_to_string @401 - Z3_mk_tactic @402 - Z3_tactic_inc_ref @403 - Z3_tactic_dec_ref @404 - Z3_mk_probe @405 - Z3_probe_inc_ref @406 - Z3_probe_dec_ref @407 - Z3_tactic_and_then @408 - Z3_tactic_or_else @409 - Z3_tactic_par_or @410 - Z3_tactic_par_and_then @411 - Z3_tactic_try_for @412 - Z3_tactic_when @413 - Z3_tactic_cond @414 - Z3_tactic_repeat @415 - Z3_tactic_skip @416 - Z3_tactic_fail @417 - Z3_tactic_fail_if @418 - Z3_tactic_fail_if_not_decided @419 - Z3_tactic_using_params @420 - Z3_probe_const @421 - Z3_probe_lt @422 - Z3_probe_gt @423 - Z3_probe_le @424 - Z3_probe_ge @425 - Z3_probe_eq @426 - Z3_probe_and @427 - Z3_probe_or @428 - Z3_probe_not @429 - Z3_get_num_tactics @430 - Z3_get_tactic_name @431 - Z3_get_num_probes @432 - Z3_get_probe_name @433 - Z3_tactic_get_help @434 - Z3_tactic_get_param_descrs @435 - Z3_tactic_get_descr @436 - Z3_probe_get_descr @437 - Z3_probe_apply @438 - Z3_tactic_apply @439 - Z3_tactic_apply_ex @440 - Z3_apply_result_inc_ref @441 - Z3_apply_result_dec_ref @442 - Z3_apply_result_to_string @443 - Z3_apply_result_get_num_subgoals @444 - Z3_apply_result_get_subgoal @445 - Z3_apply_result_convert_model @446 - Z3_mk_solver @447 - Z3_mk_simple_solver @448 - Z3_mk_solver_for_logic @449 - Z3_mk_solver_from_tactic @450 - Z3_solver_get_help @451 - Z3_solver_get_param_descrs @452 - Z3_solver_set_params @453 - Z3_solver_inc_ref @454 - Z3_solver_dec_ref @455 - Z3_solver_push @456 - Z3_solver_pop @457 - Z3_solver_reset @458 - Z3_solver_get_num_scopes @459 - Z3_solver_assert @460 - Z3_solver_get_assertions @461 - Z3_solver_check @462 - Z3_solver_check_assumptions @463 - Z3_solver_get_model @464 - Z3_solver_get_proof @465 - Z3_solver_get_unsat_core @466 - Z3_solver_get_reason_unknown @467 - Z3_solver_get_statistics @468 - Z3_solver_to_string @469 - Z3_stats_to_string @470 - Z3_stats_inc_ref @471 - Z3_stats_dec_ref @472 - Z3_stats_size @473 - Z3_stats_get_key @474 - Z3_stats_is_uint @475 - Z3_stats_is_double @476 - Z3_stats_get_uint_value @477 - Z3_stats_get_double_value @478 - Z3_mk_injective_function @479 - Z3_set_logic @480 - Z3_push @481 - Z3_pop @482 - Z3_get_num_scopes @483 - Z3_persist_ast @484 - Z3_assert_cnstr @485 - Z3_check_and_get_model @486 - Z3_check @487 - Z3_check_assumptions @488 - Z3_get_implied_equalities @489 - Z3_del_model @490 - Z3_soft_check_cancel @491 - Z3_get_search_failure @492 - Z3_mk_label @493 - Z3_get_relevant_labels @494 - Z3_get_relevant_literals @495 - Z3_get_guessed_literals @496 - Z3_del_literals @497 - Z3_get_num_literals @498 - Z3_get_label_symbol @499 - Z3_get_literal @500 - Z3_disable_literal @501 - Z3_block_literals @502 - Z3_get_model_num_constants @503 - Z3_get_model_constant @504 - Z3_get_model_num_funcs @505 - Z3_get_model_func_decl @506 - Z3_eval_func_decl @507 - Z3_is_array_value @508 - Z3_get_array_value @509 - Z3_get_model_func_else @510 - Z3_get_model_func_num_entries @511 - Z3_get_model_func_entry_num_args @512 - Z3_get_model_func_entry_arg @513 - Z3_get_model_func_entry_value @514 - Z3_eval @515 - Z3_eval_decl @516 - Z3_context_to_string @517 - Z3_statistics_to_string @518 - Z3_get_context_assignment @519 + Z3_param_descrs_to_string @26 + Z3_mk_int_symbol @27 + Z3_mk_string_symbol @28 + Z3_mk_uninterpreted_sort @29 + Z3_mk_bool_sort @30 + Z3_mk_int_sort @31 + Z3_mk_real_sort @32 + Z3_mk_bv_sort @33 + Z3_mk_finite_domain_sort @34 + Z3_mk_array_sort @35 + Z3_mk_tuple_sort @36 + Z3_mk_enumeration_sort @37 + Z3_mk_list_sort @38 + Z3_mk_constructor @39 + Z3_del_constructor @40 + Z3_mk_datatype @41 + Z3_mk_constructor_list @42 + Z3_del_constructor_list @43 + Z3_mk_datatypes @44 + Z3_query_constructor @45 + Z3_mk_func_decl @46 + Z3_mk_app @47 + Z3_mk_const @48 + Z3_mk_fresh_func_decl @49 + Z3_mk_fresh_const @50 + Z3_mk_true @51 + Z3_mk_false @52 + Z3_mk_eq @53 + Z3_mk_distinct @54 + Z3_mk_not @55 + Z3_mk_ite @56 + Z3_mk_iff @57 + Z3_mk_implies @58 + Z3_mk_xor @59 + Z3_mk_and @60 + Z3_mk_or @61 + Z3_mk_add @62 + Z3_mk_mul @63 + Z3_mk_sub @64 + Z3_mk_unary_minus @65 + Z3_mk_div @66 + Z3_mk_mod @67 + Z3_mk_rem @68 + Z3_mk_power @69 + Z3_mk_lt @70 + Z3_mk_le @71 + Z3_mk_gt @72 + Z3_mk_ge @73 + Z3_mk_int2real @74 + Z3_mk_real2int @75 + Z3_mk_is_int @76 + Z3_mk_bvnot @77 + Z3_mk_bvredand @78 + Z3_mk_bvredor @79 + Z3_mk_bvand @80 + Z3_mk_bvor @81 + Z3_mk_bvxor @82 + Z3_mk_bvnand @83 + Z3_mk_bvnor @84 + Z3_mk_bvxnor @85 + Z3_mk_bvneg @86 + Z3_mk_bvadd @87 + Z3_mk_bvsub @88 + Z3_mk_bvmul @89 + Z3_mk_bvudiv @90 + Z3_mk_bvsdiv @91 + Z3_mk_bvurem @92 + Z3_mk_bvsrem @93 + Z3_mk_bvsmod @94 + Z3_mk_bvult @95 + Z3_mk_bvslt @96 + Z3_mk_bvule @97 + Z3_mk_bvsle @98 + Z3_mk_bvuge @99 + Z3_mk_bvsge @100 + Z3_mk_bvugt @101 + Z3_mk_bvsgt @102 + Z3_mk_concat @103 + Z3_mk_extract @104 + Z3_mk_sign_ext @105 + Z3_mk_zero_ext @106 + Z3_mk_repeat @107 + Z3_mk_bvshl @108 + Z3_mk_bvlshr @109 + Z3_mk_bvashr @110 + Z3_mk_rotate_left @111 + Z3_mk_rotate_right @112 + Z3_mk_ext_rotate_left @113 + Z3_mk_ext_rotate_right @114 + Z3_mk_int2bv @115 + Z3_mk_bv2int @116 + Z3_mk_bvadd_no_overflow @117 + Z3_mk_bvadd_no_underflow @118 + Z3_mk_bvsub_no_overflow @119 + Z3_mk_bvsub_no_underflow @120 + Z3_mk_bvsdiv_no_overflow @121 + Z3_mk_bvneg_no_overflow @122 + Z3_mk_bvmul_no_overflow @123 + Z3_mk_bvmul_no_underflow @124 + Z3_mk_select @125 + Z3_mk_store @126 + Z3_mk_const_array @127 + Z3_mk_map @128 + Z3_mk_array_default @129 + Z3_mk_set_sort @130 + Z3_mk_empty_set @131 + Z3_mk_full_set @132 + Z3_mk_set_add @133 + Z3_mk_set_del @134 + Z3_mk_set_union @135 + Z3_mk_set_intersect @136 + Z3_mk_set_difference @137 + Z3_mk_set_complement @138 + Z3_mk_set_member @139 + Z3_mk_set_subset @140 + Z3_mk_numeral @141 + Z3_mk_real @142 + Z3_mk_int @143 + Z3_mk_unsigned_int @144 + Z3_mk_int64 @145 + Z3_mk_unsigned_int64 @146 + Z3_mk_pattern @147 + Z3_mk_bound @148 + Z3_mk_forall @149 + Z3_mk_exists @150 + Z3_mk_quantifier @151 + Z3_mk_quantifier_ex @152 + Z3_mk_forall_const @153 + Z3_mk_exists_const @154 + Z3_mk_quantifier_const @155 + Z3_mk_quantifier_const_ex @156 + Z3_get_symbol_kind @157 + Z3_get_symbol_int @158 + Z3_get_symbol_string @159 + Z3_get_sort_name @160 + Z3_get_sort_id @161 + Z3_sort_to_ast @162 + Z3_is_eq_sort @163 + Z3_get_sort_kind @164 + Z3_get_bv_sort_size @165 + Z3_get_finite_domain_sort_size @166 + Z3_get_array_sort_domain @167 + Z3_get_array_sort_range @168 + Z3_get_tuple_sort_mk_decl @169 + Z3_get_tuple_sort_num_fields @170 + Z3_get_tuple_sort_field_decl @171 + Z3_get_datatype_sort_num_constructors @172 + Z3_get_datatype_sort_constructor @173 + Z3_get_datatype_sort_recognizer @174 + Z3_get_datatype_sort_constructor_accessor @175 + Z3_get_relation_arity @176 + Z3_get_relation_column @177 + Z3_func_decl_to_ast @178 + Z3_is_eq_func_decl @179 + Z3_get_func_decl_id @180 + Z3_get_decl_name @181 + Z3_get_decl_kind @182 + Z3_get_domain_size @183 + Z3_get_arity @184 + Z3_get_domain @185 + Z3_get_range @186 + Z3_get_decl_num_parameters @187 + Z3_get_decl_parameter_kind @188 + Z3_get_decl_int_parameter @189 + Z3_get_decl_double_parameter @190 + Z3_get_decl_symbol_parameter @191 + Z3_get_decl_sort_parameter @192 + Z3_get_decl_ast_parameter @193 + Z3_get_decl_func_decl_parameter @194 + Z3_get_decl_rational_parameter @195 + Z3_app_to_ast @196 + Z3_get_app_decl @197 + Z3_get_app_num_args @198 + Z3_get_app_arg @199 + Z3_is_eq_ast @200 + Z3_get_ast_id @201 + Z3_get_ast_hash @202 + Z3_get_sort @203 + Z3_is_well_sorted @204 + Z3_get_bool_value @205 + Z3_get_ast_kind @206 + Z3_is_app @207 + Z3_is_numeral_ast @208 + Z3_is_algebraic_number @209 + Z3_to_app @210 + Z3_to_func_decl @211 + Z3_get_numeral_string @212 + Z3_get_numeral_decimal_string @213 + Z3_get_numerator @214 + Z3_get_denominator @215 + Z3_get_numeral_small @216 + Z3_get_numeral_int @217 + Z3_get_numeral_uint @218 + Z3_get_numeral_uint64 @219 + Z3_get_numeral_int64 @220 + Z3_get_numeral_rational_int64 @221 + Z3_get_algebraic_number_lower @222 + Z3_get_algebraic_number_upper @223 + Z3_pattern_to_ast @224 + Z3_get_pattern_num_terms @225 + Z3_get_pattern @226 + Z3_get_index_value @227 + Z3_is_quantifier_forall @228 + Z3_get_quantifier_weight @229 + Z3_get_quantifier_num_patterns @230 + Z3_get_quantifier_pattern_ast @231 + Z3_get_quantifier_num_no_patterns @232 + Z3_get_quantifier_no_pattern_ast @233 + Z3_get_quantifier_num_bound @234 + Z3_get_quantifier_bound_name @235 + Z3_get_quantifier_bound_sort @236 + Z3_get_quantifier_body @237 + Z3_simplify @238 + Z3_simplify_ex @239 + Z3_simplify_get_help @240 + Z3_simplify_get_param_descrs @241 + Z3_update_term @242 + Z3_substitute @243 + Z3_substitute_vars @244 + Z3_translate @245 + Z3_model_inc_ref @246 + Z3_model_dec_ref @247 + Z3_model_eval @248 + Z3_model_get_const_interp @249 + Z3_model_get_func_interp @250 + Z3_model_get_num_consts @251 + Z3_model_get_const_decl @252 + Z3_model_get_num_funcs @253 + Z3_model_get_func_decl @254 + Z3_model_get_num_sorts @255 + Z3_model_get_sort @256 + Z3_model_get_sort_universe @257 + Z3_is_as_array @258 + Z3_get_as_array_func_decl @259 + Z3_func_interp_inc_ref @260 + Z3_func_interp_dec_ref @261 + Z3_func_interp_get_num_entries @262 + Z3_func_interp_get_entry @263 + Z3_func_interp_get_else @264 + Z3_func_interp_get_arity @265 + Z3_func_entry_inc_ref @266 + Z3_func_entry_dec_ref @267 + Z3_func_entry_get_value @268 + Z3_func_entry_get_num_args @269 + Z3_func_entry_get_arg @270 + Z3_open_log @271 + Z3_append_log @272 + Z3_close_log @273 + Z3_toggle_warning_messages @274 + Z3_set_ast_print_mode @275 + Z3_ast_to_string @276 + Z3_pattern_to_string @277 + Z3_sort_to_string @278 + Z3_func_decl_to_string @279 + Z3_model_to_string @280 + Z3_benchmark_to_smtlib_string @281 + Z3_parse_smtlib2_string @282 + Z3_parse_smtlib2_file @283 + Z3_parse_smtlib_string @284 + Z3_parse_smtlib_file @285 + Z3_get_smtlib_num_formulas @286 + Z3_get_smtlib_formula @287 + Z3_get_smtlib_num_assumptions @288 + Z3_get_smtlib_assumption @289 + Z3_get_smtlib_num_decls @290 + Z3_get_smtlib_decl @291 + Z3_get_smtlib_num_sorts @292 + Z3_get_smtlib_sort @293 + Z3_get_smtlib_error @294 + Z3_parse_z3_string @295 + Z3_parse_z3_file @296 + Z3_get_error_code @297 + Z3_set_error_handler @298 + Z3_set_error @299 + Z3_get_error_msg @300 + Z3_get_error_msg_ex @301 + Z3_get_version @302 + Z3_reset_memory @303 + Z3_mk_theory @304 + Z3_theory_get_ext_data @305 + Z3_theory_mk_sort @306 + Z3_theory_mk_value @307 + Z3_theory_mk_constant @308 + Z3_theory_mk_func_decl @309 + Z3_theory_get_context @310 + Z3_set_delete_callback @311 + Z3_set_reduce_app_callback @312 + Z3_set_reduce_eq_callback @313 + Z3_set_reduce_distinct_callback @314 + Z3_set_new_app_callback @315 + Z3_set_new_elem_callback @316 + Z3_set_init_search_callback @317 + Z3_set_push_callback @318 + Z3_set_pop_callback @319 + Z3_set_restart_callback @320 + Z3_set_reset_callback @321 + Z3_set_final_check_callback @322 + Z3_set_new_eq_callback @323 + Z3_set_new_diseq_callback @324 + Z3_set_new_assignment_callback @325 + Z3_set_new_relevant_callback @326 + Z3_theory_assert_axiom @327 + Z3_theory_assume_eq @328 + Z3_theory_enable_axiom_simplification @329 + Z3_theory_get_eqc_root @330 + Z3_theory_get_eqc_next @331 + Z3_theory_get_num_parents @332 + Z3_theory_get_parent @333 + Z3_theory_is_value @334 + Z3_theory_is_decl @335 + Z3_theory_get_num_elems @336 + Z3_theory_get_elem @337 + Z3_theory_get_num_apps @338 + Z3_theory_get_app @339 + Z3_mk_fixedpoint @340 + Z3_fixedpoint_inc_ref @341 + Z3_fixedpoint_dec_ref @342 + Z3_fixedpoint_add_rule @343 + Z3_fixedpoint_add_fact @344 + Z3_fixedpoint_assert @345 + Z3_fixedpoint_query @346 + Z3_fixedpoint_query_relations @347 + Z3_fixedpoint_get_answer @348 + Z3_fixedpoint_get_reason_unknown @349 + Z3_fixedpoint_update_rule @350 + Z3_fixedpoint_get_num_levels @351 + Z3_fixedpoint_get_cover_delta @352 + Z3_fixedpoint_add_cover @353 + Z3_fixedpoint_get_statistics @354 + Z3_fixedpoint_register_relation @355 + Z3_fixedpoint_set_predicate_representation @356 + Z3_fixedpoint_simplify_rules @357 + Z3_fixedpoint_set_params @358 + Z3_fixedpoint_get_help @359 + Z3_fixedpoint_get_param_descrs @360 + Z3_fixedpoint_to_string @361 + Z3_fixedpoint_push @362 + Z3_fixedpoint_pop @363 + Z3_fixedpoint_init @364 + Z3_fixedpoint_set_reduce_assign_callback @365 + Z3_fixedpoint_set_reduce_app_callback @366 + Z3_mk_ast_vector @367 + Z3_ast_vector_inc_ref @368 + Z3_ast_vector_dec_ref @369 + Z3_ast_vector_size @370 + Z3_ast_vector_get @371 + Z3_ast_vector_set @372 + Z3_ast_vector_resize @373 + Z3_ast_vector_push @374 + Z3_ast_vector_translate @375 + Z3_ast_vector_to_string @376 + Z3_mk_ast_map @377 + Z3_ast_map_inc_ref @378 + Z3_ast_map_dec_ref @379 + Z3_ast_map_contains @380 + Z3_ast_map_find @381 + Z3_ast_map_insert @382 + Z3_ast_map_erase @383 + Z3_ast_map_reset @384 + Z3_ast_map_size @385 + Z3_ast_map_keys @386 + Z3_ast_map_to_string @387 + Z3_mk_goal @388 + Z3_goal_inc_ref @389 + Z3_goal_dec_ref @390 + Z3_goal_precision @391 + Z3_goal_assert @392 + Z3_goal_inconsistent @393 + Z3_goal_depth @394 + Z3_goal_reset @395 + Z3_goal_size @396 + Z3_goal_formula @397 + Z3_goal_num_exprs @398 + Z3_goal_is_decided_sat @399 + Z3_goal_is_decided_unsat @400 + Z3_goal_translate @401 + Z3_goal_to_string @402 + Z3_mk_tactic @403 + Z3_tactic_inc_ref @404 + Z3_tactic_dec_ref @405 + Z3_mk_probe @406 + Z3_probe_inc_ref @407 + Z3_probe_dec_ref @408 + Z3_tactic_and_then @409 + Z3_tactic_or_else @410 + Z3_tactic_par_or @411 + Z3_tactic_par_and_then @412 + Z3_tactic_try_for @413 + Z3_tactic_when @414 + Z3_tactic_cond @415 + Z3_tactic_repeat @416 + Z3_tactic_skip @417 + Z3_tactic_fail @418 + Z3_tactic_fail_if @419 + Z3_tactic_fail_if_not_decided @420 + Z3_tactic_using_params @421 + Z3_probe_const @422 + Z3_probe_lt @423 + Z3_probe_gt @424 + Z3_probe_le @425 + Z3_probe_ge @426 + Z3_probe_eq @427 + Z3_probe_and @428 + Z3_probe_or @429 + Z3_probe_not @430 + Z3_get_num_tactics @431 + Z3_get_tactic_name @432 + Z3_get_num_probes @433 + Z3_get_probe_name @434 + Z3_tactic_get_help @435 + Z3_tactic_get_param_descrs @436 + Z3_tactic_get_descr @437 + Z3_probe_get_descr @438 + Z3_probe_apply @439 + Z3_tactic_apply @440 + Z3_tactic_apply_ex @441 + Z3_apply_result_inc_ref @442 + Z3_apply_result_dec_ref @443 + Z3_apply_result_to_string @444 + Z3_apply_result_get_num_subgoals @445 + Z3_apply_result_get_subgoal @446 + Z3_apply_result_convert_model @447 + Z3_mk_solver @448 + Z3_mk_simple_solver @449 + Z3_mk_solver_for_logic @450 + Z3_mk_solver_from_tactic @451 + Z3_solver_get_help @452 + Z3_solver_get_param_descrs @453 + Z3_solver_set_params @454 + Z3_solver_inc_ref @455 + Z3_solver_dec_ref @456 + Z3_solver_push @457 + Z3_solver_pop @458 + Z3_solver_reset @459 + Z3_solver_get_num_scopes @460 + Z3_solver_assert @461 + Z3_solver_get_assertions @462 + Z3_solver_check @463 + Z3_solver_check_assumptions @464 + Z3_solver_get_model @465 + Z3_solver_get_proof @466 + Z3_solver_get_unsat_core @467 + Z3_solver_get_reason_unknown @468 + Z3_solver_get_statistics @469 + Z3_solver_to_string @470 + Z3_stats_to_string @471 + Z3_stats_inc_ref @472 + Z3_stats_dec_ref @473 + Z3_stats_size @474 + Z3_stats_get_key @475 + Z3_stats_is_uint @476 + Z3_stats_is_double @477 + Z3_stats_get_uint_value @478 + Z3_stats_get_double_value @479 + Z3_mk_injective_function @480 + Z3_set_logic @481 + Z3_push @482 + Z3_pop @483 + Z3_get_num_scopes @484 + Z3_persist_ast @485 + Z3_assert_cnstr @486 + Z3_check_and_get_model @487 + Z3_check @488 + Z3_check_assumptions @489 + Z3_get_implied_equalities @490 + Z3_del_model @491 + Z3_soft_check_cancel @492 + Z3_get_search_failure @493 + Z3_mk_label @494 + Z3_get_relevant_labels @495 + Z3_get_relevant_literals @496 + Z3_get_guessed_literals @497 + Z3_del_literals @498 + Z3_get_num_literals @499 + Z3_get_label_symbol @500 + Z3_get_literal @501 + Z3_disable_literal @502 + Z3_block_literals @503 + Z3_get_model_num_constants @504 + Z3_get_model_constant @505 + Z3_get_model_num_funcs @506 + Z3_get_model_func_decl @507 + Z3_eval_func_decl @508 + Z3_is_array_value @509 + Z3_get_array_value @510 + Z3_get_model_func_else @511 + Z3_get_model_func_num_entries @512 + Z3_get_model_func_entry_num_args @513 + Z3_get_model_func_entry_arg @514 + Z3_get_model_func_entry_value @515 + Z3_eval @516 + Z3_eval_decl @517 + Z3_context_to_string @518 + Z3_statistics_to_string @519 + Z3_get_context_assignment @520 diff --git a/dll/z3_dbg.def b/dll/z3_dbg.def index 0c830c94e..e74292bd3 100644 --- a/dll/z3_dbg.def +++ b/dll/z3_dbg.def @@ -25,497 +25,498 @@ EXPORTS Z3_param_descrs_get_kind @23 Z3_param_descrs_size @24 Z3_param_descrs_get_name @25 - Z3_mk_int_symbol @26 - Z3_mk_string_symbol @27 - Z3_mk_uninterpreted_sort @28 - Z3_mk_bool_sort @29 - Z3_mk_int_sort @30 - Z3_mk_real_sort @31 - Z3_mk_bv_sort @32 - Z3_mk_finite_domain_sort @33 - Z3_mk_array_sort @34 - Z3_mk_tuple_sort @35 - Z3_mk_enumeration_sort @36 - Z3_mk_list_sort @37 - Z3_mk_constructor @38 - Z3_del_constructor @39 - Z3_mk_datatype @40 - Z3_mk_constructor_list @41 - Z3_del_constructor_list @42 - Z3_mk_datatypes @43 - Z3_query_constructor @44 - Z3_mk_func_decl @45 - Z3_mk_app @46 - Z3_mk_const @47 - Z3_mk_fresh_func_decl @48 - Z3_mk_fresh_const @49 - Z3_mk_true @50 - Z3_mk_false @51 - Z3_mk_eq @52 - Z3_mk_distinct @53 - Z3_mk_not @54 - Z3_mk_ite @55 - Z3_mk_iff @56 - Z3_mk_implies @57 - Z3_mk_xor @58 - Z3_mk_and @59 - Z3_mk_or @60 - Z3_mk_add @61 - Z3_mk_mul @62 - Z3_mk_sub @63 - Z3_mk_unary_minus @64 - Z3_mk_div @65 - Z3_mk_mod @66 - Z3_mk_rem @67 - Z3_mk_power @68 - Z3_mk_lt @69 - Z3_mk_le @70 - Z3_mk_gt @71 - Z3_mk_ge @72 - Z3_mk_int2real @73 - Z3_mk_real2int @74 - Z3_mk_is_int @75 - Z3_mk_bvnot @76 - Z3_mk_bvredand @77 - Z3_mk_bvredor @78 - Z3_mk_bvand @79 - Z3_mk_bvor @80 - Z3_mk_bvxor @81 - Z3_mk_bvnand @82 - Z3_mk_bvnor @83 - Z3_mk_bvxnor @84 - Z3_mk_bvneg @85 - Z3_mk_bvadd @86 - Z3_mk_bvsub @87 - Z3_mk_bvmul @88 - Z3_mk_bvudiv @89 - Z3_mk_bvsdiv @90 - Z3_mk_bvurem @91 - Z3_mk_bvsrem @92 - Z3_mk_bvsmod @93 - Z3_mk_bvult @94 - Z3_mk_bvslt @95 - Z3_mk_bvule @96 - Z3_mk_bvsle @97 - Z3_mk_bvuge @98 - Z3_mk_bvsge @99 - Z3_mk_bvugt @100 - Z3_mk_bvsgt @101 - Z3_mk_concat @102 - Z3_mk_extract @103 - Z3_mk_sign_ext @104 - Z3_mk_zero_ext @105 - Z3_mk_repeat @106 - Z3_mk_bvshl @107 - Z3_mk_bvlshr @108 - Z3_mk_bvashr @109 - Z3_mk_rotate_left @110 - Z3_mk_rotate_right @111 - Z3_mk_ext_rotate_left @112 - Z3_mk_ext_rotate_right @113 - Z3_mk_int2bv @114 - Z3_mk_bv2int @115 - Z3_mk_bvadd_no_overflow @116 - Z3_mk_bvadd_no_underflow @117 - Z3_mk_bvsub_no_overflow @118 - Z3_mk_bvsub_no_underflow @119 - Z3_mk_bvsdiv_no_overflow @120 - Z3_mk_bvneg_no_overflow @121 - Z3_mk_bvmul_no_overflow @122 - Z3_mk_bvmul_no_underflow @123 - Z3_mk_select @124 - Z3_mk_store @125 - Z3_mk_const_array @126 - Z3_mk_map @127 - Z3_mk_array_default @128 - Z3_mk_set_sort @129 - Z3_mk_empty_set @130 - Z3_mk_full_set @131 - Z3_mk_set_add @132 - Z3_mk_set_del @133 - Z3_mk_set_union @134 - Z3_mk_set_intersect @135 - Z3_mk_set_difference @136 - Z3_mk_set_complement @137 - Z3_mk_set_member @138 - Z3_mk_set_subset @139 - Z3_mk_numeral @140 - Z3_mk_real @141 - Z3_mk_int @142 - Z3_mk_unsigned_int @143 - Z3_mk_int64 @144 - Z3_mk_unsigned_int64 @145 - Z3_mk_pattern @146 - Z3_mk_bound @147 - Z3_mk_forall @148 - Z3_mk_exists @149 - Z3_mk_quantifier @150 - Z3_mk_quantifier_ex @151 - Z3_mk_forall_const @152 - Z3_mk_exists_const @153 - Z3_mk_quantifier_const @154 - Z3_mk_quantifier_const_ex @155 - Z3_get_symbol_kind @156 - Z3_get_symbol_int @157 - Z3_get_symbol_string @158 - Z3_get_sort_name @159 - Z3_get_sort_id @160 - Z3_sort_to_ast @161 - Z3_is_eq_sort @162 - Z3_get_sort_kind @163 - Z3_get_bv_sort_size @164 - Z3_get_finite_domain_sort_size @165 - Z3_get_array_sort_domain @166 - Z3_get_array_sort_range @167 - Z3_get_tuple_sort_mk_decl @168 - Z3_get_tuple_sort_num_fields @169 - Z3_get_tuple_sort_field_decl @170 - Z3_get_datatype_sort_num_constructors @171 - Z3_get_datatype_sort_constructor @172 - Z3_get_datatype_sort_recognizer @173 - Z3_get_datatype_sort_constructor_accessor @174 - Z3_get_relation_arity @175 - Z3_get_relation_column @176 - Z3_func_decl_to_ast @177 - Z3_is_eq_func_decl @178 - Z3_get_func_decl_id @179 - Z3_get_decl_name @180 - Z3_get_decl_kind @181 - Z3_get_domain_size @182 - Z3_get_arity @183 - Z3_get_domain @184 - Z3_get_range @185 - Z3_get_decl_num_parameters @186 - Z3_get_decl_parameter_kind @187 - Z3_get_decl_int_parameter @188 - Z3_get_decl_double_parameter @189 - Z3_get_decl_symbol_parameter @190 - Z3_get_decl_sort_parameter @191 - Z3_get_decl_ast_parameter @192 - Z3_get_decl_func_decl_parameter @193 - Z3_get_decl_rational_parameter @194 - Z3_app_to_ast @195 - Z3_get_app_decl @196 - Z3_get_app_num_args @197 - Z3_get_app_arg @198 - Z3_is_eq_ast @199 - Z3_get_ast_id @200 - Z3_get_ast_hash @201 - Z3_get_sort @202 - Z3_is_well_sorted @203 - Z3_get_bool_value @204 - Z3_get_ast_kind @205 - Z3_is_app @206 - Z3_is_numeral_ast @207 - Z3_is_algebraic_number @208 - Z3_to_app @209 - Z3_to_func_decl @210 - Z3_get_numeral_string @211 - Z3_get_numeral_decimal_string @212 - Z3_get_numerator @213 - Z3_get_denominator @214 - Z3_get_numeral_small @215 - Z3_get_numeral_int @216 - Z3_get_numeral_uint @217 - Z3_get_numeral_uint64 @218 - Z3_get_numeral_int64 @219 - Z3_get_numeral_rational_int64 @220 - Z3_get_algebraic_number_lower @221 - Z3_get_algebraic_number_upper @222 - Z3_pattern_to_ast @223 - Z3_get_pattern_num_terms @224 - Z3_get_pattern @225 - Z3_get_index_value @226 - Z3_is_quantifier_forall @227 - Z3_get_quantifier_weight @228 - Z3_get_quantifier_num_patterns @229 - Z3_get_quantifier_pattern_ast @230 - Z3_get_quantifier_num_no_patterns @231 - Z3_get_quantifier_no_pattern_ast @232 - Z3_get_quantifier_num_bound @233 - Z3_get_quantifier_bound_name @234 - Z3_get_quantifier_bound_sort @235 - Z3_get_quantifier_body @236 - Z3_simplify @237 - Z3_simplify_ex @238 - Z3_simplify_get_help @239 - Z3_simplify_get_param_descrs @240 - Z3_update_term @241 - Z3_substitute @242 - Z3_substitute_vars @243 - Z3_translate @244 - Z3_model_inc_ref @245 - Z3_model_dec_ref @246 - Z3_model_eval @247 - Z3_model_get_const_interp @248 - Z3_model_get_func_interp @249 - Z3_model_get_num_consts @250 - Z3_model_get_const_decl @251 - Z3_model_get_num_funcs @252 - Z3_model_get_func_decl @253 - Z3_model_get_num_sorts @254 - Z3_model_get_sort @255 - Z3_model_get_sort_universe @256 - Z3_is_as_array @257 - Z3_get_as_array_func_decl @258 - Z3_func_interp_inc_ref @259 - Z3_func_interp_dec_ref @260 - Z3_func_interp_get_num_entries @261 - Z3_func_interp_get_entry @262 - Z3_func_interp_get_else @263 - Z3_func_interp_get_arity @264 - Z3_func_entry_inc_ref @265 - Z3_func_entry_dec_ref @266 - Z3_func_entry_get_value @267 - Z3_func_entry_get_num_args @268 - Z3_func_entry_get_arg @269 - Z3_open_log @270 - Z3_append_log @271 - Z3_close_log @272 - Z3_toggle_warning_messages @273 - Z3_set_ast_print_mode @274 - Z3_ast_to_string @275 - Z3_pattern_to_string @276 - Z3_sort_to_string @277 - Z3_func_decl_to_string @278 - Z3_model_to_string @279 - Z3_benchmark_to_smtlib_string @280 - Z3_parse_smtlib2_string @281 - Z3_parse_smtlib2_file @282 - Z3_parse_smtlib_string @283 - Z3_parse_smtlib_file @284 - Z3_get_smtlib_num_formulas @285 - Z3_get_smtlib_formula @286 - Z3_get_smtlib_num_assumptions @287 - Z3_get_smtlib_assumption @288 - Z3_get_smtlib_num_decls @289 - Z3_get_smtlib_decl @290 - Z3_get_smtlib_num_sorts @291 - Z3_get_smtlib_sort @292 - Z3_get_smtlib_error @293 - Z3_parse_z3_string @294 - Z3_parse_z3_file @295 - Z3_get_error_code @296 - Z3_set_error_handler @297 - Z3_set_error @298 - Z3_get_error_msg @299 - Z3_get_error_msg_ex @300 - Z3_get_version @301 - Z3_reset_memory @302 - Z3_mk_theory @303 - Z3_theory_get_ext_data @304 - Z3_theory_mk_sort @305 - Z3_theory_mk_value @306 - Z3_theory_mk_constant @307 - Z3_theory_mk_func_decl @308 - Z3_theory_get_context @309 - Z3_set_delete_callback @310 - Z3_set_reduce_app_callback @311 - Z3_set_reduce_eq_callback @312 - Z3_set_reduce_distinct_callback @313 - Z3_set_new_app_callback @314 - Z3_set_new_elem_callback @315 - Z3_set_init_search_callback @316 - Z3_set_push_callback @317 - Z3_set_pop_callback @318 - Z3_set_restart_callback @319 - Z3_set_reset_callback @320 - Z3_set_final_check_callback @321 - Z3_set_new_eq_callback @322 - Z3_set_new_diseq_callback @323 - Z3_set_new_assignment_callback @324 - Z3_set_new_relevant_callback @325 - Z3_theory_assert_axiom @326 - Z3_theory_assume_eq @327 - Z3_theory_enable_axiom_simplification @328 - Z3_theory_get_eqc_root @329 - Z3_theory_get_eqc_next @330 - Z3_theory_get_num_parents @331 - Z3_theory_get_parent @332 - Z3_theory_is_value @333 - Z3_theory_is_decl @334 - Z3_theory_get_num_elems @335 - Z3_theory_get_elem @336 - Z3_theory_get_num_apps @337 - Z3_theory_get_app @338 - Z3_mk_fixedpoint @339 - Z3_fixedpoint_inc_ref @340 - Z3_fixedpoint_dec_ref @341 - Z3_fixedpoint_add_rule @342 - Z3_fixedpoint_add_fact @343 - Z3_fixedpoint_assert @344 - Z3_fixedpoint_query @345 - Z3_fixedpoint_query_relations @346 - Z3_fixedpoint_get_answer @347 - Z3_fixedpoint_get_reason_unknown @348 - Z3_fixedpoint_update_rule @349 - Z3_fixedpoint_get_num_levels @350 - Z3_fixedpoint_get_cover_delta @351 - Z3_fixedpoint_add_cover @352 - Z3_fixedpoint_get_statistics @353 - Z3_fixedpoint_register_relation @354 - Z3_fixedpoint_set_predicate_representation @355 - Z3_fixedpoint_simplify_rules @356 - Z3_fixedpoint_set_params @357 - Z3_fixedpoint_get_help @358 - Z3_fixedpoint_get_param_descrs @359 - Z3_fixedpoint_to_string @360 - Z3_fixedpoint_push @361 - Z3_fixedpoint_pop @362 - Z3_fixedpoint_init @363 - Z3_fixedpoint_set_reduce_assign_callback @364 - Z3_fixedpoint_set_reduce_app_callback @365 - Z3_mk_ast_vector @366 - Z3_ast_vector_inc_ref @367 - Z3_ast_vector_dec_ref @368 - Z3_ast_vector_size @369 - Z3_ast_vector_get @370 - Z3_ast_vector_set @371 - Z3_ast_vector_resize @372 - Z3_ast_vector_push @373 - Z3_ast_vector_translate @374 - Z3_ast_vector_to_string @375 - Z3_mk_ast_map @376 - Z3_ast_map_inc_ref @377 - Z3_ast_map_dec_ref @378 - Z3_ast_map_contains @379 - Z3_ast_map_find @380 - Z3_ast_map_insert @381 - Z3_ast_map_erase @382 - Z3_ast_map_reset @383 - Z3_ast_map_size @384 - Z3_ast_map_keys @385 - Z3_ast_map_to_string @386 - Z3_mk_goal @387 - Z3_goal_inc_ref @388 - Z3_goal_dec_ref @389 - Z3_goal_precision @390 - Z3_goal_assert @391 - Z3_goal_inconsistent @392 - Z3_goal_depth @393 - Z3_goal_reset @394 - Z3_goal_size @395 - Z3_goal_formula @396 - Z3_goal_num_exprs @397 - Z3_goal_is_decided_sat @398 - Z3_goal_is_decided_unsat @399 - Z3_goal_translate @400 - Z3_goal_to_string @401 - Z3_mk_tactic @402 - Z3_tactic_inc_ref @403 - Z3_tactic_dec_ref @404 - Z3_mk_probe @405 - Z3_probe_inc_ref @406 - Z3_probe_dec_ref @407 - Z3_tactic_and_then @408 - Z3_tactic_or_else @409 - Z3_tactic_par_or @410 - Z3_tactic_par_and_then @411 - Z3_tactic_try_for @412 - Z3_tactic_when @413 - Z3_tactic_cond @414 - Z3_tactic_repeat @415 - Z3_tactic_skip @416 - Z3_tactic_fail @417 - Z3_tactic_fail_if @418 - Z3_tactic_fail_if_not_decided @419 - Z3_tactic_using_params @420 - Z3_probe_const @421 - Z3_probe_lt @422 - Z3_probe_gt @423 - Z3_probe_le @424 - Z3_probe_ge @425 - Z3_probe_eq @426 - Z3_probe_and @427 - Z3_probe_or @428 - Z3_probe_not @429 - Z3_get_num_tactics @430 - Z3_get_tactic_name @431 - Z3_get_num_probes @432 - Z3_get_probe_name @433 - Z3_tactic_get_help @434 - Z3_tactic_get_param_descrs @435 - Z3_tactic_get_descr @436 - Z3_probe_get_descr @437 - Z3_probe_apply @438 - Z3_tactic_apply @439 - Z3_tactic_apply_ex @440 - Z3_apply_result_inc_ref @441 - Z3_apply_result_dec_ref @442 - Z3_apply_result_to_string @443 - Z3_apply_result_get_num_subgoals @444 - Z3_apply_result_get_subgoal @445 - Z3_apply_result_convert_model @446 - Z3_mk_solver @447 - Z3_mk_simple_solver @448 - Z3_mk_solver_for_logic @449 - Z3_mk_solver_from_tactic @450 - Z3_solver_get_help @451 - Z3_solver_get_param_descrs @452 - Z3_solver_set_params @453 - Z3_solver_inc_ref @454 - Z3_solver_dec_ref @455 - Z3_solver_push @456 - Z3_solver_pop @457 - Z3_solver_reset @458 - Z3_solver_get_num_scopes @459 - Z3_solver_assert @460 - Z3_solver_get_assertions @461 - Z3_solver_check @462 - Z3_solver_check_assumptions @463 - Z3_solver_get_model @464 - Z3_solver_get_proof @465 - Z3_solver_get_unsat_core @466 - Z3_solver_get_reason_unknown @467 - Z3_solver_get_statistics @468 - Z3_solver_to_string @469 - Z3_stats_to_string @470 - Z3_stats_inc_ref @471 - Z3_stats_dec_ref @472 - Z3_stats_size @473 - Z3_stats_get_key @474 - Z3_stats_is_uint @475 - Z3_stats_is_double @476 - Z3_stats_get_uint_value @477 - Z3_stats_get_double_value @478 - Z3_mk_injective_function @479 - Z3_set_logic @480 - Z3_push @481 - Z3_pop @482 - Z3_get_num_scopes @483 - Z3_persist_ast @484 - Z3_assert_cnstr @485 - Z3_check_and_get_model @486 - Z3_check @487 - Z3_check_assumptions @488 - Z3_get_implied_equalities @489 - Z3_del_model @490 - Z3_soft_check_cancel @491 - Z3_get_search_failure @492 - Z3_mk_label @493 - Z3_get_relevant_labels @494 - Z3_get_relevant_literals @495 - Z3_get_guessed_literals @496 - Z3_del_literals @497 - Z3_get_num_literals @498 - Z3_get_label_symbol @499 - Z3_get_literal @500 - Z3_disable_literal @501 - Z3_block_literals @502 - Z3_get_model_num_constants @503 - Z3_get_model_constant @504 - Z3_get_model_num_funcs @505 - Z3_get_model_func_decl @506 - Z3_eval_func_decl @507 - Z3_is_array_value @508 - Z3_get_array_value @509 - Z3_get_model_func_else @510 - Z3_get_model_func_num_entries @511 - Z3_get_model_func_entry_num_args @512 - Z3_get_model_func_entry_arg @513 - Z3_get_model_func_entry_value @514 - Z3_eval @515 - Z3_eval_decl @516 - Z3_context_to_string @517 - Z3_statistics_to_string @518 - Z3_get_context_assignment @519 + Z3_param_descrs_to_string @26 + Z3_mk_int_symbol @27 + Z3_mk_string_symbol @28 + Z3_mk_uninterpreted_sort @29 + Z3_mk_bool_sort @30 + Z3_mk_int_sort @31 + Z3_mk_real_sort @32 + Z3_mk_bv_sort @33 + Z3_mk_finite_domain_sort @34 + Z3_mk_array_sort @35 + Z3_mk_tuple_sort @36 + Z3_mk_enumeration_sort @37 + Z3_mk_list_sort @38 + Z3_mk_constructor @39 + Z3_del_constructor @40 + Z3_mk_datatype @41 + Z3_mk_constructor_list @42 + Z3_del_constructor_list @43 + Z3_mk_datatypes @44 + Z3_query_constructor @45 + Z3_mk_func_decl @46 + Z3_mk_app @47 + Z3_mk_const @48 + Z3_mk_fresh_func_decl @49 + Z3_mk_fresh_const @50 + Z3_mk_true @51 + Z3_mk_false @52 + Z3_mk_eq @53 + Z3_mk_distinct @54 + Z3_mk_not @55 + Z3_mk_ite @56 + Z3_mk_iff @57 + Z3_mk_implies @58 + Z3_mk_xor @59 + Z3_mk_and @60 + Z3_mk_or @61 + Z3_mk_add @62 + Z3_mk_mul @63 + Z3_mk_sub @64 + Z3_mk_unary_minus @65 + Z3_mk_div @66 + Z3_mk_mod @67 + Z3_mk_rem @68 + Z3_mk_power @69 + Z3_mk_lt @70 + Z3_mk_le @71 + Z3_mk_gt @72 + Z3_mk_ge @73 + Z3_mk_int2real @74 + Z3_mk_real2int @75 + Z3_mk_is_int @76 + Z3_mk_bvnot @77 + Z3_mk_bvredand @78 + Z3_mk_bvredor @79 + Z3_mk_bvand @80 + Z3_mk_bvor @81 + Z3_mk_bvxor @82 + Z3_mk_bvnand @83 + Z3_mk_bvnor @84 + Z3_mk_bvxnor @85 + Z3_mk_bvneg @86 + Z3_mk_bvadd @87 + Z3_mk_bvsub @88 + Z3_mk_bvmul @89 + Z3_mk_bvudiv @90 + Z3_mk_bvsdiv @91 + Z3_mk_bvurem @92 + Z3_mk_bvsrem @93 + Z3_mk_bvsmod @94 + Z3_mk_bvult @95 + Z3_mk_bvslt @96 + Z3_mk_bvule @97 + Z3_mk_bvsle @98 + Z3_mk_bvuge @99 + Z3_mk_bvsge @100 + Z3_mk_bvugt @101 + Z3_mk_bvsgt @102 + Z3_mk_concat @103 + Z3_mk_extract @104 + Z3_mk_sign_ext @105 + Z3_mk_zero_ext @106 + Z3_mk_repeat @107 + Z3_mk_bvshl @108 + Z3_mk_bvlshr @109 + Z3_mk_bvashr @110 + Z3_mk_rotate_left @111 + Z3_mk_rotate_right @112 + Z3_mk_ext_rotate_left @113 + Z3_mk_ext_rotate_right @114 + Z3_mk_int2bv @115 + Z3_mk_bv2int @116 + Z3_mk_bvadd_no_overflow @117 + Z3_mk_bvadd_no_underflow @118 + Z3_mk_bvsub_no_overflow @119 + Z3_mk_bvsub_no_underflow @120 + Z3_mk_bvsdiv_no_overflow @121 + Z3_mk_bvneg_no_overflow @122 + Z3_mk_bvmul_no_overflow @123 + Z3_mk_bvmul_no_underflow @124 + Z3_mk_select @125 + Z3_mk_store @126 + Z3_mk_const_array @127 + Z3_mk_map @128 + Z3_mk_array_default @129 + Z3_mk_set_sort @130 + Z3_mk_empty_set @131 + Z3_mk_full_set @132 + Z3_mk_set_add @133 + Z3_mk_set_del @134 + Z3_mk_set_union @135 + Z3_mk_set_intersect @136 + Z3_mk_set_difference @137 + Z3_mk_set_complement @138 + Z3_mk_set_member @139 + Z3_mk_set_subset @140 + Z3_mk_numeral @141 + Z3_mk_real @142 + Z3_mk_int @143 + Z3_mk_unsigned_int @144 + Z3_mk_int64 @145 + Z3_mk_unsigned_int64 @146 + Z3_mk_pattern @147 + Z3_mk_bound @148 + Z3_mk_forall @149 + Z3_mk_exists @150 + Z3_mk_quantifier @151 + Z3_mk_quantifier_ex @152 + Z3_mk_forall_const @153 + Z3_mk_exists_const @154 + Z3_mk_quantifier_const @155 + Z3_mk_quantifier_const_ex @156 + Z3_get_symbol_kind @157 + Z3_get_symbol_int @158 + Z3_get_symbol_string @159 + Z3_get_sort_name @160 + Z3_get_sort_id @161 + Z3_sort_to_ast @162 + Z3_is_eq_sort @163 + Z3_get_sort_kind @164 + Z3_get_bv_sort_size @165 + Z3_get_finite_domain_sort_size @166 + Z3_get_array_sort_domain @167 + Z3_get_array_sort_range @168 + Z3_get_tuple_sort_mk_decl @169 + Z3_get_tuple_sort_num_fields @170 + Z3_get_tuple_sort_field_decl @171 + Z3_get_datatype_sort_num_constructors @172 + Z3_get_datatype_sort_constructor @173 + Z3_get_datatype_sort_recognizer @174 + Z3_get_datatype_sort_constructor_accessor @175 + Z3_get_relation_arity @176 + Z3_get_relation_column @177 + Z3_func_decl_to_ast @178 + Z3_is_eq_func_decl @179 + Z3_get_func_decl_id @180 + Z3_get_decl_name @181 + Z3_get_decl_kind @182 + Z3_get_domain_size @183 + Z3_get_arity @184 + Z3_get_domain @185 + Z3_get_range @186 + Z3_get_decl_num_parameters @187 + Z3_get_decl_parameter_kind @188 + Z3_get_decl_int_parameter @189 + Z3_get_decl_double_parameter @190 + Z3_get_decl_symbol_parameter @191 + Z3_get_decl_sort_parameter @192 + Z3_get_decl_ast_parameter @193 + Z3_get_decl_func_decl_parameter @194 + Z3_get_decl_rational_parameter @195 + Z3_app_to_ast @196 + Z3_get_app_decl @197 + Z3_get_app_num_args @198 + Z3_get_app_arg @199 + Z3_is_eq_ast @200 + Z3_get_ast_id @201 + Z3_get_ast_hash @202 + Z3_get_sort @203 + Z3_is_well_sorted @204 + Z3_get_bool_value @205 + Z3_get_ast_kind @206 + Z3_is_app @207 + Z3_is_numeral_ast @208 + Z3_is_algebraic_number @209 + Z3_to_app @210 + Z3_to_func_decl @211 + Z3_get_numeral_string @212 + Z3_get_numeral_decimal_string @213 + Z3_get_numerator @214 + Z3_get_denominator @215 + Z3_get_numeral_small @216 + Z3_get_numeral_int @217 + Z3_get_numeral_uint @218 + Z3_get_numeral_uint64 @219 + Z3_get_numeral_int64 @220 + Z3_get_numeral_rational_int64 @221 + Z3_get_algebraic_number_lower @222 + Z3_get_algebraic_number_upper @223 + Z3_pattern_to_ast @224 + Z3_get_pattern_num_terms @225 + Z3_get_pattern @226 + Z3_get_index_value @227 + Z3_is_quantifier_forall @228 + Z3_get_quantifier_weight @229 + Z3_get_quantifier_num_patterns @230 + Z3_get_quantifier_pattern_ast @231 + Z3_get_quantifier_num_no_patterns @232 + Z3_get_quantifier_no_pattern_ast @233 + Z3_get_quantifier_num_bound @234 + Z3_get_quantifier_bound_name @235 + Z3_get_quantifier_bound_sort @236 + Z3_get_quantifier_body @237 + Z3_simplify @238 + Z3_simplify_ex @239 + Z3_simplify_get_help @240 + Z3_simplify_get_param_descrs @241 + Z3_update_term @242 + Z3_substitute @243 + Z3_substitute_vars @244 + Z3_translate @245 + Z3_model_inc_ref @246 + Z3_model_dec_ref @247 + Z3_model_eval @248 + Z3_model_get_const_interp @249 + Z3_model_get_func_interp @250 + Z3_model_get_num_consts @251 + Z3_model_get_const_decl @252 + Z3_model_get_num_funcs @253 + Z3_model_get_func_decl @254 + Z3_model_get_num_sorts @255 + Z3_model_get_sort @256 + Z3_model_get_sort_universe @257 + Z3_is_as_array @258 + Z3_get_as_array_func_decl @259 + Z3_func_interp_inc_ref @260 + Z3_func_interp_dec_ref @261 + Z3_func_interp_get_num_entries @262 + Z3_func_interp_get_entry @263 + Z3_func_interp_get_else @264 + Z3_func_interp_get_arity @265 + Z3_func_entry_inc_ref @266 + Z3_func_entry_dec_ref @267 + Z3_func_entry_get_value @268 + Z3_func_entry_get_num_args @269 + Z3_func_entry_get_arg @270 + Z3_open_log @271 + Z3_append_log @272 + Z3_close_log @273 + Z3_toggle_warning_messages @274 + Z3_set_ast_print_mode @275 + Z3_ast_to_string @276 + Z3_pattern_to_string @277 + Z3_sort_to_string @278 + Z3_func_decl_to_string @279 + Z3_model_to_string @280 + Z3_benchmark_to_smtlib_string @281 + Z3_parse_smtlib2_string @282 + Z3_parse_smtlib2_file @283 + Z3_parse_smtlib_string @284 + Z3_parse_smtlib_file @285 + Z3_get_smtlib_num_formulas @286 + Z3_get_smtlib_formula @287 + Z3_get_smtlib_num_assumptions @288 + Z3_get_smtlib_assumption @289 + Z3_get_smtlib_num_decls @290 + Z3_get_smtlib_decl @291 + Z3_get_smtlib_num_sorts @292 + Z3_get_smtlib_sort @293 + Z3_get_smtlib_error @294 + Z3_parse_z3_string @295 + Z3_parse_z3_file @296 + Z3_get_error_code @297 + Z3_set_error_handler @298 + Z3_set_error @299 + Z3_get_error_msg @300 + Z3_get_error_msg_ex @301 + Z3_get_version @302 + Z3_reset_memory @303 + Z3_mk_theory @304 + Z3_theory_get_ext_data @305 + Z3_theory_mk_sort @306 + Z3_theory_mk_value @307 + Z3_theory_mk_constant @308 + Z3_theory_mk_func_decl @309 + Z3_theory_get_context @310 + Z3_set_delete_callback @311 + Z3_set_reduce_app_callback @312 + Z3_set_reduce_eq_callback @313 + Z3_set_reduce_distinct_callback @314 + Z3_set_new_app_callback @315 + Z3_set_new_elem_callback @316 + Z3_set_init_search_callback @317 + Z3_set_push_callback @318 + Z3_set_pop_callback @319 + Z3_set_restart_callback @320 + Z3_set_reset_callback @321 + Z3_set_final_check_callback @322 + Z3_set_new_eq_callback @323 + Z3_set_new_diseq_callback @324 + Z3_set_new_assignment_callback @325 + Z3_set_new_relevant_callback @326 + Z3_theory_assert_axiom @327 + Z3_theory_assume_eq @328 + Z3_theory_enable_axiom_simplification @329 + Z3_theory_get_eqc_root @330 + Z3_theory_get_eqc_next @331 + Z3_theory_get_num_parents @332 + Z3_theory_get_parent @333 + Z3_theory_is_value @334 + Z3_theory_is_decl @335 + Z3_theory_get_num_elems @336 + Z3_theory_get_elem @337 + Z3_theory_get_num_apps @338 + Z3_theory_get_app @339 + Z3_mk_fixedpoint @340 + Z3_fixedpoint_inc_ref @341 + Z3_fixedpoint_dec_ref @342 + Z3_fixedpoint_add_rule @343 + Z3_fixedpoint_add_fact @344 + Z3_fixedpoint_assert @345 + Z3_fixedpoint_query @346 + Z3_fixedpoint_query_relations @347 + Z3_fixedpoint_get_answer @348 + Z3_fixedpoint_get_reason_unknown @349 + Z3_fixedpoint_update_rule @350 + Z3_fixedpoint_get_num_levels @351 + Z3_fixedpoint_get_cover_delta @352 + Z3_fixedpoint_add_cover @353 + Z3_fixedpoint_get_statistics @354 + Z3_fixedpoint_register_relation @355 + Z3_fixedpoint_set_predicate_representation @356 + Z3_fixedpoint_simplify_rules @357 + Z3_fixedpoint_set_params @358 + Z3_fixedpoint_get_help @359 + Z3_fixedpoint_get_param_descrs @360 + Z3_fixedpoint_to_string @361 + Z3_fixedpoint_push @362 + Z3_fixedpoint_pop @363 + Z3_fixedpoint_init @364 + Z3_fixedpoint_set_reduce_assign_callback @365 + Z3_fixedpoint_set_reduce_app_callback @366 + Z3_mk_ast_vector @367 + Z3_ast_vector_inc_ref @368 + Z3_ast_vector_dec_ref @369 + Z3_ast_vector_size @370 + Z3_ast_vector_get @371 + Z3_ast_vector_set @372 + Z3_ast_vector_resize @373 + Z3_ast_vector_push @374 + Z3_ast_vector_translate @375 + Z3_ast_vector_to_string @376 + Z3_mk_ast_map @377 + Z3_ast_map_inc_ref @378 + Z3_ast_map_dec_ref @379 + Z3_ast_map_contains @380 + Z3_ast_map_find @381 + Z3_ast_map_insert @382 + Z3_ast_map_erase @383 + Z3_ast_map_reset @384 + Z3_ast_map_size @385 + Z3_ast_map_keys @386 + Z3_ast_map_to_string @387 + Z3_mk_goal @388 + Z3_goal_inc_ref @389 + Z3_goal_dec_ref @390 + Z3_goal_precision @391 + Z3_goal_assert @392 + Z3_goal_inconsistent @393 + Z3_goal_depth @394 + Z3_goal_reset @395 + Z3_goal_size @396 + Z3_goal_formula @397 + Z3_goal_num_exprs @398 + Z3_goal_is_decided_sat @399 + Z3_goal_is_decided_unsat @400 + Z3_goal_translate @401 + Z3_goal_to_string @402 + Z3_mk_tactic @403 + Z3_tactic_inc_ref @404 + Z3_tactic_dec_ref @405 + Z3_mk_probe @406 + Z3_probe_inc_ref @407 + Z3_probe_dec_ref @408 + Z3_tactic_and_then @409 + Z3_tactic_or_else @410 + Z3_tactic_par_or @411 + Z3_tactic_par_and_then @412 + Z3_tactic_try_for @413 + Z3_tactic_when @414 + Z3_tactic_cond @415 + Z3_tactic_repeat @416 + Z3_tactic_skip @417 + Z3_tactic_fail @418 + Z3_tactic_fail_if @419 + Z3_tactic_fail_if_not_decided @420 + Z3_tactic_using_params @421 + Z3_probe_const @422 + Z3_probe_lt @423 + Z3_probe_gt @424 + Z3_probe_le @425 + Z3_probe_ge @426 + Z3_probe_eq @427 + Z3_probe_and @428 + Z3_probe_or @429 + Z3_probe_not @430 + Z3_get_num_tactics @431 + Z3_get_tactic_name @432 + Z3_get_num_probes @433 + Z3_get_probe_name @434 + Z3_tactic_get_help @435 + Z3_tactic_get_param_descrs @436 + Z3_tactic_get_descr @437 + Z3_probe_get_descr @438 + Z3_probe_apply @439 + Z3_tactic_apply @440 + Z3_tactic_apply_ex @441 + Z3_apply_result_inc_ref @442 + Z3_apply_result_dec_ref @443 + Z3_apply_result_to_string @444 + Z3_apply_result_get_num_subgoals @445 + Z3_apply_result_get_subgoal @446 + Z3_apply_result_convert_model @447 + Z3_mk_solver @448 + Z3_mk_simple_solver @449 + Z3_mk_solver_for_logic @450 + Z3_mk_solver_from_tactic @451 + Z3_solver_get_help @452 + Z3_solver_get_param_descrs @453 + Z3_solver_set_params @454 + Z3_solver_inc_ref @455 + Z3_solver_dec_ref @456 + Z3_solver_push @457 + Z3_solver_pop @458 + Z3_solver_reset @459 + Z3_solver_get_num_scopes @460 + Z3_solver_assert @461 + Z3_solver_get_assertions @462 + Z3_solver_check @463 + Z3_solver_check_assumptions @464 + Z3_solver_get_model @465 + Z3_solver_get_proof @466 + Z3_solver_get_unsat_core @467 + Z3_solver_get_reason_unknown @468 + Z3_solver_get_statistics @469 + Z3_solver_to_string @470 + Z3_stats_to_string @471 + Z3_stats_inc_ref @472 + Z3_stats_dec_ref @473 + Z3_stats_size @474 + Z3_stats_get_key @475 + Z3_stats_is_uint @476 + Z3_stats_is_double @477 + Z3_stats_get_uint_value @478 + Z3_stats_get_double_value @479 + Z3_mk_injective_function @480 + Z3_set_logic @481 + Z3_push @482 + Z3_pop @483 + Z3_get_num_scopes @484 + Z3_persist_ast @485 + Z3_assert_cnstr @486 + Z3_check_and_get_model @487 + Z3_check @488 + Z3_check_assumptions @489 + Z3_get_implied_equalities @490 + Z3_del_model @491 + Z3_soft_check_cancel @492 + Z3_get_search_failure @493 + Z3_mk_label @494 + Z3_get_relevant_labels @495 + Z3_get_relevant_literals @496 + Z3_get_guessed_literals @497 + Z3_del_literals @498 + Z3_get_num_literals @499 + Z3_get_label_symbol @500 + Z3_get_literal @501 + Z3_disable_literal @502 + Z3_block_literals @503 + Z3_get_model_num_constants @504 + Z3_get_model_constant @505 + Z3_get_model_num_funcs @506 + Z3_get_model_func_decl @507 + Z3_eval_func_decl @508 + Z3_is_array_value @509 + Z3_get_array_value @510 + Z3_get_model_func_else @511 + Z3_get_model_func_num_entries @512 + Z3_get_model_func_entry_num_args @513 + Z3_get_model_func_entry_arg @514 + Z3_get_model_func_entry_value @515 + Z3_eval @516 + Z3_eval_decl @517 + Z3_context_to_string @518 + Z3_statistics_to_string @519 + Z3_get_context_assignment @520 diff --git a/lib/api.py b/lib/api.py index 71449f43b..746d52cef 100644 --- a/lib/api.py +++ b/lib/api.py @@ -1100,6 +1100,7 @@ API('Z3_param_descrs_dec_ref', VOID, (_in(CONTEXT), _in(PARAM_DESCRS))) API('Z3_param_descrs_get_kind', UINT, (_in(CONTEXT), _in(PARAM_DESCRS), _in(SYMBOL))) API('Z3_param_descrs_size', UINT, (_in(CONTEXT), _in(PARAM_DESCRS))) API('Z3_param_descrs_get_name', SYMBOL, (_in(CONTEXT), _in(PARAM_DESCRS), _in(UINT))) +API('Z3_param_descrs_to_string', STRING, (_in(CONTEXT), _in(PARAM_DESCRS))) # New APIs API('Z3_interrupt', VOID, (_in(CONTEXT),)) API('Z3_get_error_msg_ex', STRING, (_in(CONTEXT), _in(ERROR_CODE))) diff --git a/lib/api_commands.cpp b/lib/api_commands.cpp index badb84ecf..342b25155 100644 --- a/lib/api_commands.cpp +++ b/lib/api_commands.cpp @@ -2328,6 +2328,11 @@ void exec_Z3_param_descrs_get_name(z3_replayer & in) { reinterpret_cast(in.get_obj(1)), in.get_uint(2)); } +void exec_Z3_param_descrs_to_string(z3_replayer & in) { + Z3_param_descrs_to_string( + reinterpret_cast(in.get_obj(0)), + reinterpret_cast(in.get_obj(1))); +} void exec_Z3_interrupt(z3_replayer & in) { Z3_interrupt( reinterpret_cast(in.get_obj(0))); @@ -3359,120 +3364,121 @@ void register_z3_replayer_cmds(z3_replayer & in) { in.register_cmd(357, exec_Z3_param_descrs_get_kind); in.register_cmd(358, exec_Z3_param_descrs_size); in.register_cmd(359, exec_Z3_param_descrs_get_name); - in.register_cmd(360, exec_Z3_interrupt); - in.register_cmd(361, exec_Z3_get_error_msg_ex); - in.register_cmd(362, exec_Z3_translate); - in.register_cmd(363, exec_Z3_mk_goal); - in.register_cmd(364, exec_Z3_goal_inc_ref); - in.register_cmd(365, exec_Z3_goal_dec_ref); - in.register_cmd(366, exec_Z3_goal_precision); - in.register_cmd(367, exec_Z3_goal_assert); - in.register_cmd(368, exec_Z3_goal_inconsistent); - in.register_cmd(369, exec_Z3_goal_depth); - in.register_cmd(370, exec_Z3_goal_reset); - in.register_cmd(371, exec_Z3_goal_size); - in.register_cmd(372, exec_Z3_goal_formula); - in.register_cmd(373, exec_Z3_goal_num_exprs); - in.register_cmd(374, exec_Z3_goal_is_decided_sat); - in.register_cmd(375, exec_Z3_goal_is_decided_unsat); - in.register_cmd(376, exec_Z3_goal_translate); - in.register_cmd(377, exec_Z3_goal_to_string); - in.register_cmd(378, exec_Z3_mk_tactic); - in.register_cmd(379, exec_Z3_mk_probe); - in.register_cmd(380, exec_Z3_tactic_inc_ref); - in.register_cmd(381, exec_Z3_tactic_dec_ref); - in.register_cmd(382, exec_Z3_probe_inc_ref); - in.register_cmd(383, exec_Z3_probe_dec_ref); - in.register_cmd(384, exec_Z3_tactic_and_then); - in.register_cmd(385, exec_Z3_tactic_or_else); - in.register_cmd(386, exec_Z3_tactic_par_or); - in.register_cmd(387, exec_Z3_tactic_par_and_then); - in.register_cmd(388, exec_Z3_tactic_try_for); - in.register_cmd(389, exec_Z3_tactic_when); - in.register_cmd(390, exec_Z3_tactic_cond); - in.register_cmd(391, exec_Z3_tactic_repeat); - in.register_cmd(392, exec_Z3_tactic_skip); - in.register_cmd(393, exec_Z3_tactic_fail); - in.register_cmd(394, exec_Z3_tactic_fail_if); - in.register_cmd(395, exec_Z3_tactic_fail_if_not_decided); - in.register_cmd(396, exec_Z3_tactic_using_params); - in.register_cmd(397, exec_Z3_probe_const); - in.register_cmd(398, exec_Z3_probe_lt); - in.register_cmd(399, exec_Z3_probe_le); - in.register_cmd(400, exec_Z3_probe_gt); - in.register_cmd(401, exec_Z3_probe_ge); - in.register_cmd(402, exec_Z3_probe_eq); - in.register_cmd(403, exec_Z3_probe_and); - in.register_cmd(404, exec_Z3_probe_or); - in.register_cmd(405, exec_Z3_probe_not); - in.register_cmd(406, exec_Z3_get_num_tactics); - in.register_cmd(407, exec_Z3_get_tactic_name); - in.register_cmd(408, exec_Z3_get_num_probes); - in.register_cmd(409, exec_Z3_get_probe_name); - in.register_cmd(410, exec_Z3_tactic_get_help); - in.register_cmd(411, exec_Z3_tactic_get_param_descrs); - in.register_cmd(412, exec_Z3_tactic_get_descr); - in.register_cmd(413, exec_Z3_probe_get_descr); - in.register_cmd(414, exec_Z3_probe_apply); - in.register_cmd(415, exec_Z3_tactic_apply); - in.register_cmd(416, exec_Z3_tactic_apply_ex); - in.register_cmd(417, exec_Z3_apply_result_inc_ref); - in.register_cmd(418, exec_Z3_apply_result_dec_ref); - in.register_cmd(419, exec_Z3_apply_result_to_string); - in.register_cmd(420, exec_Z3_apply_result_get_num_subgoals); - in.register_cmd(421, exec_Z3_apply_result_get_subgoal); - in.register_cmd(422, exec_Z3_apply_result_convert_model); - in.register_cmd(423, exec_Z3_mk_solver); - in.register_cmd(424, exec_Z3_mk_simple_solver); - in.register_cmd(425, exec_Z3_mk_solver_for_logic); - in.register_cmd(426, exec_Z3_mk_solver_from_tactic); - in.register_cmd(427, exec_Z3_solver_get_help); - in.register_cmd(428, exec_Z3_solver_get_param_descrs); - in.register_cmd(429, exec_Z3_solver_set_params); - in.register_cmd(430, exec_Z3_solver_inc_ref); - in.register_cmd(431, exec_Z3_solver_dec_ref); - in.register_cmd(432, exec_Z3_solver_push); - in.register_cmd(433, exec_Z3_solver_pop); - in.register_cmd(434, exec_Z3_solver_reset); - in.register_cmd(435, exec_Z3_solver_get_num_scopes); - in.register_cmd(436, exec_Z3_solver_assert); - in.register_cmd(437, exec_Z3_solver_get_assertions); - in.register_cmd(438, exec_Z3_solver_check); - in.register_cmd(439, exec_Z3_solver_check_assumptions); - in.register_cmd(440, exec_Z3_solver_get_model); - in.register_cmd(441, exec_Z3_solver_get_proof); - in.register_cmd(442, exec_Z3_solver_get_unsat_core); - in.register_cmd(443, exec_Z3_solver_get_reason_unknown); - in.register_cmd(444, exec_Z3_solver_get_statistics); - in.register_cmd(445, exec_Z3_solver_to_string); - in.register_cmd(446, exec_Z3_stats_to_string); - in.register_cmd(447, exec_Z3_stats_inc_ref); - in.register_cmd(448, exec_Z3_stats_dec_ref); - in.register_cmd(449, exec_Z3_stats_size); - in.register_cmd(450, exec_Z3_stats_get_key); - in.register_cmd(451, exec_Z3_stats_is_uint); - in.register_cmd(452, exec_Z3_stats_is_double); - in.register_cmd(453, exec_Z3_stats_get_uint_value); - in.register_cmd(454, exec_Z3_stats_get_double_value); - in.register_cmd(455, exec_Z3_mk_ast_vector); - in.register_cmd(456, exec_Z3_ast_vector_inc_ref); - in.register_cmd(457, exec_Z3_ast_vector_dec_ref); - in.register_cmd(458, exec_Z3_ast_vector_size); - in.register_cmd(459, exec_Z3_ast_vector_get); - in.register_cmd(460, exec_Z3_ast_vector_set); - in.register_cmd(461, exec_Z3_ast_vector_resize); - in.register_cmd(462, exec_Z3_ast_vector_push); - in.register_cmd(463, exec_Z3_ast_vector_translate); - in.register_cmd(464, exec_Z3_ast_vector_to_string); - in.register_cmd(465, exec_Z3_mk_ast_map); - in.register_cmd(466, exec_Z3_ast_map_inc_ref); - in.register_cmd(467, exec_Z3_ast_map_dec_ref); - in.register_cmd(468, exec_Z3_ast_map_contains); - in.register_cmd(469, exec_Z3_ast_map_find); - in.register_cmd(470, exec_Z3_ast_map_insert); - in.register_cmd(471, exec_Z3_ast_map_erase); - in.register_cmd(472, exec_Z3_ast_map_size); - in.register_cmd(473, exec_Z3_ast_map_reset); - in.register_cmd(474, exec_Z3_ast_map_keys); - in.register_cmd(475, exec_Z3_ast_map_to_string); + in.register_cmd(360, exec_Z3_param_descrs_to_string); + in.register_cmd(361, exec_Z3_interrupt); + in.register_cmd(362, exec_Z3_get_error_msg_ex); + in.register_cmd(363, exec_Z3_translate); + in.register_cmd(364, exec_Z3_mk_goal); + in.register_cmd(365, exec_Z3_goal_inc_ref); + in.register_cmd(366, exec_Z3_goal_dec_ref); + in.register_cmd(367, exec_Z3_goal_precision); + in.register_cmd(368, exec_Z3_goal_assert); + in.register_cmd(369, exec_Z3_goal_inconsistent); + in.register_cmd(370, exec_Z3_goal_depth); + in.register_cmd(371, exec_Z3_goal_reset); + in.register_cmd(372, exec_Z3_goal_size); + in.register_cmd(373, exec_Z3_goal_formula); + in.register_cmd(374, exec_Z3_goal_num_exprs); + in.register_cmd(375, exec_Z3_goal_is_decided_sat); + in.register_cmd(376, exec_Z3_goal_is_decided_unsat); + in.register_cmd(377, exec_Z3_goal_translate); + in.register_cmd(378, exec_Z3_goal_to_string); + in.register_cmd(379, exec_Z3_mk_tactic); + in.register_cmd(380, exec_Z3_mk_probe); + in.register_cmd(381, exec_Z3_tactic_inc_ref); + in.register_cmd(382, exec_Z3_tactic_dec_ref); + in.register_cmd(383, exec_Z3_probe_inc_ref); + in.register_cmd(384, exec_Z3_probe_dec_ref); + in.register_cmd(385, exec_Z3_tactic_and_then); + in.register_cmd(386, exec_Z3_tactic_or_else); + in.register_cmd(387, exec_Z3_tactic_par_or); + in.register_cmd(388, exec_Z3_tactic_par_and_then); + in.register_cmd(389, exec_Z3_tactic_try_for); + in.register_cmd(390, exec_Z3_tactic_when); + in.register_cmd(391, exec_Z3_tactic_cond); + in.register_cmd(392, exec_Z3_tactic_repeat); + in.register_cmd(393, exec_Z3_tactic_skip); + in.register_cmd(394, exec_Z3_tactic_fail); + in.register_cmd(395, exec_Z3_tactic_fail_if); + in.register_cmd(396, exec_Z3_tactic_fail_if_not_decided); + in.register_cmd(397, exec_Z3_tactic_using_params); + in.register_cmd(398, exec_Z3_probe_const); + in.register_cmd(399, exec_Z3_probe_lt); + in.register_cmd(400, exec_Z3_probe_le); + in.register_cmd(401, exec_Z3_probe_gt); + in.register_cmd(402, exec_Z3_probe_ge); + in.register_cmd(403, exec_Z3_probe_eq); + in.register_cmd(404, exec_Z3_probe_and); + in.register_cmd(405, exec_Z3_probe_or); + in.register_cmd(406, exec_Z3_probe_not); + in.register_cmd(407, exec_Z3_get_num_tactics); + in.register_cmd(408, exec_Z3_get_tactic_name); + in.register_cmd(409, exec_Z3_get_num_probes); + in.register_cmd(410, exec_Z3_get_probe_name); + in.register_cmd(411, exec_Z3_tactic_get_help); + in.register_cmd(412, exec_Z3_tactic_get_param_descrs); + in.register_cmd(413, exec_Z3_tactic_get_descr); + in.register_cmd(414, exec_Z3_probe_get_descr); + in.register_cmd(415, exec_Z3_probe_apply); + in.register_cmd(416, exec_Z3_tactic_apply); + in.register_cmd(417, exec_Z3_tactic_apply_ex); + in.register_cmd(418, exec_Z3_apply_result_inc_ref); + in.register_cmd(419, exec_Z3_apply_result_dec_ref); + in.register_cmd(420, exec_Z3_apply_result_to_string); + in.register_cmd(421, exec_Z3_apply_result_get_num_subgoals); + in.register_cmd(422, exec_Z3_apply_result_get_subgoal); + in.register_cmd(423, exec_Z3_apply_result_convert_model); + in.register_cmd(424, exec_Z3_mk_solver); + in.register_cmd(425, exec_Z3_mk_simple_solver); + in.register_cmd(426, exec_Z3_mk_solver_for_logic); + in.register_cmd(427, exec_Z3_mk_solver_from_tactic); + in.register_cmd(428, exec_Z3_solver_get_help); + in.register_cmd(429, exec_Z3_solver_get_param_descrs); + in.register_cmd(430, exec_Z3_solver_set_params); + in.register_cmd(431, exec_Z3_solver_inc_ref); + in.register_cmd(432, exec_Z3_solver_dec_ref); + in.register_cmd(433, exec_Z3_solver_push); + in.register_cmd(434, exec_Z3_solver_pop); + in.register_cmd(435, exec_Z3_solver_reset); + in.register_cmd(436, exec_Z3_solver_get_num_scopes); + in.register_cmd(437, exec_Z3_solver_assert); + in.register_cmd(438, exec_Z3_solver_get_assertions); + in.register_cmd(439, exec_Z3_solver_check); + in.register_cmd(440, exec_Z3_solver_check_assumptions); + in.register_cmd(441, exec_Z3_solver_get_model); + in.register_cmd(442, exec_Z3_solver_get_proof); + in.register_cmd(443, exec_Z3_solver_get_unsat_core); + in.register_cmd(444, exec_Z3_solver_get_reason_unknown); + in.register_cmd(445, exec_Z3_solver_get_statistics); + in.register_cmd(446, exec_Z3_solver_to_string); + in.register_cmd(447, exec_Z3_stats_to_string); + in.register_cmd(448, exec_Z3_stats_inc_ref); + in.register_cmd(449, exec_Z3_stats_dec_ref); + in.register_cmd(450, exec_Z3_stats_size); + in.register_cmd(451, exec_Z3_stats_get_key); + in.register_cmd(452, exec_Z3_stats_is_uint); + in.register_cmd(453, exec_Z3_stats_is_double); + in.register_cmd(454, exec_Z3_stats_get_uint_value); + in.register_cmd(455, exec_Z3_stats_get_double_value); + in.register_cmd(456, exec_Z3_mk_ast_vector); + in.register_cmd(457, exec_Z3_ast_vector_inc_ref); + in.register_cmd(458, exec_Z3_ast_vector_dec_ref); + in.register_cmd(459, exec_Z3_ast_vector_size); + in.register_cmd(460, exec_Z3_ast_vector_get); + in.register_cmd(461, exec_Z3_ast_vector_set); + in.register_cmd(462, exec_Z3_ast_vector_resize); + in.register_cmd(463, exec_Z3_ast_vector_push); + in.register_cmd(464, exec_Z3_ast_vector_translate); + in.register_cmd(465, exec_Z3_ast_vector_to_string); + in.register_cmd(466, exec_Z3_mk_ast_map); + in.register_cmd(467, exec_Z3_ast_map_inc_ref); + in.register_cmd(468, exec_Z3_ast_map_dec_ref); + in.register_cmd(469, exec_Z3_ast_map_contains); + in.register_cmd(470, exec_Z3_ast_map_find); + in.register_cmd(471, exec_Z3_ast_map_insert); + in.register_cmd(472, exec_Z3_ast_map_erase); + in.register_cmd(473, exec_Z3_ast_map_size); + in.register_cmd(474, exec_Z3_ast_map_reset); + in.register_cmd(475, exec_Z3_ast_map_keys); + in.register_cmd(476, exec_Z3_ast_map_to_string); } diff --git a/lib/api_log_macros.cpp b/lib/api_log_macros.cpp index 4358b3dc0..997978725 100644 --- a/lib/api_log_macros.cpp +++ b/lib/api_log_macros.cpp @@ -2570,23 +2570,29 @@ void log_Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, unsigned a2 U(a2); C(359); } +void log_Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1) { + R(); + P(a0); + P(a1); + C(360); +} void log_Z3_interrupt(Z3_context a0) { R(); P(a0); - C(360); + C(361); } void log_Z3_get_error_msg_ex(Z3_context a0, Z3_error_code a1) { R(); P(a0); U(static_cast(a1)); - C(361); + C(362); } void log_Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2) { R(); P(a0); P(a1); P(a2); - C(362); + C(363); } void log_Z3_mk_goal(Z3_context a0, Z3_bool a1, Z3_bool a2, Z3_bool a3) { R(); @@ -2594,144 +2600,144 @@ void log_Z3_mk_goal(Z3_context a0, Z3_bool a1, Z3_bool a2, Z3_bool a3) { I(a1); I(a2); I(a3); - C(363); + C(364); } void log_Z3_goal_inc_ref(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(364); + C(365); } void log_Z3_goal_dec_ref(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(365); + C(366); } void log_Z3_goal_precision(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(366); + C(367); } void log_Z3_goal_assert(Z3_context a0, Z3_goal a1, Z3_ast a2) { R(); P(a0); P(a1); P(a2); - C(367); + C(368); } void log_Z3_goal_inconsistent(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(368); + C(369); } void log_Z3_goal_depth(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(369); + C(370); } void log_Z3_goal_reset(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(370); + C(371); } void log_Z3_goal_size(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(371); + C(372); } void log_Z3_goal_formula(Z3_context a0, Z3_goal a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(372); + C(373); } void log_Z3_goal_num_exprs(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(373); + C(374); } void log_Z3_goal_is_decided_sat(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(374); + C(375); } void log_Z3_goal_is_decided_unsat(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(375); + C(376); } void log_Z3_goal_translate(Z3_context a0, Z3_goal a1, Z3_context a2) { R(); P(a0); P(a1); P(a2); - C(376); + C(377); } void log_Z3_goal_to_string(Z3_context a0, Z3_goal a1) { R(); P(a0); P(a1); - C(377); + C(378); } void log_Z3_mk_tactic(Z3_context a0, Z3_string a1) { R(); P(a0); S(a1); - C(378); + C(379); } void log_Z3_mk_probe(Z3_context a0, Z3_string a1) { R(); P(a0); S(a1); - C(379); + C(380); } void log_Z3_tactic_inc_ref(Z3_context a0, Z3_tactic a1) { R(); P(a0); P(a1); - C(380); + C(381); } void log_Z3_tactic_dec_ref(Z3_context a0, Z3_tactic a1) { R(); P(a0); P(a1); - C(381); + C(382); } void log_Z3_probe_inc_ref(Z3_context a0, Z3_probe a1) { R(); P(a0); P(a1); - C(382); + C(383); } void log_Z3_probe_dec_ref(Z3_context a0, Z3_probe a1) { R(); P(a0); P(a1); - C(383); + C(384); } void log_Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2) { R(); P(a0); P(a1); P(a2); - C(384); + C(385); } void log_Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2) { R(); P(a0); P(a1); P(a2); - C(385); + C(386); } void log_Z3_tactic_par_or(Z3_context a0, unsigned a1, Z3_tactic const * a2) { R(); @@ -2739,28 +2745,28 @@ void log_Z3_tactic_par_or(Z3_context a0, unsigned a1, Z3_tactic const * a2) { U(a1); for (unsigned i = 0; i < a1; i++) { P(a2[i]); } Ap(a1); - C(386); + C(387); } void log_Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2) { R(); P(a0); P(a1); P(a2); - C(387); + C(388); } void log_Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(388); + C(389); } void log_Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2) { R(); P(a0); P(a1); P(a2); - C(389); + C(390); } void log_Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3) { R(); @@ -2768,163 +2774,163 @@ void log_Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3) P(a1); P(a2); P(a3); - C(390); + C(391); } void log_Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(391); + C(392); } void log_Z3_tactic_skip(Z3_context a0) { R(); P(a0); - C(392); + C(393); } void log_Z3_tactic_fail(Z3_context a0) { R(); P(a0); - C(393); + C(394); } void log_Z3_tactic_fail_if(Z3_context a0, Z3_probe a1) { R(); P(a0); P(a1); - C(394); + C(395); } void log_Z3_tactic_fail_if_not_decided(Z3_context a0) { R(); P(a0); - C(395); + C(396); } void log_Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2) { R(); P(a0); P(a1); P(a2); - C(396); + C(397); } void log_Z3_probe_const(Z3_context a0, double a1) { R(); P(a0); D(a1); - C(397); + C(398); } void log_Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2) { R(); P(a0); P(a1); P(a2); - C(398); + C(399); } void log_Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2) { R(); P(a0); P(a1); P(a2); - C(399); + C(400); } void log_Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2) { R(); P(a0); P(a1); P(a2); - C(400); + C(401); } void log_Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2) { R(); P(a0); P(a1); P(a2); - C(401); + C(402); } void log_Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2) { R(); P(a0); P(a1); P(a2); - C(402); + C(403); } void log_Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2) { R(); P(a0); P(a1); P(a2); - C(403); + C(404); } void log_Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2) { R(); P(a0); P(a1); P(a2); - C(404); + C(405); } void log_Z3_probe_not(Z3_context a0, Z3_probe a1) { R(); P(a0); P(a1); - C(405); + C(406); } void log_Z3_get_num_tactics(Z3_context a0) { R(); P(a0); - C(406); + C(407); } void log_Z3_get_tactic_name(Z3_context a0, unsigned a1) { R(); P(a0); U(a1); - C(407); + C(408); } void log_Z3_get_num_probes(Z3_context a0) { R(); P(a0); - C(408); + C(409); } void log_Z3_get_probe_name(Z3_context a0, unsigned a1) { R(); P(a0); U(a1); - C(409); + C(410); } void log_Z3_tactic_get_help(Z3_context a0, Z3_tactic a1) { R(); P(a0); P(a1); - C(410); + C(411); } void log_Z3_tactic_get_param_descrs(Z3_context a0, Z3_tactic a1) { R(); P(a0); P(a1); - C(411); + C(412); } void log_Z3_tactic_get_descr(Z3_context a0, Z3_string a1) { R(); P(a0); S(a1); - C(412); + C(413); } void log_Z3_probe_get_descr(Z3_context a0, Z3_string a1) { R(); P(a0); S(a1); - C(413); + C(414); } void log_Z3_probe_apply(Z3_context a0, Z3_probe a1, Z3_goal a2) { R(); P(a0); P(a1); P(a2); - C(414); + C(415); } void log_Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2) { R(); P(a0); P(a1); P(a2); - C(415); + C(416); } void log_Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3) { R(); @@ -2932,38 +2938,38 @@ void log_Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a P(a1); P(a2); P(a3); - C(416); + C(417); } void log_Z3_apply_result_inc_ref(Z3_context a0, Z3_apply_result a1) { R(); P(a0); P(a1); - C(417); + C(418); } void log_Z3_apply_result_dec_ref(Z3_context a0, Z3_apply_result a1) { R(); P(a0); P(a1); - C(418); + C(419); } void log_Z3_apply_result_to_string(Z3_context a0, Z3_apply_result a1) { R(); P(a0); P(a1); - C(419); + C(420); } void log_Z3_apply_result_get_num_subgoals(Z3_context a0, Z3_apply_result a1) { R(); P(a0); P(a1); - C(420); + C(421); } void log_Z3_apply_result_get_subgoal(Z3_context a0, Z3_apply_result a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(421); + C(422); } void log_Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, unsigned a2, Z3_model a3) { R(); @@ -2971,104 +2977,104 @@ void log_Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, unsign P(a1); U(a2); P(a3); - C(422); + C(423); } void log_Z3_mk_solver(Z3_context a0) { R(); P(a0); - C(423); + C(424); } void log_Z3_mk_simple_solver(Z3_context a0) { R(); P(a0); - C(424); + C(425); } void log_Z3_mk_solver_for_logic(Z3_context a0, Z3_symbol a1) { R(); P(a0); Sy(a1); - C(425); + C(426); } void log_Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1) { R(); P(a0); P(a1); - C(426); + C(427); } void log_Z3_solver_get_help(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(427); + C(428); } void log_Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(428); + C(429); } void log_Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2) { R(); P(a0); P(a1); P(a2); - C(429); + C(430); } void log_Z3_solver_inc_ref(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(430); + C(431); } void log_Z3_solver_dec_ref(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(431); + C(432); } void log_Z3_solver_push(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(432); + C(433); } void log_Z3_solver_pop(Z3_context a0, Z3_solver a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(433); + C(434); } void log_Z3_solver_reset(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(434); + C(435); } void log_Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(435); + C(436); } void log_Z3_solver_assert(Z3_context a0, Z3_solver a1, Z3_ast a2) { R(); P(a0); P(a1); P(a2); - C(436); + C(437); } void log_Z3_solver_get_assertions(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(437); + C(438); } void log_Z3_solver_check(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(438); + C(439); } void log_Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, unsigned a2, Z3_ast const * a3) { R(); @@ -3077,132 +3083,132 @@ void log_Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, unsigned a2, Z U(a2); for (unsigned i = 0; i < a2; i++) { P(a3[i]); } Ap(a2); - C(439); + C(440); } void log_Z3_solver_get_model(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(440); + C(441); } void log_Z3_solver_get_proof(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(441); + C(442); } void log_Z3_solver_get_unsat_core(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(442); + C(443); } void log_Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(443); + C(444); } void log_Z3_solver_get_statistics(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(444); + C(445); } void log_Z3_solver_to_string(Z3_context a0, Z3_solver a1) { R(); P(a0); P(a1); - C(445); + C(446); } void log_Z3_stats_to_string(Z3_context a0, Z3_stats a1) { R(); P(a0); P(a1); - C(446); + C(447); } void log_Z3_stats_inc_ref(Z3_context a0, Z3_stats a1) { R(); P(a0); P(a1); - C(447); + C(448); } void log_Z3_stats_dec_ref(Z3_context a0, Z3_stats a1) { R(); P(a0); P(a1); - C(448); + C(449); } void log_Z3_stats_size(Z3_context a0, Z3_stats a1) { R(); P(a0); P(a1); - C(449); + C(450); } void log_Z3_stats_get_key(Z3_context a0, Z3_stats a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(450); + C(451); } void log_Z3_stats_is_uint(Z3_context a0, Z3_stats a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(451); + C(452); } void log_Z3_stats_is_double(Z3_context a0, Z3_stats a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(452); + C(453); } void log_Z3_stats_get_uint_value(Z3_context a0, Z3_stats a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(453); + C(454); } void log_Z3_stats_get_double_value(Z3_context a0, Z3_stats a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(454); + C(455); } void log_Z3_mk_ast_vector(Z3_context a0) { R(); P(a0); - C(455); + C(456); } void log_Z3_ast_vector_inc_ref(Z3_context a0, Z3_ast_vector a1) { R(); P(a0); P(a1); - C(456); + C(457); } void log_Z3_ast_vector_dec_ref(Z3_context a0, Z3_ast_vector a1) { R(); P(a0); P(a1); - C(457); + C(458); } void log_Z3_ast_vector_size(Z3_context a0, Z3_ast_vector a1) { R(); P(a0); P(a1); - C(458); + C(459); } void log_Z3_ast_vector_get(Z3_context a0, Z3_ast_vector a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(459); + C(460); } void log_Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, unsigned a2, Z3_ast a3) { R(); @@ -3210,65 +3216,65 @@ void log_Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, unsigned a2, Z3_ast P(a1); U(a2); P(a3); - C(460); + C(461); } void log_Z3_ast_vector_resize(Z3_context a0, Z3_ast_vector a1, unsigned a2) { R(); P(a0); P(a1); U(a2); - C(461); + C(462); } void log_Z3_ast_vector_push(Z3_context a0, Z3_ast_vector a1, Z3_ast a2) { R(); P(a0); P(a1); P(a2); - C(462); + C(463); } void log_Z3_ast_vector_translate(Z3_context a0, Z3_ast_vector a1, Z3_context a2) { R(); P(a0); P(a1); P(a2); - C(463); + C(464); } void log_Z3_ast_vector_to_string(Z3_context a0, Z3_ast_vector a1) { R(); P(a0); P(a1); - C(464); + C(465); } void log_Z3_mk_ast_map(Z3_context a0) { R(); P(a0); - C(465); + C(466); } void log_Z3_ast_map_inc_ref(Z3_context a0, Z3_ast_map a1) { R(); P(a0); P(a1); - C(466); + C(467); } void log_Z3_ast_map_dec_ref(Z3_context a0, Z3_ast_map a1) { R(); P(a0); P(a1); - C(467); + C(468); } void log_Z3_ast_map_contains(Z3_context a0, Z3_ast_map a1, Z3_ast a2) { R(); P(a0); P(a1); P(a2); - C(468); + C(469); } void log_Z3_ast_map_find(Z3_context a0, Z3_ast_map a1, Z3_ast a2) { R(); P(a0); P(a1); P(a2); - C(469); + C(470); } void log_Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3) { R(); @@ -3276,36 +3282,36 @@ void log_Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3) { P(a1); P(a2); P(a3); - C(470); + C(471); } void log_Z3_ast_map_erase(Z3_context a0, Z3_ast_map a1, Z3_ast a2) { R(); P(a0); P(a1); P(a2); - C(471); + C(472); } void log_Z3_ast_map_size(Z3_context a0, Z3_ast_map a1) { R(); P(a0); P(a1); - C(472); + C(473); } void log_Z3_ast_map_reset(Z3_context a0, Z3_ast_map a1) { R(); P(a0); P(a1); - C(473); + C(474); } void log_Z3_ast_map_keys(Z3_context a0, Z3_ast_map a1) { R(); P(a0); P(a1); - C(474); + C(475); } void log_Z3_ast_map_to_string(Z3_context a0, Z3_ast_map a1) { R(); P(a0); P(a1); - C(475); + C(476); } diff --git a/lib/api_log_macros.h b/lib/api_log_macros.h index ca2dde6d5..ac5e806c2 100644 --- a/lib/api_log_macros.h +++ b/lib/api_log_macros.h @@ -741,6 +741,8 @@ void log_Z3_param_descrs_size(Z3_context a0, Z3_param_descrs a1); #define LOG_Z3_param_descrs_size(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_size(_ARG0, _ARG1); } void log_Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, unsigned a2); #define LOG_Z3_param_descrs_get_name(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_get_name(_ARG0, _ARG1, _ARG2); } +void log_Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1); +#define LOG_Z3_param_descrs_to_string(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_to_string(_ARG0, _ARG1); } void log_Z3_interrupt(Z3_context a0); #define LOG_Z3_interrupt(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_interrupt(_ARG0); } void log_Z3_get_error_msg_ex(Z3_context a0, Z3_error_code a1); diff --git a/lib/api_params.cpp b/lib/api_params.cpp index 2badef8d6..74899bc44 100644 --- a/lib/api_params.cpp +++ b/lib/api_params.cpp @@ -179,4 +179,21 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p) { + Z3_TRY; + LOG_Z3_param_descrs_to_string(c, p); + RESET_ERROR_CODE(); + std::ostringstream buffer; + buffer << "("; + unsigned sz = to_param_descrs_ptr(p)->size(); + for (unsigned i = 0; i < sz; i++) { + if (i > 0) + buffer << ", "; + buffer << to_param_descrs_ptr(p)->get_param_name(i); + } + buffer << ")"; + return mk_c(c)->mk_external_string(buffer.str()); + Z3_CATCH_RETURN(""); + } + }; diff --git a/lib/z3_api.h b/lib/z3_api.h index 6afcdcb49..f4c4e8260 100644 --- a/lib/z3_api.h +++ b/lib/z3_api.h @@ -1456,6 +1456,12 @@ extern "C" { */ Z3_symbol Z3_API Z3_param_descrs_get_name(__in Z3_context c, __in Z3_param_descrs p, __in unsigned i); + /** + \brief Convert a parameter description set into a string. This function is mainly used for printing the + contents of a parameter description set. + */ + Z3_string Z3_API Z3_param_descrs_to_string(__in Z3_context c, __in Z3_param_descrs p); + /*@}*/ #endif diff --git a/python/z3.py b/python/z3.py index dea752a87..011d63851 100644 --- a/python/z3.py +++ b/python/z3.py @@ -4421,18 +4421,7 @@ class ParamDescrsRef: return self.get_kind(arg) def __repr__(self): - r = io.StringIO() - first = True - r.write(u'(') - for i in range(self.size()): - if first: - first = False - else: - r.write(u' ') - r.write(u'%s' % self.get_name(i)) - r.write(u')') - return r.getvalue() - + return Z3_param_descrs_to_string(self.ctx.ref(), self.descr) ######################################### # diff --git a/python/z3core.py b/python/z3core.py index 588e9fa86..5ae71a35d 100644 --- a/python/z3core.py +++ b/python/z3core.py @@ -696,6 +696,8 @@ def init(PATH): _lib.Z3_param_descrs_size.argtypes = [ContextObj, ParamDescrs] _lib.Z3_param_descrs_get_name.restype = Symbol _lib.Z3_param_descrs_get_name.argtypes = [ContextObj, ParamDescrs, ctypes.c_uint] + _lib.Z3_param_descrs_to_string.restype = ctypes.c_char_p + _lib.Z3_param_descrs_to_string.argtypes = [ContextObj, ParamDescrs] _lib.Z3_interrupt.argtypes = [ContextObj] _lib.Z3_get_error_msg_ex.restype = ctypes.c_char_p _lib.Z3_get_error_msg_ex.argtypes = [ContextObj, ctypes.c_uint] @@ -3341,6 +3343,13 @@ def Z3_param_descrs_get_name(a0, a1, a2): raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) return r +def Z3_param_descrs_to_string(a0, a1): + r = lib().Z3_param_descrs_to_string(a0, a1) + err = lib().Z3_get_error_code(a0) + if err != Z3_OK: + raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) + return r + def Z3_interrupt(a0): lib().Z3_interrupt(a0) err = lib().Z3_get_error_code(a0) From 44db8c083db990a71ecd31c586671303d3f8f005 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Oct 2012 09:42:45 -0700 Subject: [PATCH 12/16] exposed solver object param descrs Signed-off-by: Leonardo de Moura --- lib/ni_solver.cpp | 6 ++++++ lib/smt_solver.cpp | 8 ++------ lib/smt_solver.h | 2 +- lib/solver.cpp | 13 ++++++++++--- 4 files changed, 19 insertions(+), 10 deletions(-) diff --git a/lib/ni_solver.cpp b/lib/ni_solver.cpp index be7272d36..a0341cb32 100644 --- a/lib/ni_solver.cpp +++ b/lib/ni_solver.cpp @@ -146,6 +146,12 @@ public: if (m_context) m_context->set_progress_callback(callback); } + + + virtual void collect_param_descrs(param_descrs & r) { + smt::solver::collect_param_descrs(r); + } + }; solver * mk_non_incremental_smt_solver(cmd_context & ctx) { diff --git a/lib/smt_solver.cpp b/lib/smt_solver.cpp index 82b599869..6bdfd0524 100644 --- a/lib/smt_solver.cpp +++ b/lib/smt_solver.cpp @@ -181,10 +181,6 @@ namespace smt { void updt_params(params_ref const & p) { params2front_end_params(p, fparams()); } - - void collect_param_descrs(param_descrs & d) { - solver_front_end_params_descrs(d); - } }; solver::solver(ast_manager & m, front_end_params & fp, params_ref const & p) { @@ -346,8 +342,8 @@ namespace smt { return m_imp->updt_params(p); } - void solver::collect_param_descrs(param_descrs & d) const { - return m_imp->collect_param_descrs(d); + void solver::collect_param_descrs(param_descrs & d) { + solver_front_end_params_descrs(d); } context & solver::kernel() { diff --git a/lib/smt_solver.h b/lib/smt_solver.h index 68d85e8d6..1d04df9ed 100644 --- a/lib/smt_solver.h +++ b/lib/smt_solver.h @@ -228,7 +228,7 @@ namespace smt { /** \brief Collect a description of the configuration parameters. */ - void collect_param_descrs(param_descrs & d) const; + static void collect_param_descrs(param_descrs & d); /** \brief Return a reference to the kernel. diff --git a/lib/solver.cpp b/lib/solver.cpp index 185223048..fd2be70d3 100644 --- a/lib/solver.cpp +++ b/lib/solver.cpp @@ -55,9 +55,16 @@ public: } virtual void collect_param_descrs(param_descrs & r) { - if (m_context == 0) - return; - m_context->collect_param_descrs(r); + if (m_context == 0) { + ast_manager m; + m.register_decl_plugins(); + front_end_params p; + smt::solver s(m, p); + s.collect_param_descrs(r); + } + else { + m_context->collect_param_descrs(r); + } } virtual void init(ast_manager & m, symbol const & logic) { From c48bd1e8de4f5f2881c450bf1e88d91f2abe6bb5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Oct 2012 12:16:20 -0700 Subject: [PATCH 13/16] updated release notes Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 909b15b11..af966c9a8 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,5 +1,32 @@ RELEASE NOTES +Version 4.2 +=========== + +- Now, Z3 automatically adds arithmetic coercions: to_real and to_int. + Option (set-option :int-real-coercions false) disables this feature. + If SMTLIB2_COMPLIANT=true in the command line, then :int-real-coercions is also set to false. + +- SMTLIB2_COMPLIANT is false by default. Use command line option SMTLIB2_COMPLIANT=true to enable it back. + +- Added "make install" and "make uninstall" to Makefile.in. + +- Added "make install-z3py" and "make uninstall-z3py" to Makefile.in. + +- Fixed crash/bug in the simplifier. The crash occurred when option ":sort-sums true" was used. + +- Added "--with-python=" option to configure script. + +- Cleanned c++, maxsat, test_mapi examples. + +- Move RELEASE_NOTES files to source code distribution. + +- Removed unnecessary files from source code distribution. + +- Removed unnecessary compilation modes from z3-prover.sln. + +- Added Xor procedure to Z3Py. + First source code release (October 2, 2012) =========================================== From c2623e15c3c0646418a194049e92cb93dd3d61bd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 12 Oct 2012 21:05:32 +0100 Subject: [PATCH 14/16] Switched ParamDescrs.ToString to native implementation Signed-off-by: Christoph M. Wintersteiger --- Microsoft.Z3/ParamDescrs.cs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/Microsoft.Z3/ParamDescrs.cs b/Microsoft.Z3/ParamDescrs.cs index 961bceeff..ca6db9abf 100644 --- a/Microsoft.Z3/ParamDescrs.cs +++ b/Microsoft.Z3/ParamDescrs.cs @@ -75,12 +75,7 @@ namespace Microsoft.Z3 /// public override string ToString() { - String res = ""; - Symbol[] n = Names; - if (n.Length > 0) res = n[0].ToString(); - for (uint i = 1; i < n.Length; i++) - res += " " + n[i].ToString(); - return res; + return Native.Z3_param_descrs_to_string(Context.nCtx, NativeObject); } #region Internal From 75457e13933bfa02201681fd3033062531f66ae1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Oct 2012 16:34:54 -0700 Subject: [PATCH 15/16] int<->real coercions. Signed-off-by: Leonardo de Moura --- c++/z3++.h | 1 + lib/arith_decl_plugin.cpp | 40 +++++++++++++++++--- lib/arith_rewriter.cpp | 36 ++++++++++++++++++ lib/array_decl_plugin.cpp | 24 +++++++----- lib/ast.cpp | 79 +++++++++++++++++++++++++++++++++++++-- lib/ast.h | 12 ++++++ lib/basic_cmds.cpp | 8 ++++ lib/cmd_context.cpp | 2 + lib/front_end_params.h | 3 +- 9 files changed, 184 insertions(+), 21 deletions(-) diff --git a/c++/z3++.h b/c++/z3++.h index 5d85b09c4..8a2499321 100644 --- a/c++/z3++.h +++ b/c++/z3++.h @@ -246,6 +246,7 @@ namespace z3 { ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); } ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); } operator Z3_ast() const { return m_ast; } + operator bool() const { return m_ast != 0; } ast & operator=(ast const & s) { Z3_inc_ref(s.ctx(), s.m_ast); if (m_ast) Z3_dec_ref(ctx(), m_ast); m_ctx = s.m_ctx; m_ast = s.m_ast; return *this; } Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; } unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; } diff --git a/lib/arith_decl_plugin.cpp b/lib/arith_decl_plugin.cpp index 926e91c20..4aadafae2 100644 --- a/lib/arith_decl_plugin.cpp +++ b/lib/arith_decl_plugin.cpp @@ -332,8 +332,8 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { case OP_SUB: return is_real ? m_r_sub_decl : m_i_sub_decl; case OP_UMINUS: return is_real ? m_r_uminus_decl : m_i_uminus_decl; case OP_MUL: return is_real ? m_r_mul_decl : m_i_mul_decl; - case OP_DIV: SASSERT(is_real); return m_r_div_decl; - case OP_IDIV: SASSERT(!is_real); return m_i_div_decl; + case OP_DIV: return m_r_div_decl; + case OP_IDIV: return m_i_div_decl; case OP_REM: return m_i_rem_decl; case OP_MOD: return m_i_mod_decl; case OP_TO_REAL: return m_to_real_decl; @@ -415,6 +415,24 @@ func_decl * arith_decl_plugin::mk_num_decl(unsigned num_parameters, parameter co else return m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, num_parameters, parameters)); } + +static bool use_coercion(decl_kind k) { + return k == OP_ADD || k == OP_SUB || k == OP_MUL || k == OP_POWER || k == OP_LE || k == OP_GE || k == OP_LT || k == OP_GT || k == OP_UMINUS; +} + +static bool has_real_arg(unsigned arity, sort * const * domain, sort * real_sort) { + for (unsigned i = 0; i < arity; i++) + if (domain[i] == real_sort) + return true; + return false; +} + +static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args, sort * real_sort) { + for (unsigned i = 0; i < num_args; i++) + if (m->get_sort(args[i]) == real_sort) + return true; + return false; +} func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -424,8 +442,13 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } - bool is_real = arity > 0 && domain[0] == m_real_decl; - return mk_func_decl(fix_kind(k, arity), is_real); + if (m_manager->int_real_coercions() && use_coercion(k)) { + return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl)); + } + else { + bool is_real = arity > 0 && domain[0] == m_real_decl; + return mk_func_decl(fix_kind(k, arity), is_real); + } } func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -436,8 +459,13 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } - bool is_real = num_args > 0 && m_manager->get_sort(args[0]) == m_real_decl; - return mk_func_decl(fix_kind(k, num_args), is_real); + if (m_manager->int_real_coercions() && use_coercion(k)) { + return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl)); + } + else { + bool is_real = num_args > 0 && m_manager->get_sort(args[0]) == m_real_decl; + return mk_func_decl(fix_kind(k, num_args), is_real); + } } void arith_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { diff --git a/lib/arith_rewriter.cpp b/lib/arith_rewriter.cpp index 74562befd..3efc14abe 100644 --- a/lib/arith_rewriter.cpp +++ b/lib/arith_rewriter.cpp @@ -943,6 +943,42 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { return BR_DONE; } else { + if (m_util.is_add(arg) || m_util.is_mul(arg) || m_util.is_power(arg)) { + // Try to apply simplifications such as: + // (to_int (+ 1.0 (to_real x))) --> (+ 1 x) + + // if all arguments of arg are + // - integer numerals, OR + // - to_real applications + // then, to_int can be eliminated + unsigned num_args = to_app(arg)->get_num_args(); + unsigned i = 0; + for (; i < num_args; i++) { + expr * c = to_app(arg)->get_arg(i); + if (m_util.is_numeral(c, a) && a.is_int()) + continue; + if (m_util.is_to_real(c)) + continue; + break; // failed + } + if (i == num_args) { + // simplification can be applied + expr_ref_buffer new_args(m()); + for (i = 0; i < num_args; i++) { + expr * c = to_app(arg)->get_arg(i); + if (m_util.is_numeral(c, a) && a.is_int()) { + new_args.push_back(m_util.mk_numeral(a, true)); + } + else { + SASSERT(m_util.is_to_real(c)); + new_args.push_back(to_app(c)->get_arg(0)); + } + } + SASSERT(num_args == new_args.size()); + result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), new_args.size(), new_args.c_ptr()); + return BR_REWRITE1; + } + } return BR_FAILED; } } diff --git a/lib/array_decl_plugin.cpp b/lib/array_decl_plugin.cpp index f2e12d46a..23d5145ea 100644 --- a/lib/array_decl_plugin.cpp +++ b/lib/array_decl_plugin.cpp @@ -237,18 +237,20 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) { m_manager->raise_exception("select requires as many arguments as the size of the domain"); return 0; } - if (domain[0] != s) { - m_manager->raise_exception("first argument of select needs to be an array"); - return 0; - } + ptr_buffer new_domain; // we need this because of coercions. + new_domain.push_back(s); for (unsigned i = 0; i + 1 < num_parameters; ++i) { - if (!parameters[i].is_ast() || domain[i+1] != parameters[i].get_ast()) { + if (!parameters[i].is_ast() || + !is_sort(parameters[i].get_ast()) || + !m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) { m_manager->raise_exception("domain sort and parameter do not match"); UNREACHABLE(); return 0; } + new_domain.push_back(to_sort(parameters[i].get_ast())); } - return m_manager->mk_func_decl(m_select_sym, arity, domain, get_array_range(domain[0]), + SASSERT(new_domain.size() == arity); + return m_manager->mk_func_decl(m_select_sym, arity, new_domain.c_ptr(), get_array_range(domain[0]), func_decl_info(m_family_id, OP_SELECT)); } @@ -273,18 +275,22 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { UNREACHABLE(); return 0; } + ptr_buffer new_domain; // we need this because of coercions. + new_domain.push_back(s); for (unsigned i = 0; i < num_parameters; ++i) { - if (!parameters[i].is_ast()) { + if (!parameters[i].is_ast() || !is_sort(parameters[i].get_ast())) { m_manager->raise_exception("expecting sort parameter"); return 0; } - if (parameters[i].get_ast() != domain[i+1]) { + if (!m_manager->compatible_sorts(to_sort(parameters[i].get_ast()), domain[i+1])) { m_manager->raise_exception("domain sort and parameter do not match"); UNREACHABLE(); return 0; } + new_domain.push_back(to_sort(parameters[i].get_ast())); } - return m_manager->mk_func_decl(m_store_sym, arity, domain, domain[0], + SASSERT(new_domain.size() == arity); + return m_manager->mk_func_decl(m_store_sym, arity, new_domain.c_ptr(), domain[0], func_decl_info(m_family_id, OP_STORE)); } diff --git a/lib/ast.cpp b/lib/ast.cpp index 8d997c4e9..bfb4a09b4 100644 --- a/lib/ast.cpp +++ b/lib/ast.cpp @@ -1231,6 +1231,7 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs): } void ast_manager::init() { + m_int_real_coercions = true; m_debug_ref_count = false; m_fresh_id = 0; m_expr_id_gen.reset(0); @@ -1241,6 +1242,7 @@ void ast_manager::init() { m_pattern_family_id = get_family_id("pattern"); m_model_value_family_id = get_family_id("model-value"); m_user_sort_family_id = get_family_id("user-sort"); + m_arith_family_id = get_family_id("arith"); basic_decl_plugin * plugin = alloc(basic_decl_plugin); register_plugin(m_basic_family_id, plugin); m_bool_sort = plugin->mk_bool_sort(); @@ -1772,7 +1774,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c sort * expected = decl->get_domain(0); for (unsigned i = 0; i < num_args; i++) { sort * given = get_sort(args[i]); - if (expected != given) { + if (!compatible_sorts(expected, given)) { string_buffer<> buff; buff << "invalid function application, sort mismatch on argument at position " << (i+1); throw ast_exception(buff.c_str()); @@ -1786,7 +1788,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c for (unsigned i = 0; i < num_args; i++) { sort * expected = decl->get_domain(i); sort * given = get_sort(args[i]); - if (expected != given) { + if (!compatible_sorts(expected, given)) { string_buffer<> buff; buff << "invalid function application, sort mismatch on argument at position " << (i+1); throw ast_exception(buff.c_str()); @@ -1822,11 +1824,80 @@ bool ast_manager::check_sorts(ast const * n) const { } } +bool ast_manager::compatible_sorts(sort * s1, sort * s2) const { + if (s1 == s2) + return true; + if (m_int_real_coercions) + return s1->get_family_id() == m_arith_family_id && s2->get_family_id() == m_arith_family_id; + return false; +} + +bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * const * args) { + SASSERT(m_int_real_coercions); + if (decl->is_associative()) { + sort * d = decl->get_domain(0); + if (d->get_family_id() == m_arith_family_id) { + for (unsigned i = 0; i < num_args; i++) { + if (d != get_sort(args[i])) + return true; + } + } + } + else { + for (unsigned i = 0; i < num_args; i++) { + sort * d = decl->get_domain(i); + if (d->get_family_id() == m_arith_family_id && d != get_sort(args[i])) + return true; + } + } + return false; +} + app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const * args) { unsigned sz = app::get_obj_size(num_args); void * mem = allocate_node(sz); - app * new_node = new (mem) app(decl, num_args, args); - app * r = register_node(new_node); + app * new_node; + app * r; + if (m_int_real_coercions && coercion_needed(decl, num_args, args)) { + expr_ref_buffer new_args(*this); + if (decl->is_associative()) { + sort * d = decl->get_domain(0); + for (unsigned i = 0; i < num_args; i++) { + sort * s = get_sort(args[i]); + if (d != s && d->get_family_id() == m_arith_family_id && s->get_family_id() == m_arith_family_id) { + if (d->get_decl_kind() == REAL_SORT) + new_args.push_back(mk_app(m_arith_family_id, OP_TO_REAL, args[i])); + else + new_args.push_back(mk_app(m_arith_family_id, OP_TO_INT, args[i])); + } + else { + new_args.push_back(args[i]); + } + } + } + else { + for (unsigned i = 0; i < num_args; i++) { + sort * d = decl->get_domain(i); + sort * s = get_sort(args[i]); + if (d != s && d->get_family_id() == m_arith_family_id && s->get_family_id() == m_arith_family_id) { + if (d->get_decl_kind() == REAL_SORT) + new_args.push_back(mk_app(m_arith_family_id, OP_TO_REAL, args[i])); + else + new_args.push_back(mk_app(m_arith_family_id, OP_TO_INT, args[i])); + } + else { + new_args.push_back(args[i]); + } + } + } + SASSERT(new_args.size() == num_args); + new_node = new (mem) app(decl, num_args, new_args.c_ptr()); + r = register_node(new_node); + } + else { + new_node = new (mem) app(decl, num_args, args); + r = register_node(new_node); + } #ifndef SMTCOMP if (m_trace_stream != NULL && r == new_node) { *m_trace_stream << "[mk-app] #" << r->get_id() << " "; diff --git a/lib/ast.h b/lib/ast.h index 8691ed1f4..558af34bd 100644 --- a/lib/ast.h +++ b/lib/ast.h @@ -1282,6 +1282,8 @@ enum proof_gen_mode { // // ----------------------------------- +class arith_decl_plugin; + class ast_manager { protected: protected: @@ -1331,11 +1333,13 @@ protected: expr_dependency_array_manager m_expr_dependency_array_manager; ptr_vector m_plugins; proof_gen_mode m_proof_mode; + bool m_int_real_coercions; // If true, use hack that automatically introduces to_int/to_real when needed. family_id m_basic_family_id; family_id m_label_family_id; family_id m_pattern_family_id; family_id m_model_value_family_id; family_id m_user_sort_family_id; + family_id m_arith_family_id; ast_table m_ast_table; id_gen m_expr_id_gen; id_gen m_decl_id_gen; @@ -1355,11 +1359,19 @@ protected: void init(); + bool coercion_needed(func_decl * decl, unsigned num_args, expr * const * args); + public: ast_manager(proof_gen_mode = PGM_DISABLED, std::ostream * trace_stream = NULL, bool is_format_manager = false); ast_manager(ast_manager const & src, bool disable_proofs = false); ~ast_manager(); + + void enable_int_real_coercions(bool f) { m_int_real_coercions = f; } + bool int_real_coercions() const { return m_int_real_coercions; } + // Return true if s1 and s2 are equal, or coercions are enabled, and s1 and s2 are compatible. + bool compatible_sorts(sort * s1, sort * s2) const; + // For debugging purposes void display_free_ids(std::ostream & out) { m_expr_id_gen.display_free_ids(out); out << "\n"; m_decl_id_gen.display_free_ids(out); } diff --git a/lib/basic_cmds.cpp b/lib/basic_cmds.cpp index e7eec649d..d05c69baa 100644 --- a/lib/basic_cmds.cpp +++ b/lib/basic_cmds.cpp @@ -258,6 +258,7 @@ protected: symbol m_global_decls; symbol m_numeral_as_real; symbol m_error_behavior; + symbol m_int_real_coercions; ini_params m_ini; bool is_builtin_option(symbol const & s) const { @@ -288,6 +289,7 @@ public: m_global_decls(":global-decls"), m_numeral_as_real(":numeral-as-real"), m_error_behavior(":error-behavior"), + m_int_real_coercions(":int-real-coercions"), m_ini(false) { params.register_params(m_ini); register_pp_params(m_ini); @@ -376,6 +378,9 @@ class set_option_cmd : public set_get_option_cmd { else if (m_option == m_numeral_as_real) { ctx.set_numeral_as_real(to_bool(value)); } + else if (m_option == m_int_real_coercions) { + ctx.m().enable_int_real_coercions(to_bool(value)); + } #ifdef Z3DEBUG else if (m_option == ":enable-assertions") { enable_assertions(to_bool(value)); @@ -536,6 +541,9 @@ public: print_string(ctx, "continued-execution"); } } + else if (opt == m_int_real_coercions) { + print_bool(ctx, ctx.m().int_real_coercions()); + } else { std::string iopt = smt_keyword2opt_name(opt); std::string r; diff --git a/lib/cmd_context.cpp b/lib/cmd_context.cpp index 6127a5351..333e53b3a 100644 --- a/lib/cmd_context.cpp +++ b/lib/cmd_context.cpp @@ -532,6 +532,8 @@ void cmd_context::init_manager() { m_manager = alloc(ast_manager, m_params.m_proof_mode, m_params.m_trace_stream); m_pmanager = alloc(pdecl_manager, *m_manager); init_manager_core(true); + if (m_params.m_smtlib2_compliant) + m_manager->enable_int_real_coercions(false); } void cmd_context::init_external_manager() { diff --git a/lib/front_end_params.h b/lib/front_end_params.h index 9c6c1af8c..d13c01076 100644 --- a/lib/front_end_params.h +++ b/lib/front_end_params.h @@ -95,8 +95,7 @@ struct front_end_params : public preprocessor_params, public spc_params, public #else m_auto_config(false), #endif -#if 1 - // #if defined(SMTCOMP) TODO: put it back after SMTCOMP +#if 0 m_smtlib2_compliant(true), #else m_smtlib2_compliant(false), From 5c0d82d555b2d9704b14ac847fd85e430bbf80af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Oct 2012 16:42:28 -0700 Subject: [PATCH 16/16] Updated Release notes Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 3 +++ 1 file changed, 3 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index af966c9a8..551bc3f16 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -27,6 +27,9 @@ Version 4.2 - Added Xor procedure to Z3Py. +- Z3 by default switches to an incremental solver when a Solver object is used to solve many queries. + In the this version, we switch back to the tactic framework if the incremental solver returns "unknown". + First source code release (October 2, 2012) ===========================================