Index of values

Logical "and"

Logical "or"

Monadic bind

Logical "not"

Literal without its sign

Declare that the given symbol is AC, and update the Env subsequently by adding clauses, etc.

Add clauses to the set

Add a clause to the Queue

Add active clauses

Add simplification w.r.t active set

Add rule that finds redundant clauses within active set

Add simplification of the active set

Add basic simplification rule

Add a binary inference rule

add_clause ~tag ~proof c adds the constraint c to the SAT solver, annotated with proof.

add_imply l res means that the conjunction of lemmas in l implies that the lemma res is proven

Add tautology detection rule

Add tautology detection rule

Add the given cut to the list of lemmas.

Add a literal rewrite rule

Add a multi-clause simplification rule

Add passive clauses

Add a mean of proving lemmas

Add redundancy criterion w.r.t.

Add a term rewrite rule

Add forward rewriting rule

Add clauses to the queue

Merge the given signature with the context's one

Add simplification clauses

add a function to call before each saturation step

Add a unary inference rule

Add unary simplification rule (not dependent on proof state)

available names for selection functions

Set of (signed) proved literals

Use all simplification rules to convert a clause into a set of maximally simplified clause (or [] if they are all trivial).

Half FIFO, half default

All literals

apply c t fills the hole of c with the given term t.

Same as ClauseContext.apply, but now variables from the context and variables from the term live in the same scope

apply_sign s lit is lit if s, neg lit otherwise

Are these two cut formulas alpha-equivalent?

If payload t = Case p, then return Some p, else return None

Get a graph of the proof

Return the subterm at the given position, or

Perform backward simplification with the given clause.

basic simplifications (remove duplicate literals, trivial literals, destructive equality resolution...)

Basic (and fast) simplifications

FIFO

bind state f calls f to go one step further from state

Get an extension by its name, if any

Eliminate negative divisibility literals within a power-of-prime quotient of Z: not (d^i | m) ----->

Chain together two divisibility literals, assuming they share the same prime

Eliminate divisibility literals with a non-power-of-prime quotient of Z (for instance 6 | a ---> { 2 | a, 3 | a })

Infer divisibility constraints from integer equations, for instace C or 2a=b ----> C or 2 | b if a is maximal

cancellative equality factoring

cancellative inequality chaining.

Factoring between two inequation literals

Simplification: a < b ----> a+1 ≤ b

cancellative superposition where given clause is active

cancellative superposition where given clause is passive

cancellation (unifies some terms on both sides of a comparison operator)

Positive integer: maximum width of an inequality case switch.

Cases of the cover set

Is the current problem satisfiable?

Forbid empty clauses with trails, i.e.

Checks that the SAT context is still valid

check whether we still have some time w.r.t timeout

classify id returns the role id plays in inductive reasoning

Lookup which clause the position is about, return it and the rest of the position.

Current set of clauses

Current set of clauses

Combine a list of pairs w, coeff where w is a weight function, and coeff a strictly positive number.

Logical "and" of the given eligibility criteria.

true iff the clause is (indirectly) deduced from a goal or lemma

Compare two terms

Compare proofs by their result

condensation

contexual Literal.t cutting of the given clause by the active set

Convert raw input statements into clauses, triggering Env_intf.S.on_input_statement

Intercepts input lemmas and converts them into clauses.

Build a new clause from the given literals.

Build a new clause from the given literals.

The current phase is stored in the state using this key

Get the current phase

debug functions: much more detailed printing

declarations set returns a list of type declarations that should be made if set is new (declare the top cst and its subcases)

Declare the type of a symbol (updates signature)

Declare that the domain of the type ty_id is restricted to given list of cases, in the form forall var. Or_{c in cases} var = c.

Default selection function

Default extension.

Use Literal.heuristic_weight

Obtain the default queue

distance_to_conjecture p returns None if p has no ancestor that is a conjecture (including p itself).

See Proof.distance_to_goal, applied to the clause's proof

Positive integer: maximum prime number suitable for div_case_switch (ie maximum n for enumeration of cases in n^k | x)

do binary inferences that involve the given clause

do generating inferences

do unary inferences for the given clause

dominates c1 c2 if depth c1 < depth c2.

Value that should not be used

Bitvector that indicates which of the literals of subst(clause) are eligible for paramodulation.

Bitvector that indicates which of the literals of subst(clause) are eligible for resolution.

More efficient version of Clause_intf.S.eligible_res with Subst.empty

Eliminate unshielded variables using an adaptation of Cooper's algorithm

Set a maximal depth for terms.

Equations

equality subsumption

Is there any AC symbol?

Exit

Use heuristics for selecting "small" clauses

