qbfsat - solve a 2QBF-SAT problem in the circuit

    qbfsat [options] [selection]

This command solves an "exists-forall" 2QBF-SAT problem defined over the currently
selected module. Existentially-quantified variables are declared by assigning a wire
"$anyconst". Universally-quantified variables may be explicitly declared by assigning
a wire "$allconst", but module inputs will be treated as universally-quantified
variables by default.

        Do not delete temporary files and directories. Useful for debugging.

    -dump-final-smt2 <file>
        Pass the --dump-smt2 option to yosys-smtbmc.

        Add an "$assume" cell for the conjunction of all one-bit module output wires.

        When adding $assume cells for one-bit module output wires, assume they are
        negative polarity signals and should always be low, for example like the
        miters created with the `miter` command.

        Ignore "\minimize" and "\maximize" attributes, do not emit "(maximize)" or
        "(minimize)" in the SMT-LIBv2, and generally make no attempt to optimize anything.

        If a wire is marked with the "\minimize" or "\maximize" attribute, do not
        attempt to optimize that value with the default iterated solving and threshold
        bisection approach. Instead, have yosys-smtbmc emit a "(minimize)" or "(maximize)"
        command in the SMT-LIBv2 output and hope that the solver supports optimizing
        quantified bitvector problems.

    -solver <solver>
        Use a particular solver. Choose one of: "z3", "yices", and "cvc4".
        (default: yices)

    -solver-option <name> <value>
        Set the specified solver option in the SMT-LIBv2 problem file.

    -timeout <value>
        Set the per-iteration timeout in seconds.
        (default: no timeout)

    -O0, -O1, -O2
        Control the use of ABC to simplify the QBF-SAT problem before solving.

        Generate an error if the solver does not return "sat".

        Generate an error if the solver does not return "unsat".

        Print the output from yosys-smtbmc.

        If the problem is satisfiable, replace each "$anyconst" cell with its
        corresponding constant value from the model produced by the solver.

    -specialize-from-file <solution file>
        Do not run the solver, but instead only attempt to replace each "$anyconst"
        cell in the current module with a constant value provided by the specified file.

    -write-solution <solution file>
        If the problem is satisfiable, write the corresponding constant value for each
        "$anyconst" cell from the model produced by the solver to the specified file.