Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Implementation of quantifier utilities
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/quant_util.h"
      14                 :            : 
      15                 :            : #include "theory/quantifiers/term_util.h"
      16                 :            : 
      17                 :            : using namespace cvc5::internal::kind;
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : namespace theory {
      21                 :            : 
      22                 :     308310 : QuantifiersUtil::QuantifiersUtil(Env& env) : EnvObj(env) {}
      23                 :            : 
      24                 :          0 : QuantPhaseReq::QuantPhaseReq(Node n, bool computeEq)
      25                 :            : {
      26                 :          0 :   initialize(n, computeEq);
      27                 :          0 : }
      28                 :            : 
      29                 :          0 : void QuantPhaseReq::initialize(Node n, bool computeEq)
      30                 :            : {
      31                 :          0 :   std::map<Node, int> phaseReqs2;
      32                 :          0 :   computePhaseReqs(n, false, phaseReqs2);
      33                 :          0 :   for (std::map<Node, int>::iterator it = phaseReqs2.begin();
      34         [ -  - ]:          0 :        it != phaseReqs2.end();
      35                 :          0 :        ++it)
      36                 :            :   {
      37         [ -  - ]:          0 :     if (it->second == 1)
      38                 :            :     {
      39                 :          0 :       d_phase_reqs[it->first] = true;
      40                 :            :     }
      41         [ -  - ]:          0 :     else if (it->second == -1)
      42                 :            :     {
      43                 :          0 :       d_phase_reqs[it->first] = false;
      44                 :            :     }
      45                 :            :   }
      46         [ -  - ]:          0 :   Trace("inst-engine-phase-req")
      47                 :          0 :       << "Phase requirements for " << n << ":" << std::endl;
      48                 :            :   // now, compute if any patterns are equality required
      49         [ -  - ]:          0 :   if (computeEq)
      50                 :            :   {
      51                 :          0 :     for (std::map<Node, bool>::iterator it = d_phase_reqs.begin();
      52         [ -  - ]:          0 :          it != d_phase_reqs.end();
      53                 :          0 :          ++it)
      54                 :            :     {
      55         [ -  - ]:          0 :       Trace("inst-engine-phase-req")
      56                 :          0 :           << "   " << it->first << " -> " << it->second << std::endl;
      57         [ -  - ]:          0 :       if (it->first.getKind() == Kind::EQUAL)
      58                 :            :       {
      59         [ -  - ]:          0 :         if (quantifiers::TermUtil::hasInstConstAttr(it->first[0]))
      60                 :            :         {
      61         [ -  - ]:          0 :           if (!quantifiers::TermUtil::hasInstConstAttr(it->first[1]))
      62                 :            :           {
      63                 :          0 :             d_phase_reqs_equality_term[it->first[0]] = it->first[1];
      64                 :          0 :             d_phase_reqs_equality[it->first[0]] = it->second;
      65         [ -  - ]:          0 :             Trace("inst-engine-phase-req")
      66                 :          0 :                 << "      " << it->first[0] << (it->second ? " == " : " != ")
      67                 :          0 :                 << it->first[1] << std::endl;
      68                 :            :           }
      69                 :            :         }
      70         [ -  - ]:          0 :         else if (quantifiers::TermUtil::hasInstConstAttr(it->first[1]))
      71                 :            :         {
      72                 :          0 :           d_phase_reqs_equality_term[it->first[1]] = it->first[0];
      73                 :          0 :           d_phase_reqs_equality[it->first[1]] = it->second;
      74         [ -  - ]:          0 :           Trace("inst-engine-phase-req")
      75                 :          0 :               << "      " << it->first[1] << (it->second ? " == " : " != ")
      76                 :          0 :               << it->first[0] << std::endl;
      77                 :            :         }
      78                 :            :       }
      79                 :            :     }
      80                 :            :   }
      81                 :          0 : }
      82                 :            : 
      83                 :          0 : void QuantPhaseReq::computePhaseReqs(Node n,
      84                 :            :                                      bool polarity,
      85                 :            :                                      std::map<Node, int>& phaseReqs)
      86                 :            : {
      87                 :          0 :   bool newReqPol = false;
      88                 :            :   bool newPolarity;
      89         [ -  - ]:          0 :   if (n.getKind() == Kind::NOT)
      90                 :            :   {
      91                 :          0 :     newReqPol = true;
      92                 :          0 :     newPolarity = !polarity;
      93                 :            :   }
      94 [ -  - ][ -  - ]:          0 :   else if (n.getKind() == Kind::OR || n.getKind() == Kind::IMPLIES)
                 [ -  - ]
      95                 :            :   {
      96         [ -  - ]:          0 :     if (!polarity)
      97                 :            :     {
      98                 :          0 :       newReqPol = true;
      99                 :          0 :       newPolarity = false;
     100                 :            :     }
     101                 :            :   }
     102         [ -  - ]:          0 :   else if (n.getKind() == Kind::AND)
     103                 :            :   {
     104         [ -  - ]:          0 :     if (polarity)
     105                 :            :     {
     106                 :          0 :       newReqPol = true;
     107                 :          0 :       newPolarity = true;
     108                 :            :     }
     109                 :            :   }
     110                 :            :   else
     111                 :            :   {
     112         [ -  - ]:          0 :     int val = polarity ? 1 : -1;
     113         [ -  - ]:          0 :     if (phaseReqs.find(n) == phaseReqs.end())
     114                 :            :     {
     115                 :          0 :       phaseReqs[n] = val;
     116                 :            :     }
     117         [ -  - ]:          0 :     else if (val != phaseReqs[n])
     118                 :            :     {
     119                 :          0 :       phaseReqs[n] = 0;
     120                 :            :     }
     121                 :            :   }
     122         [ -  - ]:          0 :   if (newReqPol)
     123                 :            :   {
     124         [ -  - ]:          0 :     for (int i = 0; i < (int)n.getNumChildren(); i++)
     125                 :            :     {
     126 [ -  - ][ -  - ]:          0 :       if (n.getKind() == Kind::IMPLIES && i == 0)
                 [ -  - ]
     127                 :            :       {
     128                 :          0 :         computePhaseReqs(n[i], !newPolarity, phaseReqs);
     129                 :            :       }
     130                 :            :       else
     131                 :            :       {
     132                 :          0 :         computePhaseReqs(n[i], newPolarity, phaseReqs);
     133                 :            :       }
     134                 :            :     }
     135                 :            :   }
     136                 :          0 : }
     137                 :            : 
     138                 :    4886364 : void QuantPhaseReq::getPolarity(
     139                 :            :     Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol)
     140                 :            : {
     141         [ +  + ]:    9485742 :   if (n.getKind() == Kind::AND || n.getKind() == Kind::OR
     142 [ +  + ][ +  + ]:    9485742 :       || n.getKind() == Kind::SEP_STAR)
                 [ +  + ]
     143                 :            :   {
     144                 :    1376540 :     newHasPol = hasPol;
     145                 :    1376540 :     newPol = pol;
     146                 :            :   }
     147         [ +  + ]:    3509824 :   else if (n.getKind() == Kind::IMPLIES)
     148                 :            :   {
     149                 :       5488 :     newHasPol = hasPol;
     150         [ +  + ]:       8232 :     newPol = child == 0 ? !pol : pol;
     151                 :            :   }
     152         [ +  + ]:    3504336 :   else if (n.getKind() == Kind::NOT)
     153                 :            :   {
     154                 :     700334 :     newHasPol = hasPol;
     155                 :     700334 :     newPol = !pol;
     156                 :            :   }
     157         [ +  + ]:    2804002 :   else if (n.getKind() == Kind::ITE)
     158                 :            :   {
     159 [ +  + ][ +  + ]:      37380 :     newHasPol = (child != 0) && hasPol;
     160                 :      37380 :     newPol = pol;
     161                 :            :   }
     162         [ -  + ]:    2766622 :   else if (n.getKind() == Kind::FORALL)
     163                 :            :   {
     164 [ -  - ][ -  - ]:          0 :     newHasPol = (child == 1) && hasPol;
     165                 :          0 :     newPol = pol;
     166                 :            :   }
     167                 :            :   else
     168                 :            :   {
     169                 :    2766622 :     newHasPol = false;
     170                 :    2766622 :     newPol = false;
     171                 :            :   }
     172                 :       2744 : }
     173                 :            : 
     174                 :     851569 : void QuantPhaseReq::getEntailPolarity(
     175                 :            :     Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol)
     176                 :            : {
     177         [ +  + ]:    1682817 :   if (n.getKind() == Kind::AND || n.getKind() == Kind::OR
     178 [ +  + ][ +  + ]:    1682817 :       || n.getKind() == Kind::SEP_STAR)
                 [ +  + ]
     179                 :            :   {
     180 [ +  + ][ +  + ]:     114938 :     newHasPol = hasPol && pol != (n.getKind() == Kind::OR);
     181                 :     114938 :     newPol = pol;
     182                 :            :   }
     183         [ +  + ]:     736631 :   else if (n.getKind() == Kind::IMPLIES)
     184                 :            :   {
     185 [ -  + ][ -  - ]:         12 :     newHasPol = hasPol && !pol;
     186         [ +  + ]:         18 :     newPol = child == 0 ? !pol : pol;
     187                 :            :   }
     188         [ +  + ]:     736619 :   else if (n.getKind() == Kind::NOT)
     189                 :            :   {
     190                 :      85127 :     newHasPol = hasPol;
     191                 :      85127 :     newPol = !pol;
     192                 :            :   }
     193                 :            :   else
     194                 :            :   {
     195                 :     651492 :     newHasPol = false;
     196                 :     651492 :     newPol = false;
     197                 :            :   }
     198                 :          6 : }
     199                 :            : 
     200                 :            : }  // namespace theory
     201                 :            : }  // namespace cvc5::internal