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
.isSort() || !t
.isInterpretedFinite())
787 // If its interpreted as infinite, we get a fresh value that does
788 // not occur in the model.
789 // Note we also consider uninterpreted sorts to be infinite here
790 // regardless of whether isInterpretedFinite is true (which is true
791 // for uninterpreted sorts iff finite model finding is enabled).
792 // This is required because the UF solver does not explicitly
793 // assign uninterpreted constants to equivalence classes in its
794 // collectModelValues method. Doing so would have the same effect
795 // as running the code in this case.
799 Trace("model-builder-debug") << "Enumerate term of type " << t
801 n
= typeConstSet
.nextTypeEnum(t
, true);
802 //--- AJR: this code checks whether n is a legal value
805 Trace("model-builder-debug") << "Check if excluded : " << n
807 #ifdef CVC4_ASSERTIONS
808 if (isUSortFiniteRestricted
)
810 // must not involve uninterpreted constants beyond cardinality
811 // bound (which assumed to coincide with #eqc)
812 // this is just an assertion now, since TypeEnumeratorProperties
813 // should ensure that only legal values are enumerated wrt this
815 std::map
<Node
, bool> visited
;
816 success
= !isExcludedUSortValue(eqc_usort_count
, n
, visited
);
819 Trace("model-builder")
820 << "Excluded value for " << t
<< " : " << n
821 << " due to out of range uninterpreted constant."
827 if (success
&& isCorecursive
)
829 if (repSet
!= NULL
&& !repSet
->empty())
831 // in the case of codatatypes, check if it is in the set of
832 // values that we cannot assign
833 success
= !isExcludedCdtValue(n
, repSet
, assertedReps
, *i2
);
836 Trace("model-builder")
837 << "Excluded value : " << n
838 << " due to alpha-equivalent codatatype expression."
849 Trace("model-builder-debug")
850 << "Get first value from finite type..." << std::endl
;
851 // Otherwise, we get the first value from the type enumerator.
852 TypeEnumerator
te(t
);
855 Trace("model-builder-debug") << "...got " << n
<< std::endl
;
856 assignConstantRep(tm
, *i2
, n
);
868 // Corner case - I'm not sure this can even happen - but it's theoretically
869 // possible to have a cyclical dependency
870 // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
871 // this case, neither one will get assigned because we are waiting
872 // to be able to evaluate. But we will never be able to evaluate because
873 // the variables that need to be assigned are in
874 // these same EC's. In this case, repeat the whole fixed-point computation
875 // with the difference that the first EC
876 // that has both assignable and evaluable expressions will get assigned.
879 Assert(!assignOne
); // check for infinite loop!
884 #ifdef CVC4_ASSERTIONS
885 // Assert that all representatives have been converted to constants
886 for (it
= typeRepSet
.begin(); it
!= typeRepSet
.end(); ++it
)
888 set
<Node
>& repSet
= TypeSet::getSet(it
);
891 Trace("model-builder") << "***Non-empty repSet, size = " << repSet
.size()
892 << ", first = " << *(repSet
.begin()) << endl
;
896 #endif /* CVC4_ASSERTIONS */
898 Trace("model-builder") << "Copy representatives to model..." << std::endl
;
900 std::map
<Node
, Node
>::iterator itMap
;
901 for (itMap
= d_constantReps
.begin(); itMap
!= d_constantReps
.end(); ++itMap
)
903 tm
->d_reps
[itMap
->first
] = itMap
->second
;
904 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
907 Trace("model-builder") << "Make sure ECs have reps..." << std::endl
;
908 // Make sure every EC has a rep
909 for (itMap
= assertedReps
.begin(); itMap
!= assertedReps
.end(); ++itMap
)
911 tm
->d_reps
[itMap
->first
] = itMap
->second
;
912 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
914 for (it
= typeNoRepSet
.begin(); it
!= typeNoRepSet
.end(); ++it
)
916 set
<Node
>& noRepSet
= TypeSet::getSet(it
);
917 for (const Node
& node
: noRepSet
)
919 tm
->d_reps
[node
] = node
;
920 tm
->d_rep_set
.add(node
.getType(), node
);
924 // modelBuilder-specific initialization
925 if (!processBuildModel(tm
))
927 Trace("model-builder")
928 << "TheoryEngineModelBuilder: fail process build model." << std::endl
;
931 Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl
;
934 void TheoryEngineModelBuilder::computeAssignableInfo(
936 TypeEnumeratorProperties
& tep
,
937 std::unordered_set
<Node
, NodeHashFunction
>& assignableEqc
,
938 std::unordered_set
<Node
, NodeHashFunction
>& evaluableEqc
,
939 std::map
<Node
, Assigner
>& eqcToAssigner
,
940 std::map
<Node
, Node
>& eqcToAssignerMaster
)
942 eq::EqualityEngine
* ee
= tm
->d_equalityEngine
;
943 bool computeAssigners
= tm
->hasAssignmentExclusionSets();
944 std::unordered_set
<Node
, NodeHashFunction
> processed
;
945 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(ee
);
946 // A flag set to true if the current equivalence class is assignable (see
948 bool assignable
= false;
949 // Set to true if the current equivalence class is evaluatable (see
951 bool evaluable
= false;
952 // Set to true if a term in the current equivalence class has been given an
953 // assignment exclusion set.
954 bool hasESet CVC4_UNUSED
= false;
955 // Set to true if we found that a term in the current equivalence class has
956 // been given an assignment exclusion set, and we have not seen this term
957 // as part of a previous assignment exclusion group. In other words, when
958 // this flag is true we construct a new assigner object with the current
959 // equivalence class as its master.
960 bool foundESet
= false;
961 // Look at all equivalence classes in the model
962 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
965 if (d_constantReps
.find(eqc
) != d_constantReps
.end())
967 // already assigned above, skip
970 // reset information for the current equivalence classe
975 // the assignment exclusion set for the current equivalence class
976 std::vector
<Node
> eset
;
977 // the group to which this equivalence class belongs when exclusion sets
978 // were assigned (see the argument group of
979 // TheoryModel::getAssignmentExclusionSet).
980 std::vector
<Node
> group
;
981 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, ee
);
982 // For each term in the current equivalence class, we update the above
983 // information. We may terminate this loop before looking at all terms if we
984 // have inferred the value of all of the information above.
985 for (; !eqc_i
.isFinished(); ++eqc_i
)
988 if (!isAssignable(n
))
991 if (!computeAssigners
)
995 // both flags set, we are done
999 // expressions that are not assignable should not be given assignment
1001 Assert(!tm
->getAssignmentExclusionSet(n
, group
, eset
));
1007 if (!computeAssigners
)
1011 // both flags set, we are done
1014 // we don't compute assigners, skip
1018 // process the assignment exclusion set for term n
1019 // was it processed as a slave of a group?
1020 if (processed
.find(n
) != processed
.end())
1022 // Should not have two assignment exclusion sets for the same
1023 // equivalence class
1025 Assert(eqcToAssignerMaster
.find(eqc
) != eqcToAssignerMaster
.end());
1026 // already processed as a slave term
1030 // was it assigned one?
1031 if (tm
->getAssignmentExclusionSet(n
, group
, eset
))
1033 // Should not have two assignment exclusion sets for the same
1034 // equivalence class
1042 assignableEqc
.insert(eqc
);
1046 evaluableEqc
.insert(eqc
);
1048 // If we found an assignment exclusion set, we construct a new assigner
1052 // we don't accept assignment exclusion sets for evaluable eqc
1054 // construct the assigner
1055 Assigner
& a
= eqcToAssigner
[eqc
];
1056 // Take the representatives of each term in the assignment exclusion
1057 // set, which ensures we can look up their value in d_constReps later.
1058 std::vector
<Node
> aes
;
1059 for (const Node
& e
: eset
)
1061 // Should only supply terms that occur in the model or constants
1062 // in assignment exclusion sets.
1063 Assert(tm
->hasTerm(e
) || e
.isConst());
1064 Node er
= tm
->hasTerm(e
) ? tm
->getRepresentative(e
) : e
;
1068 a
.initialize(eqc
.getType(), &tep
, aes
);
1069 // all others in the group are slaves of this
1070 for (const Node
& g
: group
)
1072 Assert(isAssignable(g
));
1073 if (!tm
->hasTerm(g
))
1075 // Ignore those that aren't in the model, in the case the user
1076 // has supplied an assignment exclusion set to a variable not in
1080 Node gr
= tm
->getRepresentative(g
);
1083 eqcToAssignerMaster
[gr
] = eqc
;
1084 // remember that this term has been processed
1085 processed
.insert(g
);
1092 void TheoryEngineModelBuilder::postProcessModel(bool incomplete
, TheoryModel
* m
)
1094 // if we are incomplete, there is no guarantee on the model.
1095 // thus, we do not check the model here.
1100 Assert(m
!= nullptr);
1101 // debug-check the model if the checkModels() is enabled.
1102 if (options::debugCheckModels())
1108 void TheoryEngineModelBuilder::debugCheckModel(TheoryModel
* tm
)
1110 #ifdef CVC4_ASSERTIONS
1111 if (tm
->hasApproximations())
1113 // models with approximations may fail the assertions below
1116 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
1117 std::map
<Node
, Node
>::iterator itMap
;
1118 // Check that every term evaluates to its representative in the model
1119 for (eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
1120 !eqcs_i
.isFinished();
1123 // eqc is the equivalence class representative
1124 Node eqc
= (*eqcs_i
);
1125 // get the representative
1126 Node rep
= tm
->getRepresentative(eqc
);
1127 if (!rep
.isConst() && eqc
.getType().isBoolean())
1129 // if Boolean, it does not necessarily have a constant representative, use
1130 // get value instead
1131 rep
= tm
->getValue(eqc
);
1132 Assert(rep
.isConst());
1134 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
1135 for (; !eqc_i
.isFinished(); ++eqc_i
)
1138 static int repCheckInstance
= 0;
1141 // non-linear mult is not necessarily accurate wrt getValue
1142 if (n
.getKind() != kind::NONLINEAR_MULT
)
1144 Debug("check-model::rep-checking") << "( " << repCheckInstance
<< ") "
1145 << "n: " << n
<< endl
1146 << "getValue(n): " << tm
->getValue(n
)
1148 << "rep: " << rep
<< endl
;
1149 Assert(tm
->getValue(*eqc_i
) == rep
)
1150 << "run with -d check-model::rep-checking for details";
1154 #endif /* CVC4_ASSERTIONS */
1156 // builder-specific debugging
1160 Node
TheoryEngineModelBuilder::normalize(TheoryModel
* m
, TNode r
, bool evalOnly
)
1162 std::map
<Node
, Node
>::iterator itMap
= d_constantReps
.find(r
);
1163 if (itMap
!= d_constantReps
.end())
1165 return (*itMap
).second
;
1167 NodeMap::iterator it
= d_normalizedCache
.find(r
);
1168 if (it
!= d_normalizedCache
.end())
1170 return (*it
).second
;
1172 Trace("model-builder-debug") << "do normalize on " << r
<< std::endl
;
1174 if (r
.getNumChildren() > 0)
1176 std::vector
<Node
> children
;
1177 if (r
.getMetaKind() == kind::metakind::PARAMETERIZED
)
1179 children
.push_back(r
.getOperator());
1181 bool childrenConst
= true;
1182 for (size_t i
= 0; i
< r
.getNumChildren(); ++i
)
1185 bool recurse
= true;
1188 if (m
->d_equalityEngine
->hasTerm(ri
))
1191 d_constantReps
.find(m
->d_equalityEngine
->getRepresentative(ri
));
1192 if (itMap
!= d_constantReps
.end())
1194 ri
= (*itMap
).second
;
1195 Trace("model-builder-debug") << i
<< ": const child " << ri
<< std::endl
;
1201 Trace("model-builder-debug") << i
<< ": keep " << ri
<< std::endl
;
1206 Trace("model-builder-debug") << i
<< ": no hasTerm " << ri
<< std::endl
;
1210 ri
= normalize(m
, ri
, evalOnly
);
1214 childrenConst
= false;
1217 children
.push_back(ri
);
1219 retNode
= NodeManager::currentNM()->mkNode(r
.getKind(), children
);
1222 retNode
= Rewriter::rewrite(retNode
);
1225 d_normalizedCache
[r
] = retNode
;
1229 bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel
* m
)
1234 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel
* m
)
1236 if (m
->areFunctionValuesEnabled())
1243 void TheoryEngineModelBuilder::assignFunction(TheoryModel
* m
, Node f
)
1245 Assert(!options::ufHo());
1246 uf::UfModelTree
ufmt(f
);
1248 for (size_t i
= 0; i
< m
->d_uf_terms
[f
].size(); i
++)
1250 Node un
= m
->d_uf_terms
[f
][i
];
1251 vector
<TNode
> children
;
1252 children
.push_back(f
);
1253 Trace("model-builder-debug") << " process term : " << un
<< std::endl
;
1254 for (size_t j
= 0; j
< un
.getNumChildren(); ++j
)
1256 Node rc
= m
->getRepresentative(un
[j
]);
1257 Trace("model-builder-debug2") << " get rep : " << un
[j
] << " returned "
1259 Assert(rc
.isConst());
1260 children
.push_back(rc
);
1262 Node simp
= NodeManager::currentNM()->mkNode(un
.getKind(), children
);
1263 Node v
= m
->getRepresentative(un
);
1264 Trace("model-builder") << " Setting (" << simp
<< ") to (" << v
<< ")"
1266 ufmt
.setValue(m
, simp
, v
);
1269 if (default_v
.isNull())
1271 // choose default value from model if none exists
1272 TypeEnumerator
te(f
.getType().getRangeType());
1275 ufmt
.setDefaultValue(m
, default_v
);
1276 bool condenseFuncValues
= options::condenseFunctionValues();
1277 if (condenseFuncValues
)
1281 std::stringstream ss
;
1283 Node val
= ufmt
.getFunctionValue(ss
.str().c_str(), condenseFuncValues
);
1284 m
->assignFunctionDefinition(f
, val
);
1285 // ufmt.debugPrint( std::cout, m );
1288 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel
* m
, Node f
)
1290 Assert(options::ufHo());
1291 TypeNode type
= f
.getType();
1292 std::vector
<TypeNode
> argTypes
= type
.getArgTypes();
1293 std::vector
<Node
> args
;
1294 std::vector
<TNode
> apply_args
;
1295 for (unsigned i
= 0; i
< argTypes
.size(); i
++)
1297 Node v
= NodeManager::currentNM()->mkBoundVar(argTypes
[i
]);
1301 apply_args
.push_back(v
);
1304 // start with the base return value (currently we use the same default value
1305 // for all functions)
1306 TypeEnumerator
te(type
.getRangeType());
1308 std::map
<Node
, std::vector
<Node
> >::iterator itht
= m
->d_ho_uf_terms
.find(f
);
1309 if (itht
!= m
->d_ho_uf_terms
.end())
1311 for (size_t i
= 0; i
< itht
->second
.size(); i
++)
1313 Node hn
= itht
->second
[i
];
1314 Trace("model-builder-debug") << " process : " << hn
<< std::endl
;
1315 Assert(hn
.getKind() == kind::HO_APPLY
);
1316 Assert(m
->areEqual(hn
[0], f
));
1317 Node hni
= m
->getRepresentative(hn
[1]);
1318 Trace("model-builder-debug2") << " get rep : " << hn
[0]
1319 << " returned " << hni
<< std::endl
;
1320 Assert(hni
.isConst());
1321 Assert(hni
.getType().isSubtypeOf(args
[0].getType()));
1322 hni
= Rewriter::rewrite(args
[0].eqNode(hni
));
1323 Node hnv
= m
->getRepresentative(hn
);
1324 Trace("model-builder-debug2") << " get rep val : " << hn
1325 << " returned " << hnv
<< std::endl
;
1326 Assert(hnv
.isConst());
1327 if (!apply_args
.empty())
1329 Assert(hnv
.getKind() == kind::LAMBDA
1330 && hnv
[0].getNumChildren() + 1 == args
.size());
1331 std::vector
<TNode
> largs
;
1332 for (unsigned j
= 0; j
< hnv
[0].getNumChildren(); j
++)
1334 largs
.push_back(hnv
[0][j
]);
1336 Assert(largs
.size() == apply_args
.size());
1337 hnv
= hnv
[1].substitute(
1338 largs
.begin(), largs
.end(), apply_args
.begin(), apply_args
.end());
1339 hnv
= Rewriter::rewrite(hnv
);
1341 Assert(!TypeNode::leastCommonTypeNode(hnv
.getType(), curr
.getType())
1343 curr
= NodeManager::currentNM()->mkNode(kind::ITE
, hni
, hnv
, curr
);
1346 Node val
= NodeManager::currentNM()->mkNode(
1348 NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
),
1350 m
->assignFunctionDefinition(f
, val
);
1353 // This struct is used to sort terms by the "size" of their type
1354 // The size of the type is the number of nodes in the type, for example
1356 // size of Function( Int, Int ) is 3
1357 // size of Function( Function( Bool, Int ), Int ) is 5
1360 // stores the size of the type
1361 std::map
<TypeNode
, unsigned> d_type_size
;
1362 // get the size of type tn
1363 unsigned getTypeSize(TypeNode tn
)
1365 std::map
<TypeNode
, unsigned>::iterator it
= d_type_size
.find(tn
);
1366 if (it
!= d_type_size
.end())
1373 for (unsigned i
= 0; i
< tn
.getNumChildren(); i
++)
1375 sum
+= getTypeSize(tn
[i
]);
1377 d_type_size
[tn
] = sum
;
1383 // compares the type size of i and j
1384 // returns true iff the size of i is less than that of j
1385 // tiebreaks are determined by node value
1386 bool operator()(Node i
, Node j
)
1388 int si
= getTypeSize(i
.getType());
1389 int sj
= getTypeSize(j
.getType());
1405 void TheoryEngineModelBuilder::assignFunctions(TheoryModel
* m
)
1407 if (!options::assignFunctionValues())
1411 Trace("model-builder") << "Assigning function values..." << std::endl
;
1412 std::vector
<Node
> funcs_to_assign
= m
->getFunctionsToAssign();
1414 if (options::ufHo())
1416 // sort based on type size if higher-order
1417 Trace("model-builder") << "Sort functions by type..." << std::endl
;
1419 std::sort(funcs_to_assign
.begin(), funcs_to_assign
.end(), sts
);
1422 if (Trace
.isOn("model-builder"))
1424 Trace("model-builder") << "...have " << funcs_to_assign
.size()
1425 << " functions to assign:" << std::endl
;
1426 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1428 Node f
= funcs_to_assign
[k
];
1429 Trace("model-builder") << " [" << k
<< "] : " << f
<< " : "
1430 << f
.getType() << std::endl
;
1434 // construct function values
1435 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1437 Node f
= funcs_to_assign
[k
];
1438 Trace("model-builder") << " Function #" << k
<< " is " << f
<< std::endl
;
1439 // std::map< Node, std::vector< Node > >::iterator itht =
1440 // m->d_ho_uf_terms.find( f );
1441 if (!options::ufHo())
1443 Trace("model-builder") << " Assign function value for " << f
1444 << " based on APPLY_UF" << std::endl
;
1445 assignFunction(m
, f
);
1449 Trace("model-builder") << " Assign function value for " << f
1450 << " based on curried HO_APPLY" << std::endl
;
1451 assignHoFunction(m
, f
);
1454 Trace("model-builder") << "Finished assigning function values." << std::endl
;
1457 } /* namespace CVC4::theory */
1458 } /* namespace CVC4 */