1 /********************* */
2 /*! \file term_enumeration.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief Implementation of term enumeration utility
13 **/
14
15 #include "theory/quantifiers/term_enumeration.h"
16
17 #include "options/quantifiers_options.h"
18 #include "theory/quantifiers/term_util.h"
19 #include "theory/rewriter.h"
20
21 using namespace CVC4::kind;
22
23 namespace CVC4 {
24 namespace theory {
25 namespace quantifiers {
26
getEnumerateTerm(TypeNode tn,unsigned index)27 Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
28 {
29 Trace("term-db-enum") << "Get enumerate term " << tn << " " << index
30 << std::endl;
31 std::unordered_map<TypeNode, size_t, TypeNodeHashFunction>::iterator it =
32 d_typ_enum_map.find(tn);
33 size_t teIndex;
34 if (it == d_typ_enum_map.end())
35 {
36 teIndex = d_typ_enum.size();
37 d_typ_enum_map[tn] = teIndex;
38 d_typ_enum.push_back(TypeEnumerator(tn));
39 }
40 else
41 {
42 teIndex = it->second;
43 }
44 while (index >= d_enum_terms[tn].size())
45 {
46 if (d_typ_enum[teIndex].isFinished())
47 {
48 return Node::null();
49 }
50 d_enum_terms[tn].push_back(*d_typ_enum[teIndex]);
51 ++d_typ_enum[teIndex];
52 }
53 return d_enum_terms[tn][index];
54 }
55
mayComplete(TypeNode tn)56 bool TermEnumeration::mayComplete(TypeNode tn)
57 {
58 std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
59 d_may_complete.find(tn);
60 if (it == d_may_complete.end())
61 {
62 // cache
63 bool mc = mayComplete(tn, options::fmfTypeCompletionThresh());
64 d_may_complete[tn] = mc;
65 return mc;
66 }
67 return it->second;
68 }
69
mayComplete(TypeNode tn,unsigned maxCard)70 bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard)
71 {
72 bool mc = false;
73 if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
74 {
75 Cardinality c = tn.getCardinality();
76 if (!c.isLargeFinite())
77 {
78 NodeManager* nm = NodeManager::currentNM();
79 Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
80 // check if less than fixed upper bound
81 Node oth = nm->mkConst(Rational(maxCard));
82 Node eq = nm->mkNode(LEQ, card, oth);
83 eq = Rewriter::rewrite(eq);
84 mc = eq.isConst() && eq.getConst<bool>();
85 }
86 }
87 return mc;
88 }
89
90 } /* CVC4::theory::quantifiers namespace */
91 } /* CVC4::theory namespace */
92 } /* CVC4 namespace */
93