From a8f26ae1d8f94b886b4518b261868cfedf756ecd Mon Sep 17 00:00:00 2001 From: Chris Moore <0xCM00@gmail.com> Date: Mon, 15 Oct 2018 10:09:41 -0500 Subject: [PATCH 1/8] Fixes the git submodule error discussed in https://github.com/Z3Prover/z3/pull/1552 --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 2ace973a1..4c1f46ed4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -99,7 +99,7 @@ set(GIT_DIR "${CMAKE_SOURCE_DIR}/.git") if (EXISTS "${GIT_DIR}") # Try to make CMake configure depend on the current git HEAD so that # a re-configure is triggered when the HEAD changes. - add_git_dir_dependency("${GIT_DIR}" ADD_GIT_DEP_SUCCESS) + add_git_dir_dependency("${CMAKE_SOURCE_DIR}" ADD_GIT_DEP_SUCCESS) if (ADD_GIT_DEP_SUCCESS) if (INCLUDE_GIT_HASH) get_git_head_hash("${GIT_DIR}" Z3GITHASH) From 01005a46f69e3d4e0c6012b676a1fe87352e6cb2 Mon Sep 17 00:00:00 2001 From: Matthew Parkinson Date: Mon, 15 Oct 2018 16:59:31 +0100 Subject: [PATCH 2/8] Made it more legal C++17 --- src/muz/base/dl_rule_set.cpp | 3 ++- src/muz/spacer/spacer_context.h | 7 ++++--- src/muz/spacer/spacer_quant_generalizer.cpp | 3 ++- src/qe/qe_vartest.h | 3 ++- 4 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index 80af80266..fdafefcdc 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -696,9 +696,10 @@ namespace datalog { } strats_index++; } + using namespace std::placeholders; //we have managed to topologicaly order all the components SASSERT(std::find_if(m_components.begin(), m_components.end(), - std::bind1st(std::not_equal_to(), (item_set*)0)) == m_components.end()); + std::bind(std::not_equal_to(), (item_set*)0, _1)) == m_components.end()); //reverse the strats array, so that the only the later components would depend on earlier ones std::reverse(m_strats.begin(), m_strats.end()); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 0d8b2daf6..614f46d29 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -28,6 +28,7 @@ Notes: #undef max #endif #include +#include #include "util/scoped_ptr_vector.h" #include "muz/spacer/spacer_manager.h" #include "muz/spacer/spacer_prop_solver.h" @@ -189,7 +190,7 @@ public: } }; -struct lemma_lt_proc : public std::binary_function { +struct lemma_lt_proc : public std::function { bool operator() (lemma *a, lemma *b) { return (a->level () < b->level ()) || (a->level () == b->level () && @@ -727,11 +728,11 @@ inline std::ostream &operator<<(std::ostream &out, pob const &p) { return p.display(out); } -struct pob_lt_proc : public std::binary_function { +struct pob_lt_proc : public std::function { bool operator() (const pob *pn1, const pob *pn2) const; }; -struct pob_gt_proc : public std::binary_function { +struct pob_gt_proc : public std::function { bool operator() (const pob *n1, const pob *n2) const { return pob_lt_proc()(n2, n1); } diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index a11ab4d9e..6443b9b7d 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -19,6 +19,7 @@ Revision History: --*/ +#include #include "muz/spacer/spacer_context.h" #include "muz/spacer/spacer_generalizers.h" @@ -36,7 +37,7 @@ Revision History: using namespace spacer; namespace { -struct index_lt_proc : public std::binary_function { +struct index_lt_proc : public std::function { arith_util m_arith; index_lt_proc(ast_manager &m) : m_arith(m) {} bool operator() (app *a, app *b) { diff --git a/src/qe/qe_vartest.h b/src/qe/qe_vartest.h index 52609893f..04acacbd9 100644 --- a/src/qe/qe_vartest.h +++ b/src/qe/qe_vartest.h @@ -21,9 +21,10 @@ Revision History: #include "ast/ast.h" #include "util/uint_set.h" +#include // TBD: move under qe namespace -class is_variable_proc : public std::unary_function { +class is_variable_proc : public std::function { public: virtual bool operator()(const expr* e) const = 0; }; From 6704a4be0298a0b19c69663965d187cb1b6ccbda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Oct 2018 12:52:19 -0700 Subject: [PATCH 3/8] Revert "Made Z3 compile for C++17 with MSVC" --- src/muz/base/dl_rule_set.cpp | 3 +-- src/muz/spacer/spacer_context.h | 7 +++---- src/muz/spacer/spacer_quant_generalizer.cpp | 3 +-- src/qe/qe_vartest.h | 3 +-- 4 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index fdafefcdc..80af80266 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -696,10 +696,9 @@ namespace datalog { } strats_index++; } - using namespace std::placeholders; //we have managed to topologicaly order all the components SASSERT(std::find_if(m_components.begin(), m_components.end(), - std::bind(std::not_equal_to(), (item_set*)0, _1)) == m_components.end()); + std::bind1st(std::not_equal_to(), (item_set*)0)) == m_components.end()); //reverse the strats array, so that the only the later components would depend on earlier ones std::reverse(m_strats.begin(), m_strats.end()); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 614f46d29..0d8b2daf6 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -28,7 +28,6 @@ Notes: #undef max #endif #include -#include #include "util/scoped_ptr_vector.h" #include "muz/spacer/spacer_manager.h" #include "muz/spacer/spacer_prop_solver.h" @@ -190,7 +189,7 @@ public: } }; -struct lemma_lt_proc : public std::function { +struct lemma_lt_proc : public std::binary_function { bool operator() (lemma *a, lemma *b) { return (a->level () < b->level ()) || (a->level () == b->level () && @@ -728,11 +727,11 @@ inline std::ostream &operator<<(std::ostream &out, pob const &p) { return p.display(out); } -struct pob_lt_proc : public std::function { +struct pob_lt_proc : public std::binary_function { bool operator() (const pob *pn1, const pob *pn2) const; }; -struct pob_gt_proc : public std::function { +struct pob_gt_proc : public std::binary_function { bool operator() (const pob *n1, const pob *n2) const { return pob_lt_proc()(n2, n1); } diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index 6443b9b7d..a11ab4d9e 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -19,7 +19,6 @@ Revision History: --*/ -#include #include "muz/spacer/spacer_context.h" #include "muz/spacer/spacer_generalizers.h" @@ -37,7 +36,7 @@ Revision History: using namespace spacer; namespace { -struct index_lt_proc : public std::function { +struct index_lt_proc : public std::binary_function { arith_util m_arith; index_lt_proc(ast_manager &m) : m_arith(m) {} bool operator() (app *a, app *b) { diff --git a/src/qe/qe_vartest.h b/src/qe/qe_vartest.h index 04acacbd9..52609893f 100644 --- a/src/qe/qe_vartest.h +++ b/src/qe/qe_vartest.h @@ -21,10 +21,9 @@ Revision History: #include "ast/ast.h" #include "util/uint_set.h" -#include // TBD: move under qe namespace -class is_variable_proc : public std::function { +class is_variable_proc : public std::unary_function { public: virtual bool operator()(const expr* e) const = 0; }; From cfd048658278c7079e52a41e9ec34fa2b4ed1abc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20Janiszewski?= Date: Fri, 12 Oct 2018 21:15:31 +0200 Subject: [PATCH 4/8] Catch exceptions by const-reference Exceptions caught by value incur needless cost in C++, most of them can be caught by const-reference, especially as nearly none are actually used. This could allow compiler generate a slightly more efficient code. --- src/ast/datatype_decl_plugin.cpp | 2 +- src/ast/for_each_expr.cpp | 2 +- src/ast/occurs.cpp | 4 ++-- src/cmd_context/check_logic.cpp | 4 ++-- src/cmd_context/cmd_context.cpp | 2 +- src/math/polynomial/algebraic_numbers.cpp | 2 +- src/math/polynomial/polynomial.cpp | 2 +- src/math/subpaving/tactic/subpaving_tactic.cpp | 4 ++-- src/muz/base/dl_rule.cpp | 2 +- src/muz/base/hnf.cpp | 2 +- src/muz/spacer/spacer_context.cpp | 2 +- src/muz/spacer/spacer_farkas_learner.cpp | 2 +- src/muz/spacer/spacer_iuc_proof.cpp | 2 +- src/muz/spacer/spacer_manager.cpp | 2 +- src/muz/spacer/spacer_quant_generalizer.cpp | 2 +- src/muz/spacer/spacer_util.cpp | 2 +- src/muz/tab/tab_context.cpp | 2 +- src/muz/transforms/dl_mk_elim_term_ite.cpp | 2 +- src/opt/opt_context.cpp | 4 ++-- src/parsers/smt2/smt2parser.cpp | 2 +- src/parsers/util/simple_parser.cpp | 2 +- src/qe/qe_datatypes.cpp | 2 +- src/qe/qe_term_graph.cpp | 2 +- src/sat/sat_bdd.cpp | 6 +++--- src/sat/sat_solver.cpp | 2 +- src/smt/smt_model_checker.cpp | 2 +- src/smt/smt_model_finder.cpp | 6 +++--- src/smt/uses_theory.cpp | 2 +- src/tactic/arith/bv2real_rewriter.cpp | 2 +- src/tactic/arith/fix_dl_var_tactic.cpp | 2 +- src/tactic/arith/lia2pb_tactic.cpp | 2 +- src/tactic/arith/pb2bv_tactic.cpp | 2 +- src/tactic/bv/bv1_blaster_tactic.cpp | 2 +- src/tactic/goal.h | 2 +- src/tactic/probe.cpp | 4 ++-- src/tactic/ufbv/ufbv_rewriter.cpp | 2 +- 36 files changed, 45 insertions(+), 45 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 284c4df93..9cb685ccc 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -231,7 +231,7 @@ namespace datatype { } return s; } - catch (invalid_datatype) { + catch (const invalid_datatype &) { m_manager->raise_exception("invalid datatype"); return nullptr; } diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index d46388801..311133e05 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -58,7 +58,7 @@ bool has_skolem_functions(expr * n) { try { for_each_expr(p, n); } - catch (has_skolem_functions_ns::found) { + catch (const has_skolem_functions_ns::found &) { return true; } return false; diff --git a/src/ast/occurs.cpp b/src/ast/occurs.cpp index c76e73748..9ddb2fa56 100644 --- a/src/ast/occurs.cpp +++ b/src/ast/occurs.cpp @@ -58,7 +58,7 @@ bool occurs(expr * n1, expr * n2) { try { quick_for_each_expr(p, n2); } - catch (occurs_namespace::found) { + catch (const occurs_namespace::found &) { return true; } return false; @@ -69,7 +69,7 @@ bool occurs(func_decl * d, expr * n) { try { quick_for_each_expr(p, n); } - catch (occurs_namespace::found) { + catch (const occurs_namespace::found &) { return true; } return false; diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 57e15c6a3..47c919d4a 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -476,7 +476,7 @@ struct check_logic::imp { quick_for_each_expr(*this, n); return true; } - catch (failed) { + catch (const failed &) { return false; } } @@ -495,7 +495,7 @@ struct check_logic::imp { check_sort(f->get_range()); return true; } - catch (failed) { + catch (const failed &) { return false; } } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 8a23f80a0..7b7f81561 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1833,7 +1833,7 @@ void cmd_context::validate_model() { for_each_expr(contains_underspecified, a); for_each_expr(contains_underspecified, r); } - catch (contains_underspecified_op_proc::found) { + catch (const contains_underspecified_op_proc::found &) { continue; } TRACE("model_validate", model_smt2_pp(tout, *this, *md, 0);); diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index aa4fc5a39..528c10537 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -1989,7 +1989,7 @@ namespace algebraic_numbers { TRACE("anum_eval_sign", tout << "all variables are assigned to rationals, value of p: " << r << "\n";); return qm().sign(r); } - catch (opt_var2basic::failed) { + catch (const opt_var2basic::failed &) { // continue } diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 24658fdcf..00a4d0593 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -4493,7 +4493,7 @@ namespace polynomial { } #endif } - catch (sparse_mgcd_failed) { + catch (const sparse_mgcd_failed &) { flet use_prs(m_use_prs_gcd, false); gcd_prs(u, v, x, r); } diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index 935fd5e19..7a3f2e7b3 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -183,7 +183,7 @@ class subpaving_tactic : public tactic { process_clause(g.form(i)); } } - catch (subpaving::exception) { + catch (const subpaving::exception &) { throw tactic_exception("failed to internalize goal into subpaving module"); } } @@ -195,7 +195,7 @@ class subpaving_tactic : public tactic { try { (*m_ctx)(); } - catch (subpaving::exception) { + catch (const subpaving::exception &) { throw tactic_exception("failed building subpaving tree..."); } if (m_display) { diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 0dbeba5b3..fe1f101b1 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -422,7 +422,7 @@ namespace datalog { try { quick_for_each_expr(proc, fml); } - catch (contains_predicate_proc::found) { + catch (const contains_predicate_proc::found &) { return true; } return false; diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp index f0cbc0620..1e6196950 100644 --- a/src/muz/base/hnf.cpp +++ b/src/muz/base/hnf.cpp @@ -219,7 +219,7 @@ private: quick_for_each_expr(m_proc, m_mark1, fml); m_mark1.reset(); } - catch (contains_predicate_proc::found) { + catch (const contains_predicate_proc::found &) { m_mark1.reset(); return true; } diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 30b68ebf6..9a9043f2f 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2737,7 +2737,7 @@ lbool context::solve(unsigned from_lvl) // } } VERIFY (validate ()); - } catch (unknown_exception) + } catch (const unknown_exception &) {} if (m_last_result == l_true) { diff --git a/src/muz/spacer/spacer_farkas_learner.cpp b/src/muz/spacer/spacer_farkas_learner.cpp index d97bee49f..291226b55 100644 --- a/src/muz/spacer/spacer_farkas_learner.cpp +++ b/src/muz/spacer/spacer_farkas_learner.cpp @@ -95,7 +95,7 @@ bool farkas_learner::is_pure_expr(func_decl_set const& symbs, expr* e, ast_manag is_pure_expr_proc proc(symbs, m); try { for_each_expr(proc, e); - } catch (is_pure_expr_proc::non_pure) { + } catch (const is_pure_expr_proc::non_pure &) { return false; } return true; diff --git a/src/muz/spacer/spacer_iuc_proof.cpp b/src/muz/spacer/spacer_iuc_proof.cpp index b6a522b76..949507fb4 100644 --- a/src/muz/spacer/spacer_iuc_proof.cpp +++ b/src/muz/spacer/spacer_iuc_proof.cpp @@ -88,7 +88,7 @@ bool iuc_proof::is_core_pure(expr* e) const try { for_each_expr(proc, e); } - catch (is_pure_expr_proc::non_pure) + catch (const is_pure_expr_proc::non_pure &) {return false;} return true; diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index 856207463..817d620c9 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -247,7 +247,7 @@ bool has_zk_const(expr *e){ try { for_each_expr(p, e); } - catch (has_zk_const_ns::found) { + catch (const has_zk_const_ns::found &) { return true; } return false; diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index a11ab4d9e..f3307a596 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -120,7 +120,7 @@ struct index_lt_proc : public std::binary_function { for (expr *e : v) quick_for_each_expr(fn, visited, e); } - catch (has_nlira_functor::found ) { + catch (const has_nlira_functor::found &) { return true; } return false; diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index ec01218f1..2a5f1e2cc 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -891,7 +891,7 @@ namespace { for_each_expr(cs, fml); return false; } - catch(found) { + catch(const found &) { return true; } } diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index c60c770bf..b5be996dc 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -415,7 +415,7 @@ namespace tb { try { quick_for_each_expr(p, t); } - catch (non_constructor) { + catch (const non_constructor &) { return false; } return true; diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp index f0d9a8843..7e0356e7e 100644 --- a/src/muz/transforms/dl_mk_elim_term_ite.cpp +++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp @@ -57,7 +57,7 @@ namespace { term_ite_proc f(m); try { quick_for_each_expr(f, e); - } catch (term_ite_proc::found) { + } catch (const term_ite_proc::found &) { return true; } return false; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index ff37bfa95..d9c3457fa 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -706,7 +706,7 @@ namespace opt { quick_for_each_expr(proc, visited, f); } } - catch (is_bv::found) { + catch (const is_bv::found &) { return false; } return true; @@ -737,7 +737,7 @@ namespace opt { try { quick_for_each_expr(proc, visited, p); } - catch (is_propositional_fn::found) { + catch (const is_propositional_fn::found &) { return false; } return true; diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 1a16b817b..58b16717d 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -3084,7 +3084,7 @@ namespace smt2 { << ": " << ex.msg() << "\")" << std::endl; exit(ex.error_code()); } - catch (stop_parser_exception) { + catch (const stop_parser_exception &) { m_scanner.stop_caching(); return !found_errors; } diff --git a/src/parsers/util/simple_parser.cpp b/src/parsers/util/simple_parser.cpp index c9d00ebcc..48c42c240 100644 --- a/src/parsers/util/simple_parser.cpp +++ b/src/parsers/util/simple_parser.cpp @@ -118,7 +118,7 @@ bool simple_parser::parse(std::istream & in, expr_ref & result) { if (!result) throw parser_error(); } - catch (parser_error) { + catch (const parser_error &) { warning_msg("parser error"); return false; } diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp index 5499d638d..7ade47458 100644 --- a/src/qe/qe_datatypes.cpp +++ b/src/qe/qe_datatypes.cpp @@ -61,7 +61,7 @@ namespace qe { project_nonrec(model, vars, lits); } } - catch (cant_project) { + catch (const cant_project &) { TRACE("qe", tout << "can't project:" << mk_pp(var, m) << "\n";); return false; } diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index faa9cfed8..97b044f5b 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -62,7 +62,7 @@ namespace qe { is_pure_ns::proc v(is_var); quick_for_each_expr(v, e); } - catch (is_pure_ns::found) { + catch (const is_pure_ns::found &) { return false; } return true; diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index bd1745765..e7b0632d8 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -87,7 +87,7 @@ namespace sat { try { return apply_rec(arg1, arg2, op); } - catch (mem_out) { + catch (const mem_out &) { try_reorder(); if (!first) throw; first = false; @@ -546,7 +546,7 @@ namespace sat { try { return bdd(mk_not_rec(b.root), this); } - catch (mem_out) { + catch (const mem_out &) { try_reorder(); if (!first) throw; first = false; @@ -575,7 +575,7 @@ namespace sat { try { return bdd(mk_ite_rec(c.root, t.root, e.root), this); } - catch (mem_out) { + catch (const mem_out &) { try_reorder(); if (!first) throw; first = false; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index f48ac57a6..2032445ed 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1147,7 +1147,7 @@ namespace sat { } } - catch (abort_solver) { + catch (const abort_solver &) { m_reason_unknown = "sat.giveup"; return l_undef; } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 02b0e16be..58158ec06 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -261,7 +261,7 @@ namespace smt { try { for_each_expr(*this, m_visited, n); } - catch (is_model_value) { + catch (const is_model_value &) { return true; } return false; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index b8b22b067..30ea7b18e 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -177,7 +177,7 @@ namespace smt { try { for_each_expr(*this, m_visited, n); } - catch (is_model_value) { + catch (const is_model_value &) { return true; } return false; @@ -2892,7 +2892,7 @@ namespace smt { try { for_each_expr(oc, m_visited, def); } - catch (occurs) { + catch (const occurs &) { return false; } return true; @@ -2981,7 +2981,7 @@ namespace smt { try { process(f); } - catch (found_satisfied_subset) { + catch (const found_satisfied_subset &) { set_interp(); copy_non_satisfied(qcandidates, new_qs); return true; diff --git a/src/smt/uses_theory.cpp b/src/smt/uses_theory.cpp index 517951a7b..64565dc78 100644 --- a/src/smt/uses_theory.cpp +++ b/src/smt/uses_theory.cpp @@ -41,7 +41,7 @@ bool uses_theory(expr * n, family_id fid, expr_mark & visited) { try { for_each_expr(p, visited, n); } - catch (uses_theory_ns::found) { + catch (const uses_theory_ns::found &) { return true; } return false; diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp index 5839ff7a2..67fca873e 100644 --- a/src/tactic/arith/bv2real_rewriter.cpp +++ b/src/tactic/arith/bv2real_rewriter.cpp @@ -89,7 +89,7 @@ bool bv2real_util::contains_bv2real(expr* e) const { try { for_each_expr(p, e); } - catch (contains_bv2real_proc::found) { + catch (const contains_bv2real_proc::found &) { return true; } return false; diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 669ded49d..d198ce498 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -226,7 +226,7 @@ class fix_dl_var_tactic : public tactic { } return most_occs(); } - catch (failed) { + catch (const failed &) { return nullptr; } } diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index db1c22866..c177f35be 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -156,7 +156,7 @@ class lia2pb_tactic : public tactic { } return true; } - catch (failed) { + catch (const failed &) { return false; } } diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index f36e3a6db..7a64c9f16 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -1034,7 +1034,7 @@ struct is_pb_probe : public probe { return true; } - catch (pb2bv_tactic::non_pb) { + catch (const pb2bv_tactic::non_pb &) { return false; } } diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index b81bc5687..bf9ca4101 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -371,7 +371,7 @@ class bv1_blaster_tactic : public tactic { for_each_expr_core(proc, visited, f); } } - catch (not_target) { + catch (const not_target &) { return false; } return true; diff --git a/src/tactic/goal.h b/src/tactic/goal.h index 4125fab99..fa2f16eb6 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -195,7 +195,7 @@ bool test(goal const & g, Predicate & proc) { for (unsigned i = 0; i < sz; i++) quick_for_each_expr(proc, visited, g.form(i)); } - catch (typename Predicate::found) { + catch (const typename Predicate::found &) { return true; } return false; diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index dcd1dc500..432c9d123 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -524,7 +524,7 @@ public: } return false; } - catch (found) { + catch (const found &) { return true; } } @@ -554,7 +554,7 @@ public: } return false; } - catch (found) { + catch (const found &) { return true; } } diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp index ee8a4605b..66a26be00 100644 --- a/src/tactic/ufbv/ufbv_rewriter.cpp +++ b/src/tactic/ufbv/ufbv_rewriter.cpp @@ -870,7 +870,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { m_cache.insert(p); continue; } - catch (match_args_aux_proc::no_match) { + catch (const match_args_aux_proc::no_match &) { return false; } } From 844f400a62172bb9331ad7c9f3a6446e30fab169 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20Janiszewski?= Date: Tue, 16 Oct 2018 19:30:48 +0200 Subject: [PATCH 5/8] Remove superfluous const from returned types --- src/smt/theory_arith.h | 8 ++++---- src/util/lp/static_matrix.h | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index a2c6c1191..70ce6b397 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -156,9 +156,9 @@ namespace smt { row_entry & operator[](unsigned idx) { return m_entries[idx]; } row_entry const & operator[](unsigned idx) const { return m_entries[idx]; } typename vector::iterator begin_entries() { return m_entries.begin(); } - const typename vector::const_iterator begin_entries() const { return m_entries.begin(); } + typename vector::const_iterator begin_entries() const { return m_entries.begin(); } typename vector::iterator end_entries() { return m_entries.end(); } - const typename vector::const_iterator end_entries() const { return m_entries.end(); } + typename vector::const_iterator end_entries() const { return m_entries.end(); } row_entry & add_row_entry(int & pos_idx); void del_row_entry(unsigned idx); void compress(vector & cols); @@ -195,9 +195,9 @@ namespace smt { col_entry & operator[](unsigned idx) { return m_entries[idx]; } col_entry const & operator[](unsigned idx) const { return m_entries[idx]; } typename svector::iterator begin_entries() { return m_entries.begin(); } - const typename svector::const_iterator begin_entries() const { return m_entries.begin(); } + typename svector::const_iterator begin_entries() const { return m_entries.begin(); } typename svector::iterator end_entries() { return m_entries.end(); } - const typename svector::const_iterator end_entries() const { return m_entries.end(); } + typename svector::const_iterator end_entries() const { return m_entries.end(); } col_entry & add_col_entry(int & pos_idx); void del_col_entry(unsigned idx); }; diff --git a/src/util/lp/static_matrix.h b/src/util/lp/static_matrix.h index bb6cdefc8..1a0ee1bdc 100644 --- a/src/util/lp/static_matrix.h +++ b/src/util/lp/static_matrix.h @@ -93,7 +93,7 @@ public: unsigned m_row; public: ref_row(const static_matrix & m, unsigned row): m_matrix(m), m_row(row) {} - const T operator[](unsigned col) const { return m_matrix.get_elem(m_row, col); } + T operator[](unsigned col) const { return m_matrix.get_elem(m_row, col); } }; public: From dda62ae78c7422e27c60b5bc01b3ff825acbe9fc Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 17 Oct 2018 22:42:57 +0700 Subject: [PATCH 6/8] Use bool literals instead of 0/1. --- src/ackermannization/lackr.cpp | 2 +- src/api/api_fpa.cpp | 36 +++++++++---------- src/api/api_quant.cpp | 4 +-- src/ast/rewriter/bv_bounds.cpp | 6 ++-- .../transforms/dl_mk_array_instantiation.cpp | 2 +- 5 files changed, 25 insertions(+), 25 deletions(-) diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index 8c18df7b2..9130d628c 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -220,7 +220,7 @@ lbool lackr::lazy() { lackr_model_constructor mc(m_m, m_info); push_abstraction(); unsigned ackr_head = 0; - while (1) { + while (true) { m_st.m_it++; checkpoint(); TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";); diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index cdc592527..604267536 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -913,7 +913,7 @@ extern "C" { CHECK_VALID_AST(t, 0); if (sgn == nullptr) { SET_ERROR_CODE(Z3_INVALID_ARG, "sign cannot be a nullpointer"); - return 0; + return false; } ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); @@ -922,13 +922,13 @@ extern "C" { expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); - return 0; + return false; } scoped_mpf val(mpfm); bool r = plugin->is_numeral(to_expr(t), val); if (!r || mpfm.is_nan(val)) { SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); - return 0; + return false; } *sgn = mpfm.sgn(val); return r; @@ -1043,7 +1043,7 @@ extern "C" { CHECK_VALID_AST(t, 0); if (n == nullptr) { SET_ERROR_CODE(Z3_INVALID_ARG, "invalid nullptr argument"); - return 0; + return false; } ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); @@ -1055,7 +1055,7 @@ extern "C" { if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); *n = 0; - return 0; + return false; } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); @@ -1065,10 +1065,10 @@ extern "C" { !mpzm.is_uint64(z)) { SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); *n = 0; - return 0; + return false; } *n = mpzm.get_uint64(z); - return 1; + return true; Z3_CATCH_RETURN(0); } @@ -1121,7 +1121,7 @@ extern "C" { CHECK_VALID_AST(t, 0); if (n == nullptr) { SET_ERROR_CODE(Z3_INVALID_ARG, "invalid null argument"); - return 0; + return false; } ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); @@ -1132,14 +1132,14 @@ extern "C" { if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); *n = 0; - return 0; + return false; } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); *n = 0; - return 0; + return false; } unsigned ebits = val.get().get_ebits(); if (biased) { @@ -1153,7 +1153,7 @@ extern "C" { mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : mpfm.exp(val); } - return 1; + return true; Z3_CATCH_RETURN(0); } @@ -1240,7 +1240,7 @@ extern "C" { fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - return 0; + return false; } return fu.is_nan(to_expr(t)); Z3_CATCH_RETURN(Z3_FALSE); @@ -1254,7 +1254,7 @@ extern "C" { fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - return 0; + return false; } return fu.is_inf(to_expr(t)); Z3_CATCH_RETURN(Z3_FALSE); @@ -1268,7 +1268,7 @@ extern "C" { fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - return 0; + return false; } return fu.is_zero(to_expr(t)); Z3_CATCH_RETURN(Z3_FALSE); @@ -1282,7 +1282,7 @@ extern "C" { fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - return 0; + return false; } return fu.is_normal(to_expr(t)); Z3_CATCH_RETURN(Z3_FALSE); @@ -1296,7 +1296,7 @@ extern "C" { fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - return 0; + return false; } return fu.is_subnormal(to_expr(t)); Z3_CATCH_RETURN(Z3_FALSE); @@ -1310,7 +1310,7 @@ extern "C" { fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - return 0; + return false; } return fu.is_positive(to_expr(t)); Z3_CATCH_RETURN(Z3_FALSE); @@ -1324,7 +1324,7 @@ extern "C" { fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - return 0; + return false; } return fu.is_negative(to_expr(t)); Z3_CATCH_RETURN(Z3_FALSE); diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index 49aa09727..fe9faa2a5 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -132,7 +132,7 @@ extern "C" { unsigned num_decls, Z3_sort const types[], Z3_symbol const decl_names[], Z3_ast body) { - return Z3_mk_quantifier(c, 1, weight, num_patterns, patterns, num_decls, types, decl_names, body); + return Z3_mk_quantifier(c, true, weight, num_patterns, patterns, num_decls, types, decl_names, body); } Z3_ast Z3_API Z3_mk_exists(Z3_context c, @@ -141,7 +141,7 @@ extern "C" { unsigned num_decls, Z3_sort const types[], Z3_symbol const decl_names[], Z3_ast body) { - return Z3_mk_quantifier(c, 0, weight, num_patterns, patterns, num_decls, types, decl_names, body); + return Z3_mk_quantifier(c, false, weight, num_patterns, patterns, num_decls, types, decl_names, body); } Z3_ast Z3_API Z3_mk_lambda(Z3_context c, diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp index f337ca638..f30df7890 100644 --- a/src/ast/rewriter/bv_bounds.cpp +++ b/src/ast/rewriter/bv_bounds.cpp @@ -111,7 +111,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector& nis, bool ne numeral val, val1; unsigned bv_sz1; - if (0) { + if (false) { if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) { return record(to_app(lhs), val, val, negated, nis); } @@ -125,7 +125,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector& nis, bool ne return record(to_app(lhs), numeral::zero(), val, negated, nis); } - if (1) { + if (true) { numeral rhs_val; unsigned rhs_sz; if (m_m.is_eq(e, lhs, rhs) @@ -343,7 +343,7 @@ bool bv_bounds::add_constraint(expr* e) { numeral val, val1; unsigned bv_sz1; - if (0) { + if (false) { if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) { return add_bound_unsigned(to_app(lhs), val, val, negated); } diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp index 6a8f0ce81..626109528 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.cpp +++ b/src/muz/transforms/dl_mk_array_instantiation.cpp @@ -300,7 +300,7 @@ namespace datalog { expr_ref_vector res(m); svector chosen(arg_correspondance.size(), 0u); - while(1) + while(true) { expr_ref_vector new_args(m); for(unsigned i=0;i Date: Wed, 17 Oct 2018 22:47:39 +0700 Subject: [PATCH 7/8] Fix doxygen warnings. --- src/api/c++/z3++.h | 2 +- src/api/z3_optimization.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 1b1820909..7083ae468 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -277,7 +277,7 @@ namespace z3 { */ sort fpa_rounding_mode(); /** - \breif Sets RoundingMode of FloatingPoints. + \brief Sets RoundingMode of FloatingPoints. */ void set_rounding_mode(rounding_mode rm); /** diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index 8f9e2470c..f15d8ff9c 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -146,7 +146,7 @@ extern "C" { Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o); /** - \brief Retrieve the unsat core for the last #Z3_optimize_chec + \brief Retrieve the unsat core for the last #Z3_optimize_check The unsat core is a subset of the assumptions \c a. def_API('Z3_optimize_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE))) From 372cab2c5bc2705eb7c2dee9ed35c01e09691405 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 17 Oct 2018 22:49:39 +0700 Subject: [PATCH 8/8] Fix some typos. --- examples/maxsat/maxsat.c | 4 ++-- src/api/c++/z3++.h | 2 +- src/api/python/z3/z3.py | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c index 5696f5b89..50550106e 100644 --- a/examples/maxsat/maxsat.c +++ b/examples/maxsat/maxsat.c @@ -138,7 +138,7 @@ void assert_hard_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z /** \brief Assert soft constraints stored in the given array. - This funtion will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable. + This function will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable. It will also return an array containing these fresh variables. */ Z3_ast * assert_soft_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs) @@ -565,7 +565,7 @@ int fu_malik_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_as /** \brief Finds the maximal number of assumptions that can be satisfied. - An assumption is any formula preceeded with the :assumption keyword. + An assumption is any formula preceded with the :assumption keyword. "Hard" constraints can be supported by using the :formula keyword. Input: file in SMT-LIB format, and MaxSAT algorithm to be used: 0 - Naive, 1 - Fu&Malik's algo. diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 1b1820909..a355e0233 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -291,7 +291,7 @@ namespace z3 { \brief Return a tuple constructor. \c name is the name of the returned constructor, \c n are the number of arguments, \c names and \c sorts are their projected sorts. - \c projs is an output paramter. It contains the set of projection functions. + \c projs is an output parameter. It contains the set of projection functions. */ func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs); diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 703105356..d466d2e77 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8327,7 +8327,7 @@ def prove(claim, **keywords): print(s.model()) def _solve_html(*args, **keywords): - """Version of funcion `solve` used in RiSE4Fun.""" + """Version of function `solve` used in RiSE4Fun.""" s = Solver() s.set(**keywords) s.add(*args) @@ -8349,7 +8349,7 @@ def _solve_html(*args, **keywords): print(s.model()) def _solve_using_html(s, *args, **keywords): - """Version of funcion `solve_using` used in RiSE4Fun.""" + """Version of function `solve_using` used in RiSE4Fun.""" if __debug__: _z3_assert(isinstance(s, Solver), "Solver object expected") s.set(**keywords) @@ -8372,7 +8372,7 @@ def _solve_using_html(s, *args, **keywords): print(s.model()) def _prove_html(claim, **keywords): - """Version of funcion `prove` used in RiSE4Fun.""" + """Version of function `prove` used in RiSE4Fun.""" if __debug__: _z3_assert(is_bool(claim), "Z3 Boolean expression expected") s = Solver()