class documentation

Undocumented

Method __getstate__ Undocumented
Method __init__ Undocumented
Method __setstate__ Undocumented
Method add Adds constraint(s) to constraints list.
Method add_replacement Undocumented
Method batch_eval Evaluates `exprs`, returning a list of tuples (one tuple of `n` solutions for expression).
Method clear_replacements Undocumented
Method downsize Undocumented
Method eval Evaluates expression `e`, returning a tuple of `n` solutions.
Method is_false Checks if `e` can only (and TRIVIALLY) evaluate to False. If this function returns True, then the expression cannot ever be True, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be True; it's just that we can't trivially prove it...
Method is_true Checks if `e` can only (and TRIVIALLY) evaluate to True. If this function returns True, then the expression cannot ever be False, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be False; it's just that we can't trivially prove it...
Method max Evaluates `e`, returning its max possible value.
Method min Evaluates `e`, returning its min possible value.
Method remove_replacements Undocumented
Method satisfiable Checks if stored constraints conjunction is satisfiable.
Method solution Checks if `v` is a possible solution to `e`.
Method _add_solve_result Undocumented
Method _blank_copy Undocumented
Method _concrete_constraint Undocumented
Method _concrete_value Undocumented
Method _copy Undocumented
Method _replace_list Undocumented
Method _replacement Undocumented
Instance Variable _actual_frontend Undocumented
Instance Variable _allow_symbolic Undocumented
Instance Variable _auto_replace Undocumented
Instance Variable _complex_auto_replace Undocumented
Instance Variable _replace_constraints Undocumented
Instance Variable _replacement_cache Undocumented
Instance Variable _replacements Undocumented
Instance Variable _unsafe_replacement Undocumented
Instance Variable _validation_frontend Undocumented

Inherited from ConstrainedFrontend:

Method check_satisfiability Checks the satisfiability of stored constraints conjunction.
Method combine Undocumented
Method finalize Undocumented
Method independent_constraints Undocumented
Method merge Undocumented
Method simplify Simplifies the stored constraints conjunction.
Method split Undocumented
Instance Variable constraints Undocumented
Instance Variable variables Undocumented
Instance Variable _finalized Undocumented

Inherited from Frontend (via ConstrainedFrontend):

Method blank_copy Undocumented
Method branch Undocumented
Method eval_to_ast Evaluates expression `e`, returning a list of `n` concrete ASTs.
Static Method _split_constraints Returns independent constraints, split from this Frontend's `constraints`.
Method _constraint_filter Undocumented
def __init__(self, actual_frontend, allow_symbolic=None, replacements=None, replacement_cache=None, unsafe_replacement=None, complex_auto_replace=None, auto_replace=None, replace_constraints=None, **kwargs): (source)
def add(self, constraints, **kwargs): (source)

Adds constraint(s) to constraints list. :param constraints: constraint(s) to add :return:

def add_replacement(self, old, new, invalidate_cache=True, replace=True, promote=True): (source)

Undocumented

def batch_eval(self, exprs, n, extra_constraints=(), exact=None): (source)

Evaluates `exprs`, returning a list of tuples (one tuple of `n` solutions for expression). :param exprs: expressions :param n: the number of solutions to return :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: list of tuples of python primitives representing results

def clear_replacements(self): (source)

Undocumented

def eval(self, e, n, extra_constraints=(), exact=None): (source)

Evaluates expression `e`, returning a tuple of `n` solutions. :param e: the expression :param n: the number of solutions to return :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: tuple of python primitives representing results

def is_false(self, e, extra_constraints=(), exact=None): (source)

Checks if `e` can only (and TRIVIALLY) evaluate to False. If this function returns True, then the expression cannot ever be True, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be True; it's just that we can't trivially prove it. In other words, a return value of False gives you no information whatsoever. :param e: the expression :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: True if it can only evaluate to False otherwise False

def is_true(self, e, extra_constraints=(), exact=None): (source)

Checks if `e` can only (and TRIVIALLY) evaluate to True. If this function returns True, then the expression cannot ever be False, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be False; it's just that we can't trivially prove it. In other words, a return value of False gives you no information whatsoever. :param e: the expression :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: True if it can only evaluate to True otherwise False

def max(self, e, extra_constraints=(), signed=False, exact=None): (source)

Evaluates `e`, returning its max possible value. :param e: the expression :param extra_constraints: extra constraints to consider when performing the evaluation :param signed: whether the value should be treated as a signed integer :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: max possible value

def min(self, e, extra_constraints=(), signed=False, exact=None): (source)

Evaluates `e`, returning its min possible value. :param e: the expression :param extra_constraints: extra constraints to consider when performing the evaluation :param signed: whether the value should be treated as a signed integer :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: min possible value

def remove_replacements(self, old_entries): (source)

Undocumented

def satisfiable(self, extra_constraints=(), exact=None): (source)

Checks if stored constraints conjunction is satisfiable. :param extra_constraints: extra constraints to consider when checking satisfiability :param exact: whether or not to perform exact checking. Ignored by non-approximating backends. :return: True if the conjunction is satisfiable otherwise False

def solution(self, e, v, extra_constraints=(), exact=None): (source)

Checks if `v` is a possible solution to `e`. :param e: the expression :param v: the value :param extra_constraints: extra constraints to consider when performing the evaluation :param exact: whether or not to perform an exact evaluation. Ignored by non-approximating backends. :return: True if it is a possible solution otherwise False

def _add_solve_result(self, e, er, r): (source)

Undocumented

def _concrete_constraint(self, e): (source)

Undocumented

def _concrete_value(self, e): (source)
def _replace_list(self, lst): (source)

Undocumented

def _replacement(self, old): (source)

Undocumented

_actual_frontend = (source)

Undocumented

_allow_symbolic = (source)

Undocumented

_auto_replace = (source)

Undocumented

_complex_auto_replace = (source)

Undocumented

_replace_constraints = (source)

Undocumented

_replacement_cache = (source)

Undocumented

_replacements = (source)

Undocumented

_unsafe_replacement = (source)

Undocumented

_validation_frontend = (source)

Undocumented