diff --git a/CMakeLists.txt b/CMakeLists.txt index b25139c1b..7400f67e2 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -274,18 +274,6 @@ else() message(STATUS "Not using libgmp") endif() -################################################################################ -# FOCI2 support -################################################################################ -# FIXME: What is this? -option(USE_FOCI2 "Use FOCI2" OFF) -if (USE_FOCI2) - message(FATAL_ERROR "TODO") - message(STATUS "Using FOCI2") -else() - message(STATUS "Not using FOCI2") -endif() - ################################################################################ # OpenMP support ################################################################################ @@ -318,6 +306,23 @@ else() set(USE_OPENMP OFF CACHE BOOL "Use OpenMP" FORCE) endif() +################################################################################ +# API Log sync +################################################################################ +option(API_LOG_SYNC + "Use locking when logging Z3 API calls (experimental)" + OFF +) +if (API_LOG_SYNC) + if (NOT USE_OPENMP) + message(FATAL_ERROR "API_LOG_SYNC feature requires OpenMP") + endif() + list(APPEND Z3_COMPONENT_CXX_DEFINES "-DZ3_LOG_SYNC") + message(STATUS "Using API_LOG_SYNC") +else() + message(STATUS "Not using API_LOG_SYNC") +endif() + ################################################################################ # FP math ################################################################################ diff --git a/README-CMake.md b/README-CMake.md index abd2d3c87..5b3cdfd36 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -293,6 +293,7 @@ The following useful options can be passed to CMake whilst configuring. * ``ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built. Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target. * ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled. +* ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. diff --git a/contrib/cmake/src/interp/CMakeLists.txt b/contrib/cmake/src/interp/CMakeLists.txt index 949811b93..c3d8e3d5e 100644 --- a/contrib/cmake/src/interp/CMakeLists.txt +++ b/contrib/cmake/src/interp/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(interp SOURCES iz3base.cpp iz3checker.cpp - iz3foci.cpp iz3interp.cpp iz3mgr.cpp iz3pp.cpp diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 00c391fa7..e7e35817f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -96,8 +96,6 @@ VER_BUILD=None VER_REVISION=None PREFIX=sys.prefix GMP=False -FOCI2=False -FOCI2LIB='' VS_PAR=False VS_PAR_NUM=8 GPROF=False @@ -257,13 +255,6 @@ def test_gmp(cc): t.commit() return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0 -def test_foci2(cc,foci2lib): - if is_verbose(): - print("Testing FOCI2...") - t = TempFile('tstfoci2.cpp') - t.add('#include\nint main() { foci2 *f = foci2::create("lia"); return 0; }\n') - t.commit() - return exec_compiler_cmd([cc, CPPFLAGS, '-Isrc/interp', 'tstfoci2.cpp', LDFLAGS, foci2lib]) == 0 def test_openmp(cc): if not USE_OMP: @@ -650,7 +641,6 @@ def display_help(exit_code): if not IS_WINDOWS: print(" -g, --gmp use GMP.") print(" --gprof enable gprof") - print(" -f --foci2= use foci2 library at path") print(" --noomp disable OpenMP and all features that require it.") print(" --log-sync synchronize access to API log files to enable multi-thread API logging.") print("") @@ -678,13 +668,13 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED + global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, LOG_SYNC try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', - 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', + 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin', 'log-sync']) except: print("ERROR: Invalid command line option") @@ -735,9 +725,6 @@ def parse_options(): VS_PAR_NUM = int(arg) elif opt in ('-g', '--gmp'): GMP = True - elif opt in ('-f', '--foci2'): - FOCI2 = True - FOCI2LIB = arg elif opt in ('-j', '--java'): JAVA_ENABLED = True elif opt == '--gprof': @@ -778,7 +765,7 @@ def extract_c_includes(fname): root_file_name = m1.group(1) slash_pos = root_file_name.rfind('/') if slash_pos >= 0 and root_file_name.find("..") < 0 : #it is a hack for lp include files that behave as continued from "src" - print(root_file_name) + # print(root_file_name) root_file_name = root_file_name[slash_pos+1:] result.append(root_file_name) elif not system_inc_pat.match(line) and non_std_inc_pat.match(line): @@ -1181,7 +1168,6 @@ class ExeComponent(Component): for dep in deps: c_dep = get_component(dep) out.write(' ' + c_dep.get_link_name()) - out.write(' ' + FOCI2LIB) out.write(' $(LINK_EXTRA_FLAGS)\n') out.write('%s: %s\n\n' % (self.name, exefile)) @@ -1307,7 +1293,6 @@ class DLLComponent(Component): if dep not in self.reexports: c_dep = get_component(dep) out.write(' ' + c_dep.get_link_name()) - out.write(' ' + FOCI2LIB) out.write(' $(SLINK_EXTRA_FLAGS)') if IS_WINDOWS: out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name)) @@ -2307,7 +2292,7 @@ def mk_config(): if ONLY_MAKEFILES: return config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w') - global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, HAS_OMP, LOG_SYNC + global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, HAS_OMP, LOG_SYNC if IS_WINDOWS: config.write( 'CC=cl\n' @@ -2417,14 +2402,6 @@ def mk_config(): SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS else: CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS - if FOCI2: - if test_foci2(CXX,FOCI2LIB): - LDFLAGS = '%s %s' % (LDFLAGS,FOCI2LIB) - SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB) - CPPFLAGS = '%s -D_FOCI2' % CPPFLAGS - else: - print("FAILED\n") - FOCI2 = False if GIT_HASH: CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH) CXXFLAGS = '%s -std=c++11' % CXXFLAGS diff --git a/src/api/python/setup.py b/src/api/python/setup.py index ff3b0736d..24ba59ac2 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -164,6 +164,6 @@ setup( package_data={ 'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')] }, - scripts=[os.path.join('bin', EXECUTABLE_FILE)], + data_files=[('bin',[os.path.join('bin',EXECUTABLE_FILE)])], cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg}, ) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b4cdf834b..84a80ddf7 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1300,8 +1300,10 @@ class BoolSortRef(SortRef): if isinstance(val, bool): return BoolVal(val, self.ctx) if __debug__: - _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val) - _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value") + if not is_expr(val): + _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val) + if not self.eq(val.sort()): + _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value") return val def subsort(self, other): diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index f953dbf0e..3021b702b 100644 --- a/src/ast/ast_pp_util.cpp +++ b/src/ast/ast_pp_util.cpp @@ -44,8 +44,11 @@ void ast_pp_util::display_decls(std::ostream& out) { } n = coll.get_num_decls(); for (unsigned i = 0; i < n; ++i) { - ast_smt2_pp(out, coll.get_func_decls()[i], env); - out << "\n"; + func_decl* f = coll.get_func_decls()[i]; + if (f->get_family_id() == null_family_id) { + ast_smt2_pp(out, f, env); + out << "\n"; + } } } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index cf46badd6..dc1931bac 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -440,24 +440,16 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con * (seq.unit (_ BitVector 8)) ==> String constant */ br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) { - sort * s = m().get_sort(e); bv_util bvu(m()); - - if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) { - // specifically we want (_ BitVector 8) - rational n_val; - unsigned int n_size; - if (bvu.is_numeral(e, n_val, n_size)) { - if (n_size == 8) { - // convert to string constant - char ch = (char)n_val.get_int32(); - TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;); - char s_tmp[2] = {ch, '\0'}; - symbol s(s_tmp); - result = m_util.str.mk_string(s); - return BR_DONE; - } - } + rational n_val; + unsigned int n_size; + // specifically we want (_ BitVector 8) + if (bvu.is_bv(e) && bvu.is_numeral(e, n_val, n_size) && n_size == 8) { + // convert to string constant + zstring str(n_val.get_unsigned()); + TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;); + result = m_util.str.mk_string(str); + return BR_DONE; } return BR_FAILED; @@ -1431,37 +1423,10 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { } /* - * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn)) + * (re.range c_1 c_n) */ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { return BR_FAILED; - TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";); - zstring str_lo, str_hi; - if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) { - if (str_lo.length() == 1 && str_hi.length() == 1) { - unsigned int c1 = str_lo[0]; - unsigned int c2 = str_hi[0]; - if (c1 > c2) { - // exchange c1 and c2 - unsigned int tmp = c1; - c2 = c1; - c1 = tmp; - } - zstring s(c1); - expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m()); - for (unsigned int ch = c1 + 1; ch <= c2; ++ch) { - zstring s_ch(ch); - expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m()); - acc = m_util.re.mk_union(acc, acc2); - } - result = acc; - return BR_REWRITE2; - } else { - m().raise_exception("string constants in re.range must have length 1"); - } - } - - return BR_FAILED; } /* diff --git a/src/interp/foci2.h b/src/interp/foci2.h deleted file mode 100755 index bd968f11e..000000000 --- a/src/interp/foci2.h +++ /dev/null @@ -1,75 +0,0 @@ -/*++ - Copyright (c) 2011 Microsoft Corporation - - Module Name: - - foci2.h - - Abstract: - - An interface class for foci2. - - Author: - - Ken McMillan (kenmcmil) - - Revision History: - - --*/ - -#ifndef FOCI2_H -#define FOCI2_H - -#include -#include - -#ifdef _WINDOWS -#define FOCI2_EXPORT __declspec(dllexport) -#else -#define FOCI2_EXPORT __attribute__ ((visibility ("default"))) -#endif - -class foci2 { - public: - virtual ~foci2(){} - - typedef int ast; - typedef int symb; - - /** Built-in operators */ - enum ops { - And = 0, Or, Not, Iff, Ite, Equal, Plus, Times, Floor, Leq, Div, Bool, Int, Array, Tsym, Fsym, Forall, Exists, Distinct, LastOp - }; - - virtual symb mk_func(const std::string &s) = 0; - virtual symb mk_pred(const std::string &s) = 0; - virtual ast mk_op(ops op, const std::vector args) = 0; - virtual ast mk_op(ops op, ast) = 0; - virtual ast mk_op(ops op, ast, ast) = 0; - virtual ast mk_op(ops op, ast, ast, ast) = 0; - virtual ast mk_int(const std::string &) = 0; - virtual ast mk_rat(const std::string &) = 0; - virtual ast mk_true() = 0; - virtual ast mk_false() = 0; - virtual ast mk_app(symb,const std::vector args) = 0; - - virtual bool get_func(ast, symb &) = 0; - virtual bool get_pred(ast, symb &) = 0; - virtual bool get_op(ast, ops &) = 0; - virtual bool get_true(ast id) = 0; - virtual bool get_false(ast id) = 0; - virtual bool get_int(ast id, std::string &res) = 0; - virtual bool get_rat(ast id, std::string &res) = 0; - virtual const std::string &get_symb(symb) = 0; - - virtual int get_num_args(ast) = 0; - virtual ast get_arg(ast, int) = 0; - - virtual void show_ast(ast) = 0; - - virtual bool interpolate(const std::vector &frames, std::vector &itps, std::vector parents) = 0; - - FOCI2_EXPORT static foci2 *create(const std::string &); -}; - -#endif diff --git a/src/interp/foci2stub/foci2.cpp b/src/interp/foci2stub/foci2.cpp deleted file mode 100644 index 31908855b..000000000 --- a/src/interp/foci2stub/foci2.cpp +++ /dev/null @@ -1,25 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - foci2.cpp - -Abstract: - - Fake foci2, to be replaced - -Author: - - Ken McMillan (kenmcmil) - -Revision History: - ---*/ - - -#include "foci2.h" - -FOCI2_EXPORT foci2 *foci2::create(const std::string &){ - return 0; -} diff --git a/src/interp/foci2stub/foci2.h b/src/interp/foci2stub/foci2.h deleted file mode 100755 index 261dd05dc..000000000 --- a/src/interp/foci2stub/foci2.h +++ /dev/null @@ -1,75 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - foci2.h - -Abstract: - - An interface class for foci2. - -Author: - - Ken McMillan (kenmcmil) - -Revision History: - ---*/ - -#ifndef FOCI2_H -#define FOCI2_H - -#include -#include - -#ifdef WIN32 -#define FOCI2_EXPORT __declspec(dllexport) -#else -#define FOCI2_EXPORT __attribute__ ((visibility ("default"))) -#endif - -class foci2 { - public: - virtual ~foci2(){} - - typedef int ast; - typedef int symb; - - /** Built-in operators */ - enum ops { - And = 0, Or, Not, Iff, Ite, Equal, Plus, Times, Floor, Leq, Div, Bool, Int, Array, Tsym, Fsym, Forall, Exists, Distinct, LastOp - }; - - virtual symb mk_func(const std::string &s) = 0; - virtual symb mk_pred(const std::string &s) = 0; - virtual ast mk_op(ops op, const std::vector args) = 0; - virtual ast mk_op(ops op, ast) = 0; - virtual ast mk_op(ops op, ast, ast) = 0; - virtual ast mk_op(ops op, ast, ast, ast) = 0; - virtual ast mk_int(const std::string &) = 0; - virtual ast mk_rat(const std::string &) = 0; - virtual ast mk_true() = 0; - virtual ast mk_false() = 0; - virtual ast mk_app(symb,const std::vector args) = 0; - - virtual bool get_func(ast, symb &) = 0; - virtual bool get_pred(ast, symb &) = 0; - virtual bool get_op(ast, ops &) = 0; - virtual bool get_true(ast id) = 0; - virtual bool get_false(ast id) = 0; - virtual bool get_int(ast id, std::string &res) = 0; - virtual bool get_rat(ast id, std::string &res) = 0; - virtual const std::string &get_symb(symb) = 0; - - virtual int get_num_args(ast) = 0; - virtual ast get_arg(ast, int) = 0; - - virtual void show_ast(ast) = 0; - - virtual bool interpolate(const std::vector &frames, std::vector &itps, std::vector parents) = 0; - - FOCI2_EXPORT static foci2 *create(const std::string &); -}; - -#endif diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp deleted file mode 100755 index 3a873de2c..000000000 --- a/src/interp/iz3foci.cpp +++ /dev/null @@ -1,356 +0,0 @@ -/*++ - Copyright (c) 2011 Microsoft Corporation - - Module Name: - - iz3foci.cpp - - Abstract: - - Implements a secondary solver using foci2. - - Author: - - Ken McMillan (kenmcmil) - - Revision History: - - --*/ - -#include -#include - -#include "iz3hash.h" -#include "foci2.h" -#include "iz3foci.h" - -using namespace stl_ext; - -class iz3foci_impl : public iz3secondary { - - int frames; - int *parents; - foci2 *foci; - foci2::symb select_op; - foci2::symb store_op; - foci2::symb mod_op; - -public: - iz3foci_impl(iz3mgr *mgr, int _frames, int *_parents) : iz3secondary(*mgr) { - frames = _frames; - parents = _parents; - foci = 0; - } - - typedef hash_map AstToNode; - AstToNode ast_to_node; // maps Z3 ast's to foci expressions - - typedef hash_map NodeToAst; - NodeToAst node_to_ast; // maps Z3 ast's to foci expressions - - // We only use this for FuncDeclToSymbol, which has no range destructor - struct symb_hash { - size_t operator()(const symb &s) const { - return (size_t) s; - } - }; - - typedef hash_map FuncDeclToSymbol; - FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols - - typedef hash_map SymbolToFuncDecl; - SymbolToFuncDecl symbol_to_func_decl; // maps symbols to Z3 func decls - - int from_symb(symb func){ - std::string name = string_of_symbol(func); - bool is_bool = is_bool_type(get_range_type(func)); - foci2::symb f; - if(is_bool) - f = foci->mk_pred(name); - else - f = foci->mk_func(name); - symbol_to_func_decl[f] = func; - func_decl_to_symbol[func] = f; - return f; - } - - // create a symbol corresponding to a DeBruijn index of a particular type - // the type has to be encoded into the name because the same index can - // occur with different types - foci2::symb make_deBruijn_symbol(int index, type ty){ - std::ostringstream s; - // s << "#" << index << "#" << type; - return foci->mk_func(s.str()); - } - - int from_Z3_ast(ast t){ - std::pair foo(t,0); - std::pair bar = ast_to_node.insert(foo); - int &res = bar.first->second; - if(!bar.second) return res; - int nargs = num_args(t); - std::vector args(nargs); - for(int i = 0; i < nargs; i++) - args[i] = from_Z3_ast(arg(t,i)); - - switch(op(t)){ - case True: - res = foci->mk_true(); break; - case False: - res = foci->mk_false(); break; - case And: - res = foci->mk_op(foci2::And,args); break; - case Or: - res = foci->mk_op(foci2::Or,args); break; - case Not: - res = foci->mk_op(foci2::Not,args[0]); break; - case Iff: - res = foci->mk_op(foci2::Iff,args); break; - case OP_OEQ: // bit of a mystery, this one... - if(args[0] == args[1]) res = foci->mk_true(); - else res = foci->mk_op(foci2::Iff,args); - break; - case Ite: - if(is_bool_type(get_type(t))) - res = foci->mk_op(foci2::And,foci->mk_op(foci2::Or,foci->mk_op(foci2::Not,args[0]),args[1]),foci->mk_op(foci2::Or,args[0],args[2])); - else - res = foci->mk_op(foci2::Ite,args); - break; - case Equal: - res = foci->mk_op(foci2::Equal,args); break; - case Implies: - args[0] = foci->mk_op(foci2::Not,args[0]); res = foci->mk_op(foci2::Or,args); break; - case Xor: - res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Iff,args)); break; - case Leq: - res = foci->mk_op(foci2::Leq,args); break; - case Geq: - std::swap(args[0],args[1]); res = foci->mk_op(foci2::Leq,args); break; - case Gt: - res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break; - case Lt: - std::swap(args[0],args[1]); res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break; - case Plus: - res = foci->mk_op(foci2::Plus,args); break; - case Sub: - args[1] = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[1]); res = foci->mk_op(foci2::Plus,args); break; - case Uminus: - res = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[0]); break; - case Times: - res = foci->mk_op(foci2::Times,args); break; - case Idiv: - res = foci->mk_op(foci2::Div,args); break; - case Mod: - res = foci->mk_app(mod_op,args); break; - case Select: - res = foci->mk_app(select_op,args); break; - case Store: - res = foci->mk_app(store_op,args); break; - case Distinct: - res = foci->mk_op(foci2::Distinct,args); break; - case Uninterpreted: { - symb func = sym(t); - FuncDeclToSymbol::iterator it = func_decl_to_symbol.find(func); - foci2::symb f = (it == func_decl_to_symbol.end()) ? from_symb(func) : it->second; - if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==1) // HACK to handle Z3 labels - res = args[0]; - else if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==0) // HACK to handle Z3 labels - res = foci->mk_true(); - else res = foci->mk_app(f,args); - break; - } - case Numeral: { - std::string s = string_of_numeral(t); - res = foci->mk_int(s); - break; - } - case Forall: - case Exists: { - bool is_forall = op(t) == Forall; - foci2::ops qop = is_forall ? foci2::Forall : foci2::Exists; - int bvs = get_quantifier_num_bound(t); - std::vector foci_bvs(bvs); - for(int i = 0; i < bvs; i++){ - std::string name = get_quantifier_bound_name(t,i); - //Z3_string name = Z3_get_symbol_string(ctx,sym); - // type ty = get_quantifier_bound_type(t,i); - foci2::symb f = foci->mk_func(name); - foci2::ast v = foci->mk_app(f,std::vector()); - foci_bvs[i] = v; - } - foci2::ast body = from_Z3_ast(get_quantifier_body(t)); - foci_bvs.push_back(body); - res = foci->mk_op(qop,foci_bvs); - node_to_ast[res] = t; // desperate - break; - } - case Variable: { // a deBruijn index - int index = get_variable_index_value(t); - type ty = get_type(t); - foci2::symb symbol = make_deBruijn_symbol(index,ty); - res = foci->mk_app(symbol,std::vector()); - break; - } - default: - { - std::cerr << "iZ3: unsupported Z3 operator in expression\n "; - print_expr(std::cerr,t); - std::cerr << "\n"; - SASSERT(0 && "iZ3: unsupported Z3 operator"); - } - } - return res; - } - - // convert an expr to Z3 ast - ast to_Z3_ast(foci2::ast i){ - std::pair foo(i,ast()); - std::pair bar = node_to_ast.insert(foo); - if(!bar.second) return bar.first->second; - ast &res = bar.first->second; - - if(i < 0){ - res = mk_not(to_Z3_ast(-i)); - return res; - } - - // get the arguments - unsigned n = foci->get_num_args(i); - std::vector args(n); - for(unsigned j = 0; j < n; j++) - args[j] = to_Z3_ast(foci->get_arg(i,j)); - - // handle operators - foci2::ops o; - foci2::symb f; - std::string nval; - if(foci->get_true(i)) - res = mk_true(); - else if(foci->get_false(i)) - res = mk_false(); - else if(foci->get_op(i,o)){ - switch(o){ - case foci2::And: - res = make(And,args); break; - case foci2::Or: - res = make(Or,args); break; - case foci2::Not: - res = mk_not(args[0]); break; - case foci2::Iff: - res = make(Iff,args[0],args[1]); break; - case foci2::Ite: - res = make(Ite,args[0],args[1],args[2]); break; - case foci2::Equal: - res = make(Equal,args[0],args[1]); break; - case foci2::Plus: - res = make(Plus,args); break; - case foci2::Times: - res = make(Times,args); break; - case foci2::Div: - res = make(Idiv,args[0],args[1]); break; - case foci2::Leq: - res = make(Leq,args[0],args[1]); break; - case foci2::Distinct: - res = make(Distinct,args); - break; - case foci2::Tsym: - res = mk_true(); - break; - case foci2::Fsym: - res = mk_false(); - break; - case foci2::Forall: - case foci2::Exists: - { - int nargs = n; - std::vector bounds(nargs-1); - for(int i = 0; i < nargs-1; i++) - bounds[i] = args[i]; - opr oz = o == foci2::Forall ? Forall : Exists; - res = make_quant(oz,bounds,args[nargs-1]); - } - break; - default: - SASSERT(false && "unknown built-in op"); - } - } - else if(foci->get_int(i,nval)){ - res = make_int(nval); - } - else if(foci->get_func(i,f)){ - if(f == select_op){ - SASSERT(n == 2); - res = make(Select,args[0],args[1]); - } - else if(f == store_op){ - SASSERT(n == 3); - res = make(Store,args[0],args[1],args[2]); - } - else if(f == mod_op){ - SASSERT(n == 2); - res = make(Mod,args[0],args[1]); - } - else { - std::pair foo(f,(symb)0); - std::pair bar = symbol_to_func_decl.insert(foo); - symb &func_decl = bar.first->second; - if(bar.second){ - std::cout << "unknown function symbol:\n"; - foci->show_ast(i); - SASSERT(0); - } - res = make(func_decl,args); - } - } - else { - std::cerr << "iZ3: unknown FOCI expression kind\n"; - SASSERT(0 && "iZ3: unknown FOCI expression kind"); - } - return res; - } - - int interpolate(const std::vector &cnsts, std::vector &itps){ - SASSERT((int)cnsts.size() == frames); - std::string lia("lia"); -#ifdef _FOCI2 - foci = foci2::create(lia); -#else - foci = 0; -#endif - if(!foci){ - std::cerr << "iZ3: cannot find foci lia solver.\n"; - SASSERT(0); - } - select_op = foci->mk_func("select"); - store_op = foci->mk_func("store"); - mod_op = foci->mk_func("mod"); - std::vector foci_cnsts(frames), foci_itps(frames-1), foci_parents; - if(parents) - foci_parents.resize(frames); - for(int i = 0; i < frames; i++){ - foci_cnsts[i] = from_Z3_ast(cnsts[i]); - if(parents) - foci_parents[i] = parents[i]; - } - int res = foci->interpolate(foci_cnsts, foci_itps, foci_parents); - if(res == 0){ - SASSERT((int)foci_itps.size() == frames-1); - itps.resize(frames-1); - for(int i = 0; i < frames-1; i++){ - // foci->show_ast(foci_itps[i]); - itps[i] = to_Z3_ast(foci_itps[i]); - } - } - ast_to_node.clear(); - node_to_ast.clear(); - func_decl_to_symbol.clear(); - symbol_to_func_decl.clear(); - delete foci; - return res; - } - -}; - -iz3secondary *iz3foci::create(iz3mgr *mgr, int num, int *parents){ - return new iz3foci_impl(mgr,num,parents); -} diff --git a/src/interp/iz3foci.h b/src/interp/iz3foci.h deleted file mode 100755 index a84a3c3bf..000000000 --- a/src/interp/iz3foci.h +++ /dev/null @@ -1,32 +0,0 @@ -/*++ - Copyright (c) 2011 Microsoft Corporation - - Module Name: - - iz3foci.h - - Abstract: - - Implements a secondary solver using foci2. - - Author: - - Ken McMillan (kenmcmil) - - Revision History: - - --*/ - -#ifndef IZ3FOCI_H -#define IZ3FOCI_H - -#include "iz3secondary.h" - -/** Secondary prover based on Cadence FOCI. */ - -class iz3foci { - public: - static iz3secondary *create(iz3mgr *mgr, int num, int *parents); -}; - -#endif diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 87f782160..bb83349da 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -35,7 +35,6 @@ #include "iz3profiling.h" #include "iz3translate.h" -#include "iz3foci.h" #include "iz3proof.h" #include "iz3hash.h" #include "iz3interp.h" @@ -167,22 +166,6 @@ struct frame_reducer { #endif -#if 0 -static lbool test_secondary(context ctx, - int num, - ast *cnsts, - ast *interps, - int *parents = 0 - ){ - iz3secondary *sp = iz3foci::create(ctx,num,parents); - std::vector frames(num), interpolants(num-1); - std::copy(cnsts,cnsts+num,frames.begin()); - int res = sp->interpolate(frames,interpolants); - if(res == 0) - std::copy(interpolants.begin(),interpolants.end(),interps); - return res ? L_TRUE : L_FALSE; -} -#endif template struct killme { @@ -213,11 +196,7 @@ public: const std::vector &parents, std::vector &interps ){ - int num = cnsts.size(); - iz3secondary *sp = iz3foci::create(this,num,(int *)(parents.empty()?0:&parents[0])); - int res = sp->interpolate(cnsts, interps); - if(res != 0) - throw iz3_exception("secondary failed"); + throw iz3_exception("secondary interpolating prover not supported"); } void proof_to_interpolant(z3pf proof, @@ -248,10 +227,9 @@ public: if(is_linear(parents_vec)) parents_vec.clear(); - // create a secondary prover - iz3secondary *sp = iz3foci::create(this,num,parents_vec.empty()?0:&parents_vec[0]); - sp_killer.set(sp); // kill this on exit - + // secondary prover no longer supported + iz3secondary *sp = NULL; + #define BINARY_INTERPOLATION #ifndef BINARY_INTERPOLATION // create a translator diff --git a/src/interp/iz3translate.h b/src/interp/iz3translate.h index 86b0b3d2d..15e836cd8 100755 --- a/src/interp/iz3translate.h +++ b/src/interp/iz3translate.h @@ -53,12 +53,8 @@ class iz3translation : public iz3base { : iz3base(mgr,_cnsts,_parents,_theory) {} }; -//#define IZ3_TRANSLATE_DIRECT2 -#ifdef _FOCI2 -#define IZ3_TRANSLATE_DIRECT -#else +// To use a secondary prover, define IZ3_TRANSLATE_DIRECT instead of this #define IZ3_TRANSLATE_FULL -#endif #endif diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 95d66f617..de1da6ce6 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -332,7 +332,7 @@ public: } } - // get the lits of a Z3 clause as foci terms + // get the lits of a Z3 clause as secondary prover terms void get_Z3_lits(ast t, std::vector &lits){ opr dk = op(t); if(dk == False) @@ -666,9 +666,9 @@ public: #endif // interpolate using secondary prover - profiling::timer_start("foci"); + profiling::timer_start("secondary prover"); int sat = secondary->interpolate(preds,itps); - profiling::timer_stop("foci"); + profiling::timer_stop("secondary prover"); std::cout << "lemma done" << std::endl; @@ -1495,7 +1495,7 @@ public: return find_nll(new_proofs); } - // translate a Z3 proof term into a foci proof term + // translate a Z3 proof term into a secondary prover proof term Iproof::node translate_main(ast proof, non_local_lits *nll, bool expect_clause = true){ non_local_lits *old_nll = nll; diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 619f88e3b..518e848c4 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -50,7 +50,8 @@ void rule_properties::collect(rule_set const& rules) { } for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) { sort* d = r->get_decl()->get_domain(i); - if (!m.is_bool(d) && !m_dl.is_finite_sort(d) && !m_bv.is_bv_sort(d)) { + sort_size sz = d->get_num_elements(); + if (!sz.is_finite()) { m_inf_sort.push_back(m_rule); } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 7a9369fd3..3f8845546 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2176,6 +2176,8 @@ bool theory_seq::simplify_and_solve_eqs() { return m_new_propagation || ctx.inconsistent(); } +void theory_seq::internalize_eq_eh(app * atom, bool_var v) {} + bool theory_seq::internalize_term(app* term) { context & ctx = get_context(); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 2b8fb2fd7..e145d3077 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -343,7 +343,7 @@ namespace smt { virtual final_check_status final_check_eh(); virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); } virtual bool internalize_term(app*); - virtual void internalize_eq_eh(app * atom, bool_var v) {} + virtual void internalize_eq_eh(app * atom, bool_var v); virtual void new_eq_eh(theory_var, theory_var); virtual void new_diseq_eh(theory_var, theory_var); virtual void assign_eh(bool_var v, bool is_true); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 8b94ec967..63f0a88bd 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -60,6 +60,7 @@ namespace smt { totalCacheAccessCount(0), cacheHitCount(0), cacheMissCount(0), + m_fresh_id(0), m_find(*this), m_trail_stack(*this) { @@ -441,7 +442,12 @@ namespace smt { } app * theory_str::mk_fresh_const(char const* name, sort* s) { - return u.mk_skolem(symbol(name), 0, 0, s); + string_buffer<64> buffer; + buffer << name; + buffer << "!tmp"; + buffer << m_fresh_id; + m_fresh_id++; + return u.mk_skolem(symbol(buffer.c_str()), 0, 0, s); } @@ -5908,8 +5914,14 @@ namespace smt { app * n2_curr = to_app(n2); // case 0: n1_curr is const string, n2_curr is const string - if (u.str.is_string(n1_curr) && u.str.is_string(n2_curr)) { - if (n1_curr != n2_curr) { + zstring n1_curr_str, n2_curr_str; + if (u.str.is_string(n1_curr, n1_curr_str) && u.str.is_string(n2_curr, n2_curr_str)) { + TRACE("str", tout << "checking string constants: n1=" << n1_curr_str << ", n2=" << n2_curr_str << std::endl;); + if (n1_curr_str == n2_curr_str) { + // TODO(mtrberzi) potential correction: if n1_curr != n2_curr, + // assert that these two terms are in fact equal, because they ought to be + return true; + } else { return false; } } @@ -6864,7 +6876,7 @@ namespace smt { // easiest case. we will search within these bounds } else if (upper_bound_exists && !lower_bound_exists) { // search between 0 and the upper bound - v_lower_bound == rational::zero(); + v_lower_bound = rational::zero(); } else if (lower_bound_exists && !upper_bound_exists) { // check some finite portion of the search space v_upper_bound = v_lower_bound + rational(10); @@ -9227,7 +9239,7 @@ namespace smt { ); // ---------------------------------------------------------------------------------------- - + ptr_vector orList; ptr_vector andList; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 0403b0623..4752e8a1b 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -350,6 +350,8 @@ protected: unsigned long cacheHitCount; unsigned long cacheMissCount; + unsigned m_fresh_id; + // cache mapping each string S to Length(S) obj_map length_ast_map; diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index e2b1eb682..b74515566 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -34,25 +34,24 @@ namespace lean { class lar_solver : public column_namer { //////////////////// fields ////////////////////////// - lp_settings m_settings; - stacked_value m_status; - stacked_value m_simplex_strategy; + lp_settings m_settings; + stacked_value m_status; + stacked_value m_simplex_strategy; std::unordered_map m_ext_vars_to_columns; - vector m_columns_to_ext_vars_or_term_indices; - stacked_vector m_vars_to_ul_pairs; - vector m_constraints; - stacked_value m_constraint_count; + vector m_columns_to_ext_vars_or_term_indices; + stacked_vector m_vars_to_ul_pairs; + vector m_constraints; + stacked_value m_constraint_count; // the set of column indices j such that bounds have changed for j - int_set m_columns_with_changed_bound; - int_set m_rows_with_changed_bounds; - int_set m_basic_columns_with_changed_cost; - stacked_value m_infeasible_column_index; // such can be found at the initialization step - stacked_value m_term_count; - vector m_terms; - vector m_orig_terms; - const var_index m_terms_start_index; - indexed_vector m_column_buffer; - std::function m_column_type_function; + int_set m_columns_with_changed_bound; + int_set m_rows_with_changed_bounds; + int_set m_basic_columns_with_changed_cost; + stacked_value m_infeasible_column_index; // such can be found at the initialization step + stacked_value m_term_count; + vector m_terms; + vector m_orig_terms; + const var_index m_terms_start_index; + indexed_vector m_column_buffer; public: lar_core_solver m_mpq_lar_core_solver; unsigned constraint_count() const { @@ -83,7 +82,6 @@ public: lar_solver() : m_status(OPTIMAL), m_infeasible_column_index(-1), m_terms_start_index(1000000), - m_column_type_function ([this] (unsigned j) {return m_mpq_lar_core_solver.m_column_types()[j];}), m_mpq_lar_core_solver(m_settings, *this) {} diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h index 4c08ec8e6..4c793d56e 100644 --- a/src/util/lp/mps_reader.h +++ b/src/util/lp/mps_reader.h @@ -651,11 +651,11 @@ class mps_reader { /* If rhs is a constraint's right-hand-side value and range is the constraint's range value, then the range interval is defined according to the following table: - sense interval G [rhs, rhs + |range|] L [rhs - |range|, rhs] - E [rhs, rhs + |range|] if range ¡Ý 0 [rhs - |range|, rhs] if range < 0 + E [rhs, rhs + |range|] if range > 0, + [rhs - |range|, rhs] if range < 0 where |range| is range's absolute value. */ diff --git a/src/util/mpz.h b/src/util/mpz.h index 2661cb5da..67947b602 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -497,7 +497,9 @@ public: STRACE("mpz", tout << "[mpz] 0 - " << to_string(a) << " == ";); if (is_small(a) && a.m_val == INT_MIN) { // neg(INT_MIN) is not a small int + MPZ_BEGIN_CRITICAL(); set_big_i64(a, - static_cast(INT_MIN)); + MPZ_END_CRITICAL(); return; } #ifndef _MP_GMP @@ -518,7 +520,9 @@ public: if (a.m_val < 0) { if (a.m_val == INT_MIN) { // abs(INT_MIN) is not a small int + MPZ_BEGIN_CRITICAL(); set_big_i64(a, - static_cast(INT_MIN)); + MPZ_END_CRITICAL(); } else a.m_val = -a.m_val; diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp index 60c85b660..ac2f64482 100644 --- a/src/util/small_object_allocator.cpp +++ b/src/util/small_object_allocator.cpp @@ -68,6 +68,7 @@ void small_object_allocator::reset() { #define MASK ((1 << PTR_ALIGNMENT) - 1) + void small_object_allocator::deallocate(size_t size, void * p) { if (size == 0) return; @@ -92,6 +93,7 @@ void small_object_allocator::deallocate(size_t size, void * p) { m_free_list[slot_id] = p; } + void * small_object_allocator::allocate(size_t size) { if (size == 0) return 0; @@ -100,8 +102,9 @@ void * small_object_allocator::allocate(size_t size) { return memory::allocate(size); #endif m_alloc_size += size; - if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) + if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) { return memory::allocate(size); + } #ifdef Z3DEBUG size_t osize = size; #endif