1 /********************* */
2 /*! \file theory_arith.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, Gereon Kremer
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Arithmetic theory.
16 #include "cvc4_private.h"
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/inference_manager.h"
25 #include "theory/arith/nl/nonlinear_extension.h"
26 #include "theory/arith/operator_elim.h"
27 #include "theory/theory.h"
33 class TheoryArithPrivate
;
36 * Implementation of linear and non-linear integer and real arithmetic.
37 * The linear arithmetic solver is based upon:
38 * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
40 class TheoryArith
: public Theory
{
42 friend class TheoryArithPrivate
;
44 TheoryArithPrivate
* d_internal
;
46 TimerStat d_ppRewriteTimer
;
49 TheoryArith(context::Context
* c
,
50 context::UserContext
* u
,
53 const LogicInfo
& logicInfo
,
54 ProofNodeManager
* pnm
= nullptr);
55 virtual ~TheoryArith();
57 //--------------------------------- initialization
58 /** get the official theory rewriter of this theory */
59 TheoryRewriter
* getTheoryRewriter() override
;
61 * Returns true if this theory needs an equality engine, which is assigned
62 * to it (d_equalityEngine) by the equality engine manager during
63 * TheoryEngine::finishInit, prior to calling finishInit for this theory.
64 * If this method returns true, it stores instructions for the notifications
65 * this Theory wishes to receive from its equality engine.
67 bool needsEqualityEngine(EeSetupInfo
& esi
) override
;
68 /** finish initialization */
69 void finishInit() override
;
70 //--------------------------------- end initialization
73 * Does non-context dependent setup for a node connected to a theory.
75 void preRegisterTerm(TNode n
) override
;
77 //--------------------------------- standard check
78 /** Pre-check, called before the fact queue of the theory is processed. */
79 bool preCheck(Effort level
) override
;
80 /** Post-check, called after the fact queue of the theory is processed. */
81 void postCheck(Effort level
) override
;
82 /** Pre-notify fact, return true if processed. */
83 bool preNotifyFact(TNode atom
,
87 bool isInternal
) override
;
88 //--------------------------------- end standard check
89 bool needsCheckLastEffort() override
;
90 void propagate(Effort e
) override
;
91 TrustNode
explain(TNode n
) override
;
93 bool collectModelInfo(TheoryModel
* m
, const std::set
<Node
>& termSet
) override
;
95 * Collect model values in m based on the relevant terms given by termSet.
97 bool collectModelValues(TheoryModel
* m
,
98 const std::set
<Node
>& termSet
) override
;
100 void shutdown() override
{}
102 void presolve() override
;
103 void notifyRestart() override
;
104 PPAssertStatus
ppAssert(TrustNode tin
,
105 TrustSubstitutionMap
& outSubstitutions
) override
;
106 TrustNode
ppRewrite(TNode atom
) override
;
107 void ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) override
;
109 std::string
identify() const override
{ return std::string("TheoryArith"); }
111 EqualityStatus
getEqualityStatus(TNode a
, TNode b
) override
;
113 void notifySharedTerm(TNode n
) override
;
115 Node
getModelValue(TNode var
) override
;
117 std::pair
<bool, Node
> entailmentCheck(TNode lit
) override
;
119 /** Return a reference to the arith::InferenceManager. */
120 InferenceManager
& getInferenceManager()
122 return d_inferenceManager
;
127 * Preprocess rewrite terms, return the trust node encapsulating the
128 * preprocessed form of n, and the proof generator that can provide the
129 * proof for the equivalence of n and this term.
131 * This calls the operator elimination utility to eliminate extended
134 TrustNode
ppRewriteTerms(TNode n
);
135 /** Get the proof equality engine */
136 eq::ProofEqEngine
* getProofEqEngine();
137 /** The state object wrapping TheoryArithPrivate */
139 /** The arith::InferenceManager. */
140 InferenceManager d_inferenceManager
;
143 * The non-linear extension, responsible for all approaches for non-linear
146 std::unique_ptr
<nl::NonlinearExtension
> d_nonlinearExtension
;
147 /** The preprocess utility */
148 ArithPreprocess d_arithPreproc
;
149 /** The theory rewriter for this theory. */
150 ArithRewriter d_rewriter
;
151 };/* class TheoryArith */
153 }/* CVC4::theory::arith namespace */
154 }/* CVC4::theory namespace */
155 }/* CVC4 namespace */