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-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Implementation of theory model buidler class
14 #include "theory/theory_model_builder.h"
16 #include "expr/dtype.h"
17 #include "options/quantifiers_options.h"
18 #include "options/smt_options.h"
19 #include "options/uf_options.h"
20 #include "theory/theory_engine.h"
21 #include "theory/uf/theory_uf_model.h"
24 using namespace CVC4::kind
;
25 using namespace CVC4::context
;
30 void TheoryEngineModelBuilder::Assigner::initialize(
31 TypeNode tn
, TypeEnumeratorProperties
* tep
, const std::vector
<Node
>& aes
)
33 d_te
.reset(new TypeEnumerator(tn
, tep
));
34 d_assignExcSet
.insert(d_assignExcSet
.end(), aes
.begin(), aes
.end());
37 Node
TheoryEngineModelBuilder::Assigner::getNextAssignment()
39 Assert(d_te
!= nullptr);
42 TypeEnumerator
& te
= *d_te
;
43 // Check if we have run out of elements. This should never happen; if it
44 // does we assert false and return null.
50 // must increment until we find one that is not in the assignment
55 success
= std::find(d_assignExcSet
.begin(), d_assignExcSet
.end(), n
)
56 == d_assignExcSet
.end();
57 // increment regardless of fail or succeed, to set up the next value
63 TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine
* te
) : d_te(te
)
67 Node
TheoryEngineModelBuilder::evaluateEqc(TheoryModel
* m
, TNode r
)
69 eq::EqClassIterator eqc_i
= eq::EqClassIterator(r
, m
->d_equalityEngine
);
70 for (; !eqc_i
.isFinished(); ++eqc_i
)
73 Trace("model-builder-debug") << "Look at term : " << n
<< std::endl
;
76 Trace("model-builder-debug") << "...try to normalize" << std::endl
;
77 Node normalized
= normalize(m
, n
, true);
78 if (normalized
.isConst())
87 bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel
* tm
, Assigner
& a
)
93 std::vector
<Node
>& eset
= a
.d_assignExcSet
;
94 std::map
<Node
, Node
>::iterator it
;
95 for (unsigned i
= 0, size
= eset
.size(); i
< size
; i
++)
97 // Members of exclusion set must have values, otherwise we are not yet
105 // Assignable members of assignment exclusion set should be representatives
106 // of their equivalence classes. This ensures we look up the constant
107 // representatives for assignable members of assignment exclusion sets.
108 Assert(er
== tm
->getRepresentative(er
));
109 it
= d_constantReps
.find(er
);
110 if (it
== d_constantReps
.end())
112 Trace("model-build-aes")
113 << "isAssignerActive: not active due to " << er
<< std::endl
;
117 eset
[i
] = it
->second
;
119 Trace("model-build-aes") << "isAssignerActive: active!" << std::endl
;
124 bool TheoryEngineModelBuilder::isAssignable(TNode n
)
126 if (n
.getKind() == kind::SELECT
|| n
.getKind() == kind::APPLY_SELECTOR_TOTAL
)
128 // selectors are always assignable (where we guarantee that they are not
130 if (!options::ufHo())
132 Assert(!n
.getType().isFunction());
137 // might be a function field
138 return !n
.getType().isFunction();
141 else if (n
.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGN
)
143 // Extracting the sign of a floating-point number acts similar to a
144 // selector on a datatype, i.e. if `(sign x)` wasn't assigned a value, we
145 // can pick an arbitrary one. Note that the other components of a
146 // floating-point number should always be assigned a value.
151 // non-function variables, and fully applied functions
152 if (!options::ufHo())
154 // no functions exist, all functions are fully applied
155 Assert(n
.getKind() != kind::HO_APPLY
);
156 Assert(!n
.getType().isFunction());
157 return n
.isVar() || n
.getKind() == kind::APPLY_UF
;
161 // Assert( n.getKind() != kind::APPLY_UF );
162 return (n
.isVar() && !n
.getType().isFunction())
163 || n
.getKind() == kind::APPLY_UF
164 || (n
.getKind() == kind::HO_APPLY
165 && n
[0].getType().getNumChildren() == 2);
170 void TheoryEngineModelBuilder::addAssignableSubterms(TNode n
,
178 if (cache
.find(n
) != cache
.end())
184 tm
->d_equalityEngine
->addTerm(n
);
186 for (TNode::iterator child_it
= n
.begin(); child_it
!= n
.end(); ++child_it
)
188 addAssignableSubterms(*child_it
, tm
, cache
);
193 void TheoryEngineModelBuilder::assignConstantRep(TheoryModel
* tm
,
197 d_constantReps
[eqc
] = const_rep
;
198 Trace("model-builder") << " Assign: Setting constant rep of " << eqc
199 << " to " << const_rep
<< endl
;
200 tm
->d_rep_set
.setTermForRepresentative(const_rep
, eqc
);
203 bool TheoryEngineModelBuilder::isExcludedCdtValue(
205 std::set
<Node
>* repSet
,
206 std::map
<Node
, Node
>& assertedReps
,
209 Trace("model-builder-debug")
210 << "Is " << val
<< " and excluded codatatype value for " << eqc
<< "? "
212 for (set
<Node
>::iterator i
= repSet
->begin(); i
!= repSet
->end(); ++i
)
214 Assert(assertedReps
.find(*i
) != assertedReps
.end());
215 Node rep
= assertedReps
[*i
];
216 Trace("model-builder-debug") << " Rep : " << rep
<< std::endl
;
217 // check matching val to rep with eqc as a free variable
219 if (isCdtValueMatch(val
, rep
, eqc
, eqc_m
))
221 Trace("model-builder-debug") << " ...matches with " << eqc
<< " -> "
222 << eqc_m
<< std::endl
;
223 if (eqc_m
.getKind() == kind::UNINTERPRETED_CONSTANT
)
225 Trace("model-builder-debug") << "*** " << val
226 << " is excluded datatype for " << eqc
235 bool TheoryEngineModelBuilder::isCdtValueMatch(Node v
,
248 // only if an uninterpreted constant?
257 else if (v
.getKind() == kind::APPLY_CONSTRUCTOR
258 && r
.getKind() == kind::APPLY_CONSTRUCTOR
)
260 if (v
.getOperator() == r
.getOperator())
262 for (unsigned i
= 0; i
< v
.getNumChildren(); i
++)
264 if (!isCdtValueMatch(v
[i
], r
[i
], eqc
, eqc_m
))
275 bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn
)
281 else if (tn
.isArray())
283 return involvesUSort(tn
.getArrayIndexType())
284 || involvesUSort(tn
.getArrayConstituentType());
288 return involvesUSort(tn
.getSetElementType());
290 else if (tn
.isDatatype())
292 const DType
& dt
= tn
.getDType();
293 return dt
.involvesUninterpretedType();
301 bool TheoryEngineModelBuilder::isExcludedUSortValue(
302 std::map
<TypeNode
, unsigned>& eqc_usort_count
,
304 std::map
<Node
, bool>& visited
)
307 if (visited
.find(v
) == visited
.end())
310 TypeNode tn
= v
.getType();
313 Trace("model-builder-debug") << "Is excluded usort value : " << v
<< " "
315 unsigned card
= eqc_usort_count
[tn
];
316 Trace("model-builder-debug") << " Cardinality is " << card
<< std::endl
;
318 v
.getConst
<UninterpretedConstant
>().getIndex().toUnsignedInt();
319 Trace("model-builder-debug") << " Index is " << index
<< std::endl
;
320 return index
> 0 && index
>= card
;
322 for (unsigned i
= 0; i
< v
.getNumChildren(); i
++)
324 if (isExcludedUSortValue(eqc_usort_count
, v
[i
], visited
))
333 void TheoryEngineModelBuilder::addToTypeList(
335 std::vector
<TypeNode
>& type_list
,
336 std::unordered_set
<TypeNode
, TypeNodeHashFunction
>& visiting
)
338 if (std::find(type_list
.begin(), type_list
.end(), tn
) == type_list
.end())
340 if (visiting
.find(tn
) == visiting
.end())
343 /* This must make a recursive call on all types that are subterms of
344 * values of the current type.
345 * Note that recursive traversal here is over enumerated expressions
346 * (very low expression depth). */
349 addToTypeList(tn
.getArrayIndexType(), type_list
, visiting
);
350 addToTypeList(tn
.getArrayConstituentType(), type_list
, visiting
);
354 addToTypeList(tn
.getSetElementType(), type_list
, visiting
);
356 else if (tn
.isDatatype())
358 const DType
& dt
= tn
.getDType();
359 for (unsigned i
= 0; i
< dt
.getNumConstructors(); i
++)
361 for (unsigned j
= 0; j
< dt
[i
].getNumArgs(); j
++)
363 TypeNode ctn
= dt
[i
][j
].getRangeType();
364 addToTypeList(ctn
, type_list
, visiting
);
368 Assert(std::find(type_list
.begin(), type_list
.end(), tn
)
370 type_list
.push_back(tn
);
375 bool TheoryEngineModelBuilder::buildModel(TheoryModel
* tm
)
377 Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl
;
378 eq::EqualityEngine
* ee
= tm
->d_equalityEngine
;
380 Trace("model-builder")
381 << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl
;
382 // model-builder specific initialization
383 if (!preProcessBuildModel(tm
))
385 Trace("model-builder")
386 << "TheoryEngineModelBuilder: fail preprocess build model."
391 Trace("model-builder")
392 << "TheoryEngineModelBuilder: Add assignable subterms..." << std::endl
;
393 // Loop through all terms and make sure that assignable sub-terms are in the
395 // Also, record #eqc per type (for finite model finding)
396 std::map
<TypeNode
, unsigned> eqc_usort_count
;
397 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(ee
);
400 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
402 eq::EqClassIterator eqc_i
= eq::EqClassIterator((*eqcs_i
), ee
);
403 for (; !eqc_i
.isFinished(); ++eqc_i
)
405 addAssignableSubterms(*eqc_i
, tm
, cache
);
407 TypeNode tn
= (*eqcs_i
).getType();
410 if (eqc_usort_count
.find(tn
) == eqc_usort_count
.end())
412 eqc_usort_count
[tn
] = 1;
416 eqc_usort_count
[tn
]++;
422 Trace("model-builder") << "Collect representatives..." << std::endl
;
424 // Process all terms in the equality engine, store representatives for each EC
425 d_constantReps
.clear();
426 std::map
<Node
, Node
> assertedReps
;
427 TypeSet typeConstSet
, typeRepSet
, typeNoRepSet
;
428 // Compute type enumerator properties. This code ensures we do not
429 // enumerate terms that have uninterpreted constants that violate the
430 // bounds imposed by finite model finding. For example, if finite
431 // model finding insists that there are only 2 values { U1, U2 } of type U,
432 // then the type enumerator for list of U should enumerate:
433 // nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ...
434 // instead of enumerating (cons U3 nil).
435 TypeEnumeratorProperties tep
;
436 if (options::finiteModelFind())
438 tep
.d_fixed_usort_card
= true;
439 for (std::map
<TypeNode
, unsigned>::iterator it
= eqc_usort_count
.begin();
440 it
!= eqc_usort_count
.end();
443 Trace("model-builder") << "Fixed bound (#eqc) for " << it
->first
<< " : "
444 << it
->second
<< std::endl
;
445 tep
.d_fixed_card
[it
->first
] = Integer(it
->second
);
447 typeConstSet
.setTypeEnumeratorProperties(&tep
);
450 // AJR: build ordered list of types that ensures that base types are
452 // (I think) this is only strictly necessary for finite model finding +
453 // parametric types instantiated with uninterpreted sorts, but is probably
454 // a good idea to do in general since it leads to models with smaller term
456 std::vector
<TypeNode
> type_list
;
457 eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
458 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
460 // eqc is the equivalence class representative
461 Node eqc
= (*eqcs_i
);
462 Trace("model-builder") << "Processing EC: " << eqc
<< endl
;
463 Assert(tm
->d_equalityEngine
->getRepresentative(eqc
) == eqc
);
464 TypeNode eqct
= eqc
.getType();
465 Assert(assertedReps
.find(eqc
) == assertedReps
.end());
466 Assert(d_constantReps
.find(eqc
) == d_constantReps
.end());
468 // Loop through terms in this EC
470 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
471 for (; !eqc_i
.isFinished(); ++eqc_i
)
474 Trace("model-builder") << " Processing Term: " << n
<< endl
;
475 // Record as rep if this node was specified as a representative
476 if (tm
->d_reps
.find(n
) != tm
->d_reps
.end())
478 // AJR: I believe this assertion is too strict,
479 // e.g. datatypes may assert representative for two constructor terms
480 // that are not in the care graph and are merged during
482 // Assert(rep.isNull());
484 Assert(!rep
.isNull());
485 Trace("model-builder") << " Rep( " << eqc
<< " ) = " << rep
488 // Record as const_rep if this node is constant
491 Assert(const_rep
.isNull());
493 Trace("model-builder") << " ConstRep( " << eqc
<< " ) = " << const_rep
496 // model-specific processing of the term
497 tm
->addTermInternal(n
);
500 // Assign representative for this EC
501 if (!const_rep
.isNull())
503 // Theories should not specify a rep if there is already a constant in the
505 // AJR: I believe this assertion is too strict, eqc with asserted reps may
506 // merge with constant eqc
507 // Assert(rep.isNull() || rep == const_rep);
508 assignConstantRep(tm
, eqc
, const_rep
);
509 typeConstSet
.add(eqct
.getBaseType(), const_rep
);
511 else if (!rep
.isNull())
513 assertedReps
[eqc
] = rep
;
514 typeRepSet
.add(eqct
.getBaseType(), eqc
);
515 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
516 addToTypeList(eqct
.getBaseType(), type_list
, visiting
);
520 typeNoRepSet
.add(eqct
, eqc
);
521 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
522 addToTypeList(eqct
, type_list
, visiting
);
526 Trace("model-builder") << "Compute assignable information..." << std::endl
;
527 // The set of equivalence classes that are "assignable"
528 std::unordered_set
<Node
, NodeHashFunction
> assignableEqc
;
529 // The set of equivalence classes that are "evaluable"
530 std::unordered_set
<Node
, NodeHashFunction
> evaluableEqc
;
531 // Assigner objects for relevant equivalence classes
532 std::map
<Node
, Assigner
> eqcToAssigner
;
533 // Maps equivalence classes to the equivalence class that maps to its assigner
534 // object in the above map.
535 std::map
<Node
, Node
> eqcToAssignerMaster
;
536 // Compute the above information
537 computeAssignableInfo(
538 tm
, tep
, assignableEqc
, evaluableEqc
, eqcToAssigner
, eqcToAssignerMaster
);
540 // Need to ensure that each EC has a constant representative.
542 Trace("model-builder") << "Processing EC's..." << std::endl
;
544 TypeSet::iterator it
;
545 vector
<TypeNode
>::iterator type_it
;
546 set
<Node
>::iterator i
, i2
;
547 bool changed
, unassignedAssignable
, assignOne
= false;
548 set
<TypeNode
> evaluableSet
;
550 // Double-fixed-point loop
551 // Outer loop handles a special corner case (see code at end of loop for
555 // Inner fixed-point loop: we are trying to learn constant values for every
556 // EC. Each time through this loop, we process all of the
557 // types by type and may learn some new EC values. EC's in one type may
558 // depend on EC's in another type, so we need a fixed-point loop
559 // to ensure that we learn as many EC values as possible
563 unassignedAssignable
= false;
564 evaluableSet
.clear();
566 // Iterate over all types we've seen
567 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
569 TypeNode t
= *type_it
;
570 TypeNode tb
= t
.getBaseType();
571 set
<Node
>* noRepSet
= typeNoRepSet
.getSet(t
);
573 // 1. Try to evaluate the EC's in this type
574 if (noRepSet
!= NULL
&& !noRepSet
->empty())
576 Trace("model-builder") << " Eval phase, working on type: " << t
579 d_normalizedCache
.clear();
580 for (i
= noRepSet
->begin(); i
!= noRepSet
->end();)
584 Trace("model-builder-debug") << "Look at eqc : " << (*i2
)
587 // only possible to normalize if we are evaluable
588 evaluable
= evaluableEqc
.find(*i2
) != evaluableEqc
.end();
591 normalized
= evaluateEqc(tm
, *i2
);
593 if (!normalized
.isNull())
595 Assert(normalized
.isConst());
596 typeConstSet
.add(tb
, normalized
);
597 assignConstantRep(tm
, *i2
, normalized
);
598 Trace("model-builder") << " Eval: Setting constant rep of "
599 << (*i2
) << " to " << normalized
<< endl
;
607 evaluableSet
.insert(tb
);
609 // If assignable, remember there is an equivalence class that is
610 // not assigned and assignable.
611 if (assignableEqc
.find(*i2
) != assignableEqc
.end())
613 unassignedAssignable
= true;
619 // 2. Normalize any non-const representative terms for this type
620 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
621 if (repSet
!= NULL
&& !repSet
->empty())
623 Trace("model-builder")
624 << " Normalization phase, working on type: " << t
<< endl
;
625 d_normalizedCache
.clear();
626 for (i
= repSet
->begin(); i
!= repSet
->end();)
628 Assert(assertedReps
.find(*i
) != assertedReps
.end());
629 Node rep
= assertedReps
[*i
];
630 Node normalized
= normalize(tm
, rep
, false);
631 Trace("model-builder") << " Normalizing rep (" << rep
632 << "), normalized to (" << normalized
<< ")"
634 if (normalized
.isConst())
637 typeConstSet
.add(tb
, normalized
);
638 assignConstantRep(tm
, *i
, normalized
);
639 assertedReps
.erase(*i
);
646 if (normalized
!= rep
)
648 assertedReps
[*i
] = normalized
;
658 if (!unassignedAssignable
)
663 // 3. Assign unassigned assignable EC's using type enumeration - assign a
664 // value *different* from all other EC's if the type is infinite
665 // Assign first value from type enumerator otherwise - for finite types, we
666 // rely on polite framework to ensure that EC's that have to be
667 // different are different.
669 // Only make assignments on a type if:
670 // 1. there are no terms that share the same base type with un-normalized
672 // 2. there are no terms that share teh same base type that are unevaluated
674 // Alternatively, if 2 or 3 don't hold but we are in a special
675 // deadlock-breaking mode where assignOne is true, go ahead and make one
678 // must iterate over the ordered type list to ensure that we do not
679 // enumerate values with subterms
680 // having types that we are currently enumerating (when possible)
681 // for example, this ensures we enumerate uninterpreted sort U before (List
682 // of U) and (Array U U)
683 // however, it does not break cyclic type dependencies for mutually
684 // recursive datatypes, but this is handled
685 // by recording all subterms of enumerated values in TypeSet::addSubTerms.
686 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
688 TypeNode t
= *type_it
;
689 // continue if there are no more equivalence classes of this type to
691 std::set
<Node
>* noRepSetPtr
= typeNoRepSet
.getSet(t
);
692 if (noRepSetPtr
== NULL
)
696 set
<Node
>& noRepSet
= *noRepSetPtr
;
697 if (noRepSet
.empty())
702 // get properties of this type
703 bool isCorecursive
= false;
706 const DType
& dt
= t
.getDType();
707 isCorecursive
= dt
.isCodatatype()
708 && (!dt
.isFinite(t
) || dt
.isRecursiveSingleton(t
));
710 #ifdef CVC4_ASSERTIONS
711 bool isUSortFiniteRestricted
= false;
712 if (options::finiteModelFind())
714 isUSortFiniteRestricted
= !t
.isSort() && involvesUSort(t
);
718 TypeNode tb
= t
.getBaseType();
721 set
<Node
>* repSet
= typeRepSet
.getSet(tb
);
722 if (repSet
!= NULL
&& !repSet
->empty())
726 if (evaluableSet
.find(tb
) != evaluableSet
.end())
731 Trace("model-builder") << " Assign phase, working on type: " << t
733 bool assignable
, evaluable CVC4_UNUSED
;
734 std::map
<Node
, Assigner
>::iterator itAssigner
;
735 std::map
<Node
, Node
>::iterator itAssignerM
;
736 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
737 for (i
= noRepSet
.begin(); i
!= noRepSet
.end();)
741 // check whether it has an assigner object
742 itAssignerM
= eqcToAssignerMaster
.find(*i2
);
743 if (itAssignerM
!= eqcToAssignerMaster
.end())
745 // Take the master's assigner. Notice we don't care which order
746 // equivalence classes are assigned. For instance, the master can
747 // be assigned after one of its slaves.
748 itAssigner
= eqcToAssigner
.find(itAssignerM
->second
);
752 itAssigner
= eqcToAssigner
.find(*i2
);
754 if (itAssigner
!= eqcToAssigner
.end())
756 assignable
= isAssignerActive(tm
, itAssigner
->second
);
760 assignable
= assignableEqc
.find(*i2
) != assignableEqc
.end();
762 evaluable
= evaluableEqc
.find(*i2
) != evaluableEqc
.end();
763 Trace("model-builder-debug")
764 << " eqc " << *i2
<< " is assignable=" << assignable
765 << ", evaluable=" << evaluable
<< std::endl
;
768 Assert(!evaluable
|| assignOne
);
769 // this assertion ensures that if we are assigning to a term of
770 // Boolean type, then the term must be assignable.
771 // Note we only assign to terms of Boolean type if the term occurs in
772 // a singleton equivalence class; otherwise the term would have been
773 // in the equivalence class of true or false and would not need
775 Assert(!t
.isBoolean() || isAssignable(*i2
));
777 if (itAssigner
!= eqcToAssigner
.end())
779 Trace("model-builder-debug")
780 << "Get value from assigner for finite type..." << std::endl
;
781 // if it has an assigner, get the value from the assigner.
782 n
= itAssigner
->second
.getNextAssignment();
785 else if (!t
.isFinite())
787 // if its infinite, we get a fresh value that does not occur in
792 Trace("model-builder-debug") << "Enumerate term of type " << t
794 n
= typeConstSet
.nextTypeEnum(t
, true);
795 //--- AJR: this code checks whether n is a legal value
798 Trace("model-builder-debug") << "Check if excluded : " << n
800 #ifdef CVC4_ASSERTIONS
801 if (isUSortFiniteRestricted
)
803 // must not involve uninterpreted constants beyond cardinality
804 // bound (which assumed to coincide with #eqc)
805 // this is just an assertion now, since TypeEnumeratorProperties
806 // should ensure that only legal values are enumerated wrt this
808 std::map
<Node
, bool> visited
;
809 success
= !isExcludedUSortValue(eqc_usort_count
, n
, visited
);
812 Trace("model-builder")
813 << "Excluded value for " << t
<< " : " << n
814 << " due to out of range uninterpreted constant."
820 if (success
&& isCorecursive
)
822 if (repSet
!= NULL
&& !repSet
->empty())
824 // in the case of codatatypes, check if it is in the set of
825 // values that we cannot assign
826 success
= !isExcludedCdtValue(n
, repSet
, assertedReps
, *i2
);
829 Trace("model-builder")
830 << "Excluded value : " << n
831 << " due to alpha-equivalent codatatype expression."
842 Trace("model-builder-debug")
843 << "Get first value from finite type..." << std::endl
;
844 // Otherwise, we get the first value from the type enumerator.
845 TypeEnumerator
te(t
);
848 Trace("model-builder-debug") << "...got " << n
<< std::endl
;
849 assignConstantRep(tm
, *i2
, n
);
861 // Corner case - I'm not sure this can even happen - but it's theoretically
862 // possible to have a cyclical dependency
863 // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
864 // this case, neither one will get assigned because we are waiting
865 // to be able to evaluate. But we will never be able to evaluate because
866 // the variables that need to be assigned are in
867 // these same EC's. In this case, repeat the whole fixed-point computation
868 // with the difference that the first EC
869 // that has both assignable and evaluable expressions will get assigned.
872 Assert(!assignOne
); // check for infinite loop!
877 #ifdef CVC4_ASSERTIONS
878 // Assert that all representatives have been converted to constants
879 for (it
= typeRepSet
.begin(); it
!= typeRepSet
.end(); ++it
)
881 set
<Node
>& repSet
= TypeSet::getSet(it
);
884 Trace("model-builder") << "***Non-empty repSet, size = " << repSet
.size()
885 << ", first = " << *(repSet
.begin()) << endl
;
889 #endif /* CVC4_ASSERTIONS */
891 Trace("model-builder") << "Copy representatives to model..." << std::endl
;
893 std::map
<Node
, Node
>::iterator itMap
;
894 for (itMap
= d_constantReps
.begin(); itMap
!= d_constantReps
.end(); ++itMap
)
896 tm
->d_reps
[itMap
->first
] = itMap
->second
;
897 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
900 Trace("model-builder") << "Make sure ECs have reps..." << std::endl
;
901 // Make sure every EC has a rep
902 for (itMap
= assertedReps
.begin(); itMap
!= assertedReps
.end(); ++itMap
)
904 tm
->d_reps
[itMap
->first
] = itMap
->second
;
905 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
907 for (it
= typeNoRepSet
.begin(); it
!= typeNoRepSet
.end(); ++it
)
909 set
<Node
>& noRepSet
= TypeSet::getSet(it
);
910 for (const Node
& node
: noRepSet
)
912 tm
->d_reps
[node
] = node
;
913 tm
->d_rep_set
.add(node
.getType(), node
);
917 // modelBuilder-specific initialization
918 if (!processBuildModel(tm
))
920 Trace("model-builder")
921 << "TheoryEngineModelBuilder: fail process build model." << std::endl
;
924 Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl
;
927 void TheoryEngineModelBuilder::computeAssignableInfo(
929 TypeEnumeratorProperties
& tep
,
930 std::unordered_set
<Node
, NodeHashFunction
>& assignableEqc
,
931 std::unordered_set
<Node
, NodeHashFunction
>& evaluableEqc
,
932 std::map
<Node
, Assigner
>& eqcToAssigner
,
933 std::map
<Node
, Node
>& eqcToAssignerMaster
)
935 eq::EqualityEngine
* ee
= tm
->d_equalityEngine
;
936 bool computeAssigners
= tm
->hasAssignmentExclusionSets();
937 std::unordered_set
<Node
, NodeHashFunction
> processed
;
938 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(ee
);
939 // A flag set to true if the current equivalence class is assignable (see
941 bool assignable
= false;
942 // Set to true if the current equivalence class is evaluatable (see
944 bool evaluable
= false;
945 // Set to true if a term in the current equivalence class has been given an
946 // assignment exclusion set.
947 bool hasESet CVC4_UNUSED
= false;
948 // Set to true if we found that a term in the current equivalence class has
949 // been given an assignment exclusion set, and we have not seen this term
950 // as part of a previous assignment exclusion group. In other words, when
951 // this flag is true we construct a new assigner object with the current
952 // equivalence class as its master.
953 bool foundESet
= false;
954 // Look at all equivalence classes in the model
955 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
958 if (d_constantReps
.find(eqc
) != d_constantReps
.end())
960 // already assigned above, skip
963 // reset information for the current equivalence classe
968 // the assignment exclusion set for the current equivalence class
969 std::vector
<Node
> eset
;
970 // the group to which this equivalence class belongs when exclusion sets
971 // were assigned (see the argument group of
972 // TheoryModel::getAssignmentExclusionSet).
973 std::vector
<Node
> group
;
974 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, ee
);
975 // For each term in the current equivalence class, we update the above
976 // information. We may terminate this loop before looking at all terms if we
977 // have inferred the value of all of the information above.
978 for (; !eqc_i
.isFinished(); ++eqc_i
)
981 if (!isAssignable(n
))
984 if (!computeAssigners
)
988 // both flags set, we are done
992 // expressions that are not assignable should not be given assignment
994 Assert(!tm
->getAssignmentExclusionSet(n
, group
, eset
));
1000 if (!computeAssigners
)
1004 // both flags set, we are done
1007 // we don't compute assigners, skip
1011 // process the assignment exclusion set for term n
1012 // was it processed as a slave of a group?
1013 if (processed
.find(n
) != processed
.end())
1015 // Should not have two assignment exclusion sets for the same
1016 // equivalence class
1018 Assert(eqcToAssignerMaster
.find(eqc
) != eqcToAssignerMaster
.end());
1019 // already processed as a slave term
1023 // was it assigned one?
1024 if (tm
->getAssignmentExclusionSet(n
, group
, eset
))
1026 // Should not have two assignment exclusion sets for the same
1027 // equivalence class
1035 assignableEqc
.insert(eqc
);
1039 evaluableEqc
.insert(eqc
);
1041 // If we found an assignment exclusion set, we construct a new assigner
1045 // we don't accept assignment exclusion sets for evaluable eqc
1047 // construct the assigner
1048 Assigner
& a
= eqcToAssigner
[eqc
];
1049 // Take the representatives of each term in the assignment exclusion
1050 // set, which ensures we can look up their value in d_constReps later.
1051 std::vector
<Node
> aes
;
1052 for (const Node
& e
: eset
)
1054 // Should only supply terms that occur in the model or constants
1055 // in assignment exclusion sets.
1056 Assert(tm
->hasTerm(e
) || e
.isConst());
1057 Node er
= tm
->hasTerm(e
) ? tm
->getRepresentative(e
) : e
;
1061 a
.initialize(eqc
.getType(), &tep
, aes
);
1062 // all others in the group are slaves of this
1063 for (const Node
& g
: group
)
1065 Assert(isAssignable(g
));
1066 if (!tm
->hasTerm(g
))
1068 // Ignore those that aren't in the model, in the case the user
1069 // has supplied an assignment exclusion set to a variable not in
1073 Node gr
= tm
->getRepresentative(g
);
1076 eqcToAssignerMaster
[gr
] = eqc
;
1077 // remember that this term has been processed
1078 processed
.insert(g
);
1085 void TheoryEngineModelBuilder::postProcessModel(bool incomplete
, TheoryModel
* m
)
1087 // if we are incomplete, there is no guarantee on the model.
1088 // thus, we do not check the model here.
1093 Assert(m
!= nullptr);
1094 // debug-check the model if the checkModels() is enabled.
1095 if (options::debugCheckModels())
1101 void TheoryEngineModelBuilder::debugCheckModel(TheoryModel
* tm
)
1103 #ifdef CVC4_ASSERTIONS
1104 if (tm
->hasApproximations())
1106 // models with approximations may fail the assertions below
1109 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
1110 std::map
<Node
, Node
>::iterator itMap
;
1111 // Check that every term evaluates to its representative in the model
1112 for (eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
1113 !eqcs_i
.isFinished();
1116 // eqc is the equivalence class representative
1117 Node eqc
= (*eqcs_i
);
1118 // get the representative
1119 Node rep
= tm
->getRepresentative(eqc
);
1120 if (!rep
.isConst() && eqc
.getType().isBoolean())
1122 // if Boolean, it does not necessarily have a constant representative, use
1123 // get value instead
1124 rep
= tm
->getValue(eqc
);
1125 Assert(rep
.isConst());
1127 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
1128 for (; !eqc_i
.isFinished(); ++eqc_i
)
1131 static int repCheckInstance
= 0;
1134 // non-linear mult is not necessarily accurate wrt getValue
1135 if (n
.getKind() != kind::NONLINEAR_MULT
)
1137 Debug("check-model::rep-checking") << "( " << repCheckInstance
<< ") "
1138 << "n: " << n
<< endl
1139 << "getValue(n): " << tm
->getValue(n
)
1141 << "rep: " << rep
<< endl
;
1142 Assert(tm
->getValue(*eqc_i
) == rep
)
1143 << "run with -d check-model::rep-checking for details";
1147 #endif /* CVC4_ASSERTIONS */
1149 // builder-specific debugging
1153 Node
TheoryEngineModelBuilder::normalize(TheoryModel
* m
, TNode r
, bool evalOnly
)
1155 std::map
<Node
, Node
>::iterator itMap
= d_constantReps
.find(r
);
1156 if (itMap
!= d_constantReps
.end())
1158 return (*itMap
).second
;
1160 NodeMap::iterator it
= d_normalizedCache
.find(r
);
1161 if (it
!= d_normalizedCache
.end())
1163 return (*it
).second
;
1165 Trace("model-builder-debug") << "do normalize on " << r
<< std::endl
;
1167 if (r
.getNumChildren() > 0)
1169 std::vector
<Node
> children
;
1170 if (r
.getMetaKind() == kind::metakind::PARAMETERIZED
)
1172 children
.push_back(r
.getOperator());
1174 bool childrenConst
= true;
1175 for (size_t i
= 0; i
< r
.getNumChildren(); ++i
)
1178 bool recurse
= true;
1181 if (m
->d_equalityEngine
->hasTerm(ri
))
1184 d_constantReps
.find(m
->d_equalityEngine
->getRepresentative(ri
));
1185 if (itMap
!= d_constantReps
.end())
1187 ri
= (*itMap
).second
;
1197 ri
= normalize(m
, ri
, evalOnly
);
1201 childrenConst
= false;
1204 children
.push_back(ri
);
1206 retNode
= NodeManager::currentNM()->mkNode(r
.getKind(), children
);
1209 retNode
= Rewriter::rewrite(retNode
);
1212 d_normalizedCache
[r
] = retNode
;
1216 bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel
* m
)
1221 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel
* m
)
1223 if (m
->areFunctionValuesEnabled())
1230 void TheoryEngineModelBuilder::assignFunction(TheoryModel
* m
, Node f
)
1232 Assert(!options::ufHo());
1233 uf::UfModelTree
ufmt(f
);
1235 for (size_t i
= 0; i
< m
->d_uf_terms
[f
].size(); i
++)
1237 Node un
= m
->d_uf_terms
[f
][i
];
1238 vector
<TNode
> children
;
1239 children
.push_back(f
);
1240 Trace("model-builder-debug") << " process term : " << un
<< std::endl
;
1241 for (size_t j
= 0; j
< un
.getNumChildren(); ++j
)
1243 Node rc
= m
->getRepresentative(un
[j
]);
1244 Trace("model-builder-debug2") << " get rep : " << un
[j
] << " returned "
1246 Assert(rc
.isConst());
1247 children
.push_back(rc
);
1249 Node simp
= NodeManager::currentNM()->mkNode(un
.getKind(), children
);
1250 Node v
= m
->getRepresentative(un
);
1251 Trace("model-builder") << " Setting (" << simp
<< ") to (" << v
<< ")"
1253 ufmt
.setValue(m
, simp
, v
);
1256 if (default_v
.isNull())
1258 // choose default value from model if none exists
1259 TypeEnumerator
te(f
.getType().getRangeType());
1262 ufmt
.setDefaultValue(m
, default_v
);
1263 bool condenseFuncValues
= options::condenseFunctionValues();
1264 if (condenseFuncValues
)
1268 std::stringstream ss
;
1270 Node val
= ufmt
.getFunctionValue(ss
.str().c_str(), condenseFuncValues
);
1271 m
->assignFunctionDefinition(f
, val
);
1272 // ufmt.debugPrint( std::cout, m );
1275 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel
* m
, Node f
)
1277 Assert(options::ufHo());
1278 TypeNode type
= f
.getType();
1279 std::vector
<TypeNode
> argTypes
= type
.getArgTypes();
1280 std::vector
<Node
> args
;
1281 std::vector
<TNode
> apply_args
;
1282 for (unsigned i
= 0; i
< argTypes
.size(); i
++)
1284 Node v
= NodeManager::currentNM()->mkBoundVar(argTypes
[i
]);
1288 apply_args
.push_back(v
);
1291 // start with the base return value (currently we use the same default value
1292 // for all functions)
1293 TypeEnumerator
te(type
.getRangeType());
1295 std::map
<Node
, std::vector
<Node
> >::iterator itht
= m
->d_ho_uf_terms
.find(f
);
1296 if (itht
!= m
->d_ho_uf_terms
.end())
1298 for (size_t i
= 0; i
< itht
->second
.size(); i
++)
1300 Node hn
= itht
->second
[i
];
1301 Trace("model-builder-debug") << " process : " << hn
<< std::endl
;
1302 Assert(hn
.getKind() == kind::HO_APPLY
);
1303 Assert(m
->areEqual(hn
[0], f
));
1304 Node hni
= m
->getRepresentative(hn
[1]);
1305 Trace("model-builder-debug2") << " get rep : " << hn
[0]
1306 << " returned " << hni
<< std::endl
;
1307 Assert(hni
.isConst());
1308 Assert(hni
.getType().isSubtypeOf(args
[0].getType()));
1309 hni
= Rewriter::rewrite(args
[0].eqNode(hni
));
1310 Node hnv
= m
->getRepresentative(hn
);
1311 Trace("model-builder-debug2") << " get rep val : " << hn
1312 << " returned " << hnv
<< std::endl
;
1313 Assert(hnv
.isConst());
1314 if (!apply_args
.empty())
1316 Assert(hnv
.getKind() == kind::LAMBDA
1317 && hnv
[0].getNumChildren() + 1 == args
.size());
1318 std::vector
<TNode
> largs
;
1319 for (unsigned j
= 0; j
< hnv
[0].getNumChildren(); j
++)
1321 largs
.push_back(hnv
[0][j
]);
1323 Assert(largs
.size() == apply_args
.size());
1324 hnv
= hnv
[1].substitute(
1325 largs
.begin(), largs
.end(), apply_args
.begin(), apply_args
.end());
1326 hnv
= Rewriter::rewrite(hnv
);
1328 Assert(!TypeNode::leastCommonTypeNode(hnv
.getType(), curr
.getType())
1330 curr
= NodeManager::currentNM()->mkNode(kind::ITE
, hni
, hnv
, curr
);
1333 Node val
= NodeManager::currentNM()->mkNode(
1335 NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
),
1337 m
->assignFunctionDefinition(f
, val
);
1340 // This struct is used to sort terms by the "size" of their type
1341 // The size of the type is the number of nodes in the type, for example
1343 // size of Function( Int, Int ) is 3
1344 // size of Function( Function( Bool, Int ), Int ) is 5
1347 // stores the size of the type
1348 std::map
<TypeNode
, unsigned> d_type_size
;
1349 // get the size of type tn
1350 unsigned getTypeSize(TypeNode tn
)
1352 std::map
<TypeNode
, unsigned>::iterator it
= d_type_size
.find(tn
);
1353 if (it
!= d_type_size
.end())
1360 for (unsigned i
= 0; i
< tn
.getNumChildren(); i
++)
1362 sum
+= getTypeSize(tn
[i
]);
1364 d_type_size
[tn
] = sum
;
1370 // compares the type size of i and j
1371 // returns true iff the size of i is less than that of j
1372 // tiebreaks are determined by node value
1373 bool operator()(Node i
, Node j
)
1375 int si
= getTypeSize(i
.getType());
1376 int sj
= getTypeSize(j
.getType());
1392 void TheoryEngineModelBuilder::assignFunctions(TheoryModel
* m
)
1394 if (!options::assignFunctionValues())
1398 Trace("model-builder") << "Assigning function values..." << std::endl
;
1399 std::vector
<Node
> funcs_to_assign
= m
->getFunctionsToAssign();
1401 if (options::ufHo())
1403 // sort based on type size if higher-order
1404 Trace("model-builder") << "Sort functions by type..." << std::endl
;
1406 std::sort(funcs_to_assign
.begin(), funcs_to_assign
.end(), sts
);
1409 if (Trace
.isOn("model-builder"))
1411 Trace("model-builder") << "...have " << funcs_to_assign
.size()
1412 << " functions to assign:" << std::endl
;
1413 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1415 Node f
= funcs_to_assign
[k
];
1416 Trace("model-builder") << " [" << k
<< "] : " << f
<< " : "
1417 << f
.getType() << std::endl
;
1421 // construct function values
1422 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1424 Node f
= funcs_to_assign
[k
];
1425 Trace("model-builder") << " Function #" << k
<< " is " << f
<< std::endl
;
1426 // std::map< Node, std::vector< Node > >::iterator itht =
1427 // m->d_ho_uf_terms.find( f );
1428 if (!options::ufHo())
1430 Trace("model-builder") << " Assign function value for " << f
1431 << " based on APPLY_UF" << std::endl
;
1432 assignFunction(m
, f
);
1436 Trace("model-builder") << " Assign function value for " << f
1437 << " based on curried HO_APPLY" << std::endl
;
1438 assignHoFunction(m
, f
);
1441 Trace("model-builder") << "Finished assigning function values." << std::endl
;
1444 } /* namespace CVC4::theory */
1445 } /* namespace CVC4 */