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
128
129
130
131
132
133
134
135
136
137
138
139
140
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Dejan Jovanovic, Gereon Kremer
*
* 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.
* ****************************************************************************
*
* Base class for shared solver.
*/
#include "cvc4_private.h"
#ifndef CVC5__THEORY__SHARED_SOLVER__H
#define CVC5__THEORY__SHARED_SOLVER__H
#include "expr/node.h"
#include "theory/shared_terms_database.h"
#include "theory/term_registration_visitor.h"
#include "theory/valuation.h"
namespace cvc5 {
class LogicInfo;
class ProofNodeManager;
class TheoryEngine;
namespace theory {
struct EeSetupInfo;
/**
* A base class for shared solver. The shared solver is the component of theory
* engine that behaves like a theory solver, and whose purpose is to ensure the
* main theory combination method can be performed in CombinationEngine.
* Its role is to:
* (1) Notify the individual theories of shared terms via addSharedTerms,
* (2) Be the official interface for equality statuses,
* (3) Propagate equalities to TheoryEngine when necessary and explain them.
*/
class SharedSolver
{
public:
SharedSolver(TheoryEngine& te, ProofNodeManager* pnm);
virtual ~SharedSolver() {}
//------------------------------------- initialization
/**
* Returns true if we need an equality engine, this has the same contract
* as Theory::needsEqualityEngine.
*/
virtual bool needsEqualityEngine(theory::EeSetupInfo& esi);
/**
* Set the equality engine. This should be called by equality engine manager
* during EqEngineManager::initializeTheories.
*/
virtual void setEqualityEngine(eq::EqualityEngine* ee) = 0;
//------------------------------------- end initialization
/**
* Called when the given atom is pre-registered in TheoryEngine.
*
* This calls Theory::preRegisterTerm on all subterms of atom for the
* appropriate theories.
*
* Also, if sharing is enabled, this adds atom as an equality to propagate in
* the shared terms database if it is an equality, and adds its shared terms
* to the appropariate theories.
*
* @param atom The atom to preregister
*/
void preRegister(TNode atom);
/**
* Pre-notify assertion fact with the given atom. This is called when any
* fact is asserted in TheoryEngine, just before it is dispatched to the
* appropriate theory.
*
* This calls Theory::notifySharedTerm for the shared terms of the atom.
*/
void preNotifySharedFact(TNode atom);
/**
* Get the equality status of a and b.
*
* This method is used by theories via Valuation mostly for determining their
* care graph.
*/
virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
/**
* Explain literal, which returns a conjunction of literals that entail
* the given one.
*/
virtual TrustNode explain(TNode literal, TheoryId id) = 0;
/**
* Assert equality to the shared terms database.
*
* This method is called by TheoryEngine when a fact has been marked to
* send to THEORY_BUILTIN, meaning that shared terms database should
* maintain this fact. This is the case when either an equality is
* asserted from the SAT solver or a theory propagates an equality between
* shared terms.
*/
virtual void assertSharedEquality(TNode equality,
bool polarity,
TNode reason) = 0;
/** Is term t a shared term? */
virtual bool isShared(TNode t) const;
/**
* Method called by equalityEngine when a becomes (dis-)equal to b and a and b
* are shared with the theory. Returns false if there is a direct conflict
* (via rewrite for example).
*/
bool propagateSharedEquality(theory::TheoryId theory,
TNode a,
TNode b,
bool value);
/** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
void sendLemma(TrustNode trn, TheoryId atomsTo);
protected:
/** Solver-specific pre-register shared */
virtual void preRegisterSharedInternal(TNode t) = 0;
/** Reference to the theory engine */
TheoryEngine& d_te;
/** Logic info of theory engine (cached) */
const LogicInfo& d_logicInfo;
/** The database of shared terms.*/
SharedTermsDatabase d_sharedTerms;
/** Default visitor for pre-registration */
PreRegisterVisitor d_preRegistrationVisitor;
/** Visitor for collecting shared terms */
SharedTermsVisitor d_sharedTermsVisitor;
};
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__SHARED_SOLVER__H */
|
