GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_util.cpp Lines: 68 83 81.9 %
Date: 2021-03-22 Branches: 93 224 41.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_util.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Implementation of quantifier utilities
13
 **/
14
15
#include "theory/quantifiers/quant_util.h"
16
17
#include "theory/quantifiers/term_util.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
24
96075
QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
25
96075
  initialize( n, computeEq );
26
96075
}
27
28
96075
void QuantPhaseReq::initialize( Node n, bool computeEq ){
29
192150
  std::map< Node, int > phaseReqs2;
30
96075
  computePhaseReqs( n, false, phaseReqs2 );
31
268271
  for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
32
172196
    if( it->second==1 ){
33
82255
      d_phase_reqs[ it->first ] = true;
34
89941
    }else if( it->second==-1 ){
35
89856
      d_phase_reqs[ it->first ] = false;
36
    }
37
  }
38
96075
  Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;
39
  //now, compute if any patterns are equality required
40
96075
  if( computeEq ){
41
    for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
42
      Debug("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;
43
      if( it->first.getKind()==EQUAL ){
44
        if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){
45
          if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
46
            d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
47
            d_phase_reqs_equality[ it->first[0] ] = it->second;
48
            Debug("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
49
          }
50
        }else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
51
          d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
52
          d_phase_reqs_equality[ it->first[1] ] = it->second;
53
          Debug("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
54
        }
55
      }
56
    }
57
  }
58
96075
}
59
60
302069
void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
61
302069
  bool newReqPol = false;
62
  bool newPolarity;
63
302069
  if( n.getKind()==NOT ){
64
82342
    newReqPol = true;
65
82342
    newPolarity = !polarity;
66
219727
  }else if( n.getKind()==OR || n.getKind()==IMPLIES ){
67
39736
    if( !polarity ){
68
39736
      newReqPol = true;
69
39736
      newPolarity = false;
70
    }
71
179991
  }else if( n.getKind()==AND ){
72
7708
    if( polarity ){
73
      newReqPol = true;
74
      newPolarity = true;
75
    }
76
  }else{
77
172283
    int val = polarity ? 1 : -1;
78
172283
    if( phaseReqs.find( n )==phaseReqs.end() ){
79
172196
      phaseReqs[n] = val;
80
87
    }else if( val!=phaseReqs[n] ){
81
85
      phaseReqs[n] = 0;
82
    }
83
  }
84
302069
  if( newReqPol ){
85
328072
    for( int i=0; i<(int)n.getNumChildren(); i++ ){
86
205994
      if( n.getKind()==IMPLIES && i==0 ){
87
        computePhaseReqs( n[i], !newPolarity, phaseReqs );
88
      }else{
89
205994
        computePhaseReqs( n[i], newPolarity, phaseReqs );
90
      }
91
    }
92
  }
93
302069
}
94
95
1451224
void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
96
1451224
  if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){
97
315375
    newHasPol = hasPol;
98
315375
    newPol = pol;
99
1135849
  }else if( n.getKind()==IMPLIES ){
100
8
    newHasPol = hasPol;
101
8
    newPol = child==0 ? !pol : pol;
102
1135841
  }else if( n.getKind()==NOT ){
103
168516
    newHasPol = hasPol;
104
168516
    newPol = !pol;
105
967325
  }else if( n.getKind()==ITE ){
106
13281
    newHasPol = (child!=0) && hasPol;
107
13281
    newPol = pol;
108
954044
  }else if( n.getKind()==FORALL ){
109
128
    newHasPol = (child==1) && hasPol;
110
128
    newPol = pol;
111
  }else{
112
953916
    newHasPol = false;
113
953916
    newPol = false;
114
  }
115
1451224
}
116
117
3946790
void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
118
3946790
  if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){
119
1934820
    newHasPol = hasPol && pol!=( n.getKind()==OR );
120
1934820
    newPol = pol;
121
2011970
  }else if( n.getKind()==IMPLIES ){
122
20676
    newHasPol = hasPol && !pol;
123
20676
    newPol = child==0 ? !pol : pol;
124
1991294
  }else if( n.getKind()==NOT ){
125
245697
    newHasPol = hasPol;
126
245697
    newPol = !pol;
127
  }else{
128
1745597
    newHasPol = false;
129
1745597
    newPol = false;
130
  }
131
3946790
}
132
133
} /* namespace CVC4::theory */
134
26676
} /* namespace CVC4 */