1 /********************* */
2 /*! \file model_builder.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
12 ** \brief Implementation of model builder class
15 #include "theory/quantifiers/model_builder.h"
17 #include "options/quantifiers_options.h"
18 #include "theory/quantifiers/first_order_model.h"
19 #include "theory/quantifiers/instantiate.h"
20 #include "theory/quantifiers/model_engine.h"
21 #include "theory/quantifiers/quantifiers_attributes.h"
22 #include "theory/quantifiers/term_database.h"
23 #include "theory/quantifiers/term_util.h"
24 #include "theory/quantifiers/trigger.h"
25 #include "theory/theory_engine.h"
26 #include "theory/uf/equality_engine.h"
27 #include "theory/uf/theory_uf.h"
28 #include "theory/uf/theory_uf_model.h"
29 #include "theory/uf/theory_uf_strong_solver.h"
33 using namespace CVC4::kind
;
34 using namespace CVC4::context
;
35 using namespace CVC4::theory
;
36 using namespace CVC4::theory::quantifiers
;
38 QModelBuilder::QModelBuilder(context::Context
* c
, QuantifiersEngine
* qe
)
39 : TheoryEngineModelBuilder(qe
->getTheoryEngine()),
44 bool QModelBuilder::optUseModel() {
45 return options::mbqiMode()!=MBQI_NONE
|| options::fmfBound();
48 bool QModelBuilder::preProcessBuildModel(TheoryModel
* m
) {
49 return preProcessBuildModelStd( m
);
52 bool QModelBuilder::preProcessBuildModelStd(TheoryModel
* m
) {
55 if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
56 FirstOrderModel
* fm
= (FirstOrderModel
*)m
;
57 //traverse equality engine
58 std::map
< TypeNode
, bool > eqc_usort
;
59 eq::EqClassesIterator eqcs_i
=
60 eq::EqClassesIterator(fm
->getEqualityEngine());
61 while( !eqcs_i
.isFinished() ){
62 TypeNode tr
= (*eqcs_i
).getType();
66 //look at quantified formulas
67 for( unsigned i
=0; i
<fm
->getNumAssertedQuantifiers(); i
++ ){
68 Node q
= fm
->getAssertedQuantifier( i
, true );
69 if( fm
->isQuantifierActive( q
) ){
70 //check if any of these quantified formulas can be set inactive
71 if( options::fmfEmptySorts() ){
72 for( unsigned i
=0; i
<q
[0].getNumChildren(); i
++ ){
73 TypeNode tn
= q
[0][i
].getType();
74 //we are allowed to assume the type is empty
75 if( tn
.isSort() && eqc_usort
.find( tn
)==eqc_usort
.end() ){
76 Trace("model-engine-debug") << "Empty domain quantified formula : " << q
<< std::endl
;
77 fm
->setQuantifierActive( q
, false );
80 }else if( options::fmfFunWellDefinedRelevant() ){
81 if( q
[0].getNumChildren()==1 ){
82 TypeNode tn
= q
[0][0].getType();
83 if( tn
.getAttribute(AbsTypeFunDefAttribute()) ){
84 //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
85 //we are allowed to assume the introduced type is empty
86 if( eqc_usort
.find( tn
)==eqc_usort
.end() ){
87 Trace("model-engine-debug") << "Irrelevant function definition : " << q
<< std::endl
;
88 fm
->setQuantifierActive( q
, false );
99 void QModelBuilder::debugModel( TheoryModel
* m
){
100 //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
101 if( Trace
.isOn("quant-check-model") ){
102 FirstOrderModel
* fm
= (FirstOrderModel
*)m
;
103 Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl
;
106 for( unsigned i
=0; i
<fm
->getNumAssertedQuantifiers(); i
++ ){
107 Node f
= fm
->getAssertedQuantifier( i
);
108 std::vector
< Node
> vars
;
109 for( unsigned j
=0; j
<f
[0].getNumChildren(); j
++ ){
110 vars
.push_back( f
[0][j
] );
112 QRepBoundExt
qrbe(d_qe
);
113 RepSetIterator
riter(d_qe
->getModel()->getRepSet(), &qrbe
);
114 if( riter
.setQuantifier( f
) ){
115 while( !riter
.isFinished() ){
117 std::vector
< Node
> terms
;
118 for (unsigned k
= 0; k
< riter
.getNumTerms(); k
++)
120 terms
.push_back( riter
.getCurrentTerm( k
) );
122 Node n
= d_qe
->getInstantiate()->getInstantiation(f
, vars
, terms
);
123 Node val
= fm
->getValue( n
);
124 if (val
!= d_qe
->getTermUtil()->d_true
)
126 Trace("quant-check-model") << "******* Instantiation " << n
<< " for " << std::endl
;
127 Trace("quant-check-model") << " " << f
<< std::endl
;
128 Trace("quant-check-model") << " Evaluates to " << val
<< std::endl
;
133 Trace("quant-check-model") << "Tested " << tests
<< " instantiations";
135 Trace("quant-check-model") << ", " << bad
<< " failed" << std::endl
;
137 Trace("quant-check-model") << "." << std::endl
;
139 if( riter
.isIncomplete() ){
140 Trace("quant-check-model") << "Warning: Could not test quantifier " << f
<< std::endl
;
147 bool TermArgBasisTrie::addTerm(FirstOrderModel
* fm
, Node n
, unsigned argIndex
)
149 if (argIndex
< n
.getNumChildren())
152 if( n
[ argIndex
].getAttribute(ModelBasisAttribute()) ){
155 r
= fm
->getRepresentative( n
[ argIndex
] );
157 std::map
< Node
, TermArgBasisTrie
>::iterator it
= d_data
.find( r
);
158 if( it
==d_data
.end() ){
159 d_data
[r
].addTerm(fm
, n
, argIndex
+ 1);
162 return it
->second
.addTerm(fm
, n
, argIndex
+ 1);
169 QModelBuilderIG::QModelBuilderIG(context::Context
* c
, QuantifiersEngine
* qe
)
170 : QModelBuilder(c
, qe
),
174 d_numQuantInstGen(0),
175 d_numQuantNoInstGen(0),
176 d_numQuantNoSelForm(0),
177 d_instGenMatches(0) {}
180 Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
185 bool QModelBuilderIG::processBuildModel( TheoryModel
* m
) {
186 FirstOrderModel
* f
= (FirstOrderModel
*)m
;
187 FirstOrderModelIG
* fm
= f
->asFirstOrderModelIG();
188 Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl
;
189 d_didInstGen
= false;
190 //reset the internal information
192 //only construct first order model if optUseModel() is true
194 Trace("model-engine-debug") << "Initializing " << fm
->getNumAssertedQuantifiers() << " quantifiers..." << std::endl
;
195 //check if any quantifiers are un-initialized
196 for( unsigned i
=0; i
<fm
->getNumAssertedQuantifiers(); i
++ ){
197 Node q
= fm
->getAssertedQuantifier( i
);
198 if( d_qe
->getModel()->isQuantifierActive( q
) ){
199 int lems
= initializeQuantifier(q
, q
, f
);
200 d_statistics
.d_init_inst_gen_lemmas
+= lems
;
201 d_addedLemmas
+= lems
;
202 if( d_qe
->inConflict() ){
207 if( d_addedLemmas
>0 ){
208 Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas
<< std::endl
;
211 Assert( !d_qe
->inConflict() );
214 //analyze the functions
215 Trace("model-engine-debug") << "Analyzing model..." << std::endl
;
217 //analyze the quantifiers
218 Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl
;
220 for( unsigned i
=0; i
<fm
->getNumAssertedQuantifiers(); i
++ ){
221 Node q
= fm
->getAssertedQuantifier( i
);
222 analyzeQuantifier( fm
, q
);
225 //if applicable, find exceptions to model via inst-gen
226 if( options::fmfInstGen() ){
228 d_instGenMatches
= 0;
230 d_numQuantInstGen
= 0;
231 d_numQuantNoInstGen
= 0;
232 d_numQuantNoSelForm
= 0;
233 //now, see if we know that any exceptions via InstGen exist
234 Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl
;
235 for( unsigned i
=0; i
<fm
->getNumAssertedQuantifiers(); i
++ ){
236 Node f
= fm
->getAssertedQuantifier( i
);
237 if( d_qe
->getModel()->isQuantifierActive( f
) ){
238 int lems
= doInstGen( fm
, f
);
239 d_statistics
.d_inst_gen_lemmas
+= lems
;
240 d_addedLemmas
+= lems
;
244 }else if( hasInstGen( f
) ){
245 d_numQuantNoInstGen
++;
247 d_numQuantNoSelForm
++;
249 if( d_qe
->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems
>0 ) ){
256 Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat
<< " / " << d_numQuantInstGen
<< " / ";
257 Trace("model-engine-debug") << d_numQuantNoInstGen
<< " / " << d_numQuantNoSelForm
<< std::endl
;
258 Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches
<< std::endl
;
259 if( Trace
.isOn("model-engine") ){
260 if( d_addedLemmas
>0 ){
261 Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas
<< std::endl
;
263 Trace("model-engine") << "No InstGen lemmas..." << std::endl
;
267 //construct the model if necessary
268 if( d_addedLemmas
==0 ){
269 //if no immediate exceptions, build the model
270 // this model will be an approximation that will need to be tested via exhaustive instantiation
271 Trace("model-engine-debug") << "Building model..." << std::endl
;
273 for( std::map
< Node
, uf::UfModelTree
>::iterator it
= fm
->d_uf_model_tree
.begin(); it
!= fm
->d_uf_model_tree
.end(); ++it
){
274 Trace("model-engine-debug-uf") << "Building model for " << it
->first
<< "..." << std::endl
;
275 constructModelUf( fm
, it
->first
);
277 Trace("model-engine-debug") << "Done building models." << std::endl
;
284 for( std::map
< Node
, uf::UfModelTree
>::iterator it
= fm
->d_uf_model_tree
.begin(); it
!= fm
->d_uf_model_tree
.end(); ++it
){
285 it
->second
.update( fm
);
286 Trace("model-func") << "QModelBuilder: Make function value from tree " << it
->first
<< std::endl
;
287 //construct function values
288 Node f_def
= it
->second
.getFunctionValue( "$x" );
289 fm
->assignFunctionDefinition( it
->first
, f_def
);
291 Assert( d_addedLemmas
==0 );
292 return TheoryEngineModelBuilder::processBuildModel( m
);
295 int QModelBuilderIG::initializeQuantifier(Node f
, Node fp
, FirstOrderModel
* fm
)
297 if( d_quant_basis_match_added
.find( f
)==d_quant_basis_match_added
.end() ){
298 //create the basis match if necessary
299 if( d_quant_basis_match
.find( f
)==d_quant_basis_match
.end() ){
300 Trace("inst-fmf-init") << "Initialize " << f
<< std::endl
;
301 //add the model basis instantiation
302 // This will help produce the necessary information for model completion.
303 // We do this by extending distinguish ground assertions (those
304 // containing terms with "model basis" attribute) to hold for all cases.
306 ////first, check if any variables are required to be equal
307 //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
308 // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
309 // Node n = it->first;
310 // if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){
311 // Notice() << "Unhandled phase req: " << n << std::endl;
314 d_quant_basis_match
[f
] = InstMatch( f
);
315 for (unsigned j
= 0; j
< f
[0].getNumChildren(); j
++)
317 Node t
= fm
->getModelBasisTerm(f
[0][j
].getType());
318 //calculate the basis match for f
319 d_quant_basis_match
[f
].setValue( j
, t
);
321 ++(d_statistics
.d_num_quants_init
);
324 Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match
[f
] << std::endl
;
325 //add model basis instantiation
326 if (d_qe
->getInstantiate()->addInstantiation(fp
, d_quant_basis_match
[f
]))
328 d_quant_basis_match_added
[f
] = true;
331 //shouldn't happen usually, but will occur if x != y is a required literal for f.
332 //Notice() << "No model basis for " << f << std::endl;
333 d_quant_basis_match_added
[f
] = false;
339 void QModelBuilderIG::analyzeModel( FirstOrderModel
* fm
){
340 FirstOrderModelIG
* fmig
= fm
->asFirstOrderModelIG();
341 d_uf_model_constructed
.clear();
342 //determine if any functions are constant
343 for( std::map
< Node
, uf::UfModelTree
>::iterator it
= fmig
->d_uf_model_tree
.begin(); it
!= fmig
->d_uf_model_tree
.end(); ++it
){
345 TermArgBasisTrie tabt
;
346 std::map
< Node
, std::vector
< Node
> >::iterator itut
= fmig
->d_uf_terms
.find( op
);
347 if( itut
!=fmig
->d_uf_terms
.end() ){
348 for( size_t i
=0; i
<itut
->second
.size(); i
++ ){
349 Node n
= fmig
->d_uf_terms
[op
][i
];
350 //for calculating if op is constant
351 Node v
= fmig
->getRepresentative( n
);
353 d_uf_prefs
[op
].d_const_val
= v
;
354 }else if( v
!=d_uf_prefs
[op
].d_const_val
){
355 d_uf_prefs
[op
].d_const_val
= Node::null();
358 //for calculating terms that we don't need to consider
359 //if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
360 if( d_basisNoMatch
.find( n
)==d_basisNoMatch
.end() ){
361 //need to consider if it is not congruent modulo model basis
362 if( !tabt
.addTerm( fmig
, n
) ){
363 d_basisNoMatch
[n
] = true;
368 if( !d_uf_prefs
[op
].d_const_val
.isNull() ){
369 fmig
->d_uf_model_gen
[op
].setDefaultValue( d_uf_prefs
[op
].d_const_val
);
370 fmig
->d_uf_model_gen
[op
].makeModel( fmig
, it
->second
);
371 Debug("fmf-model-cons") << "Function " << op
<< " is the constant function ";
372 fmig
->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs
[op
].d_const_val
);
373 Debug("fmf-model-cons") << std::endl
;
374 d_uf_model_constructed
[op
] = true;
376 d_uf_model_constructed
[op
] = false;
381 bool QModelBuilderIG::hasConstantDefinition( Node n
){
382 Node lit
= n
.getKind()==NOT
? n
[0] : n
;
383 if( lit
.getKind()==APPLY_UF
){
384 Node op
= lit
.getOperator();
385 if( !d_uf_prefs
[op
].d_const_val
.isNull() ){
392 QModelBuilderIG::Statistics::Statistics():
393 d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
394 d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
395 d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
396 d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
397 d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
398 d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
399 d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
400 d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
402 smtStatisticsRegistry()->registerStat(&d_num_quants_init
);
403 smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init
);
404 smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas
);
405 smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas
);
406 smtStatisticsRegistry()->registerStat(&d_eval_formulas
);
407 smtStatisticsRegistry()->registerStat(&d_eval_uf_terms
);
408 smtStatisticsRegistry()->registerStat(&d_eval_lits
);
409 smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown
);
412 QModelBuilderIG::Statistics::~Statistics(){
413 smtStatisticsRegistry()->unregisterStat(&d_num_quants_init
);
414 smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init
);
415 smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas
);
416 smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas
);
417 smtStatisticsRegistry()->unregisterStat(&d_eval_formulas
);
418 smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms
);
419 smtStatisticsRegistry()->unregisterStat(&d_eval_lits
);
420 smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown
);
423 //do exhaustive instantiation
424 int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel
* fm
, Node f
, int effort
) {
426 QRepBoundExt
qrbe(d_qe
);
427 RepSetIterator
riter(d_qe
->getModel()->getRepSet(), &qrbe
);
428 if( riter
.setQuantifier( f
) ){
429 FirstOrderModelIG
* fmig
= (FirstOrderModelIG
*)d_qe
->getModel();
430 Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl
;
431 fmig
->resetEvaluate();
432 Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl
;
433 EqualityQuery
* qy
= d_qe
->getEqualityQuery();
434 Instantiate
* inst
= d_qe
->getInstantiate();
435 TermUtil
* util
= d_qe
->getTermUtil();
436 while( !riter
.isFinished() && ( d_addedLemmas
==0 || !options::fmfOneInstPerRound() ) ){
438 if( Debug
.isOn("inst-fmf-ei-debug") ){
439 for( int i
=0; i
<(int)riter
.d_index
.size(); i
++ ){
440 Debug("inst-fmf-ei-debug") << i
<< " : " << riter
.d_index
[i
] << " : " << riter
.getCurrentTerm( i
) << std::endl
;
445 //see if instantiation is already true in current model
446 if( Debug
.isOn("fmf-model-eval") ){
447 Debug("fmf-model-eval") << "Evaluating ";
448 riter
.debugPrintSmall("fmf-model-eval");
449 Debug("fmf-model-eval") << "Done calculating terms." << std::endl
;
451 //if evaluate(...)==1, then the instantiation is already true in the model
452 // depIndex is the index of the least significant variable that this evaluation relies upon
453 depIndex
= riter
.getNumTerms()-1;
454 Debug("fmf-model-eval") << "We will evaluate "
455 << util
->getInstConstantBody(f
) << std::endl
;
456 eval
= fmig
->evaluate(util
->getInstConstantBody(f
), depIndex
, &riter
);
458 Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex
<< std::endl
;
460 Debug("fmf-model-eval") << " Returned " << (eval
==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex
<< std::endl
;
463 //instantiation is already true -> skip
464 riter
.incrementAtIndex(depIndex
);
466 //instantiation was not shown to be true, construct the match
468 for (unsigned i
= 0; i
< riter
.getNumTerms(); i
++)
470 m
.set(qy
, i
, riter
.getCurrentTerm(i
));
472 Debug("fmf-model-eval") << "* Add instantiation " << m
<< std::endl
;
473 //add as instantiation
474 if (inst
->addInstantiation(f
, m
, true))
477 if( d_qe
->inConflict() ){
480 //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
482 riter
.incrementAtIndex(depIndex
);
487 Debug("fmf-model-eval") << "* Failed Add instantiation " << m
<< std::endl
;
492 //print debugging information
494 d_statistics
.d_eval_formulas
+= fmig
->d_eval_formulas
;
495 d_statistics
.d_eval_uf_terms
+= fmig
->d_eval_uf_terms
;
496 d_statistics
.d_eval_lits
+= fmig
->d_eval_lits
;
497 d_statistics
.d_eval_lits_unknown
+= fmig
->d_eval_lits_unknown
;
499 Trace("inst-fmf-ei") << "For " << f
<< ", finished: " << std::endl
;
500 Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas
<< std::endl
;
501 Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas
<< std::endl
;
502 if( d_addedLemmas
>1000 ){
503 Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f
<< ": " << std::endl
;
504 Trace("model-engine-warn") << " Inst Tried: " << d_triedLemmas
<< std::endl
;
505 Trace("model-engine-warn") << " Inst Added: " << d_addedLemmas
<< std::endl
;
506 Trace("model-engine-warn") << std::endl
;
509 //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
510 return riter
.isIncomplete() ? -1 : 1;
518 void QModelBuilderDefault::reset( FirstOrderModel
* fm
){
519 d_quant_selection_lit
.clear();
520 d_quant_selection_lit_candidates
.clear();
521 d_quant_selection_lit_terms
.clear();
522 d_term_selection_lit
.clear();
523 d_op_selection_terms
.clear();
527 int QModelBuilderDefault::getSelectionScore( std::vector
< Node
>& uf_terms
) {
529 size_t maxChildren = 0;
530 for( size_t i=0; i<uf_terms.size(); i++ ){
531 if( uf_terms[i].getNumChildren()>maxChildren ){
532 maxChildren = uf_terms[i].getNumChildren();
535 //TODO: look at how many entries they have?
536 return (int)maxChildren;
541 void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel
* fm
, Node f
){
542 if( d_qe
->getModel()->isQuantifierActive( f
) ){
543 FirstOrderModelIG
* fmig
= fm
->asFirstOrderModelIG();
544 Debug("fmf-model-prefs") << "Analyze quantifier " << f
<< std::endl
;
545 //the pro/con preferences for this quantifier
546 std::vector
< Node
> pro_con
[2];
547 //the terms in the selection literal we choose
548 std::vector
< Node
> selectionLitTerms
;
549 Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f
<< std::endl
;
550 //for each asserted quantifier f,
551 // - determine selection literals
552 // - check which function/predicates have good and bad definitions for satisfying f
553 if( d_phase_reqs
.find( f
)==d_phase_reqs
.end() ){
554 d_phase_reqs
[f
].initialize( d_qe
->getTermUtil()->getInstConstantBody( f
), true );
556 int selectLitScore
= -1;
557 for( std::map
< Node
, bool >::iterator it
= d_phase_reqs
[f
].d_phase_reqs
.begin(); it
!= d_phase_reqs
[f
].d_phase_reqs
.end(); ++it
){
558 //the literal n is phase-required for quantifier f
560 Node gn
= fm
->getModelBasis(f
, n
);
561 Debug("fmf-model-req") << " Req: " << n
<< " -> " << it
->second
<< std::endl
;
563 //if the corresponding ground abstraction literal has a SAT value
564 if( d_qe
->getValuation().hasSatValue( gn
, value
) ){
565 //collect the non-ground uf terms that this literal contains
566 // and compute if all of the symbols in this literal have
567 // constant definitions.
569 std::vector
< Node
> uf_terms
;
570 if( TermUtil::hasInstConstAttr(n
) ){
572 if( gn
.getKind()==APPLY_UF
){
573 uf_terms
.push_back( gn
);
574 isConst
= hasConstantDefinition( gn
);
575 }else if( gn
.getKind()==EQUAL
){
577 for( int j
=0; j
<2; j
++ ){
578 if( TermUtil::hasInstConstAttr(n
[j
]) ){
579 if( n
[j
].getKind()==APPLY_UF
&&
580 fmig
->d_uf_model_tree
.find( gn
[j
].getOperator() )!=fmig
->d_uf_model_tree
.end() ){
581 uf_terms
.push_back( gn
[j
] );
582 isConst
= isConst
&& hasConstantDefinition( gn
[j
] );
590 //check if the value in the SAT solver matches the preference according to the quantifier
592 if( value
!=it
->second
){
593 //we have a possible selection literal
594 bool selectLit
= d_quant_selection_lit
[f
].isNull();
595 bool selectLitConstraints
= true;
596 //it is a constantly defined selection literal : the quantifier is sat
598 selectLit
= selectLit
|| d_qe
->getModel()->isQuantifierActive( f
);
599 d_qe
->getModel()->setQuantifierActive( f
, false );
600 //check if choosing this literal would add any additional constraints to default definitions
601 selectLitConstraints
= false;
602 for( int j
=0; j
<(int)uf_terms
.size(); j
++ ){
603 Node op
= uf_terms
[j
].getOperator();
604 if( d_uf_prefs
[op
].d_reconsiderModel
){
605 selectLitConstraints
= true;
608 if( !selectLitConstraints
){
612 //also check if it is naturally a better literal
614 int score
= getSelectionScore( uf_terms
);
615 //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl;
616 selectLit
= score
<selectLitScore
;
618 //see if we wish to choose this as a selection literal
619 d_quant_selection_lit_candidates
[f
].push_back( value
? n
: n
.notNode() );
621 selectLitScore
= getSelectionScore( uf_terms
);
622 Trace("inst-gen-debug") << "Choose selection literal " << gn
<< std::endl
;
623 Trace("inst-gen-debug") << " flags: " << isConst
<< " " << selectLitConstraints
<< " " << selectLitScore
<< std::endl
;
624 d_quant_selection_lit
[f
] = value
? n
: n
.notNode();
625 selectionLitTerms
.clear();
626 selectionLitTerms
.insert( selectionLitTerms
.begin(), uf_terms
.begin(), uf_terms
.end() );
627 if( !selectLitConstraints
){
635 //if we are not yet SAT, so we will add to preferences
636 if( d_qe
->getModel()->isQuantifierActive( f
) ){
637 Debug("fmf-model-prefs") << " It is " << ( pref
==1 ? "pro" : "con" );
638 Debug("fmf-model-prefs") << " the definition of " << n
<< std::endl
;
639 for( int j
=0; j
<(int)uf_terms
.size(); j
++ ){
640 pro_con
[ pref
==1 ? 0 : 1 ].push_back( uf_terms
[j
] );
645 //process information about selection literal for f
646 if( !d_quant_selection_lit
[f
].isNull() ){
647 d_quant_selection_lit_terms
[f
].insert( d_quant_selection_lit_terms
[f
].begin(), selectionLitTerms
.begin(), selectionLitTerms
.end() );
648 for( int i
=0; i
<(int)selectionLitTerms
.size(); i
++ ){
649 d_term_selection_lit
[ selectionLitTerms
[i
] ] = d_quant_selection_lit
[f
];
650 d_op_selection_terms
[ selectionLitTerms
[i
].getOperator() ].push_back( selectionLitTerms
[i
] );
653 Trace("inst-gen-warn") << "WARNING: " << f
<< " has no selection literals" << std::endl
;
655 //process information about requirements and preferences of quantifier f
656 if( !d_qe
->getModel()->isQuantifierActive( f
) ){
657 Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: ";
658 for( int i
=0; i
<(int)selectionLitTerms
.size(); i
++ ){
659 Debug("fmf-model-prefs") << selectionLitTerms
[i
] << " ";
660 d_uf_prefs
[ selectionLitTerms
[i
].getOperator() ].d_reconsiderModel
= false;
662 Debug("fmf-model-prefs") << std::endl
;
664 //note quantifier's value preferences to models
665 for( int k
=0; k
<2; k
++ ){
666 for( int j
=0; j
<(int)pro_con
[k
].size(); j
++ ){
667 Node op
= pro_con
[k
][j
].getOperator();
668 Node r
= fmig
->getRepresentative( pro_con
[k
][j
] );
669 d_uf_prefs
[op
].setValuePreference( f
, pro_con
[k
][j
], r
, k
==0 );
676 int QModelBuilderDefault::doInstGen( FirstOrderModel
* fm
, Node f
){
678 //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
679 //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
680 // effectively acting as partial instantiations instead of pointwise instantiations.
681 if( !d_quant_selection_lit
[f
].isNull() ){
682 Trace("inst-gen") << "Do Inst-Gen for " << f
<< std::endl
;
683 for( size_t i
=0; i
<d_quant_selection_lit_candidates
[f
].size(); i
++ ){
684 bool phase
= d_quant_selection_lit_candidates
[f
][i
].getKind()!=NOT
;
685 Node lit
= d_quant_selection_lit_candidates
[f
][i
].getKind()==NOT
? d_quant_selection_lit_candidates
[f
][i
][0] : d_quant_selection_lit_candidates
[f
][i
];
686 Assert( TermUtil::hasInstConstAttr(lit
) );
687 std::vector
< Node
> tr_terms
;
688 if( lit
.getKind()==APPLY_UF
){
689 //only match predicates that are contrary to this one, use literal matching
690 Node eq
= NodeManager::currentNM()->mkNode(
691 EQUAL
, lit
, NodeManager::currentNM()->mkConst(!phase
));
692 tr_terms
.push_back( eq
);
693 }else if( lit
.getKind()==EQUAL
){
694 //collect trigger terms
695 for( int j
=0; j
<2; j
++ ){
696 if( TermUtil::hasInstConstAttr(lit
[j
]) ){
697 if( lit
[j
].getKind()==APPLY_UF
){
698 tr_terms
.push_back( lit
[j
] );
705 if( tr_terms
.size()==1 && !phase
){
706 //equality between a function and a ground term, use literal matching
708 tr_terms
.push_back( lit
);
711 //if applicable, try to add exceptions here
712 if( !tr_terms
.empty() ){
713 //make a trigger for these terms, add instantiations
714 inst::Trigger
* tr
= inst::Trigger::mkTrigger( d_qe
, f
, tr_terms
, true, inst::Trigger::TR_MAKE_NEW
);
715 //Notice() << "Trigger = " << (*tr) << std::endl;
716 tr
->resetInstantiationRound();
717 tr
->reset( Node::null() );
718 //d_qe->d_optInstMakeRepresentative = false;
719 //d_qe->d_optMatchIgnoreModelBasis = true;
720 addedLemmas
+= tr
->addInstantiations( d_quant_basis_match
[f
] );
727 void QModelBuilderDefault::constructModelUf( FirstOrderModel
* fm
, Node op
){
728 FirstOrderModelIG
* fmig
= fm
->asFirstOrderModelIG();
729 if( optReconsiderFuncConstants() ){
730 //reconsider constant functions that weren't necessary
731 if( d_uf_model_constructed
[op
] ){
732 if( d_uf_prefs
[op
].d_reconsiderModel
){
733 //if we are allowed to reconsider default value, then see if the default value can be improved
734 Node v
= d_uf_prefs
[op
].d_const_val
;
735 if( d_uf_prefs
[op
].d_value_pro_con
[0][v
].empty() ){
736 Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op
<< std::endl
;
737 fmig
->d_uf_model_tree
[op
].clear();
738 fmig
->d_uf_model_gen
[op
].clear();
739 d_uf_model_constructed
[op
] = false;
744 if( !d_uf_model_constructed
[op
] ){
745 //construct the model for the uninterpretted function/predicate
746 bool setDefaultVal
= true;
747 Node defaultTerm
= fmig
->getModelBasisOpTerm(op
);
748 Trace("fmf-model-cons") << "Construct model for " << op
<< "..." << std::endl
;
749 //set the values in the model
750 std::map
< Node
, std::vector
< Node
> >::iterator itut
= fmig
->d_uf_terms
.find( op
);
751 if( itut
!=fmig
->d_uf_terms
.end() ){
752 for( size_t i
=0; i
<itut
->second
.size(); i
++ ){
753 Node n
= itut
->second
[i
];
754 // only consider unique up to congruence (in model equality engine)?
755 Node v
= fmig
->getRepresentative( n
);
756 Trace("fmf-model-cons") << "Set term " << n
<< " : "
757 << fmig
->getRepSet()->getIndexFor(v
) << " " << v
759 //if this assertion did not help the model, just consider it ground
760 //set n = v in the model tree
761 //set it as ground value
762 fmig
->d_uf_model_gen
[op
].setValue( fm
, n
, v
);
763 if( fmig
->d_uf_model_gen
[op
].optUsePartialDefaults() ){
764 //also set as default value if necessary
765 if( n
.hasAttribute(ModelBasisArgAttribute()) && n
.getAttribute(ModelBasisArgAttribute())!=0 ){
766 Trace("fmf-model-cons") << " Set as default." << std::endl
;
767 fmig
->d_uf_model_gen
[op
].setValue( fm
, n
, v
, false );
768 if( n
==defaultTerm
){
769 //incidentally already set, we will not need to find a default value
770 setDefaultVal
= false;
774 if( n
==defaultTerm
){
775 fmig
->d_uf_model_gen
[op
].setValue( fm
, n
, v
, false );
776 //incidentally already set, we will not need to find a default value
777 setDefaultVal
= false;
782 //set the overall default value if not set already (is this necessary??)
784 Trace("fmf-model-cons") << " Choose default value..." << std::endl
;
785 //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
786 Node defaultVal
= d_uf_prefs
[op
].getBestDefaultValue( defaultTerm
, fm
);
787 if( defaultVal
.isNull() ){
788 if (!fmig
->getRepSet()->hasType(defaultTerm
.getType()))
790 Node mbt
= fmig
->getModelBasisTerm(defaultTerm
.getType());
791 fmig
->getRepSetPtr()->d_type_reps
[defaultTerm
.getType()].push_back(
795 fmig
->getRepSet()->getRepresentative(defaultTerm
.getType(), 0);
797 Assert( !defaultVal
.isNull() );
798 Trace("fmf-model-cons")
799 << "Set default term : " << fmig
->getRepSet()->getIndexFor(defaultVal
)
801 fmig
->d_uf_model_gen
[op
].setValue( fm
, defaultTerm
, defaultVal
, false );
803 Debug("fmf-model-cons") << " Making model...";
804 fmig
->d_uf_model_gen
[op
].makeModel( fm
, fmig
->d_uf_model_tree
[op
] );
805 d_uf_model_constructed
[op
] = true;
806 Debug("fmf-model-cons") << " Finished constructing model for " << op
<< "." << std::endl
;