From 8b53628d67bf48b6d4d9b9339495101e9fca10e8 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 9 Mar 2016 17:01:06 +0000 Subject: [PATCH] remove a few unused decls --- src/muz/pdr/pdr_sym_mux.h | 3 --- src/opt/opt_context.h | 2 -- src/smt/asserted_formulas.h | 1 - 3 files changed, 6 deletions(-) diff --git a/src/muz/pdr/pdr_sym_mux.h b/src/muz/pdr/pdr_sym_mux.h index 78025f26b..13bdb71ec 100644 --- a/src/muz/pdr/pdr_sym_mux.h +++ b/src/muz/pdr/pdr_sym_mux.h @@ -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; }; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 5ddd3be99..482b5d3b4 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -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); diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 8478311dc..f4658f101 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -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; }