• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
        • Ipasir$a
        • Building-an-ipasir-solver-library
        • Ipasir-formula
        • Ipasir-bump-activity-vars$a
        • Ipasir-set$a
        • Ipasir-bump-activity-vars$c
        • Ipasir-get$a
        • Ipasir-set-limit$c
        • Ipasir-set$c
        • Ipasir-failed$c
        • Ipasir-assume$c
        • Ipasir-add-lit$c
        • Ipasir-val$c
        • With-local-ipasir
          • Ipasir-solve$c
          • Ipasir-reinit$c
          • Ipasir-init$c
          • Ipasir-finalize-clause$c
          • Ipasir-some-history$c
          • Ipasir-solved-assumption$c
          • Ipasir-release$c
          • Ipasir-input$c
          • Ipasir-get$c
          • Ipasir-get-status$c
          • Ipasir-get-curr-stats$c
          • Ipasir-get-assumption$c
          • Ipasir-empty-new-clause$c
          • Ipasir-callback-count$c
          • Ipasir-val
          • Ipasir-solve
          • Ipasir-set-limit
          • Ipasir-reinit
          • Ipasir-failed
          • Ipasir-callback-count
          • Ipasir-release
          • Ipasir-input
          • Ipasir-init
          • Ipasir-finalize-clause
          • Ipasir-assume
          • Ipasir-add-lit
        • Aignet
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Ipasir

    With-local-ipasir

    Create a local ipasir solver object, initialize it, and properly release it when done.

    The syntax of with-local-ipasir is similar to that of with-local-stobj, but the first argument (stobj name) is optional and defaults to ipasir. However, note that state must be available and must be one of the objects returned by the inner mv-let form; this is because ipasir-init returns state.