Merge branch 'master' of https://github.com/z3prover/z3

src/api/api_algebraic.cpp

@@ -344,7 +344,7 @@ extern "C" {
         scoped_anum_vector const & m_as;
     public:
         vector_var2anum(scoped_anum_vector & as):m_as(as) {}
-        virtual ~vector_var2anum() {}
+        ~vector_var2anum() override {}
         algebraic_numbers::manager & m() const override { return m_as.m(); }
         bool contains(polynomial::var x) const override { return static_cast<unsigned>(x) < m_as.size(); }
         algebraic_numbers::anum const & operator()(polynomial::var x) const override { return m_as.get(x); }

src/api/api_context.h

@@ -58,7 +58,7 @@ namespace api {
         solver_ref   s;
     public:
         seq_expr_solver(ast_manager& m, params_ref const& p): m(m), p(p) {}
-        lbool check_sat(expr* e) {
+        lbool check_sat(expr* e) override {
             if (!s) {
                 s = mk_smt_solver(m, p, symbol("ALL"));
             }

src/api/z3_api.h

@@ -3387,6 +3387,7 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty);
 
+#if 0
     /**
        \brief Create an integer numeral from a vector of unsigned numerals.
 
@@ -3394,12 +3395,12 @@ extern "C" {
        \param sign - true if positive, false if negative
        \param n - length of array of numerals
        \param nums - array of numerals
-       \param srt - sort of numeral (int, real, bit-vector).
+       \param s - sort of numeral (int, real, bit-vector).
 
        future_('Z3_mk_mpz_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(SORT)))
      */
 
-    //Z3_ast Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort s);
+    Z3_ast Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort s);
 
     /**
        \brief Create a rational numeral from a vector of unsigned numerals.
@@ -3416,7 +3417,8 @@ extern "C" {
        future_('Z3_mk_mpq_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(UINT), _in_array(4, UINT)))
      */
 
-    // Z3_ast Z3_mk_mpq_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]);
+    Z3_ast Z3_mk_mpq_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]);
+#endif
 
     /**
        \brief Create a real from a fraction.
@@ -6982,7 +6984,7 @@ extern "C" {
     /**
         Create uninterpreted function declaration for the user propagator.
         When expressions using the function are created by the solver invoke a callback
-        to \ref \Z3_solver_propagate_created with arguments
+        to \ref Z3_solver_propagate_created with arguments
         1. context and callback solve
         2. declared_expr: expression using function that was used as the top-level symbol
         3. declared_id: a unique identifier (unique within the current scope) to track the expression.

src/ast/fpa/fpa2bv_converter.h

@@ -239,7 +239,7 @@ class fpa2bv_converter_wrapped : public fpa2bv_converter {
     fpa2bv_converter_wrapped(ast_manager & m, th_rewriter& rw) :
         fpa2bv_converter(m),
         m_rw(rw) {}
-    virtual ~fpa2bv_converter_wrapped() {}
+    ~fpa2bv_converter_wrapped() override {}
     void mk_const(func_decl * f, expr_ref & result) override;
     void mk_rm_const(func_decl * f, expr_ref & result) override;
     app_ref wrap(expr * e);

src/ast/rewriter/push_app_ite.h

@@ -49,7 +49,7 @@ protected:
     bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override;
 public:
     ng_push_app_ite_cfg(ast_manager& m): push_app_ite_cfg(m) {}
-    virtual ~ng_push_app_ite_cfg() {}
+    ~ng_push_app_ite_cfg() override {}
 };
 
 struct push_app_ite_rw : public rewriter_tpl<push_app_ite_cfg> {

src/ast/value_generator.cpp

@@ -99,7 +99,7 @@ public:
     datatype_value_generator(value_generator& g, ast_manager& m):
         m(m), g(g), dt(m), m_sorts(m) {}
    
-    ~datatype_value_generator() {
+    ~datatype_value_generator() override {
         for (auto& kv : m_values) dealloc(kv.m_value);
     }
 

src/math/lp/factorization_factory_imp.h

@@ -28,8 +28,8 @@ namespace nla {
         const monic& m_rm;
         
         factorization_factory_imp(const monic& rm, const core& s);
-        bool find_canonical_monic_of_vars(const svector<lpvar>& vars, unsigned & i) const;
+        bool find_canonical_monic_of_vars(const svector<lpvar>& vars, unsigned & i) const override;
-        virtual bool canonize_sign(const monic& m) const;
+        bool canonize_sign(const monic& m) const override;
-        virtual bool canonize_sign(const factorization& m) const;
+        bool canonize_sign(const factorization& m) const override;
  };
 }

src/math/lp/lar_solver.h

@@ -543,7 +543,7 @@ public:
     void get_model(std::unordered_map<var_index, mpq> & variable_values) const;
     void get_rid_of_inf_eps();
     void get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const;
-    std::string get_variable_name(var_index vi) const;
+    std::string get_variable_name(var_index vi) const override;
     void set_variable_name(var_index vi, std::string);
     inline unsigned number_of_vars() const { return m_var_register.size(); }
     inline bool is_base(unsigned j) const { return m_mpq_lar_core_solver.m_r_heading[j] >= 0; }
@@ -651,7 +651,7 @@ public:
     lar_solver();
     void set_track_pivoted_rows(bool v);
     bool get_track_pivoted_rows() const;    
-    virtual ~lar_solver();
+    ~lar_solver() override;
     const vector<impq>& r_x() const { return m_mpq_lar_core_solver.m_r_x; }
     bool column_is_int(unsigned j) const;
     inline bool column_value_is_int(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].is_int(); }

src/math/lp/lp_solver.h

@@ -149,7 +149,7 @@ public:
     }
 
     
-    virtual ~lp_solver();
+    ~lp_solver() override;
 
     void flip_costs();
 

src/math/subpaving/tactic/subpaving_tactic.cpp

@@ -37,7 +37,7 @@ class subpaving_tactic : public tactic {
             e2v.mk_inv(m_inv);
         }
 
-        virtual ~display_var_proc() {}
+        ~display_var_proc() override {}
         
         ast_manager & m() const { return m_inv.get_manager(); }
         

src/nlsat/nlsat_assignment.h

@@ -32,7 +32,7 @@ namespace nlsat {
         bool_vector      m_assigned;
     public:
         assignment(anum_manager & _m):m_values(_m) {}
-        virtual ~assignment() {}
+        ~assignment() override {}
         anum_manager & am() const { return m_values.m(); }
         void swap(assignment & other) {
             m_values.swap(other.m_values);

src/sat/smt/sat_th.h

@@ -189,7 +189,7 @@ namespace euf {
 
     public:
         th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id);
-        virtual ~th_euf_solver() {}
+        ~th_euf_solver() override {}
         virtual theory_var mk_var(enode* n);
         unsigned get_num_vars() const { return m_var2enode.size(); }
         euf::enode* e_internalize(expr* e); 

src/smt/smt_model_finder.cpp

@@ -464,7 +464,7 @@ namespace smt {
                 m.limit().inc();
             }
 
-            virtual ~auf_solver() {
+            ~auf_solver() override {
                 flush_nodes();
                 reset_eval_cache();
             }

src/tactic/tactic.h

@@ -35,7 +35,7 @@ class tactic : public user_propagator::core {
     unsigned m_ref_count;
 public:
     tactic():m_ref_count(0) {}
-    virtual ~tactic() {}
+    ~tactic() override {}
 
     void inc_ref() { m_ref_count++; }
     void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }

src/test/api.cpp

@@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#ifdef _WINDOWS
 #include "api/z3.h"
 #include "api/z3_private.h"
 #include <iostream>
@@ -112,7 +111,3 @@ void tst_api() {
     test_bvneg();
     test_mk_distinct();
 }
-#else
-void tst_api() {
-}
-#endif

src/test/dl_product_relation.cpp

@@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#ifdef _WINDOWS
 #include "ast/reg_decl_plugins.h"
 #include "muz/base/dl_context.h"
 #include "muz/fp/dl_register_engine.h"
@@ -23,7 +22,7 @@ namespace datalog {
     public:
         collector_of_reduced(idx_set & accumulator) : m_acc(accumulator) {}
 
-        virtual void operator()(table_element * func_columns, const table_element * merged_func_columns) {
+        void operator()(table_element * func_columns, const table_element * merged_func_columns) override {
             m_acc.insert(static_cast<unsigned>(merged_func_columns[0]));
         }
     };
@@ -362,7 +361,3 @@ void tst_dl_product_relation() {
     test_finite_product_relation(fparams, params);
     
 }
-#else
-void tst_dl_product_relation() {
-}
-#endif

src/test/dl_relation.cpp

@@ -4,8 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#ifdef _WINDOWS
-
 #include "ast/reg_decl_plugins.h"
 #include "muz/base/dl_context.h"
 #include "muz/fp/dl_register_engine.h"
@@ -296,8 +294,3 @@ void tst_dl_relation() {
     datalog::test_interval_relation();
     datalog::test_bound_relation();
 }
-
-#else
-void tst_dl_relation() {
-}
-#endif

src/test/matcher.cpp

@@ -16,7 +16,6 @@ Author:
 Revision History:
 
 --*/
