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
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Morgan Deters, Mathias Preiner
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 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.
* ****************************************************************************
*
* A theory state for Theory.
*/
#include "cvc4_private.h"
#ifndef CVC5__THEORY__THEORY_STATE_H
#define CVC5__THEORY__THEORY_STATE_H
#include "context/cdo.h"
#include "expr/node.h"
#include "theory/valuation.h"
namespace cvc5 {
namespace theory {
namespace eq {
class EqualityEngine;
}
class TheoryState
{
public:
TheoryState(context::Context* c, context::UserContext* u, Valuation val);
virtual ~TheoryState() {}
/**
* Set equality engine, where ee is a pointer to the official equality engine
* of theory.
*/
void setEqualityEngine(eq::EqualityEngine* ee);
/** Get the SAT context */
context::Context* getSatContext() const;
/** Get the user context */
context::UserContext* getUserContext() const;
//-------------------------------------- equality information
/** Is t registered as a term in the equality engine of this class? */
virtual bool hasTerm(TNode a) const;
/**
* Get the representative of t in the equality engine of this class, or t
* itself if it is not registered as a term.
*/
virtual TNode getRepresentative(TNode t) const;
/**
* Are a and b equal according to the equality engine of this class? Also
* returns true if a and b are identical.
*/
virtual bool areEqual(TNode a, TNode b) const;
/**
* Are a and b disequal according to the equality engine of this class? Also
* returns true if the representative of a and b are distinct constants.
*/
virtual bool areDisequal(TNode a, TNode b) const;
/** get list of members in the equivalence class of a */
virtual void getEquivalenceClass(Node a, std::vector<Node>& eqc) const;
/** get equality engine */
eq::EqualityEngine* getEqualityEngine() const;
//-------------------------------------- end equality information
/**
* Set that the current state of the solver is in conflict. This should be
* called immediately after a call to conflict(...) on the output channel of
* the theory.
*/
virtual void notifyInConflict();
/** Are we currently in conflict? */
virtual bool isInConflict() const;
/** Returns true if lit is a SAT literal. */
virtual bool isSatLiteral(TNode lit) const;
/**
* Returns pointer to model. This model is only valid during last call effort
* check.
*/
TheoryModel* getModel();
/**
* Returns a pointer to the sort inference module, which lives in TheoryEngine
* and is non-null when options::sortInference is true.
*/
SortInference* getSortInference();
/** Returns true if n has a current SAT assignment and stores it in value. */
virtual bool hasSatValue(TNode n, bool& value) const;
//------------------------------------------- access methods for assertions
/**
* The following methods are intended only to be used in limited use cases,
* for cases where a theory (e.g. quantifiers) requires knowing about the
* assertions from other theories.
*/
/** The beginning iterator of facts for theory tid.*/
context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
/** The beginning iterator of facts for theory tid.*/
context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
/** Get the underlying valuation class */
Valuation& getValuation();
protected:
/** Pointer to the SAT context object used by the theory. */
context::Context* d_context;
/** Pointer to the user context object used by the theory. */
context::UserContext* d_ucontext;
/**
* The valuation proxy for the Theory to communicate back with the
* theory engine (and other theories).
*/
Valuation d_valuation;
/** Pointer to equality engine of the theory. */
eq::EqualityEngine* d_ee;
/** Are we in conflict? */
context::CDO<bool> d_conflict;
};
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__SOLVER_STATE_H */
|