Module `Clause`

Clause, properties and activation literals for IC3

author: Christoph Sticksel

type source = | PropSet Clause is a pseudo clause for property set | BlockFrontier Negation of clause reaches a state outside the property in one step | BlockRec of t Negtion of clause reaches a state outside the negation of the clause to block | IndGen of t Clause is an inductive generalization of the clause | CopyFwdProp of t Clause is a copy of the clause from forward propagation | CopyBlockProp of t Clause is a copy of the clause from blocking in future frames | Copy of t Clause is a copy of the clause for another reason: Origin of clause

and t: Clause

module ClauseTrie : Trie.S with type key = Term.t list: A trie of literals

Clauses

For every clause C = {L1, ..., Ln} two activation literals p0 and p1 are generated per clause, in addition two activation literals n0_i and n1_i per literal Li. The following terms are then lazily asserted on the first access of the actiation:

p0 => C
p1 => C'
n01 => ~L1
n11 => ~L1'
...
n0n => ~Ln
n1n => ~Ln'

where the C' and Li' are the clause and the literals, respectively, at the next instant.

val mk_clause_of_literals : source -> Term.t list -> t

Create a clause from a set of literals

The activation literals are only created in the Kind 2 term database, but nothing is sent to the solver, instead they are only made on the first access of the activation literals in actlit_p0_of_clause, actlit_p1_of_clause, actlits_n0_of_clause and actlits_n1_of_clause.

val copy_clause_block_prop : t -> t: Return a copy of the clause with fresh activation literal

val copy_clause_fwd_prop : t -> t
val copy_clause : t -> t
val id_of_clause : t -> int: Return unique identifier of clause

val length_of_clause : t -> int

Return the number of literals in the clause

Since duplicate literals are eliminated, this is not necessarily equal to the number of literals given when creating the clause.

val term_of_clause : t -> Term.t: Return the conjunction of all literals in the clause

val literals_of_clause : t -> Term.t list

Return the literals in the clause

Since duplicate literals are eliminated and ordered, this is not necessarily equal to the list of literals given when creating the clause.

val source_of_clause : t -> source: Return the source of the clause

Activation Literals

val actlit_p0_of_clause : SMTSolver.t -> t -> Term.t

Return the activation literal for the positive unprimed clause

Declare the activation literal and assert the term p0 => C on the first access of the activation literal in the given solver instance. Fail with Invalid_argument if deactivate_clause has been called for the clause in the given solver instance.

val actlit_p1_of_clause : SMTSolver.t -> t -> Term.t

Return the activation literal for the positive primed clause

Declare the activation literal and assert the term p1 => C' on the first access of the activation literal in the given solver instance. Fail with Invalid_argument if deactivate_clause has been called for the clause in the given solver instance.

val actlits_n0_of_clause : SMTSolver.t -> t -> Term.t list

Return the activation literals for the negated clause literals

Declare the activation literals and assert the terms n0_i => L_i for each literal L_i in the clause on the first access of the activation literal in the given solver instance. Fail with Invalid_argument if deactivate_clause has been called for the clause in the given solver instance.

val actlits_n1_of_clause : SMTSolver.t -> t -> Term.t list

Return the activation literals for the negated, primed literals

Declare the activation literals and assert the terms n1_i => L_i' for each literal L_i in the clause on the first access of the activation literal in the given solver instance. Fail with Invalid_argument if deactivate_clause has been called for the clause in the given solver instance.

val deactivate_clause : SMTSolver.t -> t -> unit

Assert the negation of all activation literals of clause in the solver instance

The clause is marked as unusable in the solver instance, hence all calls to actlit_p0_of_clause, actlit_p1_of_clause, actlits_n0_of_clause, actlits_n1_of_clause fail.

val undo_ind_gen : t -> t option

If the clause is an inductive generalization, return the clause before generalization

Only return one step of inductive generalization, repeat to obtain possible chains of generalizations.

Property sets

type prop_set: Set of properties

val prop_set_of_props : (string * Term.t) list -> prop_set

Create a property set from a list of named properties

The conjunction of properties is viewed as a single literal of a clause, and this clause is asserted with activation literals in the given solver instance.

val clause_of_prop_set : prop_set -> t: Return the unit clause containing the conjunction of the properties as a literals

val term_of_prop_set : prop_set -> Term.t: Return the conjunction of the properties

val props_of_prop_set : prop_set -> (string * Term.t) list: Return the named properties of the property set

val actlit_p0_of_prop_set : SMTSolver.t -> prop_set -> Term.t: Return the activation literal for the positive conjunction of properties

val actlit_p1_of_prop_set : SMTSolver.t -> prop_set -> Term.t: Return the activation literal for the positive primed conjunction of properties

val actlits_n0_of_prop_set : SMTSolver.t -> prop_set -> Term.t list: Return the (singleton list of) activation literals for the negated conjunction of properties

val actlits_n1_of_prop_set : SMTSolver.t -> prop_set -> Term.t list: Return the (singleton list of) activation literals for the negated primed conjunction of properties

Frames

val actlit_of_frame : int -> Term.t: Create or return an activation literal for the given frame

val actlit_symbol_of_frame : int -> UfSymbol.t: Create or return the uninterpreted functoin symbol for the activation literal for the given frame

Activation literals

type actlit_type = | Actlit_p0 positive unprimed | Actlit_n0 negative unprimed | Actlit_p1 positive primed | Actlit_n1 negative primed: Type of activation literal

val create_and_assert_fresh_actlit : SMTSolver.t -> string -> Term.t -> actlit_type -> Term.t

Create a fresh activation literal, declare it in the solver, and assert a term guarded with it

create_and_assert_fresh_actlit s h t a declares a fresh uninterpreted Boolean constant in the solver instance s, and asserts the term t guarded by this activation literal in the same solver instance. The parameter h is a tag used to name the constant, together with a counter that is maintained per tag.

`\|` `PropSet`	Clause is a pseudo clause for property set
`\|` `BlockFrontier`	Negation of clause reaches a state outside the property in one step
`\|` `BlockRec of t`	Negtion of clause reaches a state outside the negation of the clause to block
`\|` `IndGen of t`	Clause is an inductive generalization of the clause
`\|` `CopyFwdProp of t`	Clause is a copy of the clause from forward propagation
`\|` `CopyBlockProp of t`	Clause is a copy of the clause from blocking in future frames
`\|` `Copy of t`	Clause is a copy of the clause for another reason

`\|` `Actlit_p0`	positive unprimed
`\|` `Actlit_n0`	negative unprimed
`\|` `Actlit_p1`	positive primed
`\|` `Actlit_n1`	negative primed