src/smt/check_models.h

   1 /*********************                                                        */
   2 /*! \file check_models.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Utility for checking models
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__SMT__CHECK_MODELS_H
  18 #define CVC4__SMT__CHECK_MODELS_H
  19
  20 #include "context/cdlist.h"
  21 #include "expr/node.h"
  22 #include "smt/model.h"
  23 #include "smt/smt_solver.h"
  24
  25 namespace CVC4 {
  26 namespace smt {
  27
  28 /**
  29  * This utility is responsible for checking the current model.
  30  */
  31 class CheckModels
  32 {
  33  public:
  34   CheckModels(SmtSolver& s);
  35   ~CheckModels();
  36   /**
  37    * Check model m against the current set of input assertions al.
  38    *
  39    * This throws an exception if we fail to verify that m is a proper model
  40    * given assertion list al based on the model checking policy.
  41    */
  42   void checkModel(Model* m, context::CDList<Node>* al, bool hardFailure);
  43
  44  private:
  45   /** Reference to the SMT solver */
  46   SmtSolver& d_smt;
  47 };
  48
  49 }  // namespace smt
  50 }  // namespace CVC4
  51
  52 #endif