blob: de6e6d47790834b42811a2c94ce5af768bdc3492 (
plain)
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
|
/********************* */
/*! \file theory_state.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** 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 A theory state for Theory
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__THEORY_STATE_H
#define CVC4__THEORY__THEORY_STATE_H
#include "context/cdo.h"
#include "expr/node.h"
#include "theory/valuation.h"
namespace CVC4 {
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 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;
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 CVC4
#endif /* CVC4__THEORY__SOLVER_STATE_H */
|
