mirror of
https://github.com/Z3Prover/z3
synced 2025-04-19 07:09:03 +00:00
trinhmt
GitHub
commit
57845d4809
|
|
@ -1990,7 +1990,7 @@ class MLComponent(Component):
|
|||
out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3dllso, z3mls))
|
||||
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))
|
||||
out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
|
||||
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
|
||||
out.write('\t%s -linkall -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
|
||||
|
||||
out.write('\n')
|
||||
out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
|
||||
|
|
|
|||
|
|
@ -1289,7 +1289,7 @@ decl_kind user_sort_plugin::register_name(symbol s) {
|
|||
|
||||
decl_plugin * user_sort_plugin::mk_fresh() {
|
||||
user_sort_plugin * p = alloc(user_sort_plugin);
|
||||
for (symbol const& s : m_sort_names)
|
||||
for (symbol const& s : m_sort_names)
|
||||
p->register_name(s);
|
||||
return p;
|
||||
}
|
||||
|
|
@ -1415,7 +1415,7 @@ ast_manager::~ast_manager() {
|
|||
p->finalize();
|
||||
}
|
||||
for (decl_plugin* p : m_plugins) {
|
||||
if (p)
|
||||
if (p)
|
||||
dealloc(p);
|
||||
}
|
||||
m_plugins.reset();
|
||||
|
|
@ -1454,13 +1454,13 @@ ast_manager::~ast_manager() {
|
|||
mark_array_ref(mark, to_quantifier(n)->get_num_patterns(), to_quantifier(n)->get_patterns());
|
||||
mark_array_ref(mark, to_quantifier(n)->get_num_no_patterns(), to_quantifier(n)->get_no_patterns());
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
for (ast * n : m_ast_table) {
|
||||
if (!mark.is_marked(n)) {
|
||||
roots.push_back(n);
|
||||
}
|
||||
}
|
||||
}
|
||||
SASSERT(!roots.empty());
|
||||
for (unsigned i = 0; i < roots.size(); ++i) {
|
||||
ast* a = roots[i];
|
||||
|
|
@ -1683,7 +1683,7 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
bool contains = m_ast_table.contains(n);
|
||||
CASSERT("nondet_bug", contains || slow_not_contains(n));
|
||||
#endif
|
||||
|
||||
|
||||
ast * r = m_ast_table.insert_if_not_there(n);
|
||||
SASSERT(r->m_hash == h);
|
||||
if (r != n) {
|
||||
|
|
@ -2358,8 +2358,9 @@ quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort *
|
|||
unsigned num_patterns, expr * const * patterns,
|
||||
unsigned num_no_patterns, expr * const * no_patterns) {
|
||||
SASSERT(body);
|
||||
SASSERT(num_patterns == 0 || num_no_patterns == 0);
|
||||
SASSERT(num_decls > 0);
|
||||
if (num_patterns != 0 && num_no_patterns != 0)
|
||||
throw ast_exception("simultaneous patterns and no-patterns not supported");
|
||||
DEBUG_CODE({
|
||||
for (unsigned i = 0; i < num_patterns; ++i) {
|
||||
TRACE("ast", tout << i << " " << mk_pp(patterns[i], *this) << "\n";);
|
||||
|
|
@ -2763,7 +2764,7 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs, expr * n1, expr * n2) {
|
||||
if (num_proofs == 0)
|
||||
if (num_proofs == 0)
|
||||
return nullptr;
|
||||
if (num_proofs == 1)
|
||||
return proofs[0];
|
||||
|
|
|
|||
|
|
@ -672,14 +672,14 @@ namespace nlsat {
|
|||
return new_set;
|
||||
}
|
||||
|
||||
void interval_set_manager::peek_in_complement(interval_set const * s, anum & w, bool randomize) {
|
||||
void interval_set_manager::peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize) {
|
||||
SASSERT(!is_full(s));
|
||||
if (s == 0) {
|
||||
if (randomize) {
|
||||
int num = m_rand() % 2 == 0 ? 1 : -1;
|
||||
#define MAX_RANDOM_DEN_K 4
|
||||
int den_k = (m_rand() % MAX_RANDOM_DEN_K);
|
||||
int den = 1 << den_k;
|
||||
int den = is_int ? 1 : (1 << den_k);
|
||||
scoped_mpq _w(m_am.qm());
|
||||
m_am.qm().set(_w, num, den);
|
||||
m_am.set(w, _w);
|
||||
|
|
|
|||
|
|
@ -108,7 +108,7 @@ namespace nlsat {
|
|||
|
||||
\pre !is_full(s)
|
||||
*/
|
||||
void peek_in_complement(interval_set const * s, anum & w, bool randomize);
|
||||
void peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize);
|
||||
};
|
||||
|
||||
typedef obj_ref<interval_set, interval_set_manager> interval_set_ref;
|
||||
|
|
|
|||
|
|
@ -732,18 +732,19 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void undo_set_updt(interval_set * old_set) {
|
||||
SASSERT(m_xk != null_var);
|
||||
if (m_xk == null_var) return;
|
||||
var x = m_xk;
|
||||
m_ism.dec_ref(m_infeasible[x]);
|
||||
m_infeasible[x] = old_set;
|
||||
if (x < m_infeasible.size()) {
|
||||
m_ism.dec_ref(m_infeasible[x]);
|
||||
m_infeasible[x] = old_set;
|
||||
}
|
||||
}
|
||||
|
||||
void undo_new_stage() {
|
||||
SASSERT(m_xk != null_var);
|
||||
if (m_xk == 0) {
|
||||
m_xk = null_var;
|
||||
}
|
||||
else {
|
||||
else if (m_xk != null_var) {
|
||||
m_xk--;
|
||||
m_assignment.reset(m_xk);
|
||||
}
|
||||
|
|
@ -756,8 +757,8 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void undo_updt_eq(atom * a) {
|
||||
SASSERT(m_xk != null_var);
|
||||
m_var2eq[m_xk] = a;
|
||||
if (m_var2eq.size() > m_xk)
|
||||
m_var2eq[m_xk] = a;
|
||||
}
|
||||
|
||||
template<typename Predicate>
|
||||
|
|
@ -903,15 +904,18 @@ namespace nlsat {
|
|||
*/
|
||||
lbool value(literal l) {
|
||||
lbool val = assigned_value(l);
|
||||
if (val != l_undef)
|
||||
if (val != l_undef) {
|
||||
return val;
|
||||
}
|
||||
bool_var b = l.var();
|
||||
atom * a = m_atoms[b];
|
||||
if (a == 0)
|
||||
if (a == 0) {
|
||||
return l_undef;
|
||||
}
|
||||
var max = a->max_var();
|
||||
if (!m_assignment.is_assigned(max))
|
||||
if (!m_assignment.is_assigned(max)) {
|
||||
return l_undef;
|
||||
}
|
||||
val = to_lbool(m_evaluator.eval(a, l.sign()));
|
||||
TRACE("value_bug", tout << "value of: "; display(tout, l); tout << " := " << val << "\n";
|
||||
tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n";
|
||||
|
|
@ -1168,7 +1172,7 @@ namespace nlsat {
|
|||
void select_witness() {
|
||||
scoped_anum w(m_am);
|
||||
SASSERT(!m_ism.is_full(m_infeasible[m_xk]));
|
||||
m_ism.peek_in_complement(m_infeasible[m_xk], w, m_randomize);
|
||||
m_ism.peek_in_complement(m_infeasible[m_xk], m_is_int[m_xk], w, m_randomize);
|
||||
TRACE("nlsat",
|
||||
tout << "infeasible intervals: "; m_ism.display(tout, m_infeasible[m_xk]); tout << "\n";
|
||||
tout << "assigning "; m_display_var(tout, m_xk); tout << "(x" << m_xk << ") -> " << w << "\n";);
|
||||
|
|
@ -1232,6 +1236,59 @@ namespace nlsat {
|
|||
}
|
||||
}
|
||||
|
||||
lbool search_check() {
|
||||
lbool r = l_undef;
|
||||
while (true) {
|
||||
r = search();
|
||||
if (r != l_true) break;
|
||||
vector<rational> lows;
|
||||
vector<var> vars;
|
||||
|
||||
for (var x = 0; x < num_vars(); x++) {
|
||||
if (m_is_int[x] && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) {
|
||||
scoped_anum v(m_am), vlo(m_am);
|
||||
v = m_assignment.value(x);
|
||||
rational lo;
|
||||
m_am.int_lt(v, vlo);
|
||||
if (!m_am.is_int(vlo)) continue;
|
||||
m_am.to_rational(vlo, lo);
|
||||
// derive tight bounds.
|
||||
while (true) {
|
||||
lo++;
|
||||
if (!m_am.gt(v, lo.to_mpq())) { lo--; break; }
|
||||
}
|
||||
lows.push_back(lo);
|
||||
vars.push_back(x);
|
||||
}
|
||||
}
|
||||
if (lows.empty()) break;
|
||||
|
||||
init_search();
|
||||
for (unsigned i = 0; i < lows.size(); ++i) {
|
||||
rational lo = lows[i];
|
||||
rational hi = lo + rational::one();
|
||||
var x = vars[i];
|
||||
bool is_even = false;
|
||||
polynomial_ref p(m_pm);
|
||||
rational one(1);
|
||||
m_lemma.reset();
|
||||
p = m_pm.mk_linear(1, &one, &x, -lo);
|
||||
poly* p1 = p.get();
|
||||
m_lemma.push_back(~mk_ineq_literal(atom::GT, 1, &p1, &is_even));
|
||||
p = m_pm.mk_linear(1, &one, &x, -hi);
|
||||
poly* p2 = p.get();
|
||||
m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p2, &is_even));
|
||||
|
||||
// perform branch and bound
|
||||
clause * cls = mk_clause(m_lemma.size(), m_lemma.c_ptr(), false, 0);
|
||||
if (cls) {
|
||||
TRACE("nlsat", display(tout << "conflict " << lo << " " << hi, *cls); tout << "\n";);
|
||||
}
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool check() {
|
||||
TRACE("nlsat_smt2", display_smt2(tout););
|
||||
TRACE("nlsat_fd", tout << "is_full_dimensional: " << is_full_dimensional() << "\n";);
|
||||
|
|
@ -1250,7 +1307,7 @@ namespace nlsat {
|
|||
reordered = true;
|
||||
}
|
||||
sort_watched_clauses();
|
||||
lbool r = search();
|
||||
lbool r = search_check();
|
||||
CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout););
|
||||
if (reordered)
|
||||
restore_order();
|
||||
|
|
@ -1929,7 +1986,7 @@ namespace nlsat {
|
|||
for (var x = 0; x < num; x++) {
|
||||
p.push_back(x);
|
||||
}
|
||||
random_gen r(m_random_seed);
|
||||
random_gen r(++m_random_seed);
|
||||
shuffle(p.size(), p.c_ptr(), r);
|
||||
reorder(p.size(), p.c_ptr());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2272,10 +2272,9 @@ namespace smt {
|
|||
process_literal(atom, pol == NEG);
|
||||
}
|
||||
|
||||
void process_or(app * n, polarity p) {
|
||||
unsigned num_args = n->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++)
|
||||
visit_formula(n->get_arg(i), p);
|
||||
void process_and_or(app * n, polarity p) {
|
||||
for (expr* arg : *n)
|
||||
visit_formula(arg, p);
|
||||
}
|
||||
|
||||
void process_ite(app * n, polarity p) {
|
||||
|
|
@ -2306,13 +2305,13 @@ namespace smt {
|
|||
if (is_app(curr)) {
|
||||
if (to_app(curr)->get_family_id() == m_manager.get_basic_family_id() && m_manager.is_bool(curr)) {
|
||||
switch (static_cast<basic_op_kind>(to_app(curr)->get_decl_kind())) {
|
||||
case OP_AND:
|
||||
case OP_IMPLIES:
|
||||
case OP_XOR:
|
||||
UNREACHABLE(); // simplifier eliminated ANDs, IMPLIEs, and XORs
|
||||
break;
|
||||
case OP_OR:
|
||||
process_or(to_app(curr), pol);
|
||||
case OP_AND:
|
||||
process_and_or(to_app(curr), pol);
|
||||
break;
|
||||
case OP_NOT:
|
||||
visit_formula(to_app(curr)->get_arg(0), neg(pol));
|
||||
|
|
|
|||
|
|
@ -711,6 +711,7 @@ namespace smt {
|
|||
if (ctx.is_relevant(get_enode(*it)) && !check_monomial_assignment(*it, computed_epsilon)) {
|
||||
TRACE("non_linear_failed", tout << "check_monomial_assignment failed for:\n" << mk_ismt2_pp(var2expr(*it), get_manager()) << "\n";
|
||||
display_var(tout, *it););
|
||||
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1450,7 +1450,7 @@ namespace smt {
|
|||
// pos < strlen(base)
|
||||
// --> pos + -1*strlen(base) < 0
|
||||
argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
|
||||
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
|
||||
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, mk_strlen(substrBase))),
|
||||
zero)));
|
||||
|
||||
// len >= 0
|
||||
|
|
|
|||
|
|
@ -41,8 +41,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
|
|||
cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
|
||||
cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),
|
||||
cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m),
|
||||
cond(mk_is_nra_probe(), mk_nra_tactic(m),
|
||||
cond(mk_is_lira_probe(), mk_lira_tactic(m, p),
|
||||
cond(mk_is_nra_probe(), mk_nra_tactic(m),
|
||||
cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
|
||||
//cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
|
||||
mk_smt_tactic()))))))))))),
|
||||
|
|
|
|||
|
|
@ -26,8 +26,10 @@ Notes:
|
|||
#include "tactic/bv/max_bv_sharing_tactic.h"
|
||||
#include "sat/tactic/sat_tactic.h"
|
||||
#include "tactic/arith/nla2bv_tactic.h"
|
||||
#include "tactic/arith/elim01_tactic.h"
|
||||
#include "tactic/core/ctx_simplify_tactic.h"
|
||||
#include "tactic/core/cofactor_term_ite_tactic.h"
|
||||
#include "nlsat/tactic/qfnra_nlsat_tactic.h"
|
||||
|
||||
static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
|
||||
params_ref p = p_ref;
|
||||
|
|
@ -61,8 +63,6 @@ static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
|
|||
ctx_simp_p.set_uint("max_depth", 30);
|
||||
ctx_simp_p.set_uint("max_steps", 5000000);
|
||||
|
||||
params_ref simp_p = p_ref;
|
||||
simp_p.set_bool("hoist_mul", true);
|
||||
|
||||
params_ref elim_p = p_ref;
|
||||
elim_p.set_uint("max_memory",20);
|
||||
|
|
@ -73,21 +73,42 @@ static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
|
|||
using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
|
||||
using_params(mk_simplify_tactic(m), pull_ite_p),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p)),
|
||||
using_params(mk_simplify_tactic(m), simp_p));
|
||||
mk_elim01_tactic(m),
|
||||
skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p)));
|
||||
}
|
||||
|
||||
static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
|
||||
params_ref nia2sat_p = p;
|
||||
nia2sat_p.set_uint("nla2bv_max_bv_size", 64);
|
||||
nia2sat_p.set_uint("nla2bv_max_bv_size", 64);
|
||||
params_ref simp_p = p;
|
||||
simp_p.set_bool("hoist_mul", true); // hoist multipliers to create smaller circuits.
|
||||
|
||||
return and_then(mk_nla2bv_tactic(m, nia2sat_p),
|
||||
return and_then(using_params(mk_simplify_tactic(m), simp_p),
|
||||
mk_nla2bv_tactic(m, nia2sat_p),
|
||||
mk_qfnia_bv_solver(m, p),
|
||||
mk_fail_if_undecided_tactic());
|
||||
}
|
||||
|
||||
tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
|
||||
return and_then(mk_qfnia_premable(m, p),
|
||||
or_else(mk_qfnia_sat_solver(m, p),
|
||||
mk_smt_tactic()));
|
||||
static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) {
|
||||
params_ref nia2sat_p = p;
|
||||
nia2sat_p.set_uint("nla2bv_max_bv_size", 64);
|
||||
params_ref simp_p = p;
|
||||
simp_p.set_bool("som", true); // expand into sums of monomials
|
||||
simp_p.set_bool("factor", false);
|
||||
|
||||
|
||||
return and_then(using_params(mk_simplify_tactic(m), simp_p),
|
||||
try_for(mk_qfnra_nlsat_tactic(m, simp_p), 3000),
|
||||
mk_fail_if_undecided_tactic());
|
||||
}
|
||||
|
||||
tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref simp_p = p;
|
||||
simp_p.set_bool("som", true); // expand into sums of monomials
|
||||
|
||||
return and_then(mk_qfnia_premable(m, p),
|
||||
or_else(mk_qfnia_nlsat_solver(m, p),
|
||||
mk_qfnia_sat_solver(m, p),
|
||||
and_then(using_params(mk_simplify_tactic(m), simp_p),
|
||||
mk_smt_tactic())));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -24,7 +24,6 @@ Revision History:
|
|||
#include "qe/qe_tactic.h"
|
||||
#include "qe/qe_lite.h"
|
||||
#include "qe/qsat.h"
|
||||
#include "qe/nlqsat.h"
|
||||
#include "tactic/core/ctx_simplify_tactic.h"
|
||||
#include "smt/tactic/smt_tactic.h"
|
||||
#include "tactic/core/elim_term_ite_tactic.h"
|
||||
|
|
|
|||
Loading…
Reference in a new issue