Extension that enables Avatar splitting and create a new SAT-solver.

All currently available extensions

extract lits t returns None if t doesn't occur in lits.

Unsafe version of ClauseContext.extract.

Fail with the given error message

Favor clauses with only negative ground lits

The closest a clause is from the initial goal, the lowest its weight.

Favor clauses that have at least one non-(ground negative) lit

Only keep a subset of boolean literals

filter_trails f calls f on every trail associated with the empty clause.

find_ind_skolem term searches subterms of term for constants that are of an inductive type and that are skolems or (already) inductive constants.

Recover the proof for the AC-property of this symbol.

Find the type of the given symbol

Unsafe version of Ctx_intf.S.find_signature.

clause has been backward simplified

clause is a lemma

clause cannot be redundant

clause has been shown to be redundant

add k -> v to the flex state

flex_get k is the same as Flex_state.get_exn k (flex_state ()).

State inherited from configuration

Simplify the clause w.r.t to the active set and experts

Make a fresh ID.

selection function from string (may fail)

Perform all generating inferences

Active clauses

Set of known empty clauses

get value of boolean flag

get value of boolean flag

get_key k returns the value associated with k in the state

Passive clauses

Return a proof of false, assuming Sat_solver_intf.S.check returned Unsat.

get_proof_of_lit lit returns the proof of lit, assuming it has been proved true at level 0 (see Sat_solver_intf.S.valuation_level)

Obtain the proof, if any

Some empty clause, if present, otherwise None

run the given clause until a timeout occurs or a result is found.

Perform one step of the given clause algorithm.

custom weight function that favors clauses that are "close" to initial conjectures.

Favor positive unit clauses and ground clauses

Decide on "quoted" "symbols" (which are all distinct)

Is there an empty clause?

does the clause have some selected literals?

Has a non-empty trail?

Unsafe version of as_cst

Check whether the given constant is an inductive constant

id_is_potential_cst id ty returns true if id:ty is a skolem constant of an inductive type, or if it is already an inductive constant.

index for subsumption

index for superposition from the set

index for superposition into the set

depth of the skolem (0 if not an inductive constant)

subset of Cut_form.vars that have an inductive type

superposition where given clause is active

superposition where given clause is passive

Inject cst = case

Make a new literal from this formula that we are going to cut on.

Inject a clause into a boolean literal.

Instantiate variables whose type is a known enumerated type, with all cases of this type.

Introduce a cut on the given clause(s).

Trail.is_active t ~v is true iff all boolean literals in t are satisfied in the boolean valuation v.

Is the clause in the active set

True if the clause's trail is active in this valuation

Proof: the statement was asserted in some file

Check whether completeness was preserved so far

Check whether the idx-th literal is eligible for paramodulation

Empty trail?

Is the clause an empty clause?

check whether the queue is empty

The statement comes from the negation of a goal in some file

Looking at the clause's proof, return true iff the clause is an initial (negated) goal from the problem

returns true if the bool literal represents a lemma

Is the i-th literal maximal in subst(clause)? Equivalent to Bitvector.get (maxlits ~ord c subst) i

Is the clause a positive oriented clause?

Is the clause a passive clause?

Is the given clause redundant w.r.t the active set?

check whether a literal is selected

semantic tautology deletion, using a congruence closure algorithm to see if negative literals imply some positive Literal.t

