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;
289 tm
->d_modelBuiltSuccess
= false;
291 // Collect model info from the theories
292 Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
294 if (!d_te
->collectModelInfo(tm
))
299 // model-builder specific initialization
300 if (!preProcessBuildModel(tm
))
305 // Loop through all terms and make sure that assignable sub-terms are in the
307 // Also, record #eqc per type (for finite model finding)
308 std::map
<TypeNode
, unsigned> eqc_usort_count
;
309 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
312 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
314 eq::EqClassIterator eqc_i
=
315 eq::EqClassIterator((*eqcs_i
), tm
->d_equalityEngine
);
316 for (; !eqc_i
.isFinished(); ++eqc_i
)
318 addAssignableSubterms(*eqc_i
, tm
, cache
);
320 TypeNode tn
= (*eqcs_i
).getType();
323 if (eqc_usort_count
.find(tn
) == eqc_usort_count
.end())
325 eqc_usort_count
[tn
] = 1;
329 eqc_usort_count
[tn
]++;
335 Trace("model-builder") << "Collect representatives..." << std::endl
;
337 // Process all terms in the equality engine, store representatives for each EC
338 d_constantReps
.clear();
339 std::map
<Node
, Node
> assertedReps
;
340 TypeSet typeConstSet
, typeRepSet
, typeNoRepSet
;
341 TypeEnumeratorProperties tep
;
342 if (options::finiteModelFind())
344 tep
.d_fixed_usort_card
= true;
345 for (std::map
<TypeNode
, unsigned>::iterator it
= eqc_usort_count
.begin();
346 it
!= eqc_usort_count
.end();
349 Trace("model-builder") << "Fixed bound (#eqc) for " << it
->first
<< " : "
350 << it
->second
<< std::endl
;
351 tep
.d_fixed_card
[it
->first
] = Integer(it
->second
);
353 typeConstSet
.setTypeEnumeratorProperties(&tep
);
355 // AJR: build ordered list of types that ensures that base types are
357 // (I think) this is only strictly necessary for finite model finding +
358 // parametric types instantiated with uninterpreted sorts, but is probably
359 // a good idea to do in general since it leads to models with smaller term
361 std::vector
<TypeNode
> type_list
;
362 eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
363 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
365 // eqc is the equivalence class representative
366 Node eqc
= (*eqcs_i
);
367 Trace("model-builder") << "Processing EC: " << eqc
<< endl
;
368 Assert(tm
->d_equalityEngine
->getRepresentative(eqc
) == eqc
);
369 TypeNode eqct
= eqc
.getType();
370 Assert(assertedReps
.find(eqc
) == assertedReps
.end());
371 Assert(d_constantReps
.find(eqc
) == d_constantReps
.end());
373 // Loop through terms in this EC
375 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
376 for (; !eqc_i
.isFinished(); ++eqc_i
)
379 Trace("model-builder") << " Processing Term: " << n
<< endl
;
380 // Record as rep if this node was specified as a representative
381 if (tm
->d_reps
.find(n
) != tm
->d_reps
.end())
383 // AJR: I believe this assertion is too strict,
384 // e.g. datatypes may assert representative for two constructor terms
385 // that are not in the care graph and are merged during
387 // Assert(rep.isNull());
389 Assert(!rep
.isNull());
390 Trace("model-builder") << " Rep( " << eqc
<< " ) = " << rep
393 // Record as const_rep if this node is constant
396 Assert(const_rep
.isNull());
398 Trace("model-builder") << " ConstRep( " << eqc
<< " ) = " << const_rep
401 // model-specific processing of the term
402 tm
->addTermInternal(n
);
405 // Assign representative for this EC
406 if (!const_rep
.isNull())
408 // Theories should not specify a rep if there is already a constant in the
410 // AJR: I believe this assertion is too strict, eqc with asserted reps may
411 // merge with constant eqc
412 // Assert(rep.isNull() || rep == const_rep);
413 assignConstantRep(tm
, eqc
, const_rep
);
414 typeConstSet
.add(eqct
.getBaseType(), const_rep
);
416 else if (!rep
.isNull())
418 assertedReps
[eqc
] = rep
;
419 typeRepSet
.add(eqct
.getBaseType(), eqc
);
420 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
421 addToTypeList(eqct
.getBaseType(), type_list
, visiting
);
425 typeNoRepSet
.add(eqct
, eqc
);
426 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
427 addToTypeList(eqct
, type_list
, visiting
);
431 // Need to ensure that each EC has a constant representative.
433 Trace("model-builder") << "Processing EC's..." << std::endl
;
435 TypeSet::iterator it
;
436 vector
<TypeNode
>::iterator type_it
;
437 set
<Node
>::iterator i
, i2
;
438 bool changed
, unassignedAssignable
, assignOne
= false;
439 set
<TypeNode
> evaluableSet
;
441 // Double-fixed-point loop
442 // Outer loop handles a special corner case (see code at end of loop for
446 // Inner fixed-point loop: we are trying to learn constant values for every
447 // EC. Each time through this loop, we process all of the
448 // types by type and may learn some new EC values. EC's in one type may
449 // depend on EC's in another type, so we need a fixed-point loop
450 // to ensure that we learn as many EC values as possible
454 unassignedAssignable
= false;
455 evaluableSet
.clear();
457 // Iterate over all types we've seen
458 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
460 TypeNode t
= *type_it
;
461 TypeNode tb
= t
.getBaseType();
462 set
<Node
>* noRepSet
= typeNoRepSet
.getSet(t
);
464 // 1. Try to evaluate the EC's in this type
465 if (noRepSet
!= NULL
&& !noRepSet
->empty())
467 Trace("model-builder") << " Eval phase, working on type: " << t
469 bool assignable
, evaluable
, evaluated
;
470 d_normalizedCache
.clear();
471 for (i
= noRepSet
->begin(); i
!= noRepSet
->end();)
478 Trace("model-builder-debug") << "Look at eqc : " << (*i2
)
480 eq::EqClassIterator eqc_i
=
481 eq::EqClassIterator(*i2
, tm
->d_equalityEngine
);
482 for (; !eqc_i
.isFinished(); ++eqc_i
)
485 Trace("model-builder-debug") << "Look at term : " << n
490 Trace("model-builder-debug") << "...assignable" << std::endl
;
495 Trace("model-builder-debug") << "...try to normalize"
497 Node normalized
= normalize(tm
, n
, true);
498 if (normalized
.isConst())
500 typeConstSet
.add(tb
, normalized
);
501 assignConstantRep(tm
, *i2
, normalized
);
502 Trace("model-builder") << " Eval: Setting constant rep of "
503 << (*i2
) << " to " << normalized
516 evaluableSet
.insert(tb
);
520 unassignedAssignable
= true;
526 // 2. Normalize any non-const representative terms for this type
527 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
528 if (repSet
!= NULL
&& !repSet
->empty())
530 Trace("model-builder")
531 << " Normalization phase, working on type: " << t
<< endl
;
532 d_normalizedCache
.clear();
533 for (i
= repSet
->begin(); i
!= repSet
->end();)
535 Assert(assertedReps
.find(*i
) != assertedReps
.end());
536 Node rep
= assertedReps
[*i
];
537 Node normalized
= normalize(tm
, rep
, false);
538 Trace("model-builder") << " Normalizing rep (" << rep
539 << "), normalized to (" << normalized
<< ")"
541 if (normalized
.isConst())
544 typeConstSet
.add(tb
, normalized
);
545 assignConstantRep(tm
, *i
, normalized
);
546 assertedReps
.erase(*i
);
553 if (normalized
!= rep
)
555 assertedReps
[*i
] = normalized
;
565 if (!unassignedAssignable
)
570 // 3. Assign unassigned assignable EC's using type enumeration - assign a
571 // value *different* from all other EC's if the type is infinite
572 // Assign first value from type enumerator otherwise - for finite types, we
573 // rely on polite framework to ensure that EC's that have to be
574 // different are different.
576 // Only make assignments on a type if:
577 // 1. there are no terms that share the same base type with un-normalized
579 // 2. there are no terms that share teh same base type that are unevaluated
581 // Alternatively, if 2 or 3 don't hold but we are in a special
582 // deadlock-breaking mode where assignOne is true, go ahead and make one
585 // must iterate over the ordered type list to ensure that we do not
586 // enumerate values with subterms
587 // having types that we are currently enumerating (when possible)
588 // for example, this ensures we enumerate uninterpreted sort U before (List
589 // of U) and (Array U U)
590 // however, it does not break cyclic type dependencies for mutually
591 // recursive datatypes, but this is handled
592 // by recording all subterms of enumerated values in TypeSet::addSubTerms.
593 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
595 TypeNode t
= *type_it
;
596 // continue if there are no more equivalence classes of this type to
598 std::set
<Node
>* noRepSetPtr
= typeNoRepSet
.getSet(t
);
599 if (noRepSetPtr
== NULL
)
603 set
<Node
>& noRepSet
= *noRepSetPtr
;
604 if (noRepSet
.empty())
609 // get properties of this type
610 bool isCorecursive
= false;
613 const Datatype
& dt
= ((DatatypeType
)(t
).toType()).getDatatype();
615 dt
.isCodatatype() && (!dt
.isFinite(t
.toType())
616 || dt
.isRecursiveSingleton(t
.toType()));
618 #ifdef CVC4_ASSERTIONS
619 bool isUSortFiniteRestricted
= false;
620 if (options::finiteModelFind())
622 isUSortFiniteRestricted
= !t
.isSort() && involvesUSort(t
);
626 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
627 TypeNode tb
= t
.getBaseType();
630 set
<Node
>* repSet
= typeRepSet
.getSet(tb
);
631 if (repSet
!= NULL
&& !repSet
->empty())
635 if (evaluableSet
.find(tb
) != evaluableSet
.end())
640 Trace("model-builder") << " Assign phase, working on type: " << t
642 bool assignable
, evaluable CVC4_UNUSED
;
643 for (i
= noRepSet
.begin(); i
!= noRepSet
.end();)
647 eq::EqClassIterator eqc_i
=
648 eq::EqClassIterator(*i2
, tm
->d_equalityEngine
);
651 for (; !eqc_i
.isFinished(); ++eqc_i
)
663 Trace("model-builder-debug")
664 << " eqc " << *i2
<< " is assignable=" << assignable
665 << ", evaluable=" << evaluable
<< std::endl
;
668 Assert(!evaluable
|| assignOne
);
669 Assert(!t
.isBoolean() || (*i2
).getKind() == kind::APPLY_UF
);
671 if (t
.getCardinality().isInfinite())
673 // if (!t.isInterpretedFinite()) {
677 Trace("model-builder-debug") << "Enumerate term of type " << t
679 n
= typeConstSet
.nextTypeEnum(t
, true);
680 //--- AJR: this code checks whether n is a legal value
683 Trace("model-builder-debug") << "Check if excluded : " << n
685 #ifdef CVC4_ASSERTIONS
686 if (isUSortFiniteRestricted
)
688 // must not involve uninterpreted constants beyond cardinality
689 // bound (which assumed to coincide with #eqc)
690 // this is just an assertion now, since TypeEnumeratorProperties
691 // should ensure that only legal values are enumerated wrt this
693 std::map
<Node
, bool> visited
;
694 success
= !isExcludedUSortValue(eqc_usort_count
, n
, visited
);
697 Trace("model-builder")
698 << "Excluded value for " << t
<< " : " << n
699 << " due to out of range uninterpreted constant."
705 if (success
&& isCorecursive
)
707 if (repSet
!= NULL
&& !repSet
->empty())
709 // in the case of codatatypes, check if it is in the set of
710 // values that we cannot assign
711 success
= !isExcludedCdtValue(n
, repSet
, assertedReps
, *i2
);
714 Trace("model-builder")
715 << "Excluded value : " << n
716 << " due to alpha-equivalent codatatype expression."
726 TypeEnumerator
te(t
);
730 assignConstantRep(tm
, *i2
, n
);
742 // Corner case - I'm not sure this can even happen - but it's theoretically
743 // possible to have a cyclical dependency
744 // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
745 // this case, neither one will get assigned because we are waiting
746 // to be able to evaluate. But we will never be able to evaluate because
747 // the variables that need to be assigned are in
748 // these same EC's. In this case, repeat the whole fixed-point computation
749 // with the difference that the first EC
750 // that has both assignable and evaluable expressions will get assigned.
753 Assert(!assignOne
); // check for infinite loop!
758 #ifdef CVC4_ASSERTIONS
759 // Assert that all representatives have been converted to constants
760 for (it
= typeRepSet
.begin(); it
!= typeRepSet
.end(); ++it
)
762 set
<Node
>& repSet
= TypeSet::getSet(it
);
765 Trace("model-builder") << "***Non-empty repSet, size = " << repSet
.size()
766 << ", first = " << *(repSet
.begin()) << endl
;
770 #endif /* CVC4_ASSERTIONS */
772 Trace("model-builder") << "Copy representatives to model..." << std::endl
;
774 std::map
<Node
, Node
>::iterator itMap
;
775 for (itMap
= d_constantReps
.begin(); itMap
!= d_constantReps
.end(); ++itMap
)
777 tm
->d_reps
[itMap
->first
] = itMap
->second
;
778 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
781 Trace("model-builder") << "Make sure ECs have reps..." << std::endl
;
782 // Make sure every EC has a rep
783 for (itMap
= assertedReps
.begin(); itMap
!= assertedReps
.end(); ++itMap
)
785 tm
->d_reps
[itMap
->first
] = itMap
->second
;
786 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
788 for (it
= typeNoRepSet
.begin(); it
!= typeNoRepSet
.end(); ++it
)
790 set
<Node
>& noRepSet
= TypeSet::getSet(it
);
791 set
<Node
>::iterator i
;
792 for (i
= noRepSet
.begin(); i
!= noRepSet
.end(); ++i
)
795 tm
->d_rep_set
.add((*i
).getType(), *i
);
799 // modelBuilder-specific initialization
800 if (!processBuildModel(tm
))
806 tm
->d_modelBuiltSuccess
= true;
811 void TheoryEngineModelBuilder::debugCheckModel(Model
* m
)
813 TheoryModel
* tm
= (TheoryModel
*)m
;
814 #ifdef CVC4_ASSERTIONS
815 Assert(tm
->isBuilt());
816 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
817 std::map
<Node
, Node
>::iterator itMap
;
818 // Check that every term evaluates to its representative in the model
819 for (eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
820 !eqcs_i
.isFinished();
823 // eqc is the equivalence class representative
824 Node eqc
= (*eqcs_i
);
825 // get the representative
826 Node rep
= tm
->getRepresentative(eqc
);
827 if (!rep
.isConst() && eqc
.getType().isBoolean())
829 // if Boolean, it does not necessarily have a constant representative, use
831 rep
= tm
->getValue(eqc
);
832 Assert(rep
.isConst());
834 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
835 for (; !eqc_i
.isFinished(); ++eqc_i
)
838 static int repCheckInstance
= 0;
841 // non-linear mult is not necessarily accurate wrt getValue
842 if (n
.getKind() != kind::NONLINEAR_MULT
)
844 Debug("check-model::rep-checking") << "( " << repCheckInstance
<< ") "
845 << "n: " << n
<< endl
846 << "getValue(n): " << tm
->getValue(n
)
848 << "rep: " << rep
<< endl
;
849 Assert(tm
->getValue(*eqc_i
) == rep
,
850 "run with -d check-model::rep-checking for details");
854 #endif /* CVC4_ASSERTIONS */
856 // builder-specific debugging
860 Node
TheoryEngineModelBuilder::normalize(TheoryModel
* m
, TNode r
, bool evalOnly
)
862 std::map
<Node
, Node
>::iterator itMap
= d_constantReps
.find(r
);
863 if (itMap
!= d_constantReps
.end())
865 return (*itMap
).second
;
867 NodeMap::iterator it
= d_normalizedCache
.find(r
);
868 if (it
!= d_normalizedCache
.end())
872 Trace("model-builder-debug") << "do normalize on " << r
<< std::endl
;
874 if (r
.getNumChildren() > 0)
876 std::vector
<Node
> children
;
877 if (r
.getMetaKind() == kind::metakind::PARAMETERIZED
)
879 children
.push_back(r
.getOperator());
881 bool childrenConst
= true;
882 for (size_t i
= 0; i
< r
.getNumChildren(); ++i
)
888 if (m
->d_equalityEngine
->hasTerm(ri
))
891 d_constantReps
.find(m
->d_equalityEngine
->getRepresentative(ri
));
892 if (itMap
!= d_constantReps
.end())
894 ri
= (*itMap
).second
;
904 ri
= normalize(m
, ri
, evalOnly
);
908 childrenConst
= false;
911 children
.push_back(ri
);
913 retNode
= NodeManager::currentNM()->mkNode(r
.getKind(), children
);
916 retNode
= Rewriter::rewrite(retNode
);
917 Assert(retNode
.getKind() == kind::APPLY_UF
918 || !retNode
.getType().isFirstClass()
919 || retNode
.isConst());
922 d_normalizedCache
[r
] = retNode
;
926 bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel
* m
)
931 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel
* m
)
933 if (m
->areFunctionValuesEnabled())
940 void TheoryEngineModelBuilder::assignFunction(TheoryModel
* m
, Node f
)
942 Assert(!options::ufHo());
943 uf::UfModelTree
ufmt(f
);
945 for (size_t i
= 0; i
< m
->d_uf_terms
[f
].size(); i
++)
947 Node un
= m
->d_uf_terms
[f
][i
];
948 vector
<TNode
> children
;
949 children
.push_back(f
);
950 Trace("model-builder-debug") << " process term : " << un
<< std::endl
;
951 for (size_t j
= 0; j
< un
.getNumChildren(); ++j
)
953 Node rc
= m
->getRepresentative(un
[j
]);
954 Trace("model-builder-debug2") << " get rep : " << un
[j
] << " returned "
956 Assert(rc
.isConst());
957 children
.push_back(rc
);
959 Node simp
= NodeManager::currentNM()->mkNode(un
.getKind(), children
);
960 Node v
= m
->getRepresentative(un
);
961 Trace("model-builder") << " Setting (" << simp
<< ") to (" << v
<< ")"
963 ufmt
.setValue(m
, simp
, v
);
966 if (default_v
.isNull())
968 // choose default value from model if none exists
969 TypeEnumerator
te(f
.getType().getRangeType());
972 ufmt
.setDefaultValue(m
, default_v
);
973 bool condenseFuncValues
= options::condenseFunctionValues();
974 if (condenseFuncValues
)
978 std::stringstream ss
;
979 ss
<< "_arg_" << f
<< "_";
980 Node val
= ufmt
.getFunctionValue(ss
.str().c_str(), condenseFuncValues
);
981 m
->assignFunctionDefinition(f
, val
);
982 // ufmt.debugPrint( std::cout, m );
985 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel
* m
, Node f
)
987 Assert(options::ufHo());
988 TypeNode type
= f
.getType();
989 std::vector
<TypeNode
> argTypes
= type
.getArgTypes();
990 std::vector
<Node
> args
;
991 std::vector
<TNode
> apply_args
;
992 for (unsigned i
= 0; i
< argTypes
.size(); i
++)
994 Node v
= NodeManager::currentNM()->mkBoundVar(argTypes
[i
]);
998 apply_args
.push_back(v
);
1001 // start with the base return value (currently we use the same default value
1002 // for all functions)
1003 TypeEnumerator
te(type
.getRangeType());
1005 std::map
<Node
, std::vector
<Node
> >::iterator itht
= m
->d_ho_uf_terms
.find(f
);
1006 if (itht
!= m
->d_ho_uf_terms
.end())
1008 for (size_t i
= 0; i
< itht
->second
.size(); i
++)
1010 Node hn
= itht
->second
[i
];
1011 Trace("model-builder-debug") << " process : " << hn
<< std::endl
;
1012 Assert(hn
.getKind() == kind::HO_APPLY
);
1013 Assert(m
->areEqual(hn
[0], f
));
1014 Node hni
= m
->getRepresentative(hn
[1]);
1015 Trace("model-builder-debug2") << " get rep : " << hn
[0]
1016 << " returned " << hni
<< std::endl
;
1017 Assert(hni
.isConst());
1018 Assert(hni
.getType().isSubtypeOf(args
[0].getType()));
1019 hni
= Rewriter::rewrite(args
[0].eqNode(hni
));
1020 Node hnv
= m
->getRepresentative(hn
);
1021 Trace("model-builder-debug2") << " get rep val : " << hn
1022 << " returned " << hnv
<< std::endl
;
1023 Assert(hnv
.isConst());
1024 if (!apply_args
.empty())
1026 Assert(hnv
.getKind() == kind::LAMBDA
1027 && hnv
[0].getNumChildren() + 1 == args
.size());
1028 std::vector
<TNode
> largs
;
1029 for (unsigned j
= 0; j
< hnv
[0].getNumChildren(); j
++)
1031 largs
.push_back(hnv
[0][j
]);
1033 Assert(largs
.size() == apply_args
.size());
1034 hnv
= hnv
[1].substitute(
1035 largs
.begin(), largs
.end(), apply_args
.begin(), apply_args
.end());
1036 hnv
= Rewriter::rewrite(hnv
);
1038 Assert(!TypeNode::leastCommonTypeNode(hnv
.getType(), curr
.getType())
1040 curr
= NodeManager::currentNM()->mkNode(kind::ITE
, hni
, hnv
, curr
);
1043 Node val
= NodeManager::currentNM()->mkNode(
1045 NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
),
1047 m
->assignFunctionDefinition(f
, val
);
1050 // This struct is used to sort terms by the "size" of their type
1051 // The size of the type is the number of nodes in the type, for example
1053 // size of Function( Int, Int ) is 3
1054 // size of Function( Function( Bool, Int ), Int ) is 5
1057 // stores the size of the type
1058 std::map
<TypeNode
, unsigned> d_type_size
;
1059 // get the size of type tn
1060 unsigned getTypeSize(TypeNode tn
)
1062 std::map
<TypeNode
, unsigned>::iterator it
= d_type_size
.find(tn
);
1063 if (it
!= d_type_size
.end())
1070 for (unsigned i
= 0; i
< tn
.getNumChildren(); i
++)
1072 sum
+= getTypeSize(tn
[i
]);
1074 d_type_size
[tn
] = sum
;
1080 // compares the type size of i and j
1081 // returns true iff the size of i is less than that of j
1082 // tiebreaks are determined by node value
1083 bool operator()(Node i
, Node j
)
1085 int si
= getTypeSize(i
.getType());
1086 int sj
= getTypeSize(j
.getType());
1102 void TheoryEngineModelBuilder::assignFunctions(TheoryModel
* m
)
1104 if (!options::assignFunctionValues())
1108 Trace("model-builder") << "Assigning function values..." << std::endl
;
1109 std::vector
<Node
> funcs_to_assign
= m
->getFunctionsToAssign();
1111 if (options::ufHo())
1113 // sort based on type size if higher-order
1114 Trace("model-builder") << "Sort functions by type..." << std::endl
;
1116 std::sort(funcs_to_assign
.begin(), funcs_to_assign
.end(), sts
);
1119 if (Trace
.isOn("model-builder"))
1121 Trace("model-builder") << "...have " << funcs_to_assign
.size()
1122 << " functions to assign:" << std::endl
;
1123 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1125 Node f
= funcs_to_assign
[k
];
1126 Trace("model-builder") << " [" << k
<< "] : " << f
<< " : "
1127 << f
.getType() << std::endl
;
1131 // construct function values
1132 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1134 Node f
= funcs_to_assign
[k
];
1135 Trace("model-builder") << " Function #" << k
<< " is " << f
<< std::endl
;
1136 // std::map< Node, std::vector< Node > >::iterator itht =
1137 // m->d_ho_uf_terms.find( f );
1138 if (!options::ufHo())
1140 Trace("model-builder") << " Assign function value for " << f
1141 << " based on APPLY_UF" << std::endl
;
1142 assignFunction(m
, f
);
1146 Trace("model-builder") << " Assign function value for " << f
1147 << " based on curried HO_APPLY" << std::endl
;
1148 assignHoFunction(m
, f
);
1151 Trace("model-builder") << "Finished assigning function values." << std::endl
;
1154 } /* namespace CVC4::theory */
1155 } /* namespace CVC4 */