SmtTems

Support for SMT constraints.

Module provides support for SMT expressions as constraints.

SmtTerm

Bases: Term

SMT terms.

Source code in pacti\src\pacti\terms\smt\smt.py

class SmtTerm(Term):
    """SMT terms."""

    def __init__(self, expression: z3.BoolRef):  # noqa: WPS231  too much cognitive complexity
        """
        Constructor for SmtTerm.

        Usage:
            SMT terms are initialized by passing an SMT expression.

        Args:
            expression: A boolean expression involving uninterpreted atoms.

        Raises:
            ValueError: Unsupported argument type.
        """
        self.expression: z3.BoolRef
        if isinstance(expression, z3.BoolRef):
            self.expression = copy.deepcopy(expression)
        else:
            raise ValueError()

    def __eq__(self, other: object) -> bool:
        if not isinstance(other, type(self)):
            raise ValueError()
        return str(self) == str(other)

    def __str__(self) -> str:
        # return SmtTerm.add_globally(_expr_to_str(self.expression))
        return str(self.expression)

    def __hash__(self) -> int:
        return hash(str(self))

    def __repr__(self) -> str:
        return "<Term {0}>".format(self)

    @property
    def atoms(self) -> List[str]:  # noqa: A003
        """
        Atoms appearing in term.

        Returns:
            List of atoms referenced in term.
        """
        return _get_z3_literals(self.expression)

    @property
    def vars(self) -> List[Var]:  # noqa: A003
        """
        Variables appearing in term.

        Returns:
            List of variables referenced in term.
        """
        return [Var(atom) for atom in self.atoms]

    def contains_var(self, var_to_seek: Var) -> bool:
        """
        Tell whether term contains a given variable.

        Args:
            var_to_seek: The variable that we are seeking in the current term.

        Returns:
            `True` if the syntax of the term refers to the given variable;
                `False` otherwise.
        """
        return var_to_seek in self.vars

    def copy(self) -> SmtTerm:
        """
        Generates copy of term.

        Returns:
            Copy of term.
        """
        expression = copy.deepcopy(self.expression)
        return SmtTerm(expression)

    def rename_variable(self, source_var: Var, target_var: Var) -> SmtTerm:
        """
        Rename a variable in a term.

        Args:
            source_var: The variable to be replaced.
            target_var: The new variable.

        Returns:
            A term with `source_var` replaced by `target_var`.
        """
        ret_expr = _rename_expr(self.expression, source_var.name, target_var.name)
        return SmtTerm(ret_expr)

    def is_tautology(self) -> bool:
        """
        Tell whether term is a tautology.

        Returns:
            True if tautology.
        """
        return _is_tautology(self.expression)

    def is_sat(self) -> bool:
        """
        Tell whether term is a satisfiable.

        Returns:
            True if satisfiable.
        """
        return _is_sat(self.expression)

    def contains_behavior(self, behavior: Dict[Var, numeric]) -> bool:
        """
        Tell whether Term contains the given behavior.

        Args:
            behavior:
                The behavior in question.

        Returns:
            True if the behavior satisfies the constraint; false otherwise.

        Raises:
            ValueError: Not all variables in the constraints were assigned values.
        """
        variables_to_substitute: List[Var] = list(behavior.keys())
        if list_diff(self.vars, variables_to_substitute):
            raise ValueError("Not all variables assigned")

        new_expression = copy.deepcopy(self.expression)
        relevant_variables: List[Var] = list_intersection(variables_to_substitute, self.vars)
        for elim_var in relevant_variables:
            new_expression = _replace_var_with_val(new_expression, elim_var.name, behavior[elim_var])
        return _is_tautology(new_expression)

atoms property

Atoms appearing in term.

Returns:

Type	Description
List[str]	List of atoms referenced in term.

vars property

Variables appearing in term.

Returns:

Type	Description
List[Var]	List of variables referenced in term.

__init__(expression)

Constructor for SmtTerm.

Usage

SMT terms are initialized by passing an SMT expression.

Parameters:

Name	Type	Description	Default
expression	BoolRef	A boolean expression involving uninterpreted atoms.	required

Raises:

Type	Description
ValueError	Unsupported argument type.

Source code in pacti\src\pacti\terms\smt\smt.py

def __init__(self, expression: z3.BoolRef):  # noqa: WPS231  too much cognitive complexity
    """
    Constructor for SmtTerm.

    Usage:
        SMT terms are initialized by passing an SMT expression.

    Args:
        expression: A boolean expression involving uninterpreted atoms.

    Raises:
        ValueError: Unsupported argument type.
    """
    self.expression: z3.BoolRef
    if isinstance(expression, z3.BoolRef):
        self.expression = copy.deepcopy(expression)
    else:
        raise ValueError()

contains_behavior(behavior)

Tell whether Term contains the given behavior.

Parameters:

Name	Type	Description	Default
behavior	Dict[Var, numeric]	The behavior in question.	required

Returns:

Type	Description
bool	True if the behavior satisfies the constraint; false otherwise.

Raises:

Type	Description
ValueError	Not all variables in the constraints were assigned values.

Source code in pacti\src\pacti\terms\smt\smt.py

def contains_behavior(self, behavior: Dict[Var, numeric]) -> bool:
    """
    Tell whether Term contains the given behavior.

    Args:
        behavior:
            The behavior in question.

    Returns:
        True if the behavior satisfies the constraint; false otherwise.

    Raises:
        ValueError: Not all variables in the constraints were assigned values.
    """
    variables_to_substitute: List[Var] = list(behavior.keys())
    if list_diff(self.vars, variables_to_substitute):
        raise ValueError("Not all variables assigned")

    new_expression = copy.deepcopy(self.expression)
    relevant_variables: List[Var] = list_intersection(variables_to_substitute, self.vars)
    for elim_var in relevant_variables:
        new_expression = _replace_var_with_val(new_expression, elim_var.name, behavior[elim_var])
    return _is_tautology(new_expression)

contains_var(var_to_seek)

Tell whether term contains a given variable.

Parameters:

Name	Type	Description	Default
var_to_seek	Var	The variable that we are seeking in the current term.	required

Returns:

Type	Description
bool	True if the syntax of the term refers to the given variable; False otherwise.

Source code in pacti\src\pacti\terms\smt\smt.py

def contains_var(self, var_to_seek: Var) -> bool:
    """
    Tell whether term contains a given variable.

    Args:
        var_to_seek: The variable that we are seeking in the current term.

    Returns:
        `True` if the syntax of the term refers to the given variable;
            `False` otherwise.
    """
    return var_to_seek in self.vars

copy()

Generates copy of term.

Returns:

Type	Description
SmtTerm	Copy of term.

Source code in pacti\src\pacti\terms\smt\smt.py

def copy(self) -> SmtTerm:
    """
    Generates copy of term.

    Returns:
        Copy of term.
    """
    expression = copy.deepcopy(self.expression)
    return SmtTerm(expression)

is_sat()

Tell whether term is a satisfiable.

Returns:

Type	Description
bool	True if satisfiable.

Source code in pacti\src\pacti\terms\smt\smt.py

def is_sat(self) -> bool:
    """
    Tell whether term is a satisfiable.

    Returns:
        True if satisfiable.
    """
    return _is_sat(self.expression)

is_tautology()

Tell whether term is a tautology.

Returns:

Type	Description
bool	True if tautology.

Source code in pacti\src\pacti\terms\smt\smt.py

def is_tautology(self) -> bool:
    """
    Tell whether term is a tautology.

    Returns:
        True if tautology.
    """
    return _is_tautology(self.expression)

rename_variable(source_var, target_var)

Rename a variable in a term.

Parameters:

Name	Type	Description	Default
source_var	Var	The variable to be replaced.	required
target_var	Var	The new variable.	required

Returns:

Type	Description
SmtTerm	A term with source_var replaced by target_var.

Source code in pacti\src\pacti\terms\smt\smt.py