Is the constant a sub-constant (i.e.

is the clause a tautology w.r.t linear expressions?

Check whether the clause is a (syntactic) tautology, ie whether it contains true or "A" and "not A"

returns true iff the trail contains both i and -i.

Check whether the clause is AC-trivial

Check whether the clause is trivial

Is the literal AC-trivial?

Check whether the trail is trivial

is the clause a unit clause?

key to access the Env.flex_state.

Last computed result.

Number of literals

Number of elements

Lookup which literal the position is about, return it and the rest of the position.

To be called when completeness is not preserved

Build a cover set for the given type.

Make a new constant of the given type

Make a context from a var and literals containing this var.

Make a fresh literal with the given payload

Bring your own implementation of queue.

Map the current value

Maximal literals of the clause

Select a maximal negative literal, if any, or nothing

List of maximal literals

Merge several trails (e.g.

Merge several trails (e.g.

Constructors and utils In all the following constructors, theories defaults to the empty list.

Can we simplify the clause into a List of simplified clauses?

must_be_kept lit means that lit should survive in boolean splitting, that is, that if C <- lit, Gamma then any clause derived from C recursively will have lit in its trail.

Name of the implementation/role of the queue

Names of loaded extensions

Negate the boolean literal

Only negative literals

new flag that can be used on clauses

Get-and-remove the next passive clause to process

Extract next passive clause

norm l = abs l, not (sign l)

Use rewriting to normalize the formula

Directly from list of formulas

Construction from formulas as axiom (initial clause)

Select the queue corresponding to the given profile

Extract a clause from a statement, if any

signal triggered when a clause is added to the set

Signal triggered when an empty clause is found

Triggered every time a cut is introduced for an input lemma (i.e.

Triggered on every input statement

Triggered every time a cut is introduced, by any means.

Triggered with new inductive constants

signal triggered when a clause is removed from the set

Triggered before starting saturation

current ordering on terms

Only literals that are eligible for paramodulation

parse_args returns parameters

Parses the file list and parameters, also puts the parameters in the state

Obtain the payload

Obtain the payload of this boolean literal, that is, what the literal represents

Returns the penalty of the clause

Only positive literals

pretty print the content of the state

Prints the proof according to the given input switch

Pretty print the proof as a DOT graph

print to dot into a file

Print a set of proofs as a DOT graph, sharing common subproofs

same as Proof.S.pp_dot_seq but into a file

Non recursive printing on formatter

Print classification of signature

Printer for boolean trails, that uses Clause_intf.S.Ctx to display boxes

Print in a toplevel TPTP statement

Print in a cnf() statement

Partial order on ID.t, with: regular > constant > sub_constant > cstor

Interreduction of the given state, without generating inferences.

Printing of results

print the current list of lemmas, and their status

process_file f parses f, does the preprocessing phases, including type inference, choice of precedence, ordering, etc.

Process each file in the list successively, printing the results.

Obtain the pair conclusion, step

Extract its proof from the clause

If the literal has been propagated at decision level 0, return its value (which does not depend on the model).

Current state of the clause queue

give access to the underlying literals.

Register rules in the environment

Register the superposition module to its Environment's mixtbl.

Register the inference rules for inductive reasoning

Register inference rules to the environment

Register an extension to the (current) prover.

Remove clauses from the set

Remove active clauses

Remove passive clauses

Remove simplification clauses

Obtain the global renaming.

In-place modification of the array, in which the subterm at given position is replaced by the by term.

In-place modification of the array, in which the subterm at given position is replaced by the by term.

Only literals that are eligible for resolution

Return a value into the monad

Alias to SimplM.return_same

return_opt ~old t returns return_new u if t=Some u, else returns same old.

Finish the given phase

Rule name for Esa/Simplification/Inference steps

run m is run_with empty_state m

run_sequentiel l runs each action of the list in succession, restarting every time with the initial state (once an action has finished, its state is discarded).

run_with state m executes the actions in m starting with state, returning some value (or error) and the final state.

true iff the two cases are on the same constant

Do these two inductive constants have the same type?

Check whether the statement contains an "AC" attribute, do the proper declaration in this case

get the list of selected literals

selection function for clauses

Toggle compact proofs.

set boolean flag

set boolean flag

How to print literals?

Set the sign of the literal to the given boolean

Register rules in the environment

Register rules in the environment

Register rules in the environment

Register on Env

Current sign of the literal (positive or negative)

Current signature

Simplify the clause modulo AC

Can be called when a simplification relation becomes stronger, with the strengthened relation.

Simplify the term

Split a clause into components

Start the given phase

Compute stats

Compute statistics

call all functions registered with Env_intf.S.add_step_init

All sub-constants that are subterms of a specific case

All sub-constants of a given inductive constant

Substitution of one variable

List of active clauses subsumed by the given clause

check whether the clause is subsumed by any clause in the set

list of clauses in the active set that are subsumed by the clause

subsumes c1 c2 iff c1 subsumes c2

subsumes a b is true iff a is a subset of b

returns subsuming subst if the first clause subsumes the second one

set of AC symbols

symbols that occur in the clause

set of AC symbols occurring in the given term

Take first element of the queue, or raise Not_found

Easy iteration on an abstract view of literals

Convert to low level t

Convert to input formula

Debug printing to a string

top constant of the coverset

Get the clause's trail

Merge the trails of several clauses

trail_subsumes c1 c2 = Trail.subsumes (get_trail c1) (get_trail c2)

Trivial context, that contains 0 holes.

Simplify the clause.

update ~f changes the state using f

update_flex_state f changes flex_state () using f

update_proof c f creates a new clause that is similar to c in all aspects, but with the proof f (proof_step c)

Change the trail.

Assuming the last call to Sat_solver_intf.S.check returned Sat, get the boolean valuation for this (positive) literal in the current model.

Gives the value of a literal in the model, as well as its decision level.

Start phase, call f () to get the result, return its result using Phases.return_phase