GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_state.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_state.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 A theory state for Theory
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__THEORY_STATE_H
18
#define CVC4__THEORY__THEORY_STATE_H
19
20
#include "context/cdo.h"
21
#include "expr/node.h"
22
#include "theory/valuation.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
namespace eq {
28
class EqualityEngine;
29
}
30
31
class TheoryState
32
{
33
 public:
34
  TheoryState(context::Context* c, context::UserContext* u, Valuation val);
35
98976
  virtual ~TheoryState() {}
36
  /**
37
   * Set equality engine, where ee is a pointer to the official equality engine
38
   * of theory.
39
   */
40
  void setEqualityEngine(eq::EqualityEngine* ee);
41
  /** Get the SAT context */
42
  context::Context* getSatContext() const;
43
  /** Get the user context */
44
  context::UserContext* getUserContext() const;
45
  //-------------------------------------- equality information
46
  /** Is t registered as a term in the equality engine of this class? */
47
  virtual bool hasTerm(TNode a) const;
48
  /**
49
   * Get the representative of t in the equality engine of this class, or t
50
   * itself if it is not registered as a term.
51
   */
52
  virtual TNode getRepresentative(TNode t) const;
53
  /**
54
   * Are a and b equal according to the equality engine of this class? Also
55
   * returns true if a and b are identical.
56
   */
57
  virtual bool areEqual(TNode a, TNode b) const;
58
  /**
59
   * Are a and b disequal according to the equality engine of this class? Also
60
   * returns true if the representative of a and b are distinct constants.
61
   */
62
  virtual bool areDisequal(TNode a, TNode b) const;
63
  /** get list of members in the equivalence class of a */
64
  virtual void getEquivalenceClass(Node a, std::vector<Node>& eqc) const;
65
  /** get equality engine */
66
  eq::EqualityEngine* getEqualityEngine() const;
67
  //-------------------------------------- end equality information
68
  /**
69
   * Set that the current state of the solver is in conflict. This should be
70
   * called immediately after a call to conflict(...) on the output channel of
71
   * the theory.
72
   */
73
  virtual void notifyInConflict();
74
  /** Are we currently in conflict? */
75
  virtual bool isInConflict() const;
76
77
  /** Returns true if lit is a SAT literal. */
78
  virtual bool isSatLiteral(TNode lit) const;
79
  /**
80
   * Returns pointer to model. This model is only valid during last call effort
81
   * check.
82
   */
83
  TheoryModel* getModel();
84
  /**
85
   * Returns a pointer to the sort inference module, which lives in TheoryEngine
86
   * and is non-null when options::sortInference is true.
87
   */
88
  SortInference* getSortInference();
89
90
  /** Returns true if n has a current SAT assignment and stores it in value. */
91
  virtual bool hasSatValue(TNode n, bool& value) const;
92
93
  //------------------------------------------- access methods for assertions
94
  /**
95
   * The following methods are intended only to be used in limited use cases,
96
   * for cases where a theory (e.g. quantifiers) requires knowing about the
97
   * assertions from other theories.
98
   */
99
  /** The beginning iterator of facts for theory tid.*/
100
  context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
101
  /** The beginning iterator of facts for theory tid.*/
102
  context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
103
104
  /** Get the underlying valuation class */
105
  Valuation& getValuation();
106
107
 protected:
108
  /** Pointer to the SAT context object used by the theory. */
109
  context::Context* d_context;
110
  /** Pointer to the user context object used by the theory. */
111
  context::UserContext* d_ucontext;
112
  /**
113
   * The valuation proxy for the Theory to communicate back with the
114
   * theory engine (and other theories).
115
   */
116
  Valuation d_valuation;
117
  /** Pointer to equality engine of the theory. */
118
  eq::EqualityEngine* d_ee;
119
  /** Are we in conflict? */
120
  context::CDO<bool> d_conflict;
121
};
122
123
}  // namespace theory
124
}  // namespace CVC4
125
126
#endif /* CVC4__THEORY__SOLVER_STATE_H */