Index of values

Logical "and"

Logical "or"

Monadic bind

Logical "not"

Literal without its sign

Add term with coefficient.

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 a binary inference rule

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

Add given number to constant

Add a precedence constraint with its priority.

Add a precedence constraint rule

Add tautology detection rule

Add a literal rewrite rule

Add a multi-clause simplification rule

Add passive clauses

Add redundancy criterion w.r.t.

Add a term rewrite rule

Add forward rewriting rule

Merge the given signature with the context's one

Add simplification clauses

Add basic simplification rule

Specify explicitely the status of some symbols

add a function to call before each saturation step

add_stmt st set adds rewrite rules from st to set, if any

Add a unary inference rule

Add clauses to the queue

Returns the age of the clause (or 0 for the empty clause)

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

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

Apply a substitution

Apply a substitution.

Apply a substitution to the monome's terms

apply the substitution to the clause

Apply a substitution with renaming (careful with collisions!)

Apply a substitution but doesn't rename free variables.

Apply a substitution but doesn't rename free variables.

Same as ArithLit.apply_subst but takes care simplifying the literal.

Simple interface on top of Literals.variant with distinc scopes

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

Unsafe version of Ind_cst.as_cst

Get a graph of the proof

downcasts iff t is a sub-constant of cst

Return the subterm at the given position, or

Subterm at given position, or

available names for selection functions

Additional axioms

List of (persistent) axioms that are needed for simplifications to be complete for the given symbol.

backward version of demodulation: add to the set active clauses that can potentially be rewritten by the given clause

Perform backward simplification with the given clause.

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

Strong orientation toward 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)

All sub-constants that are subterms of a specific case

Positive integer: maximum width of an inequality case switch.

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

Current set of clauses

Current set of clauses

coefficients

coeffs_n l gcd, if length l = n, returns a function that takes a list of n-1 terms k1, ..., k(n-1) and returns a list of monomes m1, ..., mn that depend on k1, ..., k(n-1) such that the sum l1 * m1 + l2 * m2 + ... + ln * mn = 0.

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.

Compare monomes as if they were multisets of terms, the coefficient in front of a term being its multiplicity.

partial comparison of literals under the given term ordering

lexicographic comparison of literals

Compare two terms

Compare proofs by their result

Try to compare two monomes.

condensation

Empty monomial, from constant (decides type)

constant

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.

Cases of the cover set

All sub-constants of a given inductive constant

Build a new clause from the given literals.

Build a new clause from the given literals.

Get the cover set of this constant:

cst_of_id id ty returns a new or existing constant for this id.

cst_of_term t returns a new or existing constant for this term, if any.

The current phase is stored in the state using this key

Get the current phase

Index + literal position

cut the subterm position off.

debug functions: much more detailed printing

declarations_of_cst c returns a list of type declarations that should be made if c is new (declare the subcases of its coverset)

Declare the type of a symbol (updates signature)

Adds the constant to the set of inductive constants, make a coverset...

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 extension.

Use Literal.heuristic_weight

Obtain the default queue

Default selection function

rewrite clause using orientable unit equations

depth of literal

Find the solution vector for this diophantine equation, or fails.

generalize diophantine equation solving to a list of at least two coefficients.

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)

divisible e n returns true if all coefficients of e are divisible by n and n is an int >= 2

do binary inferences that involve the given clause

do generating inferences

do unary inferences for the given clause

dominates c sub is true if sub is a sub-constant of c, or if some sub-constant of c dominates sub transitively

dominates ~strict m1 m2 is true if m1 is always greater than m2, in any model or variable valuation.

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.

Eliminate unshielded variables using an adaptation of Cooper's algorithm

Set a maximal depth for terms.

Equations

equality subsumption

Returns substitutions that make the monome always equal to zero.

equality of literals

commutative equality of lits

Is there any AC symbol?

Exit

Use heuristics for selecting "small" clauses

Prover extension

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.

