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 |
49742 |
QuantifiersUtil::QuantifiersUtil(Env& env) : EnvObj(env) {} |
26 |
|
|
27 |
112782 |
QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ |
28 |
112782 |
initialize( n, computeEq ); |
29 |
112782 |
} |
30 |
|
|
31 |
112782 |
void QuantPhaseReq::initialize( Node n, bool computeEq ){ |
32 |
225564 |
std::map< Node, int > phaseReqs2; |
33 |
112782 |
computePhaseReqs( n, false, phaseReqs2 ); |
34 |
309048 |
for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){ |
35 |
196266 |
if( it->second==1 ){ |
36 |
88702 |
d_phase_reqs[ it->first ] = true; |
37 |
107564 |
}else if( it->second==-1 ){ |
38 |
107497 |
d_phase_reqs[ it->first ] = false; |
39 |
|
} |
40 |
|
} |
41 |
112782 |
Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl; |
42 |
|
//now, compute if any patterns are equality required |
43 |
112782 |
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 |
112782 |
} |
62 |
|
|
63 |
340080 |
void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){ |
64 |
340080 |
bool newReqPol = false; |
65 |
|
bool newPolarity; |
66 |
340080 |
if( n.getKind()==NOT ){ |
67 |
88771 |
newReqPol = true; |
68 |
88771 |
newPolarity = !polarity; |
69 |
251309 |
}else if( n.getKind()==OR || n.getKind()==IMPLIES ){ |
70 |
45439 |
if( !polarity ){ |
71 |
45439 |
newReqPol = true; |
72 |
45439 |
newPolarity = false; |
73 |
|
} |
74 |
205870 |
}else if( n.getKind()==AND ){ |
75 |
9535 |
if( polarity ){ |
76 |
|
newReqPol = true; |
77 |
|
newPolarity = true; |
78 |
|
} |
79 |
|
}else{ |
80 |
196335 |
int val = polarity ? 1 : -1; |
81 |
196335 |
if( phaseReqs.find( n )==phaseReqs.end() ){ |
82 |
196266 |
phaseReqs[n] = val; |
83 |
69 |
}else if( val!=phaseReqs[n] ){ |
84 |
67 |
phaseReqs[n] = 0; |
85 |
|
} |
86 |
|
} |
87 |
340080 |
if( newReqPol ){ |
88 |
361508 |
for( int i=0; i<(int)n.getNumChildren(); i++ ){ |
89 |
227298 |
if( n.getKind()==IMPLIES && i==0 ){ |
90 |
|
computePhaseReqs( n[i], !newPolarity, phaseReqs ); |
91 |
|
}else{ |
92 |
227298 |
computePhaseReqs( n[i], newPolarity, phaseReqs ); |
93 |
|
} |
94 |
|
} |
95 |
|
} |
96 |
340080 |
} |
97 |
|
|
98 |
1508234 |
void QuantPhaseReq::getPolarity( |
99 |
|
Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol) |
100 |
|
{ |
101 |
1508234 |
if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ |
102 |
347975 |
newHasPol = hasPol; |
103 |
347975 |
newPol = pol; |
104 |
1160259 |
}else if( n.getKind()==IMPLIES ){ |
105 |
8 |
newHasPol = hasPol; |
106 |
8 |
newPol = child==0 ? !pol : pol; |
107 |
1160251 |
}else if( n.getKind()==NOT ){ |
108 |
175540 |
newHasPol = hasPol; |
109 |
175540 |
newPol = !pol; |
110 |
984711 |
}else if( n.getKind()==ITE ){ |
111 |
15861 |
newHasPol = (child!=0) && hasPol; |
112 |
15861 |
newPol = pol; |
113 |
968850 |
}else if( n.getKind()==FORALL ){ |
114 |
152 |
newHasPol = (child==1) && hasPol; |
115 |
152 |
newPol = pol; |
116 |
|
}else{ |
117 |
968698 |
newHasPol = false; |
118 |
968698 |
newPol = false; |
119 |
|
} |
120 |
1508234 |
} |
121 |
|
|
122 |
4004591 |
void QuantPhaseReq::getEntailPolarity( |
123 |
|
Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol) |
124 |
|
{ |
125 |
4004591 |
if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ |
126 |
2002225 |
newHasPol = hasPol && pol!=( n.getKind()==OR ); |
127 |
2002225 |
newPol = pol; |
128 |
2002366 |
}else if( n.getKind()==IMPLIES ){ |
129 |
22940 |
newHasPol = hasPol && !pol; |
130 |
22940 |
newPol = child==0 ? !pol : pol; |
131 |
1979426 |
}else if( n.getKind()==NOT ){ |
132 |
252385 |
newHasPol = hasPol; |
133 |
252385 |
newPol = !pol; |
134 |
|
}else{ |
135 |
1727041 |
newHasPol = false; |
136 |
1727041 |
newPol = false; |
137 |
|
} |
138 |
4004591 |
} |
139 |
|
|
140 |
|
} // namespace theory |
141 |
29505 |
} // namespace cvc5 |