def rename_variable(self, source_var: Var, target_var: Var) -> SmtTerm:
    """
    Rename a variable in a term.

    Args:
        source_var: The variable to be replaced.
        target_var: The new variable.

    Returns:
        A term with `source_var` replaced by `target_var`.
    """
    ret_expr = _rename_expr(self.expression, source_var.name, target_var.name)
    return SmtTerm(ret_expr)

SmtTermList

Bases: TermList

A TermList of SmtTerm instances.

Source code in pacti\src\pacti\terms\smt\smt.py

class SmtTermList(TermList):  # noqa: WPS338
    """A TermList of SmtTerm instances."""

    def __init__(self, terms: Optional[List[SmtTerm]] = None):
        """
        Constructor for SmtTermList.

        Args:
            terms: A list of SmtTerm objects.

        Raises:
            ValueError: incorrect argument type provided.
        """
        if terms is None:
            self.terms = []
        elif all(isinstance(t, SmtTerm) for t in terms):
            self.terms = terms.copy()
        else:
            raise ValueError("SmtTermList constructor argument must be a list of SmtTerms.")

    def __str__(self) -> str:
        res = "[\n  "
        res += "\n  ".join(self.to_str_list())
        res += "\n]"
        return res

    def __hash__(self) -> int:
        return hash(tuple(self.terms))

    def __le__(self, other: SmtTermList) -> bool:
        return self.refines(other)

    def is_semantically_equivalent_to(self, other: SmtTermList) -> bool:
        """
        Tell whether two termlists are semantically equivalent.

        Args:
            other:
                The termlist against which we compare self.

        Returns:
            True if the two termlists are semantically equivalent.
        """
        return self.refines(other) and other.refines(self)

    def to_str_list(self) -> List[str]:
        """
        Convert termlist into a list of strings.

        Returns:
            A list of strings corresponding to the terms of the termlist.
        """
        return [str(term) for term in self.terms]

    def contains_behavior(self, behavior: Dict[Var, numeric]) -> bool:
        """
        Tell whether TermList contains the given behavior.

        Args:
            behavior:
                The behavior in question.

        Returns:
            True if the behavior satisfies the constraints; false otherwise.

        Raises:
            ValueError: Not all variables in the constraints were assigned values.
        """
        for term in self.terms:
            try:
                if not term.contains_behavior(behavior):
                    return False
            except ValueError as e:
                raise ValueError(e)
        return True

    def _to_smtexpr(self) -> z3.BoolRef:
        return z3.And(*[xs.expression for xs in self.terms])

    @staticmethod
    def _transform_term(  # noqa: WPS231  too much cognitive complexity
        term: SmtTerm,
        context: SmtTermList,
        vars_to_elim: list,
        refine: bool,
        simplify: bool = True,
        tactics_order: Optional[List[int]] = None,
    ) -> Tuple[SmtTerm, SmtTermList]:
        new_term: SmtTerm

        # Check whether there is something to do with this term
        if list_intersection(vars_to_elim, term.vars):
            atoms_to_elim = list(map(str, list_intersection(vars_to_elim, list_union(term.vars, context.vars))))
            reference_term = SmtTerm(_elim_variables(term.expression, context._to_smtexpr(), atoms_to_elim, refine))
            new_term = reference_term.copy()
            final_context = context.copy()

            # now check whether we can find equivalent "in-context" semantics using a reduced context
            if simplify:
                golden_compare = context | SmtTermList([reference_term])
                indices_removed: List[int] = []
                for i, _ in enumerate(context.terms):
                    test_context = SmtTermList(list_remove_indices(context.terms, indices_removed + [i]))
                    test_term = SmtTerm(
                        _elim_variables(term.expression, test_context._to_smtexpr(), atoms_to_elim, refine)
                    )
                    test_compare = context | SmtTermList([test_term])

                    if (golden_compare).is_semantically_equivalent_to(test_compare):
                        indices_removed.append(i)
                        new_term = test_term.copy()
                        final_context = test_context.copy()
        else:
            new_term = term.copy()
            final_context = context.copy()
        if not new_term.is_sat():
            raise ValueError("Computed term is empty")
        return new_term, final_context

    def _transform_termlist(  # noqa: WPS231  too much cognitive complexity
        self,
        context: SmtTermList,
        vars_to_elim: list,
        refine: bool,
        simplify: bool = True,
        tactics_order: Optional[List[int]] = None,
    ) -> Tuple[SmtTermList, TacticStatistics]:
        new_terms = []

        # only keep the context with relevant variables
        relevant_terms = []
        for term in context.terms:
            if list_intersection(term.vars, vars_to_elim):
                relevant_terms.append(term)
        relevant_context = SmtTermList(relevant_terms)

        for term in self.terms:
            try:
                new_term, _ = SmtTermList._transform_term(
                    term, relevant_context, vars_to_elim, refine, simplify, tactics_order
                )
            except ValueError as e:
                raise ValueError(e)
            new_terms.append(new_term)
        return SmtTermList(new_terms), []

    def elim_vars_by_refining(  # noqa: WPS231  too much cognitive complexity
        self,
        context: SmtTermList,
        vars_to_elim: list,
        simplify: bool = True,
        tactics_order: Optional[List[int]] = None,
    ) -> Tuple[SmtTermList, TacticStatistics]:
        """
        Eliminate variables from SmtTermList by refining it in context.

        Example:
            Suppose the current list of terms is $\\{x + y \\le 6\\}$, the
            context is $\\{y \\le 5\\}$, and the resulting terms should not
            contain variable $y$. Then the current TermList could be
            refined to $\\{x \\le 1\\}$ because $x \\le 1
            \\;\\land\\; y \\le 5 \\Rightarrow x + y \\le 6$.

        Args:
            context:
                The TermList providing the context for the refinement.
            vars_to_elim:
                Variables that should not appear in the resulting term.
            simplify:
                Whether to perform simplifications.
            tactics_order:
                Optionally, the order of tactics to invoke during transformation.

        Returns:
            A tuple of (a) a list of terms not containing any variables in `vars_to_elim`
                and which, in the context provided, imply the terms contained in the
                calling termlist; and (b) the list of tuples, for each processed term, of
                the tactic used, time spend, and tactic invocation count.

        Raises:
            ValueError: Self has empty intersection with its context.
        """
        try:
            return self._transform_termlist(
                context=context, vars_to_elim=vars_to_elim, refine=True, simplify=simplify, tactics_order=tactics_order
            )
        except ValueError as e:
            raise ValueError(e)

    def elim_vars_by_relaxing(
        self,
        context: SmtTermList,
        vars_to_elim: list,
        simplify: bool = True,
        tactics_order: Optional[List[int]] = None,
    ) -> Tuple[SmtTermList, TacticStatistics]:
        """
        Eliminate variables from SmtTemList by abstracting it in context.

        Example:
            Suppose the current list of terms is $\\{x - y \\le 6\\}$, the
            context is $\\{y \\le 5\\}$, and the resulting terms should not
            contain variable $y$. Then the current TermList could be
            relaxed to $\\{x \\le 11\\}$ because $x - y \\le 6
            \\;\\land\\; y \\le 5 \\Rightarrow x \\le 11$.

        Args:
            context:
                The TermList providing the context for the transformation.
            vars_to_elim:
                Variables that should not appear in the relaxed terms.
            simplify:
                Whether to perform simplifications.
            tactics_order:
                Optionally, the order of tactics to invoke during transformation.

        Returns:
            A tuple of (a) a list of terms not containing any variables in `vars_to_elim`
                and which, in the context provided, are implied by the terms
                contained in the calling termlist; and (b) the list of tuples, for each
                processed term, of the tactic used, time spend, and tactic invocation count.
        """
        return self._transform_termlist(
            context=context, vars_to_elim=vars_to_elim, refine=False, simplify=simplify, tactics_order=tactics_order
        )

    def simplify(self, context: Optional[SmtTermList] = None) -> SmtTermList:
        """
        Remove redundant terms in the TermList using the provided context.

        Example:
            Suppose the TermList is $\\{x - 2y \\le 5, x - y \\le 0\\}$ and
            the context is $\\{x + y \\le 0\\}$. Then the TermList could be
            simplified to $\\{x - y \\le 0\\}$.

        Args:
            context:
                The TermList providing the context for the simplification.

        Returns:
            A new TermList with redundant terms removed using the provided context.
        """
        newterms: List[SmtTerm] = []
        external_context = SmtTermList([])
        if context:
            external_context = context
        for i, term_under_analysis in enumerate(self.terms):
            useful_context = SmtTermList(newterms) | SmtTermList(self.terms[i + 1 :]) | external_context
            if not useful_context.refines(SmtTermList([term_under_analysis])):
                newterms.append(term_under_analysis.copy())
        return SmtTermList(newterms)

    def refines(self, other: SmtTermList) -> bool:
        """
        Tells whether the argument is a larger specification.

        Args:
            other:
                TermList against which we are comparing self.

        Returns:
            self <= other
        """
        antecedent = self._to_smtexpr()
        consequent = other._to_smtexpr()
        test_expr: z3.BoolRef = z3.Implies(antecedent, consequent)
        return _is_tautology(test_expr)

    def is_empty(self) -> bool:
        """
        Tell whether the argument has no satisfying assignments.

        Returns:
            True if constraints cannot be satisfied.
        """
        test_expr = self._to_smtexpr()
        if _is_sat(test_expr):  # noqa: WPS531 if condition can be simplified
            return False
        return True

