mirror of
https://github.com/Z3Prover/z3
synced 2025-04-11 03:33:35 +00:00
add documentation comment to bind_variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6f0155ce94
commit
e3098b0ec5
|
@ -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);
|
||||
|
||||
/**
|
||||
|
|
Loading…
Reference in a new issue