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