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(Model
* m
)
377 Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl
;
378 TheoryModel
* tm
= (TheoryModel
*)m
;
379 eq::EqualityEngine
* ee
= tm
->d_equalityEngine
;
381 // buildModel should only be called once per check
382 Assert(!tm
->isBuilt());
388 tm
->d_modelBuilt
= true;
389 tm
->d_modelBuiltSuccess
= false;
391 // Collect model info from the theories
392 Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
394 if (!d_te
->collectModelInfo(tm
))
396 Trace("model-builder")
397 << "TheoryEngineModelBuilder: fail collect model info" << std::endl
;
401 Trace("model-builder")
402 << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl
;
403 // model-builder specific initialization
404 if (!preProcessBuildModel(tm
))
406 Trace("model-builder")
407 << "TheoryEngineModelBuilder: fail preprocess build model."
412 Trace("model-builder")
413 << "TheoryEngineModelBuilder: Add assignable subterms..." << std::endl
;
414 // Loop through all terms and make sure that assignable sub-terms are in the
416 // Also, record #eqc per type (for finite model finding)
417 std::map
<TypeNode
, unsigned> eqc_usort_count
;
418 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(ee
);
421 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
423 eq::EqClassIterator eqc_i
= eq::EqClassIterator((*eqcs_i
), ee
);
424 for (; !eqc_i
.isFinished(); ++eqc_i
)
426 addAssignableSubterms(*eqc_i
, tm
, cache
);
428 TypeNode tn
= (*eqcs_i
).getType();
431 if (eqc_usort_count
.find(tn
) == eqc_usort_count
.end())
433 eqc_usort_count
[tn
] = 1;
437 eqc_usort_count
[tn
]++;
443 Trace("model-builder") << "Collect representatives..." << std::endl
;
445 // Process all terms in the equality engine, store representatives for each EC
446 d_constantReps
.clear();
447 std::map
<Node
, Node
> assertedReps
;
448 TypeSet typeConstSet
, typeRepSet
, typeNoRepSet
;
449 // Compute type enumerator properties. This code ensures we do not
450 // enumerate terms that have uninterpreted constants that violate the
451 // bounds imposed by finite model finding. For example, if finite
452 // model finding insists that there are only 2 values { U1, U2 } of type U,
453 // then the type enumerator for list of U should enumerate:
454 // nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ...
455 // instead of enumerating (cons U3 nil).
456 TypeEnumeratorProperties tep
;
457 if (options::finiteModelFind())
459 tep
.d_fixed_usort_card
= true;
460 for (std::map
<TypeNode
, unsigned>::iterator it
= eqc_usort_count
.begin();
461 it
!= eqc_usort_count
.end();
464 Trace("model-builder") << "Fixed bound (#eqc) for " << it
->first
<< " : "
465 << it
->second
<< std::endl
;
466 tep
.d_fixed_card
[it
->first
] = Integer(it
->second
);
468 typeConstSet
.setTypeEnumeratorProperties(&tep
);
471 // AJR: build ordered list of types that ensures that base types are
473 // (I think) this is only strictly necessary for finite model finding +
474 // parametric types instantiated with uninterpreted sorts, but is probably
475 // a good idea to do in general since it leads to models with smaller term
477 std::vector
<TypeNode
> type_list
;
478 eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
479 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
481 // eqc is the equivalence class representative
482 Node eqc
= (*eqcs_i
);
483 Trace("model-builder") << "Processing EC: " << eqc
<< endl
;
484 Assert(tm
->d_equalityEngine
->getRepresentative(eqc
) == eqc
);
485 TypeNode eqct
= eqc
.getType();
486 Assert(assertedReps
.find(eqc
) == assertedReps
.end());
487 Assert(d_constantReps
.find(eqc
) == d_constantReps
.end());
489 // Loop through terms in this EC
491 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
492 for (; !eqc_i
.isFinished(); ++eqc_i
)
495 Trace("model-builder") << " Processing Term: " << n
<< endl
;
496 // Record as rep if this node was specified as a representative
497 if (tm
->d_reps
.find(n
) != tm
->d_reps
.end())
499 // AJR: I believe this assertion is too strict,
500 // e.g. datatypes may assert representative for two constructor terms
501 // that are not in the care graph and are merged during
503 // Assert(rep.isNull());
505 Assert(!rep
.isNull());
506 Trace("model-builder") << " Rep( " << eqc
<< " ) = " << rep
509 // Record as const_rep if this node is constant
512 Assert(const_rep
.isNull());
514 Trace("model-builder") << " ConstRep( " << eqc
<< " ) = " << const_rep
517 // model-specific processing of the term
518 tm
->addTermInternal(n
);
521 // Assign representative for this EC
522 if (!const_rep
.isNull())
524 // Theories should not specify a rep if there is already a constant in the
526 // AJR: I believe this assertion is too strict, eqc with asserted reps may
527 // merge with constant eqc
528 // Assert(rep.isNull() || rep == const_rep);
529 assignConstantRep(tm
, eqc
, const_rep
);
530 typeConstSet
.add(eqct
.getBaseType(), const_rep
);
532 else if (!rep
.isNull())
534 assertedReps
[eqc
] = rep
;
535 typeRepSet
.add(eqct
.getBaseType(), eqc
);
536 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
537 addToTypeList(eqct
.getBaseType(), type_list
, visiting
);
541 typeNoRepSet
.add(eqct
, eqc
);
542 std::unordered_set
<TypeNode
, TypeNodeHashFunction
> visiting
;
543 addToTypeList(eqct
, type_list
, visiting
);
547 Trace("model-builder") << "Compute assignable information..." << std::endl
;
548 // The set of equivalence classes that are "assignable"
549 std::unordered_set
<Node
, NodeHashFunction
> assignableEqc
;
550 // The set of equivalence classes that are "evaluable"
551 std::unordered_set
<Node
, NodeHashFunction
> evaluableEqc
;
552 // Assigner objects for relevant equivalence classes
553 std::map
<Node
, Assigner
> eqcToAssigner
;
554 // Maps equivalence classes to the equivalence class that maps to its assigner
555 // object in the above map.
556 std::map
<Node
, Node
> eqcToAssignerMaster
;
557 // Compute the above information
558 computeAssignableInfo(
559 tm
, tep
, assignableEqc
, evaluableEqc
, eqcToAssigner
, eqcToAssignerMaster
);
561 // Need to ensure that each EC has a constant representative.
563 Trace("model-builder") << "Processing EC's..." << std::endl
;
565 TypeSet::iterator it
;
566 vector
<TypeNode
>::iterator type_it
;
567 set
<Node
>::iterator i
, i2
;
568 bool changed
, unassignedAssignable
, assignOne
= false;
569 set
<TypeNode
> evaluableSet
;
571 // Double-fixed-point loop
572 // Outer loop handles a special corner case (see code at end of loop for
576 // Inner fixed-point loop: we are trying to learn constant values for every
577 // EC. Each time through this loop, we process all of the
578 // types by type and may learn some new EC values. EC's in one type may
579 // depend on EC's in another type, so we need a fixed-point loop
580 // to ensure that we learn as many EC values as possible
584 unassignedAssignable
= false;
585 evaluableSet
.clear();
587 // Iterate over all types we've seen
588 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
590 TypeNode t
= *type_it
;
591 TypeNode tb
= t
.getBaseType();
592 set
<Node
>* noRepSet
= typeNoRepSet
.getSet(t
);
594 // 1. Try to evaluate the EC's in this type
595 if (noRepSet
!= NULL
&& !noRepSet
->empty())
597 Trace("model-builder") << " Eval phase, working on type: " << t
600 d_normalizedCache
.clear();
601 for (i
= noRepSet
->begin(); i
!= noRepSet
->end();)
605 Trace("model-builder-debug") << "Look at eqc : " << (*i2
)
608 // only possible to normalize if we are evaluable
609 evaluable
= evaluableEqc
.find(*i2
) != evaluableEqc
.end();
612 normalized
= evaluateEqc(tm
, *i2
);
614 if (!normalized
.isNull())
616 Assert(normalized
.isConst());
617 typeConstSet
.add(tb
, normalized
);
618 assignConstantRep(tm
, *i2
, normalized
);
619 Trace("model-builder") << " Eval: Setting constant rep of "
620 << (*i2
) << " to " << normalized
<< endl
;
628 evaluableSet
.insert(tb
);
630 // If assignable, remember there is an equivalence class that is
631 // not assigned and assignable.
632 if (assignableEqc
.find(*i2
) != assignableEqc
.end())
634 unassignedAssignable
= true;
640 // 2. Normalize any non-const representative terms for this type
641 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
642 if (repSet
!= NULL
&& !repSet
->empty())
644 Trace("model-builder")
645 << " Normalization phase, working on type: " << t
<< endl
;
646 d_normalizedCache
.clear();
647 for (i
= repSet
->begin(); i
!= repSet
->end();)
649 Assert(assertedReps
.find(*i
) != assertedReps
.end());
650 Node rep
= assertedReps
[*i
];
651 Node normalized
= normalize(tm
, rep
, false);
652 Trace("model-builder") << " Normalizing rep (" << rep
653 << "), normalized to (" << normalized
<< ")"
655 if (normalized
.isConst())
658 typeConstSet
.add(tb
, normalized
);
659 assignConstantRep(tm
, *i
, normalized
);
660 assertedReps
.erase(*i
);
667 if (normalized
!= rep
)
669 assertedReps
[*i
] = normalized
;
679 if (!unassignedAssignable
)
684 // 3. Assign unassigned assignable EC's using type enumeration - assign a
685 // value *different* from all other EC's if the type is infinite
686 // Assign first value from type enumerator otherwise - for finite types, we
687 // rely on polite framework to ensure that EC's that have to be
688 // different are different.
690 // Only make assignments on a type if:
691 // 1. there are no terms that share the same base type with un-normalized
693 // 2. there are no terms that share teh same base type that are unevaluated
695 // Alternatively, if 2 or 3 don't hold but we are in a special
696 // deadlock-breaking mode where assignOne is true, go ahead and make one
699 // must iterate over the ordered type list to ensure that we do not
700 // enumerate values with subterms
701 // having types that we are currently enumerating (when possible)
702 // for example, this ensures we enumerate uninterpreted sort U before (List
703 // of U) and (Array U U)
704 // however, it does not break cyclic type dependencies for mutually
705 // recursive datatypes, but this is handled
706 // by recording all subterms of enumerated values in TypeSet::addSubTerms.
707 for (type_it
= type_list
.begin(); type_it
!= type_list
.end(); ++type_it
)
709 TypeNode t
= *type_it
;
710 // continue if there are no more equivalence classes of this type to
712 std::set
<Node
>* noRepSetPtr
= typeNoRepSet
.getSet(t
);
713 if (noRepSetPtr
== NULL
)
717 set
<Node
>& noRepSet
= *noRepSetPtr
;
718 if (noRepSet
.empty())
723 // get properties of this type
724 bool isCorecursive
= false;
727 const DType
& dt
= t
.getDType();
728 isCorecursive
= dt
.isCodatatype()
729 && (!dt
.isFinite(t
) || dt
.isRecursiveSingleton(t
));
731 #ifdef CVC4_ASSERTIONS
732 bool isUSortFiniteRestricted
= false;
733 if (options::finiteModelFind())
735 isUSortFiniteRestricted
= !t
.isSort() && involvesUSort(t
);
739 TypeNode tb
= t
.getBaseType();
742 set
<Node
>* repSet
= typeRepSet
.getSet(tb
);
743 if (repSet
!= NULL
&& !repSet
->empty())
747 if (evaluableSet
.find(tb
) != evaluableSet
.end())
752 Trace("model-builder") << " Assign phase, working on type: " << t
754 bool assignable
, evaluable CVC4_UNUSED
;
755 std::map
<Node
, Assigner
>::iterator itAssigner
;
756 std::map
<Node
, Node
>::iterator itAssignerM
;
757 set
<Node
>* repSet
= typeRepSet
.getSet(t
);
758 for (i
= noRepSet
.begin(); i
!= noRepSet
.end();)
762 // check whether it has an assigner object
763 itAssignerM
= eqcToAssignerMaster
.find(*i2
);
764 if (itAssignerM
!= eqcToAssignerMaster
.end())
766 // Take the master's assigner. Notice we don't care which order
767 // equivalence classes are assigned. For instance, the master can
768 // be assigned after one of its slaves.
769 itAssigner
= eqcToAssigner
.find(itAssignerM
->second
);
773 itAssigner
= eqcToAssigner
.find(*i2
);
775 if (itAssigner
!= eqcToAssigner
.end())
777 assignable
= isAssignerActive(tm
, itAssigner
->second
);
781 assignable
= assignableEqc
.find(*i2
) != assignableEqc
.end();
783 evaluable
= evaluableEqc
.find(*i2
) != evaluableEqc
.end();
784 Trace("model-builder-debug")
785 << " eqc " << *i2
<< " is assignable=" << assignable
786 << ", evaluable=" << evaluable
<< std::endl
;
789 Assert(!evaluable
|| assignOne
);
790 // this assertion ensures that if we are assigning to a term of
791 // Boolean type, then the term must be assignable.
792 // Note we only assign to terms of Boolean type if the term occurs in
793 // a singleton equivalence class; otherwise the term would have been
794 // in the equivalence class of true or false and would not need
796 Assert(!t
.isBoolean() || isAssignable(*i2
));
798 if (itAssigner
!= eqcToAssigner
.end())
800 Trace("model-builder-debug")
801 << "Get value from assigner for finite type..." << std::endl
;
802 // if it has an assigner, get the value from the assigner.
803 n
= itAssigner
->second
.getNextAssignment();
806 else if (!t
.isFinite())
808 // if its infinite, we get a fresh value that does not occur in
813 Trace("model-builder-debug") << "Enumerate term of type " << t
815 n
= typeConstSet
.nextTypeEnum(t
, true);
816 //--- AJR: this code checks whether n is a legal value
819 Trace("model-builder-debug") << "Check if excluded : " << n
821 #ifdef CVC4_ASSERTIONS
822 if (isUSortFiniteRestricted
)
824 // must not involve uninterpreted constants beyond cardinality
825 // bound (which assumed to coincide with #eqc)
826 // this is just an assertion now, since TypeEnumeratorProperties
827 // should ensure that only legal values are enumerated wrt this
829 std::map
<Node
, bool> visited
;
830 success
= !isExcludedUSortValue(eqc_usort_count
, n
, visited
);
833 Trace("model-builder")
834 << "Excluded value for " << t
<< " : " << n
835 << " due to out of range uninterpreted constant."
841 if (success
&& isCorecursive
)
843 if (repSet
!= NULL
&& !repSet
->empty())
845 // in the case of codatatypes, check if it is in the set of
846 // values that we cannot assign
847 success
= !isExcludedCdtValue(n
, repSet
, assertedReps
, *i2
);
850 Trace("model-builder")
851 << "Excluded value : " << n
852 << " due to alpha-equivalent codatatype expression."
863 Trace("model-builder-debug")
864 << "Get first value from finite type..." << std::endl
;
865 // Otherwise, we get the first value from the type enumerator.
866 TypeEnumerator
te(t
);
869 Trace("model-builder-debug") << "...got " << n
<< std::endl
;
870 assignConstantRep(tm
, *i2
, n
);
882 // Corner case - I'm not sure this can even happen - but it's theoretically
883 // possible to have a cyclical dependency
884 // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
885 // this case, neither one will get assigned because we are waiting
886 // to be able to evaluate. But we will never be able to evaluate because
887 // the variables that need to be assigned are in
888 // these same EC's. In this case, repeat the whole fixed-point computation
889 // with the difference that the first EC
890 // that has both assignable and evaluable expressions will get assigned.
893 Assert(!assignOne
); // check for infinite loop!
898 #ifdef CVC4_ASSERTIONS
899 // Assert that all representatives have been converted to constants
900 for (it
= typeRepSet
.begin(); it
!= typeRepSet
.end(); ++it
)
902 set
<Node
>& repSet
= TypeSet::getSet(it
);
905 Trace("model-builder") << "***Non-empty repSet, size = " << repSet
.size()
906 << ", first = " << *(repSet
.begin()) << endl
;
910 #endif /* CVC4_ASSERTIONS */
912 Trace("model-builder") << "Copy representatives to model..." << std::endl
;
914 std::map
<Node
, Node
>::iterator itMap
;
915 for (itMap
= d_constantReps
.begin(); itMap
!= d_constantReps
.end(); ++itMap
)
917 tm
->d_reps
[itMap
->first
] = itMap
->second
;
918 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
921 Trace("model-builder") << "Make sure ECs have reps..." << std::endl
;
922 // Make sure every EC has a rep
923 for (itMap
= assertedReps
.begin(); itMap
!= assertedReps
.end(); ++itMap
)
925 tm
->d_reps
[itMap
->first
] = itMap
->second
;
926 tm
->d_rep_set
.add(itMap
->second
.getType(), itMap
->second
);
928 for (it
= typeNoRepSet
.begin(); it
!= typeNoRepSet
.end(); ++it
)
930 set
<Node
>& noRepSet
= TypeSet::getSet(it
);
931 for (const Node
& node
: noRepSet
)
933 tm
->d_reps
[node
] = node
;
934 tm
->d_rep_set
.add(node
.getType(), node
);
938 // modelBuilder-specific initialization
939 if (!processBuildModel(tm
))
941 Trace("model-builder")
942 << "TheoryEngineModelBuilder: fail process build model." << std::endl
;
945 Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl
;
946 tm
->d_modelBuiltSuccess
= true;
949 void TheoryEngineModelBuilder::computeAssignableInfo(
951 TypeEnumeratorProperties
& tep
,
952 std::unordered_set
<Node
, NodeHashFunction
>& assignableEqc
,
953 std::unordered_set
<Node
, NodeHashFunction
>& evaluableEqc
,
954 std::map
<Node
, Assigner
>& eqcToAssigner
,
955 std::map
<Node
, Node
>& eqcToAssignerMaster
)
957 eq::EqualityEngine
* ee
= tm
->d_equalityEngine
;
958 bool computeAssigners
= tm
->hasAssignmentExclusionSets();
959 std::unordered_set
<Node
, NodeHashFunction
> processed
;
960 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(ee
);
961 // A flag set to true if the current equivalence class is assignable (see
963 bool assignable
= false;
964 // Set to true if the current equivalence class is evaluatable (see
966 bool evaluable
= false;
967 // Set to true if a term in the current equivalence class has been given an
968 // assignment exclusion set.
969 bool hasESet CVC4_UNUSED
= false;
970 // Set to true if we found that a term in the current equivalence class has
971 // been given an assignment exclusion set, and we have not seen this term
972 // as part of a previous assignment exclusion group. In other words, when
973 // this flag is true we construct a new assigner object with the current
974 // equivalence class as its master.
975 bool foundESet
= false;
976 // Look at all equivalence classes in the model
977 for (; !eqcs_i
.isFinished(); ++eqcs_i
)
980 if (d_constantReps
.find(eqc
) != d_constantReps
.end())
982 // already assigned above, skip
985 // reset information for the current equivalence classe
990 // the assignment exclusion set for the current equivalence class
991 std::vector
<Node
> eset
;
992 // the group to which this equivalence class belongs when exclusion sets
993 // were assigned (see the argument group of
994 // TheoryModel::getAssignmentExclusionSet).
995 std::vector
<Node
> group
;
996 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, ee
);
997 // For each term in the current equivalence class, we update the above
998 // information. We may terminate this loop before looking at all terms if we
999 // have inferred the value of all of the information above.
1000 for (; !eqc_i
.isFinished(); ++eqc_i
)
1003 if (!isAssignable(n
))
1006 if (!computeAssigners
)
1010 // both flags set, we are done
1014 // expressions that are not assignable should not be given assignment
1016 Assert(!tm
->getAssignmentExclusionSet(n
, group
, eset
));
1022 if (!computeAssigners
)
1026 // both flags set, we are done
1029 // we don't compute assigners, skip
1033 // process the assignment exclusion set for term n
1034 // was it processed as a slave of a group?
1035 if (processed
.find(n
) != processed
.end())
1037 // Should not have two assignment exclusion sets for the same
1038 // equivalence class
1040 Assert(eqcToAssignerMaster
.find(eqc
) != eqcToAssignerMaster
.end());
1041 // already processed as a slave term
1045 // was it assigned one?
1046 if (tm
->getAssignmentExclusionSet(n
, group
, eset
))
1048 // Should not have two assignment exclusion sets for the same
1049 // equivalence class
1057 assignableEqc
.insert(eqc
);
1061 evaluableEqc
.insert(eqc
);
1063 // If we found an assignment exclusion set, we construct a new assigner
1067 // we don't accept assignment exclusion sets for evaluable eqc
1069 // construct the assigner
1070 Assigner
& a
= eqcToAssigner
[eqc
];
1071 // Take the representatives of each term in the assignment exclusion
1072 // set, which ensures we can look up their value in d_constReps later.
1073 std::vector
<Node
> aes
;
1074 for (const Node
& e
: eset
)
1076 // Should only supply terms that occur in the model or constants
1077 // in assignment exclusion sets.
1078 Assert(tm
->hasTerm(e
) || e
.isConst());
1079 Node er
= tm
->hasTerm(e
) ? tm
->getRepresentative(e
) : e
;
1083 a
.initialize(eqc
.getType(), &tep
, aes
);
1084 // all others in the group are slaves of this
1085 for (const Node
& g
: group
)
1087 Assert(isAssignable(g
));
1088 if (!tm
->hasTerm(g
))
1090 // Ignore those that aren't in the model, in the case the user
1091 // has supplied an assignment exclusion set to a variable not in
1095 Node gr
= tm
->getRepresentative(g
);
1098 eqcToAssignerMaster
[gr
] = eqc
;
1099 // remember that this term has been processed
1100 processed
.insert(g
);
1107 void TheoryEngineModelBuilder::postProcessModel(bool incomplete
, Model
* m
)
1109 // if we are incomplete, there is no guarantee on the model.
1110 // thus, we do not check the model here.
1115 TheoryModel
* tm
= static_cast<TheoryModel
*>(m
);
1116 Assert(tm
!= nullptr);
1117 // debug-check the model if the checkModels() is enabled.
1118 if (options::debugCheckModels())
1120 debugCheckModel(tm
);
1124 void TheoryEngineModelBuilder::debugCheckModel(TheoryModel
* tm
)
1126 #ifdef CVC4_ASSERTIONS
1127 Assert(tm
->isBuilt());
1128 if (tm
->hasApproximations())
1130 // models with approximations may fail the assertions below
1133 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
1134 std::map
<Node
, Node
>::iterator itMap
;
1135 // Check that every term evaluates to its representative in the model
1136 for (eqcs_i
= eq::EqClassesIterator(tm
->d_equalityEngine
);
1137 !eqcs_i
.isFinished();
1140 // eqc is the equivalence class representative
1141 Node eqc
= (*eqcs_i
);
1142 // get the representative
1143 Node rep
= tm
->getRepresentative(eqc
);
1144 if (!rep
.isConst() && eqc
.getType().isBoolean())
1146 // if Boolean, it does not necessarily have a constant representative, use
1147 // get value instead
1148 rep
= tm
->getValue(eqc
);
1149 Assert(rep
.isConst());
1151 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, tm
->d_equalityEngine
);
1152 for (; !eqc_i
.isFinished(); ++eqc_i
)
1155 static int repCheckInstance
= 0;
1158 // non-linear mult is not necessarily accurate wrt getValue
1159 if (n
.getKind() != kind::NONLINEAR_MULT
)
1161 Debug("check-model::rep-checking") << "( " << repCheckInstance
<< ") "
1162 << "n: " << n
<< endl
1163 << "getValue(n): " << tm
->getValue(n
)
1165 << "rep: " << rep
<< endl
;
1166 Assert(tm
->getValue(*eqc_i
) == rep
)
1167 << "run with -d check-model::rep-checking for details";
1171 #endif /* CVC4_ASSERTIONS */
1173 // builder-specific debugging
1177 Node
TheoryEngineModelBuilder::normalize(TheoryModel
* m
, TNode r
, bool evalOnly
)
1179 std::map
<Node
, Node
>::iterator itMap
= d_constantReps
.find(r
);
1180 if (itMap
!= d_constantReps
.end())
1182 return (*itMap
).second
;
1184 NodeMap::iterator it
= d_normalizedCache
.find(r
);
1185 if (it
!= d_normalizedCache
.end())
1187 return (*it
).second
;
1189 Trace("model-builder-debug") << "do normalize on " << r
<< std::endl
;
1191 if (r
.getNumChildren() > 0)
1193 std::vector
<Node
> children
;
1194 if (r
.getMetaKind() == kind::metakind::PARAMETERIZED
)
1196 children
.push_back(r
.getOperator());
1198 bool childrenConst
= true;
1199 for (size_t i
= 0; i
< r
.getNumChildren(); ++i
)
1202 bool recurse
= true;
1205 if (m
->d_equalityEngine
->hasTerm(ri
))
1208 d_constantReps
.find(m
->d_equalityEngine
->getRepresentative(ri
));
1209 if (itMap
!= d_constantReps
.end())
1211 ri
= (*itMap
).second
;
1221 ri
= normalize(m
, ri
, evalOnly
);
1225 childrenConst
= false;
1228 children
.push_back(ri
);
1230 retNode
= NodeManager::currentNM()->mkNode(r
.getKind(), children
);
1233 retNode
= Rewriter::rewrite(retNode
);
1234 Assert(retNode
.getKind() == kind::APPLY_UF
1235 || !retNode
.getType().isFirstClass() || retNode
.isConst());
1238 d_normalizedCache
[r
] = retNode
;
1242 bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel
* m
)
1247 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel
* m
)
1249 if (m
->areFunctionValuesEnabled())
1256 void TheoryEngineModelBuilder::assignFunction(TheoryModel
* m
, Node f
)
1258 Assert(!options::ufHo());
1259 uf::UfModelTree
ufmt(f
);
1261 for (size_t i
= 0; i
< m
->d_uf_terms
[f
].size(); i
++)
1263 Node un
= m
->d_uf_terms
[f
][i
];
1264 vector
<TNode
> children
;
1265 children
.push_back(f
);
1266 Trace("model-builder-debug") << " process term : " << un
<< std::endl
;
1267 for (size_t j
= 0; j
< un
.getNumChildren(); ++j
)
1269 Node rc
= m
->getRepresentative(un
[j
]);
1270 Trace("model-builder-debug2") << " get rep : " << un
[j
] << " returned "
1272 Assert(rc
.isConst());
1273 children
.push_back(rc
);
1275 Node simp
= NodeManager::currentNM()->mkNode(un
.getKind(), children
);
1276 Node v
= m
->getRepresentative(un
);
1277 Trace("model-builder") << " Setting (" << simp
<< ") to (" << v
<< ")"
1279 ufmt
.setValue(m
, simp
, v
);
1282 if (default_v
.isNull())
1284 // choose default value from model if none exists
1285 TypeEnumerator
te(f
.getType().getRangeType());
1288 ufmt
.setDefaultValue(m
, default_v
);
1289 bool condenseFuncValues
= options::condenseFunctionValues();
1290 if (condenseFuncValues
)
1294 std::stringstream ss
;
1296 Node val
= ufmt
.getFunctionValue(ss
.str().c_str(), condenseFuncValues
);
1297 m
->assignFunctionDefinition(f
, val
);
1298 // ufmt.debugPrint( std::cout, m );
1301 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel
* m
, Node f
)
1303 Assert(options::ufHo());
1304 TypeNode type
= f
.getType();
1305 std::vector
<TypeNode
> argTypes
= type
.getArgTypes();
1306 std::vector
<Node
> args
;
1307 std::vector
<TNode
> apply_args
;
1308 for (unsigned i
= 0; i
< argTypes
.size(); i
++)
1310 Node v
= NodeManager::currentNM()->mkBoundVar(argTypes
[i
]);
1314 apply_args
.push_back(v
);
1317 // start with the base return value (currently we use the same default value
1318 // for all functions)
1319 TypeEnumerator
te(type
.getRangeType());
1321 std::map
<Node
, std::vector
<Node
> >::iterator itht
= m
->d_ho_uf_terms
.find(f
);
1322 if (itht
!= m
->d_ho_uf_terms
.end())
1324 for (size_t i
= 0; i
< itht
->second
.size(); i
++)
1326 Node hn
= itht
->second
[i
];
1327 Trace("model-builder-debug") << " process : " << hn
<< std::endl
;
1328 Assert(hn
.getKind() == kind::HO_APPLY
);
1329 Assert(m
->areEqual(hn
[0], f
));
1330 Node hni
= m
->getRepresentative(hn
[1]);
1331 Trace("model-builder-debug2") << " get rep : " << hn
[0]
1332 << " returned " << hni
<< std::endl
;
1333 Assert(hni
.isConst());
1334 Assert(hni
.getType().isSubtypeOf(args
[0].getType()));
1335 hni
= Rewriter::rewrite(args
[0].eqNode(hni
));
1336 Node hnv
= m
->getRepresentative(hn
);
1337 Trace("model-builder-debug2") << " get rep val : " << hn
1338 << " returned " << hnv
<< std::endl
;
1339 Assert(hnv
.isConst());
1340 if (!apply_args
.empty())
1342 Assert(hnv
.getKind() == kind::LAMBDA
1343 && hnv
[0].getNumChildren() + 1 == args
.size());
1344 std::vector
<TNode
> largs
;
1345 for (unsigned j
= 0; j
< hnv
[0].getNumChildren(); j
++)
1347 largs
.push_back(hnv
[0][j
]);
1349 Assert(largs
.size() == apply_args
.size());
1350 hnv
= hnv
[1].substitute(
1351 largs
.begin(), largs
.end(), apply_args
.begin(), apply_args
.end());
1352 hnv
= Rewriter::rewrite(hnv
);
1354 Assert(!TypeNode::leastCommonTypeNode(hnv
.getType(), curr
.getType())
1356 curr
= NodeManager::currentNM()->mkNode(kind::ITE
, hni
, hnv
, curr
);
1359 Node val
= NodeManager::currentNM()->mkNode(
1361 NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
),
1363 m
->assignFunctionDefinition(f
, val
);
1366 // This struct is used to sort terms by the "size" of their type
1367 // The size of the type is the number of nodes in the type, for example
1369 // size of Function( Int, Int ) is 3
1370 // size of Function( Function( Bool, Int ), Int ) is 5
1373 // stores the size of the type
1374 std::map
<TypeNode
, unsigned> d_type_size
;
1375 // get the size of type tn
1376 unsigned getTypeSize(TypeNode tn
)
1378 std::map
<TypeNode
, unsigned>::iterator it
= d_type_size
.find(tn
);
1379 if (it
!= d_type_size
.end())
1386 for (unsigned i
= 0; i
< tn
.getNumChildren(); i
++)
1388 sum
+= getTypeSize(tn
[i
]);
1390 d_type_size
[tn
] = sum
;
1396 // compares the type size of i and j
1397 // returns true iff the size of i is less than that of j
1398 // tiebreaks are determined by node value
1399 bool operator()(Node i
, Node j
)
1401 int si
= getTypeSize(i
.getType());
1402 int sj
= getTypeSize(j
.getType());
1418 void TheoryEngineModelBuilder::assignFunctions(TheoryModel
* m
)
1420 if (!options::assignFunctionValues())
1424 Trace("model-builder") << "Assigning function values..." << std::endl
;
1425 std::vector
<Node
> funcs_to_assign
= m
->getFunctionsToAssign();
1427 if (options::ufHo())
1429 // sort based on type size if higher-order
1430 Trace("model-builder") << "Sort functions by type..." << std::endl
;
1432 std::sort(funcs_to_assign
.begin(), funcs_to_assign
.end(), sts
);
1435 if (Trace
.isOn("model-builder"))
1437 Trace("model-builder") << "...have " << funcs_to_assign
.size()
1438 << " functions to assign:" << std::endl
;
1439 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1441 Node f
= funcs_to_assign
[k
];
1442 Trace("model-builder") << " [" << k
<< "] : " << f
<< " : "
1443 << f
.getType() << std::endl
;
1447 // construct function values
1448 for (unsigned k
= 0; k
< funcs_to_assign
.size(); k
++)
1450 Node f
= funcs_to_assign
[k
];
1451 Trace("model-builder") << " Function #" << k
<< " is " << f
<< std::endl
;
1452 // std::map< Node, std::vector< Node > >::iterator itht =
1453 // m->d_ho_uf_terms.find( f );
1454 if (!options::ufHo())
1456 Trace("model-builder") << " Assign function value for " << f
1457 << " based on APPLY_UF" << std::endl
;
1458 assignFunction(m
, f
);
1462 Trace("model-builder") << " Assign function value for " << f
1463 << " based on curried HO_APPLY" << std::endl
;
1464 assignHoFunction(m
, f
);
1467 Trace("model-builder") << "Finished assigning function values." << std::endl
;
1470 } /* namespace CVC4::theory */
1471 } /* namespace CVC4 */