src/theory/fp/theory_fp.h

   1 /*********************                                                        */
   2 /*! \file theory_fp.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Martin Brain, Aina Niemetz
   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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #ifndef CVC4__THEORY__FP__THEORY_FP_H
  21 #define CVC4__THEORY__FP__THEORY_FP_H
  22
  23 #include <string>
  24 #include <utility>
  25
  26 #include "context/cdo.h"
  27 #include "theory/fp/theory_fp_rewriter.h"
  28 #include "theory/theory.h"
  29 #include "theory/uf/equality_engine.h"
  30
  31 namespace CVC4 {
  32 namespace theory {
  33 namespace fp {
  34
  35 class FpConverter;
  36
  37 class TheoryFp : public Theory
  38 {
  39  public:
  40   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
  41   TheoryFp(context::Context* c,
  42            context::UserContext* u,
  43            OutputChannel& out,
  44            Valuation valuation,
  45            const LogicInfo& logicInfo,
  46            ProofNodeManager* pnm = nullptr);
  47
  48   //--------------------------------- initialization
  49   /** Get the official theory rewriter of this theory. */
  50   TheoryRewriter* getTheoryRewriter() override;
  51   /**
  52    * Returns true if we need an equality engine. If so, we initialize the
  53    * information regarding how it should be setup. For details, see the
  54    * documentation in Theory::needsEqualityEngine.
  55    */
  56   bool needsEqualityEngine(EeSetupInfo& esi) override;
  57   /** Finish initialization. */
  58   void finishInit() override;
  59   //--------------------------------- end initialization
  60
  61   TrustNode expandDefinition(Node node) override;
  62
  63   void preRegisterTerm(TNode node) override;
  64
  65   TrustNode ppRewrite(TNode node) override;
  66
  67   //--------------------------------- standard check
  68   /** Do we need a check call at last call effort? */
  69   bool needsCheckLastEffort() override;
  70   /** Post-check, called after the fact queue of the theory is processed. */
  71   void postCheck(Effort level) override;
  72   /** Pre-notify fact, return true if processed. */
  73   bool preNotifyFact(TNode atom,
  74                      bool pol,
  75                      TNode fact,
  76                      bool isPrereg,
  77                      bool isInternal) override;
  78   //--------------------------------- end standard check
  79
  80   Node getModelValue(TNode var) override;
  81   bool collectModelInfo(TheoryModel* m,
  82                         const std::set<Node>& relevantTerms) override;
  83   /**
  84    * Collect model values in m based on the relevant terms given by
  85    * relevantTerms.
  86    */
  87   bool collectModelValues(TheoryModel* m,
  88                           const std::set<Node>& relevantTerms) override;
  89
  90   std::string identify() const override { return "THEORY_FP"; }
  91
  92   TrustNode explain(TNode n) override;
  93
  94  protected:
  95   using PairTypeNodeHashFunction = PairHashFunction<TypeNode,
  96                                                     TypeNode,
  97                                                     TypeNodeHashFunction,
  98                                                     TypeNodeHashFunction>;
  99   /** Uninterpreted functions for undefined cases of non-total operators. */
 100   using ComparisonUFMap =
 101       context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
 102   /** Uninterpreted functions for lazy handling of conversions. */
 103   using ConversionUFMap = context::
 104       CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>;
 105   using ConversionAbstractionMap = ComparisonUFMap;
 106   using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>;
 107
 108   /** Equality engine. */
 109   class NotifyClass : public eq::EqualityEngineNotify {
 110    protected:
 111     TheoryFp& d_theorySolver;
 112
 113    public:
 114     NotifyClass(TheoryFp& solver) : d_theorySolver(solver) {}
 115     bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
 116     bool eqNotifyTriggerTermEquality(TheoryId tag,
 117                                      TNode t1,
 118                                      TNode t2,
 119                                      bool value) override;
 120     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
 121     void eqNotifyNewClass(TNode t) override {}
 122     void eqNotifyMerge(TNode t1, TNode t2) override {}
 123     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
 124   };
 125   friend NotifyClass;
 126
 127   NotifyClass d_notification;
 128
 129   /** General utility. */
 130   void registerTerm(TNode node);
 131   bool isRegistered(TNode node);
 132
 133   context::CDHashSet<Node, NodeHashFunction> d_registeredTerms;
 134
 135   /** The word-blaster. Translates FP -> BV. */
 136   std::unique_ptr<FpConverter> d_conv;
 137
 138   bool d_expansionRequested;
 139
 140   void convertAndEquateTerm(TNode node);
 141
 142   /** Interaction with the rest of the solver **/
 143   void handleLemma(Node node);
 144   /**
 145    * Called when literal node is inferred by the equality engine. This
 146    * propagates node on the output channel.
 147    */
 148   bool propagateLit(TNode node);
 149   /**
 150    * Called when two constants t1 and t2 merge in the equality engine. This
 151    * sends a conflict on the output channel.
 152    */
 153   void conflictEqConstantMerge(TNode t1, TNode t2);
 154
 155   bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
 156
 157   Node minUF(Node);
 158   Node maxUF(Node);
 159
 160   Node toUBVUF(Node);
 161   Node toSBVUF(Node);
 162
 163   Node toRealUF(Node);
 164
 165   Node abstractRealToFloat(Node);
 166   Node abstractFloatToReal(Node);
 167
 168  private:
 169   context::CDO<Node> d_conflictNode;
 170
 171   ComparisonUFMap d_minMap;
 172   ComparisonUFMap d_maxMap;
 173   ConversionUFMap d_toUBVMap;
 174   ConversionUFMap d_toSBVMap;
 175   ComparisonUFMap d_toRealMap;
 176   ConversionAbstractionMap d_realToFloatMap;
 177   ConversionAbstractionMap d_floatToRealMap;
 178   AbstractionMap d_abstractionMap;  // abstract -> original
 179
 180   /** The theory rewriter for this theory. */
 181   TheoryFpRewriter d_rewriter;
 182   /** A (default) theory state object */
 183   TheoryState d_state;
 184 }; /* class TheoryFp */
 185
 186 }  // namespace fp
 187 }  // namespace theory
 188 }  // namespace CVC4
 189
 190 #endif /* CVC4__THEORY__FP__THEORY_FP_H */