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

Line Exec Source
1
/*********************                                                        */
2
/*! \file shared_solver.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Dejan Jovanovic
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 Base class for shared solver
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__SHARED_SOLVER__H
18
#define CVC4__THEORY__SHARED_SOLVER__H
19
20
#include "expr/node.h"
21
#include "theory/shared_terms_database.h"
22
#include "theory/term_registration_visitor.h"
23
#include "theory/valuation.h"
24
25
namespace CVC4 {
26
27
class LogicInfo;
28
class ProofNodeManager;
29
class TheoryEngine;
30
31
namespace theory {
32
33
struct EeSetupInfo;
34
35
/**
36
 * A base class for shared solver. The shared solver is the component of theory
37
 * engine that behaves like a theory solver, and whose purpose is to ensure the
38
 * main theory combination method can be performed in CombinationEngine.
39
 * Its role is to:
40
 * (1) Notify the individual theories of shared terms via addSharedTerms,
41
 * (2) Be the official interface for equality statuses,
42
 * (3) Propagate equalities to TheoryEngine when necessary and explain them.
43
 */
44
class SharedSolver
45
{
46
 public:
47
  SharedSolver(TheoryEngine& te, ProofNodeManager* pnm);
48
8994
  virtual ~SharedSolver() {}
49
  //------------------------------------- initialization
50
  /**
51
   * Returns true if we need an equality engine, this has the same contract
52
   * as Theory::needsEqualityEngine.
53
   */
54
  virtual bool needsEqualityEngine(theory::EeSetupInfo& esi);
55
  /**
56
   * Set the equality engine. This should be called by equality engine manager
57
   * during EqEngineManager::initializeTheories.
58
   */
59
  virtual void setEqualityEngine(eq::EqualityEngine* ee) = 0;
60
  //------------------------------------- end initialization
61
  /**
62
   * Called when the given atom is pre-registered in TheoryEngine.
63
   *
64
   * This calls Theory::preRegisterTerm on all subterms of atom for the
65
   * appropriate theories.
66
   *
67
   * Also, if sharing is enabled, this adds atom as an equality to propagate in
68
   * the shared terms database if it is an equality, and adds its shared terms
69
   * to the appropariate theories.
70
   *
71
   * @param atom The atom to preregister
72
   */
73
  void preRegister(TNode atom);
74
  /**
75
   * Pre-notify assertion fact with the given atom. This is called when any
76
   * fact is asserted in TheoryEngine, just before it is dispatched to the
77
   * appropriate theory.
78
   *
79
   * This calls Theory::notifySharedTerm for the shared terms of the atom.
80
   */
81
  void preNotifySharedFact(TNode atom);
82
  /**
83
   * Get the equality status of a and b.
84
   *
85
   * This method is used by theories via Valuation mostly for determining their
86
   * care graph.
87
   */
88
  virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
89
  /**
90
   * Explain literal, which returns a conjunction of literals that entail
91
   * the given one.
92
   */
93
  virtual TrustNode explain(TNode literal, TheoryId id) = 0;
94
  /**
95
   * Assert equality to the shared terms database.
96
   *
97
   * This method is called by TheoryEngine when a fact has been marked to
98
   * send to THEORY_BUILTIN, meaning that shared terms database should
99
   * maintain this fact. This is the case when either an equality is
100
   * asserted from the SAT solver or a theory propagates an equality between
101
   * shared terms.
102
   */
103
  virtual void assertSharedEquality(TNode equality,
104
                                    bool polarity,
105
                                    TNode reason) = 0;
106
  /** Is term t a shared term? */
107
  virtual bool isShared(TNode t) const;
108
109
  /**
110
   * Method called by equalityEngine when a becomes (dis-)equal to b and a and b
111
   * are shared with the theory. Returns false if there is a direct conflict
112
   * (via rewrite for example).
113
   */
114
  bool propagateSharedEquality(theory::TheoryId theory,
115
                               TNode a,
116
                               TNode b,
117
                               bool value);
118
  /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
119
  void sendLemma(TrustNode trn, TheoryId atomsTo);
120
121
 protected:
122
  /** Solver-specific pre-register shared */
123
  virtual void preRegisterSharedInternal(TNode t) = 0;
124
  /** Reference to the theory engine */
125
  TheoryEngine& d_te;
126
  /** Logic info of theory engine (cached) */
127
  const LogicInfo& d_logicInfo;
128
  /** The database of shared terms.*/
129
  SharedTermsDatabase d_sharedTerms;
130
  /** Default visitor for pre-registration */
131
  PreRegisterVisitor d_preRegistrationVisitor;
132
  /** Visitor for collecting shared terms */
133
  SharedTermsVisitor d_sharedTermsVisitor;
134
};
135
136
}  // namespace theory
137
}  // namespace CVC4
138
139
#endif /* CVC4__THEORY__SHARED_SOLVER__H */