( * ) [Syntax.Infix] | |
(!) [Syntax.Infix] | |
(&&) [Syntax.Infix] | |
(+) [Syntax.Infix] | |
(-) [Syntax.Infix] | |
(/) [Syntax.Infix] | |
(<) [Syntax.Infix] | |
(<=) [Syntax.Infix] | |
(=) [Syntax.Infix] | |
(mod) [Syntax.Infix] | |
(||) [Syntax.Infix] | |
A | |
abs [ZZ] | |
abs [QQ] | |
abstract [Wedge] |
Compute a wedge that over-approximates a given formula
|
abstract [Abstract] | abstract ?exists srk man phi computes the strongest property that is
implied by phi which is expressible within a given abstract domain.
|
abstract_iter [Iteration.Domain] | |
abstract_post [Transition.Make] | |
add [Transition.Make] |
Non-deterministically choose between two transitions
|
add [Interpretation] | |
add [Linear.Ring] | |
add [Linear.AbelianGroup] | |
add [Linear.Vector] | |
add [Linear.QQMatrix] | |
add [SrkZ3.CHC] | add solver formulas asserts that each formula in formulas holds.
|
add [SrkZ3.Solver] | |
add [Smt.Solver] | |
add [Interval] | |
add [Syntax.ContextTable] | |
add [Syntax.Expr.Map] | |
add [Syntax.Expr.Set] | |
add [Syntax.Expr.HT] | |
add [ZZ] | |
add [QQ] | |
add_bool [Interpretation] | |
add_column [Linear.QQMatrix] | |
add_entry [Linear.QQMatrix] | |
add_fun [Interpretation] | |
add_real [Interpretation] | |
add_row [Linear.QQMatrix] | |
add_rule [SrkZ3.CHC] | add_rule solver hypothesis conclusion adds the rule hypothesis =>
conclusion to solver .
|
add_saturate [Polynomial.Rewrite] |
Add a new zero-polynomial to a rewrite system and saturate
|
add_term [Linear.Vector] | |
add_vars [SrkApron] | |
adjacent_pairs [SrkUtil] | |
admit_cs_term [CoordinateSystem] |
Extend a coordinate system with one additional coordinate term, if that
coordinate does not already belong to the system.
|
admit_term [CoordinateSystem] |
Extend a coordinate system to admit a term
|
admits [CoordinateSystem] |
Does a coordinate system admit the given term?
|
affine_hull [Abstract] | affine_hull srk phi symbols computes a basis for the affine hull of phi,
projected onto the given set of symbols.
|
affine_interpretation [Smt] |
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.
|
alpha [Transition.Make.Iter] | |
apron_of [Interval] | |
assign [Transition.Make] | assign v t is a transition that assigns the term t to the variable
v .
|
assume [Transition.Make] | assume phi is a transition that doesn't modify any variables, but can
only be executed when phi holds
|
B | |
block [Polynomial.Monomial] |
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.
|
bool [Interpretation] | |
bottom [Wedge] | |
bottom [SrkApron] | |
bottom [Interval] | |
bottom [Memo.Tabulate.RecFun] | |
bottom [Memo.Tabulate.Fun] | |
bounds [Wedge] |
Given a wedge
wedge and a term term , compute a lower and upper bounds
for term within the region wedge .
|
boxify [Abstract] | boxify srk phi terms computes the strongest formula of the form
/\ { lo <= t <= hi : t in terms }
that is implied by phi .
|
boxify [SrkApron] | |
C | |
call [Memo.Tabulate.S] | |
call_direct [Memo.Tabulate.S] | |
cartesian_product [SrkUtil] | |
ceiling [QQ] | |
check [SrkZ3.CHC] | |
check [SrkZ3.Solver] | |
check [Smt.Solver] | |
check_strategy [Quantifier] |
Verify that a SAT strategy is in fact a winning strategy.
|
clear [Syntax.ContextTable] | |
clear [DisjointSet.Make] | |
closure [Transition.Make.Iter] | |
closure [Iteration.PreDomain] | |
closure_plus [Iteration.DomainPlus] | |
cod_equal [Memo.Tabulate.RecFun] | |
cod_equal [Memo.Tabulate.Fun] | |
coeff [Linear.Vector] | |
coeff_of_qq [SrkApron] | |
colorize [Log] | |
column_set [Linear.QQMatrix] | |
compare [Transition.Var] | |
compare [Transition.Make] |
Compare is a purely syntactic comparison.
|
compare [Polynomial.Mvp] | |
compare [Polynomial.Monomial] | |
compare [Linear.QQVector] | |
compare [Linear.ZZVector] | |
compare [Interval] | |
compare [Syntax.Formula] | |
compare [Syntax.Term] | |
compare [Syntax.Expr] | |
compare [Syntax.Symbol] | |
compare [ZZ] | |
compare [QQ] | |
compare [SrkUtil.Int.I] | |
compare_expr [Syntax] | |
compare_formula [Syntax] | |
compare_symbol [Syntax] | |
compare_term [Syntax] | |
compose [Polynomial.Univariate] | |
conjoin [Polyhedron] | |
const [Interval] | |
const [Syntax.Infix] | |
const_dim [Linear] |
Dimension for representing the coefficient of the constant 1.
|
const_id [CoordinateSystem] |
Virtual coordinate associated with 1
|
const_linterm [Linear] |
Representation of a rational number as an affine term.
|
const_of [Interval] | |
const_of_linterm [Linear] |
Convert an affine term to a rational number, if possible.
|
construct [Transition.Make] |
Guarded parallel assignment
|
context [Syntax.Context] | |
coordinate_system [Wedge] | |
copy [Wedge] | |
copy [CoordinateSystem] | |
copy [DisjointSet.Make] | |
create [Syntax.ContextTable] | |
create [Syntax.Expr.HT] | |
create [DisjointSet.Make] | |
cs_term_id [CoordinateSystem] |
Find the coordinate associated with an coordinate term.
|
D | |
debug [Log] | |
debug_formatter [Log] | |
debug_mode [Log] | |
debug_phases [Log] | |
debug_pp [Log] | |
debugf [Log] | |
default_debug [Log] | |
default_sep [SrkUtil] | |
defines [Transition.Make] | |
deglex [Polynomial.Monomial] |
Compare by total degree, then lexicographic order
|
degrevlex [Polynomial.Monomial] |
Compare by total degree, then reverse lexicographic order
|
denominator [QQ] | |
destruct [Syntax.Formula] | |
destruct [Syntax.Term] | |
destruct [Syntax] | |
destruct_atom [Interpretation] | |
destruct_coordinate [CoordinateSystem] | |
dim [CoordinateSystem] |
Number of dimensions in the coordinate system
|
dim_of_sym [Linear] |
Map a dimension to symbol.
|
dim_of_var [SrkApron.Env] | |
dimension [SrkApron.Env] | |
dimensions [SrkApron.Env] | |
dimensions [Polynomial.Mvp] |
Enumerate the set of dimensions that appear in a polynomial
|
direct_subcoordinates [CoordinateSystem] |
Find the set of all coordinates that are associated with *direct* subterms
of the term associated with a given coordinate.
|
distinct_pairs [SrkUtil] | |
div [Polynomial.Monomial] | |
div [Interval] | |
div [ZZ] |
Integer division conforming to SMTLIB2:
a == (a/b)*b + a%b and 0 <= a%b < |b|
|
div [QQ] | |
div_monomial [Polynomial.Mvp] |
Divide a polynomial by a monomial
|
divide_right [Linear] |
Given two matrices A and B, compute a matrix C such that CB = A (if one
exists).
|
dom_equal [Memo.Tabulate.RecFun] | |
dom_equal [Memo.Tabulate.Fun] | |
dot [Linear.Vector] | |
E | |
easy_sat [Quantifier] |
Alternating quantifier satisfiability
|
elem [Interval] | |
eliminate_ite [Syntax] | |
empty [SrkApron.Env] | |
empty [Interpretation] | |
empty [Syntax.Expr.Map] | |
empty [Syntax.Expr.Set] | |
empty [Syntax.Env] | |
empty [FeatureTree] | |
ensure_min_max [Wedge] | |
ensure_nonlinear_symbols [Wedge] |
Ensure that the named symbols
pow : Real x Real -> Real and log : Real
x Real -> Real belong to a given context.
|
ensure_symbols [Nonlinear] |
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.
|
entails [Smt] | |
entries [Linear.QQMatrix] | |
entry [Linear.QQMatrix] | |
enum [Polyhedron] | |
enum [Interpretation] |
Enumerate the concrete bindings in an interpretation.
|
enum [Polynomial.Monomial] | |
enum [Linear.Vector] | |
enum [Syntax.Expr.Map] | |
enum [Syntax.Expr.Set] | |
enum [Syntax.Expr.HT] | |
enum [Syntax.Env] | |
enum [FeatureTree] | |
eq [DisjointSet.Make] | |
equal [Transition.Make.Iter] | |
equal [Transition.Make] |
Test whether two transitions are equal up to logical equivalence and
renaming skolem constants.
|
equal [Iteration.PreDomain] | |
equal [Wedge] | |
equal [SrkApron] | |
equal [Polynomial.Monomial] | |
equal [Linear.Ring] | |
equal [Linear.AbelianGroup] | |
equal [Linear.Vector] | |
equal [Linear.QQMatrix] | |
equal [Interval] | |
equal [Syntax.Formula] | |
equal [Syntax.Term] | |
equal [Syntax.Expr] | |
equal [ZZ] | |
equal [QQ] | |
equal [SrkUtil.Int.I] | |
equational_saturation [Wedge] | |
equiv [Smt] | |
error [Log] | |
error_pp [Log] | |
errorf [Log] | |
eval [Polynomial.Univariate] | |
eval [Syntax.Formula] | |
eval [Syntax.Term] | |
eval_memo [Syntax.Formula] | |
eval_partial [Syntax.Term] | |
eval_texpr [SrkApron] |
Evaluate an expression in the environment Top.
|
evaluate_affine [Linear] | |
evaluate_formula [Interpretation] | |
evaluate_linterm [Linear] | evaluate_linterm env t evaluates the affine term t in the environment
env
|
evaluate_term [Interpretation] | |
existential_closure [Syntax.Formula] | |
exists [Transition.Make] | exists ex tr removes the variables that do not satisfy the predicate
ex from the footprint of a transition.
|
exists [Wedge] |
Project symbols out of a wedge that do not satisfy the given predicate.
|
exists [SrkApron] | |
exists [Syntax.Infix] | |
exp [Polynomial.Mvp] |
Exponentiation by a positive integer
|
exp [Polynomial.Univariate] |
Exponentiation
|
exp [QQ] | |
exp [SrkUtil] | |
exp_const [Interval] | const_power ivl k computes an interval surrounding the set the set
{ x^k : x in ivl } .
|
expr_of_z3 [SrkZ3] |
Convert a Z3 expression into an expression.
|
expr_typ [Syntax] | |
F | |
f [Memo.Tabulate.RecFun] |
Function to be tabulated
|
f [Memo.Tabulate.Fun] |
Function to be tabulated
|
factor [Polynomial.QQX] |
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.
|
farkas_equalities [Wedge] |
Compute a representation of the set of equalities that are entailed by a
given wedge as a list
(term0, vector0),...,(termn,vectorn) .
|
fatal [Log] | |
fatalf [Log] | |
features [FeatureTree] | |
filter [SrkApron.Env] | |
filter [Syntax.Expr.Map] | |
filter_map [Syntax.Expr.Map] | |
find [Syntax.ContextTable] | |
find [Syntax.Expr.Map] | |
find [Syntax.Expr.HT] | |
find [Syntax.Env] | |
find [DisjointSet.Make] | |
find_impl [DisjointSet.Make] | |
find_leq [FeatureTree] |
Find an element with features <= the given feature vector, and which
satisfies the given predicate.
|
find_leq_map [FeatureTree] |
Find an element
elt with features <= the given feature vector, and on
which the given partial function f is defined; return f elt .
|
floor [Interval] | |
floor [QQ] | |
fls [Syntax.Infix] | |
fold [Syntax.Expr.Map] | |
fold_constants [Syntax] | |
forall [Syntax.Infix] | |
formula_of_property [SrkApron] | |
formula_of_z3 [SrkZ3] |
Convert a Z3 expression into a formula.
|
free_vars [Syntax] | |
G | |
gcd [ZZ] | |
gcd [QQ] | |
generators [Polynomial.Rewrite] | |
get_concrete_model [SrkZ3.Solver] | |
get_concrete_model [Smt.Solver] | |
get_concrete_model [Smt] | |
get_context [CoordinateSystem] | |
get_context [Interpretation] | |
get_manager [SrkApron] | |
get_model [SrkZ3.Solver] | |
get_model [Smt.Solver] | |
get_model [Smt] | |
get_named_symbol [Syntax] |
Retrieve the symbol associated with a given name.
|
get_solution [SrkZ3.CHC] | |
get_transform [Transition.Make] |
Retrieve the value of a variable after a transition as a term over input
variables (and Skolem constants)
|
get_unsat_core [SrkZ3.Solver] | |
get_unsat_core [Smt.Solver] | |
grobner_basis [Polynomial.Rewrite] |
Saturate a polynomial rewrite system with implied equalities
|
guard [Transition.Make] |
The condition under which a transition may be executed.
|
H | |
hash [Syntax.Formula] | |
hash [Syntax.Term] | |
hash [ZZ] | |
hash [QQ] | |
hash [Memo.Tabulate.RecFun] | |
hash [Memo.Tabulate.Fun] | |
hash [SrkUtil.Int.I] | |
havoc [Transition.Make] |
Assign a list of variables non-deterministic values.
|
I | |
identity [Polynomial.Univariate] |
The polynomial
p(x) = x
|
identity [Linear.QQMatrix] | |
idiv [QQ] | |
implicant_of [Polyhedron] |
Convert a polyhedron to a conjunction of atomic formulas (as returned by
Interpretation.select_implicant ).
|
insert [FeatureTree] | |
int_dim [CoordinateSystem] |
Number of integer dimensions in the coordinate system
|
int_dim [SrkApron.Env] | |
int_of_symbol [Syntax] | |
integral [Interval] | |
inter [Syntax.Expr.Set] | |
interpolate [Transition.Make] |
Given a path (list of transitions
tr_1 ... tr_n ) and a post-condition
formula, determine whether the path implies the post-condition.
|
interpolate_seq [SrkZ3] |
Sequence interpolation.
|
interpret [Nonlinear] |
Replace non-linear uninterpreted functions with interpreted ones.
|
interpret_rewriter [Nonlinear] |
Replace non-linear uninterpreted functions with interpreted ones.
|
intersect_rowspace [Linear] |
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 .
|
invalid_argf [Log] | |
inverse [QQ] | |
is_bottom [Wedge] | |
is_bottom [SrkApron] | |
is_empty [Syntax.Expr.Map] | |
is_negative [Interval] | |
is_nonnegative [Interval] | |
is_nonpositive [Interval] | |
is_one [Transition.Make] | |
is_positive [Interval] | |
is_registered_name [Syntax] |
Test if a name is already associated with a symbol
|
is_sat [Wedge] |
Check if a formula is satisfiable by computing an over-approximating wedge
and checking whether it is feasible.
|
is_sat [Smt] | |
is_top [Wedge] | |
is_top [SrkApron] | |
is_zero [Transition.Make] | |
is_zero [Linear.Vector] | |
J | |
join [Transition.Make.Iter] | |
join [Iteration.PreDomain] | |
join [Wedge] | |
join [SrkApron] | |
join [Interval] | |
join [Memo.Tabulate.RecFun] | |
join [Memo.Tabulate.Fun] | |
K | |
keys [Syntax.Expr.Map] | |
keys [Syntax.Expr.HT] | |
L | |
lcm [Polynomial.Monomial] |
Least common multiple
|
lcm [ZZ] | |
lcm [QQ] | |
lcons_eqz [SrkApron] | |
lcons_geqz [SrkApron] | |
lcons_gtz [SrkApron] | |
left [Iteration.Sum] | |
leq [SrkApron] | |
leq [Interval] | |
leq [ZZ] | |
leq [QQ] | |
level_leq [Log] | |
level_of_string [Log] | |
lex [Polynomial.Monomial] |
Lexicographic order
|
lexpr_of_vec [SrkApron] | |
linearize [Nonlinear] |
Compute a linear approximation of a non-linear formula.
|
linterm_of [Linear] |
Convert a rational vector representing an affine term.
|
linterm_size [Linear] |
Count the number of dimensions with non-zero coefficients
|
load_smtlib2 [SrkZ3] |
Parse a SMTLIB2-formatted string
|
local_project [Polyhedron] |
Model-guided projection of a polyhedron.
|
log [Interval] | |
log [Log.Make] | |
log_pp [Log.Make] | |
logf [Log.Make] | |
loggers [Log] | |
lower [Interval] | |
lt [ZZ] | |
lt [QQ] | |
M | |
make [Interval] | |
make_bounded [Interval] | |
map [Syntax.Expr.Map] | |
max [ZZ] | |
max [QQ] | |
max_rowspace_projection [Linear] |
Given matrices
A and B , find a matrix C whose rows constitute a
basis for the vector space { v : exists u. uA = vB }
|
maximize [Quantifier] |
Alternating quantifier optimization
|
meet [Wedge] | |
meet [SrkApron] | |
meet [Interval] | |
meet_atoms [Wedge] | |
meet_lcons [SrkApron] | |
meet_tcons [SrkApron] | |
mem [Polyhedron] |
Test whether a point, representing as a map from symbols to rationals, is
inside a polyhedron.
|
mem [SrkApron.Env] | |
mem [Syntax.ContextTable] | |
mem [Syntax.Expr.Set] | |
mem [Syntax.Expr.HT] | |
mem_transform [Transition.Make] |
Is a variable written to in a transition?
|
memo [Memo.Make] | |
memo [Memo] |
Memoize a function using built-in polymorphic hash.
|
memo_recursive [Memo.Make] | |
memo_recursive [Memo] |
Memoize a recursive function using built-in polymorphic hash.
|
merge [Syntax.Expr.Map] | |
merge_array [SrkUtil] |
Merge two (sorted) arrays
|
min [ZZ] | |
min [QQ] | |
mk_add [Syntax.Context] | |
mk_add [Syntax] | |
mk_and [Syntax.Context] | |
mk_and [Syntax] | |
mk_app [Syntax.Context] | |
mk_app [Syntax] | |
mk_ceiling [Syntax] | |
mk_const [Syntax.Context] | |
mk_const [Syntax] | |
mk_context [SrkSimplify.TermPolynomial] | |
mk_div [Syntax.Context] | |
mk_div [Syntax] | |
mk_empty [CoordinateSystem] | |
mk_eq [Syntax.Context] | |
mk_eq [Syntax] | |
mk_exists [Syntax.Context] | |
mk_exists [Syntax] | |
mk_exists_const [Syntax.Context] | |
mk_exists_const [Syntax] | |
mk_false [Syntax.Context] | |
mk_false [Syntax] | |
mk_floor [Syntax.Context] | |
mk_floor [Syntax] | |
mk_forall [Syntax.Context] | |
mk_forall [Syntax] | |
mk_forall_const [Syntax.Context] | |
mk_forall_const [Syntax] | |
mk_idiv [Syntax.Context] | |
mk_idiv [Syntax] |
C99 integer division.
|
mk_if [Syntax] | |
mk_iff [Syntax] | |
mk_ite [Syntax.Context] | |
mk_ite [Syntax] | |
mk_leq [Syntax.Context] | |
mk_leq [Syntax] | |
mk_lt [Syntax.Context] | |
mk_lt [Syntax] | |
mk_mod [Syntax.Context] | |
mk_mod [Syntax] | |
mk_mul [Syntax.Context] | |
mk_mul [Syntax] | |
mk_neg [Syntax.Context] | |
mk_neg [Syntax] |
Unary negation
|
mk_not [Syntax.Context] | |
mk_not [Syntax] | |
mk_or [Syntax.Context] | |
mk_or [Syntax] | |
mk_pow [Syntax] | |
mk_real [Syntax.Context] | |
mk_real [Syntax] | |
mk_rewrite [Polynomial.Rewrite] |
Given an admissible order and a list of zero polynomials, orient the
polynomials into a rewrite system.
|
mk_show [SrkUtil] | |
mk_solver [SrkZ3.CHC] | |
mk_solver [SrkZ3] | |
mk_solver [Smt] | |
mk_sub [Syntax.Context] | |
mk_sub [Syntax] |
Subtraction
|
mk_symbol [Syntax.Context] | |
mk_symbol [Syntax] | |
mk_true [Syntax.Context] | |
mk_true [Syntax] | |
mk_truncate [Syntax] | truncate(t) removes the fractional part of t (rounding it towards
0).
|
mk_var [Syntax.Context] | |
mk_var [Syntax] | |
modulo [Interval] | |
modulo [ZZ] |
Modulo conforming to SMTLIB2:
a == (a/b)*b + a%b and 0 <= a%b < |b|
|
modulo [QQ] | |
mul [Transition.Make] |
Sequentially compose two transitions.
|
mul [Polynomial.Mvp] | |
mul [Polynomial.Monomial] | |
mul [Polynomial.Univariate] | |
mul [Linear.Ring] | |
mul [Linear.QQMatrix] | |
mul [Interval] | |
mul [ZZ] | |
mul [QQ] | |
mul_term [Polynomial.Monomial] | |
my_verbosity_level [Log.Make] | |
N | |
nb_columns [Linear.QQMatrix] | |
nb_rows [Linear.QQMatrix] | |
negate [Linear.Ring] | |
negate [Linear.AbelianGroup] | |
negate [Linear.Vector] | |
negate [Interval] | |
negate [ZZ] | |
negate [QQ] | |
nnf_rewriter [Syntax] |
Convert to negation normal form (down pass).
|
normalize [Quantifier] | |
nudge [QQ] |
Compute an upper and lower bound for a rational number (with small
representations) via truncated continued fractions.
|
nudge_down [QQ] |
Compute an lower bound for a rational number (with a small
representation).
|
nudge_up [QQ] |
Compute an upper bound for a rational number (with a small
representation).
|
nullspace [Linear] | nullspace mat dimensions computes a basis for the vector space { x :
max*x = 0} , projected on to the set of dimensions dimensions .
|
numerator [QQ] | |
O | |
of_apron [Interval] | |
of_atoms [Wedge] | |
of_dim [Polynomial.Mvp] | |
of_enum [SrkApron.Env] | |
of_enum [Polynomial.Monomial] | |
of_enum [Linear.Vector] | |
of_float [QQ] | |
of_formula [Polyhedron] |
Convert formula that contains only conjunction and linear equalities and
disequalities into a polyhedron.
|
of_frac [QQ] | |
of_implicant [Polyhedron] |
Convert a conjunction of atomic formulas (as returned by
Interpretation.select_implicant ) to a polyhedron.
|
of_int [ZZ] | |
of_int [QQ] | |
of_linterm [Linear] |
Convert a rational vector to an affine term.
|
of_list [SrkApron.Env] | |
of_list [Linear.Vector] | |
of_list [FeatureTree] | |
of_set [SrkApron.Env] | |
of_string [ZZ] | |
of_string [QQ] | |
of_symbol [Transition.Var] | |
of_term [BigO] | |
of_term [SrkSimplify.TermPolynomial] | |
of_term [Linear.Vector] | |
of_vec [Polynomial.Mvp] |
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.
|
of_zz [QQ] | |
of_zzfrac [QQ] | |
one [Transition.Make] |
Skip (unit of
mul ).
|
one [Polynomial.Mvp] | |
one [Polynomial.Monomial] | |
one [Polynomial.Univariate] | |
one [Linear.Ring] | |
one [Interval] | |
one [ZZ] | |
one [QQ] | |
optimize_box [SrkZ3] |
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.
|
order [Polynomial.Univariate] | |
orient [Linear] |
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.
|
P | |
parallel_assign [Transition.Make] |
Parallel assignment of a list of terms to a list of variables.
|
partition_implicant [SrkSimplify] | |
phase [Log] | |
phases_ht [Log] | |
pivot [Polynomial.Monomial] | |
pivot [Linear.Vector] | |
pivot [Linear.QQMatrix] | |
polyhedron [Wedge] | |
polynomial_of_coordinate [CoordinateSystem] | |
polynomial_of_term [CoordinateSystem] |
Find a polynomial associated with an admissible term over
*non-multiplicative* cooridnate.
|
polynomial_of_vec [CoordinateSystem] |
Convert a vector to a polynomial *without multiplicative coordinates*.
|
pop [SrkZ3.CHC] | |
pop [SrkZ3.Solver] | |
pop [Smt.Solver] | |
power [Polynomial.Monomial] | |
pp [BigO] | |
pp [Transition.Var] | |
pp [Transition.Make.Iter] | |
pp [Transition.Make] | |
pp [Iteration.PreDomain] | |
pp [Wedge] | |
pp [CoordinateSystem] | |
pp [Polyhedron] | |
pp [SrkApron.Env] | |
pp [SrkApron] | |
pp [Interpretation] | |
pp [Polynomial.Rewrite] | |
pp [Polynomial.Mvp] | |
pp [Polynomial.Monomial] | |
pp [Polynomial.QQX] | |
pp [Linear.QQMatrix] | |
pp [Linear.QQVector] | |
pp [Linear.ZZVector] | |
pp [Interval] | |
pp [Syntax.Formula] | |
pp [Syntax.Term] | |
pp [Syntax.Expr] | |
pp [ZZ] | |
pp [QQ] | |
pp [SrkUtil.Int.Set] | |
pp [SrkUtil.Int.I] | |
pp_cs_term [CoordinateSystem] | |
pp_linterm [Linear] |
Pretty-print an affine term
|
pp_print_enum [SrkUtil] | |
pp_print_enum_nobox [SrkUtil] | |
pp_print_list [SrkUtil] | |
pp_smtlib2 [Syntax] |
Print a formula as a satisfiability query in SMTLIB2 format.
|
pp_strategy [Quantifier] | |
pp_symbol [Syntax] | |
pp_typ [Syntax] | |
pp_vector [CoordinateSystem] | |
preduce [Polynomial.Rewrite] |
Reduce a multi-variate polynomial using the given rewrite rules until no
more rewrite rules apply.
|
prenex [Syntax.Formula] | |
print_stats [Log] | |
project [Polyhedron] |
Fourier-Motzkin elimination.
|
project_ideal [CoordinateSystem] | |
purify [SrkSimplify] |
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.
|
push [SrkZ3.CHC] | |
push [SrkZ3.Solver] | |
push [Smt.Solver] | |
push [Syntax.Env] | |
Q | |
qe [SrkZ3] |
Quantifier elimination
|
qe_mbp [Quantifier] |
Quantifier eliminiation via model-based projection
|
qq_of_coeff [SrkApron] | |
qq_of_scalar [SrkApron] | |
R | |
rational_eigenvalues [Linear.QQMatrix] |
Compute a list rational eigenvalues of a matrix, along with their
algebraic multiplicities.
|
rational_triangulation [Linear] |
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.
|
real [Interpretation] | |
real_dim [CoordinateSystem] |
Number of real dimensions in the coordinate system
|
real_dim [SrkApron.Env] | |
rebalance [FeatureTree] | |
reduce [Polynomial.Rewrite] |
Reduce a multi-variate polynomial using the given rewrite rules until
no more rewrite rules apply
|
reduce_rewrite [Polynomial.Rewrite] | |
refine [Syntax.Expr] | |
register_named_symbol [Syntax] |
Register a named symbol.
|
register_relation [SrkZ3.CHC] |
Register a symbol as a relation in a system of constrained Horn clauses.
|
remove [Syntax.Expr.Map] | |
remove [Syntax.Expr.HT] | |
remove [FeatureTree] | |
rename [SrkApron] | |
replace [Syntax.ContextTable] | |
replace [Syntax.Expr.HT] | |
reset [SrkZ3.Solver] | |
reset [Smt.Solver] | |
reverse_map [DisjointSet.Make] | |
rewrite [Syntax] |
Rewrite an expression.
|
right [Iteration.Sum] | |
row [Linear.QQMatrix] | |
row_set [Linear.QQMatrix] | |
rowsi [Linear.QQMatrix] | |
S | |
same_set [DisjointSet.Make] | |
scalar [Polynomial.Mvp] | |
scalar [Polynomial.Univariate] | |
scalar_mul [Linear.Vector] | |
scalar_mul [Linear.QQMatrix] | |
search [SrkUtil] |
Search for an index in a sorted array
|
select_implicant [Interpretation] | select_implicant srk m ?env phi selects an implicant I of phi such
that m,?env |= I |= phi .
|
select_ite [Interpretation] | |
set_verbosity_level [Log] | |
show [Transition.Var] | |
show [Transition.Make.Iter] | |
show [Transition.Make] | |
show [Iteration.PreDomain] | |
show [Wedge] | |
show [SrkApron] | |
show [Polynomial.QQX] | |
show [Linear.QQMatrix] | |
show [Linear.QQVector] | |
show [Linear.ZZVector] | |
show [Interval] | |
show [Syntax.Formula] | |
show [Syntax.Term] | |
show [ZZ] | |
show [QQ] | |
show [SrkUtil.Int.I] | |
show_strategy [Quantifier] | |
show_symbol [Syntax] | |
simplify_terms [SrkSimplify] | |
simplify_terms_rewriter [SrkSimplify] | |
simsat [Quantifier] |
Satisfiability via strategy improvement
|
simsat_forward [Quantifier] |
Satisfiability via strategy improvement, forwards version
|
singleton [Polynomial.Monomial] | |
size [Syntax] | |
skolemize_free [Syntax.Formula] | |
solve [Linear] | solve mat b computes a rational vector x such that mat*x = b , if
such a vector exists.
|
solve_exn [Linear] | solve_exn mat b computes a rational vector x such that mat*x =
b .
|
split_linear [Polynomial.Mvp] |
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
|
star [Transition.Make.Iter] | |
start_time [Log] | |
strengthen [Wedge] | |
sub [Polynomial.Mvp] | |
sub [Linear.Vector] | |
sub [ZZ] | |
sub [QQ] | |
subcoordinates [CoordinateSystem] |
Find the set of all coordinates that are associated with subterms of the
term associated with a given coordinate.
|
substitute [Interpretation] |
Replace constant symbols by their interpretations within an expression.
|
substitute [Polynomial.Mvp] |
Generalization of polynomial composition -- substitute each dimension
for a multivariate polynomial
|
substitute [Syntax] | |
substitute_const [Syntax] | |
substitute_map [Syntax] | |
summation [Polynomial.QQX] |
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) .
|
sym_of_dim [Linear] |
Map a symbol to a dimension.
|
symbol_name [Syntax] |
Retrieve the name of a named symbol.
|
symbol_of [Transition.Var] | |
symbol_of_int [Syntax] | |
symbolic_bounds [Wedge] |
Given a wedge
wedge and a symbol symbol , compute a list of lower bounds
and upper bounds for symbol that are implied by wedge .
|
symbolic_bounds_formula [Wedge] |
Compute lower and upper bounds for a symbol that are implied by the given
formula (if they exist).
|
symbols [Syntax] | |
T | |
tcons_eqz [SrkApron] | |
tcons_geqz [SrkApron] | |
tcons_gtz [SrkApron] | |
term_of [SrkSimplify.TermPolynomial] | |
term_of [Polynomial.Mvp] | |
term_of [Polynomial.Monomial] | |
term_of_coordinate [CoordinateSystem] |
Find the term associated with a coordinate
|
term_of_polynomial [CoordinateSystem] | |
term_of_texpr [SrkApron] | |
term_of_vec [CoordinateSystem] | |
term_of_z3 [SrkZ3] |
Convert a Z3 expression into a term.
|
term_typ [Syntax] | |
texpr_of_term [SrkApron] | |
time [Log] | |
to_apron [Polyhedron] | |
to_atoms [Wedge] | |
to_float [QQ] | |
to_formula [Wedge] | |
to_formula [Polyhedron] |
Inverse of
of_formula
|
to_int [ZZ] | |
to_int [QQ] | |
to_string [SrkZ3.CHC] | |
to_string [SrkZ3.Solver] | |
to_string [Smt.Solver] | |
to_zz [QQ] | |
to_zzfrac [QQ] | |
top [Wedge] | |
top [Polyhedron] | |
top [SrkApron] | |
top [Interval] | |
tr_symbols [Iteration.PreDomain] | |
transform [Transition.Make] |
Enumerate the variables and values assigned in a transition.
|
transpose [Linear.QQMatrix] | |
tru [Syntax.Infix] | |
try_fourier_motzkin [Polyhedron] |
Apply Fourier-Motzkin elimination to the subset of symbols that appear
linearly.
|
tuples [SrkUtil] | |
typ [Transition.Var] | |
typ_symbol [Syntax] | |
type_of_id [CoordinateSystem] | |
U | |
uninterpret [Nonlinear] |
Replace non-linear arithmetic with uninterpreted functions.
|
uninterpret_rewriter [Nonlinear] |
Replace non-linear arithmetic with uninterpreted functions.
|
union [Syntax.Expr.Set] | |
union [DisjointSet.Make] | |
universal_closure [Syntax.Formula] | |
update [Memo.Tabulate.S] | |
upper [Interval] | |
uses [Transition.Make] | |
V | |
valid_triple [Transition.Make] |
Given a pre-condition
P , a path path , and a post-condition Q ,
determine whether the Hoare triple {P}path{Q} is valid.
|
value [Interpretation] | |
values [Syntax.Expr.Map] | |
values [Syntax.Expr.HT] | |
vanishing_ideal [Wedge] | |
var [Syntax.Infix] | |
var_of_dim [SrkApron.Env] | |
vars [SrkApron.Env] | |
vec_of [Polynomial.Mvp] |
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.
|
vec_of_lexpr [SrkApron] | |
vec_of_term [CoordinateSystem] |
Find the vector associated with an admissible term.
|
vector_right_mul [Linear] | vector_right_mul m a computes m*a
|
verbosity_level [Log] | |
W | |
widen [Transition.Make.Iter] | |
widen [Transition.Make] |
Widen abstracts both input transitions to the Cube abstract domain,
performs the Cube widening operator, and then converts back to a transition.
|
widen [Iteration.PreDomain] | |
widen [Wedge] | |
widen [SrkApron] | |
winning_strategy [Quantifier] |
Compute a winning SAT/UNSAT strategy for a formula.
|
wrap [Interpretation] |
Wrap a function mapping symbols to values in an interpretation.
|
Z | |
z3_of_expr [SrkZ3] | |
z3_of_formula [SrkZ3] | |
z3_of_term [SrkZ3] | |
zero [Transition.Make] |
Unexecutable transition (unit of
add ).
|
zero [Linear.Ring] | |
zero [Linear.AbelianGroup] | |
zero [Linear.Vector] | |
zero [Linear.QQMatrix] | |
zero [Interval] | |
zero [ZZ] | |
zero [QQ] |