__init__(terms=None)

Constructor for SmtTermList.

Parameters:

Name	Type	Description	Default
terms	Optional[List[SmtTerm]]	A list of SmtTerm objects.	None

Raises:

Type	Description
ValueError	incorrect argument type provided.

Source code in pacti\src\pacti\terms\smt\smt.py

def __init__(self, terms: Optional[List[SmtTerm]] = None):
    """
    Constructor for SmtTermList.

    Args:
        terms: A list of SmtTerm objects.

    Raises:
        ValueError: incorrect argument type provided.
    """
    if terms is None:
        self.terms = []
    elif all(isinstance(t, SmtTerm) for t in terms):
        self.terms = terms.copy()
    else:
        raise ValueError("SmtTermList constructor argument must be a list of SmtTerms.")

contains_behavior(behavior)

Tell whether TermList contains the given behavior.

Parameters:

Name	Type	Description	Default
behavior	Dict[Var, numeric]	The behavior in question.	required

Returns:

Type	Description
bool	True if the behavior satisfies the constraints; false otherwise.

Raises:

Type	Description
ValueError	Not all variables in the constraints were assigned values.

Source code in pacti\src\pacti\terms\smt\smt.py

def contains_behavior(self, behavior: Dict[Var, numeric]) -> bool:
    """
    Tell whether TermList contains the given behavior.

    Args:
        behavior:
            The behavior in question.

    Returns:
        True if the behavior satisfies the constraints; false otherwise.

    Raises:
        ValueError: Not all variables in the constraints were assigned values.
    """
    for term in self.terms:
        try:
            if not term.contains_behavior(behavior):
                return False
        except ValueError as e:
            raise ValueError(e)
    return True

