Index of values

Compute a wedge that over-approximates a given formula

abstract ?exists srk man phi computes the strongest property that is implied by phi which is expressible within a given abstract domain.

Non-deterministically choose between two transitions

add solver formulas asserts that each formula in formulas holds.

add_rule solver hypothesis conclusion adds the rule hypothesis => conclusion to solver.

Add a new zero-polynomial to a rewrite system and saturate

Extend a coordinate system with one additional coordinate term, if that coordinate does not already belong to the system.

Extend a coordinate system to admit a term

Does a coordinate system admit the given term?

affine_hull srk phi symbols computes a basis for the affine hull of phi, projected onto the given set of symbols.

Given an a model m and a formula phi such that m |= phi, attempt to compute a new interpretation m' such that m' |= phi, m(x) = m'(x) for all constant symbols and non-real functions, and for all real functions f, m'(f) is affine.

assign v t is a transition that assigns the term t to the variable v.

assume phi is a transition that doesn't modify any variables, but can only be executed when phi holds

Given a list of *subsets* of dimensions p1, ..., pn, a monomial m can be considered as a list of monomials ("blocks") m1, ..., mn, m0, where each mi contains the dimensions that belong to pi (and not to any lower i), and m0 contains the dimensions not belonging to any pi.

Given a wedge wedge and a term term, compute a lower and upper bounds for term within the region wedge.

boxify srk phi terms computes the strongest formula of the form /\ { lo <= t <= hi : t in terms } that is implied by phi.

Verify that a SAT strategy is in fact a winning strategy.

Compare is a purely syntactic comparison.

Dimension for representing the coefficient of the constant 1.

Virtual coordinate associated with 1

Representation of a rational number as an affine term.

Convert an affine term to a rational number, if possible.

Guarded parallel assignment

Find the coordinate associated with an coordinate term.

Compare by total degree, then lexicographic order

Compare by total degree, then reverse lexicographic order

Number of dimensions in the coordinate system

Map a dimension to symbol.

Enumerate the set of dimensions that appear in a polynomial

Find the set of all coordinates that are associated with *direct* subterms of the term associated with a given coordinate.

Integer division conforming to SMTLIB2: a == (a/b)*b + a%b and 0 <= a%b < |b|

Divide a polynomial by a monomial

Given two matrices A and B, compute a matrix C such that CB = A (if one exists).

Alternating quantifier satisfiability

Ensure that the named symbols pow : Real x Real -> Real and log : Real x Real -> Real belong to a given context.

Ensure that a context has the following named symbols mul (rational multiplication), imul (integer multiplication), mod (rational modulo), imod (integer modulo), inv (rational inverse). If the symbols are not present in the context ensure_symbols registers them.

Enumerate the concrete bindings in an interpretation.

Test whether two transitions are equal up to logical equivalence and renaming skolem constants.

Evaluate an expression in the environment Top.

evaluate_linterm env t evaluates the affine term t in the environment env

exists ex tr removes the variables that do not satisfy the predicate ex from the footprint of a transition.

Project symbols out of a wedge that do not satisfy the given predicate.

Exponentiation by a positive integer

Exponentiation

const_power ivl k computes an interval surrounding the set the set { x^k : x in ivl }.

Convert a Z3 expression into an expression.

Function to be tabulated

Function to be tabulated

Given a polynomial p(x), compute a factorization p(x) = c*q1(x)^d1 * ... qn(x)^dn such that each qi is an irreducible polynomial with integer coefficients.

Compute a representation of the set of equalities that are entailed by a given wedge as a list (term0, vector0),...,(termn,vectorn).

Find an element with features <= the given feature vector, and which satisfies the given predicate.

Find an element elt with features <= the given feature vector, and on which the given partial function f is defined; return f elt.

Convert a Z3 expression into a formula.

Retrieve the symbol associated with a given name.

Retrieve the value of a variable after a transition as a term over input variables (and Skolem constants)

Saturate a polynomial rewrite system with implied equalities

The condition under which a transition may be executed.

Assign a list of variables non-deterministic values.

The polynomial p(x) = x

Convert a polyhedron to a conjunction of atomic formulas (as returned by Interpretation.select_implicant).

Number of integer dimensions in the coordinate system

Given a path (list of transitions tr_1 ... tr_n) and a post-condition formula, determine whether the path implies the post-condition.

Sequence interpolation.

Replace non-linear uninterpreted functions with interpreted ones.

Replace non-linear uninterpreted functions with interpreted ones.

Given two matrices A and B, compute matrices C and D such that CA = DB is a basis for the intersection of the rowspaces of A and B.

Test if a name is already associated with a symbol

Check if a formula is satisfiable by computing an over-approximating wedge and checking whether it is feasible.

Least common multiple

Lexicographic order

Compute a linear approximation of a non-linear formula.

Convert a rational vector representing an affine term.

Count the number of dimensions with non-zero coefficients

