Use override

Author: peterschrammel

src/solvers/sat/cnf_clause_list.h

@@ -26,19 +26,25 @@ class cnf_clause_listt:public cnft
   cnf_clause_listt() { }
   virtual ~cnf_clause_listt() { }
 
-  virtual void lcnf(const bvt &bv);
+  void lcnf(const bvt &bv) override;
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   { return "CNF clause list"; }
 
-  virtual tvt l_get(literalt) const
+  tvt l_get(literalt) const override
   {
     return tvt::unknown();
   }
 
-  virtual resultt prop_solve() { return resultt::P_ERROR; }
+  resultt prop_solve() override
+  {
+    return resultt::P_ERROR;
+  }
 
-  virtual size_t no_clauses() const { return clauses.size(); }
+  size_t no_clauses() const override
+  {
+    return clauses.size();
+  }
 
   typedef std::list<bvt> clausest;
 
@@ -89,7 +95,7 @@ class cnf_clause_list_assignmentt:public cnf_clause_listt
     return assignment;
   }
 
-  virtual tvt l_get(literalt literal) const
+  tvt l_get(literalt literal) const override
   {
     if(literal.is_true())
       return tvt(true);

src/solvers/sat/dimacs_cnf.h

@@ -46,24 +46,24 @@ class dimacs_cnf_dumpt:public cnft
   explicit dimacs_cnf_dumpt(std::ostream &_out);
   virtual ~dimacs_cnf_dumpt() { }
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   {
     return "DIMACS CNF Dumper";
   }
 
-  virtual void lcnf(const bvt &bv);
+  void lcnf(const bvt &bv) override;
 
-  virtual resultt prop_solve()
+  resultt prop_solve() override
   {
     return resultt::P_ERROR;
   }
 
-  virtual tvt l_get(literalt) const
+  tvt l_get(literalt) const override
   {
     return tvt::unknown();
   }
 
-  virtual size_t no_clauses() const
+  size_t no_clauses() const override
   {
     return 0;
   }

src/solvers/sat/pbs_dimacs_cnf.h

@@ -47,13 +47,13 @@ class pbs_dimacs_cnft:public dimacs_cnft
 
   bool pbs_solve();
 
-  virtual resultt prop_solve();
+  resultt prop_solve() override;
 
-  virtual tvt l_get(literalt a) const;
+  tvt l_get(literalt a) const override;
 
   // dummy functions
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   {
     return "PBS - Pseudo Boolean/CNF Solver and Optimizer";
   }

src/solvers/sat/satcheck_booleforce.h

@@ -20,11 +20,11 @@ class satcheck_booleforce_baset:public cnf_solvert
 public:
   virtual ~satcheck_booleforce_baset();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  const std::string solver_text() override;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv);
+  void lcnf(const bvt &bv) override;
 };
 
 class satcheck_booleforcet:public satcheck_booleforce_baset

src/solvers/sat/satcheck_cadical.h

@@ -23,17 +23,23 @@ class satcheck_cadicalt:public cnf_solvert
   satcheck_cadicalt();
   virtual ~satcheck_cadicalt();
 
-  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) override;
-  virtual void set_assignment(literalt a, bool value) override;
-
-  virtual void set_assumptions(const bvt &_assumptions) override;
-  virtual bool has_set_assumptions() const override { return false; }
-  virtual bool has_is_in_conflict() const override { return false; }
-  virtual bool is_in_conflict(literalt a) const override;
+  const std::string solver_text() override;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override;
+
+  void lcnf(const bvt &bv) override;
+  void set_assignment(literalt a, bool value) override;
+
+  void set_assumptions(const bvt &_assumptions) override;
+  bool has_set_assumptions() const override
+  {
+    return false;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return false;
+  }
+  bool is_in_conflict(literalt a) const override;
 
 protected:
   // NOLINTNEXTLINE(readability/identifiers)

src/solvers/sat/satcheck_glucose.h

@@ -30,21 +30,27 @@ class satcheck_glucose_baset:public cnf_solvert
   explicit satcheck_glucose_baset(T *);
   virtual ~satcheck_glucose_baset();
 
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv);
-  virtual void set_assignment(literalt a, bool value);
+  void lcnf(const bvt &bv) override;
+  void set_assignment(literalt a, bool value) override;
 
   // extra MiniSat feature: solve with assumptions
-  virtual void set_assumptions(const bvt &_assumptions);
+  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; }
+  bool is_in_conflict(literalt a) const override;
+  bool has_set_assumptions() const override
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return true;
+  }
 
 protected:
   T *solver;