elim_vars_by_refining(context, vars_to_elim, simplify=True, tactics_order=None)

Eliminate variables from SmtTermList by refining it in context.

Example

Suppose the current list of terms is \(\{x + y \le 6\}\), the context is \(\{y \le 5\}\), and the resulting terms should not contain variable \(y\). Then the current TermList could be refined to \(\{x \le 1\}\) because \(x \le 1 \;\land\; y \le 5 \Rightarrow x + y \le 6\).

Parameters:

Name	Type	Description	Default
context	SmtTermList	The TermList providing the context for the refinement.	required
vars_to_elim	list	Variables that should not appear in the resulting term.	required
simplify	bool	Whether to perform simplifications.	True
tactics_order	Optional[List[int]]	Optionally, the order of tactics to invoke during transformation.	None

Returns:

Type	Description
Tuple[SmtTermList, TacticStatistics]	A tuple of (a) a list of terms not containing any variables in vars_to_elim and which, in the context provided, imply the terms contained in the calling termlist; and (b) the list of tuples, for each processed term, of the tactic used, time spend, and tactic invocation count.

Raises:

Type	Description
ValueError	Self has empty intersection with its context.

Source code in pacti\src\pacti\terms\smt\smt.py

def elim_vars_by_refining(  # noqa: WPS231  too much cognitive complexity
    self,
    context: SmtTermList,
    vars_to_elim: list,
    simplify: bool = True,
    tactics_order: Optional[List[int]] = None,
) -> Tuple[SmtTermList, TacticStatistics]:
    """
    Eliminate variables from SmtTermList by refining it in context.

    Example:
        Suppose the current list of terms is $\\{x + y \\le 6\\}$, the
        context is $\\{y \\le 5\\}$, and the resulting terms should not
        contain variable $y$. Then the current TermList could be
        refined to $\\{x \\le 1\\}$ because $x \\le 1
        \\;\\land\\; y \\le 5 \\Rightarrow x + y \\le 6$.

    Args:
        context:
            The TermList providing the context for the refinement.
        vars_to_elim:
            Variables that should not appear in the resulting term.
        simplify:
            Whether to perform simplifications.
        tactics_order:
            Optionally, the order of tactics to invoke during transformation.

    Returns:
        A tuple of (a) a list of terms not containing any variables in `vars_to_elim`
            and which, in the context provided, imply the terms contained in the
            calling termlist; and (b) the list of tuples, for each processed term, of
            the tactic used, time spend, and tactic invocation count.

    Raises:
        ValueError: Self has empty intersection with its context.
    """
    try:
        return self._transform_termlist(
            context=context, vars_to_elim=vars_to_elim, refine=True, simplify=simplify, tactics_order=tactics_order
        )
    except ValueError as e:
        raise ValueError(e)

