Repository: pacti-org/pacti (language: python)

Issue:
Outputs are now deterministic wrt a given input
With this update, a given input provided to gear will yield the same result.

WARNING! It breaks compatibility with the previous input format. Variables and requirements are now lists instead of sets.


Discussion / hints:

Fix patch:
diff --git a/examples/example.json b/examples/example.json
index ba64bb7b..d9c2af5b 100644
--- a/examples/example.json
+++ b/examples/example.json
@@ -19,7 +19,7 @@
             {"coefficients":{"i":-1,"o":1},
             "constant":0},
             {"coefficients":{"i":1,"o":-2},
-            "constant":5}
+            "constant":2}
         ]
     },
     "contract2":{
@@ -31,7 +31,7 @@
         ],
         "assumptions":
         [
-            {"coefficients":{"o":3},
+            {"coefficients":{"o":5},
             "constant":1},
             {"coefficients":{"o":-1},
             "constant":1}
diff --git a/examples/example_quotient.json b/examples/example_quotient.json
index 9fea5152..d0f18a81 100644
--- a/examples/example_quotient.json
+++ b/examples/example_quotient.json
@@ -10,12 +10,16 @@
         "assumptions":
         [
             {"coefficients":{"i":1},
+            "constant":1},
+            {"coefficients":{"i":-1},
             "constant":1}
         ],
         "guarantees":
         [
             {"coefficients":{"i":-2,"o_p":1},
-            "constant":1}
+            "constant":1},
+            {"coefficients":{"i":2,"o_p":-1},
+            "constant":-1}
         ]
     },
     "contract2":{
@@ -28,11 +32,15 @@
         "assumptions":
         [
             {"coefficients":{"i":1},
+            "constant":2},
+            {"coefficients":{"i":-1},
             "constant":2}
         ],
         "guarantees":
         [
             {"coefficients":{"o":1,"i":-2},
+            "constant":0},
+            {"coefficients":{"o":-1,"i":2},
             "constant":0}
         ]
     },
diff --git a/src/gear/gear.py b/src/gear/gear.py
index fa387b51..b21afbf4 100644
--- a/src/gear/gear.py
+++ b/src/gear/gear.py
@@ -10,8 +10,8 @@
 import gear.polyhedralterm as polyhedralterm
 
 
-def getVarset(aList):
-    return set([iocontract.Var(varstr) for varstr in aList])
+def getVarlist(aList):
+    return list([iocontract.Var(varstr) for varstr in aList])
 
 
 @click.command()
@@ -28,10 +28,10 @@ def readInputFile(inputfilename, outputfilename):
         for key in ["assumptions", "guarantees"]:
             reqs.append([polyhedralterm.PolyhedralTerm(term["coefficients"], term["constant"]) for term in c[key]])
         cont = iocontract.IoContract(
-            inputVars=getVarset(c["InputVars"]),
-            outputVars=getVarset(c["OutputVars"]),
-            assumptions=polyhedralterm.PolyhedralTermSet(set(reqs[0])),
-            guarantees=polyhedralterm.PolyhedralTermSet(set(reqs[1])),
+            inputVars=getVarlist(c["InputVars"]),
+            outputVars=getVarlist(c["OutputVars"]),
+            assumptions=polyhedralterm.PolyhedralTermList(list(reqs[0])),
+            guarantees=polyhedralterm.PolyhedralTermList(list(reqs[1])),
         )
         contracts.append(cont)
     print("Contract1:\n" + str(contracts[0]))
diff --git a/src/gear/iocontract.py b/src/gear/iocontract.py
index be2aa0f2..219e9783 100644
--- a/src/gear/iocontract.py
+++ b/src/gear/iocontract.py
@@ -1,24 +1,25 @@
 """
-IoContracts contains Gear's basic definitions: Var, Term, TemSet, and
+IoContracts contains Gear's basic definitions: Var, Term, TemList, and
 IoContract. Var creates variables; Term is an abstract class representing
-constraints; a TermSet (also an abstract class) is a collection of terms
+constraints; a TermList (also an abstract class) is a collection of terms
 semantically equivalent to the term which is the conjunction of all terms
-contained in the TermSet; IoContract is an assume-guarantee specification
+contained in the TermList; IoContract is an assume-guarantee specification
 consisting of assumptions, guarantees, and input and output variables. The
-assumptions and guarantees are given by TermSets. Assumptions make predicates
+assumptions and guarantees are given by TermLists. Assumptions make predicates
 only on inputs, and guarantees on both input and outputs (and no other
 variable).
 
 This module implements all supported contract operations and relations. In order
 to instantiate contracts and perform this operations, it is necessary to extend
-Term and TermSet with specific constraint formalisms.
+Term and TermList with specific constraint formalisms.
 """
 from __future__ import annotations
 
 import copy
 import logging
 from abc import ABC, abstractmethod
-from typing import Set
+from typing import List
+from gear.utils import *
 
 
 class Var:
@@ -92,25 +93,25 @@ def copy(self):
         pass
 
 
-class TermSet(ABC):
+class TermList(ABC):
     """
     A collection of terms, or constraints.
 
-    A TermSet is semantically equivalent to a single term which is the
-    conjunction of all terms contained in the TermSet. TermSet is an abstract
+    A TermList is semantically equivalent to a single term which is the
+    conjunction of all terms contained in the TermList. TermList is an abstract
     class that must be extended to support a specific constraint formalism.
     """
 
-    def __init__(self, termSet: set):
-        self.terms = termSet.copy()
+    def __init__(self, termList: List):
+        self.terms = termList.copy()
 
     @property
     def vars(self):
