From 5e198f4119097b8718baae4f37ca9768ce159753 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 12 Jun 2018 13:28:49 -0700 Subject: [PATCH] Fix clang compilation issues --- src/qe/qe_mbp.h | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index c35351fb3..0bb8ba00f 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -33,7 +33,7 @@ namespace qe { struct def { expr_ref var, term; - def(expr_ref& v, expr_ref& t): var(v), term(t) {} + def(const expr_ref& v, expr_ref& t): var(v), term(t) {} }; class project_plugin { @@ -69,17 +69,17 @@ namespace qe { impl * m_impl; public: mbp(ast_manager& m, params_ref const& p = params_ref()); - + ~mbp(); void updt_params(params_ref const& p); - + static void get_param_descrs(param_descrs & r); - + /** \brief - Apply model-based qe on constants provided as vector of variables. - Return the updated formula and updated set of variables that were not eliminated. + Apply model-based qe on constants provided as vector of variables. + Return the updated formula and updated set of variables that were not eliminated. */ void operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls); @@ -90,13 +90,13 @@ namespace qe { void solve(model& model, app_ref_vector& vars, expr_ref_vector& lits); /** - \brief + \brief Extract literals from formulas based on model. */ void extract_literals(model& model, expr_ref_vector& lits); /** - \brief + \brief Maximize objective t under current model for constraints in fmls. */ opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt); @@ -105,11 +105,11 @@ namespace qe { \brief Apply spacer friendly MBP. Use parameters to control behavior. - - reduce_all_selects (false) - - dont_sub (false) + - reduce_all_selects (false) + - dont_sub (false) */ void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml); }; } -#endif +#endif