elim_vars_by_relaxing(context, vars_to_elim, simplify=True, tactics_order=None)

Eliminate variables from SmtTemList by abstracting it in context.

Example

Suppose the current list of terms is \(\{x - y \le 6\}\), the context is \(\{y \le 5\}\), and the resulting terms should not contain variable \(y\). Then the current TermList could be relaxed to \(\{x \le 11\}\) because \(x - y \le 6 \;\land\; y \le 5 \Rightarrow x \le 11\).

Parameters:

Name	Type	Description	Default
context	SmtTermList	The TermList providing the context for the transformation.	required
vars_to_elim	list	Variables that should not appear in the relaxed terms.	required
simplify	bool	Whether to perform simplifications.	True
tactics_order	Optional[List[int]]	Optionally, the order of tactics to invoke during transformation.	None

Returns:

Type	Description
Tuple[SmtTermList, TacticStatistics]	A tuple of (a) a list of terms not containing any variables in vars_to_elim and which, in the context provided, are implied by the terms contained in the calling termlist; and (b) the list of tuples, for each processed term, of the tactic used, time spend, and tactic invocation count.

Source code in pacti\src\pacti\terms\smt\smt.py

def elim_vars_by_relaxing(
    self,
    context: SmtTermList,
    vars_to_elim: list,
    simplify: bool = True,
    tactics_order: Optional[List[int]] = None,
) -> Tuple[SmtTermList, TacticStatistics]:
    """
    Eliminate variables from SmtTemList by abstracting it in context.

    Example:
        Suppose the current list of terms is $\\{x - y \\le 6\\}$, the
        context is $\\{y \\le 5\\}$, and the resulting terms should not
        contain variable $y$. Then the current TermList could be
        relaxed to $\\{x \\le 11\\}$ because $x - y \\le 6
        \\;\\land\\; y \\le 5 \\Rightarrow x \\le 11$.

    Args:
        context:
            The TermList providing the context for the transformation.
        vars_to_elim:
            Variables that should not appear in the relaxed terms.
        simplify:
            Whether to perform simplifications.
        tactics_order:
            Optionally, the order of tactics to invoke during transformation.

    Returns:
        A tuple of (a) a list of terms not containing any variables in `vars_to_elim`
            and which, in the context provided, are implied by the terms
            contained in the calling termlist; and (b) the list of tuples, for each
            processed term, of the tactic used, time spend, and tactic invocation count.
    """
    return self._transform_termlist(
        context=context, vars_to_elim=vars_to_elim, refine=False, simplify=simplify, tactics_order=tactics_order
    )

