src/theory/uf/theory_uf.h

   1 /*********************                                                        */
   2 /*! \file theory_uf.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   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 This is the interface to TheoryUF implementations
  13  **
  14  ** This is the interface to TheoryUF implementations.  All
  15  ** implementations of TheoryUF should inherit from this class.
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #ifndef CVC4__THEORY__UF__THEORY_UF_H
  21 #define CVC4__THEORY__UF__THEORY_UF_H
  22
  23 #include "context/cdo.h"
  24 #include "expr/node.h"
  25 #include "expr/node_trie.h"
  26 #include "theory/theory.h"
  27 #include "theory/theory_eq_notify.h"
  28 #include "theory/uf/equality_engine.h"
  29 #include "theory/uf/proof_checker.h"
  30 #include "theory/uf/proof_equality_engine.h"
  31 #include "theory/uf/symmetry_breaker.h"
  32 #include "theory/uf/theory_uf_rewriter.h"
  33
  34 namespace CVC4 {
  35 namespace theory {
  36 namespace uf {
  37
  38 class CardinalityExtension;
  39 class HoExtension;
  40
  41 class TheoryUF : public Theory {
  42  public:
  43   class NotifyClass : public TheoryEqNotifyClass
  44   {
  45    public:
  46     NotifyClass(TheoryInferenceManager& im, TheoryUF& uf)
  47         : TheoryEqNotifyClass(im), d_uf(uf)
  48     {
  49     }
  50
  51     void eqNotifyNewClass(TNode t) override
  52     {
  53       Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")"
  54                          << std::endl;
  55       d_uf.eqNotifyNewClass(t);
  56     }
  57
  58     void eqNotifyMerge(TNode t1, TNode t2) override
  59     {
  60       Debug("uf-notify") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2
  61                          << ")" << std::endl;
  62       d_uf.eqNotifyMerge(t1, t2);
  63     }
  64
  65     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
  66     {
  67       Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
  68       d_uf.eqNotifyDisequal(t1, t2, reason);
  69     }
  70
  71    private:
  72     /** Reference to the parent theory */
  73     TheoryUF& d_uf;
  74   };/* class TheoryUF::NotifyClass */
  75
  76 private:
  77   /** The associated cardinality extension (or nullptr if it does not exist) */
  78   std::unique_ptr<CardinalityExtension> d_thss;
  79   /** the higher-order solver extension (or nullptr if it does not exist) */
  80   std::unique_ptr<HoExtension> d_ho;
  81
  82   /** node for true */
  83   Node d_true;
  84
  85   /** All the function terms that the theory has seen */
  86   context::CDList<TNode> d_functionsTerms;
  87
  88   /** Symmetry analyzer */
  89   SymmetryBreaker d_symb;
  90
  91   /** called when a new equivalance class is created */
  92   void eqNotifyNewClass(TNode t);
  93
  94   /** called when two equivalance classes have merged */
  95   void eqNotifyMerge(TNode t1, TNode t2);
  96
  97   /** called when two equivalence classes are made disequal */
  98   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
  99
 100  public:
 101
 102   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
 103   TheoryUF(context::Context* c,
 104            context::UserContext* u,
 105            OutputChannel& out,
 106            Valuation valuation,
 107            const LogicInfo& logicInfo,
 108            ProofNodeManager* pnm = nullptr,
 109            std::string instanceName = "");
 110
 111   ~TheoryUF();
 112
 113   //--------------------------------- initialization
 114   /** get the official theory rewriter of this theory */
 115   TheoryRewriter* getTheoryRewriter() override;
 116   /**
 117    * Returns true if we need an equality engine. If so, we initialize the
 118    * information regarding how it should be setup. For details, see the
 119    * documentation in Theory::needsEqualityEngine.
 120    */
 121   bool needsEqualityEngine(EeSetupInfo& esi) override;
 122   /** finish initialization */
 123   void finishInit() override;
 124   //--------------------------------- end initialization
 125
 126   //--------------------------------- standard check
 127   /** Do we need a check call at last call effort? */
 128   bool needsCheckLastEffort() override;
 129   /** Post-check, called after the fact queue of the theory is processed. */
 130   void postCheck(Effort level) override;
 131   /** Pre-notify fact, return true if processed. */
 132   bool preNotifyFact(TNode atom,
 133                      bool pol,
 134                      TNode fact,
 135                      bool isPrereg,
 136                      bool isInternal) override;
 137   /** Notify fact */
 138   void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
 139   //--------------------------------- end standard check
 140
 141   /** Collect model values in m based on the relevant terms given by termSet */
 142   bool collectModelValues(TheoryModel* m,
 143                           const std::set<Node>& termSet) override;
 144
 145   TrustNode ppRewrite(TNode node) override;
 146   void preRegisterTerm(TNode term) override;
 147   TrustNode explain(TNode n) override;
 148
 149
 150   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 151   void presolve() override;
 152
 153   void computeCareGraph() override;
 154
 155   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 156
 157   std::string identify() const override { return "THEORY_UF"; }
 158  private:
 159   /** Explain why this literal is true by building an explanation */
 160   void explain(TNode literal, Node& exp);
 161
 162   bool areCareDisequal(TNode x, TNode y);
 163   void addCarePairs(const TNodeTrie* t1,
 164                     const TNodeTrie* t2,
 165                     unsigned arity,
 166                     unsigned depth);
 167
 168   TheoryUfRewriter d_rewriter;
 169   /** Proof rule checker */
 170   UfProofRuleChecker d_ufProofChecker;
 171   /** A (default) theory state object */
 172   TheoryState d_state;
 173   /** A (default) inference manager */
 174   TheoryInferenceManager d_im;
 175   /** The notify class */
 176   NotifyClass d_notify;
 177 };/* class TheoryUF */
 178
 179 }/* CVC4::theory::uf namespace */
 180 }/* CVC4::theory namespace */
 181 }/* CVC4 namespace */
 182
 183 #endif /* CVC4__THEORY__UF__THEORY_UF_H */