Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Morgan Deters, Tim King
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * The theory of uninterpreted functions (UF)
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__UF__THEORY_UF_H
      19                 :            : #define CVC5__THEORY__UF__THEORY_UF_H
      20                 :            : 
      21                 :            : #include "expr/node.h"
      22                 :            : #include "theory/care_pair_argument_callback.h"
      23                 :            : #include "theory/theory.h"
      24                 :            : #include "theory/theory_eq_notify.h"
      25                 :            : #include "theory/theory_state.h"
      26                 :            : #include "theory/uf/diamonds_proof_generator.h"
      27                 :            : #include "theory/uf/proof_checker.h"
      28                 :            : #include "theory/uf/symmetry_breaker.h"
      29                 :            : #include "theory/uf/theory_uf_rewriter.h"
      30                 :            : 
      31                 :            : namespace cvc5::internal {
      32                 :            : namespace theory {
      33                 :            : namespace uf {
      34                 :            : 
      35                 :            : class CardinalityExtension;
      36                 :            : class HoExtension;
      37                 :            : class ConversionsSolver;
      38                 :            : class LambdaLift;
      39                 :            : 
      40                 :            : class TheoryUF : public Theory {
      41                 :            :  public:
      42                 :            :   class NotifyClass : public TheoryEqNotifyClass
      43                 :            :   {
      44                 :            :    public:
      45                 :      50996 :     NotifyClass(TheoryInferenceManager& im, TheoryUF& uf)
      46                 :      50996 :         : TheoryEqNotifyClass(im), d_uf(uf)
      47                 :            :     {
      48                 :      50996 :     }
      49                 :            : 
      50                 :     780301 :     void eqNotifyNewClass(TNode t) override
      51                 :            :     {
      52         [ +  - ]:    1560600 :       Trace("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")"
      53                 :     780301 :                          << std::endl;
      54                 :     780301 :       d_uf.eqNotifyNewClass(t);
      55                 :     780301 :     }
      56                 :            : 
      57                 :    9051120 :     void eqNotifyMerge(TNode t1, TNode t2) override
      58                 :            :     {
      59         [ +  - ]:   18102200 :       Trace("uf-notify") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2
      60                 :    9051120 :                          << ")" << std::endl;
      61                 :    9051120 :       d_uf.eqNotifyMerge(t1, t2);
      62                 :    9051120 :     }
      63                 :            : 
      64                 :    1693130 :     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
      65                 :            :     {
      66         [ +  - ]:    1693130 :       Trace("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
      67                 :    1693130 :       d_uf.eqNotifyDisequal(t1, t2, reason);
      68                 :    1693130 :     }
      69                 :            : 
      70                 :            :    private:
      71                 :            :     /** Reference to the parent theory */
      72                 :            :     TheoryUF& d_uf;
      73                 :            :   };/* class TheoryUF::NotifyClass */
      74                 :            : 
      75                 :            : private:
      76                 :            :   /** The associated cardinality extension (or nullptr if it does not exist) */
      77                 :            :   std::unique_ptr<CardinalityExtension> d_thss;
      78                 :            :   /** the lambda lifting utility */
      79                 :            :   std::unique_ptr<LambdaLift> d_lambdaLift;
      80                 :            :   /** the higher-order solver extension (or nullptr if it does not exist) */
      81                 :            :   std::unique_ptr<HoExtension> d_ho;
      82                 :            :   /** the conversions solver */
      83                 :            :   std::unique_ptr<ConversionsSolver> d_csolver;
      84                 :            :   /** Diamonds proof generator */
      85                 :            :   DiamondsProofGenerator d_dpfgen;
      86                 :            : 
      87                 :            :   /** node for true */
      88                 :            :   Node d_true;
      89                 :            : 
      90                 :            :   /** All the function terms that the theory has seen */
      91                 :            :   context::CDList<TNode> d_functionsTerms;
      92                 :            : 
      93                 :            :   /** Symmetry analyzer */
      94                 :            :   SymmetryBreaker d_symb;
      95                 :            : 
      96                 :            :   /** called when a new equivalance class is created */
      97                 :            :   void eqNotifyNewClass(TNode t);
      98                 :            : 
      99                 :            :   /** called when two equivalance classes have merged */
     100                 :            :   void eqNotifyMerge(TNode t1, TNode t2);
     101                 :            : 
     102                 :            :   /** called when two equivalence classes are made disequal */
     103                 :            :   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
     104                 :            : 
     105                 :            :  public:
     106                 :            : 
     107                 :            :   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
     108                 :            :   TheoryUF(Env& env,
     109                 :            :            OutputChannel& out,
     110                 :            :            Valuation valuation,
     111                 :            :            std::string instanceName = "");
     112                 :            : 
     113                 :            :   ~TheoryUF();
     114                 :            : 
     115                 :            :   //--------------------------------- initialization
     116                 :            :   /** get the official theory rewriter of this theory */
     117                 :            :   TheoryRewriter* getTheoryRewriter() override;
     118                 :            :   /** get the proof checker of this theory */
     119                 :            :   ProofRuleChecker* getProofChecker() override;
     120                 :            :   /**
     121                 :            :    * Returns true if we need an equality engine. If so, we initialize the
     122                 :            :    * information regarding how it should be setup. For details, see the
     123                 :            :    * documentation in Theory::needsEqualityEngine.
     124                 :            :    */
     125                 :            :   bool needsEqualityEngine(EeSetupInfo& esi) override;
     126                 :            :   /** finish initialization */
     127                 :            :   void finishInit() override;
     128                 :            :   //--------------------------------- end initialization
     129                 :            : 
     130                 :            :   //--------------------------------- standard check
     131                 :            :   /** Do we need a check call at last call effort? */
     132                 :            :   bool needsCheckLastEffort() override;
     133                 :            :   /** Post-check, called after the fact queue of the theory is processed. */
     134                 :            :   void postCheck(Effort level) override;
     135                 :            :   /** Notify fact */
     136                 :            :   void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
     137                 :            :   //--------------------------------- end standard check
     138                 :            : 
     139                 :            :   /** Collect model values in m based on the relevant terms given by termSet */
     140                 :            :   bool collectModelValues(TheoryModel* m,
     141                 :            :                           const std::set<Node>& termSet) override;
     142                 :            : 
     143                 :            :   TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
     144                 :            :   void preRegisterTerm(TNode term) override;
     145                 :            :   TrustNode explain(TNode n) override;
     146                 :            : 
     147                 :            :   void ppStaticLearn(TNode in, std::vector<TrustNode>& learned) override;
     148                 :            :   void presolve() override;
     149                 :            : 
     150                 :            :   void computeCareGraph() override;
     151                 :            : 
     152                 :            :   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
     153                 :            : 
     154                 :          0 :   std::string identify() const override { return "THEORY_UF"; }
     155                 :            :  private:
     156                 :            :   /** Called when preregistering terms of kind APPLY_UF or HO_APPLY */
     157                 :            :   void preRegisterFunctionTerm(TNode node);
     158                 :            :   /** Explain why this literal is true by building an explanation */
     159                 :            :   void explain(TNode literal, Node& exp);
     160                 :            : 
     161                 :            :   /** Overrides to ensure that pairs of lambdas are not considered disequal. */
     162                 :            :   bool areCareDisequal(TNode x, TNode y) override;
     163                 :            :   /**
     164                 :            :    * Overrides to use the theory state instead of the equality engine, since
     165                 :            :    * for higher-order, some terms that do not occur in the equality engine are
     166                 :            :    * considered.
     167                 :            :    */
     168                 :            :   void processCarePairArgs(TNode a, TNode b) override;
     169                 :            :   /**
     170                 :            :    * Is t a higher order type? A higher-order type is a function type having
     171                 :            :    * an argument type that is also a function type. This is used for checking
     172                 :            :    * logic exceptions.
     173                 :            :    */
     174                 :            :   bool isHigherOrderType(TypeNode tn);
     175                 :            :   TheoryUfRewriter d_rewriter;
     176                 :            :   /** Proof rule checker */
     177                 :            :   UfProofRuleChecker d_checker;
     178                 :            :   /** A (default) theory state object */
     179                 :            :   TheoryState d_state;
     180                 :            :   /** A (default) inference manager */
     181                 :            :   TheoryInferenceManager d_im;
     182                 :            :   /** The notify class */
     183                 :            :   NotifyClass d_notify;
     184                 :            :   /** Cache for isHigherOrderType */
     185                 :            :   std::map<TypeNode, bool> d_isHoType;
     186                 :            :   /** The care pair argument callback, used for theory combination */
     187                 :            :   CarePairArgumentCallback d_cpacb;
     188                 :            : };/* class TheoryUF */
     189                 :            : 
     190                 :            : }  // namespace uf
     191                 :            : }  // namespace theory
     192                 :            : }  // namespace cvc5::internal
     193                 :            : 
     194                 :            : #endif /* CVC5__THEORY__UF__THEORY_UF_H */