Mark various QBF solver methods override

We should use `override` instead of `virtual`.

Author: tautschnig

src/solvers/qbf/qbf_bdd_core.h

@@ -31,12 +31,12 @@ class qbf_bdd_certificatet:public qdimacs_coret
 
 public:
   qbf_bdd_certificatet(void);
-  virtual ~qbf_bdd_certificatet(void);
+  ~qbf_bdd_certificatet(void) override;
 
-  virtual literalt new_variable(void);
+  literalt new_variable(void) override;
 
-  virtual tvt l_get(literalt a) const;
-  virtual const exprt f_get(literalt l);
+  tvt l_get(literalt a) const override;
+  const exprt f_get(literalt l) override;
 };
 
 
@@ -50,20 +50,20 @@ class qbf_bdd_coret:public qbf_bdd_certificatet
 
 public:
   qbf_bdd_coret();
-  virtual ~qbf_bdd_coret();
+  ~qbf_bdd_coret() override;
 
-  virtual literalt new_variable();
+  literalt new_variable() override;
 
-  virtual void lcnf(const bvt &bv);
-  virtual literalt lor(literalt a, literalt b);
-  virtual literalt lor(const bvt &bv);
+  void lcnf(const bvt &bv) override;
+  literalt lor(literalt a, literalt b) override;
+  literalt lor(const bvt &bv) override;
 
-  virtual std::string solver_text() const;
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  std::string solver_text() const override;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override;
 
-  virtual bool is_in_core(literalt l) const;
-  virtual modeltypet m_get(literalt a) const;
+  bool is_in_core(literalt l) const override;
+  modeltypet m_get(literalt a) const override;
 
 protected:
   void compress_certificate(void);

src/solvers/qbf/qbf_quantor.h

@@ -16,11 +16,11 @@ class qbf_quantort:public qdimacs_cnft
 {
 public:
   explicit qbf_quantort(message_handlert &message_handler);
-  virtual ~qbf_quantort();
+  ~qbf_quantort() override;
 
-  virtual std::string solver_text() const;
+  std::string solver_text() const override;
   virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  tvt l_get(literalt a) const override;
 };
 
 #endif // CPROVER_SOLVERS_QBF_QBF_QUANTOR_H

src/solvers/qbf/qbf_qube.h

@@ -16,11 +16,11 @@ class qbf_qubet:public qdimacs_cnft
 {
 public:
   explicit qbf_qubet(message_handlert &message_handler);
-  virtual ~qbf_qubet();
+  ~qbf_qubet() override;
 
-  virtual std::string solver_text() const;
+  std::string solver_text() const override;
   virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  tvt l_get(literalt a) const override;
 };
 
 #endif // CPROVER_SOLVERS_QBF_QBF_QUBE_H

src/solvers/qbf/qbf_qube_core.h

@@ -24,14 +24,14 @@ class qbf_qube_coret:public qdimacs_coret
 
 public:
   explicit qbf_qube_coret(message_handlert &message_handler);
-  virtual ~qbf_qube_coret();
+  ~qbf_qube_coret() override;
 
-  virtual std::string solver_text() const;
+  std::string solver_text() const override;
   virtual resultt prop_solve();
 
-  virtual bool is_in_core(literalt l) const;
+  bool is_in_core(literalt l) const override;
 
-  virtual tvt l_get(literalt a) const
+  tvt l_get(literalt a) const override
   {
     unsigned v=a.var_no();
 
@@ -49,9 +49,9 @@ class qbf_qube_coret:public qdimacs_coret
     return tvt::unknown();
   }
 
-  virtual modeltypet m_get(literalt a) const;
+  modeltypet m_get(literalt a) const override;
 
-  virtual const exprt f_get(literalt)
+  const exprt f_get(literalt) override
   {
     INVARIANT(false, "qube does not support full certificates.");
   }

src/solvers/qbf/qbf_skizzo.h

