1 /********************* */
2 /*! \file theory_model_builder.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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 // this assertion ensures that if we are assigning to a term of
670 // Boolean type, then the term is either a variable or an APPLY_UF.
671 // Note we only assign to terms of Boolean type if the term occurs in
672 // a singleton equivalence class; otherwise the term would have been
673 // in the equivalence class of true or false and would not need
675 Assert(!t
.isBoolean() || (*i2
).isVar()
676 || (*i2
).getKind() == kind::APPLY_UF
);
678 if (t
.getCardinality().isInfinite())
680 // if (!t.isInterpretedFinite()) {
684 Trace("model-builder-debug") << "Enumerate term of type " << t
686 n
= typeConstSet
.nextTypeEnum(t
, true);
687 //--- AJR: this code checks whether n is a legal value
690 Trace("model-builder-debug") << "Check if excluded : " << n
692 #ifdef CVC4_ASSERTIONS
693 if (isUSortFiniteRestricted
)
695 // must not involve uninterpreted constants beyond cardinality
696 // bound (which assumed to coincide with #eqc)
697 // this is just an assertion now, since TypeEnumeratorProperties
698 // should ensure that only legal values are enumerated wrt this
700 std::map
<Node
, bool> visited
;
701 success
= !isExcludedUSortValue(eqc_usort_count
, n
, visited
);
704 Trace("model-builder")
705 << "Excluded value for " << t
<< " : " << n
706 << " due to out of range uninterpreted constant."
712 if (success
&& isCorecursive
)
714 if (repSet
!= NULL
&& !repSet
->empty())
716 // in the case of codatatypes, check if it is in the set of
717 // values that we cannot assign
718 success
= !isExcludedCdtValue(n
, repSet
, assertedReps
, *i2
);
721 Trace("model-builder")
722 << "Excluded value : " << n
723 << " due to alpha-equivalent codatatype expression."
733 TypeEnumerator
te(t
);
737 assignConstantRep(tm
, *i2
, n
);
749 // Corner case - I'm not sure this can even happen - but it's theoretically
750 // possible to have a cyclical dependency
751 // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
752 // this case, neither one will get assigned because we are waiting
753 // to be able to evaluate. But we will never be able to evaluate because
754 // the variables that need to be assigned are in
755 // these same EC's. In this case, repeat the whole fixed-point computation
756 // with the difference that the first EC
757 // that has both assignable and evaluable expressions will get assigned.
760 Assert(!assignOne
); // check for infinite loop!
765 #ifdef CVC4_ASSERTIONS
766 // Assert that all representatives have been converted to constants
767 for (it
= typeRepSet
.begin(); it
!= typeRepSet
.end(); ++it
)
769 set
<Node
>& repSet
= TypeSet::getSet(it
);
772 Trace("model-builder") << "***Non-empty repSet, size = " << repSet
.size()
773 << ", first = " << *(repSet
.begin()) << endl
;
777 #endif /* CVC4_ASSERTIONS */
779 Trace("model-builder") << "Copy representatives to model..." << std::endl
;
781 std::map
<Node
, Node
>::iterator itMap
;
782 for (itMap
= d_constantReps
.begin(); itMap
!= d_constantReps
.end(); ++itMap
)
784 tm
->d_reps
[itMap
->first
] = itMap
->second
;
785 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
788 Trace("model-builder") << "Make sure ECs have reps..." << std::endl
;
789 // Make sure every EC has a rep
790 for (itMap
= assertedReps
.begin(); itMap
!= assertedReps
.end(); ++itMap
)
792 tm
->d_reps
[itMap
->first
] = itMap
->second
;
793 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
795 for (it
= typeNoRepSet
.begin(); it
!= typeNoRepSet
.end(); ++it
)
797 set
<Node
>& noRepSet
= TypeSet::getSet(it
);
798 set
<Node
>::iterator i
;
799 for (i
= noRepSet
.begin(); i
!= noRepSet
.end(); ++i
)
802 tm
->d_rep_set
.add((*i
).getType(), *i
);
806 // modelBuilder-specific initialization
807 if (!processBuildModel(tm
))
812 tm
->d_modelBuiltSuccess
= true;
816 void TheoryEngineModelBuilder::postProcessModel(bool incomplete
, Model
* m
)
818 // if we are incomplete, there is no guarantee on the model.
819 // thus, we do not check the model here. (related to #1693).
824 TheoryModel
* tm
= static_cast<TheoryModel
*>(m
);
825 Assert(tm
!= nullptr);
826 // debug-check the model if the checkModels() is enabled.
827 if (options::checkModels())
833 void TheoryEngineModelBuilder::debugCheckModel(TheoryModel
* tm
)
835 #ifdef CVC4_ASSERTIONS
836 Assert(tm
->isBuilt());
837 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
838 std::map
<Node
, Node
>::iterator itMap
;
839 // Check that every term evaluates to its representative in the model
840 for (eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
841 !eqcs_i
.isFinished();
844 // eqc is the equivalence class representative
845 Node eqc
= (*eqcs_i
);
846 // get the representative
847 Node rep
= tm
->getRepresentative(eqc
);
848 if (!rep
.isConst() && eqc
.getType().isBoolean())
850 // if Boolean, it does not necessarily have a constant representative, use
852 rep
= tm
->getValue(eqc
);
853 Assert(rep
.isConst());
855 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
856 for (; !eqc_i
.isFinished(); ++eqc_i
)
859 static int repCheckInstance
= 0;
862 // non-linear mult is not necessarily accurate wrt getValue
863 if (n
.getKind() != kind::NONLINEAR_MULT
)
865 Debug("check-model::rep-checking") << "( " << repCheckInstance
<< ") "
866 << "n: " << n
<< endl
867 << "getValue(n): " << tm
->getValue(n
)
869 << "rep: " << rep
<< endl
;
870 Assert(tm
->getValue(*eqc_i
) == rep
,
871 "run with -d check-model::rep-checking for details");
875 #endif /* CVC4_ASSERTIONS */
877 // builder-specific debugging
881 Node
TheoryEngineModelBuilder::normalize(TheoryModel
* m
, TNode r
, bool evalOnly
)
883 std::map
<Node
, Node
>::iterator itMap
= d_constantReps
.find(r
);
884 if (itMap
!= d_constantReps
.end())
886 return (*itMap
).second
;
888 NodeMap::iterator it
= d_normalizedCache
.find(r
);
889 if (it
!= d_normalizedCache
.end())
893 Trace("model-builder-debug") << "do normalize on " << r
<< std::endl
;
895 if (r
.getNumChildren() > 0)
897 std::vector
<Node
> children
;
898 if (r
.getMetaKind() == kind::metakind::PARAMETERIZED
)
900 children
.push_back(r
.getOperator());
902 bool childrenConst
= true;
903 for (size_t i
= 0; i
< r
.getNumChildren(); ++i
)
909 if (m
->d_equalityEngine
->hasTerm(ri
))
912 d_constantReps
.find(m
->d_equalityEngine
->getRepresentative(ri
));
913 if (itMap
!= d_constantReps
.end())
915 ri
= (*itMap
).second
;
925 ri
= normalize(m
, ri
, evalOnly
);
929 childrenConst
= false;
932 children
.push_back(ri
);
934 retNode
= NodeManager::currentNM()->mkNode(r
.getKind(), children
);
937 retNode
= Rewriter::rewrite(retNode
);
938 Assert(retNode
.getKind() == kind::APPLY_UF
939 || !retNode
.getType().isFirstClass()
940 || retNode
.isConst());
943 d_normalizedCache
[r
] = retNode
;
947 bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel
* m
)
952 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel
* m
)
954 if (m
->areFunctionValuesEnabled())
961 void TheoryEngineModelBuilder::assignFunction(TheoryModel
* m
, Node f
)
963 Assert(!options::ufHo());
964 uf::UfModelTree
ufmt(f
);
966 for (size_t i
= 0; i
< m
->d_uf_terms
[f
].size(); i
++)
968 Node un
= m
->d_uf_terms
[f
][i
];
969 vector
<TNode
> children
;
970 children
.push_back(f
);
971 Trace("model-builder-debug") << " process term : " << un
<< std::endl
;
972 for (size_t j
= 0; j
< un
.getNumChildren(); ++j
)
974 Node rc
= m
->getRepresentative(un
[j
]);
975 Trace("model-builder-debug2") << " get rep : " << un
[j
] << " returned "
977 Assert(rc
.isConst());
978 children
.push_back(rc
);
980 Node simp
= NodeManager::currentNM()->mkNode(un
.getKind(), children
);
981 Node v
= m
->getRepresentative(un
);
982 Trace("model-builder") << " Setting (" << simp
<< ") to (" << v
<< ")"
984 ufmt
.setValue(m
, simp
, v
);
987 if (default_v
.isNull())
989 // choose default value from model if none exists
990 TypeEnumerator
te(f
.getType().getRangeType());
993 ufmt
.setDefaultValue(m
, default_v
);
994 bool condenseFuncValues
= options::condenseFunctionValues();
995 if (condenseFuncValues
)
999 std::stringstream ss
;
1000 ss
<< "_arg_" << f
<< "_";
1001 Node val
= ufmt
.getFunctionValue(ss
.str().c_str(), condenseFuncValues
);
1002 m
->assignFunctionDefinition(f
, val
);
1003 // ufmt.debugPrint( std::cout, m );
1006 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel
* m
, Node f
)
1008 Assert(options::ufHo());
1009 TypeNode type
= f
.getType();
1010 std::vector
<TypeNode
> argTypes
= type
.getArgTypes();
1011 std::vector
<Node
> args
;
1012 std::vector
<TNode
> apply_args
;
1013 for (unsigned i
= 0; i
< argTypes
.size(); i
++)
1015 Node v
= NodeManager::currentNM()->mkBoundVar(argTypes
[i
]);
1019 apply_args
.push_back(v
);
1022 // start with the base return value (currently we use the same default value
1023 // for all functions)
1024 TypeEnumerator
te(type
.getRangeType());
1026 std::map
<Node
, std::vector
<Node
> >::iterator itht
= m
->d_ho_uf_terms
.find(f
);
1027 if (itht
!= m
->d_ho_uf_terms
.end())
1029 for (size_t i
= 0; i
< itht
->second
.size(); i
++)
1031 Node hn
= itht
->second
[i
];
1032 Trace("model-builder-debug") << " process : " << hn
<< std::endl
;
1033 Assert(hn
.getKind() == kind::HO_APPLY
);
1034 Assert(m
->areEqual(hn
[0], f
));
1035 Node hni
= m
->getRepresentative(hn
[1]);
1036 Trace("model-builder-debug2") << " get rep : " << hn
[0]
1037 << " returned " << hni
<< std::endl
;
1038 Assert(hni
.isConst());
1039 Assert(hni
.getType().isSubtypeOf(args
[0].getType()));
1040 hni
= Rewriter::rewrite(args
[0].eqNode(hni
));
1041 Node hnv
= m
->getRepresentative(hn
);
1042 Trace("model-builder-debug2") << " get rep val : " << hn
1043 << " returned " << hnv
<< std::endl
;
1044 Assert(hnv
.isConst());
1045 if (!apply_args
.empty())
1047 Assert(hnv
.getKind() == kind::LAMBDA
1048 && hnv
[0].getNumChildren() + 1 == args
.size());
1049 std::vector
<TNode
> largs
;
1050 for (unsigned j
= 0; j
< hnv
[0].getNumChildren(); j
++)
1052 largs
.push_back(hnv
[0][j
]);
1054 Assert(largs
.size() == apply_args
.size());
1055 hnv
= hnv
[1].substitute(
1056 largs
.begin(), largs
.end(), apply_args
.begin(), apply_args
.end());
1057 hnv
= Rewriter::rewrite(hnv
);
1059 Assert(!TypeNode::leastCommonTypeNode(hnv
.getType(), curr
.getType())
1061 curr
= NodeManager::currentNM()->mkNode(kind::ITE
, hni
, hnv
, curr
);
1064 Node val
= NodeManager::currentNM()->mkNode(
1066 NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
),
1068 m
->assignFunctionDefinition(f
, val
);
1071 // This struct is used to sort terms by the "size" of their type
1072 // The size of the type is the number of nodes in the type, for example
1074 // size of Function( Int, Int ) is 3
1075 // size of Function( Function( Bool, Int ), Int ) is 5
1078 // stores the size of the type
1079 std::map
<TypeNode
, unsigned> d_type_size
;
1080 // get the size of type tn
1081 unsigned getTypeSize(TypeNode tn
)
1083 std::map
<TypeNode
, unsigned>::iterator it
= d_type_size
.find(tn
);
1084 if (it
!= d_type_size
.end())
1091 for (unsigned i
= 0; i
< tn
.getNumChildren(); i
++)
1093 sum
+= getTypeSize(tn
[i
]);
1095 d_type_size
[tn
] = sum
;
1101 // compares the type size of i and j
1102 // returns true iff the size of i is less than that of j
1103 // tiebreaks are determined by node value
1104 bool operator()(Node i
, Node j
)
1106 int si
= getTypeSize(i
.getType());
1107 int sj
= getTypeSize(j
.getType());
1123 void TheoryEngineModelBuilder::assignFunctions(TheoryModel
* m
)
1125 if (!options::assignFunctionValues())
1129 Trace("model-builder") << "Assigning function values..." << std::endl
;
1130 std::vector
<Node
> funcs_to_assign
= m
->getFunctionsToAssign();
1132 if (options::ufHo())
1134 // sort based on type size if higher-order
1135 Trace("model-builder") << "Sort functions by type..." << std::endl
;
1137 std::sort(funcs_to_assign
.begin(), funcs_to_assign
.end(), sts
);
1140 if (Trace
.isOn("model-builder"))
1142 Trace("model-builder") << "...have " << funcs_to_assign
.size()
1143 << " functions to assign:" << std::endl
;
1144 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1146 Node f
= funcs_to_assign
[k
];
1147 Trace("model-builder") << " [" << k
<< "] : " << f
<< " : "
1148 << f
.getType() << std::endl
;
1152 // construct function values
1153 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1155 Node f
= funcs_to_assign
[k
];
1156 Trace("model-builder") << " Function #" << k
<< " is " << f
<< std::endl
;
1157 // std::map< Node, std::vector< Node > >::iterator itht =
1158 // m->d_ho_uf_terms.find( f );
1159 if (!options::ufHo())
1161 Trace("model-builder") << " Assign function value for " << f
1162 << " based on APPLY_UF" << std::endl
;
1163 assignFunction(m
, f
);
1167 Trace("model-builder") << " Assign function value for " << f
1168 << " based on curried HO_APPLY" << std::endl
;
1169 assignHoFunction(m
, f
);
1172 Trace("model-builder") << "Finished assigning function values." << std::endl
;
1175 } /* namespace CVC4::theory */
1176 } /* namespace CVC4 */