mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

remove a few unused decls

Browse source
This commit is contained in:
Nuno Lopes 2016-03-09 17:01:06 +00:00
parent 402e132ce5
commit 8b53628d67
3 changed files with 0 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/pdr/pdr_sym_mux.h
View file

@ -93,7 +93,6 @@ private:
std::string get_suffix(unsigned i);
void ensure_tuple_size(func_decl * prim, unsigned sz);
expr_ref isolate_o_idx(expr* e, unsigned idx) const;
public:
sym_mux(ast_manager & m);
@ -241,8 +240,6 @@ public:
func_decl * const * begin_prim_preds() const { return m_prim_preds.begin(); }
func_decl * const * end_prim_preds() const { return m_prim_preds.end(); }
void get_muxed_cube_from_model(const model_core & model, expr_ref_vector & res) const;
std::string pp_model(const model_core & mdl) const;
};
}

2
src/opt/opt_context.h
View file

@ -226,8 +226,6 @@ namespace opt {
virtual bool verify_model(unsigned id, model* mdl, rational const& v);
private:
void validate_feasibility(maxsmt& ms);
lbool execute(objective const& obj, bool committed, bool scoped);
lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);
lbool execute_maxsat(symbol const& s, bool committed, bool scoped);

1
src/smt/asserted_formulas.h
View file

@ -106,7 +106,6 @@ public:
void assert_expr(expr * e, proof * in_pr);
void assert_expr(expr * e);
void reset();
void set_cancel_flag(bool f);
void push_scope();
void pop_scope(unsigned num_scopes);
bool inconsistent() const { return m_inconsistent; }