1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Model class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__SMT__MODEL_H |
19 |
|
#define CVC5__SMT__MODEL_H |
20 |
|
|
21 |
|
#include <iosfwd> |
22 |
|
#include <vector> |
23 |
|
|
24 |
|
#include "expr/node.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace smt { |
28 |
|
|
29 |
|
class Model; |
30 |
|
|
31 |
|
std::ostream& operator<<(std::ostream&, const Model&); |
32 |
|
|
33 |
|
/** |
34 |
|
* A utility for representing a model for pretty printing. |
35 |
|
*/ |
36 |
29 |
class Model { |
37 |
|
public: |
38 |
|
/** Constructor |
39 |
|
* @param isKnownSat True if this model is associated with a "sat" response, |
40 |
|
* or false if it is associated with an "unknown" response. |
41 |
|
*/ |
42 |
|
Model(bool isKnownSat, const std::string& inputName); |
43 |
|
/** get the input name (file name, etc.) this model is associated to */ |
44 |
|
std::string getInputName() const { return d_inputName; } |
45 |
|
/** |
46 |
|
* Returns true if this model is guaranteed to be a model of the input |
47 |
|
* formula. Notice that when cvc5 answers "unknown", it may have a model |
48 |
|
* available for which this method returns false. In this case, this model is |
49 |
|
* only a candidate solution. |
50 |
|
*/ |
51 |
|
bool isKnownSat() const { return d_isKnownSat; } |
52 |
|
/** Get domain elements */ |
53 |
|
const std::vector<Node>& getDomainElements(TypeNode tn) const; |
54 |
|
/** Get value */ |
55 |
|
Node getValue(TNode n) const; |
56 |
|
/** Get separation logic heap and nil, return true if they have been set */ |
57 |
|
bool getHeapModel(Node& h, Node& nilEq) const; |
58 |
|
//----------------------- model declarations |
59 |
|
/** |
60 |
|
* Set that tn is a sort that should be printed in the model, when applicable, |
61 |
|
* based on the output language. |
62 |
|
* |
63 |
|
* @param tn The uninterpreted sort |
64 |
|
* @param elements The domain elements of tn in the model |
65 |
|
*/ |
66 |
|
void addDeclarationSort(TypeNode tn, const std::vector<Node>& elements); |
67 |
|
/** |
68 |
|
* Set that n is a variable that should be printed in the model, when |
69 |
|
* applicable, based on the output language. |
70 |
|
* |
71 |
|
* @param n The variable |
72 |
|
* @param value The value of the variable in the model |
73 |
|
*/ |
74 |
|
void addDeclarationTerm(Node n, Node value); |
75 |
|
/** |
76 |
|
* Set the separation logic model information where h is the heap and nilEq |
77 |
|
* is the value of sep.nil. |
78 |
|
* |
79 |
|
* @param h The value of heap in the heap model |
80 |
|
* @param nilEq The value of sep.nil in the heap model |
81 |
|
*/ |
82 |
|
void setHeapModel(Node h, Node nilEq); |
83 |
|
/** get declared sorts */ |
84 |
|
const std::vector<TypeNode>& getDeclaredSorts() const; |
85 |
|
/** get declared terms */ |
86 |
|
const std::vector<Node>& getDeclaredTerms() const; |
87 |
|
//----------------------- end model declarations |
88 |
|
protected: |
89 |
|
/** the input name (file name, etc.) this model is associated to */ |
90 |
|
std::string d_inputName; |
91 |
|
/** |
92 |
|
* Flag set to false if the model is associated with an "unknown" response |
93 |
|
* from the solver. |
94 |
|
*/ |
95 |
|
bool d_isKnownSat; |
96 |
|
/** |
97 |
|
* The list of types to print, generally corresponding to declare-sort |
98 |
|
* commands. |
99 |
|
*/ |
100 |
|
std::vector<TypeNode> d_declareSorts; |
101 |
|
/** The interpretation of the above sorts, as a list of domain elements. */ |
102 |
|
std::map<TypeNode, std::vector<Node>> d_domainElements; |
103 |
|
/** |
104 |
|
* The list of terms to print, is typically one-to-one with declare-fun |
105 |
|
* commands. |
106 |
|
*/ |
107 |
|
std::vector<Node> d_declareTerms; |
108 |
|
/** Mapping terms to values */ |
109 |
|
std::map<Node, Node> d_declareTermValues; |
110 |
|
/** Separation logic heap and nil */ |
111 |
|
Node d_sepHeap; |
112 |
|
Node d_sepNilEq; |
113 |
|
}; |
114 |
|
|
115 |
|
} // namespace smt |
116 |
|
} // namespace cvc5 |
117 |
|
|
118 |
|
#endif /* CVC5__SMT__MODEL_H */ |