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                 :     300048 : QuantifiersUtil::QuantifiersUtil(Env& env) : EnvObj(env) {}
      23                 :            : 
      24                 :          0 : QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
      25                 :          0 :   initialize( n, computeEq );
      26                 :          0 : }
      27                 :            : 
      28                 :          0 : void QuantPhaseReq::initialize( Node n, bool computeEq ){
      29                 :          0 :   std::map< Node, int > phaseReqs2;
      30                 :          0 :   computePhaseReqs( n, false, phaseReqs2 );
      31         [ -  - ]:          0 :   for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
      32         [ -  - ]:          0 :     if( it->second==1 ){
      33                 :          0 :       d_phase_reqs[ it->first ] = true;
      34         [ -  - ]:          0 :     }else if( it->second==-1 ){
      35                 :          0 :       d_phase_reqs[ it->first ] = false;
      36                 :            :     }
      37                 :            :   }
      38         [ -  - ]:          0 :   Trace("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;
      39                 :            :   //now, compute if any patterns are equality required
      40         [ -  - ]:          0 :   if( computeEq ){
      41         [ -  - ]:          0 :     for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
      42         [ -  - ]:          0 :       Trace("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;
      43         [ -  - ]:          0 :       if (it->first.getKind() == Kind::EQUAL)
      44                 :            :       {
      45         [ -  - ]:          0 :         if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){
      46         [ -  - ]:          0 :           if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
      47                 :          0 :             d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
      48                 :          0 :             d_phase_reqs_equality[ it->first[0] ] = it->second;
      49                 :          0 :             Trace("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
      50                 :            :           }
      51         [ -  - ]:          0 :         }else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
      52                 :          0 :           d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
      53                 :          0 :           d_phase_reqs_equality[ it->first[1] ] = it->second;
      54                 :          0 :           Trace("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
      55                 :            :         }
      56                 :            :       }
      57                 :            :     }
      58                 :            :   }
      59                 :          0 : }
      60                 :            : 
      61                 :          0 : void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
      62                 :          0 :   bool newReqPol = false;
      63                 :            :   bool newPolarity;
      64         [ -  - ]:          0 :   if (n.getKind() == Kind::NOT)
      65                 :            :   {
      66                 :          0 :     newReqPol = true;
      67                 :          0 :     newPolarity = !polarity;
      68                 :            :   }
      69 [ -  - ][ -  - ]:          0 :   else if (n.getKind() == Kind::OR || n.getKind() == Kind::IMPLIES)
                 [ -  - ]
      70                 :            :   {
      71         [ -  - ]:          0 :     if( !polarity ){
      72                 :          0 :       newReqPol = true;
      73                 :          0 :       newPolarity = false;
      74                 :            :     }
      75                 :            :   }
      76         [ -  - ]:          0 :   else if (n.getKind() == Kind::AND)
      77                 :            :   {
      78         [ -  - ]:          0 :     if( polarity ){
      79                 :          0 :       newReqPol = true;
      80                 :          0 :       newPolarity = true;
      81                 :            :     }
      82                 :            :   }
      83                 :            :   else
      84                 :            :   {
      85         [ -  - ]:          0 :     int val = polarity ? 1 : -1;
      86         [ -  - ]:          0 :     if( phaseReqs.find( n )==phaseReqs.end() ){
      87                 :          0 :       phaseReqs[n] = val;
      88         [ -  - ]:          0 :     }else if( val!=phaseReqs[n] ){
      89                 :          0 :       phaseReqs[n] = 0;
      90                 :            :     }
      91                 :            :   }
      92         [ -  - ]:          0 :   if( newReqPol ){
      93         [ -  - ]:          0 :     for( int i=0; i<(int)n.getNumChildren(); i++ ){
      94 [ -  - ][ -  - ]:          0 :       if (n.getKind() == Kind::IMPLIES && i == 0)
                 [ -  - ]
      95                 :            :       {
      96                 :          0 :         computePhaseReqs( n[i], !newPolarity, phaseReqs );
      97                 :            :       }
      98                 :            :       else
      99                 :            :       {
     100                 :          0 :         computePhaseReqs( n[i], newPolarity, phaseReqs );
     101                 :            :       }
     102                 :            :     }
     103                 :            :   }
     104                 :          0 : }
     105                 :            : 
     106                 :    3859544 : void QuantPhaseReq::getPolarity(
     107                 :            :     Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol)
     108                 :            : {
     109         [ +  + ]:    7500344 :   if (n.getKind() == Kind::AND || n.getKind() == Kind::OR
     110 [ +  + ][ +  + ]:    7500344 :       || n.getKind() == Kind::SEP_STAR)
                 [ +  + ]
     111                 :            :   {
     112                 :    1044730 :     newHasPol = hasPol;
     113                 :    1044730 :     newPol = pol;
     114                 :            :   }
     115         [ +  + ]:    2814814 :   else if (n.getKind() == Kind::IMPLIES)
     116                 :            :   {
     117                 :       3676 :     newHasPol = hasPol;
     118         [ +  + ]:       5514 :     newPol = child==0 ? !pol : pol;
     119                 :            :   }
     120         [ +  + ]:    2811138 :   else if (n.getKind() == Kind::NOT)
     121                 :            :   {
     122                 :     536552 :     newHasPol = hasPol;
     123                 :     536552 :     newPol = !pol;
     124                 :            :   }
     125         [ +  + ]:    2274586 :   else if (n.getKind() == Kind::ITE)
     126                 :            :   {
     127 [ +  + ][ +  + ]:      29430 :     newHasPol = (child!=0) && hasPol;
     128                 :      29430 :     newPol = pol;
     129                 :            :   }
     130         [ -  + ]:    2245156 :   else if (n.getKind() == Kind::FORALL)
     131                 :            :   {
     132 [ -  - ][ -  - ]:          0 :     newHasPol = (child==1) && hasPol;
     133                 :          0 :     newPol = pol;
     134                 :            :   }
     135                 :            :   else
     136                 :            :   {
     137                 :    2245156 :     newHasPol = false;
     138                 :    2245156 :     newPol = false;
     139                 :            :   }
     140                 :       1838 : }
     141                 :            : 
     142                 :     849555 : void QuantPhaseReq::getEntailPolarity(
     143                 :            :     Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol)
     144                 :            : {
     145         [ +  + ]:    1678786 :   if (n.getKind() == Kind::AND || n.getKind() == Kind::OR
     146 [ +  + ][ +  + ]:    1678786 :       || n.getKind() == Kind::SEP_STAR)
                 [ +  + ]
     147                 :            :   {
     148 [ +  + ][ +  + ]:     115200 :     newHasPol = hasPol && pol != (n.getKind() == Kind::OR);
     149                 :     115200 :     newPol = pol;
     150                 :            :   }
     151         [ +  + ]:     734355 :   else if (n.getKind() == Kind::IMPLIES)
     152                 :            :   {
     153 [ -  + ][ -  - ]:         12 :     newHasPol = hasPol && !pol;
     154         [ +  + ]:         18 :     newPol = child==0 ? !pol : pol;
     155                 :            :   }
     156         [ +  + ]:     734343 :   else if (n.getKind() == Kind::NOT)
     157                 :            :   {
     158                 :      85012 :     newHasPol = hasPol;
     159                 :      85012 :     newPol = !pol;
     160                 :            :   }
     161                 :            :   else
     162                 :            :   {
     163                 :     649331 :     newHasPol = false;
     164                 :     649331 :     newPol = false;
     165                 :            :   }
     166                 :          6 : }
     167                 :            : 
     168                 :            : }  // namespace theory
     169                 :            : }  // namespace cvc5::internal