* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros
* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md
* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled
* trace: improve trace tag handling system with hierarchical tagging
- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
(class names and descriptions to be refined in a future update)
* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals
* trace : add cstring header
* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py
* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.
* trace : Add TODO comment for future implementation of tag_class activation
* trace : Disable code related to tag_class until implementation is ready (#7663).
* Make spacer_sem_matcher::reset() public
* Add .clang-format for src/muz/spacer
* Mark substitution::get_bindings() as const
* Fix in spacer_antiunify
* Various helper methods in spacer_util
Minor functions to compute number of free variables, detect presence of certain
sub-expressions, etc.
The diff is ugly because of clang-format
* Add spacer_cluster for clustering lemmas
A cluster of lemmas is a set of lemmas that are all instances of the same
pattern, where a pattern is a qff formula with free variables.
Currently, the instances are required to be explicit, that is, they are all
obtained by substituting concrete values (i.e., numbers) for free variables of
the pattern.
Lemmas are clustered in cluster_db in each predicate transformer.
* Integrate spacer_cluster into spacer_context
* Custom clang-format pragmas for spacer_context
spacer_context.(cpp|h) are large and have inconsistent formatting. Disable
clang-format for them until merge with main z3 branch and re-format.
* Computation of convex closure and matrix kernel
Various LA functions. The implementations are somewhat preliminary.
Convex closure is simplemented via syntactic convex closure procedure.
Kernel computation considers many common cases.
spacer_arith_kernel_sage implements kernel computation by call external
Sage binary. It is used only for debugging and experiments. There is no
link dependence on Sage. If desired, it can be removed.
* Add spacer_concretize
* Utility methods for spacer conjecture rule
* Add spacer_expand_bnd_generalizer
Generalizes arithmetic inequality literals of the form x <= c,
by changing constant c to other constants found in the problem.
* Add spacer_global_generalizer
Global generalizer checks every new lemma against a cluster
of previously learned lemmas, and, if possible, conjectures
a new pob, that, when blocked, generalizes multiple existing
lemmas.
* Remove fp.spacer.print_json option
The option is used to dump state of spacer into json for debugging.
It has been replaced by `fp.spacer.trace_file` that allows dumping an execution
of spacer. The json file can be reconstructed from the trace file elsewhere.
* Workaround for segfault in spacer_proof_utils
Issue #3 in hgvk94/z3
Segfault in some proof reduction. Avoid by bailing out on reduction.
* Revert bug for incomplete models
* Use local fresh variables in spacer_global_generalizer
* Cleanup of spacer_convex_closure
* Allow arbitrary expressions to name cols in convex_closure
* WIP: convex closure
* WIP: convex closure
* Fix bindings order in spacer_global_generalizer
The matcher creates substitution using std_order, which is
reverse of expected order (variable 0 is last). Adjust the code
appropriately for that.
* Increase verbosity level for smt_context stats
* Dead code in qe_mbp
* bug fixes in spacer_global_generalizer::subsumer
* Partially remove dependence of size of m_alphas
I want m_alphas to potentially be greater than currently used alpha variables.
This is helpful for reusing them across multiple calls to convex closure
* Subtle bug in kernel computation
Coefficient was being passed by reference and, therefore, was
being changed indirectly.
In the process, updated the code to be more generic to avoid rational
computation in the middle of matrix manipulation.
* another test for sparse_matrix_ops::kernel
* Implementation of matrix kernel using Fraction Free Elimination
Ensures that the kernel is int for int matrices. All divisions are exact.
* clang-format sparse_matrix_ops.h
* another implementation of ffe kernel in sparse_matrix_ops
* Re-do arith_kernel and convex_closure
* update spacer_global_generalization for new subsumer
* remove spacer.gg.use_sage parameter
* cleanup of spacer_global_generalizer
* Removed dependency on sage
* fix in spacer_convex_closure
* spacer_sem_matcher: consider an additional semantic matching
disabled until it is shown useful
* spacer_global_generalizer: improve do_conjecture
- if conjecture does not apply to pob, use lemma instead
- better normalization
- improve debug prints
* spacer_conjecture: formatting
* spacer_cluster: improve debug prints
* spacer_context: improve debug prints
* spacer_context: re-queue may pobs
enabled even if global re-queue is disabled
* spacer_cluster print formatting
* reset methods on pob
* cleanup of print and local variable names
* formatting
* reset generalization data once it has been used
* refactored extra pob creation during global guidance
* fix bug copying sparse matrix into spacer matrix
* bug fix in spacer_convex_closure
* formatting change in spacer_context
* spacer_cluster: get_min_lvl
chose level based on pob as well as lemmas
* spacer_context: add desired_level to pob
desired_level indicates at which level pob should be proved.
A pob will be pushed to desired_level if necessary
* spacer_context: renamed subsume stats
the name of success/failed was switched
* spacer_convex_closure: fix prototype of is_congruent_mod()
* spacer_convex_closure: hacks in infer_div_pred()
* spacer_util: do not expand literals with mod
By default, equality literal t=p is expanded into t<=p && t>=p
Disable the expansion in case t contains 'mod' operator since such
expansion is usually not helpful for divisibility
* spacer_util: rename m_util into m_arith
* spacer_util: cleanup normalize()
* spacer_util: formatting
* spacer_context: formatting cleanup on subsume and conjecture
* spacer_context: fix handling may pobs when abs_weakness is enabled
A pob might be undef, so weakness must be bumped up
* spacer_arith_kernel: enhance debug print
* spacer_global_generalizer: improve matching on conjecture
* spacer_global_generalizer: set desired level on conjecture pob
* spacer_global_generalizer: debug print
* spacer_global_generalizer: set min level on new pobs
the new level should not be higher than the pob that was generalized
* spacer_global_generalizer: do no re-create closed pobs
If a generalized pob exist and closed, do not re-create it.
* spacer_context: normalize twice
* spacer_context: forward propagate only same kind of pobs
* sketch of inductive generalizer
A better implementation of inductive generalizer that in addition to dropping
literals also attempts to weaken them.
Current implementation is a sketch to be extended based on examples/requirements.
* fix ordering in spacer_cluster_util
* fix resetting of substitution matcher in spacer_conjecture
Old code would forget to reset the substitution provided to the sem_matcher.
Thus, if the substitution was matched once (i.e., one literal of interest is
found), no other literal would be matched.
* add spacer_util is_normalized() method
used for debugging only
* simplify normalization of pob expressions
pob expressions are normalized to increase syntactic matching.
Some of the normalization rules seem out of place, so removing them for now.
* fix in spacer_global_generalizer
If conjecture fails, do not try other generalization strategies -- they will not apply.
* fix in spacer_context
do not check that may pob is blocked by existing lemmas.
It is likely to be blocked. Our goal is to block it again and generalize
to a new lemma.
This can be further improved by moving directly to generalization when pob is
blocked by existing lemmas...
Co-authored-by: hgvk94 <hgvk94@gmail.com>
The fix is to remove a hack that used a theory rewriter to simplify
the conversion. Now the conversion happens less often than possible.
Will need more thinking to fix properly.
The unsoundness at this point would cause SPACER to generate lemmas
that do not block a proof obligation and then get stuck in an infinite loop
blocking and generating the same lemma.
propositional formulas (disjunctions) can appear as literals. This
makes it tricky to recognize whether a formula is a unit clause when
re-building unit resolution.
Added work-around that identifies whether a formula is a literal based
on its appearance in previous unit resolution step.
This is a new version that conceptually addresses the bugs in
all previous version. However, it had a hard-to-debug memory
corruption. The bug appeared only in optimized compilation under
Linux with GCC.
This code is suspect and should be reviewed and further tested
- compute_marks didn't find all units
- call to m.mk_unit_resolution expects that there is at least one unit
- hyp-reduced proof wasn't used
- bug in early termination
- any hypothesis was replaced with the old derivation of the literal
- handle the case of a single literal premise under hypothesis that is
replaced by an empty clause under hypothesis
The algorithms implemented in the engine are described in the following papers
Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96
Nikolaj Bjørner, Arie Gurfinkel:
Property Directed Polyhedral Abstraction. VMCAI 2015: 263-281
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki:
SMT-Based Model Checking for Recursive Programs. CAV 2014: 17-34
