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..1b7d89542 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -1,4 +1,4 @@ - # Z3's CMake build system +# Z3's CMake build system [CMake](https://cmake.org/) is a "meta build system" that reads a description of the project written in the ``CMakeLists.txt`` files and emits a build @@ -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/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt index 74fddd2bb..abf09ff0c 100644 --- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt +++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt @@ -8,6 +8,7 @@ z3_add_component(rewriter bv_rewriter.cpp datatype_rewriter.cpp der.cpp + distribute_forall.cpp dl_rewriter.cpp enum2bv_rewriter.cpp expr_replacer.cpp diff --git a/contrib/cmake/src/ast/simplifier/CMakeLists.txt b/contrib/cmake/src/ast/simplifier/CMakeLists.txt index 7597374a6..9575c5c89 100644 --- a/contrib/cmake/src/ast/simplifier/CMakeLists.txt +++ b/contrib/cmake/src/ast/simplifier/CMakeLists.txt @@ -10,7 +10,6 @@ z3_add_component(simplifier bv_simplifier_params.cpp bv_simplifier_plugin.cpp datatype_simplifier_plugin.cpp - distribute_forall.cpp elim_bounds.cpp fpa_simplifier_plugin.cpp inj_axiom.cpp 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 112e1f5ad..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': @@ -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/api_ast.cpp b/src/api/api_ast.cpp index c9cdc6ab3..3cec4ec02 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1124,6 +1124,20 @@ extern "C" { case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; + case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE; + case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT; + case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH; + case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS; + case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX; + case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX; + case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE; + case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE; + case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT; + case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT; + case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX; + case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET; + case _OP_REGEXP_FULL: return Z3_OP_RE_FULL_SET; + case OP_STRING_STOI: return Z3_OP_STR_TO_INT; case OP_STRING_ITOS: return Z3_OP_INT_TO_STR; diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index cac62d2f0..23ffe61bd 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -797,6 +797,22 @@ namespace Microsoft.Z3 public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } } #endregion + #region Sequences and Strings + + /// + /// Check whether expression is a string constant. + /// + /// a Boolean + public bool IsString { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } } + + /// + /// Retrieve string corresponding to string constant. + /// + /// the expression should be a string constant, (IsString should be true). + public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } } + + #endregion + #region Proof Terms /// /// Indicates whether the term is a binary equivalence modulo namings. diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index a7f62e6e8..12992fa8a 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -19,6 +19,7 @@ Notes: using System; using System.Diagnostics.Contracts; +using System.Collections.Generic; namespace Microsoft.Z3 { @@ -131,6 +132,24 @@ namespace Microsoft.Z3 } } + /// + /// Enumerate constants in model. + /// + public IEnumerable> Consts + { + get + { + uint nc = NumConsts; + for (uint i = 0; i < nc; ++i) + { + var f = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i)); + IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); + if (n == IntPtr.Zero) continue; + yield return new KeyValuePair(f, Expr.Create(Context, n)); + } + } + } + /// /// The number of function interpretations in the model. /// diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index ea3fd2147..71a2e3e1e 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -126,7 +126,7 @@ public class Expr extends AST if (isApp() && args.length != getNumArgs()) { throw new Z3Exception("Number of arguments does not match"); } - return new Expr(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(), + return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(), args.length, Expr.arrayToNative(args))); } @@ -1277,6 +1277,26 @@ public class Expr extends AST return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT; } + /** + * Check whether expression is a string constant. + * @return a boolean + */ + public boolean isString() + { + return isApp() && Native.isString(getContext().nCtx(), getNativeObject()); + } + + /** + * Retrieve string corresponding to string constant. + * Remark: the expression should be a string constant, (isString() should return true). + * @throws Z3Exception on error + * @return a string + */ + public String getString() + { + return Native.getString(getContext().nCtx(), getNativeObject()); + } + /** * Indicates whether the term is a binary equivalence modulo namings. * Remarks: This binary predicate is used in proof terms. It captures diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b86e9a797..dbd8019c4 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1304,8 +1304,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/api/z3_api.h b/src/api/z3_api.h index 45065f856..93da0b2c7 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5349,6 +5349,10 @@ extern "C" { /** \brief Add a new formula \c a to the given goal. + Conjunctions are split into separate formulas. + If the goal is \c false, adding new formulas is a no-op. + If the formula \c a is \c true, then nothing is added. + If the formula \c a is \c false, then the entire goal is replaced by the formula \c false. def_API('Z3_goal_assert', VOID, (_in(CONTEXT), _in(GOAL), _in(AST))) */ 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/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 8ad33d6fc..4d531d2db 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -935,9 +935,9 @@ bool datatype_util::is_recursive(sort * ty) { bool datatype_util::is_enum_sort(sort* s) { - if (!is_datatype(s)) { - return false; - } + if (!is_datatype(s)) { + return false; + } bool r = false; if (m_is_enum.find(s, r)) return r; diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 725c0b043..32b62342b 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -143,11 +143,11 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE; diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index 09f020ca6..28f889739 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -91,7 +91,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p } void pb_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - if (logic == symbol::null || logic == "QF_FD") { + if (logic == symbol::null || logic == "QF_FD" || logic == "ALL") { op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K)); op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K)); op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE)); diff --git a/src/ast/simplifier/distribute_forall.cpp b/src/ast/rewriter/distribute_forall.cpp similarity index 92% rename from src/ast/simplifier/distribute_forall.cpp rename to src/ast/rewriter/distribute_forall.cpp index 78e5d5ded..c64c0f089 100644 --- a/src/ast/simplifier/distribute_forall.cpp +++ b/src/ast/rewriter/distribute_forall.cpp @@ -20,12 +20,12 @@ Revision History: --*/ #include"var_subst.h" #include"ast_ll_pp.h" - +#include"ast_util.h" #include"distribute_forall.h" +#include"bool_rewriter.h" -distribute_forall::distribute_forall(ast_manager & m, basic_simplifier_plugin & p) : +distribute_forall::distribute_forall(ast_manager & m) : m_manager(m), - m_bsimp(p), m_cache(m) { } @@ -109,6 +109,8 @@ void distribute_forall::reduce1_quantifier(quantifier * q) { expr * e = get_cached(q->get_expr()); if (m_manager.is_not(e) && m_manager.is_or(to_app(e)->get_arg(0))) { + bool_rewriter br(m_manager); + // found target for simplification // (forall X (not (or F1 ... Fn))) // --> @@ -121,8 +123,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) { for (unsigned i = 0; i < num_args; i++) { expr * arg = or_e->get_arg(i); expr_ref not_arg(m_manager); - // m_bsimp.mk_not applies basic simplifications. For example, if arg is of the form (not a), then it will return a. - m_bsimp.mk_not(arg, not_arg); + br.mk_not(arg, not_arg); quantifier_ref tmp_q(m_manager); tmp_q = m_manager.update_quantifier(q, not_arg); expr_ref new_q(m_manager); @@ -132,7 +133,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) { expr_ref result(m_manager); // m_bsimp.mk_and actually constructs a (not (or ...)) formula, // it will also apply basic simplifications. - m_bsimp.mk_and(new_args.size(), new_args.c_ptr(), result); + br.mk_and(new_args.size(), new_args.c_ptr(), result); cache_result(q, result); } else { diff --git a/src/ast/simplifier/distribute_forall.h b/src/ast/rewriter/distribute_forall.h similarity index 90% rename from src/ast/simplifier/distribute_forall.h rename to src/ast/rewriter/distribute_forall.h index 4c2eefb56..b2c239239 100644 --- a/src/ast/simplifier/distribute_forall.h +++ b/src/ast/rewriter/distribute_forall.h @@ -22,7 +22,6 @@ Revision History: #define DISTRIBUTE_FORALL_H_ #include"ast.h" -#include"basic_simplifier_plugin.h" #include"act_cache.h" /** @@ -47,7 +46,6 @@ Revision History: class distribute_forall { typedef act_cache expr_map; ast_manager & m_manager; - basic_simplifier_plugin & m_bsimp; // useful for constructing formulas and/or/not in simplified form. ptr_vector m_todo; expr_map m_cache; ptr_vector m_new_args; @@ -57,7 +55,7 @@ class distribute_forall { public: - distribute_forall(ast_manager & m, basic_simplifier_plugin & p); + distribute_forall(ast_manager & m); /** \brief Apply the distribute_forall transformation (when possible) to all universal quantifiers in \c f. diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index dc1931bac..ce707b108 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -92,25 +92,25 @@ public: expr_ref fml(m.mk_true(), m); return sym_expr::mk_pred(fml, m.mk_bool_sort()); } - virtual T mk_and(T x, T y) { - if (x->is_char() && y->is_char()) { - if (x->get_char() == y->get_char()) { - return x; - } - if (m.are_distinct(x->get_char(), y->get_char())) { - expr_ref fml(m.mk_false(), m); - return sym_expr::mk_pred(fml, x->get_sort()); - } - } + virtual T mk_and(T x, T y) { + if (x->is_char() && y->is_char()) { + if (x->get_char() == y->get_char()) { + return x; + } + if (m.are_distinct(x->get_char(), y->get_char())) { + expr_ref fml(m.mk_false(), m); + return sym_expr::mk_pred(fml, x->get_sort()); + } + } - sort* s = x->get_sort(); - if (m.is_bool(s)) s = y->get_sort(); - var_ref v(m.mk_var(0, s), m); - expr_ref fml1 = x->accept(v); - expr_ref fml2 = y->accept(v); - if (m.is_true(fml1)) { - return y; - } + sort* s = x->get_sort(); + if (m.is_bool(s)) s = y->get_sort(); + var_ref v(m.mk_var(0, s), m); + expr_ref fml1 = x->accept(v); + expr_ref fml2 = y->accept(v); + if (m.is_true(fml1)) { + return y; + } if (m.is_true(fml2)) return x; expr_ref fml(m.mk_and(fml1, fml2), m); return sym_expr::mk_pred(fml, x->get_sort()); @@ -178,10 +178,10 @@ public: return sym_expr::mk_pred(fml, x->get_sort()); } - /*virtual vector, T>> generate_min_terms(vector constraints){ - - return 0; - }*/ + /*virtual vector, T>> generate_min_terms(vector constraints){ + + return 0; + }*/ }; re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {} diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index daf20e095..a3ad7fd07 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -391,7 +391,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite if (is_marked(e)) { m_num_sharing++; return; - } + } if (stack_depth > m_max_stack_depth) { return; } diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index f09d35158..a098f3c94 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -250,7 +250,7 @@ ATOMIC_CMD(get_assertions_cmd, "get-assertions", "retrieve asserted terms when i -ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions();); +ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions(); ctx.print_success();); UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", CPK_SYMBOL, symbol const &, if (ctx.set_logic(arg)) @@ -622,7 +622,7 @@ public: m_status(":status"), m_reason_unknown(":reason-unknown"), m_all_statistics(":all-statistics"), - m_assertion_stack_levels("assertion-stack-levels") { + m_assertion_stack_levels(":assertion-stack-levels") { } virtual char const * get_usage() const { return ""; } virtual char const * get_descr(cmd_context & ctx) const { return "get information."; } @@ -652,7 +652,7 @@ public: ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl; } else if (opt == m_reason_unknown) { - ctx.regular_stream() << "(:reason-unknown \"" << ctx.reason_unknown() << "\")" << std::endl; + ctx.regular_stream() << "(:reason-unknown \"" << escaped(ctx.reason_unknown().c_str()) << "\")" << std::endl; } else if (opt == m_all_statistics) { ctx.display_statistics(); @@ -852,9 +852,7 @@ void install_basic_cmds(cmd_context & ctx) { ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(*) (+)", "declare mutually recursive datatypes.\n ::= ( +)\n ::= ( *)\n ::= ( )\nexample: (declare-datatypes (T) ((BinTree (leaf (value T)) (node (left BinTree) (right BinTree)))))")); ctx.insert(alloc(builtin_cmd, "check-sat-asuming", "( hprop_literali* )", "check sat assuming a collection of literals")); - // ctx.insert(alloc(builtin_cmd, "define-fun-rec", "hfun-defi", "define a function satisfying recursive equations")); - // ctx.insert(alloc(builtin_cmd, "define-funs-rec", "( hfun_decin+1 ) ( htermin+1 )", "define multiple mutually recursive functions")); - // ctx.insert(alloc(get_unsat_assumptions_cmd)); + ctx.insert(alloc(get_unsat_assumptions_cmd)); ctx.insert(alloc(reset_assertions_cmd)); } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f590725a7..d4273d42d 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -326,6 +326,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_numeral_as_real(false), m_ignore_check(false), m_exit_on_error(false), + m_processing_pareto(false), m_manager(m), m_own_manager(m == 0), m_manager_initialized(false), @@ -529,10 +530,6 @@ bool cmd_context::logic_has_fpa() const { return !has_logic() || smt_logics::logic_has_fpa(m_logic); } -bool cmd_context::logic_has_str() const { - return !has_logic() || m_logic == "QF_S"; -} - bool cmd_context::logic_has_array() const { return !has_logic() || smt_logics::logic_has_array(m_logic); } @@ -637,7 +634,7 @@ bool cmd_context::set_logic(symbol const & s) { std::string cmd_context::reason_unknown() const { if (m_check_sat_result.get() == 0) - throw cmd_exception("state of the most recent check-sat command is not known"); + return "state of the most recent check-sat command is not known"; return m_check_sat_result->reason_unknown(); } @@ -1130,6 +1127,7 @@ void cmd_context::insert_aux_pdecl(pdecl * p) { } void cmd_context::reset(bool finalize) { + m_processing_pareto = false; m_logic = symbol::null; m_check_sat_result = 0; m_numeral_as_real = false; @@ -1174,6 +1172,7 @@ void cmd_context::reset(bool finalize) { } void cmd_context::assert_expr(expr * t) { + m_processing_pareto = false; if (!m_check_logic(t)) throw cmd_exception(m_check_logic.get_last_error()); m_check_sat_result = 0; @@ -1186,6 +1185,7 @@ void cmd_context::assert_expr(expr * t) { } void cmd_context::assert_expr(symbol const & name, expr * t) { + m_processing_pareto = false; if (!m_check_logic(t)) throw cmd_exception(m_check_logic.get_last_error()); if (!produce_unsat_cores() || name == symbol::null) { @@ -1286,6 +1286,7 @@ static void restore(ast_manager & m, ptr_vector & c, unsigned old_sz) { } void cmd_context::restore_assertions(unsigned old_sz) { + m_processing_pareto = false; if (!has_manager()) { // restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one. SASSERT(old_sz == m_assertions.size()); @@ -1303,6 +1304,7 @@ void cmd_context::restore_assertions(unsigned old_sz) { void cmd_context::pop(unsigned n) { m_check_sat_result = 0; + m_processing_pareto = false; if (n == 0) return; unsigned lvl = m_scopes.size(); @@ -1333,7 +1335,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions unsigned rlimit = m_params.m_rlimit; scoped_watch sw(*this); lbool r; - bool was_pareto = false, was_opt = false; + bool was_opt = false; if (m_opt && !m_opt->empty()) { was_opt = true; @@ -1342,21 +1344,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(m().limit(), rlimit); - ptr_vector cnstr(m_assertions); - cnstr.append(num_assumptions, assumptions); - get_opt()->set_hard_constraints(cnstr); + if (!m_processing_pareto) { + ptr_vector cnstr(m_assertions); + cnstr.append(num_assumptions, assumptions); + get_opt()->set_hard_constraints(cnstr); + } try { r = get_opt()->optimize(); - while (r == l_true && get_opt()->is_pareto()) { - was_pareto = true; - get_opt()->display_assignment(regular_stream()); - regular_stream() << "\n"; - if (get_opt()->print_model()) { - model_ref mdl; - get_opt()->get_model(mdl); - display_model(mdl); - } - r = get_opt()->optimize(); + if (r == l_true && get_opt()->is_pareto()) { + m_processing_pareto = true; } } catch (z3_error & ex) { @@ -1366,8 +1362,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions get_opt()->display_assignment(regular_stream()); throw cmd_exception(ex.msg()); } - if (was_pareto && r == l_false) { - r = l_true; + if (m_processing_pareto && r != l_true) { + m_processing_pareto = false; } get_opt()->set_status(r); } @@ -1400,7 +1396,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions validate_model(); } validate_check_sat_result(r); - if (was_opt && r != l_false && !was_pareto) { + if (was_opt && r != l_false && !m_processing_pareto) { get_opt()->display_assignment(regular_stream()); } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 8885bc5d6..ed92ab909 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -123,7 +123,6 @@ public: virtual void display_assignment(std::ostream& out) = 0; virtual bool is_pareto() = 0; virtual void set_logic(symbol const& s) = 0; - virtual bool print_model() const = 0; virtual void get_box_model(model_ref& mdl, unsigned index) = 0; virtual void updt_params(params_ref const& p) = 0; }; @@ -161,6 +160,7 @@ protected: status m_status; bool m_numeral_as_real; bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. + bool m_processing_pareto; // used when re-entering check-sat for pareto front. bool m_exit_on_error; static std::ostringstream g_error_stream; @@ -257,7 +257,6 @@ protected: bool logic_has_array() const; bool logic_has_datatype() const; bool logic_has_fpa() const; - bool logic_has_str() const; void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; } void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;} 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/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 7484a77fa..05bb5489a 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1728,7 +1728,7 @@ namespace pdr { void context::validate_search() { expr_ref tr = m_search.get_trace(*this); - TRACE("pdr", tout << tr << "\n";); + TRACE("pdr", tout << tr << "\n";); smt::kernel solver(m, get_fparams()); solver.assert_expr(tr); lbool res = solver.check(); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1310727aa..54909939f 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -319,11 +319,6 @@ namespace opt { return r; } - bool context::print_model() const { - opt_params optp(m_params); - return optp.print_model(); - } - void context::get_base_model(model_ref& mdl) { mdl = m_model; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 53bfc19c5..66f0ef015 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -183,7 +183,6 @@ namespace opt { virtual bool empty() { return m_scoped_state.m_objectives.empty(); } virtual void set_hard_constraints(ptr_vector & hard); virtual lbool optimize(); - virtual bool print_model() const; virtual void set_model(model_ref& _m) { m_model = _m; } virtual void get_model(model_ref& _m); virtual void get_box_model(model_ref& _m, unsigned index); diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 51f58396c..13bf51313 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -7,7 +7,6 @@ def_module_params('opt', ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), - ('print_model', BOOL, False, 'display model for satisfiable constraints'), ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 83c31715d..b9ed925b0 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -130,13 +130,36 @@ public: m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr()); } + bool is_literal(expr* e) const { + return + is_uninterp_const(e) || + (m.is_not(e, e) && is_uninterp_const(e)); + } + virtual lbool check_sat(unsigned sz, expr * const * assumptions) { m_solver.pop_to_base_level(); + expr_ref_vector _assumptions(m); + obj_map asm2fml; + for (unsigned i = 0; i < sz; ++i) { + if (!is_literal(assumptions[i])) { + expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m); + expr_ref fml(m.mk_eq(a, assumptions[i]), m); + assert_expr(fml); + _assumptions.push_back(a); + asm2fml.insert(a, assumptions[i]); + } + else { + _assumptions.push_back(assumptions[i]); + asm2fml.insert(assumptions[i], assumptions[i]); + } + } + + TRACE("sat", tout << _assumptions << "\n";); dep2asm_t dep2asm; m_model = 0; lbool r = internalize_formulas(); if (r != l_true) return r; - r = internalize_assumptions(sz, assumptions, dep2asm); + r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm); if (r != l_true) return r; r = m_solver.check(m_asms.size(), m_asms.c_ptr()); @@ -150,7 +173,7 @@ public: case l_false: // TBD: expr_dependency core is not accounted for. if (!m_asms.empty()) { - extract_core(dep2asm); + extract_core(dep2asm, asm2fml); } break; default: @@ -241,6 +264,7 @@ public: sat::bool_var_vector bvars; vector lconseq; dep2asm_t dep2asm; + obj_map asm2fml; m_solver.pop_to_base_level(); lbool r = internalize_formulas(); if (r != l_true) return r; @@ -251,7 +275,7 @@ public: r = m_solver.get_consequences(m_asms, bvars, lconseq); if (r == l_false) { if (!m_asms.empty()) { - extract_core(dep2asm); + extract_core(dep2asm, asm2fml); } return r; } @@ -302,7 +326,6 @@ public: return l_true; } - virtual std::string reason_unknown() const { return m_unknown; } @@ -569,7 +592,7 @@ private: } } - void extract_core(dep2asm_t& dep2asm) { + void extract_core(dep2asm_t& dep2asm, obj_map const& asm2fml) { u_map asm2dep; extract_asm2dep(dep2asm, asm2dep); sat::literal_vector const& core = m_solver.get_core(); @@ -590,6 +613,9 @@ private: for (unsigned i = 0; i < core.size(); ++i) { expr* e = 0; VERIFY(asm2dep.find(core[i].index(), e)); + if (asm2fml.contains(e)) { + e = asm2fml.find(e); + } m_core.push_back(e); } } diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 26395f9ab..5c7ed33f8 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -43,7 +43,7 @@ Revision History: #include"quasi_macros.h" asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): - m_manager(m), + m(m), m_params(p), m_pre_simplifier(m), m_simplifier(m), @@ -63,7 +63,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): setup_simplifier_plugins(m_simplifier, m_bsimp, arith_simp, m_bvsimp); SASSERT(m_bsimp != 0); SASSERT(arith_simp != 0); - m_macro_finder = alloc(macro_finder, m_manager, m_macro_manager); + m_macro_finder = alloc(macro_finder, m, m_macro_manager); basic_simplifier_plugin * basic_simp = 0; bv_simplifier_plugin * bv_simp = 0; @@ -90,16 +90,16 @@ void asserted_formulas::setup() { } void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp) { - bsimp = alloc(basic_simplifier_plugin, m_manager); + bsimp = alloc(basic_simplifier_plugin, m); s.register_plugin(bsimp); - asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, m_params); + asimp = alloc(arith_simplifier_plugin, m, *bsimp, m_params); s.register_plugin(asimp); - s.register_plugin(alloc(array_simplifier_plugin, m_manager, *bsimp, s, m_params)); - bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, m_params); + s.register_plugin(alloc(array_simplifier_plugin, m, *bsimp, s, m_params)); + bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, m_params); s.register_plugin(bvsimp); - s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp)); - s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp)); - s.register_plugin(alloc(seq_simplifier_plugin, m_manager, *bsimp)); + s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp)); + s.register_plugin(alloc(fpa_simplifier_plugin, m, *bsimp)); + s.register_plugin(alloc(seq_simplifier_plugin, m, *bsimp)); } void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) { @@ -108,7 +108,7 @@ void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, pro SASSERT(!m_inconsistent); SASSERT(m_scopes.empty()); m_asserted_formulas.append(num_formulas, formulas); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) m_asserted_formula_prs.append(num_formulas, prs); } @@ -125,9 +125,9 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, expr_ref_vector & r SASSERT(!result.empty()); return; } - if (m_manager.is_false(e)) + if (m.is_false(e)) m_inconsistent = true; - ::push_assertion(m_manager, e, pr, result, result_prs); + ::push_assertion(m, e, pr, result, result_prs); } void asserted_formulas::set_eliminate_and(bool flag) { @@ -145,13 +145,13 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { push_assertion(e, _in_pr, m_asserted_formulas, m_asserted_formula_prs); return; } - proof_ref in_pr(_in_pr, m_manager); - expr_ref r1(m_manager); - proof_ref pr1(m_manager); - expr_ref r2(m_manager); - proof_ref pr2(m_manager); - TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m_manager) << "\n";); - TRACE("assert_expr_bug", tout << mk_pp(e, m_manager) << "\n";); + proof_ref in_pr(_in_pr, m); + expr_ref r1(m); + proof_ref pr1(m); + expr_ref r2(m); + proof_ref pr2(m); + TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m) << "\n";); + TRACE("assert_expr_bug", tout << mk_pp(e, m) << "\n";); if (m_params.m_pre_simplifier) { m_pre_simplifier(e, r1, pr1); } @@ -161,14 +161,14 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { } set_eliminate_and(false); // do not eliminate and before nnf. m_simplifier(r1, r2, pr2); - TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m_manager) << "\n";); - if (m_manager.proofs_enabled()) { + TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m) << "\n";); + if (m.proofs_enabled()) { if (e == r2) pr2 = in_pr; else - pr2 = m_manager.mk_modus_ponens(in_pr, m_manager.mk_transitivity(pr1, pr2)); + pr2 = m.mk_modus_ponens(in_pr, m.mk_transitivity(pr1, pr2)); } - TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m_manager) << "\n";); + TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m) << "\n";); push_assertion(r2, pr2, m_asserted_formulas, m_asserted_formula_prs); TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout);); } @@ -176,7 +176,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { void asserted_formulas::assert_expr(expr * e) { if (inconsistent()) return; - assert_expr(e, m_manager.mk_asserted(e)); + assert_expr(e, m.mk_asserted(e)); } void asserted_formulas::get_assertions(ptr_vector & result) { @@ -184,13 +184,13 @@ void asserted_formulas::get_assertions(ptr_vector & result) { } void asserted_formulas::push_scope() { - SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m_manager.canceled()); + SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m.canceled()); TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout);); m_scopes.push_back(scope()); m_macro_manager.push_scope(); scope & s = m_scopes.back(); s.m_asserted_formulas_lim = m_asserted_formulas.size(); - SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m_manager.canceled()); + SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m.canceled()); s.m_inconsistent_old = m_inconsistent; m_defined_names.push(); m_bv_sharing.push_scope(); @@ -206,7 +206,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) { m_inconsistent = s.m_inconsistent_old; m_defined_names.pop(num_scopes); m_asserted_formulas.shrink(s.m_asserted_formulas_lim); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim); m_asserted_qhead = s.m_asserted_formulas_lim; m_scopes.shrink(new_lvl); @@ -228,7 +228,7 @@ void asserted_formulas::reset() { #ifdef Z3DEBUG bool asserted_formulas::check_well_sorted() const { for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { - if (!is_well_sorted(m_manager, m_asserted_formulas.get(i))) return false; + if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false; } return true; } @@ -322,7 +322,7 @@ void asserted_formulas::display(std::ostream & out) const { for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { if (i == m_asserted_qhead) out << "[HEAD] ==>\n"; - out << mk_pp(m_asserted_formulas.get(i), m_manager) << "\n"; + out << mk_pp(m_asserted_formulas.get(i), m) << "\n"; } out << "inconsistent: " << inconsistent() << "\n"; } @@ -331,7 +331,7 @@ void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) co if (!m_asserted_formulas.empty()) { unsigned sz = m_asserted_formulas.size(); for (unsigned i = 0; i < sz; i++) - ast_def_ll_pp(out, m_manager, m_asserted_formulas.get(i), pp_visited, true, false); + ast_def_ll_pp(out, m, m_asserted_formulas.get(i), pp_visited, true, false); out << "asserted formulas:\n"; for (unsigned i = 0; i < sz; i++) out << "#" << m_asserted_formulas[i]->get_id() << " "; @@ -346,23 +346,23 @@ void asserted_formulas::reduce_asserted_formulas() { if (inconsistent()) { return; } - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); for (; i < sz && !inconsistent(); i++) { expr * n = m_asserted_formulas.get(i); SASSERT(n != 0); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); m_simplifier(n, new_n, new_pr); - TRACE("reduce_asserted_formulas", tout << mk_pp(n, m_manager) << " -> " << mk_pp(new_n, m_manager) << "\n";); + TRACE("reduce_asserted_formulas", tout << mk_pp(n, m) << " -> " << mk_pp(new_n, m) << "\n";); if (n == new_n.get()) { push_assertion(n, pr, new_exprs, new_prs); } else { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + new_pr = m.mk_modus_ponens(pr, new_pr); push_assertion(new_n, new_pr, new_exprs, new_prs); } if (canceled()) { @@ -376,15 +376,15 @@ void asserted_formulas::swap_asserted_formulas(expr_ref_vector & new_exprs, proo SASSERT(!inconsistent() || !new_exprs.empty()); m_asserted_formulas.shrink(m_asserted_qhead); m_asserted_formulas.append(new_exprs); - if (m_manager.proofs_enabled()) { + if (m.proofs_enabled()) { m_asserted_formula_prs.shrink(m_asserted_qhead); m_asserted_formula_prs.append(new_prs); } } void asserted_formulas::find_macros_core() { - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); unsigned sz = m_asserted_formulas.size(); m_macro_finder->operator()(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, m_asserted_formula_prs.c_ptr() + m_asserted_qhead, new_exprs, new_prs); @@ -407,9 +407,9 @@ void asserted_formulas::expand_macros() { void asserted_formulas::apply_quasi_macros() { IF_IVERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";); TRACE("before_quasi_macros", display(tout);); - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); - quasi_macros proc(m_manager, m_macro_manager, m_simplifier); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); + quasi_macros proc(m, m_macro_manager, m_simplifier); while (proc(m_asserted_formulas.size() - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, m_asserted_formula_prs.c_ptr() + m_asserted_qhead, @@ -424,27 +424,27 @@ void asserted_formulas::apply_quasi_macros() { void asserted_formulas::nnf_cnf() { IF_IVERBOSE(10, verbose_stream() << "(smt.nnf)\n";); - nnf apply_nnf(m_manager, m_defined_names); - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); - expr_ref_vector push_todo(m_manager); - proof_ref_vector push_todo_prs(m_manager); + nnf apply_nnf(m, m_defined_names); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); + expr_ref_vector push_todo(m); + proof_ref_vector push_todo_prs(m); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); - TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m_manager) << "\n";); + TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref r1(m_manager); - proof_ref pr1(m_manager); - CASSERT("well_sorted",is_well_sorted(m_manager, n)); + expr_ref r1(m); + proof_ref pr1(m); + CASSERT("well_sorted",is_well_sorted(m, n)); push_todo.reset(); push_todo_prs.reset(); apply_nnf(n, push_todo, push_todo_prs, r1, pr1); - CASSERT("well_sorted",is_well_sorted(m_manager, r1)); - pr = m_manager.mk_modus_ponens(pr, pr1); + CASSERT("well_sorted",is_well_sorted(m, r1)); + pr = m.mk_modus_ponens(pr, pr1); push_todo.push_back(r1); push_todo_prs.push_back(pr); @@ -456,13 +456,13 @@ void asserted_formulas::nnf_cnf() { expr * n = push_todo.get(k); proof * pr = 0; m_simplifier(n, r1, pr1); - CASSERT("well_sorted",is_well_sorted(m_manager, r1)); + CASSERT("well_sorted",is_well_sorted(m, r1)); if (canceled()) { return; } - if (m_manager.proofs_enabled()) - pr = m_manager.mk_modus_ponens(push_todo_prs.get(k), pr1); + if (m.proofs_enabled()) + pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1); else pr = 0; push_assertion(r1, pr, new_exprs, new_prs); @@ -476,23 +476,23 @@ void asserted_formulas::NAME() { IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ TRACE(LABEL, tout << "before:\n"; display(tout);); \ FUNCTOR_DEF; \ - expr_ref_vector new_exprs(m_manager); \ - proof_ref_vector new_prs(m_manager); \ + expr_ref_vector new_exprs(m); \ + proof_ref_vector new_prs(m); \ unsigned i = m_asserted_qhead; \ unsigned sz = m_asserted_formulas.size(); \ for (; i < sz; i++) { \ expr * n = m_asserted_formulas.get(i); \ proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m_manager); \ + expr_ref new_n(m); \ functor(n, new_n); \ - TRACE("simplifier_simple_step", tout << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";); \ + TRACE("simplifier_simple_step", tout << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";); \ if (n == new_n.get()) { \ push_assertion(n, pr, new_exprs, new_prs); \ } \ - else if (m_manager.proofs_enabled()) { \ - proof_ref new_pr(m_manager); \ - new_pr = m_manager.mk_rewrite_star(n, new_n, 0, 0); \ - new_pr = m_manager.mk_modus_ponens(pr, new_pr); \ + else if (m.proofs_enabled()) { \ + proof_ref new_pr(m); \ + new_pr = m.mk_rewrite_star(n, new_n, 0, 0); \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ push_assertion(new_n, new_pr, new_exprs, new_prs); \ } \ else { \ @@ -505,7 +505,7 @@ void asserted_formulas::NAME() { TRACE(LABEL, display(tout);); \ } -MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute-forall"); +MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m), "distribute_forall", "distribute-forall"); void asserted_formulas::reduce_and_solve() { IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";); @@ -516,22 +516,22 @@ void asserted_formulas::reduce_and_solve() { void asserted_formulas::infer_patterns() { IF_IVERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";); TRACE("before_pattern_inference", display(tout);); - pattern_inference infer(m_manager, m_params); - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); + pattern_inference infer(m, m_params); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); infer(n, new_n, new_pr); if (n == new_n.get()) { push_assertion(n, pr, new_exprs, new_prs); } - else if (m_manager.proofs_enabled()) { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + else if (m.proofs_enabled()) { + new_pr = m.mk_modus_ponens(pr, new_pr); push_assertion(new_n, new_pr, new_exprs, new_prs); } else { @@ -554,16 +554,16 @@ void asserted_formulas::commit(unsigned new_qhead) { void asserted_formulas::eliminate_term_ite() { IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";); TRACE("before_elim_term_ite", display(tout);); - elim_term_ite elim(m_manager, m_defined_names); - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); + elim_term_ite elim(m, m_defined_names); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); elim(n, new_exprs, new_prs, new_n, new_pr); SASSERT(new_n.get() != 0); DEBUG_CODE({ @@ -574,8 +574,8 @@ void asserted_formulas::eliminate_term_ite() { if (n == new_n.get()) { push_assertion(n, pr, new_exprs, new_prs); } - else if (m_manager.proofs_enabled()) { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + else if (m.proofs_enabled()) { + new_pr = m.mk_modus_ponens(pr, new_pr); push_assertion(new_n, new_pr, new_exprs, new_prs); } else { @@ -602,31 +602,31 @@ void asserted_formulas::propagate_values() { // - new_exprs2 is the set R // // The loop also updates the m_cache. It adds the entries x -> n to it. - expr_ref_vector new_exprs1(m_manager); - proof_ref_vector new_prs1(m_manager); - expr_ref_vector new_exprs2(m_manager); - proof_ref_vector new_prs2(m_manager); + expr_ref_vector new_exprs1(m); + proof_ref_vector new_prs1(m); + expr_ref_vector new_exprs2(m); + proof_ref_vector new_prs2(m); unsigned sz = m_asserted_formulas.size(); for (unsigned i = 0; i < sz; i++) { - expr_ref n(m_asserted_formulas.get(i), m_manager); - proof_ref pr(m_asserted_formula_prs.get(i, 0), m_manager); - TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";); + expr_ref n(m_asserted_formulas.get(i), m); + proof_ref pr(m_asserted_formula_prs.get(i, 0), m); + TRACE("simplifier", tout << mk_pp(n, m) << "\n";); expr* lhs, *rhs; - if (m_manager.is_eq(n, lhs, rhs) && - (m_manager.is_value(lhs) || m_manager.is_value(rhs))) { - if (m_manager.is_value(lhs)) { + if (m.is_eq(n, lhs, rhs) && + (m.is_value(lhs) || m.is_value(rhs))) { + if (m.is_value(lhs)) { std::swap(lhs, rhs); - n = m_manager.mk_eq(lhs, rhs); - pr = m_manager.mk_symmetry(pr); + n = m.mk_eq(lhs, rhs); + pr = m.mk_symmetry(pr); } - if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) { + if (!m.is_value(lhs) && !m_simplifier.is_cached(lhs)) { if (i >= m_asserted_qhead) { new_exprs1.push_back(n); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) new_prs1.push_back(pr); } - TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n"; - if (pr) tout << "proof: " << mk_pp(pr, m_manager) << "\n";); + TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m) << "\n->\n" << mk_pp(rhs, m) << "\n"; + if (pr) tout << "proof: " << mk_pp(pr, m) << "\n";); m_simplifier.cache_result(lhs, rhs, pr); found = true; continue; @@ -634,7 +634,7 @@ void asserted_formulas::propagate_values() { } if (i >= m_asserted_qhead) { new_exprs2.push_back(n); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) new_prs2.push_back(pr); } } @@ -646,14 +646,14 @@ void asserted_formulas::propagate_values() { for (unsigned i = 0; i < sz; i++) { expr * n = new_exprs2.get(i); proof * pr = new_prs2.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); m_simplifier(n, new_n, new_pr); if (n == new_n.get()) { push_assertion(n, pr, new_exprs1, new_prs1); } else { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + new_pr = m.mk_modus_ponens(pr, new_pr); push_assertion(new_n, new_pr, new_exprs1, new_prs1); } } @@ -677,25 +677,25 @@ void asserted_formulas::propagate_booleans() { cont = false; unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); -#define PROCESS() { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m_manager); \ - proof_ref new_pr(m_manager); \ - m_simplifier(n, new_n, new_pr); \ - m_asserted_formulas.set(i, new_n); \ - if (m_manager.proofs_enabled()) { \ - new_pr = m_manager.mk_modus_ponens(pr, new_pr); \ - m_asserted_formula_prs.set(i, new_pr); \ - } \ - if (n != new_n) { \ - cont = true; \ - modified = true; \ - } \ - if (m_manager.is_not(new_n)) \ - m_simplifier.cache_result(to_app(new_n)->get_arg(0), m_manager.mk_false(), m_manager.mk_iff_false(new_pr)); \ - else \ - m_simplifier.cache_result(new_n, m_manager.mk_true(), m_manager.mk_iff_true(new_pr)); \ +#define PROCESS() { \ + expr * n = m_asserted_formulas.get(i); \ + proof * pr = m_asserted_formula_prs.get(i, 0); \ + expr_ref new_n(m); \ + proof_ref new_pr(m); \ + m_simplifier(n, new_n, new_pr); \ + m_asserted_formulas.set(i, new_n); \ + if (m.proofs_enabled()) { \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ + m_asserted_formula_prs.set(i, new_pr); \ + } \ + if (n != new_n) { \ + cont = true; \ + modified = true; \ + } \ + if (m.is_not(new_n)) \ + m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \ + else \ + m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \ } for (; i < sz; i++) { PROCESS(); @@ -715,57 +715,57 @@ void asserted_formulas::propagate_booleans() { } #define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \ -bool asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ - TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - FUNCTOR; \ - bool changed = false; \ - expr_ref_vector new_exprs(m_manager); \ - proof_ref_vector new_prs(m_manager); \ - unsigned i = m_asserted_qhead; \ - unsigned sz = m_asserted_formulas.size(); \ - for (; i < sz; i++) { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m_manager); \ - proof_ref new_pr(m_manager); \ - functor(n, new_n, new_pr); \ - if (n == new_n.get()) { \ - push_assertion(n, pr, new_exprs, new_prs); \ - } \ - else if (m_manager.proofs_enabled()) { \ - changed = true; \ - if (!new_pr) new_pr = m_manager.mk_rewrite(n, new_n); \ - new_pr = m_manager.mk_modus_ponens(pr, new_pr); \ - push_assertion(new_n, new_pr, new_exprs, new_prs); \ - } \ - else { \ - changed = true; \ - push_assertion(new_n, 0, new_exprs, new_prs); \ - } \ - } \ - swap_asserted_formulas(new_exprs, new_prs); \ - TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - if (changed && REDUCE) { \ - reduce_and_solve(); \ + bool asserted_formulas::NAME() { \ + IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - } \ - return changed; \ -} + FUNCTOR; \ + bool changed = false; \ + expr_ref_vector new_exprs(m); \ + proof_ref_vector new_prs(m); \ + unsigned i = m_asserted_qhead; \ + unsigned sz = m_asserted_formulas.size(); \ + for (; i < sz; i++) { \ + expr * n = m_asserted_formulas.get(i); \ + proof * pr = m_asserted_formula_prs.get(i, 0); \ + expr_ref new_n(m); \ + proof_ref new_pr(m); \ + functor(n, new_n, new_pr); \ + if (n == new_n.get()) { \ + push_assertion(n, pr, new_exprs, new_prs); \ + } \ + else if (m.proofs_enabled()) { \ + changed = true; \ + if (!new_pr) new_pr = m.mk_rewrite(n, new_n); \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ + push_assertion(new_n, new_pr, new_exprs, new_prs); \ + } \ + else { \ + changed = true; \ + push_assertion(new_n, 0, new_exprs, new_prs); \ + } \ + } \ + swap_asserted_formulas(new_exprs, new_prs); \ + TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ + if (changed && REDUCE) { \ + reduce_and_solve(); \ + TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ + } \ + return changed; \ + } -MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m_manager, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false); +MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false); -MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m_manager), "pull_nested_quantifiers", "pull-nested-quantifiers", false); +MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m), "pull_nested_quantifiers", "pull-nested-quantifiers", false); proof * asserted_formulas::get_inconsistency_proof() const { if (!inconsistent()) return 0; - if (!m_manager.proofs_enabled()) + if (!m.proofs_enabled()) return 0; unsigned sz = m_asserted_formulas.size(); for (unsigned i = 0; i < sz; i++) { expr * f = m_asserted_formulas.get(i); - if (m_manager.is_false(f)) + if (m.is_false(f)) return m_asserted_formula_prs.get(i); } UNREACHABLE(); @@ -780,14 +780,14 @@ void asserted_formulas::refine_inj_axiom() { for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - if (is_quantifier(n) && simplify_inj_axiom(m_manager, to_quantifier(n), new_n)) { - TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";); + expr_ref new_n(m); + if (is_quantifier(n) && simplify_inj_axiom(m, to_quantifier(n), new_n)) { + TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";); m_asserted_formulas.set(i, new_n); - if (m_manager.proofs_enabled()) { - proof_ref new_pr(m_manager); - new_pr = m_manager.mk_rewrite(n, new_n); - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + if (m.proofs_enabled()) { + proof_ref new_pr(m); + new_pr = m.mk_rewrite(n, new_n); + new_pr = m.mk_modus_ponens(pr, new_pr); m_asserted_formula_prs.set(i, new_pr); } } @@ -797,36 +797,36 @@ void asserted_formulas::refine_inj_axiom() { MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate-bit-vector-over-integers", true); -MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap-fourier-motzkin", true); +MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m), "elim_bounds", "cheap-fourier-motzkin", true); -MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true); +MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true); -#define LIFT_ITE(NAME, FUNCTOR, MSG) \ -void asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ - TRACE("lift_ite", display(tout);); \ - FUNCTOR; \ - unsigned i = m_asserted_qhead; \ - unsigned sz = m_asserted_formulas.size(); \ - for (; i < sz; i++) { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m_manager); \ - proof_ref new_pr(m_manager); \ - functor(n, new_n, new_pr); \ - TRACE("lift_ite_step", tout << mk_pp(n, m_manager) << "\n";); \ - IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \ - m_asserted_formulas.set(i, new_n); \ - if (m_manager.proofs_enabled()) { \ - new_pr = m_manager.mk_modus_ponens(pr, new_pr); \ - m_asserted_formula_prs.set(i, new_pr); \ - } \ - } \ - TRACE("lift_ite", display(tout);); \ - reduce_and_solve(); \ -} +#define LIFT_ITE(NAME, FUNCTOR, MSG) \ + void asserted_formulas::NAME() { \ + IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ + TRACE("lift_ite", display(tout);); \ + FUNCTOR; \ + unsigned i = m_asserted_qhead; \ + unsigned sz = m_asserted_formulas.size(); \ + for (; i < sz; i++) { \ + expr * n = m_asserted_formulas.get(i); \ + proof * pr = m_asserted_formula_prs.get(i, 0); \ + expr_ref new_n(m); \ + proof_ref new_pr(m); \ + functor(n, new_n, new_pr); \ + TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \ + IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \ + m_asserted_formulas.set(i, new_n); \ + if (m.proofs_enabled()) { \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ + m_asserted_formula_prs.set(i, new_pr); \ + } \ + } \ + TRACE("lift_ite", display(tout);); \ + reduce_and_solve(); \ + } LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite"); LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite"); @@ -848,12 +848,12 @@ void asserted_formulas::max_bv_sharing() { for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); m_bv_sharing(n, new_n, new_pr); m_asserted_formulas.set(i, new_n); - if (m_manager.proofs_enabled()) { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + if (m.proofs_enabled()) { + new_pr = m.mk_modus_ponens(pr, new_pr); m_asserted_formula_prs.set(i, new_pr); } } diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 9e9ecf33a..6ad36cc70 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -35,7 +35,7 @@ class arith_simplifier_plugin; class bv_simplifier_plugin; class asserted_formulas { - ast_manager & m_manager; + ast_manager & m; smt_params & m_params; simplifier m_pre_simplifier; simplifier m_simplifier; @@ -94,7 +94,7 @@ class asserted_formulas { unsigned get_total_size() const; bool has_bv() const; void max_bv_sharing(); - bool canceled() { return m_manager.canceled(); } + bool canceled() { return m.canceled(); } public: asserted_formulas(ast_manager & m, smt_params & p); @@ -115,7 +115,7 @@ public: void commit(); void commit(unsigned new_qhead); expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); } - proof * get_formula_proof(unsigned idx) const { return m_manager.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; } + proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; } expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); } proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); } void init(unsigned num_formulas, expr * const * formulas, proof * const * prs); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 6c2ff4962..a501f474a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -44,6 +44,7 @@ def_module_params(module_name='smt', ('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'), + ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 1e3f29142..944911f9b 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -35,6 +35,7 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_ignore_int = p.arith_ignore_int(); m_arith_bound_prop = static_cast(p.arith_propagation_mode()); m_arith_dump_lemmas = p.arith_dump_lemmas(); + m_arith_reflect = p.arith_reflect(); } @@ -85,4 +86,4 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nl_arith_branching); DISPLAY_PARAM(m_nl_arith_rounds); DISPLAY_PARAM(m_arith_euclidean_solver); -} \ No newline at end of file +} diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 129d77c85..41a269820 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -51,9 +51,9 @@ namespace smt { if (!m_theory_var_priority.find(v2, p_v2)) { p_v2 = 0.0; } - // add clause activity - p_v1 += m_activity[v1]; - p_v2 += m_activity[v2]; + // add clause activity + p_v1 += m_activity[v1]; + p_v2 += m_activity[v2]; return p_v1 > p_v2; } }; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 50b957331..0c32f3c76 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3035,7 +3035,7 @@ namespace smt { // not counting any literals that get assigned by this method // this relies on bcp() to give us its old m_qhead and therefore // bcp() should always be called before this method - + unsigned assigned_literal_end = m_assigned_literals.size(); for (; qhead < assigned_literal_end; ++qhead) { literal l = m_assigned_literals[qhead]; diff --git a/src/smt/smt_for_each_relevant_expr.cpp b/src/smt/smt_for_each_relevant_expr.cpp index bf039e8a1..84f93dd33 100644 --- a/src/smt/smt_for_each_relevant_expr.cpp +++ b/src/smt/smt_for_each_relevant_expr.cpp @@ -23,7 +23,7 @@ Revision History: namespace smt { - bool check_at_labels::check(expr* n) { + bool check_at_labels::check(expr* n) { m_first = true; return count_at_labels_pos(n) <= 1; } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 279ea20cf..b50527acf 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -279,7 +279,7 @@ namespace smt { m_aux_context->pop(1); return r == l_false; // quantifier is satisfied by m_curr_model } - + model_ref complete_cex; m_aux_context->get_model(complete_cex); @@ -425,7 +425,7 @@ namespace smt { ptr_vector::const_iterator end = m_qm->end_quantifiers(); for (; it != end; ++it) { quantifier * q = *it; - if(!m_qm->mbqi_enabled(q)) continue; + if(!m_qm->mbqi_enabled(q)) continue; TRACE("model_checker", tout << "Check: " << mk_pp(q, m) << "\n"; tout << m_context->get_assignment(q) << "\n";); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index fa48fea57..6c47bf855 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -426,19 +426,19 @@ namespace smt { ptr_buffer to_unmark; unsigned num_vars = get_num_vars(); for (unsigned i = 0; i < num_vars; i++) { - enode * n = get_enode(i); + enode * n = get_enode(i); if (ctx.is_relevant(n)) { - enode * r = n->get_root(); - if (!r->is_marked()){ - if(is_array_sort(r) && ctx.is_shared(r)) { - TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); - theory_var r_th_var = r->get_th_var(get_id()); - SASSERT(r_th_var != null_theory_var); - result.push_back(r_th_var); - } - r->set_mark(); - to_unmark.push_back(r); - } + enode * r = n->get_root(); + if (!r->is_marked()){ + if(is_array_sort(r) && ctx.is_shared(r)) { + TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); + theory_var r_th_var = r->get_th_var(get_id()); + SASSERT(r_th_var != null_theory_var); + result.push_back(r_th_var); + } + r->set_mark(); + to_unmark.push_back(r); + } } } unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 05aa33d13..a5a34a079 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -487,7 +487,7 @@ namespace smt { result = m_theory_var2var_index[v]; } if (result == UINT_MAX) { - result = m_solver->add_var(v); + result = m_solver->add_var(v); // TBD: is_int(v); m_theory_var2var_index.setx(v, result, UINT_MAX); m_var_index2theory_var.setx(result, v, UINT_MAX); m_var_trail.push_back(v); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 62846e709..d560a54a1 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -25,6 +25,7 @@ #include #include"theory_seq_empty.h" #include"theory_arith.h" +#include"ast_util.h" namespace smt { @@ -98,7 +99,7 @@ namespace smt { if (defaultCharset) { // valid C strings can't contain the null byte ('\0') charSetSize = 255; - char_set = alloc_svect(char, charSetSize); + char_set.resize(256, 0); int idx = 0; // small letters for (int i = 97; i < 123; i++) { @@ -157,8 +158,7 @@ namespace smt { } else { const char setset[] = { 'a', 'b', 'c' }; int fSize = sizeof(setset) / sizeof(char); - - char_set = alloc_svect(char, fSize); + char_set.resize(fSize, 0); charSetSize = fSize; for (int i = 0; i < charSetSize; i++) { char_set[i] = setset[i]; @@ -494,6 +494,7 @@ namespace smt { sort * string_sort = u.str.mk_string_sort(); app * a = mk_fresh_const(name.c_str(), string_sort); + m_trail.push_back(a); TRACE("str", tout << "a->get_family_id() = " << a->get_family_id() << std::endl << "this->get_family_id() = " << this->get_family_id() << std::endl;); @@ -507,7 +508,6 @@ namespace smt { m_basicstr_axiom_todo.push_back(ctx.get_enode(a)); TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); - m_trail.push_back(a); variable_set.insert(a); internal_variable_set.insert(a); track_variable_scope(a); @@ -521,6 +521,7 @@ namespace smt { sort * string_sort = u.str.mk_string_sort(); app * a = mk_fresh_const("regex", string_sort); + m_trail.push_back(a); ctx.internalize(a, false); SASSERT(ctx.get_enode(a) != NULL); @@ -529,7 +530,6 @@ namespace smt { m_basicstr_axiom_todo.push_back(ctx.get_enode(a)); TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); - m_trail.push_back(a); variable_set.insert(a); //internal_variable_set.insert(a); regex_variable_set.insert(a); @@ -5563,7 +5563,7 @@ namespace smt { if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) { ndVec.pop_back(); ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0])); - for (int i = 1; i < arg1VecSize; i++) { + for (size_t i = 1; i < arg1VecSize; i++) { ndVec.push_back(arg1_grdItor->first[i]); } } else { @@ -5666,7 +5666,7 @@ namespace smt { if (subStrCnt == 1) { zstring subStrVal; if (u.str.is_string(subStrVec[0], subStrVal)) { - for (int i = 0; i < strCnt; i++) { + for (size_t i = 0; i < strCnt; i++) { zstring strVal; if (u.str.is_string(strVec[i], strVal)) { if (strVal.contains(subStrVal)) { @@ -5675,7 +5675,7 @@ namespace smt { } } } else { - for (int i = 0; i < strCnt; i++) { + for (size_t i = 0; i < strCnt; i++) { if (strVec[i] == subStrVec[0]) { return true; } @@ -5683,7 +5683,7 @@ namespace smt { } return false; } else { - for (int i = 0; i <= (strCnt - subStrCnt); i++) { + for (size_t i = 0; i <= (strCnt - subStrCnt); i++) { // The first node in subStrVect should be // * constant: a suffix of a note in strVec[i] // * variable: @@ -5712,7 +5712,7 @@ namespace smt { // middle nodes bool midNodesOK = true; - for (int j = 1; j < subStrCnt - 1; j++) { + for (size_t j = 1; j < subStrCnt - 1; j++) { if (subStrVec[j] != strVec[i + j]) { midNodesOK = false; break; @@ -6927,9 +6927,9 @@ namespace smt { ast_manager & m = get_manager(); if (lenTester_fvar_map.contains(lenTester)) { expr * fVar = lenTester_fvar_map[lenTester]; - expr * toAssert = gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue); + expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m); TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); - if (toAssert != NULL) { + if (toAssert) { assert_axiom(toAssert); } } @@ -7304,7 +7304,7 @@ namespace smt { TRACE("str", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;); } } - } else if (ex_sort == bool_sort) { + } else if (ex_sort == bool_sort && !is_quantifier(ex)) { TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << ": expr is of sort Bool" << std::endl;); // set up axioms for boolean terms @@ -7351,7 +7351,7 @@ namespace smt { // if expr is an application, recursively inspect all arguments if (is_app(ex)) { - app * term = (app*)ex; + app * term = to_app(ex); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) { set_up_axioms(term->get_arg(i)); @@ -9123,7 +9123,7 @@ namespace smt { zstring theory_str::gen_val_string(int len, int_vector & encoding) { SASSERT(charSetSize > 0); - SASSERT(char_set != NULL); + SASSERT(!char_set.empty()); std::string re(len, char_set[0]); for (int i = 0; i < (int) encoding.size() - 1; i++) { @@ -9173,7 +9173,7 @@ namespace smt { } } - expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, + expr* theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, zstring lenStr, int tries) { ast_manager & m = get_manager(); context & ctx = get_context(); @@ -9240,8 +9240,7 @@ namespace smt { // ---------------------------------------------------------------------------------------- - ptr_vector orList; - ptr_vector andList; + expr_ref_vector orList(m), andList(m); for (long long i = l; i < h; i++) { orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) )); @@ -9262,7 +9261,7 @@ namespace smt { } else { strAst = mk_string(aStr); } - andList.push_back(m.mk_eq(orList[orList.size() - 1], m.mk_eq(freeVar, strAst))); + andList.push_back(m.mk_eq(orList[orList.size() - 1].get(), m.mk_eq(freeVar, strAst))); } if (!coverAll) { orList.push_back(m.mk_eq(val_indicator, mk_string("more"))); @@ -9273,21 +9272,8 @@ namespace smt { } } - expr ** or_items = alloc_svect(expr*, orList.size()); - expr ** and_items = alloc_svect(expr*, andList.size() + 1); - - for (int i = 0; i < (int) orList.size(); i++) { - or_items[i] = orList[i]; - } - if (orList.size() > 1) - and_items[0] = m.mk_or(orList.size(), or_items); - else - and_items[0] = or_items[0]; - - for (int i = 0; i < (int) andList.size(); i++) { - and_items[i + 1] = andList[i]; - } - expr * valTestAssert = m.mk_and(andList.size() + 1, and_items); + andList.push_back(mk_or(orList)); + expr_ref valTestAssert = mk_and(andList); // --------------------------------------- // If the new value tester is $$_val_x_16_i @@ -9300,20 +9286,9 @@ namespace smt { if (vTester != val_indicator) andList.push_back(m.mk_eq(vTester, mk_string("more"))); } - expr * assertL = NULL; - if (andList.size() == 1) { - assertL = andList[0]; - } else { - expr ** and_items = alloc_svect(expr*, andList.size()); - for (int i = 0; i < (int) andList.size(); i++) { - and_items[i] = andList[i]; - } - assertL = m.mk_and(andList.size(), and_items); - } - + expr_ref assertL = mk_and(andList); // (assertL => valTestAssert) <=> (!assertL OR valTestAssert) - valTestAssert = m.mk_or(m.mk_not(assertL), valTestAssert); - return valTestAssert; + return m.mk_or(m.mk_not(assertL), valTestAssert); } expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, @@ -9378,7 +9353,7 @@ namespace smt { << " doesn't have an equivalence class value." << std::endl;); refresh_theory_var(aTester); - expr * makeupAssert = gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i); + expr_ref makeupAssert(gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i), m); TRACE("str", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl << mk_ismt2_pp(makeupAssert, m) << std::endl;); @@ -9400,8 +9375,7 @@ namespace smt { fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester)); print_value_tester_list(fvar_valueTester_map[freeVar][len]); } - expr * nextAssert = gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1); - return nextAssert; + return gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1); } return NULL; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 4752e8a1b..0bbc44ab8 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -330,9 +330,9 @@ protected: std::map regex_nfa_cache; // Regex term --> NFA - char * char_set; - std::map charSetLookupTable; - int charSetSize; + svector char_set; + std::map charSetLookupTable; + int charSetSize; obj_pair_map concat_astNode_map; @@ -553,7 +553,7 @@ protected: expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries); expr * gen_free_var_options(expr * freeVar, expr * len_indicator, zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr); - expr * gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, + expr* gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, zstring lenStr, int tries); void print_value_tester_list(svector > & testerList); bool get_next_val_encode(int_vector & base, int_vector & next); diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index c4ead74df..2bb364b6a 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -153,5 +153,5 @@ bool smt_logics::logic_has_pb(symbol const& s) { } bool smt_logics::logic_has_datatype(symbol const& s) { - return s == "QF_FD"; + return s == "QF_FD" || s == "ALL"; } diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 918e0fc6d..ca6390c9c 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -103,7 +103,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat tactic * st = main_p(and_then(preamble_st, // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function // symbols. In this case, we should not use the `sat', but instead `smt'. Alternatively, - // the UFs can be eliminated by eager ackermannization in the preamble. + // the UFs can be eliminated by eager ackermannization in the preamble. cond(mk_is_qfbv_eq_probe(), and_then(mk_bv1_blaster_tactic(m), using_params(smt, solver_p)), diff --git a/src/test/lp.cpp b/src/test/lp.cpp index 235dab960..9e05112f5 100644 --- a/src/test/lp.cpp +++ b/src/test/lp.cpp @@ -1159,12 +1159,14 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite lp_solver * solver = reader.create_solver(dual); setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver); - int begin = get_millisecond_count(); + stopwatch sw; + sw.start(); if (dual) { std::cout << "solving for dual" << std::endl; } solver->find_maximal_solution(); - int span = get_millisecond_span(begin); + sw.stop(); + double span = sw.get_seconds(); std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl; if (solver->get_status() == lp_status::OPTIMAL) { if (reader.column_names().size() < 20) { @@ -1213,7 +1215,8 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i if (reader.is_ok()) { auto * solver = reader.create_solver(dual); setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver); - int begin = get_millisecond_count(); + stopwatch sw; + sw.start(); solver->find_maximal_solution(); std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl; @@ -1227,7 +1230,7 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i } std::cout << "cost = " << cost.get_double() << std::endl; } - std::cout << "processed in " << get_millisecond_span(begin) / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl; + std::cout << "processed in " << sw.get_current_seconds() / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl; delete solver; } else { std::cout << "cannot process " << file_name << std::endl; @@ -2426,9 +2429,10 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read std::cout << "status = " << lp_status_to_string(solver->get_status()) << std::endl; return; } - int begin = get_millisecond_count(); + stopwatch sw; + sw.start(); lp_status status = solver->solve(); - std::cout << "status is " << lp_status_to_string(status) << ", processed for " << get_millisecond_span(begin) / 1000.0 <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl; + std::cout << "status is " << lp_status_to_string(status) << ", processed for " << sw.get_current_seconds() <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl; if (solver->get_status() == INFEASIBLE) { vector> evidence; solver->get_infeasibility_explanation(evidence); diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index e577e15df..a522c9a41 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -29,7 +29,7 @@ Revision History: #include #endif -#if defined(__x86_64__) || defined(_M_X64) || \ +#if defined(__x86_64__) || defined(_M_X64) || \ defined(__i386) || defined(_M_IX86) #define USE_INTRINSICS #endif diff --git a/src/util/lp/lp_primal_simplex.h b/src/util/lp/lp_primal_simplex.h index fcddb4eb1..715d76408 100644 --- a/src/util/lp/lp_primal_simplex.h +++ b/src/util/lp/lp_primal_simplex.h @@ -55,10 +55,6 @@ public: void set_core_solver_bounds(); - void update_time_limit_from_starting_time(int start_time) { - this->m_settings.time_limit -= (get_millisecond_span(start_time) / 1000.); - } - void find_maximal_solution(); void fill_A_x_and_basis_for_stage_one_total_inf(); diff --git a/src/util/lp/lp_primal_simplex.hpp b/src/util/lp/lp_primal_simplex.hpp index 9e1af2bbe..b6b6006e5 100644 --- a/src/util/lp/lp_primal_simplex.hpp +++ b/src/util/lp/lp_primal_simplex.hpp @@ -152,7 +152,6 @@ template void lp_primal_simplex::set_core_solver_ template void lp_primal_simplex::find_maximal_solution() { - int preprocessing_start_time = get_millisecond_count(); if (this->problem_is_empty()) { this->m_status = lp_status::EMPTY; return; @@ -169,7 +168,6 @@ template void lp_primal_simplex::find_maximal_sol fill_acceptable_values_for_x(); this->count_slacks_and_artificials(); set_core_solver_bounds(); - update_time_limit_from_starting_time(preprocessing_start_time); solve_with_total_inf(); } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 6b6aba2ad..aac3692f9 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -8,9 +8,9 @@ #include #include #include -#include #include #include "util/lp/lp_utils.h" +#include "util/stopwatch.h" namespace lean { typedef unsigned var_index; @@ -69,10 +69,6 @@ enum non_basic_column_value_position { at_low_bound, at_upper_bound, at_fixed, f template bool is_epsilon_small(const X & v, const double& eps); // forward definition -int get_millisecond_count(); -int get_millisecond_span(int start_time); - - class lp_resource_limit { public: virtual bool get_cancel_flag() = 0; @@ -92,12 +88,13 @@ struct lp_settings { private: class default_lp_resource_limit : public lp_resource_limit { lp_settings& m_settings; - int m_start_time; + stopwatch m_sw; public: - default_lp_resource_limit(lp_settings& s): m_settings(s), m_start_time(get_millisecond_count()) {} + default_lp_resource_limit(lp_settings& s): m_settings(s) { + m_sw.start(); + } virtual bool get_cancel_flag() { - int span_in_mills = get_millisecond_span(m_start_time); - return (span_in_mills / 1000.0 > m_settings.time_limit); + return (m_sw.get_current_seconds() > m_settings.time_limit); } }; diff --git a/src/util/lp/lp_settings.hpp b/src/util/lp/lp_settings.hpp index b57a3acda..b27d837e0 100644 --- a/src/util/lp/lp_settings.hpp +++ b/src/util/lp/lp_settings.hpp @@ -52,19 +52,6 @@ lp_status lp_status_from_string(std::string status) { lean_unreachable(); return lp_status::UNKNOWN; // it is unreachable } -int get_millisecond_count() { - timeb tb; - ftime(&tb); - return tb.millitm + (tb.time & 0xfffff) * 1000; -} - -int get_millisecond_span(int start_time) { - int span = get_millisecond_count() - start_time; - if (span < 0) - span += 0x100000 * 1000; - return span; -} - template diff --git a/src/util/lp/matrix.hpp b/src/util/lp/matrix.hpp index 27cdabd3e..d032cab8c 100644 --- a/src/util/lp/matrix.hpp +++ b/src/util/lp/matrix.hpp @@ -58,8 +58,8 @@ unsigned get_width_of_column(unsigned j, vector> & A) { unsigned r = 0; for (unsigned i = 0; i < A.size(); i++) { vector & t = A[i]; - std::string str= t[j]; - unsigned s = str.size(); + std::string str = t[j]; + unsigned s = static_cast(str.size()); if (r < s) { r = s; } @@ -69,8 +69,8 @@ unsigned get_width_of_column(unsigned j, vector> & A) { void print_matrix_with_widths(vector> & A, vector & ws, std::ostream & out) { for (unsigned i = 0; i < A.size(); i++) { - for (unsigned j = 0; j < A[i].size(); j++) { - print_blanks(ws[j] - A[i][j].size(), out); + for (unsigned j = 0; j < static_cast(A[i].size()); j++) { + print_blanks(ws[j] - static_cast(A[i][j].size()), out); out << A[i][j] << " "; } out << std::endl; diff --git a/src/util/lp/sparse_matrix.hpp b/src/util/lp/sparse_matrix.hpp index ff6ac9997..32bb8ed4e 100644 --- a/src/util/lp/sparse_matrix.hpp +++ b/src/util/lp/sparse_matrix.hpp @@ -1050,8 +1050,8 @@ bool sparse_matrix::get_pivot_for_column(unsigned &i, unsigned &j, int c_p if (i_inv < k) continue; unsigned j_inv = adjust_column_inverse(j); if (j_inv < k) continue; - int small = elem_is_too_small(i, j, c_partial_pivoting); - if (!small) { + int _small = elem_is_too_small(i, j, c_partial_pivoting); + if (!_small) { #ifdef LEAN_DEBUG // if (!really_best_pivot(i, j, c_partial_pivoting, k)) { // print_active_matrix(k); @@ -1063,7 +1063,7 @@ bool sparse_matrix::get_pivot_for_column(unsigned &i, unsigned &j, int c_p j = j_inv; return true; } - if (small != 2) { // 2 means that the pair is not in the matrix + if (_small != 2) { // 2 means that the pair is not in the matrix pivots_candidates_that_are_too_small.push_back(std::make_pair(i, j)); } } diff --git a/src/util/trace.cpp b/src/util/trace.cpp index 72984d808..05a3e49bd 100644 --- a/src/util/trace.cpp +++ b/src/util/trace.cpp @@ -52,7 +52,7 @@ void disable_trace(const char * tag) { bool is_trace_enabled(const char * tag) { return g_enable_all_trace_tags || - (g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast(tag))); + (g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast(tag))); } void close_trace() { diff --git a/src/util/warning.cpp b/src/util/warning.cpp index ed4cd8725..9c6a285b9 100644 --- a/src/util/warning.cpp +++ b/src/util/warning.cpp @@ -115,22 +115,22 @@ void format2ostream(std::ostream & out, char const* msg, va_list args) { while (true) { int nc = VPRF(buff.c_ptr(), buff.size(), msg, args); #if !defined(_WINDOWS) && defined(_AMD64_) - // For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf. - // Z3 crashes when trying to use va_list args again. + // For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf. + // Z3 crashes when trying to use va_list args again. // Hack: I truncate the message instead of expanding the buffer to make sure that // va_list args is only used once. - END_ERR_HANDLER(); - if (nc < 0) { - // vsnprintf didn't work, so we just print the msg - out << msg; - return; - } - if (nc >= static_cast(buff.size())) { + END_ERR_HANDLER(); + if (nc < 0) { + // vsnprintf didn't work, so we just print the msg + out << msg; + return; + } + if (nc >= static_cast(buff.size())) { // truncate the message buff[buff.size() - 1] = 0; - } + } out << buff.c_ptr(); - return; + return; #else if (nc >= 0 && nc < static_cast(buff.size())) break; // success