1 /*********************                                                        */
2 /*! \file theory_arith.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Tim King, Alex Ozdemir, Morgan Deters
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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 Arithmetic theory.
13  ** Arithmetic theory.
14  **/
15 
16 #include "cvc4_private.h"
17 
18 #pragma once
19 
20 #include "theory/theory.h"
21 #include "expr/node.h"
22 #include "proof/arith_proof_recorder.h"
23 #include "theory/arith/theory_arith_private_forward.h"
24 
25 
26 namespace CVC4 {
27 namespace theory {
28 
29 namespace arith {
30 
31 /**
32  * Implementation of QF_LRA.
33  * Based upon:
34  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
35  */
36 class TheoryArith : public Theory {
37 private:
38   friend class TheoryArithPrivate;
39 
40   TheoryArithPrivate* d_internal;
41 
42   TimerStat d_ppRewriteTimer;
43 
44   /**
45    * @brief Where to store Farkas proofs of lemmas
46    */
47   proof::ArithProofRecorder * d_proofRecorder;
48 
49 public:
50   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
51               Valuation valuation, const LogicInfo& logicInfo);
52   virtual ~TheoryArith();
53 
54   /**
55    * Does non-context dependent setup for a node connected to a theory.
56    */
57   void preRegisterTerm(TNode n) override;
58 
59   Node expandDefinition(LogicRequest& logicRequest, Node node) override;
60 
61   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
62 
63   void check(Effort e) override;
64   bool needsCheckLastEffort() override;
65   void propagate(Effort e) override;
66   Node explain(TNode n) override;
67   bool getCurrentSubstitution(int effort,
68                               std::vector<Node>& vars,
69                               std::vector<Node>& subs,
70                               std::map<Node, std::vector<Node> >& exp) override;
71   bool isExtfReduced(int effort,
72                      Node n,
73                      Node on,
74                      std::vector<Node>& exp) override;
75 
76   bool collectModelInfo(TheoryModel* m) override;
77 
shutdown()78   void shutdown() override {}
79 
80   void presolve() override;
81   void notifyRestart() override;
82   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
83   Node ppRewrite(TNode atom) override;
84   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
85 
identify()86   std::string identify() const override { return std::string("TheoryArith"); }
87 
88   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
89 
90   void addSharedTerm(TNode n) override;
91 
92   Node getModelValue(TNode var) override;
93 
94   std::pair<bool, Node> entailmentCheck(
95       TNode lit,
96       const EntailmentCheckParameters* params,
97       EntailmentCheckSideEffects* out) override;
98 
setProofRecorder(proof::ArithProofRecorder * proofRecorder)99   void setProofRecorder(proof::ArithProofRecorder * proofRecorder)
100   {
101     d_proofRecorder = proofRecorder;
102   }
103 
104 };/* class TheoryArith */
105 
106 }/* CVC4::theory::arith namespace */
107 }/* CVC4::theory namespace */
108 }/* CVC4 namespace */
109