Updated the compilation instructions in the README to reflect changes in the Mona installation process. The repository now uses 'mona-1.4-modif.tar.gz' and a streamlined './install.sh' script instead of the old configure and make steps. This simplifies the setup process for new users.

Updated the README instructions for compiling Mona to reflect current versioning and installation practices. Switched from a custom script to standard configure and make commands for better compatibility. This should streamline the setup process for new users significantly.

This commit adds two archive artifacts, mona-1.4-orig.tar.gz and mona-1.4-modif.tar.gz, which appear to capture the upstream MONA 1.4 source and a locally modified variant. While there’s no code diff to inspect directly here, checking these into the repo likely supports reproducible patching, comparison, or packaging work around MONA. The practical effect is that the project now has the source inputs on hand for downstream build or integration tasks.

This commit backs out part of a previous solver behavior change that always ran pretty-action computation during heap entailment, which could trigger unwanted side effects even when pretty printing was not requested. It introduces a new global pretty_print flag, wires it to a --pprint CLI option, and makes the solver choose compute_pretty_actions only when that flag is enabled, otherwise falling back to the normal action path. The result is safer default execution with pretty-printing preserved as an explicit opt-in.

This change is a terminology cleanup in remove-aliases.py: the grammar rule, recursive parser references, comments, and working variables now consistently use formula instead of entailment. The behavior of the alias-removal pipeline does not appear to change, but the code is easier to follow and better matches the broader concept the script is actually parsing. Practical effect: no functional difference, just clearer parser semantics for future maintenance.

This change adds a targeted cleanup step in remove-aliases.py to strip a specific &{FLOW,(20,21)=__norm#E}[] suffix before entailment processing continues. The issue was likely causing unrelated flow metadata to be treated as part of the logical entailment, which could break or confuse the downstream fixpoint logic. In practice, alias removal should now behave more predictably on inputs that include this extra annotation.

This fixes a parsing bug in visit_restHead where the code was incorrectly indexing into node.children[0] before unpacking, which could break traversal for that grammar branch. The change now unpacks node.children directly, aligning the visitor with the actual parse tree structure and letting alias-removal logic continue to inspect boolExp and alias nodes correctly. In practice, this should make the alias cleanup pass more reliable for inputs that hit restHead.

This updates remove-aliases.py to treat quantified predicate forms as valid boolean expressions by introducing a quantifierPred rule. The parser can now handle expressions shaped like pred(arg: entailment), which were previously outside the grammar and likely rejected or mishandled during alias removal. In practice, this broadens the supported input language and makes the transformation step work on more complex logical formulas.

The parser grammar in remove-aliases.py previously recognized * and + in expression contexts but omitted -, which could cause valid subtraction expressions to fail during alias removal. This change extends operatorsExp to include the minus operator, bringing the grammar in line with expected arithmetic syntax. Practically, expressions using subtraction should now parse and transform cleanly.

This change cleans up remove-aliases.py by extracting inline operator tokens like |-, comparison operators, and arithmetic operators into dedicated grammar rules. The parser behavior stays the same, but the grammar is now more structured and readable, which makes future changes to expression handling less error-prone. In practice, this is a small but useful maintainability improvement for anyone evolving the alias-removal logic.

This change renames the start and end delimiters used for quasiquoted entailments, replacing e with f to better reflect that the quoted content is a formula. The update touches both the OCaml debug/pretty-print path in context.ml and the remove-aliases.py parser so generated output and downstream alias rewriting stay in sync. It’s a small syntax cleanup, but it reduces ambiguity and keeps the tooling consistent around formula quasiquotes. Practical effect: formula snippets now use the clearer [f| ... |f] form everywhere.

This change rewrites the Parsimonious grammar in remove-aliases.py to parse more generic aliased statements instead of assuming a strict left-hand-side |- right-hand-side entailment structure. The grammar now treats |-, *, and & uniformly as statement separators, simplifies expression rules, and updates the visitor methods to match the new parse tree shape. In practice, the alias remover should now work on a wider range of inputs with less special-casing.

This change relaxes the grammar in remove-aliases.py so heapPred can match forms where the expression inside ::<...> is optional instead of mandatory. That makes the parser more tolerant of heap predicate variants that omit that segment, which likely avoids failures on valid inputs the script previously rejected. In practice, alias removal should now work across a wider range of heap annotations with fewer parse errors.

This change fixes a parser ambiguity in the boolean expression grammar by moving <= and >= ahead of < and > in the alternation list. Without that ordering, shorter operators can greedily match first and break parsing for the longer comparison forms. The update makes alias removal more reliable for expressions using non-strict comparisons, with a small but meaningful correctness improvement.

This change adjusts remove-aliases.py so boolExp can compare either plain expressions or expEnclosed values, instead of only bare exp terms. That fixes a parser limitation where parenthesized or enclosed expressions could not participate in <, >, <=, or >= boolean predicates. In practice, the alias-removal pass should now accept and handle a broader range of valid conditional syntax more reliably.