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