-
bmc.h
- External header file
-
bmcInt.h
- Internal header file
-
bmcBmcInc.c
- High level functionalities layer for BMC (incremental) algorithms
-
bmcBmcNonInc.c
- High level functionalities layer for non incremental sat
solving
-
bmcCheck.c
- Some useful functions to check propositional formulae.
Temporary located into the bmc package
-
bmcCmd.c
- Bmc.Cmd module
-
bmcConv.c
- Convertion function of BE to corresponding BDD boolean
expression, and viceversa
-
bmcDump.c
- Dumping functionalities, like dimacs and others
-
bmcGen.c
- Bmc.Gen module
-
bmcInt.c
- Private interfaces implementation of package bmc
-
bmcModel.c
- Bmc.Model module
-
bmcOpt.c
- bmc Opt module
-
bmcPkg.c
- Bmc.Pkg module
-
bmcSimulate.c
- Incremental SAT Based simulation
-
bmcTableau.c
- Bmc.Tableau module
-
bmcTableauLTLformula.c
- Bmc.Tableau module
-
bmcTableauPLTLformula.c
- Bmc.TableauPLTL module
-
bmcTest.c
- Test routines for bmc package
-
bmcTrace.c
- This module contains functions to build traces from BE models
-
bmcUtils.c
- Utilities for the bmc package
-
bmcWff.c
- Well Formed Formula manipulation routines
bmc.h
External header file
By: Roberto Cavada
bmcInt.h
Internal header file
By: Roberto Cavada
bmcBmcInc.c
High level functionalities layer for BMC (incremental) algorithms
By: Andrei Tchaltsev
User-commands directly use function defined in this module.
-
Bmc_GenSolveLtlInc()
- Solves LTL problem the same way as the original
Bmc_GenSolveLtl but just adds BE representing the path incrementaly.
-
Bmc_GenSolveInvarZigzag()
- Solve an INVARSPEC problems with algorithm
ZigZag
-
Bmc_GenSolveInvarDual()
- Solve an INVARSPEC problems wiht algorithm Dual
-
Bmc_GenSolveInvarFalsification()
- Solve an INVARSPEC problems wiht algorithm Fasification
-
bmc_add_be_into_solver()
- Converts Be into CNF, and adds it into a group of a solver.
-
bmc_add_be_into_solver_positively()
- Converts Be into CNF, and adds it into a group of a solver,
sets polarity to 1, and then destroys the CNF.
-
bmc_build_uniqueness()
- Builds the uniqueness contraint for dual and zigzag
algorithms
bmcBmcNonInc.c
High level functionalities layer for non incremental sat
solving
By: Roberto Cavada
bmcCheck.c
Some useful functions to check propositional formulae.
Temporary located into the bmc package
By: Roberto Cavada
-
Bmc_CheckFairnessListForPropositionalFormulae()
- Helper function to simplify calling to
'bmc_check_wff_list' for searching of propositional wff only.
Returns a new list of wffs which contains legal wffs only
-
Bmc_WffListMatchProperty()
- For each element belonging to a given list of wffs,
calls the given matching function. If function matches, calls given
answering function
-
Bmc_IsPropositionalFormula()
- Given a wff returns 1 if wff is a propositional formula,
zero (0) otherwise.
-
bmc_is_propositional_formula_aux()
- Useful wrapper for
Bmc_CheckFairnessListForPropositionalFormulae
-
bmc_check_if_wff_is_valid()
- private service for
Bmc_CheckFairnessListForPropositionalFormulae
-
bmc_add_valid_wff_to_list()
- private service for
Bmc_CheckFairnessListForPropositionalFormulae
bmcCmd.c
Bmc.Cmd module
By: Roberto Cavada
This module contains all the bmc commands implementation.
Options parsing and checking is performed here, than the high-level Bmc
layer is called
See AlsobmcPkg.c,
bmcBmc.c
-
Bmc_CommandBmcSetup()
- Initializes the bmc sub-system, and builds the model in
a Boolean Expression format
-
UsageBmcSetup()
- Usage string for Bmc_CommandBmcSetup
-
Bmc_CommandBmcSimulate()
- Bmc_CommandBmcSimulate generates a trace of the problem
represented from the simple path from 0 (zero) to k
-
UsageBmcSimulate()
- Usage string for UsageBmcSimulate
-
Bmc_CommandBmcIncSimulate()
- Bmc_CommandBmcIncSimulate does incremental
simulation of the model starting from an initial state.
-
UsageBmcIncSimulate()
- Usage string for UsageBmcIncSimulate
-
Bmc_CommandBmcPickState()
- Picks a state from the set of initial states
-
UsageBmcPickState()
- Usage string for UsageBmcPickState
-
Bmc_CommandBmcSimulateCheckFeasibleConstraints()
- Checks feasibility of a list of constraints for the
simulation
-
UsageBmcSimulateCheckFeasibleConstraints()
- Usage string for
UsageBmcSimulateCheckFeasibleConstraints
-
Bmc_CommandGenLtlSpecBmc()
- Generates length_max+1 problems iterating the problem
bound from zero to length_max, and dumps each problem to a dimacs file
-
UsageBmcGenLtlSpec()
- Usage string for command gen_ltlspec_bmc
-
Bmc_CommandGenLtlSpecBmcOnePb()
- Generates only one problem with fixed bound and
loopback, and dumps the problem to a dimacs file. The single problem
is dumped for the given LTL specification, or for all LTL
specifications if no formula is given
-
UsageBmcGenLtlSpecOnePb()
- Usage string for command gen_ltlspec_bmc_onepb
-
Bmc_CommandCheckLtlSpecBmc()
- Checks the given LTL specification, or all LTL
specifications in the properties database if no formula is given
-
UsageBmcCheckLtlSpec()
- Usage string for command check_ltlspec_bmc
-
Bmc_CommandCheckLtlSpecBmcOnePb()
- Checks the given LTL specification, or all LTL
specifications if no formula is given. Checking parameters are the problem
bound and the loopback values
-
UsageBmcCheckLtlSpecOnePb()
- Usage string for command check_ltlspec_bmc_onepb
-
Bmc_CommandCheckLtlSpecBmcInc()
- Checks the given LTL specification, or all LTL
specifications in the properties database if no formula is given,
using incremental algorithms
-
UsageBmcCheckLtlSpecInc()
- Usage string for command check_ltlspec_bmc_inc
-
Bmc_CommandGenInvarBmc()
- Generates and dumps the problem for the given
invariant or for all invariants if no formula is given. SAT solver is not
invoked.
-
UsageBmcGenInvar()
- Usage string for command gen_invar_bmc
-
Bmc_CommandCheckInvarBmc()
- Generates and solve the given invariant, or all
invariants if no formula is given
-
UsageBmcCheckInvar()
- Usage string for command check_invar_bmc
-
Bmc_CommandCheckInvarBmcInc()
- Solve the given invariant, or all
invariants if no formula is given, using incremental algorithms.
-
UsageBmcCheckInvarInc()
- Usage string for command check_invar_bmc_inc
-
Bmc_check_psl_property()
- Top-level function for bmc of PSL properties
-
Bmc_cmd_options_handling()
- Bmc commands options handling for commands (optionally)
acceping options -k -l -o -a -n -p -P
-
bmc_build_master_be_fsm()
-
-
Bmc_check_if_model_was_built()
- A service for commands, to check if bmc
has been built
bmcConv.c
Convertion function of BE to corresponding BDD boolean
expression, and viceversa
By: Alessandro Cimatti and Lorenzo Delana
This implementation is still depedent on the rbc package
-
Bmc_Conv_Be2Bexp()
- Given a be, constructs the corresponding boolean
expression
-
Bmc_Conv_Bexp2Be()
- Converts given boolean expression into
correspondent reduced boolean circuit
-
Bmc_Conv_BexpList2BeList()
- Converts given boolean expressions list
into correspondent reduced boolean circuits list
-
Bmc_Conv_cleanup_cached_entries_about()
- Removes from the cache those entries that depend on
the given symbol
-
Bmc_Conv_get_BeModel2SymbModel()
- This function converts a BE model (i.e. a list of BE
literals) to symbolic expressions.
-
Bmc_Conv_init_cache()
- Initializes module Conv
-
Bmc_Conv_quit_cache()
- De-initializes module Conv
-
Be2bexpDfsData_push()
- Sets a node into the stack
-
Be2bexpDfsData_head()
- Be2bexpDfsData_head
-
Be2bexpDfsData_pop()
- Be2bexpDfsData_pop
-
Be2bexp_Set()
- Be2bexpSet
-
Be2bexp_First()
- Be2bexpFirst
-
Be2bexp_Back()
- Be2bexp_Back
-
Be2bexp_Last()
- Be2bexp_Last
-
bmc_conv_set_cache()
- Update the bexpr -> be cache
-
bmc_conv_query_cache()
- Queries the bexpr->be cache
-
bmc_conv_bexp2be_recur()
- Private service for Bmc_Conv_Bexp2Be
bmcDump.c
Dumping functionalities, like dimacs and others
By: Roberto Cavada, Marco Roveri
This module supplies services that dump a Bmc problem
into a file, in DIMACS format and others
bmcGen.c
Bmc.Gen module
By: Roberto Cavada
This module contains all the problems generation functions
See AlsobmcBmc.c,
bmcTableau.c,
bmcModel.c
-
Bmc_Gen_InvarProblem()
- Builds and returns the invariant problem of the
given propositional formula
-
Bmc_Gen_LtlProblem()
- Returns the LTL problem at length k with loopback l
(single loop, no loop and all loopbacks are allowed)
-
Bmc_Gen_InvarBaseStep()
- Returns the base step of the invariant construction
-
Bmc_Gen_InvarInductStep()
- Returns the induction step of the invariant construction
bmcInt.c
Private interfaces implementation of package bmc
By: Roberto Cavada
-
Bmc_GetTestTableau()
-
-
Bmc_rewrite_invar()
- Rewrites an invariant specification containing input
variables or next with an observer state variable
-
Bmc_rewrite_cleanup()
- Crean up the memory after the rewritten property check
bmcModel.c
Bmc.Model module
By: Roberto Cavada
This module contains all the model-related operations
See AlsobmcGen.c,
bmcTableau.c,
bmcConv.c,
bmcVarMgr.c
-
Bmc_Model_GetInit0()
- Retrieves the init states from the given fsm, and
compiles them into a BE at time 0
-
Bmc_Model_GetInitI()
- Retrieves the init states from the given fsm, and
compiles them into a BE at time i
-
Bmc_Model_GetInvarAtTime()
- Retrieves the invars from the given fsm, and
compiles them into a BE at the given time
-
Bmc_Model_GetTransAtTime()
- Retrieves the trans from the given fsm, and compiles
it into a MSatEnc at the given time
-
Bmc_Model_GetUnrolling()
- Unrolls the transition relation from j to k, taking
into account of invars
-
Bmc_Model_Invar_Dual_forward_unrolling()
- Unrolls the transition relation from j to k, taking
into account of invars
-
Bmc_Model_GetPathNoInit()
- Returns the path for the model from 0 to k,
taking into account the invariants (and no init)
-
Bmc_Model_GetPathWithInit()
- Returns the path for the model from 0 to k,
taking into account initial conditions and invariants
-
Bmc_Model_GetFairness()
- Generates and returns an expression representing
all fairnesses in a conjunctioned form
bmcOpt.c
bmc Opt module
By: Alessandro Mariotti
This module contains all the bmc options handling functions
-
opt_check_bmc_pb_length()
- Check function for the bmc_pb_lenght option
-
opt_check_bmc_pb_loop()
- Check function for the bmc_pb_loop option
-
opt_check_bmc_invar_alg()
- Check function for the bmc_invar_alg option
-
opt_get_bmc_invar_alg()
- Get function for the bmc_invar_alg function
-
opt_check_bmc_inc_invar_alg()
- Check function for the bmc_inc_invar_alg function
-
opt_get_bmc_inc_invar_alg()
- Get function for the bmc_inc_invar_alg function
-
opt_get_integer()
- Get the integer representation of the given string
-
opt_get_string()
- Get function for simple strings
bmcPkg.c
Bmc.Pkg module
By: Roberto Cavada
This module contains all the bmc package handling functions
-
Bmc_Init()
- Initializes the BMC structure
-
Bmc_Quit()
- Frees all resources allocated for the BMC model manager
-
Bmc_AddCmd()
- Adds all bmc-related commands to the interactive shell
bmcSimulate.c
Incremental SAT Based simulation
By: Marco Roveri
Incremental SAT Based simulation
See Alsooptional
-
Bmc_Simulate()
- Performs simulation
-
Bmc_StepWiseSimulation()
- SAT Based Incremental simulation
-
Bmc_simulate_check_feasible_constraints()
- Checks the truth value of a list of constraints on the
current state, transitions and next states,
from given starting state. This can be used
in guided interactive simulation to propose
the set of transitions which are allowed to
occur in the interactive simulation.
-
Bmc_pick_state_from_constr()
- Picks a state from the initial state, creates a trace
from it.
-
bmc_simulate_set_curr_sim_trace()
- Internal function used during the simulation to set the
current simulation trace
-
bmc_simulate_add_be_into_inc_solver_positively()
- Converts Be into CNF, and adds it into a group of a
incremental solver, sets polarity to 1, and then destroys
the CNF.
-
bmc_simulate_add_be_into_non_inc_solver_positively()
- Converts Be into CNF, and adds it into a group of a
non-incremental solver, sets polarity to 1, and
then destroys the CNF.
bmcTableau.c
Bmc.Tableau module
By: Marco Benedetti, Roberto Cavada
This module contains all the tableau-related operations
See AlsobmcModel.c,
bmcConv.c,
bmcVarMgr.c
bmcTableau.c,
bmcTableauLTLformula.c,
bmcTableauPLTLformula.c,
bmcGen.c
-
Bmc_Tableau_GetNoLoop()
- Builds tableau without loop at time zero, taking into
account of fairness
-
Bmc_Tableau_GetSingleLoop()
- Builds tableau for all possible loops in [l, k], in
the particular case in which depth is 1. This function takes into account
of fairness
-
Bmc_Tableau_GetAllLoops()
- Builds tableau for all possible loops in [l, k[,
taking into account of fairness
-
Bmc_Tableau_GetAllLoopsDepth1()
- Builds tableau for all possible loops in [l, k], in
the particular case in which depth is 1. This function takes into account
of fairness
-
Bmc_Tableau_GetLtlTableau()
- Builds a tableau for the LTL at length k with loopback l
(single loop, no loop and all loopbacks are allowed)
-
Bmc_TableauLTL_GetSingleLoopWithFairness()
- Builds the tableau at time zero. Loop is allowed,
fairness are taken into account
-
Bmc_TableauLTL_GetSingleLoop()
- Builds the tableau at time zero. Loop is allowed,
fairness are taken into account
-
Bmc_TableauLTL_GetNoLoop()
- Builds tableau without loop at time zero, taking into
account of fairness
-
Bmc_TableauLTL_GetAllLoops()
- Builds tableau for all possible loops in [l, k[,
taking into account of fairness
-
Bmc_TableauLTL_GetAllLoopsDepth1()
- Builds tableau for all possible loops in [l, k], in
the particular case in which depth is 1. This function takes into account
of fairness
-
Bmc_TableauPLTL_GetNoLoop()
- Returns the tableau for a PLTL formula on a bounded path
of length k, reasoning on fairness conditions as well.
-
Bmc_TableauPLTL_GetSingleLoop()
- Returns the tableau for a PLTL formula on a (k,l)-loop,
conjuncted with both fairness conditions and the loop
condition on time steps k and l.
-
Bmc_TableauPLTL_GetAllLoops()
- Returns the conjunction of the single-loop tableaux for
all possible (k,l)-loops for a fixed k. Each single-loop
tableau takes into account of both fairness constraints
and loop condition.
-
Bmc_TableauPLTL_GetAllLoopsDepth1()
- Builds tableau for all possible (k,l)-loops for a
fixed k, in the particular case depth==1.
This function takes into account of fairness.
-
Bmc_Tableau_GetLoopCondition()
- Builds a tableau that constraints state k to be equal to
state l. This is the condition for a path of length (k+1)
to represent a (k-l)loop (new semantics).
-
Bmc_Tableau_GetAllLoopsDisjunction()
- Builds the disjunction of all the loops conditions
for (k-l)-loops with l in [0, k[
-
isPureFuture()
- Checks wether a formula contains only future operators
-
isPureFuture_aux()
- Memoized private service of isPureFuture
bmcTableauLTLformula.c
Bmc.Tableau module
By: Roberto Cavada
This module contains all the operations related to the
construction of tableaux for LTL formulas
See AlsobmcGen.c,
bmcModel.c,
bmcConv.c,
bmcVarMgr.c
-
BmcInt_Tableau_GetAtTime()
- Given a wff expressed in ltl builds the model-independent
tableau at 'time' of a path formula bounded by [k, l]
-
bmc_tableauGetNextAtTime()
- Resolves the NEXT operator, building the tableau for
its argument
-
bmc_tableauGetEventuallyAtTime()
- Resolves the future operator, and builds a conjunctive
expression of tableaus, by iterating intime up to k in a different manner
depending on the [l, k] interval form
-
bmc_tableauGetGloballyAtTime()
- As bmc_tableauGetEventuallyAtTime, but builds a
conjunctioned expression in order to be able to assure a global constraint
-
bmc_tableauGetUntilAtTime()
- Builds an expression which evaluates the until operator
-
bmc_tableauGetReleasesAtTime()
- Builds an expression which evaluates the release
operator
-
bmc_tableauGetUntilAtTime_aux()
- auxiliary part of bmc_tableauGetUntilAtTime
-
bmc_tableauGetReleasesAtTime_aux()
- auxiliary part of bmc_tableauGetReleasesAtTime
bmcTableauPLTLformula.c
Bmc.TableauPLTL module
By: Marco Benedetti
Implements all the functions needed to build tableaux for
PLTL formulas.
See AlsobmcTableau.c,
bmcGen.c
-
()
-
-
()
-
-
Bmc_TableauPLTL_GetTableau()
- Builds the tableau for a PLTL formula.
-
Bmc_TableauPLTL_GetAllTimeTableau()
- Builds the conjunction of the tableaux for a PLTL formula
computed on every time instant along a (k,l)-loop.
-
getTableauAtTime()
- Builds the tableau for a PLTL formula "pltl_wff" at time
"time".
-
evaluateOn()
- Evaluates (either disjunctively or conjunctively) a PLTL
formula over an interval of time.
-
projectOntoMainDomain()
- Projects a (possibly open) interval [a,b
-
tau()
- Gives an upper bound on the past temporal horizon of a
PLTL formula.
bmcTest.c
Test routines for bmc package
By: Roberto Cavada, Marco Benedetti
-
Bmc_TestReset()
- Call this function to reset the test sub-package (into
the reset command for example)
-
Bmc_TestTableau()
- The first time Bmc_TestTableau is called in the current
session this function creates a smv file with a model and generates a random
ltl spec to test tableau. The following times it is called it appends a new
formula to the file.
-
UsageBmcTestTableau()
- Usage string for Bmc_TestTableau
-
bmc_test_mk_loopback_ltl()
- For each variable p in the set of state variables,
generates the global equivalence of p and X^(loop length), starting from
the loop start
-
bmc_test_gen_tableau()
- Given a WFF in NNF, converts it into a tableau
formula, then back to WFF_(k,l) and returns WFF -> WFF_(k,l)
-
bmc_test_gen_wff()
- Builds a random LTL WFF with specified
max depth and max connectives.
-
bmc_test_bexpr_output()
- Write to specified FILE stream given node_ptr
formula with specified output_type format. There are
follow formats: BMC_BEXP_OUTPUT_SMV, BMC_BEXP_OUTPUT_LB
bmcTrace.c
This module contains functions to build traces from BE models
By: Marco Pensallorto
-
Bmc_create_trace_from_cnf_model()
- Creates a trace out of a cnf model
-
bmc_trace_utils_complete_trace()
- Populates trace with valid defaults assignments
-
bmc_trace_utils_append_input_state()
- Appends a _complete_ (i,S') pair to existing trace
bmcUtils.c
Utilities for the bmc package
By: Roberto Cavada
-
Bmc_Utils_ConvertLoopFromString()
- Given a string representing a loopback possible value,
returns the corresponding integer. The (optional)
parameter result will be assigned to SUCCESS if the
conversion has been successfully performed, otherwise
to GENERIC_ERROR is the conversion failed. If result is
NULL, SUCCESS is the aspected value, and an assertion
is implicitly performed to check the conversion
outcome.
-
Bmc_Utils_ConvertLoopFromInteger()
- Given an integer containing the inner representation of
the loopback value, returns as parameter the
corresponding user-side value as string
-
Bmc_Utils_IsNoLoopback()
- Returns true if l has the internally encoded "no loop"
value
-
Bmc_Utils_IsNoLoopbackString()
- Returns true if the given string represents the no
loopback value
-
Bmc_Utils_IsSingleLoopback()
- Returns true if the given loop value represents a single
(relative or absolute) loopback
-
Bmc_Utils_IsAllLoopbacks()
- Returns true if the given loop value represents the "all
possible loopbacks" semantic
-
Bmc_Utils_IsAllLoopbacksString()
- Returns true if the given string represents the "all
possible loops" value.
-
Bmc_Utils_GetNoLoopback()
- Returns the integer value which represents the "no loop"
semantic
-
Bmc_Utils_GetAllLoopbacks()
- Returns the integer value which represents the "all loops"
semantic
-
Bmc_Utils_GetAllLoopbacksString()
- Returns a constant string which represents the "all loops"
semantic.
-
Bmc_Utils_RelLoop2AbsLoop()
- Converts a relative loop value (wich can also be an
absolute loop value) to an absolute loop value
-
Bmc_Utils_Check_k_l()
- Checks the (k,l) couple. l must be absolute.
-
Bmc_Utils_GetSuccTime()
- Given time<=k and a [l, k] interval, returns next time,
or BMC_NO_LOOP if time is equal to k and there is no
loop
-
Bmc_Utils_ExpandMacrosInFilename()
- Search into a given string any symbol which belongs to a
determined set of symbols, and expand each found
symbol, finally returning the resulting string
-
Bmc_Utils_generate_and_print_cntexample()
- Given a problem, and a solver containing a model for that
problem, generates and prints a counter-example
-
Bmc_Utils_generate_cntexample()
- Given a problem, and a solver containing a model for that
problem, generates a counter-example
-
Bmc_Utils_get_vars_list_for_uniqueness()
- Creates a list of BE variables that are intended to be
used by the routine that makes the state unique in
invariant checking.
-
Bmc_Utils_get_vars_list_for_uniqueness_fsm()
- Creates a list of BE variables that are intended to be
used by the routine that makes the state unique in
invariant checking.
-
Bmc_Utils_apply_inlining()
- Applies inlining taking into account of current user
settings
-
Bmc_Utils_apply_inlining4inc()
- Applies inlining forcing inclusion of the conjunct
set. Useful in the incremental SAT applications to
guarantee soundness
-
Bmc_Utils_simple_costraint_from_string()
- Reads a simple expression and builds the corresponding BE
formula.
-
Bmc_Utils_next_costraint_from_string()
- Reads a next expression and builds the corresponding BE
formula.
-
bmc_utils_costraint_from_string()
- Reads an expression and builds the corresponding BE
formula. If accept_next_expr is true, then a next
expression is parsed, otherwise a simple expression is
parsed.
bmcWff.c
Well Formed Formula manipulation routines
By: Alessandro Cimatti and Lorenzo Delana
-
Bmc_Wff_MkTruth()
- Makes a truth WFF
-
Bmc_Wff_MkFalsity()
- Makes a false WFF
-
Bmc_Wff_MkNot()
- Makes a not WFF
-
Bmc_Wff_MkAnd()
- Makes an and WFF
-
Bmc_Wff_MkOr()
- Makes an or WFF
-
Bmc_Wff_MkImplies()
- Makes an implies WFF
-
Bmc_Wff_MkIff()
- Makes an iff WFF
-
Bmc_Wff_MkNext()
- Makes a next WFF
-
Bmc_Wff_MkXopNext()
- Applies op_next x times
-
Bmc_Wff_MkOpNext()
- Makes an op_next WFF
-
Bmc_Wff_MkOpPrec()
- Makes an op_next WFF
-
Bmc_Wff_MkOpNotPrecNot()
- Makes an op_next WFF
-
Bmc_Wff_MkGlobally()
- Makes a globally WFF
-
Bmc_Wff_MkHistorically()
- Makes a historically WFF
-
Bmc_Wff_MkEventually()
- Makes an eventually WFF
-
Bmc_Wff_MkOnce()
- Makes an once WFF
-
Bmc_Wff_MkUntil()
- Makes an until WFF
-
Bmc_Wff_MkSince()
- Makes an since WFF
-
Bmc_Wff_MkReleases()
- Makes a releases WFF
-
Bmc_Wff_MkTriggered()
- Makes a triggered WFF
-
Bmc_Wff_MkNnf()
- Makes the negative normal form of given WFF
-
Bmc_Wff_GetDepth()
- Returns the modal depth of the given formula
-
bmc_wff_mkBinary()
- Makes a binary WFF
-
bmc_wff_mkUnary()
- Makes a unary WFF
-
bmc_wff_mkConst()
- Makes a constant WFF
Last updated on 2010/11/04 13h:34