1 /********************* */
2 /*! \file full_model_check.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Francois Bobot
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 full model check class
13 **/
14
15 #include "theory/quantifiers/fmf/full_model_check.h"
16 #include "options/quantifiers_options.h"
17 #include "options/theory_options.h"
18 #include "options/uf_options.h"
19 #include "theory/quantifiers/first_order_model.h"
20 #include "theory/quantifiers/instantiate.h"
21 #include "theory/quantifiers/term_database.h"
22 #include "theory/quantifiers/term_util.h"
23
24 using namespace std;
25 using namespace CVC4;
26 using namespace CVC4::kind;
27 using namespace CVC4::context;
28 using namespace CVC4::theory;
29 using namespace CVC4::theory::quantifiers;
30 using namespace CVC4::theory::inst;
31 using namespace CVC4::theory::quantifiers::fmcheck;
32
33 struct ModelBasisArgSort
34 {
35 std::vector< Node > d_terms;
36 // number of arguments that are model-basis terms
37 std::unordered_map<Node, unsigned, NodeHashFunction> d_mba_count;
operator ()ModelBasisArgSort38 bool operator() (int i,int j) {
39 return (d_mba_count[d_terms[i]] < d_mba_count[d_terms[j]]);
40 }
41 };
42
hasGeneralization(FirstOrderModelFmc * m,Node c,int index)43 bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
44 if (index==(int)c.getNumChildren()) {
45 return d_data!=-1;
46 }else{
47 TypeNode tn = c[index].getType();
48 Node st = m->getStar(tn);
49 if(d_child.find(st)!=d_child.end()) {
50 if( d_child[st].hasGeneralization(m, c, index+1) ){
51 return true;
52 }
53 }
54 if( c[index]!=st && d_child.find( c[index] )!=d_child.end() ){
55 if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){
56 return true;
57 }
58 }
59 if( c[index].getType().isSort() ){
60 //for star: check if all children are defined and have generalizations
61 if( c[index]==st ){ ///options::fmfFmcCoverSimplify()
62 //check if all children exist and are complete
63 unsigned num_child_def =
64 d_child.size() - (d_child.find(st) != d_child.end() ? 1 : 0);
65 if (num_child_def == m->getRepSet()->getNumRepresentatives(tn))
66 {
67 bool complete = true;
68 for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
69 if( !m->isStar(it->first) ){
70 if( !it->second.hasGeneralization(m, c, index+1) ){
71 complete = false;
72 break;
73 }
74 }
75 }
76 if( complete ){
77 return true;
78 }
79 }
80 }
81 }
82
83 return false;
84 }
85 }
86
getGeneralizationIndex(FirstOrderModelFmc * m,std::vector<Node> & inst,int index)87 int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {
88 Debug("fmc-entry-trie") << "Get generalization index " << inst.size() << " " << index << std::endl;
89 if (index==(int)inst.size()) {
90 return d_data;
91 }else{
92 int minIndex = -1;
93 Node st = m->getStar(inst[index].getType());
94 if (d_child.find(st) != d_child.end())
95 {
96 minIndex = d_child[st].getGeneralizationIndex(m, inst, index + 1);
97 }
98 Node cc = inst[index];
99 if (cc != st && d_child.find(cc) != d_child.end())
100 {
101 int gindex = d_child[cc].getGeneralizationIndex(m, inst, index + 1);
102 if (minIndex == -1 || (gindex != -1 && gindex < minIndex))
103 {
104 minIndex = gindex;
105 }
106 }
107 return minIndex;
108 }
109 }
110
addEntry(FirstOrderModelFmc * m,Node c,Node v,int data,int index)111 void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index ) {
112 if (index==(int)c.getNumChildren()) {
113 if(d_data==-1) {
114 d_data = data;
115 }
116 }
117 else {
118 d_child[ c[index] ].addEntry(m,c,v,data,index+1);
119 if( d_complete==0 ){
120 d_complete = -1;
121 }
122 }
123 }
124
getEntries(FirstOrderModelFmc * m,Node c,std::vector<int> & compat,std::vector<int> & gen,int index,bool is_gen)125 void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {
126 if (index==(int)c.getNumChildren()) {
127 if( d_data!=-1) {
128 if( is_gen ){
129 gen.push_back(d_data);
130 }
131 compat.push_back(d_data);
132 }
133 }else{
134 if (m->isStar(c[index])) {
135 for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
136 it->second.getEntries(m, c, compat, gen, index+1, is_gen );
137 }
138 }else{
139 Node st = m->getStar(c[index].getType());
140 if(d_child.find(st)!=d_child.end()) {
141 d_child[st].getEntries(m, c, compat, gen, index+1, false);
142 }
143 if( d_child.find( c[index] )!=d_child.end() ){
144 d_child[ c[index] ].getEntries(m, c, compat, gen, index+1, is_gen);
145 }
146 }
147
148 }
149 }
150
addEntry(FirstOrderModelFmc * m,Node c,Node v)151 bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {
152 if (d_et.hasGeneralization(m, c)) {
153 Trace("fmc-debug") << "Already has generalization, skip." << std::endl;
154 return false;
155 }
156 int newIndex = (int)d_cond.size();
157 if (!d_has_simplified) {
158 std::vector<int> compat;
159 std::vector<int> gen;
160 d_et.getEntries(m, c, compat, gen);
161 for( unsigned i=0; i<compat.size(); i++) {
162 if( d_status[compat[i]]==status_unk ){
163 if( d_value[compat[i]]!=v ){
164 d_status[compat[i]] = status_non_redundant;
165 }
166 }
167 }
168 for( unsigned i=0; i<gen.size(); i++) {
169 if( d_status[gen[i]]==status_unk ){
170 if( d_value[gen[i]]==v ){
171 d_status[gen[i]] = status_redundant;
172 }
173 }
174 }
175 d_status.push_back( status_unk );
176 }
177 d_et.addEntry(m, c, v, newIndex);
178 d_cond.push_back(c);
179 d_value.push_back(v);
180 return true;
181 }
182
evaluate(FirstOrderModelFmc * m,std::vector<Node> & inst)183 Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
184 int gindex = d_et.getGeneralizationIndex(m, inst);
185 if (gindex!=-1) {
186 return d_value[gindex];
187 }else{
188 Trace("fmc-warn") << "Warning : evaluation came up null!" << std::endl;
189 return Node::null();
190 }
191 }
192
getGeneralizationIndex(FirstOrderModelFmc * m,std::vector<Node> & inst)193 int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
194 return d_et.getGeneralizationIndex(m, inst);
195 }
196
basic_simplify(FirstOrderModelFmc * m)197 void Def::basic_simplify( FirstOrderModelFmc * m ) {
198 d_has_simplified = true;
199 std::vector< Node > cond;
200 cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
201 d_cond.clear();
202 std::vector< Node > value;
203 value.insert( value.end(), d_value.begin(), d_value.end() );
204 d_value.clear();
205 d_et.reset();
206 for (unsigned i=0; i<d_status.size(); i++) {
207 if( d_status[i]!=status_redundant ){
208 addEntry(m, cond[i], value[i]);
209 }
210 }
211 d_status.clear();
212 }
213
simplify(FullModelChecker * mc,FirstOrderModelFmc * m)214 void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
215 Trace("fmc-simplify") << "Simplify definition, #cond = " << d_cond.size() << std::endl;
216 basic_simplify( m );
217 Trace("fmc-simplify") << "post-basic simplify, #cond = " << d_cond.size() << std::endl;
218
219 //check if the last entry is not all star, if so, we can make the last entry all stars
220 if( !d_cond.empty() ){
221 bool last_all_stars = true;
222 Node cc = d_cond[d_cond.size()-1];
223 for( unsigned i=0; i<cc.getNumChildren(); i++ ){
224 if (!m->isStar(cc[i]))
225 {
226 last_all_stars = false;
227 break;
228 }
229 }
230 if( !last_all_stars ){
231 Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl;
232 Trace("fmc-cover-simplify") << "Before: " << std::endl;
233 debugPrint("fmc-cover-simplify",Node::null(), mc);
234 Trace("fmc-cover-simplify") << std::endl;
235 std::vector< Node > cond;
236 cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
237 d_cond.clear();
238 std::vector< Node > value;
239 value.insert( value.end(), d_value.begin(), d_value.end() );
240 d_value.clear();
241 d_et.reset();
242 d_has_simplified = false;
243 //change the last to all star
244 std::vector< Node > nc;
245 nc.push_back( cc.getOperator() );
246 for( unsigned j=0; j< cc.getNumChildren(); j++){
247 nc.push_back(m->getStar(cc[j].getType()));
248 }
249 cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc );
250 //re-add the entries
251 for (unsigned i=0; i<cond.size(); i++) {
252 addEntry(m, cond[i], value[i]);
253 }
254 Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;
255 basic_simplify( m );
256 Trace("fmc-cover-simplify") << "After: " << std::endl;
257 debugPrint("fmc-cover-simplify",Node::null(), mc);
258 Trace("fmc-cover-simplify") << std::endl;
259 }
260 }
261 Trace("fmc-simplify") << "finish simplify, #cond = " << d_cond.size() << std::endl;
262 }
263
debugPrint(const char * tr,Node op,FullModelChecker * m)264 void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
265 if (!op.isNull()) {
266 Trace(tr) << "Model for " << op << " : " << std::endl;
267 }
268 for( unsigned i=0; i<d_cond.size(); i++) {
269 //print the condition
270 if (!op.isNull()) {
271 Trace(tr) << op;
272 }
273 m->debugPrintCond(tr, d_cond[i], true);
274 Trace(tr) << " -> ";
275 m->debugPrint(tr, d_value[i]);
276 Trace(tr) << std::endl;
277 }
278 }
279
280
FullModelChecker(context::Context * c,QuantifiersEngine * qe)281 FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :
282 QModelBuilder( c, qe ){
283 d_true = NodeManager::currentNM()->mkConst(true);
284 d_false = NodeManager::currentNM()->mkConst(false);
285 }
286
preProcessBuildModel(TheoryModel * m)287 bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
288 //standard pre-process
289 if( !preProcessBuildModelStd( m ) ){
290 return false;
291 }
292
293 FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
294 Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
295 d_preinitialized_eqc.clear();
296 d_preinitialized_types.clear();
297 //traverse equality engine
298 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
299 while( !eqcs_i.isFinished() ){
300 Node r = *eqcs_i;
301 TypeNode tr = r.getType();
302 d_preinitialized_eqc[tr] = r;
303 ++eqcs_i;
304 }
305
306 //must ensure model basis terms exists in model for each relevant type
307 fm->initialize();
308 for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
309 Node op = it->first;
310 Trace("fmc") << "preInitialize types for " << op << std::endl;
311 TypeNode tno = op.getType();
312 for( unsigned i=0; i<tno.getNumChildren(); i++) {
313 Trace("fmc") << "preInitializeType " << tno[i] << std::endl;
314 preInitializeType( fm, tno[i] );
315 }
316 }
317 //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
318 if( !options::fmfEmptySorts() ){
319 for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
320 Node q = fm->getAssertedQuantifier( i );
321 //make sure all types are set
322 for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
323 preInitializeType( fm, q[0][j].getType() );
324 }
325 }
326 }
327 return true;
328 }
329
processBuildModel(TheoryModel * m)330 bool FullModelChecker::processBuildModel(TheoryModel* m){
331 if (!m->areFunctionValuesEnabled())
332 {
333 // nothing to do if no functions
334 return true;
335 }
336 FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
337 Trace("fmc") << "---Full Model Check reset() " << std::endl;
338 d_quant_models.clear();
339 d_rep_ids.clear();
340 d_star_insts.clear();
341 //process representatives
342 RepSet* rs = fm->getRepSetPtr();
343 for (std::map<TypeNode, std::vector<Node> >::iterator it =
344 rs->d_type_reps.begin();
345 it != rs->d_type_reps.end();
346 ++it)
347 {
348 if( it->first.isSort() ){
349 Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
350 for( size_t a=0; a<it->second.size(); a++ ){
351 Node r = fm->getRepresentative( it->second[a] );
352 if( Trace.isOn("fmc-model-debug") ){
353 std::vector< Node > eqc;
354 d_qe->getEqualityQuery()->getEquivalenceClass( r, eqc );
355 Trace("fmc-model-debug") << " " << (it->second[a]==r);
356 Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
357 //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
358 Trace("fmc-model-debug") << " {";
359 for( size_t i=0; i<eqc.size(); i++ ){
360 Trace("fmc-model-debug") << eqc[i] << ", ";
361 }
362 Trace("fmc-model-debug") << "}" << std::endl;
363 }
364 d_rep_ids[it->first][r] = (int)a;
365 }
366 Trace("fmc-model-debug") << std::endl;
367 }
368 }
369
370 //now, make models
371 for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
372 Node op = it->first;
373 //reset the model
374 fm->d_models[op]->reset();
375
376 std::vector< Node > add_conds;
377 std::vector< Node > add_values;
378 bool needsDefault = true;
379 std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( op );
380 if( itut!=fm->d_uf_terms.end() ){
381 Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl;
382 for( size_t i=0; i<itut->second.size(); i++ ){
383 Node n = itut->second[i];
384 // only consider unique up to congruence (in model equality engine)?
385 add_conds.push_back( n );
386 add_values.push_back( n );
387 Node r = fm->getRepresentative(n);
388 Trace("fmc-model-debug") << n << " -> " << r << std::endl;
389 //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
390 }
391 }else{
392 Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl;
393 }
394 Trace("fmc-model-debug") << std::endl;
395 //possibly get default
396 if( needsDefault ){
397 Node nmb = fm->getModelBasisOpTerm(op);
398 //add default value if necessary
399 if( fm->hasTerm( nmb ) ){
400 Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
401 add_conds.push_back( nmb );
402 add_values.push_back( nmb );
403 }else{
404 Node vmb = getSomeDomainElement(fm, nmb.getType());
405 Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
406 Trace("fmc-model-debug")
407 << fm->getRepSet()->getNumRepresentatives(nmb.getType())
408 << std::endl;
409 add_conds.push_back( nmb );
410 add_values.push_back( vmb );
411 }
412 }
413
414 std::vector< Node > conds;
415 std::vector< Node > values;
416 std::vector< Node > entry_conds;
417 //get the entries for the model
418 for( size_t i=0; i<add_conds.size(); i++ ){
419 Node c = add_conds[i];
420 Node v = add_values[i];
421 Trace("fmc-model-debug")
422 << "Add cond/value : " << c << " -> " << v << std::endl;
423 std::vector< Node > children;
424 std::vector< Node > entry_children;
425 children.push_back(op);
426 entry_children.push_back(op);
427 bool hasNonStar = false;
428 for( unsigned i=0; i<c.getNumChildren(); i++) {
429 Node ri = fm->getRepresentative( c[i] );
430 children.push_back(ri);
431 bool isStar = false;
432 if (fm->isModelBasisTerm(ri))
433 {
434 ri = fm->getStar(ri.getType());
435 isStar = true;
436 }
437 else
438 {
439 hasNonStar = true;
440 }
441 if( !isStar && !ri.isConst() ){
442 Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
443 Assert( false );
444 }
445 entry_children.push_back(ri);
446 }
447 Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
448 Node nv = fm->getRepresentative( v );
449 Trace("fmc-model-debug")
450 << "Representative of " << v << " is " << nv << std::endl;
451 if( !nv.isConst() ){
452 Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
453 Assert( false );
454 }
455 Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
456 if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
457 Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
458 conds.push_back(n);
459 values.push_back(nv);
460 entry_conds.push_back(en);
461 }
462 else {
463 Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
464 }
465 }
466
467
468 //sort based on # default arguments
469 std::vector< int > indices;
470 ModelBasisArgSort mbas;
471 for (int i=0; i<(int)conds.size(); i++) {
472 mbas.d_terms.push_back(conds[i]);
473 mbas.d_mba_count[conds[i]] = fm->getModelBasisArg(conds[i]);
474 indices.push_back(i);
475 }
476 std::sort( indices.begin(), indices.end(), mbas );
477
478 for (int i=0; i<(int)indices.size(); i++) {
479 fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
480 }
481
482 Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
483 fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
484 Trace("fmc-model-simplify") << std::endl;
485
486 Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;
487 fm->d_models[op]->simplify( this, fm );
488
489 fm->d_models[op]->debugPrint("fmc-model", op, this);
490 Trace("fmc-model") << std::endl;
491
492 //for debugging
493 /*
494 for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
495 std::vector< Node > inst;
496 for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){
497 Node r = fm->getRepresentative( fm->d_uf_terms[op][i][j] );
498 inst.push_back( r );
499 }
500 Node ev = fm->d_models[op]->evaluate( fm, inst );
501 Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl;
502 AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
503 }
504 */
505 }
506 Assert( d_addedLemmas==0 );
507
508 //make function values
509 for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
510 Node f_def = getFunctionValue( fm, it->first, "$x" );
511 m->assignFunctionDefinition( it->first, f_def );
512 }
513 return TheoryEngineModelBuilder::processBuildModel( m );
514 }
515
preInitializeType(FirstOrderModelFmc * fm,TypeNode tn)516 void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
517 if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){
518 d_preinitialized_types[tn] = true;
519 if (!tn.isFunction() || options::ufHo())
520 {
521 Node mb = fm->getModelBasisTerm(tn);
522 // if the model basis term does not exist in the model,
523 // either add it directly to the model's equality engine if no other terms
524 // of this type exist, or otherwise assert that it is equal to the first
525 // equivalence class of its type.
526 if (!fm->hasTerm(mb) && !mb.isConst())
527 {
528 std::map<TypeNode, Node>::iterator itpe = d_preinitialized_eqc.find(tn);
529 if (itpe == d_preinitialized_eqc.end())
530 {
531 Trace("fmc") << "...add model basis term to EE of model " << mb << " "
532 << tn << std::endl;
533 fm->d_equalityEngine->addTerm(mb);
534 }
535 else
536 {
537 Trace("fmc") << "...add model basis eqc equality to model " << mb
538 << " == " << itpe->second << " " << tn << std::endl;
539 bool ret = fm->assertEquality(mb, itpe->second, true);
540 AlwaysAssert(ret);
541 }
542 }
543 }
544 }
545 }
546
debugPrintCond(const char * tr,Node n,bool dispStar)547 void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
548 Trace(tr) << "(";
549 for( unsigned j=0; j<n.getNumChildren(); j++) {
550 if( j>0 ) Trace(tr) << ", ";
551 debugPrint(tr, n[j], dispStar);
552 }
553 Trace(tr) << ")";
554 }
555
debugPrint(const char * tr,Node n,bool dispStar)556 void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
557 FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel();
558 if( n.isNull() ){
559 Trace(tr) << "null";
560 }
561 else if(fm->isStar(n) && dispStar) {
562 Trace(tr) << "*";
563 }
564 else
565 {
566 TypeNode tn = n.getType();
567 if( tn.isSort() && d_rep_ids.find(tn)!=d_rep_ids.end() ){
568 if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {
569 Trace(tr) << d_rep_ids[tn][n];
570 }else{
571 Trace(tr) << n;
572 }
573 }else{
574 Trace(tr) << n;
575 }
576 }
577 }
578
579
doExhaustiveInstantiation(FirstOrderModel * fm,Node f,int effort)580 int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
581 Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
582 Assert( !d_qe->inConflict() );
583 if( optUseModel() ){
584 FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();
585 if (effort==0) {
586 //register the quantifier
587 if (d_quant_cond.find(f)==d_quant_cond.end()) {
588 std::vector< TypeNode > types;
589 for(unsigned i=0; i<f[0].getNumChildren(); i++){
590 types.push_back(f[0][i].getType());
591 }
592 TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );
593 Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" );
594 d_quant_cond[f] = op;
595 }
596
597 if( options::mbqiMode()==MBQI_NONE ){
598 //just exhaustive instantiate
599 Node c = mkCondDefault( fmfmc, f );
600 d_quant_models[f].addEntry( fmfmc, c, d_false );
601 return exhaustiveInstantiate( fmfmc, f, c, -1);
602 }else{
603 //model check the quantifier
604 doCheck(fmfmc, f, d_quant_models[f], f[1]);
605 Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
606 Assert( !d_quant_models[f].d_cond.empty() );
607 d_quant_models[f].debugPrint("fmc", Node::null(), this);
608 Trace("fmc") << std::endl;
609
610 //consider all entries going to non-true
611 for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
612 if( d_quant_models[f].d_value[i]!=d_true ) {
613 Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
614 bool hasStar = false;
615 std::vector< Node > inst;
616 for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {
617 if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {
618 hasStar = true;
619 inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
620 }else{
621 inst.push_back(d_quant_models[f].d_cond[i][j]);
622 }
623 }
624 bool addInst = true;
625 if( hasStar ){
626 //try obvious (specified by inst)
627 Node ev = d_quant_models[f].evaluate(fmfmc, inst);
628 if (ev==d_true) {
629 addInst = false;
630 Trace("fmc-debug") << "...do not instantiate, evaluation was " << ev << std::endl;
631 }
632 }else{
633 //for debugging
634 if (Trace.isOn("fmc-test-inst")) {
635 Node ev = d_quant_models[f].evaluate(fmfmc, inst);
636 if( ev==d_true ){
637 Message() << "WARNING: instantiation was true! " << f << " "
638 << d_quant_models[f].d_cond[i] << std::endl;
639 AlwaysAssert(false);
640 }else{
641 Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;
642 }
643 }
644 }
645 if( addInst ){
646 if( options::fmfBound() ){
647 std::vector< Node > cond;
648 cond.push_back(d_quant_cond[f]);
649 cond.insert( cond.end(), inst.begin(), inst.end() );
650 //need to do exhaustive instantiate algorithm to set things properly (should only add one instance)
651 Node c = mkCond( cond );
652 unsigned prevInst = d_addedLemmas;
653 exhaustiveInstantiate( fmfmc, f, c, -1 );
654 if( d_addedLemmas==prevInst ){
655 d_star_insts[f].push_back(i);
656 }
657 }else{
658 //just add the instance
659 d_triedLemmas++;
660 if (d_qe->getInstantiate()->addInstantiation(f, inst, true))
661 {
662 Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
663 d_addedLemmas++;
664 if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
665 break;
666 }
667 }else{
668 Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
669 //this can happen if evaluation is unknown, or if we are generalizing a star that already has a value
670 //if( !hasStar && d_quant_models[f].d_value[i]==d_false ){
671 // Trace("fmc-warn") << "**** FMC warning: inconsistent duplicate instantiation." << std::endl;
672 //}
673 //this assertion can happen if two instantiations from this round are identical
674 // (0,1)->false (1,0)->false for forall xy. f( x, y ) = f( y, x )
675 //Assert( hasStar || d_quant_models[f].d_value[i]!=d_false );
676 //might try it next effort level
677 d_star_insts[f].push_back(i);
678 }
679 }
680 }else{
681 Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl;
682 //might try it next effort level
683 d_star_insts[f].push_back(i);
684 }
685 }
686 }
687 }
688 }else{
689 if (!d_star_insts[f].empty()) {
690 Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;
691 Trace("fmc-exh") << "Definition was : " << std::endl;
692 d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);
693 Trace("fmc-exh") << std::endl;
694 Def temp;
695 //simplify the exceptions?
696 for( int i=(d_star_insts[f].size()-1); i>=0; i--) {
697 //get witness for d_star_insts[f][i]
698 int j = d_star_insts[f][i];
699 if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
700 if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){
701 //something went wrong, resort to exhaustive instantiation
702 return 0;
703 }
704 }
705 }
706 }
707 }
708 return 1;
709 }else{
710 return 0;
711 }
712 }
713
714 /** Representative bound fmc entry
715 *
716 * This bound information corresponds to one
717 * entry in a term definition (see terminology in
718 * Chapter 5 of Finite Model Finding for
719 * Satisfiability Modulo Theories thesis).
720 * For example, a term definition for the body
721 * of a quantified formula:
722 * forall xyz. P( x, y, z )
723 * may be:
724 * ( 0, 0, 0 ) -> false
725 * ( *, 1, 2 ) -> false
726 * ( *, *, * ) -> true
727 * Indicating that the quantified formula evaluates
728 * to false in the current model for x=0, y=0, z=0,
729 * or y=1, z=2 for any x, and evaluates to true
730 * otherwise.
731 * This class is used if we wish
732 * to iterate over all values corresponding to one
733 * of these entries. For example, for the second entry:
734 * (*, 1, 2 )
735 * we iterate over all values of x, but only {1}
736 * for y and {2} for z.
737 */
738 class RepBoundFmcEntry : public QRepBoundExt
739 {
740 public:
RepBoundFmcEntry(QuantifiersEngine * qe,Node e,FirstOrderModelFmc * f)741 RepBoundFmcEntry(QuantifiersEngine* qe, Node e, FirstOrderModelFmc* f)
742 : QRepBoundExt(qe), d_entry(e), d_fm(f)
743 {
744 }
~RepBoundFmcEntry()745 ~RepBoundFmcEntry() {}
746 /** set bound */
setBound(Node owner,unsigned i,std::vector<Node> & elements)747 virtual RepSetIterator::RsiEnumType setBound(
748 Node owner, unsigned i, std::vector<Node>& elements) override
749 {
750 if (!d_fm->isStar(d_entry[i]))
751 {
752 // only need to consider the single point
753 elements.push_back(d_entry[i]);
754 return RepSetIterator::ENUM_DEFAULT;
755 }
756 return QRepBoundExt::setBound(owner, i, elements);
757 }
758
759 private:
760 /** the entry for this bound */
761 Node d_entry;
762 /** the model builder associated with this bound */
763 FirstOrderModelFmc* d_fm;
764 };
765
exhaustiveInstantiate(FirstOrderModelFmc * fm,Node f,Node c,int c_index)766 bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
767 Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " ";
768 debugPrintCond("fmc-exh", c, true);
769 Trace("fmc-exh")<< std::endl;
770 RepBoundFmcEntry rbfe(d_qe, c, fm);
771 RepSetIterator riter(d_qe->getModel()->getRepSet(), &rbfe);
772 Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;
773 //initialize
774 if (riter.setQuantifier(f))
775 {
776 Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
777 int addedLemmas = 0;
778 //now do full iteration
779 while( !riter.isFinished() ){
780 d_triedLemmas++;
781 Trace("fmc-exh-debug") << "Inst : ";
782 std::vector< Node > ev_inst;
783 std::vector< Node > inst;
784 for (unsigned i = 0; i < riter.getNumTerms(); i++)
785 {
786 Node rr = riter.getCurrentTerm( i );
787 Node r = rr;
788 //if( r.getType().isSort() ){
789 r = fm->getRepresentative( r );
790 //}else{
791 // r = fm->getCurrentModelValue( r );
792 //}
793 debugPrint("fmc-exh-debug", r);
794 Trace("fmc-exh-debug") << " (term : " << rr << ")";
795 ev_inst.push_back( r );
796 inst.push_back( rr );
797 }
798 int ev_index = d_quant_models[f].getGeneralizationIndex(fm, ev_inst);
799 Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();
800 Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
801 if (ev!=d_true) {
802 Trace("fmc-exh-debug") << ", add!";
803 //add as instantiation
804 if (d_qe->getInstantiate()->addInstantiation(f, inst, true))
805 {
806 Trace("fmc-exh-debug") << " ...success.";
807 addedLemmas++;
808 if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
809 break;
810 }
811 }else{
812 Trace("fmc-exh-debug") << ", failed.";
813 }
814 }else{
815 Trace("fmc-exh-debug") << ", already true";
816 }
817 Trace("fmc-exh-debug") << std::endl;
818 int index = riter.increment();
819 Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
820 if( !riter.isFinished() ){
821 if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_BOUND_INT ) {
822 Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
823 riter.incrementAtIndex(index - 1);
824 }
825 }
826 }
827 d_addedLemmas += addedLemmas;
828 Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.isIncomplete() << std::endl;
829 return addedLemmas>0 || !riter.isIncomplete();
830 }else{
831 Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
832 return !riter.isIncomplete();
833 }
834 }
835
doCheck(FirstOrderModelFmc * fm,Node f,Def & d,Node n)836 void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {
837 Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
838 //first check if it is a bounding literal
839 if( n.hasAttribute(BoundIntLitAttribute()) ){
840 Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;
841 d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );
842 }else if( n.getKind() == kind::BOUND_VARIABLE ){
843 Trace("fmc-debug") << "Add default entry..." << std::endl;
844 d.addEntry(fm, mkCondDefault(fm, f), n);
845 }
846 else if( n.getKind() == kind::NOT ){
847 //just do directly
848 doCheck( fm, f, d, n[0] );
849 doNegate( d );
850 }
851 else if( n.getKind() == kind::FORALL ){
852 d.addEntry(fm, mkCondDefault(fm, f), Node::null());
853 }
854 else if( n.getType().isArray() ){
855 //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
856 //Trace("fmc-warn") << " Default value was : " << odefaultValue << std::endl;
857 //Trace("fmc-debug") << "Can't process base array " << r << std::endl;
858 //can't process this array
859 d.reset();
860 d.addEntry(fm, mkCondDefault(fm, f), Node::null());
861 }
862 else if( n.getNumChildren()==0 ){
863 Node r = n;
864 if( !n.isConst() ){
865 if( !fm->hasTerm(n) ){
866 r = getSomeDomainElement(fm, n.getType() );
867 }
868 r = fm->getRepresentative( r );
869 }
870 Trace("fmc-debug") << "Add constant entry..." << std::endl;
871 d.addEntry(fm, mkCondDefault(fm, f), r);
872 }
873 else{
874 std::vector< int > var_ch;
875 std::vector< Def > children;
876 for( int i=0; i<(int)n.getNumChildren(); i++) {
877 Def dc;
878 doCheck(fm, f, dc, n[i]);
879 children.push_back(dc);
880 if( n[i].getKind() == kind::BOUND_VARIABLE ){
881 var_ch.push_back(i);
882 }
883 }
884
885 if( n.getKind()==APPLY_UF ){
886 Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;
887 //uninterpreted compose
888 doUninterpretedCompose( fm, f, d, n.getOperator(), children );
889 /*
890 } else if( n.getKind()==SELECT ){
891 Trace("fmc-debug") << "Do select compose " << n << std::endl;
892 std::vector< Def > children2;
893 children2.push_back( children[1] );
894 std::vector< Node > cond;
895 mkCondDefaultVec(fm, f, cond);
896 std::vector< Node > val;
897 doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val );
898 */
899 } else {
900 if( !var_ch.empty() ){
901 if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
902 if( var_ch.size()==2 ){
903 Trace("fmc-debug") << "Do variable equality " << n << std::endl;
904 doVariableEquality( fm, f, d, n );
905 }else{
906 Trace("fmc-debug") << "Do variable relation " << n << std::endl;
907 doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] );
908 }
909 }else{
910 Trace("fmc-warn") << "Don't know how to check " << n << std::endl;
911 d.addEntry(fm, mkCondDefault(fm, f), Node::null());
912 }
913 }else{
914 Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;
915 std::vector< Node > cond;
916 mkCondDefaultVec(fm, f, cond);
917 std::vector< Node > val;
918 //interpreted compose
919 doInterpretedCompose( fm, f, d, n, children, 0, cond, val );
920 }
921 }
922 Trace("fmc-debug") << "Simplify the definition..." << std::endl;
923 d.debugPrint("fmc-debug", Node::null(), this);
924 d.simplify(this, fm);
925 Trace("fmc-debug") << "Done simplifying" << std::endl;
926 }
927 Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;
928 d.debugPrint("fmc-debug", Node::null(), this);
929 Trace("fmc-debug") << std::endl;
930 }
931
doNegate(Def & dc)932 void FullModelChecker::doNegate( Def & dc ) {
933 for (unsigned i=0; i<dc.d_cond.size(); i++) {
934 if (!dc.d_value[i].isNull()) {
935 dc.d_value[i] = dc.d_value[i]==d_true ? d_false : ( dc.d_value[i]==d_false ? d_true : dc.d_value[i] );
936 }
937 }
938 }
939
doVariableEquality(FirstOrderModelFmc * fm,Node f,Def & d,Node eq)940 void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) {
941 std::vector<Node> cond;
942 mkCondDefaultVec(fm, f, cond);
943 if (eq[0]==eq[1]){
944 d.addEntry(fm, mkCond(cond), d_true);
945 }else{
946 TypeNode tn = eq[0].getType();
947 if( tn.isSort() ){
948 int j = fm->getVariableId(f, eq[0]);
949 int k = fm->getVariableId(f, eq[1]);
950 const RepSet* rs = fm->getRepSet();
951 if (!rs->hasType(tn))
952 {
953 getSomeDomainElement( fm, tn ); //to verify the type is initialized
954 }
955 unsigned nreps = rs->getNumRepresentatives(tn);
956 for (unsigned i = 0; i < nreps; i++)
957 {
958 Node r = fm->getRepresentative(rs->getRepresentative(tn, i));
959 cond[j+1] = r;
960 cond[k+1] = r;
961 d.addEntry( fm, mkCond(cond), d_true);
962 }
963 d.addEntry( fm, mkCondDefault(fm, f), d_false);
964 }else{
965 d.addEntry( fm, mkCondDefault(fm, f), Node::null());
966 }
967 }
968 }
969
doVariableRelation(FirstOrderModelFmc * fm,Node f,Def & d,Def & dc,Node v)970 void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) {
971 int j = fm->getVariableId(f, v);
972 for (unsigned i=0; i<dc.d_cond.size(); i++) {
973 Node val = dc.d_value[i];
974 if( val.isNull() ){
975 d.addEntry( fm, dc.d_cond[i], val);
976 }else{
977 if( dc.d_cond[i][j]!=val ){
978 if (fm->isStar(dc.d_cond[i][j])) {
979 std::vector<Node> cond;
980 mkCondVec(dc.d_cond[i],cond);
981 cond[j+1] = val;
982 d.addEntry(fm, mkCond(cond), d_true);
983 cond[j+1] = fm->getStar(val.getType());
984 d.addEntry(fm, mkCond(cond), d_false);
985 }else{
986 d.addEntry( fm, dc.d_cond[i], d_false);
987 }
988 }else{
989 d.addEntry( fm, dc.d_cond[i], d_true);
990 }
991 }
992 }
993 }
994
doUninterpretedCompose(FirstOrderModelFmc * fm,Node f,Def & d,Node op,std::vector<Def> & dc)995 void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
996 Trace("fmc-uf-debug") << "Definition : " << std::endl;
997 fm->d_models[op]->debugPrint("fmc-uf-debug", op, this);
998 Trace("fmc-uf-debug") << std::endl;
999
1000 std::vector< Node > cond;
1001 mkCondDefaultVec(fm, f, cond);
1002 std::vector< Node > val;
1003 doUninterpretedCompose( fm, f, d, *fm->d_models[op], dc, 0, cond, val);
1004 }
1005
doUninterpretedCompose(FirstOrderModelFmc * fm,Node f,Def & d,Def & df,std::vector<Def> & dc,int index,std::vector<Node> & cond,std::vector<Node> & val)1006 void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,
1007 Def & df, std::vector< Def > & dc, int index,
1008 std::vector< Node > & cond, std::vector<Node> & val ) {
1009 Trace("fmc-uf-process") << "process at " << index << std::endl;
1010 for( unsigned i=1; i<cond.size(); i++) {
1011 debugPrint("fmc-uf-process", cond[i], true);
1012 Trace("fmc-uf-process") << " ";
1013 }
1014 Trace("fmc-uf-process") << std::endl;
1015 if (index==(int)dc.size()) {
1016 //we have an entry, now do actual compose
1017 std::map< int, Node > entries;
1018 doUninterpretedCompose2( fm, f, entries, 0, cond, val, df.d_et);
1019 if( entries.empty() ){
1020 d.addEntry(fm, mkCond(cond), Node::null());
1021 }else{
1022 //add them to the definition
1023 for( unsigned e=0; e<df.d_cond.size(); e++ ){
1024 if ( entries.find(e)!=entries.end() ){
1025 Trace("fmf-uf-process-debug") << "Add entry..." << std::endl;
1026 d.addEntry(fm, entries[e], df.d_value[e] );
1027 Trace("fmf-uf-process-debug") << "Done add entry." << std::endl;
1028 }
1029 }
1030 }
1031 }else{
1032 for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
1033 if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {
1034 std::vector< Node > new_cond;
1035 new_cond.insert(new_cond.end(), cond.begin(), cond.end());
1036 if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){
1037 Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;
1038 val.push_back(dc[index].d_value[i]);
1039 doUninterpretedCompose(fm, f, d, df, dc, index+1, new_cond, val);
1040 val.pop_back();
1041 }else{
1042 Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;
1043 }
1044 }
1045 }
1046 }
1047 }
1048
doUninterpretedCompose2(FirstOrderModelFmc * fm,Node f,std::map<int,Node> & entries,int index,std::vector<Node> & cond,std::vector<Node> & val,EntryTrie & curr)1049 void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
1050 std::map< int, Node > & entries, int index,
1051 std::vector< Node > & cond, std::vector< Node > & val,
1052 EntryTrie & curr ) {
1053 Trace("fmc-uf-process") << "compose " << index << " / " << val.size() << std::endl;
1054 for( unsigned i=1; i<cond.size(); i++) {
1055 debugPrint("fmc-uf-process", cond[i], true);
1056 Trace("fmc-uf-process") << " ";
1057 }
1058 Trace("fmc-uf-process") << std::endl;
1059 if (index==(int)val.size()) {
1060 Node c = mkCond(cond);
1061 Trace("fmc-uf-entry") << "Entry : " << c << " -> index[" << curr.d_data << "]" << std::endl;
1062 entries[curr.d_data] = c;
1063 }else{
1064 Node v = val[index];
1065 Trace("fmc-uf-process") << "Process " << v << std::endl;
1066 bool bind_var = false;
1067 if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
1068 int j = fm->getVariableId(f, v);
1069 Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
1070 if (!fm->isStar(cond[j + 1]))
1071 {
1072 v = cond[j+1];
1073 }else{
1074 bind_var = true;
1075 }
1076 }
1077 if (bind_var) {
1078 Trace("fmc-uf-process") << "bind variable..." << std::endl;
1079 int j = fm->getVariableId(f, v);
1080 Assert(fm->isStar(cond[j + 1]));
1081 for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin();
1082 it != curr.d_child.end();
1083 ++it)
1084 {
1085 cond[j + 1] = it->first;
1086 doUninterpretedCompose2(
1087 fm, f, entries, index + 1, cond, val, it->second);
1088 }
1089 cond[j + 1] = fm->getStar(v.getType());
1090 }else{
1091 if( !v.isNull() ){
1092 if (curr.d_child.find(v) != curr.d_child.end())
1093 {
1094 Trace("fmc-uf-process") << "follow value..." << std::endl;
1095 doUninterpretedCompose2(
1096 fm, f, entries, index + 1, cond, val, curr.d_child[v]);
1097 }
1098 Node st = fm->getStar(v.getType());
1099 if (curr.d_child.find(st) != curr.d_child.end())
1100 {
1101 Trace("fmc-uf-process") << "follow star..." << std::endl;
1102 doUninterpretedCompose2(
1103 fm, f, entries, index + 1, cond, val, curr.d_child[st]);
1104 }
1105 }
1106 }
1107 }
1108 }
1109
doInterpretedCompose(FirstOrderModelFmc * fm,Node f,Def & d,Node n,std::vector<Def> & dc,int index,std::vector<Node> & cond,std::vector<Node> & val)1110 void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
1111 std::vector< Def > & dc, int index,
1112 std::vector< Node > & cond, std::vector<Node> & val ) {
1113 Trace("fmc-if-process") << "int compose " << index << " / " << dc.size() << std::endl;
1114 for( unsigned i=1; i<cond.size(); i++) {
1115 debugPrint("fmc-if-process", cond[i], true);
1116 Trace("fmc-if-process") << " ";
1117 }
1118 Trace("fmc-if-process") << std::endl;
1119 if ( index==(int)dc.size() ){
1120 Node c = mkCond(cond);
1121 Node v = evaluateInterpreted(n, val);
1122 d.addEntry(fm, c, v);
1123 }
1124 else {
1125 TypeNode vtn = n.getType();
1126 for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
1127 if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {
1128 std::vector< Node > new_cond;
1129 new_cond.insert(new_cond.end(), cond.begin(), cond.end());
1130 if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){
1131 bool process = true;
1132 if (vtn.isBoolean()) {
1133 //short circuit
1134 if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||
1135 (n.getKind()==AND && dc[index].d_value[i]==d_false) ){
1136 Node c = mkCond(new_cond);
1137 d.addEntry(fm, c, dc[index].d_value[i]);
1138 process = false;
1139 }
1140 }
1141 if (process) {
1142 val.push_back(dc[index].d_value[i]);
1143 doInterpretedCompose(fm, f, d, n, dc, index+1, new_cond, val);
1144 val.pop_back();
1145 }
1146 }
1147 }
1148 }
1149 }
1150 }
1151
isCompat(FirstOrderModelFmc * fm,std::vector<Node> & cond,Node c)1152 int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
1153 Trace("fmc-debug3") << "isCompat " << c << std::endl;
1154 Assert(cond.size()==c.getNumChildren()+1);
1155 for (unsigned i=1; i<cond.size(); i++) {
1156 if (cond[i] != c[i - 1] && !fm->isStar(cond[i]) && !fm->isStar(c[i - 1]))
1157 {
1158 return 0;
1159 }
1160 }
1161 return 1;
1162 }
1163
doMeet(FirstOrderModelFmc * fm,std::vector<Node> & cond,Node c)1164 bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
1165 Trace("fmc-debug3") << "doMeet " << c << std::endl;
1166 Assert(cond.size()==c.getNumChildren()+1);
1167 for (unsigned i=1; i<cond.size(); i++) {
1168 if( cond[i]!=c[i-1] ) {
1169 if (fm->isStar(cond[i]))
1170 {
1171 cond[i] = c[i - 1];
1172 }
1173 else if (!fm->isStar(c[i - 1]))
1174 {
1175 return false;
1176 }
1177 }
1178 }
1179 return true;
1180 }
1181
mkCond(std::vector<Node> & cond)1182 Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
1183 return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
1184 }
1185
mkCondDefault(FirstOrderModelFmc * fm,Node f)1186 Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {
1187 std::vector< Node > cond;
1188 mkCondDefaultVec(fm, f, cond);
1189 return mkCond(cond);
1190 }
1191
mkCondDefaultVec(FirstOrderModelFmc * fm,Node f,std::vector<Node> & cond)1192 void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {
1193 Trace("fmc-debug") << "Make default vec" << std::endl;
1194 //get function symbol for f
1195 cond.push_back(d_quant_cond[f]);
1196 for (unsigned i=0; i<f[0].getNumChildren(); i++) {
1197 Node ts = fm->getStar(f[0][i].getType());
1198 Assert( ts.getType()==f[0][i].getType() );
1199 cond.push_back(ts);
1200 }
1201 }
1202
mkCondVec(Node n,std::vector<Node> & cond)1203 void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {
1204 cond.push_back(n.getOperator());
1205 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1206 cond.push_back( n[i] );
1207 }
1208 }
1209
evaluateInterpreted(Node n,std::vector<Node> & vals)1210 Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
1211 if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
1212 if (!vals[0].isNull() && !vals[1].isNull()) {
1213 return vals[0]==vals[1] ? d_true : d_false;
1214 }else{
1215 return Node::null();
1216 }
1217 }else if( n.getKind()==ITE ){
1218 if( vals[0]==d_true ){
1219 return vals[1];
1220 }else if( vals[0]==d_false ){
1221 return vals[2];
1222 }else{
1223 return vals[1]==vals[2] ? vals[1] : Node::null();
1224 }
1225 }else if( n.getKind()==AND || n.getKind()==OR ){
1226 bool isNull = false;
1227 for (unsigned i=0; i<vals.size(); i++) {
1228 if((vals[i]==d_true && n.getKind()==OR) || (vals[i]==d_false && n.getKind()==AND)) {
1229 return vals[i];
1230 }else if( vals[i].isNull() ){
1231 isNull = true;
1232 }
1233 }
1234 return isNull ? Node::null() : vals[0];
1235 }else{
1236 std::vector<Node> children;
1237 if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
1238 children.push_back( n.getOperator() );
1239 }
1240 for (unsigned i=0; i<vals.size(); i++) {
1241 if( vals[i].isNull() ){
1242 return Node::null();
1243 }else{
1244 children.push_back( vals[i] );
1245 }
1246 }
1247 Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children);
1248 Trace("fmc-eval") << "Evaluate " << nc << " to ";
1249 nc = Rewriter::rewrite(nc);
1250 Trace("fmc-eval") << nc << std::endl;
1251 return nc;
1252 }
1253 }
1254
getSomeDomainElement(FirstOrderModelFmc * fm,TypeNode tn)1255 Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) {
1256 bool addRepId = !fm->getRepSet()->hasType(tn);
1257 Node de = fm->getSomeDomainElement(tn);
1258 if( addRepId ){
1259 d_rep_ids[tn][de] = 0;
1260 }
1261 return de;
1262 }
1263
getFunctionValue(FirstOrderModelFmc * fm,Node op,const char * argPrefix)1264 Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {
1265 return fm->getFunctionValue(op, argPrefix);
1266 }
1267
1268
useSimpleModels()1269 bool FullModelChecker::useSimpleModels() {
1270 return options::fmfFmcSimple();
1271 }
1272