GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/model.h Lines: 1 3 33.3 %
Date: 2021-03-22 Branches: 0 0 0.0 %

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