Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Gl
Witness-cp
Ccg
Install-not-normalized
Rewrite$
Removable-runes
Fgl
Fgl-rewrite-rules
Fgl-function-mode
Fgl-object
Fgl-solving
Fgl-handling-if-then-elses
Fgl-getting-bits-from-objects
Fgl-primitive-and-meta-rules
Fgl-interpreter-overview
Fgl-counterexamples
Fgl-correctness-of-binding-free-variables
Fgl-debugging
Fgl-testbenches
Def-fgl-boolean-constraint
Fgl-stack
Fgl-rewrite-tracing
Def-fgl-param-thm
Def-fgl-thm
Fgl-fast-alist-support
Fgl-array-support
Advanced-equivalence-checking-with-fgl
Solve-lane-by-lane-masked
Solve-lane-by-lane-masked+
Top-level-equal
Replace-equal-with-top-level-equal-rec
Solve-lane-by-lane
Lookup-previous-stack-frame-binding
Ipasir-sat-limit100
Fgl-internals
Efficiency
Rewrite-bounds
Bash
Def-dag-measure
Bdd
Remove-hyps
Contextual-rewriting
Simp
Rewrite$-hyps
Bash-term-to-dnf
Use-trivial-ancestors-check
Minimal-runes
Clause-processor-tools
Fn-is-body
Without-subsumption
Rewrite-equiv-hint
Def-bounds
Rewrite$-context
Try-gl-concls
Hint-utils
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Fgl
Advanced-equivalence-checking-with-fgl
Some tools for equivalence checking with FGL.
Subtopics
Solve-lane-by-lane-masked
Equality check that works around hard SAT/fraiging problems caused by writemasking.
Solve-lane-by-lane-masked+
Equality check that works around hard SAT/fraiging problems caused by writemasking, solving each case separately.
Top-level-equal
An alias for EQUAL. Useful if you want to prove an equality in FGL using a particular strategy.
Replace-equal-with-top-level-equal-rec
Solve-lane-by-lane
Equality check that, in FGL, splits an equivalence of SIMD packed integers into lane-by-lane equivalence checks.
Lookup-previous-stack-frame-binding
Ipasir-sat-limit100