Parse a SMTLIB2-formatted string

Model-guided projection of a polyhedron.

Given matrices A and B, find a matrix C whose rows constitute a basis for the vector space { v : exists u. uA = vB }

Alternating quantifier optimization

Test whether a point, representing as a map from symbols to rationals, is inside a polyhedron.

Is a variable written to in a transition?

Memoize a function using built-in polymorphic hash.

Memoize a recursive function using built-in polymorphic hash.

Merge two (sorted) arrays

C99 integer division.

Unary negation

Given an admissible order and a list of zero polynomials, orient the polynomials into a rewrite system.

Subtraction

truncate(t) removes the fractional part of t (rounding it towards 0).

Modulo conforming to SMTLIB2: a == (a/b)*b + a%b and 0 <= a%b < |b|

Sequentially compose two transitions.

Convert to negation normal form (down pass).

Compute an upper and lower bound for a rational number (with small representations) via truncated continued fractions.

Compute an lower bound for a rational number (with a small representation).

Compute an upper bound for a rational number (with a small representation).

nullspace mat dimensions computes a basis for the vector space { x : max*x = 0}, projected on to the set of dimensions dimensions.

Convert formula that contains only conjunction and linear equalities and disequalities into a polyhedron.

Convert a conjunction of atomic formulas (as returned by Interpretation.select_implicant) to a polyhedron.

Convert a rational vector to an affine term.

Convert a rational vector to a linear polynomial, where each dimension corresponds to a variable except the designated const dimension, which is treated at a constant 1.

Skip (unit of mul).

Given a formula phi and a list of objectives o1,...,on, find the least bounding interval for each objective within the feasible region defined by the formula.

Given a predicate on dimensions and a list of terms (all implicitly equal to zero), orient the equations as rewrite rules that eliminate dimensions that don't satisfy the predicate.

Parallel assignment of a list of terms to a list of variables.

Find a polynomial associated with an admissible term over *non-multiplicative* cooridnate.

Convert a vector to a polynomial *without multiplicative coordinates*.

Pretty-print an affine term

Print a formula as a satisfiability query in SMTLIB2 format.

Reduce a multi-variate polynomial using the given rewrite rules until no more rewrite rules apply.

Fourier-Motzkin elimination.

Purify function applications in a ground formula: replace each function application within a formula with a fresh symbol, and return both the resulting formula and a mapping from the fresh symbols to the terms they define.

Quantifier elimination

Quantifier eliminiation via model-based projection

Compute a list rational eigenvalues of a matrix, along with their algebraic multiplicities.

Given a matrix A, find a pair of matrices (M,T) such that MA = TM, T is lower-triangular, and the rowspace of MA is maximal.

Number of real dimensions in the coordinate system

Reduce a multi-variate polynomial using the given rewrite rules until no more rewrite rules apply

Register a named symbol.

Register a symbol as a relation in a system of constrained Horn clauses.

Rewrite an expression.

Search for an index in a sorted array

select_implicant srk m ?env phi selects an implicant I of phi such that m,?env |= I |= phi.

Satisfiability via strategy improvement

Satisfiability via strategy improvement, forwards version

solve mat b computes a rational vector x such that mat*x = b, if such a vector exists.

solve_exn mat b computes a rational vector x such that mat*x = b.

Write a polynomial as a sum t + p, where t is a linear term and p is a polynomial in which every monomial has degree >= 2

Find the set of all coordinates that are associated with subterms of the term associated with a given coordinate.

Replace constant symbols by their interpretations within an expression.

Generalization of polynomial composition -- substitute each dimension for a multivariate polynomial

Given a polynomial p(x), compute a polynomial q(x) such that that for every integer x >= 0, we have q(x) = sum_{i=0}^x p(i).

Map a symbol to a dimension.

Retrieve the name of a named symbol.

Given a wedge wedge and a symbol symbol, compute a list of lower bounds and upper bounds for symbol that are implied by wedge.

Compute lower and upper bounds for a symbol that are implied by the given formula (if they exist).

Find the term associated with a coordinate

Convert a Z3 expression into a term.

Inverse of of_formula

Enumerate the variables and values assigned in a transition.

Apply Fourier-Motzkin elimination to the subset of symbols that appear linearly.

Replace non-linear arithmetic with uninterpreted functions.

Replace non-linear arithmetic with uninterpreted functions.

Given a pre-condition P, a path path, and a post-condition Q, determine whether the Hoare triple {P}path{Q} is valid.

Convert a linear polynomial to a vector, where each dimension corresponds to a variable except the designated const dimension, which is treated at a constant 1.

Find the vector associated with an admissible term.

vector_right_mul m a computes m*a

Widen abstracts both input transitions to the Cube abstract domain, performs the Cube widening operator, and then converts back to a transition.

Compute a winning SAT/UNSAT strategy for a formula.

Wrap a function mapping symbols to values in an interpretation.

Unexecutable transition (unit of add).