diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index b3a96aea4..1869b74ce 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -3099,7 +3099,7 @@ namespace Duality { // Maps nodes of derivation tree into old subtree hash_map cex_map; - virtual void ChooseExpand(const std::set &choices, std::set &best){ + virtual void ChooseExpand(const std::set &choices, std::set &best, bool, bool){ if(old_node == 0){ Heuristic::ChooseExpand(choices,best); return; diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 3c1a7bfaa..ba841c84f 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -119,7 +119,6 @@ namespace datalog { virtual expr_ref try_get_formula(func_decl * pred) const = 0; virtual void display_output_facts(rule_set const& rules, std::ostream & out) const = 0; virtual void display_facts(std::ostream & out) const = 0; - virtual void display_profile(std::ostream& out) = 0; virtual void restrict_predicates(func_decl_set const& predicates) = 0; virtual bool result_contains_fact(relation_fact const& f) = 0; virtual void add_fact(func_decl* pred, relation_fact const& fact) = 0; diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index f353fbf2e..9878f3a9e 100644 --- a/src/muz/base/dl_engine_base.h +++ b/src/muz/base/dl_engine_base.h @@ -66,7 +66,7 @@ namespace datalog { } virtual void reset_statistics() {} - virtual void display_profile(std::ostream& out) const {} + virtual void display_profile(std::ostream& out) {} virtual void collect_statistics(statistics& st) const {} virtual unsigned get_num_levels(func_decl* pred) { throw default_exception(std::string("get_num_levels is not supported for ") + m_name); diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp index d42d071aa..00a25d169 100644 --- a/src/muz/rel/dl_table_relation.cpp +++ b/src/muz/rel/dl_table_relation.cpp @@ -54,7 +54,7 @@ namespace datalog { return alloc(table_relation, *this, s, t); } - relation_base * table_relation_plugin::mk_full(const relation_signature & s, func_decl* p, family_id kind) { + relation_base * table_relation_plugin::mk_full_relation(const relation_signature & s, func_decl* p, family_id kind) { table_signature tsig; if(!get_manager().relation_signature_to_table(s, tsig)) { return 0; diff --git a/src/muz/rel/dl_table_relation.h b/src/muz/rel/dl_table_relation.h index 8266995da..56ca509fa 100644 --- a/src/muz/rel/dl_table_relation.h +++ b/src/muz/rel/dl_table_relation.h @@ -49,7 +49,7 @@ namespace datalog { virtual bool can_handle_signature(const relation_signature & s); virtual relation_base * mk_empty(const relation_signature & s); - virtual relation_base * mk_full(const relation_signature & s, func_decl* p, family_id kind); + virtual relation_base * mk_full_relation(const relation_signature & s, func_decl* p, family_id kind); relation_base * mk_from_table(const relation_signature & s, table_base * t); protected: diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 868303660..42129be70 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -57,7 +57,7 @@ namespace opt { opt_solver::~opt_solver() { } - void opt_solver::updt_params(params_ref & _p) { + void opt_solver::updt_params(params_ref const & _p) { opt_params p(_p); m_dump_benchmarks = p.dump_benchmarks(); m_params.updt_params(_p); @@ -383,13 +383,13 @@ namespace opt { if (typeid(smt::theory_idl) == typeid(opt)) { smt::theory_idl& th = dynamic_cast(opt); - return th.mk_ge(m_fm, v, val.get_rational()); + return th.mk_ge(m_fm, v, val); } if (typeid(smt::theory_rdl) == typeid(opt) && val.get_infinitesimal().is_zero()) { smt::theory_rdl& th = dynamic_cast(opt); - return th.mk_ge(m_fm, v, val.get_rational()); + return th.mk_ge(m_fm, v, val); } // difference logic? diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 094023ba2..cdaad3cf2 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -88,7 +88,7 @@ namespace opt { virtual ~opt_solver(); virtual solver* translate(ast_manager& m, params_ref const& p); - virtual void updt_params(params_ref & p); + virtual void updt_params(params_ref const& p); virtual void collect_param_descrs(param_descrs & r); virtual void collect_statistics(statistics & st) const; virtual void assert_expr(expr * t); diff --git a/src/smt/proto_model/numeral_factory.cpp b/src/smt/proto_model/numeral_factory.cpp index a67b6c075..413cc1b9e 100644 --- a/src/smt/proto_model/numeral_factory.cpp +++ b/src/smt/proto_model/numeral_factory.cpp @@ -31,7 +31,7 @@ arith_factory::arith_factory(ast_manager & m): arith_factory::~arith_factory() { } -app * arith_factory::mk_value(rational const & val, bool is_int) { +app * arith_factory::mk_num_value(rational const & val, bool is_int) { return numeral_factory::mk_value(val, is_int ? m_util.mk_int() : m_util.mk_real()); } diff --git a/src/smt/proto_model/numeral_factory.h b/src/smt/proto_model/numeral_factory.h index 3c5d41040..e0d3cf6b5 100644 --- a/src/smt/proto_model/numeral_factory.h +++ b/src/smt/proto_model/numeral_factory.h @@ -38,7 +38,7 @@ public: arith_factory(ast_manager & m); virtual ~arith_factory(); - app * mk_value(rational const & val, bool is_int); + app * mk_num_value(rational const & val, bool is_int); }; class bv_factory : public numeral_factory { diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 39f991c72..5a0f8db95 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -1080,7 +1080,7 @@ namespace smt { virtual inf_eps_rational maximize(theory_var v, expr_ref& blocker, bool& has_shared); virtual inf_eps_rational value(theory_var v); virtual theory_var add_objective(app* term); - virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val); + expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val); void enable_record_conflict(expr* bound); void record_conflict(unsigned num_lits, literal const * lits, unsigned num_eqs, enode_pair const * eqs, diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index a08ee50ab..a8d771d1a 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3231,7 +3231,7 @@ namespace smt { TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";); num = floor(num); } - return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(var2expr(v)))); + return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(var2expr(v)))); } // ----------------------------------- diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h index 1b1653eb7..c2be89bc3 100644 --- a/src/smt/theory_dense_diff_logic.h +++ b/src/smt/theory_dense_diff_logic.h @@ -198,7 +198,7 @@ namespace smt { void del_vars(unsigned old_num_vars); void init_model(); bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective); - expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict); + expr_ref mk_ineq(theory_var v, inf_eps const& val, bool is_strict); #ifdef Z3DEBUG bool check_vector_sizes() const; bool check_matrix() const; @@ -270,8 +270,8 @@ namespace smt { virtual inf_eps_rational maximize(theory_var v, expr_ref& blocker, bool& has_shared); virtual inf_eps_rational value(theory_var v); virtual theory_var add_objective(app* term); - virtual expr_ref mk_gt(theory_var v, inf_rational const& val); - virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val); + virtual expr_ref mk_gt(theory_var v, inf_eps const& val); + expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val); // ----------------------------------- // diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index fd388b5bd..877d4f659 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -828,7 +828,7 @@ namespace smt { SASSERT(v != null_theory_var); numeral const & val = m_assignment[v]; rational num = val.get_rational().to_rational() + m_epsilon * val.get_infinitesimal().to_rational(); - return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v))); + return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int(v))); } // TBD: code is common to both sparse and dense difference logic solvers. @@ -1002,9 +1002,10 @@ namespace smt { m_assignment[i] = a; // TBD: if epsilon is != 0, then adjust a by some small fraction. } - blocker = mk_gt(v, r); + inf_eps result(rational(0), r); + blocker = mk_gt(v, result); IF_VERBOSE(10, verbose_stream() << blocker << "\n";); - return inf_eps(rational(0), r); + return result; } default: TRACE("opt", tout << "unbounded\n"; ); @@ -1034,18 +1035,18 @@ namespace smt { } template - expr_ref theory_dense_diff_logic::mk_gt(theory_var v, inf_rational const& val) { + expr_ref theory_dense_diff_logic::mk_gt(theory_var v, inf_eps const& val) { return mk_ineq(v, val, true); } template expr_ref theory_dense_diff_logic::mk_ge( - filter_model_converter& fm, theory_var v, inf_rational const& val) { + filter_model_converter& fm, theory_var v, inf_eps const& val) { return mk_ineq(v, val, false); } template - expr_ref theory_dense_diff_logic::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) { + expr_ref theory_dense_diff_logic::mk_ineq(theory_var v, inf_eps const& val, bool is_strict) { ast_manager& m = get_manager(); objective_term const& t = m_objectives[v]; expr_ref e(m), f(m), f2(m); diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 6fb9e6454..f47e61548 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -324,14 +324,15 @@ namespace smt { virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared); virtual inf_eps value(theory_var v); virtual theory_var add_objective(app* term); - virtual expr_ref mk_gt(theory_var v, inf_rational const& val); - virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val); + expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val); bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective); private: - expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict); + expr_ref mk_gt(theory_var v, inf_eps const& val); + + expr_ref mk_ineq(theory_var v, inf_eps const& val, bool is_strict); virtual void new_eq_eh(theory_var v1, theory_var v2, justification& j); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 98f94c6d2..372786c01 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -905,7 +905,7 @@ model_value_proc * theory_diff_logic::mk_value(enode * n, model_generator & numeral val = m_graph.get_assignment(v); rational num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational(); TRACE("arith", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); - return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(n->get_owner()))); + return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(n->get_owner()))); } template @@ -1242,7 +1242,8 @@ theory_diff_logic::maximize(theory_var v, expr_ref& blocker, bool& has_shar rational r = rational(val.first) + m_delta*rational(val.second); m_graph.set_assignment(i, numeral(r)); } - blocker = mk_gt(v, r); + inf_eps r1(rational(0), r); + blocker = mk_gt(v, r1); return inf_eps(rational(0), r + m_objective_consts[v]); } default: @@ -1273,7 +1274,7 @@ theory_var theory_diff_logic::add_objective(app* term) { } template -expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) { +expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_eps const& val, bool is_strict) { ast_manager& m = get_manager(); objective_term const& t = m_objectives[v]; expr_ref e(m), f(m), f2(m); @@ -1304,7 +1305,7 @@ expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_rational const& val, return f; } - inf_rational new_val = val; // - inf_rational(m_objective_consts[v]); + inf_eps new_val = val; // - inf_rational(m_objective_consts[v]); e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f)); if (new_val.get_infinitesimal().is_neg()) { @@ -1328,12 +1329,12 @@ expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_rational const& val, } template -expr_ref theory_diff_logic::mk_gt(theory_var v, inf_rational const& val) { +expr_ref theory_diff_logic::mk_gt(theory_var v, inf_eps const& val) { return mk_ineq(v, val, true); } template -expr_ref theory_diff_logic::mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val) { +expr_ref theory_diff_logic::mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { return mk_ineq(v, val, false); } diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index 58e039140..421e6feca 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -33,7 +33,6 @@ namespace smt { virtual inf_eps value(theory_var) = 0; virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) = 0; virtual theory_var add_objective(app* term) = 0; - virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return expr_ref(*((ast_manager*)0)); } bool is_linear(ast_manager& m, expr* term); bool is_numeral(arith_util& a, expr* term); }; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 3be3fd5f8..4f2683ca9 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2236,7 +2236,7 @@ bool theory_seq::add_stoi_axiom(expr* e) { expr* n; rational val; VERIFY(m_util.str.is_stoi(e, n)); - if (get_value(e, val) && !m_stoi_axioms.contains(val)) { + if (get_num_value(e, val) && !m_stoi_axioms.contains(val)) { m_stoi_axioms.insert(val); if (!val.is_minus_one()) { app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m); @@ -2260,7 +2260,7 @@ bool theory_seq::add_itos_axiom(expr* e) { rational val; expr* n; VERIFY(m_util.str.is_itos(e, n)); - if (get_value(n, val)) { + if (get_num_value(n, val)) { if (!m_itos_axioms.contains(val)) { m_itos_axioms.insert(val); app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m); @@ -2741,7 +2741,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { } else if (m_util.str.is_itos(e, e1)) { rational val; - if (get_value(e1, val)) { + if (get_num_value(e1, val)) { TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";); expr_ref num(m), res(m); num = m_autil.mk_numeral(val, true); @@ -3024,7 +3024,7 @@ void theory_seq::add_itos_length_axiom(expr* len) { unsigned num_char1 = 1, num_char2 = 1; rational len1, len2; rational ten(10); - if (get_value(n, len1)) { + if (get_num_value(n, len1)) { bool neg = len1.is_neg(); if (neg) len1.neg(); num_char1 = neg?2:1; @@ -3038,7 +3038,7 @@ void theory_seq::add_itos_length_axiom(expr* len) { } SASSERT(len1 <= upper); } - if (get_value(len, len2) && len2.is_unsigned()) { + if (get_num_value(len, len2) && len2.is_unsigned()) { num_char2 = len2.get_unsigned(); } unsigned num_char = std::max(num_char1, num_char2); @@ -3172,7 +3172,7 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) { } } -bool theory_seq::get_value(expr* e, rational& val) const { +bool theory_seq::get_num_value(expr* e, rational& val) const { context& ctx = get_context(); theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); expr_ref _val(m); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 21955bf30..0e06997ad 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -512,7 +512,7 @@ namespace smt { // arithmetic integration - bool get_value(expr* s, rational& val) const; + bool get_num_value(expr* s, rational& val) const; bool lower_bound(expr* s, rational& lo) const; bool upper_bound(expr* s, rational& hi) const; bool get_length(expr* s, rational& val) const; diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index ff295d5a3..5f370c29c 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -901,7 +901,7 @@ namespace smt { bool is_int = a.is_int(n->get_owner()); rational num = mk_value(v, is_int); TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); - return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int)); + return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int)); } /**