mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

use override

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-24 19:21:54 -07:00
parent 5baef8bcf3
commit c714abbff2
2 changed files with 24 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_special_relations.cpp
View file

@ -898,8 +898,4 @@ namespace smt {
out << "\n"; out << "\n";
} }
void theory_special_relations::display_atom( atom& a) const {
display_atom( std::cerr, a);
}
} }

50
src/smt/theory_special_relations.h
View file

@ -160,38 +160,36 @@ namespace smt {
public: public:
theory_special_relations(ast_manager& m); theory_special_relations(ast_manager& m);
virtual ~theory_special_relations(); ~theory_special_relations() override;
virtual theory * mk_fresh(context * new_ctx); theory * mk_fresh(context * new_ctx) override;
virtual bool internalize_atom(app * atom, bool gate_ctx); bool internalize_atom(app * atom, bool gate_ctx) override;
virtual bool internalize_term(app * term) { UNREACHABLE(); return false; } bool internalize_term(app * term) override { UNREACHABLE(); return false; }
virtual void new_eq_eh(theory_var v1, theory_var v2); void new_eq_eh(theory_var v1, theory_var v2) override;
virtual void new_diseq_eh(theory_var v1, theory_var v2) {} void new_diseq_eh(theory_var v1, theory_var v2) override {}
virtual bool use_diseqs() const { return false; } bool use_diseqs() const override { return false; }
virtual bool build_models() const { return true; } bool build_models() const override { return true; }
virtual final_check_status final_check_eh(); final_check_status final_check_eh() override;
virtual void reset_eh(); void reset_eh() override;
virtual void assign_eh(bool_var v, bool is_true); void assign_eh(bool_var v, bool is_true) override;
virtual void init_search_eh() {} void init_search_eh() override {}
virtual void push_scope_eh(); void push_scope_eh() override;
virtual void pop_scope_eh(unsigned num_scopes); void pop_scope_eh(unsigned num_scopes) override;
virtual void restart_eh() {} void restart_eh() override {}
virtual void collect_statistics(::statistics & st) const; void collect_statistics(::statistics & st) const override;
virtual model_value_proc * mk_value(enode * n, model_generator & mg); model_value_proc * mk_value(enode * n, model_generator & mg) override;
virtual void init_model(model_generator & m); void init_model(model_generator & m) override;
virtual bool can_propagate() { return false; } bool can_propagate() override { return false; }
virtual void propagate() {} void propagate() override {}
virtual void display(std::ostream & out) const; void display(std::ostream & out) const override;
literal mk_literal(expr* _e); literal mk_literal(expr* _e);
enode* ensure_enode(expr* e); enode* ensure_enode(expr* e);
theory_var mk_var(enode* n); theory_var mk_var(enode* n);
//BEGIN: ASHU void collect_asserted_po_atoms( vector< std::pair<bool_var,bool> >& atoms) const;
void collect_asserted_po_atoms( vector< std::pair<bool_var,bool> >& atoms) const; void display_atom( std::ostream & out, atom& a) const;
void display_atom( std::ostream & out, atom& a) const;
void display_atom( atom& a) const;
//END: ASHU
}; };
} }