mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
enable logic parameter update to configure SMTLIB logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7f51ecab37
commit
67397bf71e
|
@ -832,7 +832,7 @@ extern "C" {
|
|||
pp_params params;
|
||||
pp.set_simplify_implies(params.simplify_implies());
|
||||
ast* a1 = to_ast(a);
|
||||
pp.set_logic(mk_c(c)->fparams().m_logic.c_str());
|
||||
pp.set_logic(mk_c(c)->fparams().m_logic);
|
||||
if (!is_expr(a1)) {
|
||||
buffer << mk_pp(a1, mk_c(c)->m());
|
||||
break;
|
||||
|
@ -880,7 +880,7 @@ extern "C" {
|
|||
std::ostringstream buffer;
|
||||
ast_smt_pp pp(mk_c(c)->m());
|
||||
pp.set_benchmark_name(name);
|
||||
pp.set_logic(logic);
|
||||
pp.set_logic(logic?symbol(logic):symbol::null);
|
||||
pp.set_status(status);
|
||||
pp.add_attributes(attributes);
|
||||
pp_params params;
|
||||
|
|
|
@ -67,7 +67,7 @@ public:
|
|||
void set_source_info(const char* si) { if (si) m_source_info = si; }
|
||||
void set_status(const char* s) { if (s) m_status = s; }
|
||||
void set_category(const char* c) { if (c) m_category = c; }
|
||||
void set_logic(const char* l) { if (l) m_logic = l; }
|
||||
void set_logic(symbol const& l) { m_logic = l; }
|
||||
void add_attributes(const char* s) { if (s) m_attributes += s; }
|
||||
void add_assumption(expr* n) { m_assumptions.push_back(n); }
|
||||
void add_assumption_star(expr* n) { m_assumptions_star.push_back(n); }
|
||||
|
|
|
@ -1280,7 +1280,7 @@ void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecede
|
|||
ast_smt_pp pp(m);
|
||||
pp.set_benchmark_name("lemma");
|
||||
pp.set_status("unsat");
|
||||
pp.set_logic(m_logic.c_str());
|
||||
pp.set_logic(symbol(m_logic.c_str()));
|
||||
for (unsigned i = 0; i < num_antecedents; i++)
|
||||
pp.add_assumption(antecedents[i]);
|
||||
expr_ref n(m);
|
||||
|
|
|
@ -160,7 +160,7 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
|
|||
ast_smt_pp pp(ctx.m());
|
||||
cmd_is_declared isd(ctx);
|
||||
pp.set_is_declared(&isd);
|
||||
pp.set_logic(ctx.get_logic().str().c_str());
|
||||
pp.set_logic(ctx.get_logic());
|
||||
pp.display_smt2(ctx.regular_stream(), pr);
|
||||
ctx.regular_stream() << std::endl;
|
||||
});
|
||||
|
|
|
@ -102,7 +102,7 @@ public:
|
|||
}
|
||||
if (!failed && m_params.get_bool("print_proofs", false)) {
|
||||
ast_smt_pp pp(ctx.m());
|
||||
pp.set_logic(ctx.get_logic().str().c_str());
|
||||
pp.set_logic(ctx.get_logic());
|
||||
pp.display_expr_smt2(ctx.regular_stream(), pr.get());
|
||||
ctx.regular_stream() << std::endl;
|
||||
}
|
||||
|
|
|
@ -162,7 +162,7 @@ namespace opt {
|
|||
std::stringstream file_name;
|
||||
file_name << "opt_solver" << ++m_dump_count << ".smt2";
|
||||
std::ofstream buffer(file_name.str().c_str());
|
||||
to_smt2_benchmark(buffer, num_assumptions, assumptions, "opt_solver", "");
|
||||
to_smt2_benchmark(buffer, num_assumptions, assumptions, "opt_solver");
|
||||
buffer.close();
|
||||
IF_VERBOSE(1, verbose_stream() << "(created benchmark: " << file_name.str() << "...";
|
||||
verbose_stream().flush(););
|
||||
|
@ -400,7 +400,7 @@ namespace opt {
|
|||
unsigned num_assumptions,
|
||||
expr * const * assumptions,
|
||||
char const * name,
|
||||
char const * logic,
|
||||
symbol const& logic,
|
||||
char const * status,
|
||||
char const * attributes) {
|
||||
ast_smt_pp pp(m);
|
||||
|
|
|
@ -135,7 +135,7 @@ namespace opt {
|
|||
void to_smt2_benchmark(std::ofstream & buffer,
|
||||
unsigned num_assumptions, expr * const * assumptions,
|
||||
char const * name = "benchmarks",
|
||||
char const * logic = "", char const * status = "unknown", char const * attributes = "");
|
||||
symbol const& logic = symbol::null, char const * status = "unknown", char const * attributes = "");
|
||||
|
||||
private:
|
||||
lbool decrement_value(unsigned i, inf_eps& val);
|
||||
|
|
|
@ -38,7 +38,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
|
|||
m_rlimit = p.rlimit();
|
||||
m_max_conflicts = p.max_conflicts();
|
||||
m_core_validate = p.core_validate();
|
||||
m_logic = _p.get_str("logic", m_logic.c_str());
|
||||
m_logic = _p.get_sym("logic", m_logic);
|
||||
model_params mp(_p);
|
||||
m_model_compact = mp.compact();
|
||||
if (_p.get_bool("arith.greatest_error_pivot", false))
|
||||
|
|
|
@ -160,7 +160,7 @@ struct smt_params : public preprocessor_params,
|
|||
//
|
||||
// -----------------------------------
|
||||
bool m_smtlib_dump_lemmas;
|
||||
std::string m_logic;
|
||||
symbol m_logic;
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
|
@ -260,7 +260,7 @@ struct smt_params : public preprocessor_params,
|
|||
m_old_clause_relevancy(6),
|
||||
m_inv_clause_decay(1),
|
||||
m_smtlib_dump_lemmas(false),
|
||||
m_logic("AUFLIA"),
|
||||
m_logic(symbol::null),
|
||||
m_profile_res_sub(false),
|
||||
m_display_bool_var2expr(false),
|
||||
m_display_ll_bool_var2expr(false),
|
||||
|
|
|
@ -1218,18 +1218,18 @@ namespace smt {
|
|||
|
||||
void display_hot_bool_vars(std::ostream & out) const;
|
||||
|
||||
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, const char * logic = "AUFLIRA") const;
|
||||
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
|
||||
|
||||
void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, const char * logic = "AUFLIRA") const;
|
||||
void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
|
||||
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
|
||||
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
|
||||
literal consequent = false_literal, const char * logic = "AUFLIRA") const;
|
||||
literal consequent = false_literal, symbol const& logic = symbol::null) const;
|
||||
|
||||
void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
|
||||
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
|
||||
literal consequent = false_literal, const char * logic = "AUFLIRA") const;
|
||||
literal consequent = false_literal, symbol const& logic = symbol::null) const;
|
||||
|
||||
void display_assignment_as_smtlib2(std::ostream& out, const char * logic = "AUFLIRA") const;
|
||||
void display_assignment_as_smtlib2(std::ostream& out, symbol const& logic = symbol::null) const;
|
||||
|
||||
void display_normalized_enodes(std::ostream & out) const;
|
||||
|
||||
|
@ -1367,7 +1367,7 @@ namespace smt {
|
|||
|
||||
app * mk_eq_atom(expr * lhs, expr * rhs);
|
||||
|
||||
bool set_logic(symbol logic) { return m_setup.set_logic(logic); }
|
||||
bool set_logic(symbol const& logic) { return m_setup.set_logic(logic); }
|
||||
|
||||
void register_plugin(simplifier_plugin * s);
|
||||
|
||||
|
|
|
@ -215,7 +215,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void context::display_assignment_as_smtlib2(std::ostream& out, char const* logic) const {
|
||||
void context::display_assignment_as_smtlib2(std::ostream& out, symbol const& logic) const {
|
||||
ast_smt_pp pp(m_manager);
|
||||
pp.set_benchmark_name("lemma");
|
||||
pp.set_status("unknown");
|
||||
|
@ -421,7 +421,7 @@ namespace smt {
|
|||
st.display_internal(out);
|
||||
}
|
||||
|
||||
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent, const char * logic) const {
|
||||
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
|
||||
ast_smt_pp pp(m_manager);
|
||||
pp.set_benchmark_name("lemma");
|
||||
pp.set_status("unsat");
|
||||
|
@ -441,7 +441,7 @@ namespace smt {
|
|||
|
||||
#define BUFFER_SZ 128
|
||||
|
||||
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, const char * logic) const {
|
||||
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
|
||||
char buffer[BUFFER_SZ];
|
||||
#ifdef _WINDOWS
|
||||
sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt2", g_lemma_id);
|
||||
|
@ -456,7 +456,7 @@ namespace smt {
|
|||
|
||||
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
|
||||
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
|
||||
literal consequent, const char * logic) const {
|
||||
literal consequent, symbol const& logic) const {
|
||||
ast_smt_pp pp(m_manager);
|
||||
pp.set_benchmark_name("lemma");
|
||||
pp.set_status("unsat");
|
||||
|
@ -480,7 +480,7 @@ namespace smt {
|
|||
|
||||
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
|
||||
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
|
||||
literal consequent, const char * logic) const {
|
||||
literal consequent, symbol const& logic) const {
|
||||
char buffer[BUFFER_SZ];
|
||||
#ifdef _WINDOWS
|
||||
sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt2", g_lemma_id);
|
||||
|
|
|
@ -1433,7 +1433,7 @@ namespace smt {
|
|||
literal_buffer tmp;
|
||||
neg_literals(num_lits, lits, tmp);
|
||||
SASSERT(tmp.size() == num_lits);
|
||||
display_lemma_as_smt_problem(tmp.size(), tmp.c_ptr(), false_literal, m_fparams.m_logic.c_str());
|
||||
display_lemma_as_smt_problem(tmp.size(), tmp.c_ptr(), false_literal, m_fparams.m_logic);
|
||||
}
|
||||
mk_clause(num_lits, lits, js);
|
||||
}
|
||||
|
|
|
@ -2872,7 +2872,7 @@ namespace smt {
|
|||
if (dump_lemmas()) {
|
||||
TRACE("arith", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";);
|
||||
ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
|
||||
ante.eqs().size(), ante.eqs().c_ptr(), l, 0);
|
||||
ante.eqs().size(), ante.eqs().c_ptr(), l);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -2881,7 +2881,7 @@ namespace smt {
|
|||
context & ctx = get_context();
|
||||
if (dump_lemmas()) {
|
||||
ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
|
||||
ante.eqs().size(), ante.eqs().c_ptr(), l, 0);
|
||||
ante.eqs().size(), ante.eqs().c_ptr(), l);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -597,7 +597,7 @@ namespace smt {
|
|||
ctx.set_conflict(ctx.mk_justification(theory_conflict_justification(get_id(), r, antecedents.size(), antecedents.c_ptr())));
|
||||
|
||||
if (dump_lemmas()) {
|
||||
ctx.display_lemma_as_smt_problem(antecedents.size(), antecedents.c_ptr(), false_literal, "");
|
||||
ctx.display_lemma_as_smt_problem(antecedents.size(), antecedents.c_ptr(), false_literal);
|
||||
}
|
||||
|
||||
return;
|
||||
|
|
|
@ -632,7 +632,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
|
|||
}
|
||||
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
|
||||
if (dump_lemmas()) {
|
||||
char const * logic = m_is_lia ? "QF_LIA" : "QF_LRA";
|
||||
symbol logic(m_is_lia ? "QF_LIA" : "QF_LRA");
|
||||
ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
|
||||
}
|
||||
|
||||
|
@ -678,7 +678,7 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
|
|||
);
|
||||
|
||||
if (dump_lemmas()) {
|
||||
char const * logic = m_is_lia ? "QF_LIA" : "QF_LRA";
|
||||
symbol logic(m_is_lia ? "QF_LIA" : "QF_LRA");
|
||||
ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
|
||||
}
|
||||
|
||||
|
|
|
@ -223,7 +223,7 @@ namespace smt {
|
|||
);
|
||||
|
||||
if (m_params.m_arith_dump_lemmas) {
|
||||
char const * logic = m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA";
|
||||
symbol logic(m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA");
|
||||
ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue