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-2019 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 #include "theory/quantifiers/inst_match.h"
17 #include "theory/quantifiers/term_database.h"
18 #include "theory/quantifiers/term_util.h"
19 #include "theory/quantifiers_engine.h"
20
21 using namespace std;
22 using namespace CVC4::kind;
23 using namespace CVC4::context;
24
25 namespace CVC4 {
26 namespace theory {
27
needsModel(Theory::Effort e)28 QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
29 {
30 return QEFFORT_NONE;
31 }
32
getEqualityEngine()33 eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
34 return d_quantEngine->getActiveEqualityEngine();
35 }
36
areEqual(TNode n1,TNode n2)37 bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
38 return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 );
39 }
40
areDisequal(TNode n1,TNode n2)41 bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
42 return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 );
43 }
44
getRepresentative(TNode n)45 TNode QuantifiersModule::getRepresentative( TNode n ) {
46 return d_quantEngine->getEqualityQuery()->getRepresentative( n );
47 }
48
getTermDatabase()49 quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
50 return d_quantEngine->getTermDatabase();
51 }
52
getTermUtil()53 quantifiers::TermUtil * QuantifiersModule::getTermUtil() {
54 return d_quantEngine->getTermUtil();
55 }
56
QuantPhaseReq(Node n,bool computeEq)57 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
58 initialize( n, computeEq );
59 }
60
initialize(Node n,bool computeEq)61 void QuantPhaseReq::initialize( Node n, bool computeEq ){
62 std::map< Node, int > phaseReqs2;
63 computePhaseReqs( n, false, phaseReqs2 );
64 for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
65 if( it->second==1 ){
66 d_phase_reqs[ it->first ] = true;
67 }else if( it->second==-1 ){
68 d_phase_reqs[ it->first ] = false;
69 }
70 }
71 Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;
72 //now, compute if any patterns are equality required
73 if( computeEq ){
74 for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
75 Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl;
76 if( it->first.getKind()==EQUAL ){
77 if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){
78 if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
79 d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
80 d_phase_reqs_equality[ it->first[0] ] = it->second;
81 Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
82 }
83 }else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){
84 d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
85 d_phase_reqs_equality[ it->first[1] ] = it->second;
86 Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
87 }
88 }
89 }
90 }
91 }
92
computePhaseReqs(Node n,bool polarity,std::map<Node,int> & phaseReqs)93 void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
94 bool newReqPol = false;
95 bool newPolarity;
96 if( n.getKind()==NOT ){
97 newReqPol = true;
98 newPolarity = !polarity;
99 }else if( n.getKind()==OR || n.getKind()==IMPLIES ){
100 if( !polarity ){
101 newReqPol = true;
102 newPolarity = false;
103 }
104 }else if( n.getKind()==AND ){
105 if( polarity ){
106 newReqPol = true;
107 newPolarity = true;
108 }
109 }else{
110 int val = polarity ? 1 : -1;
111 if( phaseReqs.find( n )==phaseReqs.end() ){
112 phaseReqs[n] = val;
113 }else if( val!=phaseReqs[n] ){
114 phaseReqs[n] = 0;
115 }
116 }
117 if( newReqPol ){
118 for( int i=0; i<(int)n.getNumChildren(); i++ ){
119 if( n.getKind()==IMPLIES && i==0 ){
120 computePhaseReqs( n[i], !newPolarity, phaseReqs );
121 }else{
122 computePhaseReqs( n[i], newPolarity, phaseReqs );
123 }
124 }
125 }
126 }
127
getPolarity(Node n,int child,bool hasPol,bool pol,bool & newHasPol,bool & newPol)128 void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
129 if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){
130 newHasPol = hasPol;
131 newPol = pol;
132 }else if( n.getKind()==IMPLIES ){
133 newHasPol = hasPol;
134 newPol = child==0 ? !pol : pol;
135 }else if( n.getKind()==NOT ){
136 newHasPol = hasPol;
137 newPol = !pol;
138 }else if( n.getKind()==ITE ){
139 newHasPol = (child!=0) && hasPol;
140 newPol = pol;
141 }else if( n.getKind()==FORALL ){
142 newHasPol = (child==1) && hasPol;
143 newPol = pol;
144 }else{
145 newHasPol = false;
146 newPol = pol;
147 }
148 }
149
getEntailPolarity(Node n,int child,bool hasPol,bool pol,bool & newHasPol,bool & newPol)150 void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
151 if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){
152 newHasPol = hasPol && pol!=( n.getKind()==OR );
153 newPol = pol;
154 }else if( n.getKind()==IMPLIES ){
155 newHasPol = hasPol && !pol;
156 newPol = child==0 ? !pol : pol;
157 }else if( n.getKind()==NOT ){
158 newHasPol = hasPol;
159 newPol = !pol;
160 }else{
161 newHasPol = false;
162 newPol = pol;
163 }
164 }
165
166 } /* namespace CVC4::theory */
167 } /* namespace CVC4 */
168