1 /********************* */
2 /*! \file model_builder.cpp
4 ** Original author: Andrew Reynolds
5 ** Major contributors: none
6 ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Implementation of model builder class
15 #include "theory/quantifiers/model_engine.h"
16 #include "theory/theory_engine.h"
17 #include "theory/uf/equality_engine.h"
18 #include "theory/uf/theory_uf.h"
19 #include "theory/uf/theory_uf_model.h"
20 #include "theory/uf/theory_uf_strong_solver.h"
21 #include "theory/quantifiers/first_order_model.h"
22 #include "theory/quantifiers/term_database.h"
23 #include "theory/quantifiers/model_builder.h"
24 #include "theory/quantifiers/quantifiers_attributes.h"
25 #include "theory/quantifiers/inst_gen.h"
26 #include "theory/quantifiers/trigger.h"
27 #include "theory/quantifiers/options.h"
31 using namespace CVC4::kind
;
32 using namespace CVC4::context
;
33 using namespace CVC4::theory
;
34 using namespace CVC4::theory::quantifiers
;
37 QModelBuilder::QModelBuilder( context::Context
* c
, QuantifiersEngine
* qe
) :
38 TheoryEngineModelBuilder( qe
->getTheoryEngine() ), d_curr_model( c
, NULL
), d_qe( qe
){
39 d_considerAxioms
= true;
42 bool QModelBuilder::isQuantifierActive( Node f
) {
43 return d_qe
->hasOwnership( f
);
47 bool QModelBuilder::optUseModel() {
48 return options::mbqiMode()!=MBQI_NONE
|| options::fmfBoundInt();
51 void QModelBuilder::debugModel( FirstOrderModel
* fm
){
52 //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
53 if( Trace
.isOn("quant-model-warn") ){
54 Trace("quant-model-warn") << "Testing quantifier instantiations..." << std::endl
;
57 for( int i
=0; i
<fm
->getNumAssertedQuantifiers(); i
++ ){
58 Node f
= fm
->getAssertedQuantifier( i
);
59 std::vector
< Node
> vars
;
60 for( int j
=0; j
<(int)f
[0].getNumChildren(); j
++ ){
61 vars
.push_back( f
[0][j
] );
63 RepSetIterator
riter( d_qe
, &(fm
->d_rep_set
) );
64 if( riter
.setQuantifier( f
) ){
65 while( !riter
.isFinished() ){
67 std::vector
< Node
> terms
;
68 for( int i
=0; i
<riter
.getNumTerms(); i
++ ){
69 terms
.push_back( riter
.getTerm( i
) );
71 Node n
= d_qe
->getInstantiation( f
, vars
, terms
);
72 Node val
= fm
->getValue( n
);
73 if( val
!=fm
->d_true
){
74 Trace("quant-model-warn") << "******* Instantiation " << n
<< " for " << std::endl
;
75 Trace("quant-model-warn") << " " << f
<< std::endl
;
76 Trace("quant-model-warn") << " Evaluates to " << val
<< std::endl
;
81 Trace("quant-model-warn") << "Tested " << tests
<< " instantiations";
83 Trace("quant-model-warn") << ", " << bad
<< " failed" << std::endl
;
85 Trace("quant-model-warn") << "." << std::endl
;
87 Trace("quant-model-warn") << "Warning: Could not test quantifier " << f
<< std::endl
;
95 bool TermArgBasisTrie::addTerm2( FirstOrderModel
* fm
, Node n
, int argIndex
){
96 if( argIndex
<(int)n
.getNumChildren() ){
98 if( n
[ argIndex
].getAttribute(ModelBasisAttribute()) ){
101 r
= fm
->getRepresentative( n
[ argIndex
] );
103 std::map
< Node
, TermArgBasisTrie
>::iterator it
= d_data
.find( r
);
104 if( it
==d_data
.end() ){
105 d_data
[r
].addTerm2( fm
, n
, argIndex
+1 );
108 return it
->second
.addTerm2( fm
, n
, argIndex
+1 );
116 QModelBuilderIG::QModelBuilderIG( context::Context
* c
, QuantifiersEngine
* qe
) :
117 QModelBuilder( c
, qe
) {
121 Node
QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel
* fm
, Node n
, std::vector
< Node
> & args
, bool partial
) {
125 void QModelBuilderIG::processBuildModel( TheoryModel
* m
, bool fullModel
) {
126 FirstOrderModel
* f
= (FirstOrderModel
*)m
;
127 FirstOrderModelIG
* fm
= f
->asFirstOrderModelIG();
128 Trace("model-engine-debug") << "Process build model, fullModel = " << fullModel
<< " " << optUseModel() << std::endl
;
130 Assert( d_curr_model
==fm
);
132 for( std::map
< Node
, uf::UfModelTree
>::iterator it
= fm
->d_uf_model_tree
.begin(); it
!= fm
->d_uf_model_tree
.end(); ++it
){
133 it
->second
.update( fm
);
134 Trace("model-func") << "QModelBuilder: Make function value from tree " << it
->first
<< std::endl
;
135 //construct function values
136 fm
->d_uf_models
[ it
->first
] = it
->second
.getFunctionValue( "$x" );
138 TheoryEngineModelBuilder::processBuildModel( m
, fullModel
);
139 //mark that the model has been set
145 d_didInstGen
= false;
146 //reset the internal information
148 //only construct first order model if optUseModel() is true
150 Trace("model-engine-debug") << "Initializing " << fm
->getNumAssertedQuantifiers() << " quantifiers..." << std::endl
;
151 //check if any quantifiers are un-initialized
152 for( int i
=0; i
<fm
->getNumAssertedQuantifiers(); i
++ ){
153 Node f
= fm
->getAssertedQuantifier( i
);
154 if( isQuantifierActive( f
) ){
155 int lems
= initializeQuantifier( f
, f
);
156 d_statistics
.d_init_inst_gen_lemmas
+= lems
;
157 d_addedLemmas
+= lems
;
160 if( d_addedLemmas
>0 ){
161 Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas
<< std::endl
;
164 fm
->initialize( d_considerAxioms
);
165 //analyze the functions
166 Trace("model-engine-debug") << "Analyzing model..." << std::endl
;
168 //analyze the quantifiers
169 Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl
;
172 for( int i
=0; i
<fm
->getNumAssertedQuantifiers(); i
++ ){
173 Node f
= fm
->getAssertedQuantifier( i
);
174 if( isQuantifierActive( f
) ){
175 analyzeQuantifier( fm
, f
);
179 //if applicable, find exceptions to model via inst-gen
182 d_instGenMatches
= 0;
184 d_numQuantInstGen
= 0;
185 d_numQuantNoInstGen
= 0;
186 d_numQuantNoSelForm
= 0;
187 //now, see if we know that any exceptions via InstGen exist
188 Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl
;
189 for( int i
=0; i
<fm
->getNumAssertedQuantifiers(); i
++ ){
190 Node f
= fm
->getAssertedQuantifier( i
);
191 if( isQuantifierActive( f
) ){
192 int lems
= doInstGen( fm
, f
);
193 d_statistics
.d_inst_gen_lemmas
+= lems
;
194 d_addedLemmas
+= lems
;
198 }else if( d_quant_sat
.find( f
)!=d_quant_sat
.end() ){
200 }else if( hasInstGen( f
) ){
201 d_numQuantNoInstGen
++;
203 d_numQuantNoSelForm
++;
205 if( optOneQuantPerRoundInstGen() && lems
>0 ){
208 }else if( d_quant_sat
.find( f
)!=d_quant_sat
.end() ){
212 Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat
<< " / " << d_numQuantInstGen
<< " / ";
213 Trace("model-engine-debug") << d_numQuantNoInstGen
<< " / " << d_numQuantNoSelForm
<< std::endl
;
214 Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches
<< std::endl
;
215 if( Trace
.isOn("model-engine") ){
216 if( d_addedLemmas
>0 ){
217 Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas
<< std::endl
;
219 Trace("model-engine") << "No InstGen lemmas..." << std::endl
;
223 //construct the model if necessary
224 if( d_addedLemmas
==0 ){
225 //if no immediate exceptions, build the model
226 // this model will be an approximation that will need to be tested via exhaustive instantiation
227 Trace("model-engine-debug") << "Building model..." << std::endl
;
229 for( std::map
< Node
, uf::UfModelTree
>::iterator it
= fm
->d_uf_model_tree
.begin(); it
!= fm
->d_uf_model_tree
.end(); ++it
){
230 Trace("model-engine-debug-uf") << "Building model for " << it
->first
<< "..." << std::endl
;
231 constructModelUf( fm
, it
->first
);
234 //build model for arrays
235 for( std::map< Node, arrays::ArrayModel >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){
236 //consult the model basis select term
237 // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term
238 TypeNode tn = it->first.getType();
239 Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) );
240 it->second.setDefaultValue( fm->getRepresentative( selModelBasis ) );
243 Trace("model-engine-debug") << "Done building models." << std::endl
;
250 int QModelBuilderIG::initializeQuantifier( Node f
, Node fp
){
251 if( d_quant_basis_match_added
.find( f
)==d_quant_basis_match_added
.end() ){
252 //create the basis match if necessary
253 if( d_quant_basis_match
.find( f
)==d_quant_basis_match
.end() ){
254 Trace("inst-fmf-init") << "Initialize " << f
<< std::endl
;
255 //add the model basis instantiation
256 // This will help produce the necessary information for model completion.
257 // We do this by extending distinguish ground assertions (those
258 // containing terms with "model basis" attribute) to hold for all cases.
260 ////first, check if any variables are required to be equal
261 //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
262 // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
263 // Node n = it->first;
264 // if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){
265 // Notice() << "Unhandled phase req: " << n << std::endl;
268 d_quant_basis_match
[f
] = InstMatch( f
);
269 for( int j
=0; j
<(int)f
[0].getNumChildren(); j
++ ){
270 Node t
= d_qe
->getTermDatabase()->getModelBasisTerm( f
[0][j
].getType() );
271 //calculate the basis match for f
272 d_quant_basis_match
[f
].setValue( j
, t
);
274 ++(d_statistics
.d_num_quants_init
);
277 Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match
[f
] << std::endl
;
278 //add model basis instantiation
279 if( d_qe
->addInstantiation( fp
, d_quant_basis_match
[f
], false ) ){
280 d_quant_basis_match_added
[f
] = true;
283 //shouldn't happen usually, but will occur if x != y is a required literal for f.
284 //Notice() << "No model basis for " << f << std::endl;
285 d_quant_basis_match_added
[f
] = false;
291 void QModelBuilderIG::analyzeModel( FirstOrderModel
* fm
){
292 FirstOrderModelIG
* fmig
= fm
->asFirstOrderModelIG();
293 d_uf_model_constructed
.clear();
294 //determine if any functions are constant
295 for( std::map
< Node
, uf::UfModelTree
>::iterator it
= fmig
->d_uf_model_tree
.begin(); it
!= fmig
->d_uf_model_tree
.end(); ++it
){
297 TermArgBasisTrie tabt
;
298 for( size_t i
=0; i
<fmig
->d_uf_terms
[op
].size(); i
++ ){
299 Node n
= fmig
->d_uf_terms
[op
][i
];
300 //for calculating if op is constant
301 if( !n
.getAttribute(NoMatchAttribute()) ){
302 Node v
= fmig
->getRepresentative( n
);
304 d_uf_prefs
[op
].d_const_val
= v
;
305 }else if( v
!=d_uf_prefs
[op
].d_const_val
){
306 d_uf_prefs
[op
].d_const_val
= Node::null();
310 //for calculating terms that we don't need to consider
311 if( !n
.getAttribute(NoMatchAttribute()) || n
.getAttribute(ModelBasisArgAttribute())!=0 ){
312 if( !n
.getAttribute(BasisNoMatchAttribute()) ){
313 //need to consider if it is not congruent modulo model basis
314 if( !tabt
.addTerm( fmig
, n
) ){
315 BasisNoMatchAttribute bnma
;
316 n
.setAttribute(bnma
,true);
321 if( !d_uf_prefs
[op
].d_const_val
.isNull() ){
322 fmig
->d_uf_model_gen
[op
].setDefaultValue( d_uf_prefs
[op
].d_const_val
);
323 fmig
->d_uf_model_gen
[op
].makeModel( fmig
, it
->second
);
324 Debug("fmf-model-cons") << "Function " << op
<< " is the constant function ";
325 fmig
->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs
[op
].d_const_val
);
326 Debug("fmf-model-cons") << std::endl
;
327 d_uf_model_constructed
[op
] = true;
329 d_uf_model_constructed
[op
] = false;
334 bool QModelBuilderIG::hasConstantDefinition( Node n
){
335 Node lit
= n
.getKind()==NOT
? n
[0] : n
;
336 if( lit
.getKind()==APPLY_UF
){
337 Node op
= lit
.getOperator();
338 if( !d_uf_prefs
[op
].d_const_val
.isNull() ){
345 bool QModelBuilderIG::optInstGen(){
346 return options::fmfInstGen();
349 bool QModelBuilderIG::optOneQuantPerRoundInstGen(){
350 return options::fmfInstGenOneQuantPerRound();
353 QModelBuilderIG::Statistics::Statistics():
354 d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
355 d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
356 d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
357 d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
358 d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
359 d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
360 d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
361 d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
363 StatisticsRegistry::registerStat(&d_num_quants_init
);
364 StatisticsRegistry::registerStat(&d_num_partial_quants_init
);
365 StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas
);
366 StatisticsRegistry::registerStat(&d_inst_gen_lemmas
);
367 StatisticsRegistry::registerStat(&d_eval_formulas
);
368 StatisticsRegistry::registerStat(&d_eval_uf_terms
);
369 StatisticsRegistry::registerStat(&d_eval_lits
);
370 StatisticsRegistry::registerStat(&d_eval_lits_unknown
);
373 QModelBuilderIG::Statistics::~Statistics(){
374 StatisticsRegistry::unregisterStat(&d_num_quants_init
);
375 StatisticsRegistry::unregisterStat(&d_num_partial_quants_init
);
376 StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas
);
377 StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas
);
378 StatisticsRegistry::unregisterStat(&d_eval_formulas
);
379 StatisticsRegistry::unregisterStat(&d_eval_uf_terms
);
380 StatisticsRegistry::unregisterStat(&d_eval_lits
);
381 StatisticsRegistry::unregisterStat(&d_eval_lits_unknown
);
384 bool QModelBuilderIG::isQuantifierActive( Node f
){
385 return d_qe
->hasOwnership( f
) && ( d_considerAxioms
|| !d_qe
->getTermDatabase()->isQAttrAxiom( f
) ) && d_quant_sat
.find( f
)==d_quant_sat
.end();
388 bool QModelBuilderIG::isTermActive( Node n
){
389 return !n
.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term
390 ( n
.getAttribute(ModelBasisArgAttribute())!=0 && !n
.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
391 //and is not congruent modulo model basis
392 //to another active term
396 //do exhaustive instantiation
397 bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel
* fm
, Node f
, int effort
) {
399 RepSetIterator
riter( d_qe
, &(d_qe
->getModel()->d_rep_set
) );
400 if( riter
.setQuantifier( f
) ){
401 FirstOrderModelIG
* fmig
= (FirstOrderModelIG
*)d_qe
->getModel();
402 Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl
;
403 fmig
->resetEvaluate();
404 Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl
;
405 while( !riter
.isFinished() && ( d_addedLemmas
==0 || !options::fmfOneInstPerRound() ) ){
407 for( int i
=0; i
<(int)riter
.d_index
.size(); i
++ ){
408 Trace("try") << i
<< " : " << riter
.d_index
[i
] << " : " << riter
.getTerm( i
) << std::endl
;
412 //see if instantiation is already true in current model
413 Debug("fmf-model-eval") << "Evaluating ";
414 riter
.debugPrintSmall("fmf-model-eval");
415 Debug("fmf-model-eval") << "Done calculating terms." << std::endl
;
416 //if evaluate(...)==1, then the instantiation is already true in the model
417 // depIndex is the index of the least significant variable that this evaluation relies upon
418 depIndex
= riter
.getNumTerms()-1;
419 Debug("fmf-model-eval") << "We will evaluate " << d_qe
->getTermDatabase()->getInstConstantBody( f
) << std::endl
;
420 eval
= fmig
->evaluate( d_qe
->getTermDatabase()->getInstConstantBody( f
), depIndex
, &riter
);
422 Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex
<< std::endl
;
424 Debug("fmf-model-eval") << " Returned " << (eval
==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex
<< std::endl
;
427 //instantiation is already true -> skip
428 riter
.increment2( depIndex
);
430 //instantiation was not shown to be true, construct the match
432 for( int i
=0; i
<riter
.getNumTerms(); i
++ ){
433 m
.set( d_qe
, riter
.d_index_order
[i
], riter
.getTerm( i
) );
435 Debug("fmf-model-eval") << "* Add instantiation " << m
<< std::endl
;
436 //add as instantiation
437 if( d_qe
->addInstantiation( f
, m
) ){
439 //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
441 riter
.increment2( depIndex
);
446 Debug("fmf-model-eval") << "* Failed Add instantiation " << m
<< std::endl
;
451 //print debugging information
453 d_statistics
.d_eval_formulas
+= fmig
->d_eval_formulas
;
454 d_statistics
.d_eval_uf_terms
+= fmig
->d_eval_uf_terms
;
455 d_statistics
.d_eval_lits
+= fmig
->d_eval_lits
;
456 d_statistics
.d_eval_lits_unknown
+= fmig
->d_eval_lits_unknown
;
458 Trace("inst-fmf-ei") << "For " << f
<< ", finished: " << std::endl
;
459 Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas
<< std::endl
;
460 Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas
<< std::endl
;
461 if( d_addedLemmas
>1000 ){
462 Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f
<< ": " << std::endl
;
463 Trace("model-engine-warn") << " Inst Tried: " << d_triedLemmas
<< std::endl
;
464 Trace("model-engine-warn") << " Inst Added: " << d_addedLemmas
<< std::endl
;
465 Trace("model-engine-warn") << std::endl
;
468 //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
469 d_incomplete_check
= riter
.d_incomplete
;
478 void QModelBuilderDefault::reset( FirstOrderModel
* fm
){
479 d_quant_selection_lit
.clear();
480 d_quant_selection_lit_candidates
.clear();
481 d_quant_selection_lit_terms
.clear();
482 d_term_selection_lit
.clear();
483 d_op_selection_terms
.clear();
487 int QModelBuilderDefault::getSelectionScore( std::vector
< Node
>& uf_terms
) {
489 size_t maxChildren = 0;
490 for( size_t i=0; i<uf_terms.size(); i++ ){
491 if( uf_terms[i].getNumChildren()>maxChildren ){
492 maxChildren = uf_terms[i].getNumChildren();
495 //TODO: look at how many entries they have?
496 return (int)maxChildren;
501 void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel
* fm
, Node f
){
502 FirstOrderModelIG
* fmig
= fm
->asFirstOrderModelIG();
503 Debug("fmf-model-prefs") << "Analyze quantifier " << f
<< std::endl
;
504 //the pro/con preferences for this quantifier
505 std::vector
< Node
> pro_con
[2];
506 //the terms in the selection literal we choose
507 std::vector
< Node
> selectionLitTerms
;
508 Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f
<< std::endl
;
509 //for each asserted quantifier f,
510 // - determine selection literals
511 // - check which function/predicates have good and bad definitions for satisfying f
512 int selectLitScore
= -1;
513 QuantPhaseReq
* qpr
= d_qe
->getPhaseRequirements( f
);
514 for( std::map
< Node
, bool >::iterator it
= qpr
->d_phase_reqs
.begin(); it
!= qpr
->d_phase_reqs
.end(); ++it
){
515 //the literal n is phase-required for quantifier f
517 Node gn
= d_qe
->getTermDatabase()->getModelBasis( f
, n
);
518 Debug("fmf-model-req") << " Req: " << n
<< " -> " << it
->second
<< std::endl
;
520 //if the corresponding ground abstraction literal has a SAT value
521 if( d_qe
->getValuation().hasSatValue( gn
, value
) ){
522 //collect the non-ground uf terms that this literal contains
523 // and compute if all of the symbols in this literal have
524 // constant definitions.
526 std::vector
< Node
> uf_terms
;
527 if( TermDb::hasInstConstAttr(n
) ){
529 if( gn
.getKind()==APPLY_UF
){
530 uf_terms
.push_back( gn
);
531 isConst
= hasConstantDefinition( gn
);
532 }else if( gn
.getKind()==EQUAL
){
534 for( int j
=0; j
<2; j
++ ){
535 if( TermDb::hasInstConstAttr(n
[j
]) ){
536 if( n
[j
].getKind()==APPLY_UF
&&
537 fmig
->d_uf_model_tree
.find( gn
[j
].getOperator() )!=fmig
->d_uf_model_tree
.end() ){
538 uf_terms
.push_back( gn
[j
] );
539 isConst
= isConst
&& hasConstantDefinition( gn
[j
] );
547 //check if the value in the SAT solver matches the preference according to the quantifier
549 if( value
!=it
->second
){
550 //we have a possible selection literal
551 bool selectLit
= d_quant_selection_lit
[f
].isNull();
552 bool selectLitConstraints
= true;
553 //it is a constantly defined selection literal : the quantifier is sat
555 selectLit
= selectLit
|| d_quant_sat
.find( f
)==d_quant_sat
.end();
556 d_quant_sat
[f
] = true;
557 //check if choosing this literal would add any additional constraints to default definitions
558 selectLitConstraints
= false;
559 for( int j
=0; j
<(int)uf_terms
.size(); j
++ ){
560 Node op
= uf_terms
[j
].getOperator();
561 if( d_uf_prefs
[op
].d_reconsiderModel
){
562 selectLitConstraints
= true;
565 if( !selectLitConstraints
){
569 //also check if it is naturally a better literal
571 int score
= getSelectionScore( uf_terms
);
572 //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl;
573 selectLit
= score
<selectLitScore
;
575 //see if we wish to choose this as a selection literal
576 d_quant_selection_lit_candidates
[f
].push_back( value
? n
: n
.notNode() );
578 selectLitScore
= getSelectionScore( uf_terms
);
579 Trace("inst-gen-debug") << "Choose selection literal " << gn
<< std::endl
;
580 Trace("inst-gen-debug") << " flags: " << isConst
<< " " << selectLitConstraints
<< " " << selectLitScore
<< std::endl
;
581 d_quant_selection_lit
[f
] = value
? n
: n
.notNode();
582 selectionLitTerms
.clear();
583 selectionLitTerms
.insert( selectionLitTerms
.begin(), uf_terms
.begin(), uf_terms
.end() );
584 if( !selectLitConstraints
){
592 //if we are not yet SAT, so we will add to preferences
593 if( d_quant_sat
.find( f
)==d_quant_sat
.end() ){
594 Debug("fmf-model-prefs") << " It is " << ( pref
==1 ? "pro" : "con" );
595 Debug("fmf-model-prefs") << " the definition of " << n
<< std::endl
;
596 for( int j
=0; j
<(int)uf_terms
.size(); j
++ ){
597 pro_con
[ pref
==1 ? 0 : 1 ].push_back( uf_terms
[j
] );
602 //process information about selection literal for f
603 if( !d_quant_selection_lit
[f
].isNull() ){
604 d_quant_selection_lit_terms
[f
].insert( d_quant_selection_lit_terms
[f
].begin(), selectionLitTerms
.begin(), selectionLitTerms
.end() );
605 for( int i
=0; i
<(int)selectionLitTerms
.size(); i
++ ){
606 d_term_selection_lit
[ selectionLitTerms
[i
] ] = d_quant_selection_lit
[f
];
607 d_op_selection_terms
[ selectionLitTerms
[i
].getOperator() ].push_back( selectionLitTerms
[i
] );
610 Trace("inst-gen-warn") << "WARNING: " << f
<< " has no selection literals" << std::endl
;
612 //process information about requirements and preferences of quantifier f
613 if( d_quant_sat
.find( f
)!=d_quant_sat
.end() ){
614 Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: ";
615 for( int i
=0; i
<(int)selectionLitTerms
.size(); i
++ ){
616 Debug("fmf-model-prefs") << selectionLitTerms
[i
] << " ";
617 d_uf_prefs
[ selectionLitTerms
[i
].getOperator() ].d_reconsiderModel
= false;
619 Debug("fmf-model-prefs") << std::endl
;
621 //note quantifier's value preferences to models
622 for( int k
=0; k
<2; k
++ ){
623 for( int j
=0; j
<(int)pro_con
[k
].size(); j
++ ){
624 Node op
= pro_con
[k
][j
].getOperator();
625 Node r
= fmig
->getRepresentative( pro_con
[k
][j
] );
626 d_uf_prefs
[op
].setValuePreference( f
, pro_con
[k
][j
], r
, k
==0 );
632 int QModelBuilderDefault::doInstGen( FirstOrderModel
* fm
, Node f
){
634 //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
635 //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
636 // effectively acting as partial instantiations instead of pointwise instantiations.
637 if( !d_quant_selection_lit
[f
].isNull() ){
638 Trace("inst-gen") << "Do Inst-Gen for " << f
<< std::endl
;
639 for( size_t i
=0; i
<d_quant_selection_lit_candidates
[f
].size(); i
++ ){
640 bool phase
= d_quant_selection_lit_candidates
[f
][i
].getKind()!=NOT
;
641 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
];
642 Assert( TermDb::hasInstConstAttr(lit
) );
643 std::vector
< Node
> tr_terms
;
644 if( lit
.getKind()==APPLY_UF
){
645 //only match predicates that are contrary to this one, use literal matching
646 Node eq
= NodeManager::currentNM()->mkNode( IFF
, lit
, !phase
? fm
->d_true
: fm
->d_false
);
647 tr_terms
.push_back( eq
);
648 }else if( lit
.getKind()==EQUAL
){
649 //collect trigger terms
650 for( int j
=0; j
<2; j
++ ){
651 if( TermDb::hasInstConstAttr(lit
[j
]) ){
652 if( lit
[j
].getKind()==APPLY_UF
){
653 tr_terms
.push_back( lit
[j
] );
660 if( tr_terms
.size()==1 && !phase
){
661 //equality between a function and a ground term, use literal matching
663 tr_terms
.push_back( lit
);
666 //if applicable, try to add exceptions here
667 if( !tr_terms
.empty() ){
668 //make a trigger for these terms, add instantiations
669 inst::Trigger
* tr
= inst::Trigger::mkTrigger( d_qe
, f
, tr_terms
, 0, true, inst::Trigger::TR_MAKE_NEW
, options::smartTriggers() );
670 //Notice() << "Trigger = " << (*tr) << std::endl;
671 tr
->resetInstantiationRound();
672 tr
->reset( Node::null() );
673 //d_qe->d_optInstMakeRepresentative = false;
674 //d_qe->d_optMatchIgnoreModelBasis = true;
675 addedLemmas
+= tr
->addInstantiations( d_quant_basis_match
[f
] );
682 void QModelBuilderDefault::constructModelUf( FirstOrderModel
* fm
, Node op
){
683 FirstOrderModelIG
* fmig
= fm
->asFirstOrderModelIG();
684 if( optReconsiderFuncConstants() ){
685 //reconsider constant functions that weren't necessary
686 if( d_uf_model_constructed
[op
] ){
687 if( d_uf_prefs
[op
].d_reconsiderModel
){
688 //if we are allowed to reconsider default value, then see if the default value can be improved
689 Node v
= d_uf_prefs
[op
].d_const_val
;
690 if( d_uf_prefs
[op
].d_value_pro_con
[0][v
].empty() ){
691 Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op
<< std::endl
;
692 fmig
->d_uf_model_tree
[op
].clear();
693 fmig
->d_uf_model_gen
[op
].clear();
694 d_uf_model_constructed
[op
] = false;
699 if( !d_uf_model_constructed
[op
] ){
700 //construct the model for the uninterpretted function/predicate
701 bool setDefaultVal
= true;
702 Node defaultTerm
= d_qe
->getTermDatabase()->getModelBasisOpTerm( op
);
703 Trace("fmf-model-cons") << "Construct model for " << op
<< "..." << std::endl
;
704 //set the values in the model
705 for( size_t i
=0; i
<fmig
->d_uf_terms
[op
].size(); i
++ ){
706 Node n
= fmig
->d_uf_terms
[op
][i
];
707 if( isTermActive( n
) ){
708 Node v
= fmig
->getRepresentative( n
);
709 Trace("fmf-model-cons") << "Set term " << n
<< " : " << fmig
->d_rep_set
.getIndexFor( v
) << " " << v
<< std::endl
;
710 //if this assertion did not help the model, just consider it ground
711 //set n = v in the model tree
712 //set it as ground value
713 fmig
->d_uf_model_gen
[op
].setValue( fm
, n
, v
);
714 if( fmig
->d_uf_model_gen
[op
].optUsePartialDefaults() ){
715 //also set as default value if necessary
716 if( n
.hasAttribute(ModelBasisArgAttribute()) && n
.getAttribute(ModelBasisArgAttribute())!=0 ){
717 Trace("fmf-model-cons") << " Set as default." << std::endl
;
718 fmig
->d_uf_model_gen
[op
].setValue( fm
, n
, v
, false );
719 if( n
==defaultTerm
){
720 //incidentally already set, we will not need to find a default value
721 setDefaultVal
= false;
725 if( n
==defaultTerm
){
726 fmig
->d_uf_model_gen
[op
].setValue( fm
, n
, v
, false );
727 //incidentally already set, we will not need to find a default value
728 setDefaultVal
= false;
733 //set the overall default value if not set already (is this necessary??)
735 Trace("fmf-model-cons") << " Choose default value..." << std::endl
;
736 //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
737 Node defaultVal
= d_uf_prefs
[op
].getBestDefaultValue( defaultTerm
, fm
);
738 if( defaultVal
.isNull() ){
739 if (!fmig
->d_rep_set
.hasType(defaultTerm
.getType())) {
740 Node mbt
= d_qe
->getTermDatabase()->getModelBasisTerm(defaultTerm
.getType());
741 fmig
->d_rep_set
.d_type_reps
[defaultTerm
.getType()].push_back(mbt
);
743 defaultVal
= fmig
->d_rep_set
.d_type_reps
[defaultTerm
.getType()][0];
745 Assert( !defaultVal
.isNull() );
746 Trace("fmf-model-cons") << "Set default term : " << fmig
->d_rep_set
.getIndexFor( defaultVal
) << std::endl
;
747 fmig
->d_uf_model_gen
[op
].setValue( fm
, defaultTerm
, defaultVal
, false );
749 Debug("fmf-model-cons") << " Making model...";
750 fmig
->d_uf_model_gen
[op
].makeModel( fm
, fmig
->d_uf_model_tree
[op
] );
751 d_uf_model_constructed
[op
] = true;
752 Debug("fmf-model-cons") << " Finished constructing model for " << op
<< "." << std::endl
;
759 ////////////////////// Inst-Gen style Model Builder ///////////
761 void QModelBuilderInstGen::reset( FirstOrderModel
* fm
){
763 d_quant_selection_formula
.clear();
764 d_term_selected
.clear();
766 //d_sub_quant_inst_trie.clear();//*
769 int QModelBuilderInstGen::initializeQuantifier( Node f
, Node fp
){
770 int addedLemmas
= QModelBuilderIG::initializeQuantifier( f
, fp
);
771 for( size_t i
=0; i
<d_sub_quants
[f
].size(); i
++ ){
772 addedLemmas
+= initializeQuantifier( d_sub_quants
[f
][i
], fp
);
777 void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel
* fm
, Node f
){
778 //Node fp = getParentQuantifier( f );//*
779 //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) );
780 //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//*
781 Trace("sel-form-debug") << "* Analyze " << f
<< std::endl
;
782 //determine selection formula, set terms in selection formula as being selected
783 Node s
= getSelectionFormula( d_qe
->getTermDatabase()->getInstConstantBody( f
),
784 d_qe
->getTermDatabase()->getModelBasisBody( f
), true, 0 );
786 // s = Rewriter::rewrite( s );
788 Trace("sel-form-debug") << "Selection formula " << f
<< std::endl
;
789 Trace("sel-form-debug") << " " << s
<< std::endl
;
791 d_quant_selection_formula
[f
] = s
;
792 Node gs
= d_qe
->getTermDatabase()->getModelBasis( f
, s
);
793 setSelectedTerms( gs
);
794 //quick check if it is constant sat
795 if( hasConstantDefinition( s
) ){
796 d_quant_sat
[f
] = true;
799 Trace("sel-form-null") << "*** No selection formula for " << f
<< std::endl
;
801 //analyze sub quantifiers
802 if( d_quant_sat
.find( f
)==d_quant_sat
.end() ){
803 for( size_t i
=0; i
<d_sub_quants
[f
].size(); i
++ ){
804 analyzeQuantifier( fm
, d_sub_quants
[f
][i
] );
810 int QModelBuilderInstGen::doInstGen( FirstOrderModel
* fm
, Node f
){
812 if( d_quant_sat
.find( f
)==d_quant_sat
.end() ){
813 Node fp
= d_sub_quant_parent
.find( f
)==d_sub_quant_parent
.end() ? f
: d_sub_quant_parent
[f
];
814 if( fp
!=f
) Trace("inst-gen") << " ";
815 Trace("inst-gen") << "Do Inst-Gen for " << f
<< std::endl
;
816 if( fp
!=f
) Trace("inst-gen") << " ";
817 Trace("inst-gen") << "Sel Form : " << d_quant_selection_formula
[f
] << std::endl
;
818 //we wish to add all known exceptions to our selection formula for f. this will help to refine our current model.
819 if( !d_quant_selection_formula
[f
].isNull() ){
820 //first, try on sub quantifiers
821 bool subQuantSat
= true;
822 for( size_t i
=0; i
<d_sub_quants
[f
].size(); i
++ ){
823 addedLemmas
+= doInstGen( fm
, d_sub_quants
[f
][i
] );
824 if( d_quant_sat
.find( d_sub_quants
[f
][i
] )==d_quant_sat
.end() ){
828 if( addedLemmas
>0 || !subQuantSat
){
829 Trace("inst-gen") << " -> children added lemmas or non-satisfied" << std::endl
;
832 Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl
;
833 //get all possible values of selection formula
834 InstGenProcess
igp( d_quant_selection_formula
[f
] );
835 std::vector
< Node
> considered
;
836 considered
.push_back( fm
->d_false
);
837 igp
.calculateMatches( d_qe
, f
, considered
, true );
838 //igp.calculateMatches( d_qe, f);
839 Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp
.getNumMatches() << ")..." << std::endl
;
840 for( int i
=0; i
<igp
.getNumMatches(); i
++ ){
841 //if the match is not already true in the model
842 if( igp
.getMatchValue( i
)!=fm
->d_true
){
844 igp
.getMatch( d_qe
->getEqualityQuery(), i
, m
);
845 //Trace("inst-gen-debug") << "Inst Gen : " << m << std::endl;
846 //we only consider matches that are non-empty
847 // matches that are empty should trigger other instances that are non-empty
849 Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl
;
850 //translate to be in terms match in terms of fp
852 getParentQuantifierMatch( mp
, fp
, m
, f
);
853 //if this is a partial instantion
854 if( !m
.isComplete() ){
855 //need to make it internal here
856 //Trace("mkInternal") << "Make internal representative " << mp << std::endl;
857 //mp.makeInternalRepresentative( d_qe );
858 //Trace("mkInternal") << "Got " << mp << std::endl;
859 //if the instantiation does not yet exist
860 if( d_sub_quant_inst_trie
[fp
].addInstMatch( d_qe
, fp
, mp
, true ) ){
861 //also add it to children
862 d_child_sub_quant_inst_trie
[f
].addInstMatch( d_qe
, f
, m
);
863 //get the partial instantiation pf
864 Node pf
= d_qe
->getInstantiation( fp
, mp
);
865 Trace("inst-gen-pi") << "Partial instantiation of " << f
<< std::endl
;
866 Trace("inst-gen-pi") << " " << pf
<< std::endl
;
867 d_sub_quants
[ f
].push_back( pf
);
868 d_sub_quant_inst
[ pf
] = InstMatch( &mp
);
869 d_sub_quant_parent
[ pf
] = fp
;
870 //now make mp a complete match
871 mp
.add( d_quant_basis_match
[ fp
] );
872 d_quant_basis_match
[ pf
] = InstMatch( &mp
);
873 ++(d_statistics
.d_num_quants_init
);
874 ++(d_statistics
.d_num_partial_quants_init
);
875 addedLemmas
+= initializeQuantifier( pf
, fp
);
876 Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl
;
880 if( d_qe
->addInstantiation( fp
, mp
) ){
887 if( addedLemmas
==0 ){
888 //all sub quantifiers must be satisfied as well
890 d_quant_sat
[ f
] = true;
893 if( fp
!=f
) Trace("inst-gen") << " ";
894 Trace("inst-gen") << " -> added lemmas = " << addedLemmas
<< std::endl
;
895 if( d_quant_sat
.find( f
)!=d_quant_sat
.end() ){
896 if( fp
!=f
) Trace("inst-gen") << " ";
897 Trace("inst-gen") << " -> *** it is satisfied" << std::endl
;
905 Node
mkAndSelectionFormula( std::vector
< Node
>& children
){
906 std::vector
< Node
> ch
;
907 for( size_t i
=0; i
<children
.size(); i
++ ){
908 if( children
[i
].getKind()==AND
){
909 for( size_t j
=0; j
<children
[i
].getNumChildren(); j
++ ){
910 ch
.push_back( children
[i
][j
] );
913 ch
.push_back( children
[i
] );
916 return NodeManager::currentNM()->mkNode( AND
, ch
);
918 Node
mkAndSelectionFormula( Node n1
, Node n2
){
919 std::vector
< Node
> children
;
920 children
.push_back( n1
);
921 children
.push_back( n2
);
922 return mkAndSelectionFormula( children
);
925 //if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context,
926 // and NULL otherwise
927 Node
QModelBuilderInstGen::getSelectionFormula( Node fn
, Node n
, bool polarity
, int useOption
){
928 Trace("sel-form-debug") << "Looking for selection formula " << n
<< " " << polarity
<< std::endl
;
930 if( n
.getKind()==NOT
){
931 ret
= getSelectionFormula( fn
[0], n
[0], !polarity
, useOption
);
932 }else if( n
.getKind()==OR
|| n
.getKind()==AND
){
933 //whether we only need to find one or all
934 bool favorPol
= ( n
.getKind()!=AND
&& polarity
) || ( n
.getKind()==AND
&& !polarity
);
935 std::vector
< Node
> children
;
936 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
939 Node nn
= getSelectionFormula( fnc
, nc
, polarity
, useOption
);
940 if( nn
.isNull() && !favorPol
){
941 //cannot make selection formula
946 //if( favorPol ){ //temporary
949 if( std::find( children
.begin(), children
.end(), nn
)==children
.end() ){
950 children
.push_back( nn
);
954 if( !children
.empty() ){
956 //filter which formulas we wish to keep, make disjunction
959 for( size_t i
=0; i
<children
.size(); i
++ ){
960 //if it is constant apply uf application, return it for sure
961 if( hasConstantDefinition( children
[i
] ) ){
962 min_lit
= children
[i
];
965 int score
= getSelectionFormulaScore( children
[i
] );
966 if( min_score
<0 || score
<min_score
){
968 min_lit
= children
[i
];
972 //currently just return the best single literal
975 //selection formula must be conjunction of children
976 ret
= mkAndSelectionFormula( children
);
981 }else if( n
.getKind()==ITE
){
984 //get selection formula for the
985 for( int i
=0; i
<2; i
++ ){
986 nn
= getSelectionFormula( fn
[0], n
[0], i
==0, useOption
);
987 nc
[i
] = getSelectionFormula( fn
[i
+1], n
[i
+1], polarity
, useOption
);
988 if( !nn
.isNull() && !nc
[i
].isNull() ){
989 ret
= mkAndSelectionFormula( nn
, nc
[i
] );
993 if( ret
.isNull() && !nc
[0].isNull() && !nc
[1].isNull() ){
994 ret
= mkAndSelectionFormula( nc
[0], nc
[1] );
996 }else if( n
.getKind()==IFF
){
997 bool opPol
= !polarity
;
998 for( int p
=0; p
<2; p
++ ){
1000 for( int i
=0; i
<2; i
++ ){
1001 bool pol
= i
==0 ? p
==0 : ( opPol
? p
!=0 : p
==0 );
1002 nn
[i
] = getSelectionFormula( fn
[i
], n
[i
], pol
, useOption
);
1003 if( nn
[i
].isNull() ){
1007 if( !nn
[0].isNull() && !nn
[1].isNull() ){
1008 ret
= mkAndSelectionFormula( nn
[0], nn
[1] );
1013 //first, check if it is a usable selection literal
1014 if( isUsableSelectionLiteral( n
, useOption
) ){
1016 if( d_qe
->getValuation().hasSatValue( n
, value
) ){
1017 if( value
==polarity
){
1023 Trace("sel-form-debug") << " (wrong polarity)" << std::endl
;
1026 Trace("sel-form-debug") << " (does not have sat value)" << std::endl
;
1029 Trace("sel-form-debug") << " (is not usable literal)" << std::endl
;
1032 Trace("sel-form-debug") << " return " << ret
<< std::endl
;
1036 int QModelBuilderInstGen::getSelectionFormulaScore( Node fn
){
1037 if( fn
.getType().isBoolean() ){
1038 if( fn
.getKind()==APPLY_UF
){
1039 Node op
= fn
.getOperator();
1040 //return total number of terms
1041 return d_qe
->getTermDatabase()->d_op_nonred_count
[op
];
1044 for( size_t i
=0; i
<fn
.getNumChildren(); i
++ ){
1045 score
+= getSelectionFormulaScore( fn
[i
] );
1054 void QModelBuilderInstGen::setSelectedTerms( Node s
){
1056 //if it is apply uf and has model basis arguments, then mark term as being "selected"
1057 if( s
.getKind()==APPLY_UF
){
1058 Assert( s
.hasAttribute(ModelBasisArgAttribute()) );
1059 if( !s
.hasAttribute(ModelBasisArgAttribute()) ) std::cout
<< "no mba!! " << s
<< std::endl
;
1060 if( s
.getAttribute(ModelBasisArgAttribute())!=0 ){
1061 d_term_selected
[ s
] = true;
1062 Trace("sel-form-term") << " " << s
<< " is a selected term." << std::endl
;
1065 for( int i
=0; i
<(int)s
.getNumChildren(); i
++ ){
1066 setSelectedTerms( s
[i
] );
1070 bool QModelBuilderInstGen::isUsableSelectionLiteral( Node n
, int useOption
){
1071 if( n
.getKind()==FORALL
){
1073 }else if( n
.getKind()!=APPLY_UF
){
1074 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
1075 //if it is a variable, then return false
1076 if( n
[i
].getAttribute(ModelBasisAttribute()) ){
1081 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
1082 if( !isUsableSelectionLiteral( n
[i
], useOption
) ){
1089 void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch
& mp
, Node fp
, InstMatch
& m
, Node f
){
1091 //std::cout << "gpqm " << fp << " " << f << " " << m << std::endl;
1092 //std::cout << " " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl;
1094 for( size_t i
=0; i
<fp
[0].getNumChildren(); i
++ ){
1095 if( (int)counter
< (int)f
[0].getNumChildren() ){
1096 if( fp
[0][i
]==f
[0][counter
] ){
1097 Node n
= m
.get( counter
);
1099 mp
.set( d_qe
, i
, n
);
1105 mp
.add( d_sub_quant_inst
[f
] );
1111 void QModelBuilderInstGen::constructModelUf( FirstOrderModel
* fm
, Node op
){
1112 FirstOrderModelIG
* fmig
= fm
->asFirstOrderModelIG();
1113 bool setDefaultVal
= true;
1114 Node defaultTerm
= d_qe
->getTermDatabase()->getModelBasisOpTerm( op
);
1115 //set the values in the model
1116 for( size_t i
=0; i
<fmig
->d_uf_terms
[op
].size(); i
++ ){
1117 Node n
= fmig
->d_uf_terms
[op
][i
];
1118 if( isTermActive( n
) ){
1119 Node v
= fmig
->getRepresentative( n
);
1120 fmig
->d_uf_model_gen
[op
].setValue( fm
, n
, v
);
1122 //also possible set as default
1123 if( d_term_selected
.find( n
)!=d_term_selected
.end() || n
==defaultTerm
){
1124 Node v
= fmig
->getRepresentative( n
);
1125 fmig
->d_uf_model_gen
[op
].setValue( fm
, n
, v
, false );
1126 if( n
==defaultTerm
){
1127 setDefaultVal
= false;
1131 //set the overall default value if not set already (is this necessary??)
1132 if( setDefaultVal
){
1133 Node defaultVal
= d_uf_prefs
[op
].getBestDefaultValue( defaultTerm
, fm
);
1134 fmig
->d_uf_model_gen
[op
].setValue( fm
, defaultTerm
, defaultVal
, false );
1136 fmig
->d_uf_model_gen
[op
].makeModel( fm
, fmig
->d_uf_model_tree
[op
] );
1137 d_uf_model_constructed
[op
] = true;
1140 bool QModelBuilderInstGen::existsInstantiation( Node f
, InstMatch
& m
, bool modEq
, bool modInst
){
1141 return d_child_sub_quant_inst_trie
[f
].existsInstMatch( d_qe
, f
, m
, modEq
, true );