Skip to content
Snippets Groups Projects
Select Git revision
  • 65-include-rule-aci_norm
  • add/bind_let
  • add/or_intro
  • add/shuffle
  • bv
  • comp_simplify
  • devel/alethelf
  • devel/bb2024
  • devel/bitblasting
  • devel/new-forall_inst
  • devel/pseudoboolean-bitblasting
  • devel/rules-index-arg
  • devel/thesis-backport
  • formal-semantic
  • master default
  • minted-2023-update
  • partial-cong
  • revert-c9505bb8
  • rules/connective_def
  • rules/forall_inst
  • 0.3
  • 0.2
  • 0.1
23 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.013May128729Apr282315108126Mar20141313Feb125Dec429Nov282323Oct223Sep15Aug1298719Jul17161519Jun1154329May2823864Apr119Mar188522Feb30Jan29262423191817108529Dec282125Nov19Oct1820Jul13May17Feb1013Jan923Dec1923Aug21191811Jul932126Jun2524232120192Dec29Nov2626Aug730Jul161510923Jun231May282726252419107128Apr2622212016151413connective_def: changelog updated accordinglyrules/connectiv…rules/connective_defMerge branch 'rules/forall_inst' into 'master'65-include-rule…65-include-rule-aci_norm masterAdd `pbblast_bvand_ith_bit` to the rules listdevel/pseudoboo…devel/pseudoboolean-bitblastingOrganize example of `pbblast_bvand_ith_bit`Standardize pb blasting on bvand and bvxorcleaning code in rule forall_instrules/forall_instrules/forall_instreverting changes in forall_instconnective_def: fixing order of elements in rule invocationconnective_def: added def. of exists in terms of forallminor fix in section 2: notation for substitution functionFixes in rule forall_inst: using simultaneous subst.; adding comments about simultaneous subst. in section 1Standardizing pb blasting notationAdapt `pbblast_bvxor` to the choice operatorAdapt definition of `pbblast_bvand` with the `choice` operation, add `pbblast_bvand_ith_bit`Merge branch 'rules/la_tautology' into 'master'Merge branch 'partial-cong' into 'master'Make `cong` more flexible.Fix typo in qnt_rm_unusedImprove la_tautology descriptionrules/la_tautol…rules/la_tautologyAdd remark to congpartial-congpartial-congAdd conditional fallback to minted 2Merge branch 'master' into HEADbvbvold specAdd examples to cutting planes rulesAdd example to clarify `pbblast_pbbconst`Add short-circuit exampleFix minor typos and remove trailing zerosAdd Cutting Planes rules to Rule ListAdd PBBlasting rules to Rule ListAdded short-circuit comment to `pbblast_bveq`Make `cong` more flexible.Rule: distinct_elimMerge branch 'fixes_mallku' into 'master'Fixing back the AletheVerb indentationAdd example to `pbblast_bveq` (partial)Add pseudo boolean bitblasting rulesAdd cutting planes rulesFormula formatting and planning insert locations of new rulesAdd pseudo-boolean reasoning and bitblasting sectionRemove settings and debugminted-2023-upd…minted-2023-update