@@ -58,16 +64,16 @@ class satcheck_glucose_no_simplifiert:
 {
 public:
   satcheck_glucose_no_simplifiert();
-  virtual const std::string solver_text();
+  const std::string solver_text() override;
 };
 
 class satcheck_glucose_simplifiert:
   public satcheck_glucose_baset<Glucose::SimpSolver>
 {
 public:
   satcheck_glucose_simplifiert();
-  virtual const std::string solver_text();
-  virtual void set_frozen(literalt a);
+  const std::string solver_text() override;
+  void set_frozen(literalt a) override;
   bool is_eliminated(literalt a) const;
 };
 

src/solvers/sat/satcheck_ipasir.h

@@ -22,23 +22,29 @@ class satcheck_ipasirt:public cnf_solvert
   virtual ~satcheck_ipasirt() override;
 
   /// This method returns the description produced by the linked SAT solver
-  virtual const std::string solver_text() override;
+  const std::string solver_text() override;
 
-  virtual resultt prop_solve() override;
+  resultt prop_solve() override;
 
   /// This method returns the truth value for a literal of the current SAT model
-  virtual tvt l_get(literalt a) const override final;
+  tvt l_get(literalt a) const override final;
 
-  virtual void lcnf(const bvt &bv) override final;
+  void lcnf(const bvt &bv) override final;
 
   /* This method is not supported, and currently not called anywhere in CBMC */
-  virtual void set_assignment(literalt a, bool value) override;
-
-  virtual void set_assumptions(const bvt &_assumptions) override;
-
-  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; }
+  void set_assignment(literalt a, bool value) override;
+
+  void set_assumptions(const bvt &_assumptions) override;
+
+  bool is_in_conflict(literalt a) const override;
+  bool has_set_assumptions() const override final
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override final
+  {
+    return true;
+  }
 
 protected:
   void *solver;

src/solvers/sat/satcheck_lingeling.h

@@ -21,18 +21,24 @@ class satcheck_lingelingt:public cnf_solvert
   satcheck_lingelingt();
   virtual ~satcheck_lingelingt();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
-
-  virtual void lcnf(const bvt &bv);
-  virtual void set_assignment(literalt a, bool value);
-
-  virtual void set_assumptions(const bvt &_assumptions);
-  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;
-  virtual void set_frozen(literalt a);
+  const std::string solver_text() override;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override;
+
+  void lcnf(const bvt &bv) override;
+  void set_assignment(literalt a, bool value) override;
+
+  void set_assumptions(const bvt &_assumptions) override;
+  bool has_set_assumptions() const override
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return true;
+  }
+  bool is_in_conflict(literalt a) const override;
+  void set_frozen(literalt a) override;
 
 protected:
   // NOLINTNEXTLINE(readability/identifiers)

src/solvers/sat/satcheck_minisat.h

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

src/solvers/sat/satcheck_minisat2.h

@@ -30,14 +30,14 @@ class satcheck_minisat2_baset:public cnf_solvert
   explicit satcheck_minisat2_baset(T *);
   virtual ~satcheck_minisat2_baset();
 
-  virtual resultt prop_solve() override;
-  virtual tvt l_get(literalt a) const final;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override final;
 
-  virtual void lcnf(const bvt &bv) final;
-  virtual void set_assignment(literalt a, bool value) override;
+  void lcnf(const bvt &bv) override final;
+  void set_assignment(literalt a, bool value) override;
 
   // extra MiniSat feature: solve with assumptions
-  virtual void set_assumptions(const bvt &_assumptions) override;
+  void set_assumptions(const bvt &_assumptions) override;
 
   // extra MiniSat feature: default branching decision
   void set_polarity(literalt a, bool value);
@@ -48,9 +48,15 @@ class satcheck_minisat2_baset:public cnf_solvert
   // extra MiniSat feature: permit previously interrupted SAT query to continue
   void clear_interrupt();
 
-  virtual bool is_in_conflict(literalt a) const override;
-  virtual bool has_set_assumptions() const final { return true; }
-  virtual bool has_is_in_conflict() const final { return true; }
+  bool is_in_conflict(literalt a) const override;
+  bool has_set_assumptions() const override final
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override final
+  {
+    return true;
+  }
 
   void set_time_limit_seconds(uint32_t lim) override
   {
@@ -71,7 +77,7 @@ class satcheck_minisat_no_simplifiert:
 public:
   satcheck_minisat_no_simplifiert();
   explicit satcheck_minisat_no_simplifiert(message_handlert &message_handler);
-  virtual const std::string solver_text();
+  const std::string solver_text() override;
 };
 
 class satcheck_minisat_simplifiert:
@@ -80,8 +86,8 @@ class satcheck_minisat_simplifiert:
 public:
   satcheck_minisat_simplifiert();
   explicit satcheck_minisat_simplifiert(message_handlert &message_handler);
-  virtual const std::string solver_text() final;
-  virtual void set_frozen(literalt a) final;
+  const std::string solver_text() override final;
+  void set_frozen(literalt a) override final;
   bool is_eliminated(literalt a) const;
 };