-        """The set of variables contained in this set of terms."""
-        varset = set()
+        """The list of variables contained in this list of terms."""
+        varlist = list()
         for t in self.terms:
-            varset = varset | t.vars
-        return varset
+            varlist = list_union(varlist, t.vars)
+        return varlist
 
     def __str__(self) -> str:
         if len(self.terms) > 0:
@@ -122,27 +123,27 @@ def __str__(self) -> str:
     def __eq__(self, other):
         return self.terms == other.terms
 
-    def get_terms_with_vars(self, variable_set: Set[Var]):
+    def get_terms_with_vars(self, variable_list: List[Var]):
         """
-        Returns the set of terms which contain any of the variables indicated.
+        Returns the list of terms which contain any of the variables indicated.
 
         Args:
-            varSet: a set of variables being sought in current TermSet.
+            varList: a list of variables being sought in current TermList.
         """
-        terms = set()
+        terms = list()
         for t in self.terms:
-            if len(t.vars & variable_set) > 0:
-                terms.add(t)
+            if len(list_intersection(t.vars, variable_list)) > 0:
+                terms.append(t)
         return type(self)(terms)
 
     def __and__(self, other):
-        return type(self)(self.terms & other.terms)
+        return type(self)(list_intersection(self.terms, other.terms))
 
     def __or__(self, other):
-        return type(self)(self.terms | other.terms)
+        return type(self)(list_union(self.terms, other.terms))
 
     def __sub__(self, other):
-        return type(self)(self.terms - other.terms)
+        return type(self)(list_union(self.terms, other.terms))
 
     def __le__(self, other):
         return self.refines(other)
@@ -151,75 +152,75 @@ def copy(self):
         return type(self)(copy.copy(self.terms))
 
     @abstractmethod
-    def abduce_with_context(self, context: TermSet, vars_to_elim: Set[Var]) -> TermSet:
+    def abduce_with_context(self, context: TermList, vars_to_elim: List[Var]) -> TermList:
         """
         Abduce terms containing variables to be eliminated using a user-provided
         context.
 
-        Given a context :math:`\\Gamma`, and the set of terms contained in self,
-        :math:`s`, this routine identifies a TermSet :math:`x` lacking variables
+        Given a context :math:`\\Gamma`, and the list of terms contained in self,
+        :math:`s`, this routine identifies a TermList :math:`x` lacking variables
         vars_to_elim such that :math:`\\frac{\\Gamma\\colon \\; x}{\\Gamma: \\;
         s}`.
 
         Args:
             context:
-                Set of context terms that will be used to abduce the TermSet.
+                List of context terms that will be used to abduce the TermList.
             vars_to_elim:
-                Variables that cannot be present in TermSet after abduction.
+                Variables that cannot be present in TermList after abduction.
 
         Returns:
-            A set of terms not containing any variables in :code:`vars_to_elim`
+            A list of terms not containing any variables in :code:`vars_to_elim`
             and which, in the context provided, imply the terms contained in the
-            calling termset.
+            calling termlist.
         """
 
     @abstractmethod
-    def deduce_with_context(self, context: TermSet, vars_to_elim: Set[Var]) -> TermSet:
+    def deduce_with_context(self, context: TermList, vars_to_elim: List[Var]) -> TermList:
         """
         Deduce terms containing variables to be eliminated using a user-provided
         context.
 
-        Given a context :math:`\\Gamma`, and the set of terms contained in self,
+        Given a context :math:`\\Gamma`, and the list of terms contained in self,
         :math:`s`, this routine identifies a formula :math:`x` lacking variables
         vars_to_elim such that :math:`\\frac{\\Gamma\\colon \\; s}{\\Gamma: \\;
         x}`.
 
         Args:
             context:
-                Set of context terms that will be used to abstract the TermSet.
+                List of context terms that will be used to abstract the TermList.
             vars_to_elim:
-                Variables that cannot be present in TermSet after deduction.
+                Variables that cannot be present in TermList after deduction.
 
         Returns:
-            A set of terms not containing any variables in :code:`vars_to_elim`
+            A list of terms not containing any variables in :code:`vars_to_elim`
             and which, in the context provided, are implied by the terms
-            contained in the calling termset.
+            contained in the calling termlist.
         """
 
     @abstractmethod
-    def simplify(self, context=set()):
-        """Remove redundant terms in TermSet.
+    def simplify(self, context=list()):
+        """Remove redundant terms in TermList.
 
-        Let :math:`S` be this TermSet and suppose :math:`T \\subseteq S`. Let
+        Let :math:`S` be this TermList and suppose :math:`T \\subseteq S`. Let
         :math:`S_T = S \\setminus T`. Simplify will remove from :math:`S` a
         maximal subset :math:`T` such that :math:`\\frac{\\Gamma, S_T\\colon \\;
         \\top}{\\Gamma, S_T\\colon \\; \\wedge_{t \\in T} t}`.
 
         Args:
             context:
-                Set of context terms that will be used to remove redundancies in
-                the TermSet.
+                List of context terms that will be used to remove redundancies in
+                the TermList.
         """
 
     @abstractmethod
-    def refines(self, other: TermSet) -> bool:
+    def refines(self, other: TermList) -> bool:
         """
         Tell whether the argument is a larger specification, i.e., compute self
         <= other.
 
         Args:
             other:
-                TermSet against which we are comparing self.
+                TermList against which we are comparing self.
         """
 
 
@@ -235,20 +236,20 @@ class IoContract:
         outputvars:
             Variables which are outputs of the implementations of the contract.
 
-        a(TermSet): Contract assumptions.
+        a(TermList): Contract assumptions.
 
-        g(TermSet): Contract guarantees.
+        g(TermList): Contract guarantees.
     """
 
