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 |
97124 |
QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ |
26 |
97124 |
initialize( n, computeEq ); |
27 |
97124 |
} |
28 |
|
|
29 |
97124 |
void QuantPhaseReq::initialize( Node n, bool computeEq ){ |
30 |
194248 |
std::map< Node, int > phaseReqs2; |
31 |
97124 |
computePhaseReqs( n, false, phaseReqs2 ); |
32 |
269335 |
for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){ |
33 |
172211 |
if( it->second==1 ){ |
34 |
80491 |
d_phase_reqs[ it->first ] = true; |
35 |
91720 |
}else if( it->second==-1 ){ |
36 |
91653 |
d_phase_reqs[ it->first ] = false; |
37 |
|
} |
38 |
|
} |
39 |
97124 |
Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl; |
40 |
|
//now, compute if any patterns are equality required |
41 |
97124 |
if( computeEq ){ |
42 |
|
for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){ |
43 |
|
Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl; |
44 |
|
if( it->first.getKind()==EQUAL ){ |
45 |
|
if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){ |
46 |
|
if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ |
47 |
|
d_phase_reqs_equality_term[ it->first[0] ] = it->first[1]; |
48 |
|
d_phase_reqs_equality[ it->first[0] ] = it->second; |
49 |
|
Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl; |
50 |
|
} |
51 |
|
}else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ |
52 |
|
d_phase_reqs_equality_term[ it->first[1] ] = it->first[0]; |
53 |
|
d_phase_reqs_equality[ it->first[1] ] = it->second; |
54 |
|
Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl; |
55 |
|
} |
56 |
|
} |
57 |
|
} |
58 |
|
} |
59 |
97124 |
} |
60 |
|
|
61 |
300740 |
void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){ |
62 |
300740 |
bool newReqPol = false; |
63 |
|
bool newPolarity; |
64 |
300740 |
if( n.getKind()==NOT ){ |
65 |
80560 |
newReqPol = true; |
66 |
80560 |
newPolarity = !polarity; |
67 |
220180 |
}else if( n.getKind()==OR || n.getKind()==IMPLIES ){ |
68 |
40122 |
if( !polarity ){ |
69 |
40122 |
newReqPol = true; |
70 |
40122 |
newPolarity = false; |
71 |
|
} |
72 |
180058 |
}else if( n.getKind()==AND ){ |
73 |
7778 |
if( polarity ){ |
74 |
|
newReqPol = true; |
75 |
|
newPolarity = true; |
76 |
|
} |
77 |
|
}else{ |
78 |
172280 |
int val = polarity ? 1 : -1; |
79 |
172280 |
if( phaseReqs.find( n )==phaseReqs.end() ){ |
80 |
172211 |
phaseReqs[n] = val; |
81 |
69 |
}else if( val!=phaseReqs[n] ){ |
82 |
67 |
phaseReqs[n] = 0; |
83 |
|
} |
84 |
|
} |
85 |
300740 |
if( newReqPol ){ |
86 |
324298 |
for( int i=0; i<(int)n.getNumChildren(); i++ ){ |
87 |
203616 |
if( n.getKind()==IMPLIES && i==0 ){ |
88 |
|
computePhaseReqs( n[i], !newPolarity, phaseReqs ); |
89 |
|
}else{ |
90 |
203616 |
computePhaseReqs( n[i], newPolarity, phaseReqs ); |
91 |
|
} |
92 |
|
} |
93 |
|
} |
94 |
300740 |
} |
95 |
|
|
96 |
1343695 |
void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { |
97 |
1343695 |
if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ |
98 |
305044 |
newHasPol = hasPol; |
99 |
305044 |
newPol = pol; |
100 |
1038651 |
}else if( n.getKind()==IMPLIES ){ |
101 |
8 |
newHasPol = hasPol; |
102 |
8 |
newPol = child==0 ? !pol : pol; |
103 |
1038643 |
}else if( n.getKind()==NOT ){ |
104 |
157718 |
newHasPol = hasPol; |
105 |
157718 |
newPol = !pol; |
106 |
880925 |
}else if( n.getKind()==ITE ){ |
107 |
12456 |
newHasPol = (child!=0) && hasPol; |
108 |
12456 |
newPol = pol; |
109 |
868469 |
}else if( n.getKind()==FORALL ){ |
110 |
164 |
newHasPol = (child==1) && hasPol; |
111 |
164 |
newPol = pol; |
112 |
|
}else{ |
113 |
868305 |
newHasPol = false; |
114 |
868305 |
newPol = false; |
115 |
|
} |
116 |
1343695 |
} |
117 |
|
|
118 |
4172023 |
void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { |
119 |
4172023 |
if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ |
120 |
2134904 |
newHasPol = hasPol && pol!=( n.getKind()==OR ); |
121 |
2134904 |
newPol = pol; |
122 |
2037119 |
}else if( n.getKind()==IMPLIES ){ |
123 |
23012 |
newHasPol = hasPol && !pol; |
124 |
23012 |
newPol = child==0 ? !pol : pol; |
125 |
2014107 |
}else if( n.getKind()==NOT ){ |
126 |
258842 |
newHasPol = hasPol; |
127 |
258842 |
newPol = !pol; |
128 |
|
}else{ |
129 |
1755265 |
newHasPol = false; |
130 |
1755265 |
newPol = false; |
131 |
|
} |
132 |
4172023 |
} |
133 |
|
|
134 |
|
} // namespace theory |
135 |
29340 |
} // namespace cvc5 |