mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

fix typo in comment defining macros (#6306)

Browse source 
The existing comment describes macros as "formulas of the form
`(forall X (= (f X) T[X]))` ... where `T[X]` does not contain `X`". This is
incorrect; of course the macros' definitions are allowed to be in terms of
the macros' arguments. The comment should say "...does not contain `f`" because
macros can't be recursive.
This commit is contained in:
J Sailor 2022-08-28 20:49:52 -04:00 • committed by GitHub
parent a0ca5d745e
commit f5d2b9b89a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/macros/macro_manager.h
View file

@ -29,7 +29,7 @@ Revision History:
\brief Macros are universally quantified formulas of the form: \brief Macros are universally quantified formulas of the form:
(forall X (= (f X) T[X])) (forall X (= (f X) T[X]))
(forall X (iff (f X) T[X])) (forall X (iff (f X) T[X]))
where T[X] does not contain X. where T[X] does not contain f.
This class is responsible for storing macros and expanding them. This class is responsible for storing macros and expanding them.
It has support for backtracking and tagging declarations in an expression as forbidded for being macros. It has support for backtracking and tagging declarations in an expression as forbidded for being macros.