1 /********************* */
2 /*! \file rewrite_engine.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, 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 Rewrite engine module
13 **
14 ** This class manages rewrite rules for quantifiers
15 **/
16
17 #include "theory/quantifiers/rewrite_engine.h"
18
19 #include "options/quantifiers_options.h"
20 #include "theory/quantifiers/first_order_model.h"
21 #include "theory/quantifiers/ematching/inst_match_generator.h"
22 #include "theory/quantifiers/instantiate.h"
23 #include "theory/quantifiers/fmf/model_engine.h"
24 #include "theory/quantifiers/quant_conflict_find.h"
25 #include "theory/quantifiers/quant_util.h"
26 #include "theory/quantifiers/quantifiers_attributes.h"
27 #include "theory/quantifiers/term_database.h"
28 #include "theory/quantifiers/term_util.h"
29 #include "theory/theory_engine.h"
30
31 using namespace CVC4;
32 using namespace std;
33 using namespace CVC4::theory;
34 using namespace CVC4::theory::quantifiers;
35 using namespace CVC4::kind;
36
37 struct PrioritySort {
38 std::vector< double > d_priority;
operator ()PrioritySort39 bool operator() (int i,int j) {
40 return d_priority[i] < d_priority[j];
41 }
42 };
43
44
RewriteEngine(context::Context * c,QuantifiersEngine * qe)45 RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
46 d_needsSort = false;
47 }
48
getPriority(Node f)49 double RewriteEngine::getPriority( Node f ) {
50 Node rr = QuantAttributes::getRewriteRule( f );
51 Node rrr = rr[2];
52 Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;
53 bool deterministic = rrr[1].getKind()!=OR;
54
55 if( rrr.getKind()==RR_REWRITE ){
56 return deterministic ? 0.0 : 3.0;
57 }else if( rrr.getKind()==RR_DEDUCTION ){
58 return deterministic ? 1.0 : 4.0;
59 }else if( rrr.getKind()==RR_REDUCTION ){
60 return deterministic ? 2.0 : 5.0;
61 }else{
62 return 6.0;
63 }
64
65 //return deterministic ? 0.0 : 1.0;
66 }
67
needsCheck(Theory::Effort e)68 bool RewriteEngine::needsCheck( Theory::Effort e ){
69 return e==Theory::EFFORT_FULL;
70 //return e>=Theory::EFFORT_LAST_CALL;
71 }
72
check(Theory::Effort e,QEffort quant_e)73 void RewriteEngine::check(Theory::Effort e, QEffort quant_e)
74 {
75 if (quant_e == QEFFORT_STANDARD)
76 {
77 Assert( !d_quantEngine->inConflict() );
78 Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl;
79 //if( e==Theory::EFFORT_LAST_CALL ){
80 // if( !d_quantEngine->getModel()->isModelSet() ){
81 // d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );
82 // }
83 //}
84 if( d_needsSort ){
85 d_priority_order.clear();
86 PrioritySort ps;
87 std::vector< int > indicies;
88 for( int i=0; i<(int)d_rr_quant.size(); i++ ){
89 ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );
90 indicies.push_back( i );
91 }
92 std::sort( indicies.begin(), indicies.end(), ps );
93 for( unsigned i=0; i<indicies.size(); i++ ){
94 d_priority_order.push_back( d_rr_quant[indicies[i]] );
95 }
96 d_needsSort = false;
97 }
98
99 //apply rewrite rules
100 int addedLemmas = 0;
101 //per priority level
102 int index = 0;
103 bool success = true;
104 while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) {
105 addedLemmas += checkRewriteRule( d_priority_order[index], e );
106 index++;
107 if( index<(int)d_priority_order.size() ){
108 success = addedLemmas==0 || getPriority( d_priority_order[index] )==getPriority( d_priority_order[index-1] );
109 }
110 }
111
112 Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl;
113 }
114 }
115
checkRewriteRule(Node f,Theory::Effort e)116 int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
117 int addedLemmas = 0;
118 Trace("rewrite-engine-inst") << "Check " << d_qinfo_n[f] << ", priority = " << getPriority( f ) << ", effort = " << e << "..." << std::endl;
119 QuantConflictFind * qcf = d_quantEngine->getConflictFind();
120 if( qcf ){
121 //reset QCF module
122 qcf->computeRelevantEqr();
123 qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT);
124 //get the proper quantifiers info
125 std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f );
126 if( it!=d_qinfo.end() ){
127 QuantInfo * qi = &it->second;
128 if( qi->matchGeneratorIsValid() ){
129 Node rr = QuantAttributes::getRewriteRule( f );
130 Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl;
131 qi->reset_round( qcf );
132 Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl;
133 while( !d_quantEngine->inConflict() && qi->getNextMatch( qcf ) &&
134 ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
135 Trace("rewrite-engine-inst-debug") << " Got match to complete..." << std::endl;
136 qi->debugPrintMatch( "rewrite-engine-inst-debug" );
137 std::vector< int > assigned;
138 if( !qi->isMatchSpurious( qcf ) ){
139 bool doContinue = false;
140 bool success = true;
141 int tempAddedLemmas = 0;
142 while( !d_quantEngine->inConflict() && tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
143 success = qi->completeMatch( qcf, assigned, doContinue );
144 doContinue = true;
145 if( success ){
146 Trace("rewrite-engine-inst-debug") << " Construct match..." << std::endl;
147 std::vector< Node > inst;
148 qi->getMatch( inst );
149 Trace("rewrite-engine-inst-debug") << " Add instantiation..." << std::endl;
150 for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
151 Trace("rewrite-engine-inst-debug") << " " << f[0][i] << " -> ";
152 if( i<inst.size() ){
153 Trace("rewrite-engine-inst-debug") << inst[i] << std::endl;
154 }else{
155 Trace("rewrite-engine-inst-debug") << "OUT_OF_RANGE" << std::endl;
156 Assert( false );
157 }
158 }
159 //resize to remove auxiliary variables
160 if( inst.size()>f[0].getNumChildren() ){
161 inst.resize( f[0].getNumChildren() );
162 }
163 if (d_quantEngine->getInstantiate()->addInstantiation(f, inst))
164 {
165 addedLemmas++;
166 tempAddedLemmas++;
167 /*
168 //remove rewritten terms from consideration
169 std::vector< Node > to_remove;
170 switch( rr[2].getKind() ){
171 case kind::RR_REWRITE:
172 to_remove.push_back( rr[2][0] );
173 break;
174 case kind::RR_REDUCTION:
175 for( unsigned i=0; i<rr[2][0].getNumChildren(); i++ ){
176 to_remove.push_back( rr[2][0][i] );
177 }
178 break;
179 default:
180 break;
181 }
182 for( unsigned j=0; j<to_remove.size(); j++ ){
183 Node ns = d_quantEngine->getSubstitute( to_remove[j], inst );
184 Trace("rewrite-engine-inst-debug") << "Will remove : " << ns << std::endl;
185 d_quantEngine->getTermDatabase()->setTermInactive( ns );
186 }
187 */
188 }else{
189 Trace("rewrite-engine-inst-debug") << " - failed." << std::endl;
190 }
191 Trace("rewrite-engine-inst-debug") << " Get next completion..." << std::endl;
192 }
193 }
194 //Trace("rewrite-engine-inst-debug") << " Reverted assigned variables : ";
195 //for( unsigned a=0; a<assigned.size(); a++ ) {
196 // Trace("rewrite-engine-inst-debug") << assigned[a] << " ";
197 //}
198 //Trace("rewrite-engine-inst-debug") << std::endl;
199 //qi->revertMatch( assigned );
200 //Assert( assigned.empty() );
201 Trace("rewrite-engine-inst-debug") << " - failed to complete." << std::endl;
202 }else{
203 Trace("rewrite-engine-inst-debug") << " - match is spurious." << std::endl;
204 }
205 Trace("rewrite-engine-inst-debug") << " Get next match..." << std::endl;
206 }
207 }else{
208 Trace("rewrite-engine-inst-debug") << "...Invalid qinfo." << std::endl;
209 }
210 }else{
211 Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl;
212 }
213 }
214 d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas;
215 Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl;
216 return addedLemmas;
217 }
218
registerQuantifier(Node f)219 void RewriteEngine::registerQuantifier( Node f ) {
220 Node rr = QuantAttributes::getRewriteRule( f );
221 if( !rr.isNull() ){
222 Trace("rr-register") << "Register quantifier " << f << std::endl;
223 Trace("rr-register") << " rewrite rule is : " << rr << std::endl;
224 d_rr_quant.push_back( f );
225 d_rr[f] = rr;
226 d_needsSort = true;
227 Trace("rr-register") << " guard is : " << d_rr[f][1] << std::endl;
228
229 QuantConflictFind * qcf = d_quantEngine->getConflictFind();
230 if( qcf ){
231 std::vector< Node > qcfn_c;
232
233 std::vector< Node > bvl;
234 for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
235 bvl.push_back( f[0][i] );
236 }
237
238 std::vector< Node > cc;
239 //add patterns
240 for( unsigned i=1; i<f[2].getNumChildren(); i++ ){
241 std::vector< Node > nc;
242 for( unsigned j=0; j<f[2][i].getNumChildren(); j++ ){
243 Node nn;
244 Node nbv = NodeManager::currentNM()->mkBoundVar( f[2][i][j].getType() );
245 if( f[2][i][j].getType().isBoolean() && f[2][i][j].getKind()!=APPLY_UF ){
246 nn = f[2][i][j].negate();
247 }else{
248 nn = f[2][i][j].eqNode( nbv ).negate();
249 bvl.push_back( nbv );
250 }
251 nc.push_back( nn );
252 }
253 if( !nc.empty() ){
254 Node n = nc.size()==1 ? nc[0] : NodeManager::currentNM()->mkNode( AND, nc );
255 Trace("rr-register-debug") << " pattern is " << n << std::endl;
256 if( std::find( cc.begin(), cc.end(), n )==cc.end() ){
257 cc.push_back( n );
258 }
259 }
260 }
261 qcfn_c.push_back( NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvl ) );
262
263 std::vector< Node > body_c;
264 //add the guards
265 if( d_rr[f][1].getKind()==AND ){
266 for( unsigned j=0; j<d_rr[f][1].getNumChildren(); j++ ){
267 if( MatchGen::isHandled( d_rr[f][1][j] ) ){
268 body_c.push_back( d_rr[f][1][j].negate() );
269 }
270 }
271 }else if( d_rr[f][1]!=d_quantEngine->getTermUtil()->d_true ){
272 if( MatchGen::isHandled( d_rr[f][1] ) ){
273 body_c.push_back( d_rr[f][1].negate() );
274 }
275 }
276 //add the patterns to the body
277 body_c.push_back( cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( AND, cc ) );
278 //make the body
279 qcfn_c.push_back( body_c.size()==1 ? body_c[0] : NodeManager::currentNM()->mkNode( OR, body_c ) );
280 //make the quantified formula
281 d_qinfo_n[f] = NodeManager::currentNM()->mkNode( FORALL, qcfn_c );
282 Trace("rr-register") << " qcf formula is : " << d_qinfo_n[f] << std::endl;
283 d_qinfo[f].initialize( qcf, d_qinfo_n[f], d_qinfo_n[f][1] );
284 }
285 }
286 }
287
assertNode(Node n)288 void RewriteEngine::assertNode( Node n ) {
289
290 }
291
checkCompleteFor(Node q)292 bool RewriteEngine::checkCompleteFor( Node q ) {
293 // by semantics of rewrite rules, saturation -> SAT
294 return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end();
295 }
296
getInstConstNode(Node n,Node q)297 Node RewriteEngine::getInstConstNode( Node n, Node q ) {
298 std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
299 if( it==d_inst_const_node[q].end() ){
300 Node nn =
301 d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
302 n, q);
303 d_inst_const_node[q][n] = nn;
304 return nn;
305 }else{
306 return it->second;
307 }
308 }
309