mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

Fix clang compilation issues

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-12 13:28:49 -07:00
parent ec8e3f2aee
commit 5e198f4119
1 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/qe/qe_mbp.h
View file

@ -33,7 +33,7 @@ namespace qe {
struct def { struct def {
expr_ref var, term; 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 { class project_plugin {
@ -69,17 +69,17 @@ namespace qe {
impl * m_impl; impl * m_impl;
public: public:
mbp(ast_manager& m, params_ref const& p = params_ref()); mbp(ast_manager& m, params_ref const& p = params_ref());
~mbp(); ~mbp();
void updt_params(params_ref const& p); void updt_params(params_ref const& p);
static void get_param_descrs(param_descrs & r); static void get_param_descrs(param_descrs & r);
/** /**
\brief \brief
Apply model-based qe on constants provided as vector of variables. Apply model-based qe on constants provided as vector of variables.
Return the updated formula and updated set of variables that were not eliminated. 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); 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); void solve(model& model, app_ref_vector& vars, expr_ref_vector& lits);
/** /**
\brief \brief
Extract literals from formulas based on model. Extract literals from formulas based on model.
*/ */
void extract_literals(model& model, expr_ref_vector& lits); void extract_literals(model& model, expr_ref_vector& lits);
/** /**
\brief \brief
Maximize objective t under current model for constraints in fmls. 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); 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 \brief
Apply spacer friendly MBP. Apply spacer friendly MBP.
Use parameters to control behavior. Use parameters to control behavior.
- reduce_all_selects (false) - reduce_all_selects (false)
- dont_sub (false) - dont_sub (false)
*/ */
void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml); void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml);
}; };
} }
#endif #endif