0
I Use This!
High Activity

Commits : Listings

Analyzed about 11 hours ago. based on code collected about 11 hours ago.
Jul 31, 2024 — Jul 31, 2025
Commit Message Contributor Files Modified Lines Added Lines Removed Code Location Date
Replace std::sort with std::stable_sort when the given relation is just a partial order. This change avoids discrepancies when using different implmentations of std::sort. More... over 12 years ago
dl_bit_blasting: run simplifier before bit-blasting, in order to comply with its precondition More... over 12 years ago
Fix typos More... over 12 years ago
rule_manager::mk(): default initialization of m_proof to null More... over 12 years ago
qe_lite> fix crash in is_var_eq() (by me & Nikolaj) More... over 12 years ago
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable More... over 12 years ago
fix build warning, make context simplifier traverse subterms More... over 12 years ago
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable More... over 12 years ago
Add option :bv-sort-ac true More... over 12 years ago
fix build breaks More... over 12 years ago
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable More... over 12 years ago
fix build breaks More... over 12 years ago
Fix gcc compilation errors More... over 12 years ago
Remove trace msg More... over 12 years ago
Fix non ASCII character More... over 12 years ago
missing hnf More... over 12 years ago
local changes More... over 12 years ago
significant update to Horn routines: add module hnf to extract Horn normal form (removed from rule_manager). Associate proof objects with rules to track (all) rewrites, so that proof traces can be tracked back to original rules after transformations More... over 12 years ago
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable More... over 12 years ago
add unit test for previous commit More... over 12 years ago
bit_vector: fix operator==() for the case that num_bits is a multiple of 32 More... over 12 years ago
Revert "fix crash in qe_lite::is_var_eq" More... over 12 years ago
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable More... over 12 years ago
fix crash in qe_lite::is_var_eq More... over 12 years ago
fix overloading of complement from base_table More... over 12 years ago
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable More... over 12 years ago
remove debug code More... over 12 years ago
make model and proof converters a reference More... over 12 years ago
move quantifier hoist routines to quant_hoist More... over 12 years ago
Move ast_counter to location for common utilities. It depends on get_free_vars, so is in rewriter directory More... over 12 years ago