Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz, Daniel Larraz
       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                 :            :  * Implementation of higher-order term database class.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/quantifiers/ho_term_database.h"
      17                 :            : 
      18                 :            : #include "expr/skolem_manager.h"
      19                 :            : #include "options/quantifiers_options.h"
      20                 :            : #include "theory/quantifiers/quantifiers_inference_manager.h"
      21                 :            : #include "theory/quantifiers/quantifiers_state.h"
      22                 :            : #include "theory/rewriter.h"
      23                 :            : #include "theory/uf/equality_engine.h"
      24                 :            : 
      25                 :            : using namespace cvc5::internal::kind;
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : namespace theory {
      29                 :            : namespace quantifiers {
      30                 :            : 
      31                 :       1201 : HoTermDb::HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
      32                 :       1201 :     : TermDb(env, qs, qr), d_hoFunOpPurify(userContext())
      33                 :            : {
      34                 :       1201 : }
      35                 :            : 
      36                 :       2398 : HoTermDb::~HoTermDb() {}
      37                 :            : 
      38                 :      90888 : void HoTermDb::addTermInternal(Node n)
      39                 :            : {
      40         [ +  + ]:      90888 :   if (n.getType().isFunction())
      41                 :            :   {
      42                 :            :     // nothing special to do with functions
      43                 :        976 :     return;
      44                 :            :   }
      45                 :      89912 :   NodeManager* nm = n.getNodeManager();
      46                 :      89912 :   Node curr = n;
      47                 :      89912 :   std::vector<Node> args;
      48         [ +  + ]:     128923 :   while (curr.getKind() == Kind::HO_APPLY)
      49                 :            :   {
      50                 :      39011 :     args.insert(args.begin(), curr[1]);
      51                 :      39011 :     curr = curr[0];
      52         [ +  + ]:      39011 :     if (!curr.isVar())
      53                 :            :     {
      54                 :            :       // purify the term
      55                 :       6729 :       context::CDHashSet<Node>::const_iterator itp = d_hoFunOpPurify.find(curr);
      56         [ +  + ]:       6729 :       if (itp != d_hoFunOpPurify.end())
      57                 :            :       {
      58                 :       6201 :         continue;
      59                 :            :       }
      60                 :        528 :       d_hoFunOpPurify.insert(curr);
      61                 :        528 :       Node psk = SkolemManager::mkPurifySkolem(curr);
      62                 :            :       // we do not add it to d_ops since it is an internal operator
      63                 :        528 :       Node eq = psk.eqNode(curr);
      64                 :        528 :       std::vector<Node> children;
      65                 :        528 :       children.push_back(psk);
      66                 :        528 :       children.insert(children.end(), args.begin(), args.end());
      67                 :        528 :       Node p_n = nm->mkNode(Kind::APPLY_UF, children);
      68                 :        528 :       Node eqa = p_n.eqNode(n);
      69                 :       1056 :       Node lem = nm->mkNode(Kind::AND, eq, eqa);
      70                 :        528 :       d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_HO_PURIFY);
      71                 :        528 :     }
      72                 :            :   }
      73 [ +  + ][ +  - ]:      89912 :   if (!args.empty() && curr.isVar())
                 [ +  + ]
      74                 :            :   {
      75                 :            :     // also add standard application version
      76                 :      32282 :     args.insert(args.begin(), curr);
      77                 :      32282 :     Node uf_n = nm->mkNode(Kind::APPLY_UF, args);
      78                 :      32282 :     addTerm(uf_n);
      79                 :      32282 :   }
      80                 :      89912 : }
      81                 :            : 
      82                 :      11117 : void HoTermDb::getOperatorsFor(TNode f, std::vector<TNode>& ops)
      83                 :            : {
      84                 :      11117 :   ops.push_back(f);
      85                 :      11117 :   ops.insert(ops.end(), d_hoOpSlaves[f].begin(), d_hoOpSlaves[f].end());
      86                 :      11117 : }
      87                 :            : 
      88                 :    1173533 : Node HoTermDb::getOperatorRepresentative(TNode op) const
      89                 :            : {
      90                 :    1173533 :   std::map<TNode, TNode>::const_iterator it = d_hoOpRep.find(op);
      91         [ +  + ]:    1173533 :   if (it != d_hoOpRep.end())
      92                 :            :   {
      93                 :    1080793 :     return it->second;
      94                 :            :   }
      95                 :      92740 :   return op;
      96                 :            : }
      97                 :       3950 : bool HoTermDb::finishResetInternal(CVC5_UNUSED Theory::Effort effort)
      98                 :            : {
      99         [ -  + ]:       3950 :   if (!options().quantifiers.hoMergeTermDb)
     100                 :            :   {
     101                 :          0 :     return true;
     102                 :            :   }
     103         [ +  - ]:       7900 :   Trace("quant-ho") << "HoTermDb::reset : compute equal functions..."
     104                 :       3950 :                     << std::endl;
     105                 :            :   // build operator representative map
     106                 :       3950 :   d_hoOpRep.clear();
     107                 :       3950 :   d_hoOpSlaves.clear();
     108                 :       3950 :   eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
     109                 :       3950 :   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
     110         [ +  + ]:     163824 :   while (!eqcs_i.isFinished())
     111                 :            :   {
     112                 :     159874 :     TNode r = (*eqcs_i);
     113         [ +  + ]:     159874 :     if (r.getType().isFunction())
     114                 :            :     {
     115         [ +  - ]:      20306 :       Trace("quant-ho") << "  process function eqc " << r << std::endl;
     116                 :      20306 :       Node first;
     117                 :      20306 :       eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
     118         [ +  + ]:      45521 :       while (!eqc_i.isFinished())
     119                 :            :       {
     120                 :      25215 :         TNode n = (*eqc_i);
     121                 :      25215 :         Node n_use;
     122         [ +  + ]:      25215 :         if (n.isVar())
     123                 :            :         {
     124                 :      23228 :           n_use = n;
     125                 :            :         }
     126         [ +  - ]:      50430 :         Trace("quant-ho") << "  - process " << n_use << ", from " << n
     127                 :      25215 :                           << std::endl;
     128 [ +  + ][ +  + ]:      25215 :         if (!n_use.isNull() && d_opMap.find(n_use) != d_opMap.end())
                 [ +  + ]
     129                 :            :         {
     130         [ +  + ]:      15936 :           if (first.isNull())
     131                 :            :           {
     132                 :      13087 :             first = n_use;
     133                 :      13087 :             d_hoOpRep[n_use] = n_use;
     134                 :            :           }
     135                 :            :           else
     136                 :            :           {
     137         [ +  - ]:       5698 :             Trace("quant-ho") << "  have : " << n_use << " == " << first
     138 [ -  + ][ -  - ]:       2849 :                               << ", type = " << n_use.getType() << std::endl;
     139                 :       2849 :             d_hoOpRep[n_use] = first;
     140                 :       2849 :             d_hoOpSlaves[first].push_back(n_use);
     141                 :            :           }
     142                 :            :         }
     143                 :      25215 :         ++eqc_i;
     144                 :      25215 :       }
     145                 :      20306 :     }
     146                 :     159874 :     ++eqcs_i;
     147                 :     159874 :   }
     148         [ +  - ]:       3950 :   Trace("quant-ho") << "...finished compute equal functions." << std::endl;
     149                 :            : 
     150                 :       3950 :   return true;
     151                 :            : }
     152                 :      41399 : bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp)
     153                 :            : {
     154         [ +  + ]:      41399 :   if (!d_qstate.areDisequal(a, b))
     155                 :            :   {
     156                 :      41392 :     return false;
     157                 :            :   }
     158                 :            :   // operators might be disequal
     159                 :          7 :   Node af = getMatchOperator(a);
     160                 :          7 :   Node bf = getMatchOperator(b);
     161         [ -  + ]:          7 :   if (af != bf)
     162                 :            :   {
     163                 :          0 :     if (a.getKind() == Kind::APPLY_UF && b.getKind() == Kind::APPLY_UF)
     164                 :            :     {
     165                 :          0 :       exp.push_back(af.eqNode(bf));
     166                 :          0 :       Assert(d_qstate.areEqual(af, bf))
     167                 :          0 :           << af << " and " << bf << " are not equal";
     168                 :            :     }
     169                 :            :     else
     170                 :            :     {
     171                 :          0 :       DebugUnhandled();
     172                 :            :       return false;
     173                 :            :     }
     174                 :            :   }
     175                 :          7 :   return true;
     176                 :          7 : }
     177                 :            : 
     178                 :       2758 : Node HoTermDb::getHoTypeMatchPredicate(TypeNode tn)
     179                 :            : {
     180                 :       2758 :   NodeManager* nm = tn.getNodeManager();
     181                 :       2758 :   SkolemManager* sm = nm->getSkolemManager();
     182                 :       2758 :   TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType());
     183                 :            :   return sm->mkInternalSkolemFunction(InternalSkolemId::HO_TYPE_MATCH_PRED,
     184                 :       5516 :                                       ptn);
     185                 :       2758 : }
     186                 :            : 
     187                 :            : }  // namespace quantifiers
     188                 :            : }  // namespace theory
     189                 :            : }  // namespace cvc5::internal