Factorize e into Some (e',s) if e = e' x s, None otherwise (ie if s=1).

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_cst_in_lits term searches subterms of term for constants that are of an inductive type and that are not constructors.

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

Focus on a specific term in an arithmetic literal.

Attempt to focus on the given atomic term, if it occurs directly under the arith literal

Focus on the given term, if it is one of the members of the given monome.

Same as Monome.Focus.focus_term, but

The focused monome

Fold over terms

basic fold

Fold over eligible arithmetic literals

Fold on terms under arithmetic literals, with the focus on the current term

fold f over all literals sides, with their positions.

Fold over literals who satisfy eligible.

Fold on terms of the given monome, focusing on them one by one, along with the position of the focused term

Fold over terms that are maximal in the given ordering.

Fold on focused terms in the literal, one by one, with the position of the focused term

See Literal.fold_terms, which is the same but for the eligible argument

Iterate on terms, maybe subterms, of the literal.

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

Make a fresh ID.

Perform all generating inferences

Generic unification/matching/variant, given such an operation on monomes

Active clauses

Extract an arithmetic literal

Set of known empty clauses

get_env (module Env) returns the meta-prover saved in Env, assuming the extension has been loaded in Env.

get the term l at given position in clause, and r such that l ?= r is the Literal.t at the given position.

View of a Prop or Equation literal, oriented by the position.

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)

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?

For real or rational, always true.

does the clause have some selected literals?

Has a non-empty trail?

hashing of literal

heuristic difficulty to eliminate lit

Index in the literal array

index for backward demodulation/simplifications

index for subsumption

index for forward simplifications

index for superposition from the set

index for superposition into the set

superposition where given clause is active

superposition where given clause is passive

Inject cst = case

Make a new literal from this list of clauses 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).

Recognized whether the clause is a Range-Restricted Horn clause

All literals are false, or there are no literals

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

= or !=

< or <=

Proof: the statement was asserted in some file

Check whether completeness was preserved so far

Returns true if the monome is only a constant

Check whether the given constant is an inductive constant

Check whether the idx-th literal is eligible for paramodulation

Empty trail?

Is the clause an empty clause?

check whether the queue is empty

is the literal of the form a = b?

is the literal a proper (in)equation or prop?

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

Are there no variables in the monome?

all the literals are ground?

Recognizes Horn clauses (at most one positive literal)

< or <=

Is the focused term maximal in the literal?

Is the focused term maximal in the monome?

Is the i-th literal maximal in the ordering?

Is the term at the given position, maximal in the literal w.r.t this ordering? In other words, if the term is replaced by a smaller term, can the whole literal becomes smaller?

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

is the literal negative?

is the literal of the form a != b?

Is the clause a positive oriented clause?

Is the clause a passive clause?

is the literal positive?

Recognize whether the clause is a positive unit equality.

Is the integer prime?

is the literal a boolean proposition?

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 focused term maximal in the literal, ie is it greater than all the othe terms?

Is the term a constant that was created within a cover set?

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

Tautology? (simple syntactic criterion only)

Is the literal AC-trivial?

is the clause a unit clause?

return true if the monome is the constant 0

key to access the Env.flex_state.

Last computed result.

Discovered lemmas

Number of literals

Shortcut for Monome.Int.Solve.lower_zero when strict = false

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

Extract the raw equality literals from this path

To be called when completeness is not preserved

Solve for the monome to be always lower than zero (strict determines whether the inequality is strict or not).

Shortcut for Monome.Int.Solve.lower_zero when strict = true

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

functor

functor

Apply a function to the monomes and focused monomes

checks whether subst(lit_a) is equal to lit_b.

checks whether subst(lit_a) matches lit_b.

Maximal literals of the clause

Maximal terms of the literal

Maximal terms of the literal

Bitvector of positions of maximal literals

List of maximal literals

List of maximal literals, with their index, among the array

Is the term in the monome?

