[Feature request] Sorted contract pretty printing

[NicolasRouquette]

Is your feature request related to a problem? Please describe. A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]

It is difficult to read non-trivial contracts because the variables and terms are unsorted.

Describe the solution you'd like A clear and concise description of what you want to happen.

A contract pretty printer that sorts variables by names and terms by the variables involved.

Describe alternatives you've considered A clear and concise description of any alternative solutions or features you've considered.

Additional context Add any other context or screenshots about the feature request here.

Here is an example of a contract:

InVars: [t1_entry, t1_var, duration1, soc1_entry, t2_var, duration2, t3_var, duration3]
OutVars:[soc1_var, soc2_var, soc3_var, output_t2, output_soc2, output_t3, output_soc3, output_t1, output_soc1]
A: [
  -duration3 <= 0
  duration1 + duration2 + t1_entry - t3_var <= 0
  -duration2 <= 0
  duration1 + t1_entry - t2_var <= 0
  -duration1 <= 0
  -t1_entry <= 0
  t1_entry - t1_var <= 0
  -soc1_entry <= 0
  soc1_entry <= 100
]
G: [
  0.8 duration1 + soc1_entry <= 100
  duration1 - output_t1 + t1_entry = 0
  0.5 duration1 - output_soc1 + soc1_entry <= 0
  -0.8 duration1 + output_soc1 - soc1_entry <= 0
  soc1_entry - soc1_var - 0.5 t1_entry + 0.5 t1_var <= 0
  -soc1_entry + soc1_var + 0.8 t1_entry - 0.8 t1_var <= 0
  -output_t1 + t1_var <= 0
  -output_soc1 + soc1_var <= 0
  0.4 duration2 - output_soc1 <= 0
  duration2 + output_t1 - output_t2 = 0
  0.3 duration2 - output_soc1 + output_soc2 <= 0
  -0.4 duration2 + output_soc1 - output_soc2 <= 0
  -output_soc1 - 0.3 output_t1 + soc2_var + 0.3 t2_var <= 0
  output_soc1 + 0.4 output_t1 - soc2_var - 0.4 t2_var <= 0
  -output_t2 + t2_var <= 0
  output_soc2 - soc2_var <= 0
  0.2 duration3 - output_soc2 <= 0
  duration3 + output_t2 - output_t3 = 0
  0.1 duration3 - output_soc2 + output_soc3 <= 0
  -0.2 duration3 + output_soc2 - output_soc3 <= 0
  -output_soc2 - 0.1 output_t2 + soc3_var + 0.1 t3_var <= 0
  output_soc2 + 0.2 output_t2 - soc3_var - 0.2 t3_var <= 0
  -output_t3 + t3_var <= 0
  output_soc3 - soc3_var <= 0
]

The above is difficult to follow because:

• the variables are unsorted; e.g., how many duration* variables are there?
• the terms are unsorted; e.g., how many terms involve variable duration2?

Here is a proposal:

def show_contract(c: PolyhedralContract) -> str:

    def polyhedral_term_key(t: PolyhedralTerm) -> str:
        return ','.join(sorted([v.name for v in t.vars]))

    buff=""
    inputs=sorted([v.name for v in c.inputvars])
    buff += "Inputs : ["+','.join(inputs)+"]\n"
    outputs=sorted([v.name for v in c.outputvars])
    buff += "Outputs: ["+','.join(outputs)+"]\n"
    a = sorted(c.a.terms, key=polyhedral_term_key)
    buff += "A: "+'\n\t'.join([str(PolyhedralTermList(a))])+"\n"
    g = sorted(c.g.terms, key=polyhedral_term_key)
    buff += "G: "+'\n\t'.join([str(PolyhedralTermList(g))])+"\n"

    return buff

With this function, the above contract shows like this:

Inputs : [duration1,duration2,duration3,soc1_entry,t1_entry,t1_var,t2_var,t3_var]
Outputs: [output_soc1,output_soc2,output_soc3,output_t1,output_t2,output_t3,soc1_var,soc2_var,soc3_var]
A: [
  -duration1 <= 0
  duration1 + duration2 + t1_entry - t3_var <= 0
  duration1 + t1_entry - t2_var <= 0
  -duration2 <= 0
  -duration3 <= 0
  -soc1_entry <= 0
  soc1_entry <= 100
  -t1_entry <= 0
  t1_entry - t1_var <= 0
]
G: [
  0.5 duration1 - output_soc1 + soc1_entry <= 0
  -0.8 duration1 + output_soc1 - soc1_entry <= 0
  duration1 - output_t1 + t1_entry = 0
  0.8 duration1 + soc1_entry <= 100
  0.4 duration2 - output_soc1 <= 0
  0.3 duration2 - output_soc1 + output_soc2 <= 0
  -0.4 duration2 + output_soc1 - output_soc2 <= 0
  duration2 + output_t1 - output_t2 = 0
  0.2 duration3 - output_soc2 <= 0
  0.1 duration3 - output_soc2 + output_soc3 <= 0
  -0.2 duration3 + output_soc2 - output_soc3 <= 0
  duration3 + output_t2 - output_t3 = 0
  -output_soc1 - 0.3 output_t1 + soc2_var + 0.3 t2_var <= 0
  output_soc1 + 0.4 output_t1 - soc2_var - 0.4 t2_var <= 0
  -output_soc1 + soc1_var <= 0
  -output_soc2 - 0.1 output_t2 + soc3_var + 0.1 t3_var <= 0
  output_soc2 + 0.2 output_t2 - soc3_var - 0.2 t3_var <= 0
  output_soc2 - soc2_var <= 0
  output_soc3 - soc3_var <= 0
  -output_t1 + t1_var <= 0
  -output_t2 + t2_var <= 0
  -output_t3 + t3_var <= 0
  soc1_entry - soc1_var - 0.5 t1_entry + 0.5 t1_var <= 0
  -soc1_entry + soc1_var + 0.8 t1_entry - 0.8 t1_var <= 0
]

[iincer]

This sounds useful. We should have a name that indicates that the contract is being printed in an ordered fashion, but this should not be default behavior of the print function, because two contracts could have the same "ordered print" representation, yet have different internal representations, potentially yielding different results in later processing. Perhaps the function show_contract could have an ordered Boolean argument to control this--with default value False. This way, the user would always explicitly state that the contract is being ordered.

[iincer]

Hi @NicolasRouquette, I see that this function was implemented as part fo the space mission case study. Would you like to add this to PolyhedralContract?