mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

fixed some warnings reported by clang++

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-02 17:28:27 -07:00
parent ed52dce9b0
commit c1587dc37d
4 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifier/poly_simplifier_plugin.h
View file

@ -134,6 +134,10 @@ public:
virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result); virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result); virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result);
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
return simplifier_plugin::reduce(f, num_args, args, result);
}
expr * get_monomial_body(expr * m); expr * get_monomial_body(expr * m);
int get_monomial_body_order(expr * m); int get_monomial_body_order(expr * m);

2
src/cmd_context/pdecl.h
View file

@ -181,6 +181,7 @@ class paccessor_decl : public pdecl {
ptype const & get_type() const { return m_type; } ptype const & get_type() const { return m_type; }
virtual ~paccessor_decl() {} virtual ~paccessor_decl() {}
public: public:
virtual void display(std::ostream & out) const { pdecl::display(out); }
void display(std::ostream & out, pdatatype_decl const * const * dts) const; void display(std::ostream & out, pdatatype_decl const * const * dts) const;
}; };
@ -201,6 +202,7 @@ class pconstructor_decl : public pdecl {
constructor_decl * instantiate_decl(pdecl_manager & m, sort * const * s); constructor_decl * instantiate_decl(pdecl_manager & m, sort * const * s);
virtual ~pconstructor_decl() {} virtual ~pconstructor_decl() {}
public: public:
virtual void display(std::ostream & out) const { pdecl::display(out); }
void display(std::ostream & out, pdatatype_decl const * const * dts) const; void display(std::ostream & out, pdatatype_decl const * const * dts) const;
}; };

2
src/muz_qe/pdr_context.h
View file

@ -270,7 +270,7 @@ namespace pdr {
(*this)(n, new_cores.back().first, new_cores.back().second); (*this)(n, new_cores.back().first, new_cores.back().second);
} }
} }
virtual void collect_statistics(statistics& st) {} virtual void collect_statistics(statistics& st) const {}
}; };
class context { class context {

2
src/smt/theory_diff_logic.cpp
View file

@ -22,9 +22,11 @@ Revision History:
#include"rational.h" #include"rational.h"
#include"theory_diff_logic_def.h" #include"theory_diff_logic_def.h"
namespace smt {
template class theory_diff_logic<idl_ext>; template class theory_diff_logic<idl_ext>;
template class theory_diff_logic<sidl_ext>; template class theory_diff_logic<sidl_ext>;
template class theory_diff_logic<rdl_ext>; template class theory_diff_logic<rdl_ext>;
template class theory_diff_logic<srdl_ext>; template class theory_diff_logic<srdl_ext>;
};