From 0708ecb543072f91219a27be229c4d1fee865a11 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 May 2018 09:11:33 -0700 Subject: [PATCH] dealing with compilers that don't take typename in non-template classes Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 22 +-- src/opt/sortmax.cpp | 22 +-- src/sat/ba_solver.h | 22 +-- src/smt/theory_pb.cpp | 4 +- src/tactic/arith/card2bv_tactic.h | 24 ++-- src/test/sorting_network.cpp | 20 +-- src/util/lp/cut_solver.h | 201 ---------------------------- src/util/lp/int_solver.h | 157 ---------------------- src/util/sorting_network.h | 4 +- 9 files changed, 59 insertions(+), 417 deletions(-) delete mode 100644 src/util/lp/cut_solver.h delete mode 100644 src/util/lp/int_solver.h diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 47a8a044a..7da8b2d3f 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -43,8 +43,8 @@ struct pb2bv_rewriter::imp { unsigned m_compile_card; struct card2bv_rewriter { - typedef expr* literal; - typedef ptr_vector literal_vector; + typedef expr* pliteral; + typedef ptr_vector pliteral_vector; psort_nw m_sort; ast_manager& m; imp& m_imp; @@ -861,25 +861,25 @@ struct pb2bv_rewriter::imp { } // definitions used for sorting network - literal mk_false() { return m.mk_false(); } - literal mk_true() { return m.mk_true(); } - literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); } - literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); } - literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } + pliteral mk_false() { return m.mk_false(); } + pliteral mk_true() { return m.mk_true(); } + pliteral mk_max(pliteral a, pliteral b) { return trail(m.mk_or(a, b)); } + pliteral mk_min(pliteral a, pliteral b) { return trail(m.mk_and(a, b)); } + pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } - std::ostream& pp(std::ostream& out, literal lit) { return out << mk_ismt2_pp(lit, m); } + std::ostream& pp(std::ostream& out, pliteral lit) { return out << mk_ismt2_pp(lit, m); } - literal trail(literal l) { + pliteral trail(pliteral l) { m_trail.push_back(l); return l; } - literal fresh(char const* n) { + pliteral fresh(char const* n) { expr_ref fr(m.mk_fresh_const(n, m.mk_bool_sort()), m); m_imp.m_fresh.push_back(to_app(fr)->get_decl()); return trail(fr); } - void mk_clause(unsigned n, literal const* lits) { + void mk_clause(unsigned n, pliteral const* lits) { m_imp.m_lemmas.push_back(::mk_or(m, n, lits)); } diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index 6ea7feaad..9c45e42a2 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -30,8 +30,8 @@ namespace opt { class sortmax : public maxsmt_solver_base { public: - typedef expr* literal; - typedef ptr_vector literal_vector; + typedef expr* pliteral; + typedef ptr_vector pliteral_vector; psort_nw m_sort; expr_ref_vector m_trail; func_decl_ref_vector m_fresh; @@ -126,19 +126,19 @@ namespace opt { } // definitions used for sorting network - literal mk_false() { return m.mk_false(); } - literal mk_true() { return m.mk_true(); } - literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); } - literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); } - literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } + pliteral mk_false() { return m.mk_false(); } + pliteral mk_true() { return m.mk_true(); } + pliteral mk_max(pliteral a, pliteral b) { return trail(m.mk_or(a, b)); } + pliteral mk_min(pliteral a, pliteral b) { return trail(m.mk_and(a, b)); } + pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } - std::ostream& pp(std::ostream& out, literal lit) { return out << mk_pp(lit, m); } + std::ostream& pp(std::ostream& out, pliteral lit) { return out << mk_pp(lit, m); } - literal trail(literal l) { + pliteral trail(pliteral l) { m_trail.push_back(l); return l; } - literal fresh(char const* n) { + pliteral fresh(char const* n) { expr_ref fr(m.mk_fresh_const(n, m.mk_bool_sort()), m); func_decl* f = to_app(fr)->get_decl(); m_fresh.push_back(f); @@ -146,7 +146,7 @@ namespace opt { return trail(fr); } - void mk_clause(unsigned n, literal const* lits) { + void mk_clause(unsigned n, pliteral const* lits) { s().assert_expr(mk_or(m, n, lits)); } diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 14482eabb..07e7cfd58 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -242,23 +242,23 @@ namespace sat { unsigned_vector m_pb_undef; struct ba_sort { - typedef typename sat::literal literal; - typedef typename sat::literal_vector literal_vector; + typedef sat::literal pliteral; + typedef sat::literal_vector pliteral_vector; ba_solver& s; - literal m_true; - literal_vector m_lits; + pliteral m_true; + pliteral_vector m_lits; ba_sort(ba_solver& s): s(s), m_true(null_literal) {} - literal mk_false(); - literal mk_true(); - literal mk_not(literal l); - literal fresh(char const*); - literal mk_max(literal l1, literal l2); - literal mk_min(literal l1, literal l2); + pliteral mk_false(); + pliteral mk_true(); + pliteral mk_not(pliteral l); + pliteral fresh(char const*); + pliteral mk_max(pliteral l1, pliteral l2); + pliteral mk_min(pliteral l1, pliteral l2); void mk_clause(unsigned n, literal const* lits); - std::ostream& pp(std::ostream& out, literal l) const; + std::ostream& pp(std::ostream& out, pliteral l) const; }; ba_sort m_ba; psort_nw m_sort; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 1e5b35fbf..9fc33a6a9 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1392,8 +1392,8 @@ namespace smt { ast_manager& m; theory_pb& th; pb_util pb; - typedef smt::literal literal; - typedef smt::literal_vector literal_vector; + typedef smt::literal pliteral; + typedef smt::literal_vector pliteral_vector; psort_expr(context& c, theory_pb& th): ctx(c), diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h index e11c78048..5e2051b50 100644 --- a/src/tactic/arith/card2bv_tactic.h +++ b/src/tactic/arith/card2bv_tactic.h @@ -34,8 +34,8 @@ namespace pb { class card2bv_rewriter { public: - typedef expr* literal; - typedef ptr_vector literal_vector; + typedef expr* pliteral; + typedef ptr_vector pliteral_vector; private: ast_manager& m; arith_util au; @@ -54,7 +54,7 @@ namespace pb { bool is_and(func_decl* f); bool is_atmost1(func_decl* f, unsigned sz, expr * const* args, expr_ref& result); expr_ref mk_atmost1(unsigned sz, expr * const* args); - void mk_at_most_1_small(bool last, unsigned n, literal const* xs, expr_ref_vector& result, expr_ref_vector& ors); + void mk_at_most_1_small(bool last, unsigned n, pliteral const* xs, expr_ref_vector& result, expr_ref_vector& ors); public: card2bv_rewriter(ast_manager& m); @@ -62,15 +62,15 @@ namespace pb { void mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas); // definitions used for sorting network - literal mk_false() { return m.mk_false(); } - literal mk_true() { return m.mk_true(); } - literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); } - literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); } - literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } - std::ostream& pp(std::ostream& out, literal lit); - literal fresh(); - literal trail(literal l); - void mk_clause(unsigned n, literal const* lits); + pliteral mk_false() { return m.mk_false(); } + pliteral mk_true() { return m.mk_true(); } + pliteral mk_max(pliteral a, pliteral b) { return trail(m.mk_or(a, b)); } + pliteral mk_min(pliteral a, pliteral b) { return trail(m.mk_and(a, b)); } + pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } + std::ostream& pp(std::ostream& out, pliteral lit); + pliteral fresh(); + pliteral trail(pliteral l); + void mk_clause(unsigned n, pliteral const* lits); }; diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index e3bf2d653..f5c415c04 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -152,30 +152,30 @@ struct ast_ext2 { expr_ref_vector m_clauses; expr_ref_vector m_trail; ast_ext2(ast_manager& m):m(m), m_clauses(m), m_trail(m) {} - typedef expr* literal; - typedef ptr_vector literal_vector; + typedef expr* pliteral; + typedef ptr_vector pliteral_vector; expr* trail(expr* e) { m_trail.push_back(e); return e; } - literal mk_false() { return m.mk_false(); } - literal mk_true() { return m.mk_true(); } - literal mk_max(literal a, literal b) { + pliteral mk_false() { return m.mk_false(); } + pliteral mk_true() { return m.mk_true(); } + pliteral mk_max(pliteral a, pliteral b) { return trail(m.mk_or(a, b)); } - literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); } - literal mk_not(literal a) { if (m.is_not(a,a)) return a; + pliteral mk_min(pliteral a, pliteral b) { return trail(m.mk_and(a, b)); } + pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } - std::ostream& pp(std::ostream& out, literal lit) { + std::ostream& pp(std::ostream& out, pliteral lit) { return out << mk_pp(lit, m); } - literal fresh(char const* n) { + pliteral fresh(char const* n) { return trail(m.mk_fresh_const(n, m.mk_bool_sort())); } - void mk_clause(unsigned n, literal const* lits) { + void mk_clause(unsigned n, pliteral const* lits) { m_clauses.push_back(mk_or(m, n, lits)); } }; diff --git a/src/util/lp/cut_solver.h b/src/util/lp/cut_solver.h deleted file mode 100644 index 18da0b88b..000000000 --- a/src/util/lp/cut_solver.h +++ /dev/null @@ -1,201 +0,0 @@ -/* - Copyright (c) 2017 Microsoft Corporation - Author: Nikolaj Bjorner, Lev Nachmanson -*/ -#pragma once -#include "util/vector.h" -#include "util/trace.h" -#include "util/lp/lp_settings.h" -namespace lp { -template -class cut_solver { - - struct ineq { // we only have less or equal, which is enough for integral variables - mpq m_bound; - vector> m_term; - ineq(vector>& term, mpq bound):m_bound(bound),m_term(term) { - } - }; - - vector m_ineqs; - - enum class lbool { - l_false, // false - l_true, // true - l_undef // undef - }; - - enum class literal_type { - BOOL, - INEQ, - BOUND - }; - - struct literal { - literal_type m_tag; - bool m_sign; // true means the pointed inequality is negated, or bound is negated, or boolean value is negated - - unsigned m_id; - unsigned m_index_of_ineq; // index into m_ineqs - bool m_bool_val; // used if m_tag is equal to BOOL - mpq m_bound; // used if m_tag is BOUND - literal(bool sign, bool val): m_tag(literal_type::BOOL), - m_bool_val(val){ - } - literal(bool sign, unsigned index_of_ineq) : m_tag(literal_type::INEQ), m_index_of_ineq(index_of_ineq) {} - }; - - bool lhs_is_int(const vector> & lhs) const { - for (auto & p : lhs) - if (p.first.is_int() == false) return false; - return true; - } - - public: - void add_ineq(vector> & lhs, mpq rhs) { - lp_assert(lhs_is_int(lhs)); - lp_assert(rhs.is_int()); - m_ineqs.push_back(ineq(lhs, rhs)); - } - - - bool m_inconsistent; // tracks if state is consistent - unsigned m_scope_lvl; // tracks the number of case splits - - svector m_trail; - // backtracking state from the SAT solver: - struct scope { - unsigned m_trail_lim; // pointer into assignment stack - unsigned m_clauses_to_reinit_lim; // ignore for now - bool m_inconsistent; // really needed? - }; - - svector m_scopes; - - bool at_base_lvl() const { return m_scope_lvl == 0; } - - lbool check() { - init_search(); - propagate(); - while (true) { - lbool r = bounded_search(); - if (r != lbool::l_undef) - return r; - - restart(); - simplify_problem(); - if (check_inconsistent()) return lbool::l_false; - gc(); - } - } - - cut_solver() { - } - - void init_search() { - // TBD - // initialize data-structures - } - - void simplify_problem() { - // no-op - } - - void gc() { - // no-op - } - - void restart() { - // no-op for now - } - - bool check_inconsistent() { - // TBD - return false; - } - - lbool bounded_search() { - while (true) { - checkpoint(); - bool done = false; - while (!done) { - lbool is_sat = propagate_and_backjump_step(done); - if (is_sat != lbool::l_true) return is_sat; - } - - gc(); - - if (!decide()) { - lbool is_sat = final_check(); - if (is_sat != lbool::l_undef) { - return is_sat; - } - } - } - } - - void checkpoint() { - // check for cancelation - } - - void cleanup() { - } - - lbool propagate_and_backjump_step(bool& done) { - done = true; - propagate(); - if (!inconsistent()) - return lbool::l_true; - if (!resolve_conflict()) - return lbool::l_false; - if (at_base_lvl()) { - cleanup(); // cleaner may propagate frozen clauses - if (inconsistent()) { - TRACE("sat", tout << "conflict at level 0\n";); - return lbool::l_false; - } - gc(); - } - done = false; - return lbool::l_true; - } - - lbool final_check() { - // there are no more case splits, and all clauses are satisfied. - // prepare the model for external consumption. - return lbool::l_true; - } - - - bool resolve_conflict() { - while (true) { - bool r = resolve_conflict_core(); - // after pop, clauses are reinitialized, - // this may trigger another conflict. - if (!r) - return false; - if (!inconsistent()) - return true; - } - } - - bool resolve_conflict_core() { - // this is where the main action is. - return true; - } - - void propagate() { - // this is where the main action is. - } - - bool decide() { - // this is where the main action is. - // pick the next variable and bound or value on the variable. - // return false if all variables have been assigned. - return false; - } - - bool inconsistent() const { return m_inconsistent; } - -}; -} diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h deleted file mode 100644 index 56ddf16fd..000000000 --- a/src/util/lp/int_solver.h +++ /dev/null @@ -1,157 +0,0 @@ -/* - Copyright (c) 2017 Microsoft Corporation - Author: Lev Nachmanson -*/ -#pragma once -#include "util/lp/lp_settings.h" -#include "util/lp/static_matrix.h" -#include "util/lp/iterator_on_row.h" -#include "util/lp/int_set.h" -#include "util/lp/lar_term.h" -#include "util/lp/cut_solver.h" -#include "util/lp/lar_constraints.h" - -namespace lp { -class lar_solver; -template -struct lp_constraint; -enum class lia_move { - ok, - branch, - cut, - conflict, - continue_with_check, - give_up -}; - -struct explanation { - vector> m_explanation; - void push_justification(constraint_index j, const mpq& v) { - m_explanation.push_back(std::make_pair(v, j)); - } -}; - -class int_solver { -public: - // fields - lar_solver *m_lar_solver; - int_set m_old_values_set; - vector m_old_values_data; - unsigned m_branch_cut_counter; - - // methods - int_solver(lar_solver* lp); - int_set& inf_int_set(); - const int_set& inf_int_set() const; - // main function to check that solution provided by lar_solver is valid for integral values, - // or provide a way of how it can be adjusted. - lia_move check(lar_term& t, mpq& k, explanation& ex); - bool move_non_basic_column_to_bounds(unsigned j); - lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex); -private: - - // how to tighten bounds for integer variables. - - bool gcd_test_for_row(static_matrix> & A, unsigned i, explanation &); - - // gcd test - // 5*x + 3*y + 6*z = 5 - // suppose x is fixed at 2. - // so we have 10 + 3(y + 2z) = 5 - // 5 = -3(y + 2z) - // this is unsolvable because 5/3 is not an integer. - // so we create a lemma that rules out this condition. - // - bool gcd_test(explanation & ); // returns false in case of failure. Creates a theory lemma in case of failure. - - // create goromy cuts - // either creates a conflict or a bound. - - // branch and bound: - // decide what to branch and bound on - // creates a fresh inequality. - - bool branch(const lp_constraint & new_inequality); - bool ext_gcd_test(iterator_on_row & it, - mpq const & least_coeff, - mpq const & lcm_den, - mpq const & consts, - explanation & ex); - void fill_explanation_from_fixed_columns(iterator_on_row & it, explanation &); - void add_to_explanation_from_fixed_or_boxed_column(unsigned j, explanation &); - void patch_int_infeasible_non_basic_column(unsigned j); - void patch_int_infeasible_nbasic_columns(); - bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m); - linear_combination_iterator * get_column_iterator(unsigned j); - const impq & low_bound(unsigned j) const; - const impq & upper_bound(unsigned j) const; - bool is_int(unsigned j) const; - bool is_real(unsigned j) const; - bool is_base(unsigned j) const; - bool is_boxed(unsigned j) const; - bool is_fixed(unsigned j) const; - bool is_free(unsigned j) const; - bool value_is_int(unsigned j) const; - void set_value_for_nbasic_column(unsigned j, const impq & new_val); - void set_value_for_nbasic_column_ignore_old_values(unsigned j, const impq & new_val); - bool non_basic_columns_are_at_bounds() const; - void failed(); - bool is_feasible() const; - const impq & get_value(unsigned j) const; - void display_column(std::ostream & out, unsigned j) const; - bool inf_int_set_is_correct() const; - void update_column_in_int_inf_set(unsigned j); - bool column_is_int_inf(unsigned j) const; - void trace_inf_rows() const; - int find_inf_int_base_column(); - int find_inf_int_boxed_base_column_with_smallest_range(); - lp_settings& settings(); - bool move_non_basic_columns_to_bounds(); - void branch_infeasible_int_var(unsigned); - lia_move mk_gomory_cut(lar_term& t, mpq& k,explanation & ex, unsigned inf_col, linear_combination_iterator& iter); - lia_move report_conflict_from_gomory_cut(mpq & k); - void adjust_term_and_k_for_some_ints_case_gomory(lar_term& t, mpq& k, mpq& lcm_den); - void init_check_data(); - bool constrain_free_vars(linear_combination_iterator * r); - lia_move proceed_with_gomory_cut(lar_term& t, mpq& k, explanation& ex, unsigned j); - int find_free_var_in_gomory_row(linear_combination_iterator& iter); - bool is_gomory_cut_target(linear_combination_iterator &iter); - bool at_bound(unsigned j) const; - bool at_low(unsigned j) const; - bool at_upper(unsigned j) const; - bool has_low(unsigned j) const; - bool has_upper(unsigned j) const; - unsigned row_of_basic_column(unsigned j) const; - inline static bool is_rational(const impq & n) { - return is_zero(n.y); - } - - inline static - mpq fractional_part(const impq & n) { - lp_assert(is_rational(n)); - return n.x - floor(n.x); - } - void real_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term& t, explanation & ex, unsigned inf_column); - void int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term& t, explanation& ex, mpq & lcm_den, unsigned inf_column); - constraint_index column_upper_bound_constraint(unsigned j) const; - constraint_index column_low_bound_constraint(unsigned j) const; - void display_row_info(std::ostream & out, unsigned row_index) const; - void gomory_cut_adjust_t_and_k(vector> & pol, lar_term & t, mpq &k, bool num_ints, mpq &lcm_den); - bool current_solution_is_inf_on_cut(const lar_term& t, const mpq& k) const; -public: - bool shift_var(unsigned j, unsigned range); -private: - unsigned random(); - bool has_inf_int() const; - lia_move create_branch_on_column(int j, lar_term& t, mpq& k, bool free_column) const; -public: - void display_inf_or_int_inf_columns(std::ostream & out) const; - template - void fill_cut_solver(cut_solver & cs); - template - void fill_cut_solver_for_constraint(const lar_base_constraint*, cut_solver& ); - template - void get_int_coeffs_from_constraint(const lar_base_constraint* c, vector>& coeff, T & rs); - -}; -} diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index 38c595125..f2906b00c 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -141,8 +141,8 @@ Notes: // Described in Abio et.al. CP 2013. template class psort_nw { - typedef typename psort_expr::literal literal; - typedef typename psort_expr::literal_vector literal_vector; + typedef typename psort_expr::pliteral literal; + typedef typename psort_expr::pliteral_vector literal_vector; sorting_network_config m_cfg; class vc {