src/theory/arith/theory_arith.h

   1 /*********************                                                        */
   2 /*! \file theory_arith.h
   3  ** \verbatim
   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
  11  **
  12  ** \brief Arithmetic theory.
  13  ** Arithmetic theory.
  14  **/
  15
  16 #include "cvc4_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/inference_manager.h"
  25 #include "theory/arith/nl/nonlinear_extension.h"
  26 #include "theory/arith/operator_elim.h"
  27 #include "theory/theory.h"
  28
  29 namespace CVC4 {
  30 namespace theory {
  31 namespace arith {
  32
  33 class TheoryArithPrivate;
  34
  35 /**
  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
  39  */
  40 class TheoryArith : public Theory {
  41  private:
  42   friend class TheoryArithPrivate;
  43
  44   TheoryArithPrivate* d_internal;
  45
  46   TimerStat d_ppRewriteTimer;
  47
  48  public:
  49   TheoryArith(context::Context* c,
  50               context::UserContext* u,
  51               OutputChannel& out,
  52               Valuation valuation,
  53               const LogicInfo& logicInfo,
  54               ProofNodeManager* pnm = nullptr);
  55   virtual ~TheoryArith();
  56
  57   //--------------------------------- initialization
  58   /** get the official theory rewriter of this theory */
  59   TheoryRewriter* getTheoryRewriter() override;
  60   /**
  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.
  66    */
  67   bool needsEqualityEngine(EeSetupInfo& esi) override;
  68   /** finish initialization */
  69   void finishInit() override;
  70   //--------------------------------- end initialization
  71
  72   /**
  73    * Does non-context dependent setup for a node connected to a theory.
  74    */
  75   void preRegisterTerm(TNode n) override;
  76
  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,
  84                      bool pol,
  85                      TNode fact,
  86                      bool isPrereg,
  87                      bool isInternal) override;
  88   //--------------------------------- end standard check
  89   bool needsCheckLastEffort() override;
  90   void propagate(Effort e) override;
  91   TrustNode explain(TNode n) override;
  92
  93   bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) override;
  94   /**
  95    * Collect model values in m based on the relevant terms given by termSet.
  96    */
  97   bool collectModelValues(TheoryModel* m,
  98                           const std::set<Node>& termSet) override;
  99
 100   void shutdown() override {}
 101
 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;
 108
 109   std::string identify() const override { return std::string("TheoryArith"); }
 110
 111   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 112
 113   void notifySharedTerm(TNode n) override;
 114
 115   Node getModelValue(TNode var) override;
 116
 117   std::pair<bool, Node> entailmentCheck(TNode lit) override;
 118
 119   /** Return a reference to the arith::InferenceManager. */
 120   InferenceManager& getInferenceManager()
 121   {
 122     return d_inferenceManager;
 123   }
 124
 125  private:
 126   /**
 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.
 130    *
 131    * This calls the operator elimination utility to eliminate extended
 132    * symbols.
 133    */
 134   TrustNode ppRewriteTerms(TNode n);
 135   /** Get the proof equality engine */
 136   eq::ProofEqEngine* getProofEqEngine();
 137   /** The state object wrapping TheoryArithPrivate  */
 138   ArithState d_astate;
 139   /** The arith::InferenceManager. */
 140   InferenceManager d_inferenceManager;
 141
 142   /**
 143    * The non-linear extension, responsible for all approaches for non-linear
 144    * arithmetic.
 145    */
 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 */
 152
 153 }/* CVC4::theory::arith namespace */
 154 }/* CVC4::theory namespace */
 155 }/* CVC4 namespace */