From e3098b0ec59ddf46c8f25402828d62d2fe21c122 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 May 2014 11:20:15 -0700 Subject: [PATCH] add documentation comment to bind_variables Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 51b54bc01..1952cc42f 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -278,6 +278,12 @@ namespace datalog { void register_variable(func_decl* var); + /* + Replace constants that have been registered as + variables by de-Bruijn indices and corresponding + universal (if is_forall is true) or existential + quantifier. + */ expr_ref bind_variables(expr* fml, bool is_forall); /**