Skip to content

Commit 5828e70

Browse files
committed
rename instantiate_quantifier function
Quantifier instantiation may happen eagerly, or incrementally, and renaming this function clarifies that this function is doing eager instantiation.
1 parent 77442e7 commit 5828e70

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

src/solvers/flattening/boolbv_quantifier.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -138,8 +138,9 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
138138
return {};
139139
}
140140

141-
static optionalt<exprt>
142-
instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
141+
static optionalt<exprt> eager_quantifier_instantiation(
142+
const quantifier_exprt &expr,
143+
const namespacet &ns)
143144
{
144145
const symbol_exprt &var_expr = expr.symbol();
145146

@@ -223,7 +224,7 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
223224
auto new_src =
224225
quantifier_exprt(src.id(), std::move(fresh_symbols), where_replaced);
225226

226-
const auto res = instantiate_quantifier(src, ns);
227+
const auto res = eager_quantifier_instantiation(src, ns);
227228

228229
if(res)
229230
return convert_bool(*res);

0 commit comments

Comments
 (0)