@@ -16,11 +16,11 @@ class qbf_skizzot:public qdimacs_cnft
 {
 public:
   explicit qbf_skizzot(message_handlert &message_handler);
-  virtual ~qbf_skizzot();
+  ~qbf_skizzot() override;
 
-  virtual std::string solver_text() const;
+  std::string solver_text() const override;
   virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  tvt l_get(literalt a) const override;
 };
 
 #endif // CPROVER_SOLVERS_QBF_QBF_SKIZZO_H

src/solvers/qbf/qbf_skizzo_core.h

@@ -17,13 +17,13 @@ class qbf_skizzo_coret:public qbf_bdd_certificatet
 {
 public:
   qbf_skizzo_coret();
-  virtual ~qbf_skizzo_coret();
+  ~qbf_skizzo_coret() override;
 
-  virtual std::string solver_text() const;
-  virtual resultt prop_solve();
+  std::string solver_text() const override;
+  resultt prop_solve() override;
 
-  virtual bool is_in_core(literalt l) const;
-  virtual modeltypet m_get(literalt a) const;
+  bool is_in_core(literalt l) const override;
+  modeltypet m_get(literalt a) const override;
 
 protected:
   std::string qbf_tmp_file;

src/solvers/qbf/qbf_squolem.h

@@ -24,16 +24,16 @@ class qbf_squolemt:public qdimacs_cnft
 
 public:
   qbf_squolemt();
-  virtual ~qbf_squolemt();
+  ~qbf_squolemt() override;
 
-  virtual std::string solver_text() const;
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  std::string solver_text() const override;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv);
-  virtual void add_quantifier(const quantifiert &quantifier);
-  virtual void set_quantifier(const quantifiert::typet type, const literalt l);
-  virtual void set_no_variables(size_t no);
+  void lcnf(const bvt &bv) override;
+  void add_quantifier(const quantifiert &quantifier) override;
+  void set_quantifier(const quantifiert::typet type, const literalt l) override;
+  void set_no_variables(size_t no) override;
   virtual size_t no_clauses() const { return squolem.clauses(); }
 };
 

src/solvers/qbf/qbf_squolem_core.h

@@ -24,29 +24,29 @@ class qbf_squolem_coret:public qdimacs_coret
 
 public:
   qbf_squolem_coret();
-  virtual ~qbf_squolem_coret();
+  ~qbf_squolem_coret() override;
 
-  virtual std::string solver_text() const;
-  virtual resultt prop_solve();
+  std::string solver_text() const override;
+  resultt prop_solve() override;
 
-  virtual tvt l_get(literalt a) const;
-  virtual bool is_in_core(literalt l) const;
+  tvt l_get(literalt a) const override;
+  bool is_in_core(literalt l) const override;
 
   void set_debug_filename(const std::string &str);
 
-  virtual void lcnf(const bvt &bv);
-  virtual void add_quantifier(const quantifiert &quantifier);
-  virtual void set_quantifier(const quantifiert::typet type, const literalt l);
-  virtual void set_no_variables(size_t no);
+  void lcnf(const bvt &bv) override;
+  void add_quantifier(const quantifiert &quantifier) override;
+  void set_quantifier(const quantifiert::typet type, const literalt l) override;
+  void set_no_variables(size_t no) override;
   virtual size_t no_clauses() const { return squolem->clauses(); }
 
-  virtual modeltypet m_get(literalt a) const;
+  modeltypet m_get(literalt a) const override;
 
-  virtual void write_qdimacs_cnf(std::ostream &out);
+  void write_qdimacs_cnf(std::ostream &out) override;
 
   void reset(void);
 
-  virtual const exprt f_get(literalt l);
+  const exprt f_get(literalt l) override;
 
 private:
   typedef std::unordered_map<unsigned, exprt> function_cachet;

src/solvers/qbf/qdimacs_cnf.h

@@ -21,13 +21,12 @@ class qdimacs_cnft:public dimacs_cnft
     : dimacs_cnft(message_handler)
   {
   }
-  virtual ~qdimacs_cnft() { }
 
   virtual void write_qdimacs_cnf(std::ostream &out);
 
   // dummy functions
 
-  virtual std::string solver_text() const
+  std::string solver_text() const override
   {
     return "QDIMACS CNF";
   }