• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
      • Gl
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Fgl
        • Fgl-rewrite-rules
          • Binder-functions
          • Fgl-syntactic-checker-binders
          • Binder
          • Fancy-ev
          • Annotate
          • Binder-rules
          • Def-fgl-program
          • Bind-var
          • Add-fgl-brewrites
          • Def-fgl-rewrite
          • Narrow-equiv
          • Trigger-constraints
            • Def-fgl-branch-merge
            • Add-fgl-rewrites
            • Fgl-interp-obj
            • Syntax-bind
            • Fgl-hide
            • Collect-cmr-rewrites-for-formula-name
            • Fgl-time
            • Fgl-prog2
            • Assume
            • Add-fgl-binder-meta
            • Add-fgl-primitive
            • Add-fgl-meta
            • Add-fgl-branch-merges
            • Cmr::rewritelist->lhses
            • Remove-fgl-brewrites
            • Remove-fgl-branch-merges
            • Lhses->branch-function-syms
            • Enable-execution
            • Abort-rewrite
            • Syntax-interp
            • Remove-fgl-rewrites
            • Lhses->leading-function-syms
            • Remove-fgl-primitive
            • Remove-fgl-binder-meta
            • If!
            • Disable-execution
            • Remove-fgl-meta
            • Fgl-time-fn
            • Disable-definition
            • Def-fgl-brewrite
          • Fgl-function-mode
          • Fgl-object
          • Fgl-solving
          • Fgl-handling-if-then-elses
          • Fgl-getting-bits-from-objects
          • Fgl-primitive-and-meta-rules
          • Fgl-counterexamples
          • Fgl-interpreter-overview
          • 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
          • Fgl-fty-support
          • Fgl-internals
        • Removable-runes
        • 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-rewrite-rules

    Trigger-constraints

    FGL function that can trigger the addition of Boolean constraints on some form

    Signature
    (trigger-constraints term) → *

    FGL can collect Boolean constraints among terms. It can trigger constraint generation rules (see def-fgl-boolean-constraint) when a term is added to the Boolean variable database, e.g. by being used in an IF test. This stub function allows such rules to be triggered without adding anything to the Boolean variable database. The subterm is rewritten under an IFF context, and the resulting object can trigger constraint generation rules as if it were added to the Boolean variable database.

    Definitions and Theorems

    Function: trigger-constraints

    (defun trigger-constraints (term)
      (declare (xargs :guard t))
      (let ((__function__ 'trigger-constraints))
        (declare (ignorable __function__))
        nil))