use override and final in some central classes

Author: kroening

src/solvers/flattening/arrays.h

@@ -27,7 +27,7 @@ class arrayst:public equalityt
 public:
   arrayst(const namespacet &_ns, propt &_prop);
 
-  virtual void post_process()
+  virtual void post_process() override
   {
     post_process_arrays();
     SUB::post_process();

src/solvers/flattening/boolbv.h

@@ -47,17 +47,17 @@ class boolbvt:public arrayst
   virtual bvt convert_bitvector(const exprt &expr); // no cache
 
   // overloading
-  virtual exprt get(const exprt &expr) const;
-  virtual void set_to(const exprt &expr, bool value);
-  virtual void print_assignment(std::ostream &out) const;
+  virtual exprt get(const exprt &expr) const override;
+  virtual void set_to(const exprt &expr, bool value) override;
+  virtual void print_assignment(std::ostream &out) const override;
 
-  virtual void clear_cache()
+  virtual void clear_cache() override
   {
     SUB::clear_cache();
     bv_cache.clear();
   }
 
-  virtual void post_process()
+  virtual void post_process() override
   {
     post_process_quantifiers();
     functions.post_process();
@@ -99,7 +99,7 @@ class boolbvt:public arrayst
   boolbv_mapt map;  
 
   // overloading
-  virtual literalt convert_rest(const exprt &expr);
+  virtual literalt convert_rest(const exprt &expr) override;
   virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
 
   typedef arrayst SUB;
@@ -229,8 +229,7 @@ class boolbvt:public arrayst
   exprt bv_get_cache(const exprt &expr) const;
 
   // unbounded arrays
-
-  bool is_unbounded_array(const typet &type) const;
+  bool is_unbounded_array(const typet &type) const override;
 
   // quantifier instantiations
   class quantifiert

src/solvers/flattening/equality.h

@@ -25,7 +25,7 @@ class equalityt:public prop_conv_solvert
 
   virtual literalt equality(const exprt &e1, const exprt &e2);
 
-  virtual void post_process()
+  virtual void post_process() override
   {
     add_equality_constraints();
     prop_conv_solvert::post_process();

src/solvers/prop/prop_conv.h

@@ -78,23 +78,23 @@ class prop_conv_solvert:public prop_convt
   virtual ~prop_conv_solvert() { }
 
   // overloading from decision_proceduret
-  virtual void set_to(const exprt &expr, bool value);
-  virtual decision_proceduret::resultt dec_solve();
-  virtual void print_assignment(std::ostream &out) const;
-  virtual std::string decision_procedure_text() const
+  virtual void set_to(const exprt &expr, bool value) override;
+  virtual decision_proceduret::resultt dec_solve() override;
+  virtual void print_assignment(std::ostream &out) const override;
+  virtual std::string decision_procedure_text() const override
   { return "propositional reduction"; }
-  virtual exprt get(const exprt &expr) const;
+  virtual exprt get(const exprt &expr) const override;
 
   // overloading from prop_convt
   using prop_convt::set_frozen;
-  virtual tvt l_get(literalt a) const { return prop.l_get(a); }
-  virtual void set_frozen(literalt a) { prop.set_frozen(a); }
-  virtual void set_assumptions(const bvt &_assumptions) { prop.set_assumptions(_assumptions); }
-  virtual bool has_set_assumptions() const { return prop.has_set_assumptions(); }
-  virtual void set_all_frozen() { freeze_all = true; }
-  virtual literalt convert(const exprt &expr);
-  virtual bool is_in_conflict(literalt l) const { return prop.is_in_conflict(l); }
-  virtual bool has_is_in_conflict() const { return prop.has_is_in_conflict(); }
+  virtual tvt l_get(literalt a) const override { return prop.l_get(a); }
+  virtual void set_frozen(literalt a) override { prop.set_frozen(a); }
+  virtual void set_assumptions(const bvt &_assumptions) override { prop.set_assumptions(_assumptions); }
+  virtual bool has_set_assumptions() const override { return prop.has_set_assumptions(); }
+  virtual void set_all_frozen() override { freeze_all = true; }
+  virtual literalt convert(const exprt &expr) override;
+  virtual bool is_in_conflict(literalt l) const override { return prop.is_in_conflict(l); }
+  virtual bool has_is_in_conflict() const override { return prop.has_is_in_conflict(); }
 
   // get literal for expression, if available
   virtual bool literal(const exprt &expr, literalt &literal) const;

src/solvers/sat/cnf.h

@@ -19,19 +19,19 @@ class cnft:public propt
   inline cnft():_no_variables(1) { }
   virtual ~cnft() { }
 
-  virtual literalt land(literalt a, literalt b);
-  virtual literalt lor(literalt a, literalt b);
-  virtual literalt land(const bvt &bv);
-  virtual literalt lor(const bvt &bv);
-  virtual literalt lxor(const bvt &bv);
-  virtual literalt lxor(literalt a, literalt b);
-  virtual literalt lnand(literalt a, literalt b);
-  virtual literalt lnor(literalt a, literalt b);
-  virtual literalt lequal(literalt a, literalt b);
-  virtual literalt limplies(literalt a, literalt b);
-  virtual literalt lselect(literalt a, literalt b, literalt c); // a?b:c
-  virtual literalt new_variable();
-  virtual size_t no_variables() const { return _no_variables; }
+  virtual literalt land(literalt a, literalt b) override;
+  virtual literalt lor(literalt a, literalt b) override;
+  virtual literalt land(const bvt &bv) override;
+  virtual literalt lor(const bvt &bv) override;
+  virtual literalt lxor(const bvt &bv) override;
+  virtual literalt lxor(literalt a, literalt b) override;
+  virtual literalt lnand(literalt a, literalt b) override;
+  virtual literalt lnor(literalt a, literalt b) override;
+  virtual literalt lequal(literalt a, literalt b) override;
+  virtual literalt limplies(literalt a, literalt b) override;
+  virtual literalt lselect(literalt a, literalt b, literalt c) override; // a?b:c
+  virtual literalt new_variable() override;
+  virtual size_t no_variables() const override { return _no_variables; }
   virtual void set_no_variables(size_t no) { _no_variables=no; }
   virtual size_t no_clauses() const=0;
 
@@ -65,7 +65,7 @@ class cnf_solvert:public cnft
   {
   }
 
-  virtual size_t no_clauses() const
+  virtual size_t no_clauses() const override
   {
     return clause_counter;
   }

src/solvers/sat/satcheck_minisat.h

@@ -23,22 +23,22 @@ class satcheck_minisat1_baset:public cnf_solvert
 
   virtual ~satcheck_minisat1_baset();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  virtual const std::string solver_text() override;
+  virtual resultt prop_solve() override;
+  virtual tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv);
+  virtual void lcnf(const bvt &bv) override final;
 
-  virtual void set_assignment(literalt a, bool value);
+  virtual void set_assignment(literalt a, bool value) override;
 
   // extra MiniSat feature: solve with assumptions
-  virtual void set_assumptions(const bvt &_assumptions);
+  virtual void set_assumptions(const bvt &_assumptions) override;
 
   // features  
-  virtual bool has_set_assumptions() const { return true; }
-  virtual bool has_is_in_conflict() const { return true; }
+  virtual bool has_set_assumptions() const override { return true; }
+  virtual bool has_is_in_conflict() const override { return true; }
 
-  virtual bool is_in_conflict(literalt l) const;
+  virtual bool is_in_conflict(literalt l) const override;
 
 protected:
   class Solver *solver;
@@ -59,7 +59,7 @@ class satcheck_minisat1_prooft:public satcheck_minisat1t
   satcheck_minisat1_prooft();
   ~satcheck_minisat1_prooft();
 
-  virtual const std::string solver_text();
+  virtual const std::string solver_text() override;
   simple_prooft &get_resolution_proof();
   //void set_partition_id(unsigned p_id);
 
@@ -74,8 +74,8 @@ class satcheck_minisat1_coret:public satcheck_minisat1_prooft
   satcheck_minisat1_coret();
   ~satcheck_minisat1_coret();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
+  virtual const std::string solver_text() override;
+  virtual resultt prop_solve() override;
 
   virtual bool has_in_core() const { return true; }
 

src/solvers/sat/satcheck_minisat2.h

@@ -29,21 +29,21 @@ class satcheck_minisat2_baset:public cnf_solvert
   explicit satcheck_minisat2_baset(T *);
   virtual ~satcheck_minisat2_baset();
 
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  virtual resultt prop_solve() override;
+  virtual tvt l_get(literalt a) const override final;
 
-  virtual void lcnf(const bvt &bv);
-  virtual void set_assignment(literalt a, bool value);
+  virtual void lcnf(const bvt &bv) override final;
+  virtual void set_assignment(literalt a, bool value) override;
 
   // extra MiniSat feature: solve with assumptions
-  virtual void set_assumptions(const bvt &_assumptions);
+  virtual void set_assumptions(const bvt &_assumptions) override;
 
   // extra MiniSat feature: default branching decision
   void set_polarity(literalt a, bool value);
 
-  virtual bool is_in_conflict(literalt a) const;
-  virtual bool has_set_assumptions() const { return true; }
-  virtual bool has_is_in_conflict() const { return true; }
+  virtual bool is_in_conflict(literalt a) const override;
+  virtual bool has_set_assumptions() const override final { return true; }
+  virtual bool has_is_in_conflict() const override final { return true; }
 
 protected:
   T *solver;
@@ -65,8 +65,8 @@ class satcheck_minisat_simplifiert:
 {
 public:
   satcheck_minisat_simplifiert();
-  virtual const std::string solver_text();
-  virtual void set_frozen(literalt a);
+  virtual const std::string solver_text() override final;
+  virtual void set_frozen(literalt a) override final;
   bool is_eliminated(literalt a) const;
 };