is_empty()

Tell whether the argument has no satisfying assignments.

Returns:

Type	Description
bool	True if constraints cannot be satisfied.

Source code in pacti\src\pacti\terms\smt\smt.py

def is_empty(self) -> bool:
    """
    Tell whether the argument has no satisfying assignments.

    Returns:
        True if constraints cannot be satisfied.
    """
    test_expr = self._to_smtexpr()
    if _is_sat(test_expr):  # noqa: WPS531 if condition can be simplified
        return False
    return True

is_semantically_equivalent_to(other)

Tell whether two termlists are semantically equivalent.

Parameters:

Name	Type	Description	Default
other	SmtTermList	The termlist against which we compare self.	required

Returns:

Type	Description
bool	True if the two termlists are semantically equivalent.

Source code in pacti\src\pacti\terms\smt\smt.py

def is_semantically_equivalent_to(self, other: SmtTermList) -> bool:
    """
    Tell whether two termlists are semantically equivalent.

    Args:
        other:
            The termlist against which we compare self.

    Returns:
        True if the two termlists are semantically equivalent.
    """
    return self.refines(other) and other.refines(self)

refines(other)

Tells whether the argument is a larger specification.

Parameters:

Name	Type	Description	Default
other	SmtTermList	TermList against which we are comparing self.	required

Returns:

Type	Description
bool	self <= other

Source code in pacti\src\pacti\terms\smt\smt.py

def refines(self, other: SmtTermList) -> bool:
    """
    Tells whether the argument is a larger specification.

    Args:
        other:
            TermList against which we are comparing self.

    Returns:
        self <= other
    """
    antecedent = self._to_smtexpr()
    consequent = other._to_smtexpr()
    test_expr: z3.BoolRef = z3.Implies(antecedent, consequent)
    return _is_tautology(test_expr)

simplify(context=None)

Remove redundant terms in the TermList using the provided context.

Example

Suppose the TermList is \(\{x - 2y \le 5, x - y \le 0\}\) and the context is \(\{x + y \le 0\}\). Then the TermList could be simplified to \(\{x - y \le 0\}\).

Parameters:

Name	Type	Description	Default
context	Optional[SmtTermList]	The TermList providing the context for the simplification.	None

Returns:

Type	Description
SmtTermList	A new TermList with redundant terms removed using the provided context.

Source code in pacti\src\pacti\terms\smt\smt.py

def simplify(self, context: Optional[SmtTermList] = None) -> SmtTermList:
    """
    Remove redundant terms in the TermList using the provided context.

    Example:
        Suppose the TermList is $\\{x - 2y \\le 5, x - y \\le 0\\}$ and
        the context is $\\{x + y \\le 0\\}$. Then the TermList could be
        simplified to $\\{x - y \\le 0\\}$.

    Args:
        context:
            The TermList providing the context for the simplification.

    Returns:
        A new TermList with redundant terms removed using the provided context.
    """
    newterms: List[SmtTerm] = []
    external_context = SmtTermList([])
    if context:
        external_context = context
    for i, term_under_analysis in enumerate(self.terms):
        useful_context = SmtTermList(newterms) | SmtTermList(self.terms[i + 1 :]) | external_context
        if not useful_context.refines(SmtTermList([term_under_analysis])):
            newterms.append(term_under_analysis.copy())
    return SmtTermList(newterms)

to_str_list()

Convert termlist into a list of strings.

Returns:

Type	Description
List[str]	A list of strings corresponding to the terms of the termlist.

Source code in pacti\src\pacti\terms\smt\smt.py

def to_str_list(self) -> List[str]:
    """
    Convert termlist into a list of strings.

    Returns:
        A list of strings corresponding to the terms of the termlist.
    """
    return [str(term) for term in self.terms]