1 /********************* */
2 /*! \file theory_model.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Clark Barrett, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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 class
14 #include "theory/theory_model.h"
16 #include "expr/node_algorithm.h"
17 #include "options/quantifiers_options.h"
18 #include "options/smt_options.h"
19 #include "options/uf_options.h"
20 #include "smt/smt_engine.h"
23 using namespace CVC4::kind
;
24 using namespace CVC4::context
;
29 TheoryModel::TheoryModel(context::Context
* c
,
31 bool enableFuncModels
)
33 d_substitutions(c
, false),
34 d_equalityEngine(nullptr),
35 d_using_model_core(false),
36 d_enableFuncModels(enableFuncModels
)
38 // must use function models when ufHo is enabled
39 Assert(d_enableFuncModels
|| !options::ufHo());
40 d_true
= NodeManager::currentNM()->mkConst( true );
41 d_false
= NodeManager::currentNM()->mkConst( false );
44 TheoryModel::~TheoryModel() {}
46 void TheoryModel::setEqualityEngine(eq::EqualityEngine
* ee
)
48 d_equalityEngine
= ee
;
51 bool TheoryModel::needsEqualityEngine(EeSetupInfo
& esi
)
55 esi
.d_constantsAreTriggers
= false;
59 void TheoryModel::finishInit()
61 Assert(d_equalityEngine
!= nullptr);
62 // The kinds we are treating as function application in congruence
63 d_equalityEngine
->addFunctionKind(kind::APPLY_UF
, false, options::ufHo());
64 d_equalityEngine
->addFunctionKind(kind::HO_APPLY
);
65 d_equalityEngine
->addFunctionKind(kind::SELECT
);
66 // d_equalityEngine->addFunctionKind(kind::STORE);
67 d_equalityEngine
->addFunctionKind(kind::APPLY_CONSTRUCTOR
);
68 d_equalityEngine
->addFunctionKind(kind::APPLY_SELECTOR_TOTAL
);
69 d_equalityEngine
->addFunctionKind(kind::APPLY_TESTER
);
70 // do not interpret APPLY_UF if we are not assigning function values
71 if (!d_enableFuncModels
)
73 setSemiEvaluatedKind(kind::APPLY_UF
);
77 void TheoryModel::reset(){
79 d_modelBuiltSuccess
= false;
81 d_comment_str
.clear();
82 d_sep_heap
= Node::null();
83 d_sep_nil_eq
= Node::null();
84 d_approximations
.clear();
85 d_approx_list
.clear();
87 d_assignExcSet
.clear();
92 d_ho_uf_terms
.clear();
94 d_using_model_core
= false;
98 void TheoryModel::getComments(std::ostream
& out
) const {
99 Trace("model-builder") << "get comments..." << std::endl
;
100 out
<< d_comment_str
.str();
103 void TheoryModel::setHeapModel( Node h
, Node neq
) {
108 bool TheoryModel::getHeapModel( Expr
& h
, Expr
& neq
) const {
109 if( d_sep_heap
.isNull() || d_sep_nil_eq
.isNull() ){
112 h
= d_sep_heap
.toExpr();
113 neq
= d_sep_nil_eq
.toExpr();
118 bool TheoryModel::hasApproximations() const { return !d_approx_list
.empty(); }
120 std::vector
<std::pair
<Expr
, Expr
> > TheoryModel::getApproximations() const
122 std::vector
<std::pair
<Expr
, Expr
> > approx
;
123 for (const std::pair
<Node
, Node
>& ap
: d_approx_list
)
126 std::pair
<Expr
, Expr
>(ap
.first
.toExpr(), ap
.second
.toExpr()));
131 std::vector
<Expr
> TheoryModel::getDomainElements(Type t
) const
133 // must be an uninterpreted sort
135 std::vector
<Expr
> elements
;
136 TypeNode tn
= TypeNode::fromType(t
);
137 const std::vector
<Node
>* type_refs
= d_rep_set
.getTypeRepsOrNull(tn
);
138 if (type_refs
== nullptr || type_refs
->empty())
140 // This is called when t is a sort that does not occur in this model.
141 // Sorts are always interpreted as non-empty, thus we add a single element.
142 elements
.push_back(t
.mkGroundTerm());
145 for (const Node
& n
: *type_refs
)
147 elements
.push_back(n
.toExpr());
152 Node
TheoryModel::getValue(TNode n
) const
154 //apply substitutions
155 Node nn
= d_substitutions
.apply(n
);
156 Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n
<< " to " << nn
<< std::endl
;
158 nn
= getModelValue(nn
);
159 if (nn
.isNull()) return nn
;
160 if(options::condenseFunctionValues() || nn
.getKind() != kind::LAMBDA
) {
162 nn
= Rewriter::rewrite(nn
);
164 Debug("model-getvalue") << "[model-getvalue] getValue( " << n
<< " ): " << std::endl
165 << "[model-getvalue] returning " << nn
<< std::endl
;
169 bool TheoryModel::isModelCoreSymbol(Expr sym
) const
171 if (!d_using_model_core
)
175 Node s
= Node::fromExpr(sym
);
176 Assert(s
.isVar() && s
.getKind() != BOUND_VARIABLE
);
177 return d_model_core
.find(s
) != d_model_core
.end();
180 Expr
TheoryModel::getValue( Expr expr
) const{
181 Node n
= Node::fromExpr( expr
);
182 Node ret
= getValue( n
);
186 /** get cardinality for sort */
187 Cardinality
TheoryModel::getCardinality( Type t
) const{
188 TypeNode tn
= TypeNode::fromType( t
);
189 //for now, we only handle cardinalities for uninterpreted sorts
191 if( d_rep_set
.hasType( tn
) ){
192 Debug("model-getvalue-debug") << "Get cardinality sort, #rep : " << d_rep_set
.getNumRepresentatives( tn
) << std::endl
;
193 return Cardinality( d_rep_set
.getNumRepresentatives( tn
) );
195 Debug("model-getvalue-debug") << "Get cardinality sort, unconstrained, return 1." << std::endl
;
196 return Cardinality( 1 );
199 Debug("model-getvalue-debug") << "Get cardinality other sort, unknown." << std::endl
;
200 return Cardinality( CardinalityUnknown() );
204 Node
TheoryModel::getModelValue(TNode n
) const
206 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator it
= d_modelCache
.find(n
);
207 if (it
!= d_modelCache
.end()) {
210 Debug("model-getvalue-debug") << "Get model value " << n
<< " ... ";
211 Debug("model-getvalue-debug") << d_equalityEngine
->hasTerm(n
) << std::endl
;
212 Kind nk
= n
.getKind();
213 if (n
.isConst() || nk
== BOUND_VARIABLE
)
220 NodeManager
* nm
= NodeManager::currentNM();
222 // if it is an evaluated kind, compute model values for children and evaluate
223 if (n
.getNumChildren() > 0
224 && d_unevaluated_kinds
.find(nk
) == d_unevaluated_kinds
.end()
225 && d_semi_evaluated_kinds
.find(nk
) == d_semi_evaluated_kinds
.end())
227 Debug("model-getvalue-debug")
228 << "Get model value children " << n
<< std::endl
;
229 std::vector
<Node
> children
;
230 if (n
.getKind() == APPLY_UF
)
232 Node op
= getModelValue(n
.getOperator());
233 Debug("model-getvalue-debug") << " operator : " << op
<< std::endl
;
234 children
.push_back(op
);
236 else if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
)
238 children
.push_back(n
.getOperator());
240 // evaluate the children
241 for (unsigned i
= 0, nchild
= n
.getNumChildren(); i
< nchild
; ++i
)
243 ret
= getModelValue(n
[i
]);
244 Debug("model-getvalue-debug")
245 << " " << n
<< "[" << i
<< "] is " << ret
<< std::endl
;
246 children
.push_back(ret
);
248 ret
= nm
->mkNode(n
.getKind(), children
);
249 Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret
<< std::endl
;
250 ret
= Rewriter::rewrite(ret
);
251 Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret
<< std::endl
;
253 if (ret
.getKind() == kind::CARDINALITY_CONSTRAINT
)
255 Debug("model-getvalue-debug")
256 << "get cardinality constraint " << ret
[0].getType() << std::endl
;
258 getCardinality(ret
[0].getType().toType()).getFiniteCardinality()
259 <= ret
[1].getConst
<Rational
>().getNumerator());
261 else if (ret
.getKind() == kind::CARDINALITY_VALUE
)
263 Debug("model-getvalue-debug")
264 << "get cardinality value " << ret
[0].getType() << std::endl
;
265 ret
= nm
->mkConst(Rational(
266 getCardinality(ret
[0].getType().toType()).getFiniteCardinality()));
268 d_modelCache
[n
] = ret
;
271 // it might be approximate
272 std::map
<Node
, Node
>::const_iterator ita
= d_approximations
.find(n
);
273 if (ita
!= d_approximations
.end())
275 // If the value of n is approximate based on predicate P(n), we return
277 Node v
= nm
->mkBoundVar(n
.getType());
278 Node bvl
= nm
->mkNode(BOUND_VAR_LIST
, v
);
279 Node answer
= nm
->mkNode(WITNESS
, bvl
, ita
->second
.substitute(n
, v
));
280 d_modelCache
[n
] = answer
;
283 // must rewrite the term at this point
284 ret
= Rewriter::rewrite(n
);
285 // return the representative of the term in the equality engine, if it exists
286 TypeNode t
= ret
.getType();
288 if (!options::ufHo() && (t
.isFunction() || t
.isPredicate()))
290 // functions are in the equality engine, but *not* as first-class members
291 // when higher-order is disabled. In this case, we cannot query
292 // representatives for functions since they are "internal" nodes according
293 // to the equality engine despite hasTerm returning true. However, they are
294 // first class members when higher-order is enabled. Hence, the special
300 eeHasTerm
= d_equalityEngine
->hasTerm(ret
);
304 Debug("model-getvalue-debug")
305 << "get value from representative " << ret
<< "..." << std::endl
;
306 ret
= d_equalityEngine
->getRepresentative(ret
);
307 Assert(d_reps
.find(ret
) != d_reps
.end());
308 std::map
<Node
, Node
>::const_iterator it2
= d_reps
.find(ret
);
309 if (it2
!= d_reps
.end())
312 d_modelCache
[n
] = ret
;
317 // if we are a evaluated or semi-evaluated kind, return an arbitrary value
318 // if we are not in the d_unevaluated_kinds map, we are evaluated
319 if (d_unevaluated_kinds
.find(nk
) == d_unevaluated_kinds
.end())
321 if (t
.isFunction() || t
.isPredicate())
323 if (d_enableFuncModels
)
325 std::map
<Node
, Node
>::const_iterator entry
= d_uf_models
.find(n
);
326 if (entry
!= d_uf_models
.end())
330 d_modelCache
[n
] = ret
;
333 // Unknown function symbol: return LAMBDA x. c, where c is the first
334 // constant in the enumeration of the range type
335 vector
<TypeNode
> argTypes
= t
.getArgTypes();
337 for (unsigned i
= 0, size
= argTypes
.size(); i
< size
; ++i
)
339 args
.push_back(nm
->mkBoundVar(argTypes
[i
]));
341 Node boundVarList
= nm
->mkNode(kind::BOUND_VAR_LIST
, args
);
342 TypeEnumerator
te(t
.getRangeType());
343 ret
= nm
->mkNode(kind::LAMBDA
, boundVarList
, *te
);
347 // if func models not enabled, throw an error
351 else if (!t
.isFirstClass())
353 // this is the class for regular expressions
354 // we simply invoke the rewriter on them
355 ret
= Rewriter::rewrite(ret
);
359 // Unknown term - return first enumerated value for this type
360 TypeEnumerator
te(n
.getType());
363 d_modelCache
[n
] = ret
;
371 /** add substitution */
372 void TheoryModel::addSubstitution( TNode x
, TNode t
, bool invalidateCache
){
373 if( !d_substitutions
.hasSubstitution( x
) ){
374 Debug("model") << "Add substitution in model " << x
<< " -> " << t
<< std::endl
;
375 d_substitutions
.addSubstitution( x
, t
, invalidateCache
);
377 #ifdef CVC4_ASSERTIONS
378 Node oldX
= d_substitutions
.getSubstitution(x
);
379 // check that either the old substitution is the same, or it now maps to the new substitution
380 if(oldX
!= t
&& d_substitutions
.apply(oldX
) != d_substitutions
.apply(t
)) {
382 << "Two incompatible substitutions added to TheoryModel:\n"
383 << "the term: " << x
<< "\n"
384 << "old mapping: " << d_substitutions
.apply(oldX
) << "\n"
385 << "new mapping: " << d_substitutions
.apply(t
);
387 #endif /* CVC4_ASSERTIONS */
392 void TheoryModel::addTermInternal(TNode n
)
394 Assert(d_equalityEngine
->hasTerm(n
));
395 Trace("model-builder-debug2") << "TheoryModel::addTerm : " << n
<< std::endl
;
396 //must collect UF terms
397 if (n
.getKind()==APPLY_UF
) {
398 Node op
= n
.getOperator();
399 if( std::find( d_uf_terms
[ op
].begin(), d_uf_terms
[ op
].end(), n
)==d_uf_terms
[ op
].end() ){
400 d_uf_terms
[ op
].push_back( n
);
401 Trace("model-builder-fun") << "Add apply term " << n
<< std::endl
;
403 }else if( n
.getKind()==HO_APPLY
){
405 if( std::find( d_ho_uf_terms
[ op
].begin(), d_ho_uf_terms
[ op
].end(), n
)==d_ho_uf_terms
[ op
].end() ){
406 d_ho_uf_terms
[ op
].push_back( n
);
407 Trace("model-builder-fun") << "Add ho apply term " << n
<< std::endl
;
410 // all functions must be included, marked as higher-order
411 if( n
.getType().isFunction() ){
412 Trace("model-builder-fun") << "Add function variable (without term) " << n
<< std::endl
;
413 if( d_uf_terms
.find( n
)==d_uf_terms
.end() ){
414 d_uf_terms
[n
].clear();
416 if( d_ho_uf_terms
.find( n
)==d_ho_uf_terms
.end() ){
417 d_ho_uf_terms
[n
].clear();
422 /** assert equality */
423 bool TheoryModel::assertEquality(TNode a
, TNode b
, bool polarity
)
425 Assert(d_equalityEngine
->consistent());
426 if (a
== b
&& polarity
) {
429 Trace("model-builder-assertions") << "(assert " << (polarity
? "(= " : "(not (= ") << a
<< " " << b
<< (polarity
? "));" : ")));") << endl
;
430 d_equalityEngine
->assertEquality( a
.eqNode(b
), polarity
, Node::null() );
431 return d_equalityEngine
->consistent();
434 /** assert predicate */
435 bool TheoryModel::assertPredicate(TNode a
, bool polarity
)
437 Assert(d_equalityEngine
->consistent());
438 if ((a
== d_true
&& polarity
) ||
439 (a
== d_false
&& (!polarity
))) {
442 if (a
.getKind() == EQUAL
) {
443 Trace("model-builder-assertions") << "(assert " << (polarity
? " " : "(not ") << a
<< (polarity
? ");" : "));") << endl
;
444 d_equalityEngine
->assertEquality( a
, polarity
, Node::null() );
446 Trace("model-builder-assertions") << "(assert " << (polarity
? "" : "(not ") << a
<< (polarity
? ");" : "));") << endl
;
447 d_equalityEngine
->assertPredicate( a
, polarity
, Node::null() );
449 return d_equalityEngine
->consistent();
452 /** assert equality engine */
453 bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine
* ee
,
456 Assert(d_equalityEngine
->consistent());
457 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
458 for (; !eqcs_i
.isFinished(); ++eqcs_i
) {
459 Node eqc
= (*eqcs_i
);
460 bool predicate
= false;
461 bool predTrue
= false;
462 bool predFalse
= false;
463 Trace("model-builder-debug") << "...asserting terms in equivalence class " << eqc
;
464 if (eqc
.getType().isBoolean()) {
466 predTrue
= ee
->areEqual(eqc
, d_true
);
467 predFalse
= ee
->areEqual(eqc
, d_false
);
468 Trace("model-builder-debug") << ", pred = " << predTrue
<< "/" << predFalse
;
470 Trace("model-builder-debug") << std::endl
;
471 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, ee
);
474 for (; !eqc_i
.isFinished(); ++eqc_i
) {
475 if (termSet
!= NULL
&& termSet
->find(*eqc_i
) == termSet
->end()) {
476 Trace("model-builder-debug") << "...skip node " << (*eqc_i
) << " in eqc " << eqc
<< std::endl
;
480 if (predTrue
|| predFalse
)
482 if (!assertPredicate(*eqc_i
, predTrue
))
493 Node eq
= (*eqc_i
).eqNode(rep
);
494 Trace("model-builder-assertions")
495 << "(assert " << eq
<< ");" << std::endl
;
496 d_equalityEngine
->assertEquality(eq
, true, Node::null());
497 if (!d_equalityEngine
->consistent())
506 //add the term (this is specifically for the case of singleton equivalence classes)
507 if (rep
.getType().isFirstClass())
509 d_equalityEngine
->addTerm( rep
);
510 Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep
<< std::endl
;
515 if (!assertEquality(*eqc_i
, rep
, true))
526 void TheoryModel::assertSkeleton(TNode n
)
528 Trace("model-builder-reps") << "Assert skeleton : " << n
<< std::endl
;
529 Trace("model-builder-reps") << "...rep eqc is : " << getRepresentative(n
)
534 void TheoryModel::setAssignmentExclusionSet(TNode n
,
535 const std::vector
<Node
>& eset
)
537 // should not be assigned yet
538 Assert(d_assignExcSet
.find(n
) == d_assignExcSet
.end());
539 Trace("model-builder-debug")
540 << "Exclude values of " << n
<< " : " << eset
<< std::endl
;
541 std::vector
<Node
>& aes
= d_assignExcSet
[n
];
542 aes
.insert(aes
.end(), eset
.begin(), eset
.end());
545 void TheoryModel::setAssignmentExclusionSetGroup(
546 const std::vector
<TNode
>& group
, const std::vector
<Node
>& eset
)
552 // for efficiency, we store a single copy of eset and set a slave/master
554 setAssignmentExclusionSet(group
[0], eset
);
555 std::vector
<Node
>& gslaves
= d_aesSlaves
[group
[0]];
556 for (unsigned i
= 1, gsize
= group
.size(); i
< gsize
; ++i
)
560 d_aesMaster
[gs
] = group
[0];
562 gslaves
.push_back(gs
);
566 bool TheoryModel::getAssignmentExclusionSet(TNode n
,
567 std::vector
<Node
>& group
,
568 std::vector
<Node
>& eset
)
570 // does it have a master?
571 std::map
<Node
, Node
>::iterator itm
= d_aesMaster
.find(n
);
572 if (itm
!= d_aesMaster
.end())
574 return getAssignmentExclusionSet(itm
->second
, group
, eset
);
576 std::map
<Node
, std::vector
<Node
> >::iterator ita
= d_assignExcSet
.find(n
);
577 if (ita
== d_assignExcSet
.end())
581 eset
.insert(eset
.end(), ita
->second
.begin(), ita
->second
.end());
583 // does it have slaves?
584 ita
= d_aesSlaves
.find(n
);
585 if (ita
!= d_aesSlaves
.end())
587 group
.insert(group
.end(), ita
->second
.begin(), ita
->second
.end());
592 bool TheoryModel::hasAssignmentExclusionSets() const
594 return !d_assignExcSet
.empty();
597 void TheoryModel::recordApproximation(TNode n
, TNode pred
)
599 Trace("model-builder-debug")
600 << "Record approximation : " << n
<< " satisfies the predicate " << pred
602 Assert(d_approximations
.find(n
) == d_approximations
.end());
603 Assert(pred
.getType().isBoolean());
604 d_approximations
[n
] = pred
;
605 d_approx_list
.push_back(std::pair
<Node
, Node
>(n
, pred
));
606 // model cache is invalid
607 d_modelCache
.clear();
609 void TheoryModel::recordApproximation(TNode n
, TNode pred
, Node witness
)
611 Node predDisj
= NodeManager::currentNM()->mkNode(OR
, n
.eqNode(witness
), pred
);
612 recordApproximation(n
, predDisj
);
614 void TheoryModel::setUsingModelCore()
616 d_using_model_core
= true;
617 d_model_core
.clear();
620 void TheoryModel::recordModelCoreSymbol(Expr sym
)
622 d_model_core
.insert(Node::fromExpr(sym
));
625 void TheoryModel::setUnevaluatedKind(Kind k
) { d_unevaluated_kinds
.insert(k
); }
627 void TheoryModel::setSemiEvaluatedKind(Kind k
)
629 d_semi_evaluated_kinds
.insert(k
);
632 bool TheoryModel::isLegalElimination(TNode x
, TNode val
)
634 return !expr::hasSubtermKinds(d_unevaluated_kinds
, val
);
637 bool TheoryModel::hasTerm(TNode a
)
639 return d_equalityEngine
->hasTerm( a
);
642 Node
TheoryModel::getRepresentative(TNode a
)
644 if( d_equalityEngine
->hasTerm( a
) ){
645 Node r
= d_equalityEngine
->getRepresentative( a
);
646 if( d_reps
.find( r
)!=d_reps
.end() ){
656 bool TheoryModel::areEqual(TNode a
, TNode b
)
660 }else if( d_equalityEngine
->hasTerm( a
) && d_equalityEngine
->hasTerm( b
) ){
661 return d_equalityEngine
->areEqual( a
, b
);
667 bool TheoryModel::areDisequal(TNode a
, TNode b
)
669 if( d_equalityEngine
->hasTerm( a
) && d_equalityEngine
->hasTerm( b
) ){
670 return d_equalityEngine
->areDisequal( a
, b
, false );
676 bool TheoryModel::areFunctionValuesEnabled() const
678 return d_enableFuncModels
;
681 void TheoryModel::assignFunctionDefinition( Node f
, Node f_def
) {
682 Trace("model-builder") << " Assigning function (" << f
<< ") to (" << f_def
<< ")" << endl
;
683 Assert(d_uf_models
.find(f
) == d_uf_models
.end());
685 if( options::ufHo() ){
686 //we must rewrite the function value since the definition needs to be a constant value
687 f_def
= Rewriter::rewrite( f_def
);
688 Trace("model-builder-debug")
689 << "Model value (post-rewrite) : " << f_def
<< std::endl
;
690 Assert(f_def
.isConst()) << "Non-constant f_def: " << f_def
;
693 // d_uf_models only stores models for variables
695 d_uf_models
[f
] = f_def
;
698 if (options::ufHo() && d_equalityEngine
->hasTerm(f
))
700 Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl
;
701 // assign to representative if higher-order
702 Node r
= d_equalityEngine
->getRepresentative( f
);
703 //always replace the representative, since it is initially assigned to itself
704 Trace("model-builder") << " Assign: Setting function rep " << r
<< " to " << f_def
<< endl
;
706 // also assign to other assignable functions in the same equivalence class
707 eq::EqClassIterator eqc_i
= eq::EqClassIterator(r
,d_equalityEngine
);
708 while( !eqc_i
.isFinished() ) {
710 // if an unassigned variable function
711 if( n
.isVar() && d_uf_terms
.find( n
)!=d_uf_terms
.end() && !hasAssignedFunctionDefinition( n
) ){
712 d_uf_models
[n
] = f_def
;
713 Trace("model-builder") << " Assigning function (" << n
<< ") to function definition of " << f
<< std::endl
;
717 Trace("model-builder-debug") << " ...finished." << std::endl
;
721 std::vector
< Node
> TheoryModel::getFunctionsToAssign() {
722 std::vector
< Node
> funcs_to_assign
;
723 std::map
< Node
, Node
> func_to_rep
;
726 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= d_uf_terms
.begin(); it
!= d_uf_terms
.end(); ++it
){
729 if( !hasAssignedFunctionDefinition( n
) ){
730 Trace("model-builder-fun-debug") << "Look at function : " << n
<< std::endl
;
731 if( options::ufHo() ){
732 // if in higher-order mode, assign function definitions modulo equality
733 Node r
= getRepresentative( n
);
734 std::map
< Node
, Node
>::iterator itf
= func_to_rep
.find( r
);
735 if( itf
==func_to_rep
.end() ){
737 funcs_to_assign
.push_back( n
);
738 Trace("model-builder-fun") << "Make function " << n
;
739 Trace("model-builder-fun") << " the assignable function in its equivalence class." << std::endl
;
741 // must combine uf terms
742 Trace("model-builder-fun") << "Copy " << it
->second
.size() << " uf terms";
743 d_uf_terms
[itf
->second
].insert( d_uf_terms
[itf
->second
].end(), it
->second
.begin(), it
->second
.end() );
744 std::map
< Node
, std::vector
< Node
> >::iterator ith
= d_ho_uf_terms
.find( n
);
745 if( ith
!=d_ho_uf_terms
.end() ){
746 d_ho_uf_terms
[itf
->second
].insert( d_ho_uf_terms
[itf
->second
].end(), ith
->second
.begin(), ith
->second
.end() );
747 Trace("model-builder-fun") << " and " << ith
->second
.size() << " ho uf terms";
749 Trace("model-builder-fun") << " from " << n
<< " to its assignable representative function " << itf
->second
<< std::endl
;
753 Trace("model-builder-fun") << "Function to assign : " << n
<< std::endl
;
754 funcs_to_assign
.push_back( n
);
759 Trace("model-builder-fun") << "return " << funcs_to_assign
.size() << " functions to assign..." << std::endl
;
760 return funcs_to_assign
;
763 } /* namespace CVC4::theory */
764 } /* namespace CVC4 */