1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
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::kind; |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace theory { |
24 |
|
|
25 |
31387 |
QuantifiersUtil::QuantifiersUtil(Env& env) : EnvObj(env) {} |
26 |
|
|
27 |
51919 |
QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ |
28 |
51919 |
initialize( n, computeEq ); |
29 |
51919 |
} |
30 |
|
|
31 |
51919 |
void QuantPhaseReq::initialize( Node n, bool computeEq ){ |
32 |
103838 |
std::map< Node, int > phaseReqs2; |
33 |
51919 |
computePhaseReqs( n, false, phaseReqs2 ); |
34 |
139812 |
for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){ |
35 |
87893 |
if( it->second==1 ){ |
36 |
39851 |
d_phase_reqs[ it->first ] = true; |
37 |
48042 |
}else if( it->second==-1 ){ |
38 |
47989 |
d_phase_reqs[ it->first ] = false; |
39 |
|
} |
40 |
|
} |
41 |
51919 |
Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl; |
42 |
|
//now, compute if any patterns are equality required |
43 |
51919 |
if( computeEq ){ |
44 |
|
for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){ |
45 |
|
Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl; |
46 |
|
if( it->first.getKind()==EQUAL ){ |
47 |
|
if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){ |
48 |
|
if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ |
49 |
|
d_phase_reqs_equality_term[ it->first[0] ] = it->first[1]; |
50 |
|
d_phase_reqs_equality[ it->first[0] ] = it->second; |
51 |
|
Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl; |
52 |
|
} |
53 |
|
}else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ |
54 |
|
d_phase_reqs_equality_term[ it->first[1] ] = it->first[0]; |
55 |
|
d_phase_reqs_equality[ it->first[1] ] = it->second; |
56 |
|
Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl; |
57 |
|
} |
58 |
|
} |
59 |
|
} |
60 |
|
} |
61 |
51919 |
} |
62 |
|
|
63 |
153175 |
void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){ |
64 |
153175 |
bool newReqPol = false; |
65 |
|
bool newPolarity; |
66 |
153175 |
if( n.getKind()==NOT ){ |
67 |
39906 |
newReqPol = true; |
68 |
39906 |
newPolarity = !polarity; |
69 |
113269 |
}else if( n.getKind()==OR || n.getKind()==IMPLIES ){ |
70 |
20330 |
if( !polarity ){ |
71 |
20330 |
newReqPol = true; |
72 |
20330 |
newPolarity = false; |
73 |
|
} |
74 |
92939 |
}else if( n.getKind()==AND ){ |
75 |
4991 |
if( polarity ){ |
76 |
|
newReqPol = true; |
77 |
|
newPolarity = true; |
78 |
|
} |
79 |
|
}else{ |
80 |
87948 |
int val = polarity ? 1 : -1; |
81 |
87948 |
if( phaseReqs.find( n )==phaseReqs.end() ){ |
82 |
87893 |
phaseReqs[n] = val; |
83 |
55 |
}else if( val!=phaseReqs[n] ){ |
84 |
53 |
phaseReqs[n] = 0; |
85 |
|
} |
86 |
|
} |
87 |
153175 |
if( newReqPol ){ |
88 |
161492 |
for( int i=0; i<(int)n.getNumChildren(); i++ ){ |
89 |
101256 |
if( n.getKind()==IMPLIES && i==0 ){ |
90 |
|
computePhaseReqs( n[i], !newPolarity, phaseReqs ); |
91 |
|
}else{ |
92 |
101256 |
computePhaseReqs( n[i], newPolarity, phaseReqs ); |
93 |
|
} |
94 |
|
} |
95 |
|
} |
96 |
153175 |
} |
97 |
|
|
98 |
711615 |
void QuantPhaseReq::getPolarity( |
99 |
|
Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol) |
100 |
|
{ |
101 |
711615 |
if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ |
102 |
161830 |
newHasPol = hasPol; |
103 |
161830 |
newPol = pol; |
104 |
549785 |
}else if( n.getKind()==IMPLIES ){ |
105 |
8 |
newHasPol = hasPol; |
106 |
8 |
newPol = child==0 ? !pol : pol; |
107 |
549777 |
}else if( n.getKind()==NOT ){ |
108 |
80247 |
newHasPol = hasPol; |
109 |
80247 |
newPol = !pol; |
110 |
469530 |
}else if( n.getKind()==ITE ){ |
111 |
8106 |
newHasPol = (child!=0) && hasPol; |
112 |
8106 |
newPol = pol; |
113 |
461424 |
}else if( n.getKind()==FORALL ){ |
114 |
52 |
newHasPol = (child==1) && hasPol; |
115 |
52 |
newPol = pol; |
116 |
|
}else{ |
117 |
461372 |
newHasPol = false; |
118 |
461372 |
newPol = false; |
119 |
|
} |
120 |
711615 |
} |
121 |
|
|
122 |
2449662 |
void QuantPhaseReq::getEntailPolarity( |
123 |
|
Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol) |
124 |
|
{ |
125 |
2449662 |
if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ |
126 |
1438419 |
newHasPol = hasPol && pol!=( n.getKind()==OR ); |
127 |
1438419 |
newPol = pol; |
128 |
1011243 |
}else if( n.getKind()==IMPLIES ){ |
129 |
13126 |
newHasPol = hasPol && !pol; |
130 |
13126 |
newPol = child==0 ? !pol : pol; |
131 |
998117 |
}else if( n.getKind()==NOT ){ |
132 |
134623 |
newHasPol = hasPol; |
133 |
134623 |
newPol = !pol; |
134 |
|
}else{ |
135 |
863494 |
newHasPol = false; |
136 |
863494 |
newPol = false; |
137 |
|
} |
138 |
2449662 |
} |
139 |
|
|
140 |
|
} // namespace theory |
141 |
22746 |
} // namespace cvc5 |