1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Tim King, Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Arithmetic theory. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#pragma once |
19 |
|
|
20 |
|
#include "expr/node.h" |
21 |
|
#include "theory/arith/arith_preprocess.h" |
22 |
|
#include "theory/arith/arith_rewriter.h" |
23 |
|
#include "theory/arith/arith_state.h" |
24 |
|
#include "theory/arith/branch_and_bound.h" |
25 |
|
#include "theory/arith/inference_manager.h" |
26 |
|
#include "theory/arith/pp_rewrite_eq.h" |
27 |
|
#include "theory/theory.h" |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace theory { |
31 |
|
namespace arith { |
32 |
|
namespace nl { |
33 |
|
class NonlinearExtension; |
34 |
|
} |
35 |
|
|
36 |
|
class EqualitySolver; |
37 |
|
class TheoryArithPrivate; |
38 |
|
|
39 |
|
/** |
40 |
|
* Implementation of linear and non-linear integer and real arithmetic. |
41 |
|
* The linear arithmetic solver is based upon: |
42 |
|
* http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf |
43 |
|
*/ |
44 |
|
class TheoryArith : public Theory { |
45 |
|
friend class TheoryArithPrivate; |
46 |
|
public: |
47 |
|
TheoryArith(Env& env, OutputChannel& out, Valuation valuation); |
48 |
|
virtual ~TheoryArith(); |
49 |
|
|
50 |
|
//--------------------------------- initialization |
51 |
|
/** get the official theory rewriter of this theory */ |
52 |
|
TheoryRewriter* getTheoryRewriter() override; |
53 |
|
/** get the proof checker of this theory */ |
54 |
|
ProofRuleChecker* getProofChecker() override; |
55 |
|
/** |
56 |
|
* Returns true if this theory needs an equality engine, which is assigned |
57 |
|
* to it (d_equalityEngine) by the equality engine manager during |
58 |
|
* TheoryEngine::finishInit, prior to calling finishInit for this theory. |
59 |
|
* If this method returns true, it stores instructions for the notifications |
60 |
|
* this Theory wishes to receive from its equality engine. |
61 |
|
*/ |
62 |
|
bool needsEqualityEngine(EeSetupInfo& esi) override; |
63 |
|
/** finish initialization */ |
64 |
|
void finishInit() override; |
65 |
|
//--------------------------------- end initialization |
66 |
|
/** |
67 |
|
* Does non-context dependent setup for a node connected to a theory. |
68 |
|
*/ |
69 |
|
void preRegisterTerm(TNode n) override; |
70 |
|
|
71 |
|
//--------------------------------- standard check |
72 |
|
/** Pre-check, called before the fact queue of the theory is processed. */ |
73 |
|
bool preCheck(Effort level) override; |
74 |
|
/** Post-check, called after the fact queue of the theory is processed. */ |
75 |
|
void postCheck(Effort level) override; |
76 |
|
/** Pre-notify fact, return true if processed. */ |
77 |
|
bool preNotifyFact(TNode atom, |
78 |
|
bool pol, |
79 |
|
TNode fact, |
80 |
|
bool isPrereg, |
81 |
|
bool isInternal) override; |
82 |
|
//--------------------------------- end standard check |
83 |
|
bool needsCheckLastEffort() override; |
84 |
|
void propagate(Effort e) override; |
85 |
|
TrustNode explain(TNode n) override; |
86 |
|
|
87 |
|
bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) override; |
88 |
|
/** |
89 |
|
* Collect model values in m based on the relevant terms given by termSet. |
90 |
|
*/ |
91 |
|
bool collectModelValues(TheoryModel* m, |
92 |
|
const std::set<Node>& termSet) override; |
93 |
|
|
94 |
9931 |
void shutdown() override {} |
95 |
|
|
96 |
|
void presolve() override; |
97 |
|
void notifyRestart() override; |
98 |
|
PPAssertStatus ppAssert(TrustNode tin, |
99 |
|
TrustSubstitutionMap& outSubstitutions) override; |
100 |
|
/** |
101 |
|
* Preprocess rewrite terms, return the trust node encapsulating the |
102 |
|
* preprocessed form of n, and the proof generator that can provide the |
103 |
|
* proof for the equivalence of n and this term. |
104 |
|
* |
105 |
|
* This calls the operator elimination utility to eliminate extended |
106 |
|
* symbols. |
107 |
|
*/ |
108 |
|
TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override; |
109 |
|
void ppStaticLearn(TNode in, NodeBuilder& learned) override; |
110 |
|
|
111 |
|
std::string identify() const override { return std::string("TheoryArith"); } |
112 |
|
|
113 |
|
EqualityStatus getEqualityStatus(TNode a, TNode b) override; |
114 |
|
|
115 |
|
void notifySharedTerm(TNode n) override; |
116 |
|
|
117 |
|
Node getModelValue(TNode var) override; |
118 |
|
|
119 |
|
std::pair<bool, Node> entailmentCheck(TNode lit) override; |
120 |
|
|
121 |
|
/** Return a reference to the arith::InferenceManager. */ |
122 |
5203 |
InferenceManager& getInferenceManager() |
123 |
|
{ |
124 |
5203 |
return d_im; |
125 |
|
} |
126 |
|
|
127 |
|
private: |
128 |
|
/** |
129 |
|
* Update d_arithModelCache (if it is empty right now) and compute the termSet |
130 |
|
* by calling collectAssertedTerms. |
131 |
|
*/ |
132 |
|
void updateModelCache(std::set<Node>& termSet); |
133 |
|
/** |
134 |
|
* Update d_arithModelCache (if it is empty right now) using the given |
135 |
|
* termSet. |
136 |
|
*/ |
137 |
|
void updateModelCache(const std::set<Node>& termSet); |
138 |
|
/** |
139 |
|
* Perform a sanity check on the model that all integer variables are assigned |
140 |
|
* to integer values. If an integer variables is assigned to a non-integer |
141 |
|
* value, but the respective lemma can not be added (i.e. it has already been |
142 |
|
* added) an assertion triggers. Otherwise teturns true if a lemma was added, |
143 |
|
* false otherwise. |
144 |
|
*/ |
145 |
|
bool sanityCheckIntegerModel(); |
146 |
|
|
147 |
|
/** Get the proof equality engine */ |
148 |
|
eq::ProofEqEngine* getProofEqEngine(); |
149 |
|
/** Timer for ppRewrite */ |
150 |
|
TimerStat d_ppRewriteTimer; |
151 |
|
/** The state object wrapping TheoryArithPrivate */ |
152 |
|
ArithState d_astate; |
153 |
|
/** The arith::InferenceManager. */ |
154 |
|
InferenceManager d_im; |
155 |
|
/** The preprocess rewriter for equality */ |
156 |
|
PreprocessRewriteEq d_ppre; |
157 |
|
/** The branch and bound utility */ |
158 |
|
BranchAndBound d_bab; |
159 |
|
/** The equality solver */ |
160 |
|
std::unique_ptr<EqualitySolver> d_eqSolver; |
161 |
|
/** The (old) linear arithmetic solver */ |
162 |
|
TheoryArithPrivate* d_internal; |
163 |
|
|
164 |
|
/** |
165 |
|
* The non-linear extension, responsible for all approaches for non-linear |
166 |
|
* arithmetic. |
167 |
|
*/ |
168 |
|
std::unique_ptr<nl::NonlinearExtension> d_nonlinearExtension; |
169 |
|
/** The operator elimination utility */ |
170 |
|
OperatorElim d_opElim; |
171 |
|
/** The preprocess utility */ |
172 |
|
ArithPreprocess d_arithPreproc; |
173 |
|
/** The theory rewriter for this theory. */ |
174 |
|
ArithRewriter d_rewriter; |
175 |
|
|
176 |
|
/** |
177 |
|
* Caches the current arithmetic model with the following life cycle: |
178 |
|
* postCheck retrieves the model from arith_private and puts it into the |
179 |
|
* cache. If nonlinear reasoning is enabled, the cache is used for (and |
180 |
|
* possibly updated by) model-based refinement in postCheck. |
181 |
|
* In collectModelValues, the cache is filtered for the termSet and then |
182 |
|
* used to augment the TheoryModel. |
183 |
|
*/ |
184 |
|
std::map<Node, Node> d_arithModelCache; |
185 |
|
|
186 |
|
};/* class TheoryArith */ |
187 |
|
|
188 |
|
} // namespace arith |
189 |
|
} // namespace theory |
190 |
|
} // namespace cvc5 |