From fe30a89067ff97a0aed7768af109574f00ee6e5e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Jun 2026 16:24:08 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/term_enumeration.cpp | 14 +------------- src/test/term_enumeration.cpp | 12 ------------ 2 files changed, 1 insertion(+), 25 deletions(-) diff --git a/src/ast/term_enumeration.cpp b/src/ast/term_enumeration.cpp index 84f32e967..872a6c5f4 100644 --- a/src/ast/term_enumeration.cpp +++ b/src/ast/term_enumeration.cpp @@ -6,29 +6,20 @@ * * Key ideas: * - Terms are enumerated bottom-up by "cost" (calculated by tree size). - * - Observational equivalence (OE): two terms that produce the same outputs - * on all sample inputs are considered equivalent; only one representative - * per equivalence class is kept. * - A grammar describes which function symbols (operators) and leaves * (constants, variables) are available for enumeration. */ #include -#include #include #include #include "util/vector.h" -#include "util/ref.h" #include "util/obj_hashtable.h" #include "ast/ast.h" #include "ast/ast_ll_pp.h" #include "ast/ast_pp.h" -#include "ast/arith_decl_plugin.h" -#include "ast/bv_decl_plugin.h" -#include "ast/seq_decl_plugin.h" #include "ast/term_enumeration.h" -#include "model/model.h" -#include "model/model_evaluator.h" + namespace term_enum { @@ -518,8 +509,6 @@ struct term_enumeration::iterator::iter_imp { m_names.back().push_back(symbol()); } - #if 0 - // TODO: don't enable this until we ensure only generating whnf (beta-redex free) expressions. expr_ref_vector args(m); args.push_back(m.mk_const("a", range)); for (unsigned i = 0; i < m_decls.back().size(); ++i) { @@ -527,7 +516,6 @@ struct term_enumeration::iterator::iter_imp { } app_ref sel(autil.mk_select(args), m); m_imp.m_grammar.add_func_decl(sel->get_decl()); - #endif range = get_array_range(range); } diff --git a/src/test/term_enumeration.cpp b/src/test/term_enumeration.cpp index 5ab7069a1..cfa2d563d 100644 --- a/src/test/term_enumeration.cpp +++ b/src/test/term_enumeration.cpp @@ -257,18 +257,6 @@ static void tst_nested_array_enumeration() { ENSURE(count >= 1); // At least the constant array std::cout << "Enumerated " << count << " terms of sort Array(A, Array(B, A))\n"; - - // Also enumerate terms of the inner array sort Array(B, A) - std::cout << "\nEnumerating terms of sort Array(B, A):\n"; - unsigned inner_count = 0; - for (expr* e : te.enum_terms(array_B_A)) { - std::cout << " Term " << inner_count << ": " << mk_pp(e, m) << "\n"; - inner_count++; - if (inner_count >= 10) break; - } - - // ENSURE(inner_count >= 1); - std::cout << "Enumerated " << inner_count << " terms of sort Array(B, A)\n"; te.display(std::cout); }