src/smt/model.h

   1 /*********************                                                        */
   2 /*! \file model.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Mathias Preiner
   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 Model class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__MODEL_H
  18 #define CVC4__MODEL_H
  19
  20 #include <iosfwd>
  21 #include <vector>
  22
  23 #include "expr/expr.h"
  24 #include "theory/theory_model.h"
  25 #include "util/cardinality.h"
  26
  27 namespace CVC4 {
  28
  29 class SmtEngine;
  30
  31 namespace smt {
  32
  33 class Model;
  34
  35 std::ostream& operator<<(std::ostream&, const Model&);
  36
  37 /**
  38  * This is the SMT-level model object, that is responsible for maintaining
  39  * the necessary information for how to print the model, as well as
  40  * holding a pointer to the underlying implementation of the theory model.
  41  *
  42  * The model declarations maintained by this class are context-independent
  43  * and should be updated when this model is printed.
  44  */
  45 class Model {
  46   friend std::ostream& operator<<(std::ostream&, const Model&);
  47   friend class ::CVC4::SmtEngine;
  48
  49  public:
  50   /** construct */
  51   Model(theory::TheoryModel* tm);
  52   /** virtual destructor */
  53   ~Model() {}
  54   /** get the input name (file name, etc.) this model is associated to */
  55   std::string getInputName() const { return d_inputName; }
  56   /**
  57    * Returns true if this model is guaranteed to be a model of the input
  58    * formula. Notice that when CVC4 answers "unknown", it may have a model
  59    * available for which this method returns false. In this case, this model is
  60    * only a candidate solution.
  61    */
  62   bool isKnownSat() const { return d_isKnownSat; }
  63   /** Get the underlying theory model */
  64   theory::TheoryModel* getTheoryModel();
  65   /** Get the underlying theory model (const version) */
  66   const theory::TheoryModel* getTheoryModel() const;
  67   //----------------------- helper methods in the underlying theory model
  68   /** Is the node n a model core symbol? */
  69   bool isModelCoreSymbol(TNode sym) const;
  70   /** Get value */
  71   Node getValue(TNode n) const;
  72   /** Does this model have approximations? */
  73   bool hasApproximations() const;
  74   //----------------------- end helper methods
  75   //----------------------- model declarations
  76   /** Clear the current model declarations. */
  77   void clearModelDeclarations();
  78   /**
  79    * Set that tn is a sort that should be printed in the model, when applicable,
  80    * based on the output language.
  81    */
  82   void addDeclarationSort(TypeNode tn);
  83   /**
  84    * Set that n is a variable that should be printed in the model, when
  85    * applicable, based on the output language.
  86    */
  87   void addDeclarationTerm(Node n);
  88   /** get declared sorts */
  89   const std::vector<TypeNode>& getDeclaredSorts() const;
  90   /** get declared terms */
  91   const std::vector<Node>& getDeclaredTerms() const;
  92   //----------------------- end model declarations
  93  protected:
  94   /** the input name (file name, etc.) this model is associated to */
  95   std::string d_inputName;
  96   /**
  97    * Flag set to false if the model is associated with an "unknown" response
  98    * from the solver.
  99    */
 100   bool d_isKnownSat;
 101   /**
 102    * Pointer to the underlying theory model, which maintains all data regarding
 103    * the values of sorts and terms.
 104    */
 105   theory::TheoryModel* d_tmodel;
 106   /**
 107    * The list of types to print, generally corresponding to declare-sort
 108    * commands.
 109    */
 110   std::vector<TypeNode> d_declareSorts;
 111   /**
 112    * The list of terms to print, is typically one-to-one with declare-fun
 113    * commands.
 114    */
 115   std::vector<Node> d_declareTerms;
 116 };
 117
 118 }  // namespace smt
 119 }/* CVC4 namespace */
 120
 121 #endif  /* CVC4__MODEL_H */