[CN] Simplified Constraints in state file are not fully simplified

[elaustell]

I struggled to find a minimal model to show this, so I'll just show a picture of the output I'm getting.

It's not important to understand, but the point is that there are extremely long terms in this constraint which do not have to be so long. Under terms it shows what some sub terms simplify to, so I manually have to go in and substitute those simplifications in myself. This work is very tedious and seems like it can be automated.

To try to make things a bit clearer with this example, you can note that the unproven constraint includes the term unpack_Own_Forwards0.n.data. Under terms, it can be seen that unpack_Own_Forwards0.n.data has the value 0i32. I can't see a good reason why the unsimplified constraint needs this long term that could just be simplified to 0i32.

Sorry that this is a bit confusing to understand, I'm happy to try to clarify anything.

[dc-mak]

Potentially related: #351 though in this case it's not specific to each guards.

Tl;dr yes that output is atrocious and the term simplifier needs work. Perhaps even just with pretty printing.

Do you have some sort of recursive constraint of some sort like function (boo) foo(u32 x) { x == 0i32 ? 0i32 : foo(x-1u32); }?

[elaustell]

Potentially related: #351 though in this case it's not specific to each guards.

Tl;dr yes that output is atrocious and the term simplifier needs work. Perhaps even just with pretty printing.

Do you have some sort of recursive constraint of some sort like function (boo) foo(u32 x) { x == 0i32 ? 0i32 : foo(x-1u32); }?

I have recursive predicates, which is the Own_Forwards and Own_Backwards. They have an if null(n) then return Nil else recursive call.

[peterohanley]

I have a nice small example from #533

void readex(char* tmp)
/*@
  requires take a1 = each(u64 j; 0u64 <= j && j < 1u64) { Owned<char>(array_shift<char>(tmp,j)) };
  ensures take a2 = each(u64 j; 0u64 <= j && j < 1u64) { Owned<char>(array_shift<char>(tmp,j)) };
@*/
{
    return;
}

int tmp()
{
    char tmp[2]={'H', 'i'};
    readex(tmp);
    return 1;
}

Available resources
...
each(u64 j; 0'u64 <= j && j < 2'u64 && !(true && 0'u64 <= j && j < 1'u64)) {Owned<char>(&tmp + j * 1'u64)}(const(default(u8))[0'u64 = 72'u8 /* 0x48 */][1'u64 = 105'u8 /* 0x69 */])

This should simplify that each condition into 1 <= j && j < 2 I think

[yav]

We probably want to keep going and just simplify this to j = 1, and the perhaps even remove the each, and specialize the Owned with j = 1.

[peterohanley]

Is there a situation where the problem is a missing extract and removing the each would mislead the user about what should be done? Displaying errors is long after this would affect the calculation but I'm nervous about removing a semantically idempotent wrapper in what is basically debug info.