diff --git a/README-CMake.md b/README-CMake.md index 5b3cdfd36..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 diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index ea3fd2147..ef86f510a 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))); } 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/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index f09d35158..26cd0628e 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -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 5867b9825..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; }; @@ -258,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/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/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"; }