-    def __init__(self, assumptions: TermSet, guarantees: TermSet, inputVars: Set[Var], outputVars: Set[Var]) -> None:
+    def __init__(self, assumptions: TermList, guarantees: TermList, inputVars: List[Var], outputVars: List[Var]) -> None:
         # make sure the input & output variables are disjoint
-        assert len(inputVars & outputVars) == 0
+        assert len(list_intersection(inputVars, outputVars)) == 0
         # make sure the assumptions only contain input variables
-        assert len(assumptions.vars - inputVars) == 0, print(
+        assert len(list_diff(assumptions.vars, inputVars)) == 0, print(
             "A: " + str(assumptions.vars) + " Input vars: " + str(inputVars)
         )
         # make sure the guaranteees only contain input or output variables
-        assert len(guarantees.vars - inputVars - outputVars) == 0, print(
+        assert len(list_diff(guarantees.vars, list_union(inputVars, outputVars))) == 0, print(
             "G: "
             + str(guarantees)
             + " G Vars: "
@@ -268,7 +269,7 @@ def __init__(self, assumptions: TermSet, guarantees: TermSet, inputVars: Set[Var
     @property
     def vars(self):
         """
-        The set of variables contained in the assumptions and guarantees of the
+        The list of variables contained in the assumptions and guarantees of the
         contract.
         """
         return self.a.vars | self.g.vars
@@ -298,8 +299,8 @@ def can_compose_with(self, other: IoContract) -> bool:
                 Contract whose possibility to compose with self we are
                 verifying.
         """
-        # make sure sets of output variables don't intersect
-        return len(self.outputvars & other.outputvars) == 0
+        # make sure lists of output variables don't intersect
+        return len(list_intersection(self.outputvars, other.outputvars)) == 0
 
     def can_quotient_by(self, other: IoContract) -> bool:
         """
@@ -311,7 +312,7 @@ def can_quotient_by(self, other: IoContract) -> bool:
         # make sure the top level ouputs not contained in outputs of the
         # existing component do not intersect with the inputs of the existing
         # component
-        return len((self.outputvars - other.outputvars) & other.inputvars) == 0
+        return len(list_intersection(list_diff(self.outputvars,other.outputvars), other.inputvars)) == 0
 
     def shares_io_with(self, other: IoContract) -> bool:
         """
@@ -350,28 +351,28 @@ def compose(self, other: IoContract) -> IoContract:
             The abstracted composition of the two contracts.
         """
         logging.debug("Composing contracts \n%s and \n%s", self, other)
-        intvars = (self.outputvars & other.inputvars) | (self.inputvars & other.outputvars)
-        inputvars = (self.inputvars | other.inputvars) - intvars
-        outputvars = (self.outputvars | other.outputvars) - intvars
+        intvars = list_union(list_intersection(self.outputvars, other.inputvars), list_intersection(self.inputvars, other.outputvars))
+        inputvars = list_diff(list_union(self.inputvars, other.inputvars), intvars)
+        outputvars = list_diff(list_union(self.outputvars, other.outputvars), intvars)
 
         selfinputconst = self.a.vars
         otherinputconst = other.a.vars
-        cycle_present = len(self.inputvars & other.outputvars) > 0 and len(other.inputvars & self.outputvars) > 0
+        cycle_present = len(list_intersection(self.inputvars, other.outputvars)) > 0 and len(list_intersection(other.inputvars, self.outputvars)) > 0
 
-        assumptions_forbidden_vars = intvars | outputvars
+        assumptions_forbidden_vars = list_union(intvars, outputvars)
         assert self.can_compose_with(other)
-        other_helps_self = len(other.outputvars & self.inputvars) > 0
-        self_helps_other = len(other.inputvars & self.outputvars) > 0
+        other_helps_self = len(list_intersection(other.outputvars, self.inputvars)) > 0
+        self_helps_other = len(list_intersection(other.inputvars, self.outputvars)) > 0
         #
-        other_drives_const_inputs = len(other.outputvars & selfinputconst) > 0
-        self_drives_const_inputs = len(self.outputvars & otherinputconst) > 0
+        other_drives_const_inputs = len(list_intersection(other.outputvars, selfinputconst)) > 0
+        self_drives_const_inputs = len(list_intersection(self.outputvars, otherinputconst)) > 0
         # process assumptions
         if cycle_present and (other_drives_const_inputs or self_drives_const_inputs):
             assert False, "Cannot compose due to feedback"
         elif self_helps_other and not other_helps_self:
             logging.debug("Assumption computation: self provides context for other")
             new_a = other.a.abduce_with_context(self.a | self.g, assumptions_forbidden_vars)
-            if len(new_a.vars & assumptions_forbidden_vars) > 0:
+            if len(list_intersection(new_a.vars, assumptions_forbidden_vars)) > 0:
                 raise ValueError(
                     "The guarantees \n{}\n".format(self.g)
                     + "were insufficient to abduce the assumptions \n{}\n".format(other.a)
@@ -428,17 +429,17 @@ def quotient(self, other: IoContract) -> IoContract:
             The refined quotient self/other.
         """
         assert self.can_quotient_by(other)
-        outputvars = (self.outputvars - other.outputvars) | (other.inputvars - self.inputvars)
-        inputvars = (self.inputvars - other.inputvars) | (other.outputvars - self.outputvars)
-        intvars = (self.outputvars & other.outputvars) | (self.inputvars & other.inputvars)
+        outputvars = list_union(list_diff(self.outputvars, other.outputvars), list_diff(other.inputvars, self.inputvars))
+        inputvars = list_union(list_diff(self.inputvars, other.inputvars), list_diff(other.outputvars, self.outputvars))
+        intvars = list_union(list_intersection(self.outputvars, other.outputvars), list_intersection(self.inputvars, other.inputvars))
 
         # get assumptions
         logging.debug("Computing quotient assumptions")
         assumptions = copy.deepcopy(self.a)
-        empty_context = type(assumptions)(set())
+        empty_context = type(assumptions)(list())
         if assumptions.refines(other.a):
             assumptions = assumptions | other.g
-        assumptions = assumptions.deduce_with_context(empty_context, intvars | outputvars)
+        assumptions = assumptions.deduce_with_context(empty_context, list_union(intvars, outputvars))
         logging.debug("Assumptions after processing: %s", assumptions)
 
         # get guarantees
@@ -449,7 +450,7 @@ def quotient(self, other: IoContract) -> IoContract:
         Using existing guarantees to aid system-level guarantees
         """
         )
-        guarantees = guarantees.abduce_with_context(other.a | other.g, intvars)
+        guarantees = guarantees.abduce_with_context(other.g | other.a, intvars)
         logging.debug(
             """
         Using system-level assumptions to aid quotient guarantees"""
@@ -474,6 +475,6 @@ def merge(self, other: IoContract) -> IoContract:
             The result of merging.
         """
         assert self.shares_io_with(other)
-        assumptions = self.a | other.a
-        guarantees = self.g | other.g
+        assumptions = list_union(self.a, other.a)
+        guarantees = list_union(self.g, other.g)
         return IoContract(assumptions, guarantees, self.inputvars, self.outputvars)
diff --git a/src/gear/loaders.py b/src/gear/loaders.py
index 4b8b621f..830b21c3 100644
--- a/src/gear/loaders.py
+++ b/src/gear/loaders.py
@@ -2,7 +2,7 @@
 
 import gear.iocontract as iocontract
 import gear.polyhedralterm as polyhedralterm
-from gear.gear import getVarset
+from gear.gear import getVarlist
 
 
 def readContract(contract):
@@ -25,10 +25,10 @@ def readContract(contract):
         for key in ["assumptions", "guarantees"]:
             reqs.append([polyhedralterm.PolyhedralTerm(term["coefficients"], term["constant"]) for term in c[key]])
         iocont = iocontract.IoContract(
-            inputVars=getVarset(c["InputVars"]),
-            outputVars=getVarset(c["OutputVars"]),
-            assumptions=polyhedralterm.PolyhedralTermSet(set(reqs[0])),
-            guarantees=polyhedralterm.PolyhedralTermSet(set(reqs[1])),
+            inputVars=getVarlist(c["InputVars"]),
+            outputVars=getVarlist(c["OutputVars"]),
+            assumptions=polyhedralterm.PolyhedralTermList(list(reqs[0])),
+            guarantees=polyhedralterm.PolyhedralTermList(list(reqs[1])),
         )
         list_iocontracts.append(iocont)
     if len(list_iocontracts) == 1:
diff --git a/src/gear/polyhedralterm.py b/src/gear/polyhedralterm.py
index aa9e8358..84c34a3b 100644
--- a/src/gear/polyhedralterm.py
+++ b/src/gear/polyhedralterm.py
@@ -13,11 +13,12 @@
 from scipy.optimize import linprog
 
 import gear.iocontract as iocontract
+from gear.utils import *
 
 
 class PolyhedralTerm(iocontract.Term):
     """
-    Polyhedral terms are linear inequalities over a set of variables.
+    Polyhedral terms are linear inequalities over a list of variables.
 
     Usage:
         Polyhedral terms are initialized as follows:
@@ -73,7 +74,7 @@ def __repr__(self):
         return "<Term {0}>".format(self)
 
     def __add__(self, other):
-        varlist = list(self.vars | other.vars)
+        varlist = list_union(self.vars, other.vars)
         variables = {}
         for var in varlist:
             variables[var] = self.get_coefficient(var) + other.get_coefficient(var)
@@ -89,11 +90,11 @@ def vars(self):
 
         Example:
             For the term :math:`ax + by \\le c` with variables :math:`x` and
-            :math:`y`, this function returns the set :math:`\\{x, y\\}` if
+            :math:`y`, this function returns the list :math:`\\{x, y\\}` if
             :math:`a` and :math:`b` are nonzero.
         """
         varlist = self.variables.keys()
-        return set(varlist)
+        return list(varlist)
 
     def contains_var(self, var):
         """
@@ -172,7 +173,7 @@ def get_sign(self, var):
 
     def get_matching_vars(self, variable_polarity):
         """
-        Returns the set of variables whose polarities match the polarities
+        Returns the list of variables whose polarities match the polarities
         requested.
 
         Example:
@@ -200,17 +201,17 @@ def get_matching_vars(self, variable_polarity):
         Returns:
             If all variables in the term match the polarities specified in the
             argument, the routine returns the matching variables.  Otherwise,
-            it returns an empty set.
+            it returns an empty list.
         """
-        variable_set = set()
+        variable_list = list()
         for var in variable_polarity.keys():
             if self.contains_var(var):
                 if (self.get_polarity(var, True) == variable_polarity[var]) or (self.get_coefficient(var) == 0):
-                    variable_set.add(var)
+                    variable_list.add(var)
                 else:
-                    variable_set = set()
+                    variable_list = list()
                     break
-        return variable_set
+        return variable_list
 
     def remove_variable(self, var):
         """
@@ -365,16 +366,16 @@ def polytope_to_term(poly, const, variables):
     @staticmethod
     def solve_for_variables(context, vars_to_elim):
         """
-        Interpret a set of terms as equalities and solve the system of equations
+        Interpret a list of terms as equalities and solve the system of equations
         for the given variables.
 
         Args:
             context:
-                The set of terms to be solved. Each term will be interpreted as
+                The list of terms to be solved. Each term will be interpreted as
                 an equality.
 
             vars_to_elim:
-                The set of variables whose solutions will be sought.
+                The list of variables whose solutions will be sought.
 
         Assumptions: the number of equations matches the number of vars_to_elim
         contained in the terms.
@@ -384,7 +385,7 @@ def solve_for_variables(context, vars_to_elim):
             expressed as PolyhedralTerm instances.
         """
         logging.debug("GetVals: %s Vars: %s", context, vars_to_elim)
-        vars_to_solve = context.vars & vars_to_elim
+        vars_to_solve = list_intersection(context.vars, vars_to_elim)
         assert len(context.terms) == len(vars_to_solve)
         exprs = [PolyhedralTerm.to_symbolic(term) for term in context.terms]
         logging.debug("Solving %s", exprs)
@@ -397,15 +398,15 @@ def solve_for_variables(context, vars_to_elim):
             return {}
 
 
-class PolyhedralTermSet(iocontract.TermSet):
+class PolyhedralTermList(iocontract.TermList):
     """
-    A TermSet of PolyhedralTerm instances.
+    A TermList of PolyhedralTerm instances.
     """
 
     # This routine accepts a term that will be adbuced with the help of other
     # terms The abduction aims to eliminate from the term appearances of the
     # variables contained in vars_to_elim
-    def _transform2(self, context: iocontract.TermSet, vars_to_elim: set, polarity):
+    def _transform2(self, context: iocontract.TermList, vars_to_elim: list, polarity):
         logging.debug("Context terms: %s", context)
         logging.debug("Variables to eliminate: %s", vars_to_elim)
         helpers = context | self
@@ -416,8 +417,8 @@ def _transform2(self, context: iocontract.TermSet, vars_to_elim: set, polarity):
             for var in term.vars & vars_to_elim:
                 vars_elim[var] = term.get_polarity(var, polarity)
             logging.debug("Vars to elim: %s", vars_elim)
-            vars_to_cover = set(vars_elim.keys())
-            terms_to_use = PolyhedralTermSet(set())
+            vars_to_cover = list(vars_elim.keys())
+            terms_to_use = PolyhedralTermList(list())
 
             # now we have to choose from the helpers any terms that we can use
             # to eliminate these variables
@@ -450,68 +451,68 @@ def _transform2(self, context: iocontract.TermSet, vars_to_elim: set, polarity):
 
             logging.debug("After subst: %s", term)
 
-        self.terms = set(term_list)
+        self.terms = list(term_list)
 
         # the last step needs to be a simplification
         logging.debug("Ending transformation with simplification")
         self.simplify(context)
 
-    def _transform(self, context: iocontract.TermSet, vars_to_elim: set, abduce: bool):
+    def _transform(self, context: iocontract.TermList, vars_to_elim: list, abduce: bool):
         logging.debug("Transforming: %s", self)
         logging.debug("Context terms: %s", context)
         logging.debug("Variables to eliminate: %s", vars_to_elim)
         term_list = list(self.terms)
         new_terms = list()
         for term in term_list:
-            helpers = (context | self) - PolyhedralTermSet({term})
+            helpers = (context | self) - PolyhedralTermList({term})
             try:
-                new_term = PolyhedralTermSet.transform_term(term, helpers, vars_to_elim, abduce)
+                new_term = PolyhedralTermList.transform_term(term, helpers, vars_to_elim, abduce)
             except ValueError as e:
                 new_term = term
             new_terms.append(new_term)
 
-        self.terms = set(new_terms)
+        self.terms = list(new_terms)
 
         # the last step needs to be a simplification
         logging.debug("Ending transformation with simplification")
         self.simplify(context)
 
-    def abduce_with_context(self, context: iocontract.TermSet, vars_to_elim: set) -> iocontract.TermSet:
+    def abduce_with_context(self, context: iocontract.TermList, vars_to_elim: list) -> iocontract.TermList:
         """
-        Obtain a set of PolyhedralTerm instances lacking the indicated variables
-        and implying the given TermSet in the given context.
+        Obtain a list of PolyhedralTerm instances lacking the indicated variables
+        and implying the given TermList in the given context.
 
         Example:
-            Suppose the current set of terms is :math:`\\{x + y \\le 6\\}`, the
+            Suppose the current list of terms is :math:`\\{x + y \\le 6\\}`, the
             context is :math:`\\{y \\le 5\\}`, and the abduced terms should not
-            contain variable :math:`y`. Then the current TermSet could be
+            contain variable :math:`y`. Then the current TermList could be
             abduced to :math:`\\{x \\le 1\\}` because :math:`x \\le 1
             \\;\\land\\; y \\le 5 \\Rightarrow x + y \\le 6`.
 
         Args:
             context:
-                The TermSet providing the context for the abduction.
+                The TermList providing the context for the abduction.
 
             vars_to_elim:
                 Variables that should not appear in the abduced term.
 
         Returns:
-            A set of terms not containing any variables in :code:`vars_to_elim`
+            A list of terms not containing any variables in :code:`vars_to_elim`
             and which, in the context provided, imply the terms contained in the
-            calling termset.
+            calling termlist.
         """
-        termset = self.copy()
+        termlist = self.copy()
         logging.debug("Abducing from terms: %s", self)
         logging.debug("Context: %s", context)
         logging.debug("Vars to elim: %s", vars_to_elim)
         try:
-            termset.simplify(context)
+            termlist.simplify(context)
         except ValueError as e:
             raise ValueError(
                 "Provided constraints \n{}\n".format(self) + "are unsatisfiable in context \n{}".format(context)
             ) from e
         try:
-            termset._transform(context, vars_to_elim, True)
+            termlist._transform(context, vars_to_elim, True)
         except ValueError as e:
             raise ValueError(
                 "The elimination of variables \n{}\n".format(vars_to_elim)
@@ -519,44 +520,44 @@ def abduce_with_context(self, context: iocontract.TermSet, vars_to_elim: set) ->
                 + "in context \n{}\n".format(context)
                 + "was not possible"
             ) from e
-        return termset
+        return termlist
 
-    def deduce_with_context(self, context: iocontract.TermSet, vars_to_elim: set) -> iocontract.TermSet:
+    def deduce_with_context(self, context: iocontract.TermList, vars_to_elim: list) -> iocontract.TermList:
         """
-        Obtain a set of PolyhedralTerm instances lacking the indicated variables
-        and implied by the given TermSet in the given context.
+        Obtain a list of PolyhedralTerm instances lacking the indicated variables
+        and implied by the given TermList in the given context.
 
         Example:
-            Suppose the current set of terms is :math:`\\{x - y \\le 6\\}`, the
+            Suppose the current list of terms is :math:`\\{x - y \\le 6\\}`, the
             context is :math:`\\{y \\le 5\\}`, and the deduced terms should not
-            contain variable :math:`y`. Then the current TermSet could be
+            contain variable :math:`y`. Then the current TermList could be
             deduced to :math:`\\{x \\le 11\\}` because :math:`x - y \\le 6
             \\;\\land\\; y \\le 5 \\Rightarrow x \\le 11`.
 
         Args:
             context:
-                The TermSet providing the context for the deduction.
+                The TermList providing the context for the deduction.
 
             vars_to_elim:
                 Variables that should not appear in the deduced term.
 
         Returns:
-            A set of terms not containing any variables in :code:`vars_to_elim`
+            A list of terms not containing any variables in :code:`vars_to_elim`
             and which, in the context provided, are implied by the terms
-            contained in the calling termset.
+            contained in the calling termlist.
         """
-        termset = self.copy()
+        termlist = self.copy()
         logging.debug("Deducing from term %s", self)
         logging.debug("Context: %s", context)
         logging.debug("Vars to elim: %s", vars_to_elim)
         try:
-            termset.simplify(context)
+            termlist.simplify(context)
         except ValueError as e:
             raise ValueError(
                 "Provided constraints \n{}\n".format(self) + "are unsatisfiable in context \n{}".format(context)
             ) from e
         try:
-            termset._transform(context, vars_to_elim, False)
+            termlist._transform(context, vars_to_elim, False)
         except ValueError as e:
             raise ValueError(
                 "The elimination of variables \n{}\n".format(vars_to_elim)
@@ -565,82 +566,82 @@ def deduce_with_context(self, context: iocontract.TermSet, vars_to_elim: set) ->
                 + "was not possible"
             ) from e
         # eliminate terms containing the variables to be eliminated
-        terms_to_elim = termset.get_terms_with_vars(vars_to_elim)
-        termset.terms = termset.terms - terms_to_elim.terms
-        return termset
+        terms_to_elim = termlist.get_terms_with_vars(vars_to_elim)
+        termlist.terms = list_diff(termlist.terms, terms_to_elim.terms)
+        return termlist
 
-    def simplify(self, context=set()) -> None:
+    def simplify(self, context=list()) -> None:
         """
-        Remove redundant terms in the PolyhedralTermSet using the provided
+        Remove redundant terms in the PolyhedralTermList using the provided
         context.
 
         Example:
-            Suppose the TermSet is :math:`\\{x - 2y \\le 5, x - y \\le 0\\}` and
-            the context is :math:`\\{x + y \\le 0\\}`. Then the TermSet could be
+            Suppose the TermList is :math:`\\{x - 2y \\le 5, x - y \\le 0\\}` and
+            the context is :math:`\\{x + y \\le 0\\}`. Then the TermList could be
             simplified to :math:`\\{x - y \\le 0\\}`.
 
         Args:
             context:
-                The TermSet providing the context for the simplification.
+                The TermList providing the context for the simplification.
         """
         logging.debug("Starting simplification procedure")
         logging.debug("Simplifying terms: %s", self)
         logging.debug("Context: %s", context)
-        if isinstance(context, set):
-            variables, self_mat, self_cons, ctx_mat, ctx_cons = PolyhedralTermSet.termset_to_polytope(
-                self, PolyhedralTermSet(context)
+        if isinstance(context, list):
+            variables, self_mat, self_cons, ctx_mat, ctx_cons = PolyhedralTermList.termlist_to_polytope(
+                self, PolyhedralTermList(context)
             )
         else:
-            variables, self_mat, self_cons, ctx_mat, ctx_cons = PolyhedralTermSet.termset_to_polytope(self, context)
+            variables, self_mat, self_cons, ctx_mat, ctx_cons = PolyhedralTermList.termlist_to_polytope(self, context)
         logging.debug("Polytope is \n%s", self_mat)
         try:
-            a_red, b_red = PolyhedralTermSet.reduce_polytope(self_mat, self_cons, ctx_mat, ctx_cons)
+            a_red, b_red = PolyhedralTermList.reduce_polytope(self_mat, self_cons, ctx_mat, ctx_cons)
         except ValueError as e:
             raise ValueError(
                 "The constraints \n{}\n".format(self) + "are unsatisfiable in context \n{}".format(context)
             ) from e
         logging.debug("Reduction: \n%s", a_red)
-        self.terms = PolyhedralTermSet.polytope_to_termset(a_red, b_red, variables).terms
+        self.terms = PolyhedralTermList.polytope_to_termlist(a_red, b_red, variables).terms
         logging.debug("Back to terms: \n%s", self)
 
-    def refines(self, other: PolyhedralTermSet) -> bool:
+    def refines(self, other: PolyhedralTermList) -> bool:
         """
         Tells whether the argument is a larger specification, i.e., compute self
         <= other.
 
         Args:
             other:
-                TermSet against which we are comparing self.
+                TermList against which we are comparing self.
         """
         logging.debug("Verifying refinement")
         logging.debug("LH term: %s", self)
         logging.debug("RH term: %s", other)
-        variables, self_mat, self_cons, ctx_mat, ctx_cons = PolyhedralTermSet.termset_to_polytope(self, other)
+        variables, self_mat, self_cons, ctx_mat, ctx_cons = PolyhedralTermList.termlist_to_polytope(self, other)
         logging.debug("Polytope is \n%s", self_mat)
-        result = PolyhedralTermSet.verify_polytope_containment(self_mat, self_cons, ctx_mat, ctx_cons)
+        result = PolyhedralTermList.verify_polytope_containment(self_mat, self_cons, ctx_mat, ctx_cons)
         return result
 
     @staticmethod
-    def termset_to_polytope(terms: PolyhedralTermSet, context: PolyhedralTermSet):
+    def termlist_to_polytope(terms: PolyhedralTermList, context: PolyhedralTermList):
         """
-        Converts a set of terms with its context into matrix-vector pairs.
+        Converts a list of terms with its context into matrix-vector pairs.
 
         Example:
-            Suppose the set of terms is :math:`\\{x+y \\le 1, x - y \\le 4\\}`
+            Suppose the list of terms is :math:`\\{x+y \\le 1, x - y \\le 4\\}`
             and the context is :math:`\\{x + 4w \\le 5\\}`. The routine extracts
             all variables and generates an order for them, say, :math:`[x, w,
             y]`. Then the routine returns matrix-vector pairs for both the terms
-            TermSet and the context. It returns :math:`A = \\left(
+            TermList and the context. It returns :math:`A = \\left(
             \\begin{smallmatrix} 1 & 0 & 1 \\\\ 1 &0 &-1
             \\end{smallmatrix}\\right)` and :math:`b = \\left(
             \\begin{smallmatrix} 1 \\\\ 4 \\end{smallmatrix}\\right)` for the
-            current TermSet and :math:`A_{c} = \\left( \\begin{smallmatrix} 1 &
+            current TermList and :math:`A_{c} = \\left( \\begin{smallmatrix} 1 &
             4 & 0 \\end{smallmatrix}\\right)` and :math:`b_c = \\left(
             \\begin{smallmatrix} 5 \\end{smallmatrix}\\right)` for the context.
 
         Args:
             terms:
-                Set of terms to convert to matrix-vector form.
+                list of terms to convert to matrix-vector form.
             context:
                 Context terms to convert to matrix-vector form.
 
@@ -648,7 +649,7 @@ def termset_to_polytope(terms: PolyhedralTermSet, context: PolyhedralTermSet):
             A tuple :code:`variables, A, b, a_h, b_h` consisting of the variable
             order and the matrix-vector pairs for the terms and the context.
         """
-        variables = list(terms.vars | context.vars)
+        variables = list(list_union(terms.vars,context.vars))
         a = []
         b = []
         for term in terms.terms:
@@ -674,9 +675,9 @@ def termset_to_polytope(terms: PolyhedralTermSet, context: PolyhedralTermSet):
         return variables, a, b, a_h, b_h
 
     @staticmethod
-    def polytope_to_termset(matrix, vector, variables: list[iocontract.Var]) -> PolyhedralTermSet:
+    def polytope_to_termlist(matrix, vector, variables: list[iocontract.Var]) -> PolyhedralTermList:
         """
-        Transforms a matrix-vector pair into a PolyhedralTermSet, assuming that
+        Transforms a matrix-vector pair into a PolyhedralTermList, assuming that
         the variable coefficients in the matrix are ordered as specified.
 
         Args:
@@ -689,7 +690,7 @@ def polytope_to_termset(matrix, vector, variables: list[iocontract.Var]) -> Poly
                 of the matrix.
 
         Returns:
-            The PolyhedralTermSet corresponding to the given data.
+            The PolyhedralTermList corresponding to the given data.
         """
         term_list = []
         logging.debug("&&&&&&&&&&")
@@ -706,7 +707,7 @@ def polytope_to_termset(matrix, vector, variables: list[iocontract.Var]) -> Poly
             const = vector[i]
             term = PolyhedralTerm.polytope_to_term(row, const, variables)
             term_list.append(term)
-        return PolyhedralTermSet(set(term_list))
+        return PolyhedralTermList(list(term_list))
 
     @staticmethod
     def reduce_polytope(a: np.array, b: np.array, a_help: np.array = np.array([[]]), b_help: np.array = np.array([])):
@@ -762,7 +763,8 @@ def reduce_polytope(a: np.array, b: np.array, a_help: np.array = np.array([[]]),
                 b_opt = b_temp
             res = linprog(c=objective, A_ub=a_opt, b_ub=b_opt, bounds=(None, None))  # ,options={'tol':0.000001})
             b_temp[i] -= 1
-            logging.debug("Optimal value: %s", -res["fun"])
+            if res["fun"]:
+                logging.debug("Optimal value: %s", -res["fun"])
             logging.debug("Results: %s", res)
             # if res["success"] and -res["fun"] <= b_temp[i]:
             if res["status"] != 2 and -res["fun"] <= b_temp[i]:
@@ -796,10 +798,10 @@ def verify_polytope_containment(
                 Vector of H-representation of polytope on RHS of inequality.
         """
         # If the LHS is empty, it is a refinement
-        if PolyhedralTermSet.is_polytope_empty(a_l, b_l):
+        if PolyhedralTermList.is_polytope_empty(a_l, b_l):
             return True
         # If the RHS is empty, but not the LHS, not a refinement
-        if PolyhedralTermSet.is_polytope_empty(a_r, b_r):
+        if PolyhedralTermList.is_polytope_empty(a_r, b_r):
             return False
         # If no side is empty, check whether the RHS terms are included in the
         # LHS
@@ -858,9 +860,9 @@ def is_polytope_empty(a: np.array, b: np.array) -> bool:
             return True
 
     @staticmethod
-    def get_kaykobad_context(term: PolyhedralTerm, context: PolyhedralTermSet, vars_to_elim: set, abduce: bool):
-        forbidden_vars = list(vars_to_elim & term.vars)
-        other_forbibben_vars = vars_to_elim - term.vars
+    def get_kaykobad_context(term: PolyhedralTerm, context: PolyhedralTermList, vars_to_elim: list, abduce: bool):
+        forbidden_vars = list_intersection(vars_to_elim, term.vars)
+        other_forbibben_vars = list_diff(vars_to_elim, term.vars)
         n = len(forbidden_vars)
         matrix_row_terms = list()
         partial_sums = [0.0] * n
@@ -872,7 +874,7 @@ def get_kaykobad_context(term: PolyhedralTerm, context: PolyhedralTermSet, vars_
         for i, i_var in enumerate(forbidden_vars):
             row_found = False
             logging.debug("Iterating for variable %s", i_var)
-            for context_term in context.terms - set(matrix_row_terms):
+            for context_term in list_diff(context.terms, matrix_row_terms):
                 logging.debug("Analyzing context term %s", context_term)
                 if context_term == term:
                     next
@@ -915,34 +917,33 @@ def get_kaykobad_context(term: PolyhedralTerm, context: PolyhedralTermSet, vars_
                         logging.debug("Failed third matrix-vector verification")
                         break
                 if not term_is_invalid:
-                    matrix_contains_others = matrix_contains_others or len(context_term.vars - set(forbidden_vars)) > 0
+                    matrix_contains_others = matrix_contains_others or len(list_diff(context_term.vars, forbidden_vars)) > 0
                     row_found = True
                     for j in range(n):
                         partial_sums[j] += residuals[j]
                     matrix_row_terms.append(context_term)
                     break
             if not row_found:
-                logging.debug("Hola")
                 raise ValueError("Could not find the {}th row of matrix".format(i))
-        if (not matrix_contains_others) and len(term.vars - vars_to_elim) == 0:
+        if (not matrix_contains_others) and len(list_diff(term.vars, vars_to_elim)) == 0:
             logging.debug("Hola2")
             raise ValueError("Found context will produce empty transformation")
         logging.debug("Matrix row terms %s", matrix_row_terms)
         return matrix_row_terms, forbidden_vars
 
     @staticmethod
-    def transform_term(term: PolyhedralTerm, context: PolyhedralTermSet, vars_to_elim: set, abduce: bool):
+    def transform_term(term: PolyhedralTerm, context: PolyhedralTermList, vars_to_elim: list, abduce: bool):
         logging.debug("Transforming term: %s", term)
         logging.debug("Context: %s", context)
         try:
-            matrix_row_terms, forbidden_vars = PolyhedralTermSet.get_kaykobad_context(
+            matrix_row_terms, forbidden_vars = PolyhedralTermList.get_kaykobad_context(
                 term, context, vars_to_elim, abduce
             )
         except ValueError as e:
             logging.debug("Could not transform %s", term)
             raise ValueError("Could not transform term {}".format(term)) from e
-        matrix_row_terms = PolyhedralTermSet(set(matrix_row_terms))
-        sols = PolyhedralTerm.solve_for_variables(matrix_row_terms, set(forbidden_vars))
+        matrix_row_terms = PolyhedralTermList(list(matrix_row_terms))
+        sols = PolyhedralTerm.solve_for_variables(matrix_row_terms, list(forbidden_vars))
 
         result = term.copy()
         for var in sols.keys():
diff --git a/src/gear/utils.py b/src/gear/utils.py
new file mode 100644
index 00000000..74622ccc
--- /dev/null
+++ b/src/gear/utils.py
@@ -0,0 +1,15 @@
+"""
+A set of helper routines.
+"""
+
+
+def list_intersection(list1, list2):
+    return [el for el in list1 if el in list2]
+
+def list_diff(list1, list2):
+    return [el for el in list1 if not(el in list2)]
+
+def list_union(list1, list2):
+    return list1 + [el for el in list2 if not(el in list1)]
+
+    
\ No newline at end of file


Test patch:
diff --git a/tests/test_polyhedral_terms.py b/tests/test_polyhedral_terms.py
index ce5a46f8..6c525f14 100644
--- a/tests/test_polyhedral_terms.py
+++ b/tests/test_polyhedral_terms.py
@@ -3,7 +3,7 @@
 from sympy.parsing.sympy_parser import parse_expr
 
 from gear.iocontract import Var
-from gear.polyhedralterm import PolyhedralTerm, PolyhedralTermSet
+from gear.polyhedralterm import PolyhedralTerm, PolyhedralTermList
 
 
 def to_pt(str_rep):
@@ -31,7 +31,7 @@ def to_pt(str_rep):
 
 def to_pts(str_rep_list):
     terms = [to_pt(str_rep) for str_rep in str_rep_list]
-    return PolyhedralTermSet(set(terms))
+    return PolyhedralTermList(terms)
 
 
 def test_polyhedral_abduce_1():