mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
75b77979fe
|
|
@ -3407,10 +3407,10 @@ sig
|
|||
(** Parse the given string using the SMT-LIB2 parser.
|
||||
|
||||
@return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *)
|
||||
val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
|
||||
val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector
|
||||
|
||||
(** Parse the given file using the SMT-LIB2 parser. *)
|
||||
val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
|
||||
val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector
|
||||
end
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -21,6 +21,8 @@ Notes:
|
|||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/well_sorted.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
#include "ast/used_vars.h"
|
||||
#include "ast/rewriter/var_subst.h"
|
||||
|
||||
#include "ast/fpa/fpa2bv_converter.h"
|
||||
#include "ast/rewriter/fpa_rewriter.h"
|
||||
|
|
@ -230,6 +232,39 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result)
|
|||
result = m_util.mk_fp(sgn, e, s);
|
||||
}
|
||||
|
||||
expr_ref fpa2bv_converter::extra_quantify(expr * e)
|
||||
{
|
||||
used_vars uv;
|
||||
unsigned nv;
|
||||
|
||||
ptr_buffer<sort> new_decl_sorts;
|
||||
sbuffer<symbol> new_decl_names;
|
||||
expr_ref_buffer subst_map(m);
|
||||
|
||||
uv(e);
|
||||
nv = uv.get_num_vars();
|
||||
subst_map.resize(uv.get_max_found_var_idx_plus_1());
|
||||
|
||||
for (unsigned i = 0; i < nv; i++)
|
||||
{
|
||||
if (uv.contains(i)) {
|
||||
TRACE("fpa2bv", tout << "uv[" << i << "] = " << mk_ismt2_pp(uv.get(i), m) << std::endl; );
|
||||
sort * s = uv.get(i);
|
||||
var * v = m.mk_var(i, s);
|
||||
new_decl_sorts.push_back(s);
|
||||
new_decl_names.push_back(symbol(i));
|
||||
subst_map.set(i, v);
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref res(m);
|
||||
var_subst vsubst(m);
|
||||
res = vsubst.operator()(e, nv, subst_map.c_ptr());
|
||||
TRACE("fpa2bv", tout << "subst'd = " << mk_ismt2_pp(res, m) << std::endl; );
|
||||
res = m.mk_forall(nv, new_decl_sorts.c_ptr(), new_decl_names.c_ptr(), res);
|
||||
return res;
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
|
||||
{
|
||||
TRACE("fpa2bv", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; );
|
||||
|
|
@ -252,7 +287,7 @@ void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, e
|
|||
m_bv_util.mk_extract(sbits+ebits-2, sbits-1, bv_app),
|
||||
m_bv_util.mk_extract(sbits-2, 0, bv_app));
|
||||
new_eq = m.mk_eq(fapp, flt_app);
|
||||
m_extra_assertions.push_back(new_eq);
|
||||
m_extra_assertions.push_back(extra_quantify(new_eq));
|
||||
result = flt_app;
|
||||
}
|
||||
else if (m_util.is_rm(rng)) {
|
||||
|
|
@ -263,7 +298,7 @@ void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, e
|
|||
bv_app = m.mk_app(bv_f, num, args);
|
||||
flt_app = m_util.mk_bv2rm(bv_app);
|
||||
new_eq = m.mk_eq(fapp, flt_app);
|
||||
m_extra_assertions.push_back(new_eq);
|
||||
m_extra_assertions.push_back(extra_quantify(new_eq));
|
||||
result = flt_app;
|
||||
}
|
||||
else
|
||||
|
|
|
|||
|
|
@ -220,6 +220,8 @@ private:
|
|||
|
||||
func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range);
|
||||
expr_ref nan_wrap(expr * n);
|
||||
|
||||
expr_ref extra_quantify(expr * e);
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -215,6 +215,12 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
|
|||
new_decl_names.push_back(symbol(name_buffer.c_str()));
|
||||
new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits));
|
||||
}
|
||||
else if (m_conv.is_rm(s)) {
|
||||
name_buffer.reset();
|
||||
name_buffer << n << ".bv";
|
||||
new_decl_names.push_back(symbol(name_buffer.c_str()));
|
||||
new_decl_sorts.push_back(m_conv.bu().mk_sort(3));
|
||||
}
|
||||
else {
|
||||
new_decl_sorts.push_back(s);
|
||||
new_decl_names.push_back(n);
|
||||
|
|
@ -248,6 +254,11 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
|
|||
m_conv.bu().mk_extract(ebits - 1, 0, new_var),
|
||||
m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var));
|
||||
}
|
||||
else if (m_conv.is_rm(s)) {
|
||||
expr_ref new_var(m());
|
||||
new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(3));
|
||||
new_exp = m_conv.fu().mk_bv2rm(new_var);
|
||||
}
|
||||
else
|
||||
new_exp = m().mk_var(t->get_idx(), s);
|
||||
|
||||
|
|
|
|||
|
|
@ -8,4 +8,6 @@ z3_add_component(sat_solver
|
|||
core_tactics
|
||||
sat_tactic
|
||||
solver
|
||||
TACTIC_HEADERS
|
||||
inc_sat_solver.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -28,6 +28,9 @@ solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_
|
|||
|
||||
tactic* mk_psat_tactic(ast_manager& m, params_ref const& p);
|
||||
|
||||
/*
|
||||
ADD_TACTIC('psat', '(try to) solve goal using a parallel SAT solver.', 'mk_psat_tactic(m, p)')
|
||||
*/
|
||||
|
||||
void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights);
|
||||
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ z3_add_component(lp
|
|||
SOURCES
|
||||
binary_heap_priority_queue.cpp
|
||||
binary_heap_upair_queue.cpp
|
||||
bound_propagator.cpp
|
||||
lp_bound_propagator.cpp
|
||||
core_solver_pretty_printer.cpp
|
||||
dense_matrix.cpp
|
||||
eta_matrix.cpp
|
||||
|
|
|
|||
|
|
@ -187,10 +187,6 @@ struct check_return_helper {
|
|||
~check_return_helper() {
|
||||
TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
|
||||
m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows);
|
||||
if (m_r == lia_move::cut || m_r == lia_move::branch) {
|
||||
int_solver * s = m_lar_solver->get_int_solver();
|
||||
// m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k));
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ void clear() {lp_assert(false); // not implemented
|
|||
}
|
||||
|
||||
|
||||
lar_solver::lar_solver() : m_status(lp_status::OPTIMAL),
|
||||
lar_solver::lar_solver() : m_status(lp_status::UNKNOWN),
|
||||
m_infeasible_column_index(-1),
|
||||
m_terms_start_index(1000000),
|
||||
m_mpq_lar_core_solver(m_settings, *this),
|
||||
|
|
@ -1174,6 +1174,7 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
|
|||
std::unordered_set<impq> set_of_different_pairs;
|
||||
std::unordered_set<mpq> set_of_different_singles;
|
||||
delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
|
||||
TRACE("get_model", tout << "delta=" << delta << "size = " << m_mpq_lar_core_solver.m_r_x.size() << std::endl;);
|
||||
for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
|
||||
const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
|
||||
set_of_different_pairs.insert(rp);
|
||||
|
|
|
|||
|
|
@ -542,7 +542,6 @@ public:
|
|||
for (const auto & p : columns_to_subs) {
|
||||
auto it = t.m_coeffs.find(p.first);
|
||||
lp_assert(it != t.m_coeffs.end());
|
||||
const lar_term& lt = get_term(p.second);
|
||||
mpq v = it->second;
|
||||
t.m_coeffs.erase(it);
|
||||
t.m_coeffs[p.second] = v;
|
||||
|
|
|
|||
Loading…
Reference in a new issue