The CachingSymbolicPool was added so that Symbolic variables could be shared between states after they forked. The SimpleSymbolicPool does not share symbolic variables between states after they forked. Sharing Symbolic variables would in principle reduce memory usage and might enable more solver caching hits.
Unfortunately the current implementation is broken and therefore disabled
It works correctly on this example (both states share the same symbolic version of y after forking).
procedure main()
{
var x:int;
var y:int;
if ( x > 0 )
{
assert x == x;
}
else
{
assume x == x;
}
havoc y;
assume x != y;
}
but it fails with this example.
procedure main()
{
var x:int;
var y:int;
if ( x > 0 )
{
havoc y;
}
else
{
havoc y;
}
havoc y;
assume x != y;
}
The problem in the second example is that the havoc y commands inside the if and else branch should return the same symbolic in each state but in the existing implementation they don't. The current implementation makes the mistake of trying to use a symbolic creation site as a key for caching symbolics. Really what we need to cache on is just the variable itself.
The
CachingSymbolicPoolwas added so that Symbolic variables could be shared between states after they forked. TheSimpleSymbolicPooldoes not share symbolic variables between states after they forked. Sharing Symbolic variables would in principle reduce memory usage and might enable more solver caching hits.Unfortunately the current implementation is broken and therefore disabled
It works correctly on this example (both states share the same symbolic version of
yafter forking).but it fails with this example.
procedure main() { var x:int; var y:int;
}
The problem in the second example is that the havoc y commands inside the if and else branch should return the same symbolic in each state but in the existing implementation they don't. The current implementation makes the mistake of trying to use a symbolic creation site as a key for caching symbolics. Really what we need to cache on is just the variable itself.