Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz, Morgan Deters
       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 quantifier utilities
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/quantifiers/quant_util.h"
      17                 :            : 
      18                 :            : #include "theory/quantifiers/term_util.h"
      19                 :            : 
      20                 :            : using namespace cvc5::internal::kind;
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace theory {
      24                 :            : 
      25                 :     298461 : QuantifiersUtil::QuantifiersUtil(Env& env) : EnvObj(env) {}
      26                 :            : 
      27                 :     314797 : QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
      28                 :     314797 :   initialize( n, computeEq );
      29                 :     314797 : }
      30                 :            : 
      31                 :     314797 : void QuantPhaseReq::initialize( Node n, bool computeEq ){
      32                 :     629594 :   std::map< Node, int > phaseReqs2;
      33                 :     314797 :   computePhaseReqs( n, false, phaseReqs2 );
      34         [ +  + ]:     862410 :   for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
      35         [ +  + ]:     547613 :     if( it->second==1 ){
      36                 :     250752 :       d_phase_reqs[ it->first ] = true;
      37         [ +  - ]:     296861 :     }else if( it->second==-1 ){
      38                 :     296861 :       d_phase_reqs[ it->first ] = false;
      39                 :            :     }
      40                 :            :   }
      41         [ +  - ]:     314797 :   Trace("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;
      42                 :            :   //now, compute if any patterns are equality required
      43         [ -  + ]:     314797 :   if( computeEq ){
      44         [ -  - ]:          0 :     for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
      45         [ -  - ]:          0 :       Trace("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;
      46         [ -  - ]:          0 :       if (it->first.getKind() == Kind::EQUAL)
      47                 :            :       {
      48         [ -  - ]:          0 :         if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){
      49         [ -  - ]:          0 :           if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
      50                 :          0 :             d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
      51                 :          0 :             d_phase_reqs_equality[ it->first[0] ] = it->second;
      52                 :          0 :             Trace("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
      53                 :            :           }
      54         [ -  - ]:          0 :         }else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
      55                 :          0 :           d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
      56                 :          0 :           d_phase_reqs_equality[ it->first[1] ] = it->second;
      57                 :          0 :           Trace("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
      58                 :            :         }
      59                 :            :       }
      60                 :            :     }
      61                 :            :   }
      62                 :     314797 : }
      63                 :            : 
      64                 :     957794 : void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
      65                 :     957794 :   bool newReqPol = false;
      66                 :            :   bool newPolarity;
      67         [ +  + ]:     957794 :   if (n.getKind() == Kind::NOT)
      68                 :            :   {
      69                 :     250752 :     newReqPol = true;
      70                 :     250752 :     newPolarity = !polarity;
      71                 :            :   }
      72 [ +  + ][ -  + ]:     707042 :   else if (n.getKind() == Kind::OR || n.getKind() == Kind::IMPLIES)
                 [ +  + ]
      73                 :            :   {
      74         [ +  - ]:     133379 :     if( !polarity ){
      75                 :     133379 :       newReqPol = true;
      76                 :     133379 :       newPolarity = false;
      77                 :            :     }
      78                 :            :   }
      79         [ +  + ]:     573663 :   else if (n.getKind() == Kind::AND)
      80                 :            :   {
      81         [ -  + ]:      26050 :     if( polarity ){
      82                 :          0 :       newReqPol = true;
      83                 :          0 :       newPolarity = true;
      84                 :            :     }
      85                 :            :   }
      86                 :            :   else
      87                 :            :   {
      88         [ +  + ]:     547613 :     int val = polarity ? 1 : -1;
      89         [ +  - ]:     547613 :     if( phaseReqs.find( n )==phaseReqs.end() ){
      90                 :     547613 :       phaseReqs[n] = val;
      91         [ -  - ]:          0 :     }else if( val!=phaseReqs[n] ){
      92                 :          0 :       phaseReqs[n] = 0;
      93                 :            :     }
      94                 :            :   }
      95         [ +  + ]:     957794 :   if( newReqPol ){
      96         [ +  + ]:    1027130 :     for( int i=0; i<(int)n.getNumChildren(); i++ ){
      97 [ -  + ][ -  - ]:     642997 :       if (n.getKind() == Kind::IMPLIES && i == 0)
                 [ -  + ]
      98                 :            :       {
      99                 :          0 :         computePhaseReqs( n[i], !newPolarity, phaseReqs );
     100                 :            :       }
     101                 :            :       else
     102                 :            :       {
     103                 :     642997 :         computePhaseReqs( n[i], newPolarity, phaseReqs );
     104                 :            :       }
     105                 :            :     }
     106                 :            :   }
     107                 :     957794 : }
     108                 :            : 
     109                 :    5458620 : void QuantPhaseReq::getPolarity(
     110                 :            :     Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol)
     111                 :            : {
     112         [ +  + ]:   10569100 :   if (n.getKind() == Kind::AND || n.getKind() == Kind::OR
     113 [ +  + ][ +  + ]:   10569100 :       || n.getKind() == Kind::SEP_STAR)
                 [ +  + ]
     114                 :            :   {
     115                 :    1645120 :     newHasPol = hasPol;
     116                 :    1645120 :     newPol = pol;
     117                 :            :   }
     118         [ +  + ]:    3813490 :   else if (n.getKind() == Kind::IMPLIES)
     119                 :            :   {
     120                 :          8 :     newHasPol = hasPol;
     121         [ +  + ]:         12 :     newPol = child==0 ? !pol : pol;
     122                 :            :   }
     123         [ +  + ]:    3813480 :   else if (n.getKind() == Kind::NOT)
     124                 :            :   {
     125                 :     704710 :     newHasPol = hasPol;
     126                 :     704710 :     newPol = !pol;
     127                 :            :   }
     128         [ +  + ]:    3108770 :   else if (n.getKind() == Kind::ITE)
     129                 :            :   {
     130 [ +  + ][ +  + ]:      30501 :     newHasPol = (child!=0) && hasPol;
     131                 :      30501 :     newPol = pol;
     132                 :            :   }
     133         [ +  + ]:    3078270 :   else if (n.getKind() == Kind::FORALL)
     134                 :            :   {
     135 [ +  + ][ +  + ]:        446 :     newHasPol = (child==1) && hasPol;
     136                 :        446 :     newPol = pol;
     137                 :            :   }
     138                 :            :   else
     139                 :            :   {
     140                 :    3077830 :     newHasPol = false;
     141                 :    3077830 :     newPol = false;
     142                 :            :   }
     143                 :          4 : }
     144                 :            : 
     145                 :     951425 : void QuantPhaseReq::getEntailPolarity(
     146                 :            :     Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol)
     147                 :            : {
     148         [ +  + ]:    1880770 :   if (n.getKind() == Kind::AND || n.getKind() == Kind::OR
     149 [ +  + ][ +  + ]:    1880770 :       || n.getKind() == Kind::SEP_STAR)
                 [ +  + ]
     150                 :            :   {
     151 [ +  + ][ +  + ]:     130260 :     newHasPol = hasPol && pol != (n.getKind() == Kind::OR);
     152                 :     130260 :     newPol = pol;
     153                 :            :   }
     154         [ +  + ]:     821165 :   else if (n.getKind() == Kind::IMPLIES)
     155                 :            :   {
     156 [ -  + ][ -  - ]:         12 :     newHasPol = hasPol && !pol;
     157         [ +  + ]:         18 :     newPol = child==0 ? !pol : pol;
     158                 :            :   }
     159         [ +  + ]:     821153 :   else if (n.getKind() == Kind::NOT)
     160                 :            :   {
     161                 :      97139 :     newHasPol = hasPol;
     162                 :      97139 :     newPol = !pol;
     163                 :            :   }
     164                 :            :   else
     165                 :            :   {
     166                 :     724014 :     newHasPol = false;
     167                 :     724014 :     newPol = false;
     168                 :            :   }
     169                 :          6 : }
     170                 :            : 
     171                 :            : }  // namespace theory
     172                 :            : }  // namespace cvc5::internal