Merge several trails (e.g.

Merge several trails (e.g.

build literals.

Make a precedence

Representative of the number in Z/nZ

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

narrow_term rules lit finds the set of rules (l --> clauses) in rules and substitutions sigma such that sigma(l) = sigma(tit)

narrow_term rules t finds the set of rules (l --> r) in rules and substitutions sigma such that sigma(l) = sigma(t)

Negate the boolean literal

Only negative literals

negate literal

Find some solutions that negate the equation.

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)

Normalize the monome, which means that if some terms are integer constants, they are moved to the constant part (e.g after apply X->3 in 2.X+1, one gets 2.3 +1.

normalize literals of the clause w.r.t.

normalize rules t computes the normal form of t w.r.t the set of rewrite rules

Allows to multiply or divide by any positive number since we consider that the monome is equal to (or compared with) zero.

Conversion from a formula.

Convert a list of atoms into literals

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

try to get a monome from a term.

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 with new inductive constants

signal triggered when a clause is removed from the set

Triggered before starting saturation

The opposite monome (in Left and Right), if any.

Unsafe version of ArithLit.Focus.opposite_monome.

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

Update prover with the content of this file, returns the new results or an error

Parse several files

Does the path contain this inductive constant?

path_dominates a b is true if b is a suffix of a.

Obtain the payload

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

Used for the literal ordering

Obtain the difference between last call to pop_new_results p and results p, and pop this difference.

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 ProofPrint.pp_dot_seq but into a file

Non recursive printing on formatter

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

Print in a toplevel TPTP statement

Print in a cnf() statement

Pre-processing rules

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

-1

Interreduction of the given state, without generating inferences.

Decompose the number into a product of power-of-primes.

Sequence of prime numbers smaller than (or equal to) the given number

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.

Product by a constant

Product with constant

Obtain the pair conclusion, step

Extract its proof from the clause

All proofs for all AC axioms

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

meta-prover

Purify clauses by replacing arithmetic expressions occurring under terms by variables, and adding constraints

Current state of the clause queue

quotient e c tries to divide e by c, returning e/c if it is still an integer expression.

give access to the underlying literals.

Meta-level reasoner (inference system)

reduce_same_factor m1 m2 t multiplies m1 and m2 by some constants, so that their coefficient for t is the same.

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 new selection function

Register an extension to the (current) prover.

Remove the term

Remove clauses from the set

Remove active clauses

Remove the constant

Remove passive clauses

Remove simplification clauses

Obtain the global renaming.

replace a m replaces mf.coeff × mf.term with m where mf is the focused monome in a, and return the resulting literal

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

Replace subterm, or

Only literals that are eligible for resolution

Restore to a level below in the stack

Sum of all results obtained so far

Return a value into the monad

Alias to SimplM.return_same

Finish the given phase

List of term rewrite systems

Obtain the term at the given position, at the root of the literal.

all the terms immediatly under the lit

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.

Save current state on the stack

Multiply the two literals by some constant so that their focused literals have the same coefficient

Scale to the same coefficient

For a "divides" literal, bring it to the given power.

Scan a clause for axiom patterns, and save it

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

x!=y, or ground negative lit, or like select_diff_neg_lit

if clause is a restricted range horn clause, then select nothing; otherwise, like select_complex

arbitrary negative literal with maximal weight difference between sides

Select a maximal negative literal, if any, or nothing

get the list of selected literals

selection function from string (may fail)

selection function for clauses

set boolean flag

set boolean flag

How to print literals?

Set the sign of the literal to the given boolean

Choose the way weights are computed

setup () registers some inference rules to E

Register rules in the environment

Register on Env

Current sign of the literal (positive or negative)

Assuming is_constant m, sign m returns the sign of m.

Current signature

Simplify the clause modulo AC

Simplify the clause.

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

One term.

Number of distinct terms.

Split a clause into components

split m splits into a monome with positive coefficients, and one with negative coefficients.

Split the solution into a variable substitution, and a list of constraints on non-variable terms

Start the given phase

Compute stats

Compute statistics

call all functions registered with Env_intf.S.add_step_init

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

Find substitutions such that subst(lit_a) implies lit_b.

More general version of Literal.matching, yields subst such that subst(lit_a) => lit_b.

returns subsuming subst if the first clause subsumes the second one

+1

Sum in Z/nZ

Sum of a list.

set of AC symbols

symbols that occur in the clause

set of AC symbols occurring in the given term

Plugin that encodes the fact that a type is inductive, together with the list of its constructor symbols.

sub-position

Take first element of the queue, or raise Not_found

Focused term

term_pos lit p = snd (cut lit p), the subterm position.

List of terms that occur in the monome with non-nul coefficients

Detected theories

List of theories detected so far

Conversion into a simple literal

Make a 'or' formula from literals

To list of formulas

Easy iteration on an abstract view of literals

Conversion back to an unfocused monome

Multiset of terms with multiplicity

Debug printing to a string

convert back to a term

Get the clause's trail

Merge the trails of several clauses

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

type of the monome (int or rat)

Additive inverse in Z/nZ

Conversion back to a literal

Unify the two focused terms, and possibly other terms of their respective focused monomes; yield the new literals accounting for the unification along with the unifier

Unify two focused monomes.

Unify parts of two monomes m1 and m2.

Extend the substitution to other terms within the focused monome, if possible.

Unify at least two terms of the monome together

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.

Does the variable occur in the monome?

Variant checking (alpha-equivalence).

gather variables

weight of the lit (sum of weights of terms)

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