mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
546d22e77a
|
@ -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
|
||||
|
|
|
@ -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)));
|
||||
}
|
||||
|
||||
|
|
|
@ -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<builtin_name> & 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));
|
||||
|
|
|
@ -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 "<keyword>"; }
|
||||
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", "(<symbol>*) (<datatype-declaration>+)", "declare mutually recursive datatypes.\n<datatype-declaration> ::= (<symbol> <constructor-decl>+)\n<constructor-decl> ::= (<symbol> <accessor-decl>*)\n<accessor-decl> ::= (<symbol> <sort>)\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));
|
||||
}
|
||||
|
||||
|
|
|
@ -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<expr> & 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<expr> cnstr(m_assertions);
|
||||
cnstr.append(num_assumptions, assumptions);
|
||||
get_opt()->set_hard_constraints(cnstr);
|
||||
if (!m_processing_pareto) {
|
||||
ptr_vector<expr> 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());
|
||||
}
|
||||
|
||||
|
|
|
@ -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;}
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -183,7 +183,6 @@ namespace opt {
|
|||
virtual bool empty() { return m_scoped_state.m_objectives.empty(); }
|
||||
virtual void set_hard_constraints(ptr_vector<expr> & 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);
|
||||
|
|
|
@ -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'),
|
||||
|
|
|
@ -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";
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue