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

Line Exec Source
1
/*********************                                                        */
2
/*! \file shared_solver_distributed.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Shared solver in the distributed architecture.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H
18
#define CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H
19
20
#include "expr/node.h"
21
#include "theory/shared_solver.h"
22
23
namespace CVC4 {
24
namespace theory {
25
26
/**
27
 * The shared solver in the distributed architecture. This class uses the
28
 * SharedTermsDatabase for implementing the core methods of a shared solver.
29
 */
30
class SharedSolverDistributed : public SharedSolver
31
{
32
 public:
33
  SharedSolverDistributed(TheoryEngine& te, ProofNodeManager* pnm);
34
17988
  virtual ~SharedSolverDistributed() {}
35
  //------------------------------------- initialization
36
  /**
37
   * Returns true if we need an equality engine, this has the same contract
38
   * as Theory::needsEqualityEngine.
39
   */
40
  bool needsEqualityEngine(theory::EeSetupInfo& esi) override;
41
  /** Set equality engine in the shared terms database */
42
  void setEqualityEngine(eq::EqualityEngine* ee) override;
43
  //------------------------------------- end initialization
44
  /** Assert equality to the shared terms database. */
45
  void assertSharedEquality(TNode equality,
46
                            bool polarity,
47
                            TNode reason) override;
48
  /**
49
   * Get equality status based on the equality engine of shared terms database
50
   */
51
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
52
  /** Explain literal that was propagated by a theory or using shared terms
53
   * database */
54
  TrustNode explain(TNode literal, TheoryId id) override;
55
56
 protected:
57
  /** If t is an equality, add it as one that may be propagated */
58
  void preRegisterSharedInternal(TNode t) override;
59
};
60
61
}  // namespace theory
62
}  // namespace CVC4
63
64
#endif /* CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H */