diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-04 14:00:09 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-04 19:00:09 +0000 |
| commit | b848e5a94e0d73214ec4cbcba4a08c0da2f239d5 (patch) | |
| tree | 5f99b67e8775a5881503cdfdbafe5efe07162907 /src/smt/env.cpp | |
| parent | 5712bdcd06a9f9502c3b5487386e1277702e25f4 (diff) | |
Move isFiniteType from theory engine to Env (#7287)
In preparation for breaking more dependencies on TheoryEngine.
Diffstat (limited to 'src/smt/env.cpp')
| -rw-r--r-- | src/smt/env.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 3267702fb..dafd13d98 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -19,6 +19,7 @@ #include "context/context.h" #include "expr/node.h" #include "options/base_options.h" +#include "options/quantifiers_options.h" #include "options/smt_options.h" #include "printer/printer.h" #include "proof/conv_proof_generator.h" @@ -212,4 +213,10 @@ Node Env::rewriteViaMethod(TNode n, MethodId idr) return n; } +bool Env::isFiniteType(TypeNode tn) const +{ + return isCardinalityClassFinite(tn.getCardinalityClass(), + d_options.quantifiers.finiteModelFind); +} + } // namespace cvc5 |