Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz, Andres Noetzli
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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                 :       1160 : HoTermDb::HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
      32                 :       1160 :     : TermDb(env, qs, qr), d_hoFunOpPurify(userContext())
      33                 :            : {
      34                 :       1160 : }
      35                 :            : 
      36                 :       2316 : HoTermDb::~HoTermDb() {}
      37                 :            : 
      38                 :      80183 : void HoTermDb::addTermInternal(Node n)
      39                 :            : {
      40         [ +  + ]:      80183 :   if (n.getType().isFunction())
      41                 :            :   {
      42                 :            :     // nothing special to do with functions
      43                 :        806 :     return;
      44                 :            :   }
      45                 :      79377 :   NodeManager* nm = NodeManager::currentNM();
      46                 :      79377 :   SkolemManager* sm = nm->getSkolemManager();
      47                 :     158754 :   Node curr = n;
      48                 :     158754 :   std::vector<Node> args;
      49         [ +  + ]:     109650 :   while (curr.getKind() == Kind::HO_APPLY)
      50                 :            :   {
      51                 :      30273 :     args.insert(args.begin(), curr[1]);
      52                 :      30273 :     curr = curr[0];
      53         [ +  + ]:      30273 :     if (!curr.isVar())
      54                 :            :     {
      55                 :            :       // purify the term
      56                 :       6668 :       context::CDHashSet<Node>::const_iterator itp = d_hoFunOpPurify.find(curr);
      57         [ +  + ]:       6668 :       if (itp != d_hoFunOpPurify.end())
      58                 :            :       {
      59                 :       6235 :         continue;
      60                 :            :       }
      61                 :        433 :       d_hoFunOpPurify.insert(curr);
      62                 :        866 :       Node psk = sm->mkPurifySkolem(curr);
      63                 :            :       // we do not add it to d_ops since it is an internal operator
      64                 :        866 :       Node eq = psk.eqNode(curr);
      65                 :        866 :       std::vector<Node> children;
      66                 :        433 :       children.push_back(psk);
      67                 :        433 :       children.insert(children.end(), args.begin(), args.end());
      68                 :        866 :       Node p_n = nm->mkNode(Kind::APPLY_UF, children);
      69                 :        866 :       Node eqa = p_n.eqNode(n);
      70                 :        866 :       Node lem = nm->mkNode(Kind::AND, eq, eqa);
      71                 :        433 :       d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_HO_PURIFY);
      72                 :            :     }
      73                 :            :   }
      74 [ +  + ][ +  - ]:      79377 :   if (!args.empty() && curr.isVar())
                 [ +  + ]
      75                 :            :   {
      76                 :            :     // also add standard application version
      77                 :      23605 :     args.insert(args.begin(), curr);
      78                 :      23605 :     Node uf_n = nm->mkNode(Kind::APPLY_UF, args);
      79                 :      23605 :     addTerm(uf_n);
      80                 :            :   }
      81                 :            : }
      82                 :            : 
      83                 :      12047 : void HoTermDb::getOperatorsFor(TNode f, std::vector<TNode>& ops)
      84                 :            : {
      85                 :      12047 :   ops.push_back(f);
      86                 :      12047 :   ops.insert(ops.end(), d_hoOpSlaves[f].begin(), d_hoOpSlaves[f].end());
      87                 :      12047 : }
      88                 :            : 
      89                 :    1334960 : Node HoTermDb::getOperatorRepresentative(TNode op) const
      90                 :            : {
      91                 :    1334960 :   std::map<TNode, TNode>::const_iterator it = d_hoOpRep.find(op);
      92         [ +  + ]:    1334960 :   if (it != d_hoOpRep.end())
      93                 :            :   {
      94                 :    1235240 :     return it->second;
      95                 :            :   }
      96                 :      99716 :   return op;
      97                 :            : }
      98                 :       3876 : bool HoTermDb::finishResetInternal(Theory::Effort effort)
      99                 :            : {
     100         [ -  + ]:       3876 :   if (!options().quantifiers.hoMergeTermDb)
     101                 :            :   {
     102                 :          0 :     return true;
     103                 :            :   }
     104         [ +  - ]:       7752 :   Trace("quant-ho") << "HoTermDb::reset : compute equal functions..."
     105                 :       3876 :                     << std::endl;
     106                 :            :   // build operator representative map
     107                 :       3876 :   d_hoOpRep.clear();
     108                 :       3876 :   d_hoOpSlaves.clear();
     109                 :       3876 :   eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
     110                 :       3876 :   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
     111         [ +  + ]:     124837 :   while (!eqcs_i.isFinished())
     112                 :            :   {
     113                 :     241922 :     TNode r = (*eqcs_i);
     114         [ +  + ]:     120961 :     if (r.getType().isFunction())
     115                 :            :     {
     116         [ +  - ]:      19354 :       Trace("quant-ho") << "  process function eqc " << r << std::endl;
     117                 :      38708 :       Node first;
     118                 :      19354 :       eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
     119         [ +  + ]:      43490 :       while (!eqc_i.isFinished())
     120                 :            :       {
     121                 :      48272 :         TNode n = (*eqc_i);
     122                 :      48272 :         Node n_use;
     123         [ +  + ]:      24136 :         if (n.isVar())
     124                 :            :         {
     125                 :      22151 :           n_use = n;
     126                 :            :         }
     127         [ +  - ]:      48272 :         Trace("quant-ho") << "  - process " << n_use << ", from " << n
     128                 :      24136 :                           << std::endl;
     129 [ +  + ][ +  + ]:      24136 :         if (!n_use.isNull() && d_opMap.find(n_use) != d_opMap.end())
                 [ +  + ]
     130                 :            :         {
     131         [ +  + ]:      15496 :           if (first.isNull())
     132                 :            :           {
     133                 :      12818 :             first = n_use;
     134                 :      12818 :             d_hoOpRep[n_use] = n_use;
     135                 :            :           }
     136                 :            :           else
     137                 :            :           {
     138         [ +  - ]:       5356 :             Trace("quant-ho") << "  have : " << n_use << " == " << first
     139 [ -  + ][ -  - ]:       2678 :                               << ", type = " << n_use.getType() << std::endl;
     140                 :       2678 :             d_hoOpRep[n_use] = first;
     141                 :       2678 :             d_hoOpSlaves[first].push_back(n_use);
     142                 :            :           }
     143                 :            :         }
     144                 :      24136 :         ++eqc_i;
     145                 :            :       }
     146                 :            :     }
     147                 :     120961 :     ++eqcs_i;
     148                 :            :   }
     149         [ +  - ]:       3876 :   Trace("quant-ho") << "...finished compute equal functions." << std::endl;
     150                 :            : 
     151                 :       3876 :   return true;
     152                 :            : }
     153                 :      42822 : bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp)
     154                 :            : {
     155         [ +  + ]:      42822 :   if (!d_qstate.areDisequal(a, b))
     156                 :            :   {
     157                 :      42814 :     return false;
     158                 :            :   }
     159                 :          8 :   exp.push_back(a.eqNode(b));
     160                 :            :   // operators might be disequal
     161                 :         16 :   Node af = getMatchOperator(a);
     162                 :          8 :   Node bf = getMatchOperator(b);
     163         [ -  + ]:          8 :   if (af != bf)
     164                 :            :   {
     165                 :          0 :     if (a.getKind() == Kind::APPLY_UF && b.getKind() == Kind::APPLY_UF)
     166                 :            :     {
     167                 :          0 :       exp.push_back(af.eqNode(bf).negate());
     168                 :          0 :       Assert(d_qstate.areEqual(af, bf))
     169                 :          0 :           << af << " and " << bf << " are not equal";
     170                 :            :     }
     171                 :            :     else
     172                 :            :     {
     173                 :          0 :       Assert(false);
     174                 :            :       return false;
     175                 :            :     }
     176                 :            :   }
     177                 :          8 :   return true;
     178                 :            : }
     179                 :            : 
     180                 :       3140 : Node HoTermDb::getHoTypeMatchPredicate(TypeNode tn)
     181                 :            : {
     182                 :       3140 :   NodeManager* nm = NodeManager::currentNM();
     183                 :       3140 :   SkolemManager* sm = nm->getSkolemManager();
     184                 :       3140 :   TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType());
     185                 :            :   return sm->mkInternalSkolemFunction(InternalSkolemId::HO_TYPE_MATCH_PRED,
     186                 :       6280 :                                       ptn);
     187                 :            : }
     188                 :            : 
     189                 :            : }  // namespace quantifiers
     190                 :            : }  // namespace theory
     191                 :            : }  // namespace cvc5::internal