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

fix duplicate class

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-22 00:06:34 -07:00
parent 8476a12c0f
commit 2c69aa0df1
5 changed files with 10 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/opt/opt_context.cpp
View file

@ -311,9 +311,10 @@ namespace opt {
mk_elim_uncnstr_tactic(m), mk_elim_uncnstr_tactic(m),
mk_simplify_tactic(m)); mk_simplify_tactic(m));
opt_params optp(m_params); opt_params optp(m_params);
tactic_ref tac2, tac3;
if (optp.elim_01()) { if (optp.elim_01()) {
tactic_ref tac2 = mk_elim01_tactic(m); tac2 = mk_elim01_tactic(m);
tactic_ref tac3 = mk_lia2card_tactic(m); tac3 = mk_lia2card_tactic(m);
params_ref lia_p; params_ref lia_p;
lia_p.set_bool("compile_equality", optp.pb_compile_equality()); lia_p.set_bool("compile_equality", optp.pb_compile_equality());
tac3->updt_params(lia_p); tac3->updt_params(lia_p);

5
src/smt/theory_pb.cpp
View file

@ -28,11 +28,6 @@ Notes:
#include "sparse_matrix_def.h" #include "sparse_matrix_def.h"
#include "simplex_def.h" #include "simplex_def.h"
namespace simplex {
template class simplex<mpq_ext>;
template class sparse_matrix<mpq_ext>;
};
namespace smt { namespace smt {

6
src/tactic/arith/card2bv_tactic.cpp
View file

@ -104,10 +104,10 @@ struct card2bv_rewriter_cfg : public default_rewriter_cfg {
template class rewriter_tpl<card2bv_rewriter_cfg>; template class rewriter_tpl<card2bv_rewriter_cfg>;
class pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> { class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
card2bv_rewriter_cfg m_cfg; card2bv_rewriter_cfg m_cfg;
public: public:
pb_rewriter(ast_manager & m): card_pb_rewriter(ast_manager & m):
rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg), rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
m_cfg(m) {} m_cfg(m) {}
}; };
@ -116,7 +116,7 @@ class card2bv_tactic : public tactic {
ast_manager & m; ast_manager & m;
params_ref m_params; params_ref m_params;
th_rewriter m_rw1; th_rewriter m_rw1;
pb_rewriter m_rw2; card_pb_rewriter m_rw2;
public: public:

3
src/tactic/core/simplify_tactic.cpp
View file

@ -31,6 +31,9 @@ struct simplify_tactic::imp {
m_num_steps(0) { m_num_steps(0) {
} }
~imp() {
}
ast_manager & m() const { return m_manager; } ast_manager & m() const { return m_manager; }
void set_cancel(bool f) { void set_cancel(bool f) {