From 908f09a9df876a4de3a3c45281f72000bb849004 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 1 Mar 2016 08:46:43 -0800
Subject: [PATCH 1/3] update logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/params/smt_params.cpp | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index c31b2fb6d..3158ea9a1 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -38,6 +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_smtlib_logic = _p.get_symbol("logic", m_smtlib_logic);
model_params mp(_p);
m_model_compact = mp.compact();
if (_p.get_bool("arith.greatest_error_pivot", false))
From 7f51ecab373ffe889e61823c74fa670b3c710b19 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 1 Mar 2016 09:26:14 -0800
Subject: [PATCH 2/3] enable logic parameter update to configure SMTLIB logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/api_ast.cpp | 2 +-
src/smt/params/smt_params.cpp | 2 +-
src/smt/params/smt_params.h | 4 ++--
src/smt/smt_internalizer.cpp | 2 +-
src/smt/tactic/smt_tactic.cpp | 5 +++++
5 files changed, 10 insertions(+), 5 deletions(-)
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index db10c8bb3..0203439ae 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_smtlib_logic.c_str());
+ pp.set_logic(mk_c(c)->fparams().m_logic.c_str());
if (!is_expr(a1)) {
buffer << mk_pp(a1, mk_c(c)->m());
break;
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 3158ea9a1..8dc0bb7d6 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_smtlib_logic = _p.get_symbol("logic", m_smtlib_logic);
+ m_logic = _p.get_str("logic", m_logic.c_str());
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 8127b7eef..a60f026bc 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_smtlib_logic;
+ std::string 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_smtlib_logic("AUFLIA"),
+ m_logic("AUFLIA"),
m_profile_res_sub(false),
m_display_bool_var2expr(false),
m_display_ll_bool_var2expr(false),
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 78a6b85cb..5cad7547e 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_smtlib_logic.c_str());
+ display_lemma_as_smt_problem(tmp.size(), tmp.c_ptr(), false_literal, m_fparams.m_logic.c_str());
}
mk_clause(num_lits, lits, js);
}
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index f50f0afa5..afa4cf98f 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -123,6 +123,11 @@ public:
TRACE("smt_tactic", tout << this << "\nupdt_params: " << p << "\n";);
updt_params_core(p);
fparams().updt_params(p);
+ symbol logic = p.get_sym(symbol("logic"), symbol::null);
+ if (logic != symbol::null) {
+ if (m_ctx) m_ctx->set_logic(logic);
+ m_logic = logic;
+ }
SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
}
From 67397bf71e9d48a0adbf3e9f47fe572c95c368ad Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 1 Mar 2016 09:48:24 -0800
Subject: [PATCH 3/3] enable logic parameter update to configure SMTLIB logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
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<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);
}
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);
}