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/theory_options.h"
20 #include "options/uf_options.h"
21 #include "smt/smt_engine.h"
24 using namespace CVC4::kind
;
25 using namespace CVC4::context
;
30 TheoryModel::TheoryModel(context::Context
* c
,
32 bool enableFuncModels
)
34 d_substitutions(c
, false),
35 d_equalityEngine(nullptr),
36 d_using_model_core(false),
37 d_enableFuncModels(enableFuncModels
)
39 // must use function models when ufHo is enabled
40 Assert(d_enableFuncModels
|| !options::ufHo());
41 d_true
= NodeManager::currentNM()->mkConst( true );
42 d_false
= NodeManager::currentNM()->mkConst( false );
45 TheoryModel::~TheoryModel() {}
47 void TheoryModel::finishInit(eq::EqualityEngine
* ee
)
49 Assert(ee
!= nullptr);
50 d_equalityEngine
= ee
;
51 // The kinds we are treating as function application in congruence
52 d_equalityEngine
->addFunctionKind(kind::APPLY_UF
, false, options::ufHo());
53 d_equalityEngine
->addFunctionKind(kind::HO_APPLY
);
54 d_equalityEngine
->addFunctionKind(kind::SELECT
);
55 // d_equalityEngine->addFunctionKind(kind::STORE);
56 d_equalityEngine
->addFunctionKind(kind::APPLY_CONSTRUCTOR
);
57 d_equalityEngine
->addFunctionKind(kind::APPLY_SELECTOR_TOTAL
);
58 d_equalityEngine
->addFunctionKind(kind::APPLY_TESTER
);
59 // do not interpret APPLY_UF if we are not assigning function values
60 if (!d_enableFuncModels
)
62 setSemiEvaluatedKind(kind::APPLY_UF
);
64 // Equal and not terms are not relevant terms. In other words, asserted
65 // equalities and negations of predicates (as terms) do not need to be sent
66 // to the model. Regardless, theories should send information to the model
67 // that ensures that all assertions are satisfied.
68 setIrrelevantKind(EQUAL
);
69 setIrrelevantKind(NOT
);
72 void TheoryModel::reset(){
74 d_comment_str
.clear();
75 d_sep_heap
= Node::null();
76 d_sep_nil_eq
= Node::null();
77 d_approximations
.clear();
78 d_approx_list
.clear();
80 d_assignExcSet
.clear();
85 d_ho_uf_terms
.clear();
87 d_using_model_core
= false;
91 void TheoryModel::getComments(std::ostream
& out
) const {
92 Trace("model-builder") << "get comments..." << std::endl
;
93 out
<< d_comment_str
.str();
96 void TheoryModel::setHeapModel( Node h
, Node neq
) {
101 bool TheoryModel::getHeapModel(Node
& h
, Node
& neq
) const
103 if (d_sep_heap
.isNull() || d_sep_nil_eq
.isNull())
112 bool TheoryModel::hasApproximations() const { return !d_approx_list
.empty(); }
114 std::vector
<std::pair
<Node
, Node
> > TheoryModel::getApproximations() const
116 return d_approx_list
;
119 std::vector
<Node
> TheoryModel::getDomainElements(TypeNode tn
) const
121 // must be an uninterpreted sort
123 std::vector
<Node
> elements
;
124 const std::vector
<Node
>* type_refs
= d_rep_set
.getTypeRepsOrNull(tn
);
125 if (type_refs
== nullptr || type_refs
->empty())
127 // This is called when t is a sort that does not occur in this model.
128 // Sorts are always interpreted as non-empty, thus we add a single element.
129 elements
.push_back(tn
.mkGroundTerm());
135 Node
TheoryModel::getValue(TNode n
) const
137 //apply substitutions
138 Node nn
= d_substitutions
.apply(n
);
139 Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n
<< " to " << nn
<< std::endl
;
141 nn
= getModelValue(nn
);
142 if (nn
.isNull()) return nn
;
143 if(options::condenseFunctionValues() || nn
.getKind() != kind::LAMBDA
) {
145 nn
= Rewriter::rewrite(nn
);
147 Debug("model-getvalue") << "[model-getvalue] getValue( " << n
<< " ): " << std::endl
148 << "[model-getvalue] returning " << nn
<< std::endl
;
152 bool TheoryModel::isModelCoreSymbol(Node s
) const
154 if (!d_using_model_core
)
158 Assert(s
.isVar() && s
.getKind() != BOUND_VARIABLE
);
159 return d_model_core
.find(s
) != d_model_core
.end();
162 Cardinality
TheoryModel::getCardinality(TypeNode tn
) const
164 //for now, we only handle cardinalities for uninterpreted sorts
167 Debug("model-getvalue-debug")
168 << "Get cardinality other sort, unknown." << std::endl
;
169 return Cardinality( CardinalityUnknown() );
171 if (d_rep_set
.hasType(tn
))
173 Debug("model-getvalue-debug")
174 << "Get cardinality sort, #rep : "
175 << d_rep_set
.getNumRepresentatives(tn
) << std::endl
;
176 return Cardinality(d_rep_set
.getNumRepresentatives(tn
));
178 Debug("model-getvalue-debug")
179 << "Get cardinality sort, unconstrained, return 1." << std::endl
;
180 return Cardinality(1);
183 Node
TheoryModel::getModelValue(TNode n
) const
185 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator it
= d_modelCache
.find(n
);
186 if (it
!= d_modelCache
.end()) {
189 Debug("model-getvalue-debug") << "Get model value " << n
<< " ... ";
190 Debug("model-getvalue-debug") << d_equalityEngine
->hasTerm(n
) << std::endl
;
191 Kind nk
= n
.getKind();
192 if (n
.isConst() || nk
== BOUND_VARIABLE
)
199 NodeManager
* nm
= NodeManager::currentNM();
201 // if it is an evaluated kind, compute model values for children and evaluate
202 if (n
.getNumChildren() > 0
203 && d_unevaluated_kinds
.find(nk
) == d_unevaluated_kinds
.end()
204 && d_semi_evaluated_kinds
.find(nk
) == d_semi_evaluated_kinds
.end())
206 Debug("model-getvalue-debug")
207 << "Get model value children " << n
<< std::endl
;
208 std::vector
<Node
> children
;
209 if (n
.getKind() == APPLY_UF
)
211 Node op
= getModelValue(n
.getOperator());
212 Debug("model-getvalue-debug") << " operator : " << op
<< std::endl
;
213 children
.push_back(op
);
215 else if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
)
217 children
.push_back(n
.getOperator());
219 // evaluate the children
220 for (unsigned i
= 0, nchild
= n
.getNumChildren(); i
< nchild
; ++i
)
222 ret
= getModelValue(n
[i
]);
223 Debug("model-getvalue-debug")
224 << " " << n
<< "[" << i
<< "] is " << ret
<< std::endl
;
225 children
.push_back(ret
);
227 ret
= nm
->mkNode(n
.getKind(), children
);
228 Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret
<< std::endl
;
229 ret
= Rewriter::rewrite(ret
);
230 Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret
<< std::endl
;
232 if (ret
.getKind() == kind::CARDINALITY_CONSTRAINT
)
234 Debug("model-getvalue-debug")
235 << "get cardinality constraint " << ret
[0].getType() << std::endl
;
236 ret
= nm
->mkConst(getCardinality(ret
[0].getType()).getFiniteCardinality()
237 <= ret
[1].getConst
<Rational
>().getNumerator());
239 else if (ret
.getKind() == kind::CARDINALITY_VALUE
)
241 Debug("model-getvalue-debug")
242 << "get cardinality value " << ret
[0].getType() << std::endl
;
244 Rational(getCardinality(ret
[0].getType()).getFiniteCardinality()));
246 d_modelCache
[n
] = ret
;
249 // it might be approximate
250 std::map
<Node
, Node
>::const_iterator ita
= d_approximations
.find(n
);
251 if (ita
!= d_approximations
.end())
253 // If the value of n is approximate based on predicate P(n), we return
255 Node v
= nm
->mkBoundVar(n
.getType());
256 Node bvl
= nm
->mkNode(BOUND_VAR_LIST
, v
);
257 Node answer
= nm
->mkNode(WITNESS
, bvl
, ita
->second
.substitute(n
, v
));
258 d_modelCache
[n
] = answer
;
261 // must rewrite the term at this point
262 ret
= Rewriter::rewrite(n
);
263 // return the representative of the term in the equality engine, if it exists
264 TypeNode t
= ret
.getType();
266 if (!options::ufHo() && (t
.isFunction() || t
.isPredicate()))
268 // functions are in the equality engine, but *not* as first-class members
269 // when higher-order is disabled. In this case, we cannot query
270 // representatives for functions since they are "internal" nodes according
271 // to the equality engine despite hasTerm returning true. However, they are
272 // first class members when higher-order is enabled. Hence, the special
278 eeHasTerm
= d_equalityEngine
->hasTerm(ret
);
282 Debug("model-getvalue-debug")
283 << "get value from representative " << ret
<< "..." << std::endl
;
284 ret
= d_equalityEngine
->getRepresentative(ret
);
285 Assert(d_reps
.find(ret
) != d_reps
.end());
286 std::map
<Node
, Node
>::const_iterator it2
= d_reps
.find(ret
);
287 if (it2
!= d_reps
.end())
290 d_modelCache
[n
] = ret
;
295 // if we are a evaluated or semi-evaluated kind, return an arbitrary value
296 // if we are not in the d_unevaluated_kinds map, we are evaluated
297 if (d_unevaluated_kinds
.find(nk
) == d_unevaluated_kinds
.end())
299 if (t
.isFunction() || t
.isPredicate())
301 if (d_enableFuncModels
)
303 std::map
<Node
, Node
>::const_iterator entry
= d_uf_models
.find(n
);
304 if (entry
!= d_uf_models
.end())
308 d_modelCache
[n
] = ret
;
311 // Unknown function symbol: return LAMBDA x. c, where c is the first
312 // constant in the enumeration of the range type
313 vector
<TypeNode
> argTypes
= t
.getArgTypes();
315 for (unsigned i
= 0, size
= argTypes
.size(); i
< size
; ++i
)
317 args
.push_back(nm
->mkBoundVar(argTypes
[i
]));
319 Node boundVarList
= nm
->mkNode(kind::BOUND_VAR_LIST
, args
);
320 TypeEnumerator
te(t
.getRangeType());
321 ret
= nm
->mkNode(kind::LAMBDA
, boundVarList
, *te
);
325 // if func models not enabled, throw an error
329 else if (!t
.isFirstClass())
331 // this is the class for regular expressions
332 // we simply invoke the rewriter on them
333 ret
= Rewriter::rewrite(ret
);
337 // Unknown term - return first enumerated value for this type
338 TypeEnumerator
te(n
.getType());
341 d_modelCache
[n
] = ret
;
349 /** add substitution */
350 void TheoryModel::addSubstitution( TNode x
, TNode t
, bool invalidateCache
){
351 if( !d_substitutions
.hasSubstitution( x
) ){
352 Debug("model") << "Add substitution in model " << x
<< " -> " << t
<< std::endl
;
353 d_substitutions
.addSubstitution( x
, t
, invalidateCache
);
355 #ifdef CVC4_ASSERTIONS
356 Node oldX
= d_substitutions
.getSubstitution(x
);
357 // check that either the old substitution is the same, or it now maps to the new substitution
358 if(oldX
!= t
&& d_substitutions
.apply(oldX
) != d_substitutions
.apply(t
)) {
360 << "Two incompatible substitutions added to TheoryModel:\n"
361 << "the term: " << x
<< "\n"
362 << "old mapping: " << d_substitutions
.apply(oldX
) << "\n"
363 << "new mapping: " << d_substitutions
.apply(t
);
365 #endif /* CVC4_ASSERTIONS */
370 void TheoryModel::addTermInternal(TNode n
)
372 Assert(d_equalityEngine
->hasTerm(n
));
373 Trace("model-builder-debug2") << "TheoryModel::addTerm : " << n
<< std::endl
;
374 //must collect UF terms
375 if (n
.getKind()==APPLY_UF
) {
376 Node op
= n
.getOperator();
377 if( std::find( d_uf_terms
[ op
].begin(), d_uf_terms
[ op
].end(), n
)==d_uf_terms
[ op
].end() ){
378 d_uf_terms
[ op
].push_back( n
);
379 Trace("model-builder-fun") << "Add apply term " << n
<< std::endl
;
381 }else if( n
.getKind()==HO_APPLY
){
383 if( std::find( d_ho_uf_terms
[ op
].begin(), d_ho_uf_terms
[ op
].end(), n
)==d_ho_uf_terms
[ op
].end() ){
384 d_ho_uf_terms
[ op
].push_back( n
);
385 Trace("model-builder-fun") << "Add ho apply term " << n
<< std::endl
;
388 // all functions must be included, marked as higher-order
389 if( n
.getType().isFunction() ){
390 Trace("model-builder-fun") << "Add function variable (without term) " << n
<< std::endl
;
391 if( d_uf_terms
.find( n
)==d_uf_terms
.end() ){
392 d_uf_terms
[n
].clear();
394 if( d_ho_uf_terms
.find( n
)==d_ho_uf_terms
.end() ){
395 d_ho_uf_terms
[n
].clear();
400 /** assert equality */
401 bool TheoryModel::assertEquality(TNode a
, TNode b
, bool polarity
)
403 Assert(d_equalityEngine
->consistent());
404 if (a
== b
&& polarity
) {
407 Trace("model-builder-assertions") << "(assert " << (polarity
? "(= " : "(not (= ") << a
<< " " << b
<< (polarity
? "));" : ")));") << endl
;
408 d_equalityEngine
->assertEquality( a
.eqNode(b
), polarity
, Node::null() );
409 return d_equalityEngine
->consistent();
412 /** assert predicate */
413 bool TheoryModel::assertPredicate(TNode a
, bool polarity
)
415 Assert(d_equalityEngine
->consistent());
416 if ((a
== d_true
&& polarity
) ||
417 (a
== d_false
&& (!polarity
))) {
420 if (a
.getKind() == EQUAL
) {
421 Trace("model-builder-assertions") << "(assert " << (polarity
? " " : "(not ") << a
<< (polarity
? ");" : "));") << endl
;
422 d_equalityEngine
->assertEquality( a
, polarity
, Node::null() );
424 Trace("model-builder-assertions") << "(assert " << (polarity
? "" : "(not ") << a
<< (polarity
? ");" : "));") << endl
;
425 d_equalityEngine
->assertPredicate( a
, polarity
, Node::null() );
427 return d_equalityEngine
->consistent();
430 /** assert equality engine */
431 bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine
* ee
,
432 const std::set
<Node
>* termSet
)
434 Assert(d_equalityEngine
->consistent());
435 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
436 for (; !eqcs_i
.isFinished(); ++eqcs_i
) {
437 Node eqc
= (*eqcs_i
);
438 bool predicate
= false;
439 bool predTrue
= false;
440 bool predFalse
= false;
441 Trace("model-builder-debug") << "...asserting terms in equivalence class " << eqc
;
442 if (eqc
.getType().isBoolean()) {
444 predTrue
= ee
->areEqual(eqc
, d_true
);
445 predFalse
= ee
->areEqual(eqc
, d_false
);
446 Trace("model-builder-debug") << ", pred = " << predTrue
<< "/" << predFalse
;
448 Trace("model-builder-debug") << std::endl
;
449 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, ee
);
452 for (; !eqc_i
.isFinished(); ++eqc_i
) {
453 if (termSet
!= NULL
&& termSet
->find(*eqc_i
) == termSet
->end()) {
454 Trace("model-builder-debug") << "...skip node " << (*eqc_i
) << " in eqc " << eqc
<< std::endl
;
458 if (predTrue
|| predFalse
)
460 if (!assertPredicate(*eqc_i
, predTrue
))
471 Node eq
= (*eqc_i
).eqNode(rep
);
472 Trace("model-builder-assertions")
473 << "(assert " << eq
<< ");" << std::endl
;
474 d_equalityEngine
->assertEquality(eq
, true, Node::null());
475 if (!d_equalityEngine
->consistent())
484 //add the term (this is specifically for the case of singleton equivalence classes)
485 if (rep
.getType().isFirstClass())
487 d_equalityEngine
->addTerm( rep
);
488 Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep
<< std::endl
;
493 if (!assertEquality(*eqc_i
, rep
, true))
504 void TheoryModel::assertSkeleton(TNode n
)
506 Trace("model-builder-reps") << "Assert skeleton : " << n
<< std::endl
;
507 Trace("model-builder-reps") << "...rep eqc is : " << getRepresentative(n
)
512 void TheoryModel::setAssignmentExclusionSet(TNode n
,
513 const std::vector
<Node
>& eset
)
515 // should not be assigned yet
516 Assert(d_assignExcSet
.find(n
) == d_assignExcSet
.end());
517 Trace("model-builder-debug")
518 << "Exclude values of " << n
<< " : " << eset
<< std::endl
;
519 std::vector
<Node
>& aes
= d_assignExcSet
[n
];
520 aes
.insert(aes
.end(), eset
.begin(), eset
.end());
523 void TheoryModel::setAssignmentExclusionSetGroup(
524 const std::vector
<TNode
>& group
, const std::vector
<Node
>& eset
)
530 // for efficiency, we store a single copy of eset and set a slave/master
532 setAssignmentExclusionSet(group
[0], eset
);
533 std::vector
<Node
>& gslaves
= d_aesSlaves
[group
[0]];
534 for (unsigned i
= 1, gsize
= group
.size(); i
< gsize
; ++i
)
538 d_aesMaster
[gs
] = group
[0];
540 gslaves
.push_back(gs
);
544 bool TheoryModel::getAssignmentExclusionSet(TNode n
,
545 std::vector
<Node
>& group
,
546 std::vector
<Node
>& eset
)
548 // does it have a master?
549 std::map
<Node
, Node
>::iterator itm
= d_aesMaster
.find(n
);
550 if (itm
!= d_aesMaster
.end())
552 return getAssignmentExclusionSet(itm
->second
, group
, eset
);
554 std::map
<Node
, std::vector
<Node
> >::iterator ita
= d_assignExcSet
.find(n
);
555 if (ita
== d_assignExcSet
.end())
559 eset
.insert(eset
.end(), ita
->second
.begin(), ita
->second
.end());
561 // does it have slaves?
562 ita
= d_aesSlaves
.find(n
);
563 if (ita
!= d_aesSlaves
.end())
565 group
.insert(group
.end(), ita
->second
.begin(), ita
->second
.end());
570 bool TheoryModel::hasAssignmentExclusionSets() const
572 return !d_assignExcSet
.empty();
575 void TheoryModel::recordApproximation(TNode n
, TNode pred
)
577 Trace("model-builder-debug")
578 << "Record approximation : " << n
<< " satisfies the predicate " << pred
580 Assert(d_approximations
.find(n
) == d_approximations
.end());
581 Assert(pred
.getType().isBoolean());
582 d_approximations
[n
] = pred
;
583 d_approx_list
.push_back(std::pair
<Node
, Node
>(n
, pred
));
584 // model cache is invalid
585 d_modelCache
.clear();
587 void TheoryModel::recordApproximation(TNode n
, TNode pred
, Node witness
)
589 Node predDisj
= NodeManager::currentNM()->mkNode(OR
, n
.eqNode(witness
), pred
);
590 recordApproximation(n
, predDisj
);
592 void TheoryModel::setUsingModelCore()
594 d_using_model_core
= true;
595 d_model_core
.clear();
598 void TheoryModel::recordModelCoreSymbol(Node sym
) { d_model_core
.insert(sym
); }
600 void TheoryModel::setUnevaluatedKind(Kind k
) { d_unevaluated_kinds
.insert(k
); }
602 void TheoryModel::setSemiEvaluatedKind(Kind k
)
604 d_semi_evaluated_kinds
.insert(k
);
607 void TheoryModel::setIrrelevantKind(Kind k
) { d_irrKinds
.insert(k
); }
609 const std::set
<Kind
>& TheoryModel::getIrrelevantKinds() const
614 bool TheoryModel::isLegalElimination(TNode x
, TNode val
)
616 return !expr::hasSubtermKinds(d_unevaluated_kinds
, val
);
619 bool TheoryModel::hasTerm(TNode a
)
621 return d_equalityEngine
->hasTerm( a
);
624 Node
TheoryModel::getRepresentative(TNode a
)
626 if( d_equalityEngine
->hasTerm( a
) ){
627 Node r
= d_equalityEngine
->getRepresentative( a
);
628 if( d_reps
.find( r
)!=d_reps
.end() ){
638 bool TheoryModel::areEqual(TNode a
, TNode b
)
642 }else if( d_equalityEngine
->hasTerm( a
) && d_equalityEngine
->hasTerm( b
) ){
643 return d_equalityEngine
->areEqual( a
, b
);
649 bool TheoryModel::areDisequal(TNode a
, TNode b
)
651 if( d_equalityEngine
->hasTerm( a
) && d_equalityEngine
->hasTerm( b
) ){
652 return d_equalityEngine
->areDisequal( a
, b
, false );
658 bool TheoryModel::areFunctionValuesEnabled() const
660 return d_enableFuncModels
;
663 void TheoryModel::assignFunctionDefinition( Node f
, Node f_def
) {
664 Trace("model-builder") << " Assigning function (" << f
<< ") to (" << f_def
<< ")" << endl
;
665 Assert(d_uf_models
.find(f
) == d_uf_models
.end());
667 if( options::ufHo() ){
668 //we must rewrite the function value since the definition needs to be a constant value
669 f_def
= Rewriter::rewrite( f_def
);
670 Trace("model-builder-debug")
671 << "Model value (post-rewrite) : " << f_def
<< std::endl
;
672 Assert(f_def
.isConst()) << "Non-constant f_def: " << f_def
;
675 // d_uf_models only stores models for variables
677 d_uf_models
[f
] = f_def
;
680 if (options::ufHo() && d_equalityEngine
->hasTerm(f
))
682 Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl
;
683 // assign to representative if higher-order
684 Node r
= d_equalityEngine
->getRepresentative( f
);
685 //always replace the representative, since it is initially assigned to itself
686 Trace("model-builder") << " Assign: Setting function rep " << r
<< " to " << f_def
<< endl
;
688 // also assign to other assignable functions in the same equivalence class
689 eq::EqClassIterator eqc_i
= eq::EqClassIterator(r
,d_equalityEngine
);
690 while( !eqc_i
.isFinished() ) {
692 // if an unassigned variable function
693 if( n
.isVar() && d_uf_terms
.find( n
)!=d_uf_terms
.end() && !hasAssignedFunctionDefinition( n
) ){
694 d_uf_models
[n
] = f_def
;
695 Trace("model-builder") << " Assigning function (" << n
<< ") to function definition of " << f
<< std::endl
;
699 Trace("model-builder-debug") << " ...finished." << std::endl
;
703 std::vector
< Node
> TheoryModel::getFunctionsToAssign() {
704 std::vector
< Node
> funcs_to_assign
;
705 std::map
< Node
, Node
> func_to_rep
;
708 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= d_uf_terms
.begin(); it
!= d_uf_terms
.end(); ++it
){
711 if( !hasAssignedFunctionDefinition( n
) ){
712 Trace("model-builder-fun-debug") << "Look at function : " << n
<< std::endl
;
713 if( options::ufHo() ){
714 // if in higher-order mode, assign function definitions modulo equality
715 Node r
= getRepresentative( n
);
716 std::map
< Node
, Node
>::iterator itf
= func_to_rep
.find( r
);
717 if( itf
==func_to_rep
.end() ){
719 funcs_to_assign
.push_back( n
);
720 Trace("model-builder-fun") << "Make function " << n
;
721 Trace("model-builder-fun") << " the assignable function in its equivalence class." << std::endl
;
723 // must combine uf terms
724 Trace("model-builder-fun") << "Copy " << it
->second
.size() << " uf terms";
725 d_uf_terms
[itf
->second
].insert( d_uf_terms
[itf
->second
].end(), it
->second
.begin(), it
->second
.end() );
726 std::map
< Node
, std::vector
< Node
> >::iterator ith
= d_ho_uf_terms
.find( n
);
727 if( ith
!=d_ho_uf_terms
.end() ){
728 d_ho_uf_terms
[itf
->second
].insert( d_ho_uf_terms
[itf
->second
].end(), ith
->second
.begin(), ith
->second
.end() );
729 Trace("model-builder-fun") << " and " << ith
->second
.size() << " ho uf terms";
731 Trace("model-builder-fun") << " from " << n
<< " to its assignable representative function " << itf
->second
<< std::endl
;
735 Trace("model-builder-fun") << "Function to assign : " << n
<< std::endl
;
736 funcs_to_assign
.push_back( n
);
741 Trace("model-builder-fun") << "return " << funcs_to_assign
.size() << " functions to assign..." << std::endl
;
742 return funcs_to_assign
;
745 const std::string
& TheoryModel::getName() const { return d_name
; }
747 } /* namespace CVC4::theory */
748 } /* namespace CVC4 */