mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

Introduce and use labels_vec

Browse source
This commit is contained in:
Doug Woos 2017-01-30 15:50:34 -08:00
parent 3791810920
commit 8196173e29
6 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/cmd_context/tactic_cmds.cpp
View file

@ -167,7 +167,7 @@ public:
struct check_sat_tactic_result : public simple_check_sat_result { struct check_sat_tactic_result : public simple_check_sat_result {
public: public:
svector<symbol> labels; labels_vec labels;
check_sat_tactic_result(ast_manager & m) : simple_check_sat_result(m) { check_sat_tactic_result(ast_manager & m) : simple_check_sat_result(m) {
} }
@ -181,8 +181,6 @@ public:
} }
}; };
typedef svector<symbol> & labels_ref;
class check_sat_using_tactict_cmd : public exec_given_tactic_cmd { class check_sat_using_tactict_cmd : public exec_given_tactic_cmd {
public: public:
check_sat_using_tactict_cmd(): check_sat_using_tactict_cmd():
@ -205,7 +203,7 @@ public:
ast_manager & m = ctx.m(); ast_manager & m = ctx.m();
unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout); unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout);
unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit);
svector<symbol> labels; labels_vec labels;
goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
assert_exprs_from(ctx, *g); assert_exprs_from(ctx, *g);
TRACE("check_sat_using", g->display(tout);); TRACE("check_sat_using", g->display(tout););

2
src/solver/tactic2solver.cpp
View file

@ -144,7 +144,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
proof_ref pr(m); proof_ref pr(m);
expr_dependency_ref core(m); expr_dependency_ref core(m);
std::string reason_unknown = "unknown"; std::string reason_unknown = "unknown";
svector<symbol> labels; labels_vec labels;
try { try {
switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) { switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) {
case l_true: case l_true:

6
src/tactic/model_converter.cpp
View file

@ -33,7 +33,7 @@ public:
this->m_c1->operator()(m, 0); this->m_c1->operator()(m, 0);
} }
virtual void operator()(svector<symbol> & r, unsigned goal_idx) { virtual void operator()(labels_vec & r, unsigned goal_idx) {
this->m_c2->operator()(r, goal_idx); this->m_c2->operator()(r, goal_idx);
this->m_c1->operator()(r, 0); this->m_c1->operator()(r, 0);
} }
@ -83,7 +83,7 @@ public:
UNREACHABLE(); UNREACHABLE();
} }
virtual void operator()(svector<symbol> & r, unsigned goal_idx) { virtual void operator()(labels_vec & r, unsigned goal_idx) {
unsigned num = this->m_c2s.size(); unsigned num = this->m_c2s.size();
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
if (goal_idx < this->m_szs[i]) { if (goal_idx < this->m_szs[i]) {
@ -142,7 +142,7 @@ public:
m = m_model; m = m_model;
} }
virtual void operator()(svector<symbol> & r, unsigned goal_idx) { virtual void operator()(labels_vec & r, unsigned goal_idx) {
r.append(m_labels.size(), m_labels.c_ptr()); r.append(m_labels.size(), m_labels.c_ptr());
} }

4
src/tactic/model_converter.h
View file

@ -23,6 +23,8 @@ Notes:
#include"converter.h" #include"converter.h"
#include"ref.h" #include"ref.h"
class labels_vec : public svector<symbol> {};
class model_converter : public converter { class model_converter : public converter {
public: public:
virtual void operator()(model_ref & m) {} // TODO: delete virtual void operator()(model_ref & m) {} // TODO: delete
@ -33,7 +35,7 @@ public:
operator()(m); operator()(m);
} }
virtual void operator()(svector<symbol> & r, unsigned goal_idx) {} virtual void operator()(labels_vec & r, unsigned goal_idx) {}
virtual model_converter * translate(ast_translation & translator) = 0; virtual model_converter * translate(ast_translation & translator) = 0;
}; };

2
src/tactic/tactic.cpp
View file

@ -174,7 +174,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve
} }
} }
lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector<symbol> & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
bool models_enabled = g->models_enabled(); bool models_enabled = g->models_enabled();
bool proofs_enabled = g->proofs_enabled(); bool proofs_enabled = g->proofs_enabled();
bool cores_enabled = g->unsat_core_enabled(); bool cores_enabled = g->unsat_core_enabled();

2
src/tactic/tactic.h
View file

@ -153,7 +153,7 @@ public:
#define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;) #define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;)
void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core); void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector<symbol> & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
// Throws an exception if goal \c in requires proof generation. // Throws an exception if goal \c in requires proof generation.
void fail_if_proof_generation(char const * tactic_name, goal_ref const & in); void fail_if_proof_generation(char const * tactic_name, goal_ref const & in);