address warnings from #836

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/duality/duality_solver.cpp

@@ -3099,7 +3099,7 @@ namespace Duality {
             // Maps nodes of derivation tree into old subtree
             hash_map<Node *, Node*> cex_map;
       
-            virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best){
+            virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool, bool){
                 if(old_node == 0){
                     Heuristic::ChooseExpand(choices,best);
                     return;

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;

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);

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;

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:

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<smt::theory_idl&>(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<smt::theory_rdl&>(opt);
-            return th.mk_ge(m_fm, v, val.get_rational());
+            return th.mk_ge(m_fm, v, val);
         }
 
         // difference logic?

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);

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());
 }
 

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 {

src/smt/theory_arith.h

@@ -1080,7 +1080,7 @@ namespace smt {
         virtual inf_eps_rational<inf_rational> maximize(theory_var v, expr_ref& blocker, bool& has_shared);
         virtual inf_eps_rational<inf_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,

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))));
     }
 
     // -----------------------------------

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<inf_rational> maximize(theory_var v, expr_ref& blocker, bool& has_shared);
         virtual inf_eps_rational<inf_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_gt(theory_var v, inf_eps 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);
         
         // -----------------------------------
         //

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<typename Ext>
-    expr_ref theory_dense_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
+    expr_ref theory_dense_diff_logic<Ext>::mk_gt(theory_var v, inf_eps const& val) {
         return mk_ineq(v, val, true);
     }
 
     template<typename Ext>
     expr_ref theory_dense_diff_logic<Ext>::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<typename Ext>
-    expr_ref theory_dense_diff_logic<Ext>::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) {
+    expr_ref theory_dense_diff_logic<Ext>::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);

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);
+        expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val);
-        virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational 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);
 

src/smt/theory_diff_logic_def.h

@@ -905,7 +905,7 @@ model_value_proc * theory_diff_logic<Ext>::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<typename Ext>
@@ -1242,7 +1242,8 @@ theory_diff_logic<Ext>::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<Ext>::add_objective(app* term) {
 }
 
 template<typename Ext>
-expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) {
+expr_ref theory_diff_logic<Ext>::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<Ext>::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<Ext>::mk_ineq(theory_var v, inf_rational const& val,
 }
 
 template<typename Ext>
-expr_ref theory_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
+expr_ref theory_diff_logic<Ext>::mk_gt(theory_var v, inf_eps const& val) {
     return mk_ineq(v, val, true);
 }
 
 template<typename Ext>
-expr_ref theory_diff_logic<Ext>::mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val) {
+expr_ref theory_diff_logic<Ext>::mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) {
     return mk_ineq(v, val, false);
 }
 

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);
     };

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);

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;

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));
     }
 
     /**