1 /********************* */
2 /*! \file theory_model_builder.cpp
4 ** Top contributors (to current version):
5 ** Clark Barrett, Andrew Reynolds, Morgan Deters
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 theory model buidler class
14 #include "theory/theory_model_builder.h"
16 #include "options/quantifiers_options.h"
17 #include "options/smt_options.h"
18 #include "options/uf_options.h"
19 #include "theory/theory_engine.h"
20 #include "theory/uf/theory_uf_model.h"
23 using namespace CVC4::kind
;
24 using namespace CVC4::context
;
29 TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine
* te
) : d_te(te
)
33 bool TheoryEngineModelBuilder::isAssignable(TNode n
)
35 if (n
.getKind() == kind::SELECT
|| n
.getKind() == kind::APPLY_SELECTOR_TOTAL
)
37 // selectors are always assignable (where we guarantee that they are not
41 Assert(!n
.getType().isFunction());
46 // might be a function field
47 return !n
.getType().isFunction();
52 // non-function variables, and fully applied functions
55 // no functions exist, all functions are fully applied
56 Assert(n
.getKind() != kind::HO_APPLY
);
57 Assert(!n
.getType().isFunction());
58 return n
.isVar() || n
.getKind() == kind::APPLY_UF
;
62 // Assert( n.getKind() != kind::APPLY_UF );
63 return (n
.isVar() && !n
.getType().isFunction())
64 || n
.getKind() == kind::APPLY_UF
65 || (n
.getKind() == kind::HO_APPLY
66 && n
[0].getType().getNumChildren() == 2);
71 void TheoryEngineModelBuilder::addAssignableSubterms(TNode n
,
75 if (n
.getKind() == FORALL
|| n
.getKind() == EXISTS
)
79 if (cache
.find(n
) != cache
.end())
85 tm
->d_equalityEngine
->addTerm(n
);
87 for (TNode::iterator child_it
= n
.begin(); child_it
!= n
.end(); ++child_it
)
89 addAssignableSubterms(*child_it
, tm
, cache
);
94 void TheoryEngineModelBuilder::assignConstantRep(TheoryModel
* tm
,
98 d_constantReps
[eqc
] = const_rep
;
99 Trace("model-builder") << " Assign: Setting constant rep of " << eqc
100 << " to " << const_rep
<< endl
;
101 tm
->d_rep_set
.setTermForRepresentative(const_rep
, eqc
);
104 bool TheoryEngineModelBuilder::isExcludedCdtValue(
106 std::set
<Node
>* repSet
,
107 std::map
<Node
, Node
>& assertedReps
,
110 Trace("model-builder-debug")
111 << "Is " << val
<< " and excluded codatatype value for " << eqc
<< "? "
113 for (set
<Node
>::iterator i
= repSet
->begin(); i
!= repSet
->end(); ++i
)
115 Assert(assertedReps
.find(*i
) != assertedReps
.end());
116 Node rep
= assertedReps
[*i
];
117 Trace("model-builder-debug") << " Rep : " << rep
<< std::endl
;
118 // check matching val to rep with eqc as a free variable
120 if (isCdtValueMatch(val
, rep
, eqc
, eqc_m
))
122 Trace("model-builder-debug") << " ...matches with " << eqc
<< " -> "
123 << eqc_m
<< std::endl
;
124 if (eqc_m
.getKind() == kind::UNINTERPRETED_CONSTANT
)
126 Trace("model-builder-debug") << "*** " << val
127 << " is excluded datatype for " << eqc
136 bool TheoryEngineModelBuilder::isCdtValueMatch(Node v
,
149 // only if an uninterpreted constant?
158 else if (v
.getKind() == kind::APPLY_CONSTRUCTOR
159 && r
.getKind() == kind::APPLY_CONSTRUCTOR
)
161 if (v
.getOperator() == r
.getOperator())
163 for (unsigned i
= 0; i
< v
.getNumChildren(); i
++)
165 if (!isCdtValueMatch(v
[i
], r
[i
], eqc
, eqc_m
))
176 bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn
)
182 else if (tn
.isArray())
184 return involvesUSort(tn
.getArrayIndexType())
185 || involvesUSort(tn
.getArrayConstituentType());
189 return involvesUSort(tn
.getSetElementType());
191 else if (tn
.isDatatype())
193 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
194 return dt
.involvesUninterpretedType();
202 bool TheoryEngineModelBuilder::isExcludedUSortValue(
203 std::map
<TypeNode
, unsigned>& eqc_usort_count
,
205 std::map
<Node
, bool>& visited
)
208 if (visited
.find(v
) == visited
.end())
211 TypeNode tn
= v
.getType();
214 Trace("model-builder-debug") << "Is excluded usort value : " << v
<< " "
216 unsigned card
= eqc_usort_count
[tn
];
217 Trace("model-builder-debug") << " Cardinality is " << card
<< std::endl
;
219 v
.getConst
<UninterpretedConstant
>().getIndex().toUnsignedInt();
220 Trace("model-builder-debug") << " Index is " << index
<< std::endl
;
221 return index
> 0 && index
>= card
;
223 for (unsigned i
= 0; i
< v
.getNumChildren(); i
++)
225 if (isExcludedUSortValue(eqc_usort_count
, v
[i
], visited
))
234 void TheoryEngineModelBuilder::addToTypeList(
236 std::vector
<TypeNode
>& type_list
,
237 std::unordered_set
<TypeNode
, TypeNodeHashFunction
>& visiting
)
239 if (std::find(type_list
.begin(), type_list
.end(), tn
) == type_list
.end())
241 if (visiting
.find(tn
) == visiting
.end())
244 /* This must make a recursive call on all types that are subterms of
245 * values of the current type.
246 * Note that recursive traversal here is over enumerated expressions
247 * (very low expression depth). */
250 addToTypeList(tn
.getArrayIndexType(), type_list
, visiting
);
251 addToTypeList(tn
.getArrayConstituentType(), type_list
, visiting
);
255 addToTypeList(tn
.getSetElementType(), type_list
, visiting
);
257 else if (tn
.isDatatype())
259 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
260 for (unsigned i
= 0; i
< dt
.getNumConstructors(); i
++)
262 for (unsigned j
= 0; j
< dt
[i
].getNumArgs(); j
++)
264 TypeNode ctn
= TypeNode::fromType(dt
[i
][j
].getRangeType());
265 addToTypeList(ctn
, type_list
, visiting
);
269 Assert(std::find(type_list
.begin(), type_list
.end(), tn
)
271 type_list
.push_back(tn
);
276 bool TheoryEngineModelBuilder::buildModel(Model
* m
)
278 Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl
;
279 TheoryModel
* tm
= (TheoryModel
*)m
;
281 // buildModel should only be called once per check
282 Assert(!tm
->isBuilt());
288 tm
->d_modelBuilt
= true;
290 // Collect model info from the theories
291 Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
293 d_te
->collectModelInfo(tm
);
295 // model-builder specific initialization
296 if (!preProcessBuildModel(tm
))
301 // Loop through all terms and make sure that assignable sub-terms are in the
303 // Also, record #eqc per type (for finite model finding)
304 std::map
<TypeNode
, unsigned> eqc_usort_count
;
305 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
308 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
310 eq::EqClassIterator eqc_i
=
311 eq::EqClassIterator((*eqcs_i
), tm
->d_equalityEngine
);
312 for (; !eqc_i
.isFinished(); ++eqc_i
)
314 addAssignableSubterms(*eqc_i
, tm
, cache
);
316 TypeNode tn
= (*eqcs_i
).getType();
319 if (eqc_usort_count
.find(tn
) == eqc_usort_count
.end())
321 eqc_usort_count
[tn
] = 1;
325 eqc_usort_count
[tn
]++;
331 Trace("model-builder") << "Collect representatives..." << std::endl
;
333 // Process all terms in the equality engine, store representatives for each EC
334 d_constantReps
.clear();
335 std::map
<Node
, Node
> assertedReps
;
336 TypeSet typeConstSet
, typeRepSet
, typeNoRepSet
;
337 TypeEnumeratorProperties tep
;
338 if (options::finiteModelFind())
340 tep
.d_fixed_usort_card
= true;
341 for (std::map
<TypeNode
, unsigned>::iterator it
= eqc_usort_count
.begin();
342 it
!= eqc_usort_count
.end();
345 Trace("model-builder") << "Fixed bound (#eqc) for " << it
->first
<< " : "
346 << it
->second
<< std::endl
;
347 tep
.d_fixed_card
[it
->first
] = Integer(it
->second
);
349 typeConstSet
.setTypeEnumeratorProperties(&tep
);
351 // AJR: build ordered list of types that ensures that base types are
353 // (I think) this is only strictly necessary for finite model finding +
354 // parametric types instantiated with uninterpreted sorts, but is probably
355 // a good idea to do in general since it leads to models with smaller term
357 std::vector
<TypeNode
> type_list
;
358 eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
359 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
361 // eqc is the equivalence class representative
362 Node eqc
= (*eqcs_i
);
363 Trace("model-builder") << "Processing EC: " << eqc
<< endl
;
364 Assert(tm
->d_equalityEngine
->getRepresentative(eqc
) == eqc
);
365 TypeNode eqct
= eqc
.getType();
366 Assert(assertedReps
.find(eqc
) == assertedReps
.end());
367 Assert(d_constantReps
.find(eqc
) == d_constantReps
.end());
369 // Loop through terms in this EC
371 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
372 for (; !eqc_i
.isFinished(); ++eqc_i
)
375 Trace("model-builder") << " Processing Term: " << n
<< endl
;
376 // Record as rep if this node was specified as a representative
377 if (tm
->d_reps
.find(n
) != tm
->d_reps
.end())
379 // AJR: I believe this assertion is too strict,
380 // e.g. datatypes may assert representative for two constructor terms
381 // that are not in the care graph and are merged during
383 // Assert(rep.isNull());
385 Assert(!rep
.isNull());
386 Trace("model-builder") << " Rep( " << eqc
<< " ) = " << rep
389 // Record as const_rep if this node is constant
392 Assert(const_rep
.isNull());
394 Trace("model-builder") << " ConstRep( " << eqc
<< " ) = " << const_rep
397 // model-specific processing of the term
398 tm
->addTermInternal(n
);
401 // Assign representative for this EC
402 if (!const_rep
.isNull())
404 // Theories should not specify a rep if there is already a constant in the
406 // AJR: I believe this assertion is too strict, eqc with asserted reps may
407 // merge with constant eqc
408 // Assert(rep.isNull() || rep == const_rep);
409 assignConstantRep(tm
, eqc
, const_rep
);
410 typeConstSet
.add(eqct
.getBaseType(), const_rep
);
412 else if (!rep
.isNull())
414 assertedReps
[eqc
] = rep
;
415 typeRepSet
.add(eqct
.getBaseType(), eqc
);
416 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
417 addToTypeList(eqct
.getBaseType(), type_list
, visiting
);
421 typeNoRepSet
.add(eqct
, eqc
);
422 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
423 addToTypeList(eqct
, type_list
, visiting
);
427 // Need to ensure that each EC has a constant representative.
429 Trace("model-builder") << "Processing EC's..." << std::endl
;
431 TypeSet::iterator it
;
432 vector
<TypeNode
>::iterator type_it
;
433 set
<Node
>::iterator i
, i2
;
434 bool changed
, unassignedAssignable
, assignOne
= false;
435 set
<TypeNode
> evaluableSet
;
437 // Double-fixed-point loop
438 // Outer loop handles a special corner case (see code at end of loop for
442 // Inner fixed-point loop: we are trying to learn constant values for every
443 // EC. Each time through this loop, we process all of the
444 // types by type and may learn some new EC values. EC's in one type may
445 // depend on EC's in another type, so we need a fixed-point loop
446 // to ensure that we learn as many EC values as possible
450 unassignedAssignable
= false;
451 evaluableSet
.clear();
453 // Iterate over all types we've seen
454 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
456 TypeNode t
= *type_it
;
457 TypeNode tb
= t
.getBaseType();
458 set
<Node
>* noRepSet
= typeNoRepSet
.getSet(t
);
460 // 1. Try to evaluate the EC's in this type
461 if (noRepSet
!= NULL
&& !noRepSet
->empty())
463 Trace("model-builder") << " Eval phase, working on type: " << t
465 bool assignable
, evaluable
, evaluated
;
466 d_normalizedCache
.clear();
467 for (i
= noRepSet
->begin(); i
!= noRepSet
->end();)
474 Trace("model-builder-debug") << "Look at eqc : " << (*i2
)
476 eq::EqClassIterator eqc_i
=
477 eq::EqClassIterator(*i2
, tm
->d_equalityEngine
);
478 for (; !eqc_i
.isFinished(); ++eqc_i
)
481 Trace("model-builder-debug") << "Look at term : " << n
486 Trace("model-builder-debug") << "...assignable" << std::endl
;
491 Trace("model-builder-debug") << "...try to normalize"
493 Node normalized
= normalize(tm
, n
, true);
494 if (normalized
.isConst())
496 typeConstSet
.add(tb
, normalized
);
497 assignConstantRep(tm
, *i2
, normalized
);
498 Trace("model-builder") << " Eval: Setting constant rep of "
499 << (*i2
) << " to " << normalized
512 evaluableSet
.insert(tb
);
516 unassignedAssignable
= true;
522 // 2. Normalize any non-const representative terms for this type
523 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
524 if (repSet
!= NULL
&& !repSet
->empty())
526 Trace("model-builder")
527 << " Normalization phase, working on type: " << t
<< endl
;
528 d_normalizedCache
.clear();
529 for (i
= repSet
->begin(); i
!= repSet
->end();)
531 Assert(assertedReps
.find(*i
) != assertedReps
.end());
532 Node rep
= assertedReps
[*i
];
533 Node normalized
= normalize(tm
, rep
, false);
534 Trace("model-builder") << " Normalizing rep (" << rep
535 << "), normalized to (" << normalized
<< ")"
537 if (normalized
.isConst())
540 typeConstSet
.add(tb
, normalized
);
541 assignConstantRep(tm
, *i
, normalized
);
542 assertedReps
.erase(*i
);
549 if (normalized
!= rep
)
551 assertedReps
[*i
] = normalized
;
561 if (!unassignedAssignable
)
566 // 3. Assign unassigned assignable EC's using type enumeration - assign a
567 // value *different* from all other EC's if the type is infinite
568 // Assign first value from type enumerator otherwise - for finite types, we
569 // rely on polite framework to ensure that EC's that have to be
570 // different are different.
572 // Only make assignments on a type if:
573 // 1. there are no terms that share the same base type with un-normalized
575 // 2. there are no terms that share teh same base type that are unevaluated
577 // Alternatively, if 2 or 3 don't hold but we are in a special
578 // deadlock-breaking mode where assignOne is true, go ahead and make one
581 // must iterate over the ordered type list to ensure that we do not
582 // enumerate values with subterms
583 // having types that we are currently enumerating (when possible)
584 // for example, this ensures we enumerate uninterpreted sort U before (List
585 // of U) and (Array U U)
586 // however, it does not break cyclic type dependencies for mutually
587 // recursive datatypes, but this is handled
588 // by recording all subterms of enumerated values in TypeSet::addSubTerms.
589 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
591 TypeNode t
= *type_it
;
592 // continue if there are no more equivalence classes of this type to
594 std::set
<Node
>* noRepSetPtr
= typeNoRepSet
.getSet(t
);
595 if (noRepSetPtr
== NULL
)
599 set
<Node
>& noRepSet
= *noRepSetPtr
;
600 if (noRepSet
.empty())
605 // get properties of this type
606 bool isCorecursive
= false;
609 const Datatype
& dt
= ((DatatypeType
)(t
).toType()).getDatatype();
611 dt
.isCodatatype() && (!dt
.isFinite(t
.toType())
612 || dt
.isRecursiveSingleton(t
.toType()));
614 #ifdef CVC4_ASSERTIONS
615 bool isUSortFiniteRestricted
= false;
616 if (options::finiteModelFind())
618 isUSortFiniteRestricted
= !t
.isSort() && involvesUSort(t
);
622 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
623 TypeNode tb
= t
.getBaseType();
626 set
<Node
>* repSet
= typeRepSet
.getSet(tb
);
627 if (repSet
!= NULL
&& !repSet
->empty())
631 if (evaluableSet
.find(tb
) != evaluableSet
.end())
636 Trace("model-builder") << " Assign phase, working on type: " << t
638 bool assignable
, evaluable CVC4_UNUSED
;
639 for (i
= noRepSet
.begin(); i
!= noRepSet
.end();)
643 eq::EqClassIterator eqc_i
=
644 eq::EqClassIterator(*i2
, tm
->d_equalityEngine
);
647 for (; !eqc_i
.isFinished(); ++eqc_i
)
659 Trace("model-builder-debug")
660 << " eqc " << *i2
<< " is assignable=" << assignable
661 << ", evaluable=" << evaluable
<< std::endl
;
664 Assert(!evaluable
|| assignOne
);
665 Assert(!t
.isBoolean() || (*i2
).getKind() == kind::APPLY_UF
);
667 if (t
.getCardinality().isInfinite())
669 // if (!t.isInterpretedFinite()) {
673 Trace("model-builder-debug") << "Enumerate term of type " << t
675 n
= typeConstSet
.nextTypeEnum(t
, true);
676 //--- AJR: this code checks whether n is a legal value
679 Trace("model-builder-debug") << "Check if excluded : " << n
681 #ifdef CVC4_ASSERTIONS
682 if (isUSortFiniteRestricted
)
684 // must not involve uninterpreted constants beyond cardinality
685 // bound (which assumed to coincide with #eqc)
686 // this is just an assertion now, since TypeEnumeratorProperties
687 // should ensure that only legal values are enumerated wrt this
689 std::map
<Node
, bool> visited
;
690 success
= !isExcludedUSortValue(eqc_usort_count
, n
, visited
);
693 Trace("model-builder")
694 << "Excluded value for " << t
<< " : " << n
695 << " due to out of range uninterpreted constant."
701 if (success
&& isCorecursive
)
703 if (repSet
!= NULL
&& !repSet
->empty())
705 // in the case of codatatypes, check if it is in the set of
706 // values that we cannot assign
707 success
= !isExcludedCdtValue(n
, repSet
, assertedReps
, *i2
);
710 Trace("model-builder")
711 << "Excluded value : " << n
712 << " due to alpha-equivalent codatatype expression."
722 TypeEnumerator
te(t
);
726 assignConstantRep(tm
, *i2
, n
);
738 // Corner case - I'm not sure this can even happen - but it's theoretically
739 // possible to have a cyclical dependency
740 // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
741 // this case, neither one will get assigned because we are waiting
742 // to be able to evaluate. But we will never be able to evaluate because
743 // the variables that need to be assigned are in
744 // these same EC's. In this case, repeat the whole fixed-point computation
745 // with the difference that the first EC
746 // that has both assignable and evaluable expressions will get assigned.
749 Assert(!assignOne
); // check for infinite loop!
754 #ifdef CVC4_ASSERTIONS
755 // Assert that all representatives have been converted to constants
756 for (it
= typeRepSet
.begin(); it
!= typeRepSet
.end(); ++it
)
758 set
<Node
>& repSet
= TypeSet::getSet(it
);
761 Trace("model-builder") << "***Non-empty repSet, size = " << repSet
.size()
762 << ", first = " << *(repSet
.begin()) << endl
;
766 #endif /* CVC4_ASSERTIONS */
768 Trace("model-builder") << "Copy representatives to model..." << std::endl
;
770 std::map
<Node
, Node
>::iterator itMap
;
771 for (itMap
= d_constantReps
.begin(); itMap
!= d_constantReps
.end(); ++itMap
)
773 tm
->d_reps
[itMap
->first
] = itMap
->second
;
774 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
777 Trace("model-builder") << "Make sure ECs have reps..." << std::endl
;
778 // Make sure every EC has a rep
779 for (itMap
= assertedReps
.begin(); itMap
!= assertedReps
.end(); ++itMap
)
781 tm
->d_reps
[itMap
->first
] = itMap
->second
;
782 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
784 for (it
= typeNoRepSet
.begin(); it
!= typeNoRepSet
.end(); ++it
)
786 set
<Node
>& noRepSet
= TypeSet::getSet(it
);
787 set
<Node
>::iterator i
;
788 for (i
= noRepSet
.begin(); i
!= noRepSet
.end(); ++i
)
791 tm
->d_rep_set
.add((*i
).getType(), *i
);
795 // modelBuilder-specific initialization
796 if (!processBuildModel(tm
))
806 void TheoryEngineModelBuilder::debugCheckModel(Model
* m
)
808 TheoryModel
* tm
= (TheoryModel
*)m
;
809 #ifdef CVC4_ASSERTIONS
810 Assert(tm
->isBuilt());
811 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
812 std::map
<Node
, Node
>::iterator itMap
;
813 // Check that every term evaluates to its representative in the model
814 for (eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
815 !eqcs_i
.isFinished();
818 // eqc is the equivalence class representative
819 Node eqc
= (*eqcs_i
);
820 // get the representative
821 Node rep
= tm
->getRepresentative(eqc
);
822 if (!rep
.isConst() && eqc
.getType().isBoolean())
824 // if Boolean, it does not necessarily have a constant representative, use
826 rep
= tm
->getValue(eqc
);
827 Assert(rep
.isConst());
829 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
830 for (; !eqc_i
.isFinished(); ++eqc_i
)
833 static int repCheckInstance
= 0;
836 // non-linear mult is not necessarily accurate wrt getValue
837 if (n
.getKind() != kind::NONLINEAR_MULT
)
839 Debug("check-model::rep-checking") << "( " << repCheckInstance
<< ") "
840 << "n: " << n
<< endl
841 << "getValue(n): " << tm
->getValue(n
)
843 << "rep: " << rep
<< endl
;
844 Assert(tm
->getValue(*eqc_i
) == rep
,
845 "run with -d check-model::rep-checking for details");
849 #endif /* CVC4_ASSERTIONS */
851 // builder-specific debugging
855 Node
TheoryEngineModelBuilder::normalize(TheoryModel
* m
, TNode r
, bool evalOnly
)
857 std::map
<Node
, Node
>::iterator itMap
= d_constantReps
.find(r
);
858 if (itMap
!= d_constantReps
.end())
860 return (*itMap
).second
;
862 NodeMap::iterator it
= d_normalizedCache
.find(r
);
863 if (it
!= d_normalizedCache
.end())
867 Trace("model-builder-debug") << "do normalize on " << r
<< std::endl
;
869 if (r
.getNumChildren() > 0)
871 std::vector
<Node
> children
;
872 if (r
.getMetaKind() == kind::metakind::PARAMETERIZED
)
874 children
.push_back(r
.getOperator());
876 bool childrenConst
= true;
877 for (size_t i
= 0; i
< r
.getNumChildren(); ++i
)
883 if (m
->d_equalityEngine
->hasTerm(ri
))
886 d_constantReps
.find(m
->d_equalityEngine
->getRepresentative(ri
));
887 if (itMap
!= d_constantReps
.end())
889 ri
= (*itMap
).second
;
899 ri
= normalize(m
, ri
, evalOnly
);
903 childrenConst
= false;
906 children
.push_back(ri
);
908 retNode
= NodeManager::currentNM()->mkNode(r
.getKind(), children
);
911 retNode
= Rewriter::rewrite(retNode
);
912 Assert(retNode
.getKind() == kind::APPLY_UF
913 || !retNode
.getType().isFirstClass()
914 || retNode
.isConst());
917 d_normalizedCache
[r
] = retNode
;
921 bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel
* m
)
926 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel
* m
)
932 void TheoryEngineModelBuilder::assignFunction(TheoryModel
* m
, Node f
)
934 Assert(!options::ufHo());
935 uf::UfModelTree
ufmt(f
);
937 for (size_t i
= 0; i
< m
->d_uf_terms
[f
].size(); i
++)
939 Node un
= m
->d_uf_terms
[f
][i
];
940 vector
<TNode
> children
;
941 children
.push_back(f
);
942 Trace("model-builder-debug") << " process term : " << un
<< std::endl
;
943 for (size_t j
= 0; j
< un
.getNumChildren(); ++j
)
945 Node rc
= m
->getRepresentative(un
[j
]);
946 Trace("model-builder-debug2") << " get rep : " << un
[j
] << " returned "
948 Assert(rc
.isConst());
949 children
.push_back(rc
);
951 Node simp
= NodeManager::currentNM()->mkNode(un
.getKind(), children
);
952 Node v
= m
->getRepresentative(un
);
953 Trace("model-builder") << " Setting (" << simp
<< ") to (" << v
<< ")"
955 ufmt
.setValue(m
, simp
, v
);
958 if (default_v
.isNull())
960 // choose default value from model if none exists
961 TypeEnumerator
te(f
.getType().getRangeType());
964 ufmt
.setDefaultValue(m
, default_v
);
965 bool condenseFuncValues
= options::condenseFunctionValues();
966 if (condenseFuncValues
)
970 std::stringstream ss
;
971 ss
<< "_arg_" << f
<< "_";
972 Node val
= ufmt
.getFunctionValue(ss
.str().c_str(), condenseFuncValues
);
973 m
->assignFunctionDefinition(f
, val
);
974 // ufmt.debugPrint( std::cout, m );
977 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel
* m
, Node f
)
979 Assert(options::ufHo());
980 TypeNode type
= f
.getType();
981 std::vector
<TypeNode
> argTypes
= type
.getArgTypes();
982 std::vector
<Node
> args
;
983 std::vector
<TNode
> apply_args
;
984 for (unsigned i
= 0; i
< argTypes
.size(); i
++)
986 Node v
= NodeManager::currentNM()->mkBoundVar(argTypes
[i
]);
990 apply_args
.push_back(v
);
993 // start with the base return value (currently we use the same default value
994 // for all functions)
995 TypeEnumerator
te(type
.getRangeType());
997 std::map
<Node
, std::vector
<Node
> >::iterator itht
= m
->d_ho_uf_terms
.find(f
);
998 if (itht
!= m
->d_ho_uf_terms
.end())
1000 for (size_t i
= 0; i
< itht
->second
.size(); i
++)
1002 Node hn
= itht
->second
[i
];
1003 Trace("model-builder-debug") << " process : " << hn
<< std::endl
;
1004 Assert(hn
.getKind() == kind::HO_APPLY
);
1005 Assert(m
->areEqual(hn
[0], f
));
1006 Node hni
= m
->getRepresentative(hn
[1]);
1007 Trace("model-builder-debug2") << " get rep : " << hn
[0]
1008 << " returned " << hni
<< std::endl
;
1009 Assert(hni
.isConst());
1010 Assert(hni
.getType().isSubtypeOf(args
[0].getType()));
1011 hni
= Rewriter::rewrite(args
[0].eqNode(hni
));
1012 Node hnv
= m
->getRepresentative(hn
);
1013 Trace("model-builder-debug2") << " get rep val : " << hn
1014 << " returned " << hnv
<< std::endl
;
1015 Assert(hnv
.isConst());
1016 if (!apply_args
.empty())
1018 Assert(hnv
.getKind() == kind::LAMBDA
1019 && hnv
[0].getNumChildren() + 1 == args
.size());
1020 std::vector
<TNode
> largs
;
1021 for (unsigned j
= 0; j
< hnv
[0].getNumChildren(); j
++)
1023 largs
.push_back(hnv
[0][j
]);
1025 Assert(largs
.size() == apply_args
.size());
1026 hnv
= hnv
[1].substitute(
1027 largs
.begin(), largs
.end(), apply_args
.begin(), apply_args
.end());
1028 hnv
= Rewriter::rewrite(hnv
);
1030 Assert(!TypeNode::leastCommonTypeNode(hnv
.getType(), curr
.getType())
1032 curr
= NodeManager::currentNM()->mkNode(kind::ITE
, hni
, hnv
, curr
);
1035 Node val
= NodeManager::currentNM()->mkNode(
1037 NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
),
1039 m
->assignFunctionDefinition(f
, val
);
1042 // This struct is used to sort terms by the "size" of their type
1043 // The size of the type is the number of nodes in the type, for example
1045 // size of Function( Int, Int ) is 3
1046 // size of Function( Function( Bool, Int ), Int ) is 5
1049 // stores the size of the type
1050 std::map
<TypeNode
, unsigned> d_type_size
;
1051 // get the size of type tn
1052 unsigned getTypeSize(TypeNode tn
)
1054 std::map
<TypeNode
, unsigned>::iterator it
= d_type_size
.find(tn
);
1055 if (it
!= d_type_size
.end())
1062 for (unsigned i
= 0; i
< tn
.getNumChildren(); i
++)
1064 sum
+= getTypeSize(tn
[i
]);
1066 d_type_size
[tn
] = sum
;
1072 // compares the type size of i and j
1073 // returns true iff the size of i is less than that of j
1074 // tiebreaks are determined by node value
1075 bool operator()(Node i
, Node j
)
1077 int si
= getTypeSize(i
.getType());
1078 int sj
= getTypeSize(j
.getType());
1094 void TheoryEngineModelBuilder::assignFunctions(TheoryModel
* m
)
1096 Trace("model-builder") << "Assigning function values..." << std::endl
;
1097 std::vector
<Node
> funcs_to_assign
= m
->getFunctionsToAssign();
1099 if (options::ufHo())
1101 // sort based on type size if higher-order
1102 Trace("model-builder") << "Sort functions by type..." << std::endl
;
1104 std::sort(funcs_to_assign
.begin(), funcs_to_assign
.end(), sts
);
1107 if (Trace
.isOn("model-builder"))
1109 Trace("model-builder") << "...have " << funcs_to_assign
.size()
1110 << " functions to assign:" << std::endl
;
1111 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1113 Node f
= funcs_to_assign
[k
];
1114 Trace("model-builder") << " [" << k
<< "] : " << f
<< " : "
1115 << f
.getType() << std::endl
;
1119 // construct function values
1120 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1122 Node f
= funcs_to_assign
[k
];
1123 Trace("model-builder") << " Function #" << k
<< " is " << f
<< std::endl
;
1124 // std::map< Node, std::vector< Node > >::iterator itht =
1125 // m->d_ho_uf_terms.find( f );
1126 if (!options::ufHo())
1128 Trace("model-builder") << " Assign function value for " << f
1129 << " based on APPLY_UF" << std::endl
;
1130 assignFunction(m
, f
);
1134 Trace("model-builder") << " Assign function value for " << f
1135 << " based on curried HO_APPLY" << std::endl
;
1136 assignHoFunction(m
, f
);
1139 Trace("model-builder") << "Finished assigning function values." << std::endl
;
1142 } /* namespace CVC4::theory */
1143 } /* namespace CVC4 */