-#ifdef _WINDOWS
 #include "ast/substitution/matcher.h"
 #include "ast/ast_pp.h"
 #include "ast/reg_decl_plugins.h"
@@ -110,7 +109,3 @@ void tst1() {
 void tst_matcher() {
     tst1();
 }
-#else
-void tst_matcher() {
-}
-#endif

src/test/memory.cpp

@@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#ifdef _WINDOWS
 #include "api/z3.h"
 #include "api/z3_private.h"
 #include <iostream>
@@ -59,8 +58,3 @@ void tst_memory() {
     Z3_reset_memory();
 
 }
-
-#else
-void tst_memory() {    
-}
-#endif

src/test/no_overflow.cpp

@@ -16,7 +16,6 @@ Author:
 Revision History:
 
 --*/
-#ifdef _WINDOWS
 
 #include "api/z3.h"
 #include "util/trace.h"
@@ -724,7 +723,3 @@ void tst_no_overflow() {
         }
     }
 }
-#else
-void tst_no_overflow() {
-}
-#endif

src/test/simplifier.cpp

@@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#ifdef _WINDOWS
 #include "api/z3.h"
 #include "api/z3_private.h"
 #include <iostream>
@@ -214,8 +213,3 @@ void tst_simplifier() {
     test_bool();
     test_skolemize_bug();
 }
-
-#else
-void tst_simplifier() {
-}
-#endif

src/util/hwf.cpp

@@ -312,13 +312,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
 }
 
 void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) {
-#if defined(_WINDOWS) && _MSC_VER <= 1700
-    o.value = fmod(x.value, y.value);
-    if (o.value >= (y.value/2.0))
-        o.value -= y.value;
-#else
     o.value = remainder(x.value, y.value);
-#endif
 }
 
 void hwf_manager::maximum(hwf const & x, hwf const & y, hwf & o) {

src/util/mpf.cpp

@@ -1630,11 +1630,7 @@ std::string mpf_manager::to_string_hexfloat(mpf const & x) {
                                     std::ios_base::showpoint | std::ios_base::showpos);
     ss.setf(ff);
     ss.precision(13);
-#if defined(_WIN32) && _MSC_VER >= 1800
     ss << std::hexfloat << to_double(x);
-#else
-    ss << std::hex << (*reinterpret_cast<const unsigned long long *>(&(x)));
-#endif
     return ss.str();
 }
 

src/util/trail.h

@@ -243,7 +243,7 @@ public:
     m_value(m_vector.back()) {
     }
 
-    virtual void undo() {
+    void undo() override {
         m_vector.push_back(m_value);
     }
 };