From 67397bf71e9d48a0adbf3e9f47fe572c95c368ad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 Mar 2016 09:48:24 -0800 Subject: [PATCH] enable logic parameter update to configure SMTLIB logic Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 4 ++-- src/ast/ast_smt_pp.h | 2 +- src/ast/proof_checker/proof_checker.cpp | 2 +- src/cmd_context/basic_cmds.cpp | 2 +- src/cmd_context/simplify_cmd.cpp | 2 +- src/opt/opt_solver.cpp | 4 ++-- src/opt/opt_solver.h | 2 +- src/smt/params/smt_params.cpp | 2 +- src/smt/params/smt_params.h | 4 ++-- src/smt/smt_context.h | 12 ++++++------ src/smt/smt_context_pp.cpp | 10 +++++----- src/smt/smt_internalizer.cpp | 2 +- src/smt/theory_arith_core.h | 4 ++-- src/smt/theory_dense_diff_logic_def.h | 2 +- src/smt/theory_diff_logic_def.h | 4 ++-- src/smt/theory_utvpi_def.h | 2 +- 16 files changed, 30 insertions(+), 30 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 0203439ae..e30da1aa1 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -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; diff --git a/src/ast/ast_smt_pp.h b/src/ast/ast_smt_pp.h index 59b1596fa..e88465828 100644 --- a/src/ast/ast_smt_pp.h +++ b/src/ast/ast_smt_pp.h @@ -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); } diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 16546db1e..45223cdb7 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -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); diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 957cbef4e..450bfbf5b 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -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; }); diff --git a/src/cmd_context/simplify_cmd.cpp b/src/cmd_context/simplify_cmd.cpp index 9f0d67142..1c249ce1f 100644 --- a/src/cmd_context/simplify_cmd.cpp +++ b/src/cmd_context/simplify_cmd.cpp @@ -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; } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 097cf5f3e..eff70e48e 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -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); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 128836089..3c58a4fec 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -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); diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 8dc0bb7d6..8222c3d60 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -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)) diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index a60f026bc..9c1eec649 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -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), diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index b918be2cf..8b2453e31 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -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); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 1f5566a03..a3079f52b 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -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); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 5cad7547e..a420d85d9 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -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); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index dcd2cb316..301b5d14d 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -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); } } diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 28ee4b025..fd388b5bd 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -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; diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index f444fe88e..cca78e9c0 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -632,7 +632,7 @@ void theory_diff_logic::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::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); } diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 22b19b0b1..d5ed4e825 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -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); }