1 /********************* */
2 /*! \file theory_model_builder.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Clark Barrett, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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();
50 else if (n
.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGN
)
52 // Extracting the sign of a floating-point number acts similar to a
53 // selector on a datatype, i.e. if `(sign x)` wasn't assigned a value, we
54 // can pick an arbitrary one. Note that the other components of a
55 // floating-point number should always be assigned a value.
60 // non-function variables, and fully applied functions
63 // no functions exist, all functions are fully applied
64 Assert(n
.getKind() != kind::HO_APPLY
);
65 Assert(!n
.getType().isFunction());
66 return n
.isVar() || n
.getKind() == kind::APPLY_UF
;
70 // Assert( n.getKind() != kind::APPLY_UF );
71 return (n
.isVar() && !n
.getType().isFunction())
72 || n
.getKind() == kind::APPLY_UF
73 || (n
.getKind() == kind::HO_APPLY
74 && n
[0].getType().getNumChildren() == 2);
79 void TheoryEngineModelBuilder::addAssignableSubterms(TNode n
,
87 if (cache
.find(n
) != cache
.end())
93 tm
->d_equalityEngine
->addTerm(n
);
95 for (TNode::iterator child_it
= n
.begin(); child_it
!= n
.end(); ++child_it
)
97 addAssignableSubterms(*child_it
, tm
, cache
);
102 void TheoryEngineModelBuilder::assignConstantRep(TheoryModel
* tm
,
106 d_constantReps
[eqc
] = const_rep
;
107 Trace("model-builder") << " Assign: Setting constant rep of " << eqc
108 << " to " << const_rep
<< endl
;
109 tm
->d_rep_set
.setTermForRepresentative(const_rep
, eqc
);
112 bool TheoryEngineModelBuilder::isExcludedCdtValue(
114 std::set
<Node
>* repSet
,
115 std::map
<Node
, Node
>& assertedReps
,
118 Trace("model-builder-debug")
119 << "Is " << val
<< " and excluded codatatype value for " << eqc
<< "? "
121 for (set
<Node
>::iterator i
= repSet
->begin(); i
!= repSet
->end(); ++i
)
123 Assert(assertedReps
.find(*i
) != assertedReps
.end());
124 Node rep
= assertedReps
[*i
];
125 Trace("model-builder-debug") << " Rep : " << rep
<< std::endl
;
126 // check matching val to rep with eqc as a free variable
128 if (isCdtValueMatch(val
, rep
, eqc
, eqc_m
))
130 Trace("model-builder-debug") << " ...matches with " << eqc
<< " -> "
131 << eqc_m
<< std::endl
;
132 if (eqc_m
.getKind() == kind::UNINTERPRETED_CONSTANT
)
134 Trace("model-builder-debug") << "*** " << val
135 << " is excluded datatype for " << eqc
144 bool TheoryEngineModelBuilder::isCdtValueMatch(Node v
,
157 // only if an uninterpreted constant?
166 else if (v
.getKind() == kind::APPLY_CONSTRUCTOR
167 && r
.getKind() == kind::APPLY_CONSTRUCTOR
)
169 if (v
.getOperator() == r
.getOperator())
171 for (unsigned i
= 0; i
< v
.getNumChildren(); i
++)
173 if (!isCdtValueMatch(v
[i
], r
[i
], eqc
, eqc_m
))
184 bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn
)
190 else if (tn
.isArray())
192 return involvesUSort(tn
.getArrayIndexType())
193 || involvesUSort(tn
.getArrayConstituentType());
197 return involvesUSort(tn
.getSetElementType());
199 else if (tn
.isDatatype())
201 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
202 return dt
.involvesUninterpretedType();
210 bool TheoryEngineModelBuilder::isExcludedUSortValue(
211 std::map
<TypeNode
, unsigned>& eqc_usort_count
,
213 std::map
<Node
, bool>& visited
)
216 if (visited
.find(v
) == visited
.end())
219 TypeNode tn
= v
.getType();
222 Trace("model-builder-debug") << "Is excluded usort value : " << v
<< " "
224 unsigned card
= eqc_usort_count
[tn
];
225 Trace("model-builder-debug") << " Cardinality is " << card
<< std::endl
;
227 v
.getConst
<UninterpretedConstant
>().getIndex().toUnsignedInt();
228 Trace("model-builder-debug") << " Index is " << index
<< std::endl
;
229 return index
> 0 && index
>= card
;
231 for (unsigned i
= 0; i
< v
.getNumChildren(); i
++)
233 if (isExcludedUSortValue(eqc_usort_count
, v
[i
], visited
))
242 void TheoryEngineModelBuilder::addToTypeList(
244 std::vector
<TypeNode
>& type_list
,
245 std::unordered_set
<TypeNode
, TypeNodeHashFunction
>& visiting
)
247 if (std::find(type_list
.begin(), type_list
.end(), tn
) == type_list
.end())
249 if (visiting
.find(tn
) == visiting
.end())
252 /* This must make a recursive call on all types that are subterms of
253 * values of the current type.
254 * Note that recursive traversal here is over enumerated expressions
255 * (very low expression depth). */
258 addToTypeList(tn
.getArrayIndexType(), type_list
, visiting
);
259 addToTypeList(tn
.getArrayConstituentType(), type_list
, visiting
);
263 addToTypeList(tn
.getSetElementType(), type_list
, visiting
);
265 else if (tn
.isDatatype())
267 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
268 for (unsigned i
= 0; i
< dt
.getNumConstructors(); i
++)
270 for (unsigned j
= 0; j
< dt
[i
].getNumArgs(); j
++)
272 TypeNode ctn
= TypeNode::fromType(dt
[i
][j
].getRangeType());
273 addToTypeList(ctn
, type_list
, visiting
);
277 Assert(std::find(type_list
.begin(), type_list
.end(), tn
)
279 type_list
.push_back(tn
);
284 bool TheoryEngineModelBuilder::buildModel(Model
* m
)
286 Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl
;
287 TheoryModel
* tm
= (TheoryModel
*)m
;
289 // buildModel should only be called once per check
290 Assert(!tm
->isBuilt());
296 tm
->d_modelBuilt
= true;
297 tm
->d_modelBuiltSuccess
= false;
299 // Collect model info from the theories
300 Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
302 if (!d_te
->collectModelInfo(tm
))
307 // model-builder specific initialization
308 if (!preProcessBuildModel(tm
))
313 // Loop through all terms and make sure that assignable sub-terms are in the
315 // Also, record #eqc per type (for finite model finding)
316 std::map
<TypeNode
, unsigned> eqc_usort_count
;
317 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
320 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
322 eq::EqClassIterator eqc_i
=
323 eq::EqClassIterator((*eqcs_i
), tm
->d_equalityEngine
);
324 for (; !eqc_i
.isFinished(); ++eqc_i
)
326 addAssignableSubterms(*eqc_i
, tm
, cache
);
328 TypeNode tn
= (*eqcs_i
).getType();
331 if (eqc_usort_count
.find(tn
) == eqc_usort_count
.end())
333 eqc_usort_count
[tn
] = 1;
337 eqc_usort_count
[tn
]++;
343 Trace("model-builder") << "Collect representatives..." << std::endl
;
345 // Process all terms in the equality engine, store representatives for each EC
346 d_constantReps
.clear();
347 std::map
<Node
, Node
> assertedReps
;
348 TypeSet typeConstSet
, typeRepSet
, typeNoRepSet
;
349 TypeEnumeratorProperties tep
;
350 if (options::finiteModelFind())
352 tep
.d_fixed_usort_card
= true;
353 for (std::map
<TypeNode
, unsigned>::iterator it
= eqc_usort_count
.begin();
354 it
!= eqc_usort_count
.end();
357 Trace("model-builder") << "Fixed bound (#eqc) for " << it
->first
<< " : "
358 << it
->second
<< std::endl
;
359 tep
.d_fixed_card
[it
->first
] = Integer(it
->second
);
361 typeConstSet
.setTypeEnumeratorProperties(&tep
);
363 // AJR: build ordered list of types that ensures that base types are
365 // (I think) this is only strictly necessary for finite model finding +
366 // parametric types instantiated with uninterpreted sorts, but is probably
367 // a good idea to do in general since it leads to models with smaller term
369 std::vector
<TypeNode
> type_list
;
370 eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
371 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
373 // eqc is the equivalence class representative
374 Node eqc
= (*eqcs_i
);
375 Trace("model-builder") << "Processing EC: " << eqc
<< endl
;
376 Assert(tm
->d_equalityEngine
->getRepresentative(eqc
) == eqc
);
377 TypeNode eqct
= eqc
.getType();
378 Assert(assertedReps
.find(eqc
) == assertedReps
.end());
379 Assert(d_constantReps
.find(eqc
) == d_constantReps
.end());
381 // Loop through terms in this EC
383 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
384 for (; !eqc_i
.isFinished(); ++eqc_i
)
387 Trace("model-builder") << " Processing Term: " << n
<< endl
;
388 // Record as rep if this node was specified as a representative
389 if (tm
->d_reps
.find(n
) != tm
->d_reps
.end())
391 // AJR: I believe this assertion is too strict,
392 // e.g. datatypes may assert representative for two constructor terms
393 // that are not in the care graph and are merged during
395 // Assert(rep.isNull());
397 Assert(!rep
.isNull());
398 Trace("model-builder") << " Rep( " << eqc
<< " ) = " << rep
401 // Record as const_rep if this node is constant
404 Assert(const_rep
.isNull());
406 Trace("model-builder") << " ConstRep( " << eqc
<< " ) = " << const_rep
409 // model-specific processing of the term
410 tm
->addTermInternal(n
);
413 // Assign representative for this EC
414 if (!const_rep
.isNull())
416 // Theories should not specify a rep if there is already a constant in the
418 // AJR: I believe this assertion is too strict, eqc with asserted reps may
419 // merge with constant eqc
420 // Assert(rep.isNull() || rep == const_rep);
421 assignConstantRep(tm
, eqc
, const_rep
);
422 typeConstSet
.add(eqct
.getBaseType(), const_rep
);
424 else if (!rep
.isNull())
426 assertedReps
[eqc
] = rep
;
427 typeRepSet
.add(eqct
.getBaseType(), eqc
);
428 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
429 addToTypeList(eqct
.getBaseType(), type_list
, visiting
);
433 typeNoRepSet
.add(eqct
, eqc
);
434 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
435 addToTypeList(eqct
, type_list
, visiting
);
439 // Need to ensure that each EC has a constant representative.
441 Trace("model-builder") << "Processing EC's..." << std::endl
;
443 TypeSet::iterator it
;
444 vector
<TypeNode
>::iterator type_it
;
445 set
<Node
>::iterator i
, i2
;
446 bool changed
, unassignedAssignable
, assignOne
= false;
447 set
<TypeNode
> evaluableSet
;
449 // Double-fixed-point loop
450 // Outer loop handles a special corner case (see code at end of loop for
454 // Inner fixed-point loop: we are trying to learn constant values for every
455 // EC. Each time through this loop, we process all of the
456 // types by type and may learn some new EC values. EC's in one type may
457 // depend on EC's in another type, so we need a fixed-point loop
458 // to ensure that we learn as many EC values as possible
462 unassignedAssignable
= false;
463 evaluableSet
.clear();
465 // Iterate over all types we've seen
466 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
468 TypeNode t
= *type_it
;
469 TypeNode tb
= t
.getBaseType();
470 set
<Node
>* noRepSet
= typeNoRepSet
.getSet(t
);
472 // 1. Try to evaluate the EC's in this type
473 if (noRepSet
!= NULL
&& !noRepSet
->empty())
475 Trace("model-builder") << " Eval phase, working on type: " << t
477 bool assignable
, evaluable
, evaluated
;
478 d_normalizedCache
.clear();
479 for (i
= noRepSet
->begin(); i
!= noRepSet
->end();)
486 Trace("model-builder-debug") << "Look at eqc : " << (*i2
)
488 eq::EqClassIterator eqc_i
=
489 eq::EqClassIterator(*i2
, tm
->d_equalityEngine
);
490 for (; !eqc_i
.isFinished(); ++eqc_i
)
493 Trace("model-builder-debug") << "Look at term : " << n
498 Trace("model-builder-debug") << "...assignable" << std::endl
;
503 Trace("model-builder-debug") << "...try to normalize"
505 Node normalized
= normalize(tm
, n
, true);
506 if (normalized
.isConst())
508 typeConstSet
.add(tb
, normalized
);
509 assignConstantRep(tm
, *i2
, normalized
);
510 Trace("model-builder") << " Eval: Setting constant rep of "
511 << (*i2
) << " to " << normalized
524 evaluableSet
.insert(tb
);
528 unassignedAssignable
= true;
534 // 2. Normalize any non-const representative terms for this type
535 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
536 if (repSet
!= NULL
&& !repSet
->empty())
538 Trace("model-builder")
539 << " Normalization phase, working on type: " << t
<< endl
;
540 d_normalizedCache
.clear();
541 for (i
= repSet
->begin(); i
!= repSet
->end();)
543 Assert(assertedReps
.find(*i
) != assertedReps
.end());
544 Node rep
= assertedReps
[*i
];
545 Node normalized
= normalize(tm
, rep
, false);
546 Trace("model-builder") << " Normalizing rep (" << rep
547 << "), normalized to (" << normalized
<< ")"
549 if (normalized
.isConst())
552 typeConstSet
.add(tb
, normalized
);
553 assignConstantRep(tm
, *i
, normalized
);
554 assertedReps
.erase(*i
);
561 if (normalized
!= rep
)
563 assertedReps
[*i
] = normalized
;
573 if (!unassignedAssignable
)
578 // 3. Assign unassigned assignable EC's using type enumeration - assign a
579 // value *different* from all other EC's if the type is infinite
580 // Assign first value from type enumerator otherwise - for finite types, we
581 // rely on polite framework to ensure that EC's that have to be
582 // different are different.
584 // Only make assignments on a type if:
585 // 1. there are no terms that share the same base type with un-normalized
587 // 2. there are no terms that share teh same base type that are unevaluated
589 // Alternatively, if 2 or 3 don't hold but we are in a special
590 // deadlock-breaking mode where assignOne is true, go ahead and make one
593 // must iterate over the ordered type list to ensure that we do not
594 // enumerate values with subterms
595 // having types that we are currently enumerating (when possible)
596 // for example, this ensures we enumerate uninterpreted sort U before (List
597 // of U) and (Array U U)
598 // however, it does not break cyclic type dependencies for mutually
599 // recursive datatypes, but this is handled
600 // by recording all subterms of enumerated values in TypeSet::addSubTerms.
601 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
603 TypeNode t
= *type_it
;
604 // continue if there are no more equivalence classes of this type to
606 std::set
<Node
>* noRepSetPtr
= typeNoRepSet
.getSet(t
);
607 if (noRepSetPtr
== NULL
)
611 set
<Node
>& noRepSet
= *noRepSetPtr
;
612 if (noRepSet
.empty())
617 // get properties of this type
618 bool isCorecursive
= false;
621 const Datatype
& dt
= ((DatatypeType
)(t
).toType()).getDatatype();
623 dt
.isCodatatype() && (!dt
.isFinite(t
.toType())
624 || dt
.isRecursiveSingleton(t
.toType()));
626 #ifdef CVC4_ASSERTIONS
627 bool isUSortFiniteRestricted
= false;
628 if (options::finiteModelFind())
630 isUSortFiniteRestricted
= !t
.isSort() && involvesUSort(t
);
634 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
635 TypeNode tb
= t
.getBaseType();
638 set
<Node
>* repSet
= typeRepSet
.getSet(tb
);
639 if (repSet
!= NULL
&& !repSet
->empty())
643 if (evaluableSet
.find(tb
) != evaluableSet
.end())
648 Trace("model-builder") << " Assign phase, working on type: " << t
650 bool assignable
, evaluable CVC4_UNUSED
;
651 for (i
= noRepSet
.begin(); i
!= noRepSet
.end();)
655 eq::EqClassIterator eqc_i
=
656 eq::EqClassIterator(*i2
, tm
->d_equalityEngine
);
659 for (; !eqc_i
.isFinished(); ++eqc_i
)
671 Trace("model-builder-debug")
672 << " eqc " << *i2
<< " is assignable=" << assignable
673 << ", evaluable=" << evaluable
<< std::endl
;
676 Assert(!evaluable
|| assignOne
);
677 // this assertion ensures that if we are assigning to a term of
678 // Boolean type, then the term is either a variable or an APPLY_UF.
679 // Note we only assign to terms of Boolean type if the term occurs in
680 // a singleton equivalence class; otherwise the term would have been
681 // in the equivalence class of true or false and would not need
683 Assert(!t
.isBoolean() || (*i2
).isVar()
684 || (*i2
).getKind() == kind::APPLY_UF
);
691 Trace("model-builder-debug") << "Enumerate term of type " << t
693 n
= typeConstSet
.nextTypeEnum(t
, true);
694 //--- AJR: this code checks whether n is a legal value
697 Trace("model-builder-debug") << "Check if excluded : " << n
699 #ifdef CVC4_ASSERTIONS
700 if (isUSortFiniteRestricted
)
702 // must not involve uninterpreted constants beyond cardinality
703 // bound (which assumed to coincide with #eqc)
704 // this is just an assertion now, since TypeEnumeratorProperties
705 // should ensure that only legal values are enumerated wrt this
707 std::map
<Node
, bool> visited
;
708 success
= !isExcludedUSortValue(eqc_usort_count
, n
, visited
);
711 Trace("model-builder")
712 << "Excluded value for " << t
<< " : " << n
713 << " due to out of range uninterpreted constant."
719 if (success
&& isCorecursive
)
721 if (repSet
!= NULL
&& !repSet
->empty())
723 // in the case of codatatypes, check if it is in the set of
724 // values that we cannot assign
725 success
= !isExcludedCdtValue(n
, repSet
, assertedReps
, *i2
);
728 Trace("model-builder")
729 << "Excluded value : " << n
730 << " due to alpha-equivalent codatatype expression."
740 TypeEnumerator
te(t
);
744 assignConstantRep(tm
, *i2
, n
);
756 // Corner case - I'm not sure this can even happen - but it's theoretically
757 // possible to have a cyclical dependency
758 // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
759 // this case, neither one will get assigned because we are waiting
760 // to be able to evaluate. But we will never be able to evaluate because
761 // the variables that need to be assigned are in
762 // these same EC's. In this case, repeat the whole fixed-point computation
763 // with the difference that the first EC
764 // that has both assignable and evaluable expressions will get assigned.
767 Assert(!assignOne
); // check for infinite loop!
772 #ifdef CVC4_ASSERTIONS
773 // Assert that all representatives have been converted to constants
774 for (it
= typeRepSet
.begin(); it
!= typeRepSet
.end(); ++it
)
776 set
<Node
>& repSet
= TypeSet::getSet(it
);
779 Trace("model-builder") << "***Non-empty repSet, size = " << repSet
.size()
780 << ", first = " << *(repSet
.begin()) << endl
;
784 #endif /* CVC4_ASSERTIONS */
786 Trace("model-builder") << "Copy representatives to model..." << std::endl
;
788 std::map
<Node
, Node
>::iterator itMap
;
789 for (itMap
= d_constantReps
.begin(); itMap
!= d_constantReps
.end(); ++itMap
)
791 tm
->d_reps
[itMap
->first
] = itMap
->second
;
792 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
795 Trace("model-builder") << "Make sure ECs have reps..." << std::endl
;
796 // Make sure every EC has a rep
797 for (itMap
= assertedReps
.begin(); itMap
!= assertedReps
.end(); ++itMap
)
799 tm
->d_reps
[itMap
->first
] = itMap
->second
;
800 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
802 for (it
= typeNoRepSet
.begin(); it
!= typeNoRepSet
.end(); ++it
)
804 set
<Node
>& noRepSet
= TypeSet::getSet(it
);
805 set
<Node
>::iterator i
;
806 for (i
= noRepSet
.begin(); i
!= noRepSet
.end(); ++i
)
809 tm
->d_rep_set
.add((*i
).getType(), *i
);
813 // modelBuilder-specific initialization
814 if (!processBuildModel(tm
))
819 tm
->d_modelBuiltSuccess
= true;
823 void TheoryEngineModelBuilder::postProcessModel(bool incomplete
, Model
* m
)
825 // if we are incomplete, there is no guarantee on the model.
826 // thus, we do not check the model here.
831 TheoryModel
* tm
= static_cast<TheoryModel
*>(m
);
832 Assert(tm
!= nullptr);
833 // debug-check the model if the checkModels() is enabled.
834 if (options::checkModels())
840 void TheoryEngineModelBuilder::debugCheckModel(TheoryModel
* tm
)
842 #ifdef CVC4_ASSERTIONS
843 Assert(tm
->isBuilt());
844 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
845 std::map
<Node
, Node
>::iterator itMap
;
846 // Check that every term evaluates to its representative in the model
847 for (eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
848 !eqcs_i
.isFinished();
851 // eqc is the equivalence class representative
852 Node eqc
= (*eqcs_i
);
853 // get the representative
854 Node rep
= tm
->getRepresentative(eqc
);
855 if (!rep
.isConst() && eqc
.getType().isBoolean())
857 // if Boolean, it does not necessarily have a constant representative, use
859 rep
= tm
->getValue(eqc
);
860 Assert(rep
.isConst());
862 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
863 for (; !eqc_i
.isFinished(); ++eqc_i
)
866 static int repCheckInstance
= 0;
869 // non-linear mult is not necessarily accurate wrt getValue
870 if (n
.getKind() != kind::NONLINEAR_MULT
)
872 Debug("check-model::rep-checking") << "( " << repCheckInstance
<< ") "
873 << "n: " << n
<< endl
874 << "getValue(n): " << tm
->getValue(n
)
876 << "rep: " << rep
<< endl
;
877 Assert(tm
->getValue(*eqc_i
) == rep
,
878 "run with -d check-model::rep-checking for details");
882 #endif /* CVC4_ASSERTIONS */
884 // builder-specific debugging
888 Node
TheoryEngineModelBuilder::normalize(TheoryModel
* m
, TNode r
, bool evalOnly
)
890 std::map
<Node
, Node
>::iterator itMap
= d_constantReps
.find(r
);
891 if (itMap
!= d_constantReps
.end())
893 return (*itMap
).second
;
895 NodeMap::iterator it
= d_normalizedCache
.find(r
);
896 if (it
!= d_normalizedCache
.end())
900 Trace("model-builder-debug") << "do normalize on " << r
<< std::endl
;
902 if (r
.getNumChildren() > 0)
904 std::vector
<Node
> children
;
905 if (r
.getMetaKind() == kind::metakind::PARAMETERIZED
)
907 children
.push_back(r
.getOperator());
909 bool childrenConst
= true;
910 for (size_t i
= 0; i
< r
.getNumChildren(); ++i
)
916 if (m
->d_equalityEngine
->hasTerm(ri
))
919 d_constantReps
.find(m
->d_equalityEngine
->getRepresentative(ri
));
920 if (itMap
!= d_constantReps
.end())
922 ri
= (*itMap
).second
;
932 ri
= normalize(m
, ri
, evalOnly
);
936 childrenConst
= false;
939 children
.push_back(ri
);
941 retNode
= NodeManager::currentNM()->mkNode(r
.getKind(), children
);
944 retNode
= Rewriter::rewrite(retNode
);
945 Assert(retNode
.getKind() == kind::APPLY_UF
946 || !retNode
.getType().isFirstClass()
947 || retNode
.isConst());
950 d_normalizedCache
[r
] = retNode
;
954 bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel
* m
)
959 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel
* m
)
961 if (m
->areFunctionValuesEnabled())
968 void TheoryEngineModelBuilder::assignFunction(TheoryModel
* m
, Node f
)
970 Assert(!options::ufHo());
971 uf::UfModelTree
ufmt(f
);
973 for (size_t i
= 0; i
< m
->d_uf_terms
[f
].size(); i
++)
975 Node un
= m
->d_uf_terms
[f
][i
];
976 vector
<TNode
> children
;
977 children
.push_back(f
);
978 Trace("model-builder-debug") << " process term : " << un
<< std::endl
;
979 for (size_t j
= 0; j
< un
.getNumChildren(); ++j
)
981 Node rc
= m
->getRepresentative(un
[j
]);
982 Trace("model-builder-debug2") << " get rep : " << un
[j
] << " returned "
984 Assert(rc
.isConst());
985 children
.push_back(rc
);
987 Node simp
= NodeManager::currentNM()->mkNode(un
.getKind(), children
);
988 Node v
= m
->getRepresentative(un
);
989 Trace("model-builder") << " Setting (" << simp
<< ") to (" << v
<< ")"
991 ufmt
.setValue(m
, simp
, v
);
994 if (default_v
.isNull())
996 // choose default value from model if none exists
997 TypeEnumerator
te(f
.getType().getRangeType());
1000 ufmt
.setDefaultValue(m
, default_v
);
1001 bool condenseFuncValues
= options::condenseFunctionValues();
1002 if (condenseFuncValues
)
1006 std::stringstream ss
;
1008 Node val
= ufmt
.getFunctionValue(ss
.str().c_str(), condenseFuncValues
);
1009 m
->assignFunctionDefinition(f
, val
);
1010 // ufmt.debugPrint( std::cout, m );
1013 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel
* m
, Node f
)
1015 Assert(options::ufHo());
1016 TypeNode type
= f
.getType();
1017 std::vector
<TypeNode
> argTypes
= type
.getArgTypes();
1018 std::vector
<Node
> args
;
1019 std::vector
<TNode
> apply_args
;
1020 for (unsigned i
= 0; i
< argTypes
.size(); i
++)
1022 Node v
= NodeManager::currentNM()->mkBoundVar(argTypes
[i
]);
1026 apply_args
.push_back(v
);
1029 // start with the base return value (currently we use the same default value
1030 // for all functions)
1031 TypeEnumerator
te(type
.getRangeType());
1033 std::map
<Node
, std::vector
<Node
> >::iterator itht
= m
->d_ho_uf_terms
.find(f
);
1034 if (itht
!= m
->d_ho_uf_terms
.end())
1036 for (size_t i
= 0; i
< itht
->second
.size(); i
++)
1038 Node hn
= itht
->second
[i
];
1039 Trace("model-builder-debug") << " process : " << hn
<< std::endl
;
1040 Assert(hn
.getKind() == kind::HO_APPLY
);
1041 Assert(m
->areEqual(hn
[0], f
));
1042 Node hni
= m
->getRepresentative(hn
[1]);
1043 Trace("model-builder-debug2") << " get rep : " << hn
[0]
1044 << " returned " << hni
<< std::endl
;
1045 Assert(hni
.isConst());
1046 Assert(hni
.getType().isSubtypeOf(args
[0].getType()));
1047 hni
= Rewriter::rewrite(args
[0].eqNode(hni
));
1048 Node hnv
= m
->getRepresentative(hn
);
1049 Trace("model-builder-debug2") << " get rep val : " << hn
1050 << " returned " << hnv
<< std::endl
;
1051 Assert(hnv
.isConst());
1052 if (!apply_args
.empty())
1054 Assert(hnv
.getKind() == kind::LAMBDA
1055 && hnv
[0].getNumChildren() + 1 == args
.size());
1056 std::vector
<TNode
> largs
;
1057 for (unsigned j
= 0; j
< hnv
[0].getNumChildren(); j
++)
1059 largs
.push_back(hnv
[0][j
]);
1061 Assert(largs
.size() == apply_args
.size());
1062 hnv
= hnv
[1].substitute(
1063 largs
.begin(), largs
.end(), apply_args
.begin(), apply_args
.end());
1064 hnv
= Rewriter::rewrite(hnv
);
1066 Assert(!TypeNode::leastCommonTypeNode(hnv
.getType(), curr
.getType())
1068 curr
= NodeManager::currentNM()->mkNode(kind::ITE
, hni
, hnv
, curr
);
1071 Node val
= NodeManager::currentNM()->mkNode(
1073 NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
),
1075 m
->assignFunctionDefinition(f
, val
);
1078 // This struct is used to sort terms by the "size" of their type
1079 // The size of the type is the number of nodes in the type, for example
1081 // size of Function( Int, Int ) is 3
1082 // size of Function( Function( Bool, Int ), Int ) is 5
1085 // stores the size of the type
1086 std::map
<TypeNode
, unsigned> d_type_size
;
1087 // get the size of type tn
1088 unsigned getTypeSize(TypeNode tn
)
1090 std::map
<TypeNode
, unsigned>::iterator it
= d_type_size
.find(tn
);
1091 if (it
!= d_type_size
.end())
1098 for (unsigned i
= 0; i
< tn
.getNumChildren(); i
++)
1100 sum
+= getTypeSize(tn
[i
]);
1102 d_type_size
[tn
] = sum
;
1108 // compares the type size of i and j
1109 // returns true iff the size of i is less than that of j
1110 // tiebreaks are determined by node value
1111 bool operator()(Node i
, Node j
)
1113 int si
= getTypeSize(i
.getType());
1114 int sj
= getTypeSize(j
.getType());
1130 void TheoryEngineModelBuilder::assignFunctions(TheoryModel
* m
)
1132 if (!options::assignFunctionValues())
1136 Trace("model-builder") << "Assigning function values..." << std::endl
;
1137 std::vector
<Node
> funcs_to_assign
= m
->getFunctionsToAssign();
1139 if (options::ufHo())
1141 // sort based on type size if higher-order
1142 Trace("model-builder") << "Sort functions by type..." << std::endl
;
1144 std::sort(funcs_to_assign
.begin(), funcs_to_assign
.end(), sts
);
1147 if (Trace
.isOn("model-builder"))
1149 Trace("model-builder") << "...have " << funcs_to_assign
.size()
1150 << " functions to assign:" << std::endl
;
1151 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1153 Node f
= funcs_to_assign
[k
];
1154 Trace("model-builder") << " [" << k
<< "] : " << f
<< " : "
1155 << f
.getType() << std::endl
;
1159 // construct function values
1160 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1162 Node f
= funcs_to_assign
[k
];
1163 Trace("model-builder") << " Function #" << k
<< " is " << f
<< std::endl
;
1164 // std::map< Node, std::vector< Node > >::iterator itht =
1165 // m->d_ho_uf_terms.find( f );
1166 if (!options::ufHo())
1168 Trace("model-builder") << " Assign function value for " << f
1169 << " based on APPLY_UF" << std::endl
;
1170 assignFunction(m
, f
);
1174 Trace("model-builder") << " Assign function value for " << f
1175 << " based on curried HO_APPLY" << std::endl
;
1176 assignHoFunction(m
, f
);
1179 Trace("model-builder") << "Finished assigning function values." << std::endl
;
1182 } /* namespace CVC4::theory */
1183 } /* namespace CVC4 */