You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Panic(Any { .. })
Provable: 0 / 1
thread 'main' (7565) panicked at /home/og/.cargo/git/checkouts/z3.rs-23fd15daebefed96/2551894/z3/src/ast.rs:630:1:
assertion failed: !ast.is_null()
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
Suspected fix
I suspect the panic is related to a mismatch between the scope permutation logic and the substitution logic in Unify.
The permutation logic appears to rebuild the permuted variables according to the source/left scope order only. However, when extending the right-hand substitution, the permuted variable list should be reconstructed according to the target/right scope order.
qed-proverwill panic when proving equivalence between two different relational encodings of TPCH Q2.Input contains two representations of TPCH Q2:
$SCALAR_QUERY(MIN(...))representationThe prover should return
ProvableorNotProvable, but instead it panics.Input
{ "schemas": [ { "types": [ "INTEGER", "INTEGER", "INTEGER", "REAL", "VARCHAR" ], "nullable": [ false, false, false, false, false ], "name": "tpch.partsupp", "guaranteed": [], "fields": [ "ps_partkey", "ps_suppkey", "ps_availqty", "ps_supplycost", "ps_comment" ], "key": [] }, { "types": [ "INTEGER", "VARCHAR", "VARCHAR", "VARCHAR", "VARCHAR", "INTEGER", "VARCHAR", "REAL", "VARCHAR" ], "nullable": [ false, false, false, false, false, false, false, false, false ], "name": "tpch.part", "guaranteed": [], "fields": [ "p_partkey", "p_name", "p_mfgr", "p_brand", "p_type", "p_size", "p_container", "p_retailprice", "p_comment" ], "key": [] }, { "types": [ "INTEGER", "VARCHAR", "VARCHAR" ], "nullable": [ false, false, true ], "name": "tpch.region", "guaranteed": [], "fields": [ "r_regionkey", "r_name", "r_comment" ], "key": [] }, { "types": [ "INTEGER", "VARCHAR", "INTEGER", "VARCHAR" ], "nullable": [ false, false, false, true ], "name": "tpch.nation", "guaranteed": [], "fields": [ "n_nationkey", "n_name", "n_regionkey", "n_comment" ], "key": [] }, { "types": [ "INTEGER", "VARCHAR", "VARCHAR", "INTEGER", "VARCHAR", "REAL", "VARCHAR" ], "nullable": [ false, false, false, false, false, false, false ], "name": "tpch.supplier", "guaranteed": [], "fields": [ "s_suppkey", "s_name", "s_address", "s_nationkey", "s_phone", "s_acctbal", "s_comment" ], "key": [] } ], "queries": [ { "sort": { "offset": null, "limit": { "type": "INTEGER", "operand": [], "operator": "100" }, "source": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 8, "type": "INTEGER" }, { "column": 9, "type": "INTEGER" } ], "operator": "=" }, "left": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 7, "type": "INTEGER" }, { "column": 8, "type": "INTEGER" } ], "operator": "=" }, "left": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 2, "type": "INTEGER" }, { "column": 3, "type": "INTEGER" } ], "operator": "=" }, "left": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "type": "BOOLEAN", "operand": [ { "column": 0, "type": "INTEGER" }, { "column": 5, "type": "INTEGER" } ], "operator": "=" }, { "type": "BOOLEAN", "operand": [ { "column": 4, "type": "REAL" }, { "column": 6, "type": "REAL" } ], "operator": "=" } ], "operator": "AND" }, "left": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 0, "type": "INTEGER" }, { "column": 5, "type": "INTEGER" } ], "operator": "=" }, "left": { "scan": 0 }, "kind": "INNER", "right": { "project": { "source": { "filter": { "condition": { "type": "BOOLEAN", "operand": [ { "type": "BOOLEAN", "operand": [ { "type": "VARCHAR", "operand": [ { "column": 4, "type": "VARCHAR" } ], "operator": "CAST" }, { "type": "VARCHAR", "operand": [], "operator": "'SMALL%'" } ], "operator": "LIKE" }, { "type": "BOOLEAN", "operand": [ { "column": 5, "type": "INTEGER" }, { "type": "INTEGER", "operand": [], "operator": "15" } ], "operator": "=" } ], "operator": "AND" }, "source": { "scan": 1 } } }, "target": [ { "column": 0, "type": "INTEGER" }, { "column": 2, "type": "VARCHAR" } ] } } } }, "target": [ { "column": 5, "type": "INTEGER" }, { "column": 6, "type": "VARCHAR" }, { "column": 0, "type": "INTEGER" }, { "column": 1, "type": "INTEGER" }, { "column": 3, "type": "REAL" } ] } }, "kind": "INNER", "right": { "project": { "source": { "project": { "source": { "group": { "keys": [ { "column": 0, "type": "INTEGER" } ], "function": [ { "operator": "MIN", "operand": [ { "column": 1, "type": "REAL" } ], "distinct": false, "ignoreNulls": true, "type": "REAL" } ], "source": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 0, "type": "INTEGER" }, { "column": 3, "type": "INTEGER" } ], "operator": "=" }, "left": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 5, "type": "INTEGER" }, { "column": 0, "type": "INTEGER" } ], "operator": "=" }, "left": { "filter": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 1, "type": "VARCHAR" }, { "type": "VARCHAR", "operand": [], "operator": "'EUROPE '" } ], "operator": "=" }, "source": { "scan": 2 } } }, "kind": "INNER", "right": { "scan": 3 } } }, "target": [ { "column": 3, "type": "INTEGER" } ] } }, "kind": "INNER", "right": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 2, "type": "INTEGER" }, { "column": 3, "type": "INTEGER" } ], "operator": "=" }, "left": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 0, "type": "INTEGER" }, { "column": 5, "type": "INTEGER" } ], "operator": "=" }, "left": { "scan": 0 }, "kind": "SEMI", "right": { "project": { "source": { "filter": { "condition": { "type": "BOOLEAN", "operand": [ { "type": "BOOLEAN", "operand": [ { "type": "VARCHAR", "operand": [ { "column": 4, "type": "VARCHAR" } ], "operator": "CAST" }, { "type": "VARCHAR", "operand": [], "operator": "'SMALL%'" } ], "operator": "LIKE" }, { "type": "BOOLEAN", "operand": [ { "column": 5, "type": "INTEGER" }, { "type": "INTEGER", "operand": [], "operator": "15" } ], "operator": "=" } ], "operator": "AND" }, "source": { "scan": 1 } } }, "target": [ { "column": 0, "type": "INTEGER" } ] } } } }, "target": [ { "column": 0, "type": "INTEGER" }, { "column": 3, "type": "REAL" }, { "column": 1, "type": "INTEGER" } ] } }, "kind": "INNER", "right": { "project": { "source": { "scan": 4 }, "target": [ { "column": 0, "type": "INTEGER" }, { "column": 3, "type": "INTEGER" } ] } } } }, "target": [ { "column": 0, "type": "INTEGER" }, { "column": 1, "type": "REAL" }, { "column": 4, "type": "INTEGER" } ] } } } }, "target": [ { "column": 1, "type": "INTEGER" }, { "column": 2, "type": "REAL" } ] } } } }, "target": [ { "column": 1, "type": "REAL" }, { "column": 0, "type": "INTEGER" } ] } }, "target": [ { "column": 1, "type": "INTEGER" }, { "column": 0, "type": "REAL" } ] } } } }, "target": [ { "column": 0, "type": "INTEGER" }, { "column": 1, "type": "VARCHAR" }, { "column": 3, "type": "INTEGER" } ] } }, "kind": "INNER", "right": { "scan": 4 } } }, "target": [ { "column": 0, "type": "INTEGER" }, { "column": 1, "type": "VARCHAR" }, { "column": 8, "type": "REAL" }, { "column": 4, "type": "VARCHAR" }, { "column": 5, "type": "VARCHAR" }, { "column": 7, "type": "VARCHAR" }, { "column": 9, "type": "VARCHAR" }, { "column": 6, "type": "INTEGER" } ] } }, "kind": "INNER", "right": { "scan": 3 } } }, "target": [ { "column": 0, "type": "INTEGER" }, { "column": 1, "type": "VARCHAR" }, { "column": 2, "type": "REAL" }, { "column": 3, "type": "VARCHAR" }, { "column": 4, "type": "VARCHAR" }, { "column": 5, "type": "VARCHAR" }, { "column": 6, "type": "VARCHAR" }, { "column": 9, "type": "VARCHAR" }, { "column": 10, "type": "INTEGER" } ] } }, "kind": "INNER", "right": { "filter": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 1, "type": "VARCHAR" }, { "type": "VARCHAR", "operand": [], "operator": "'EUROPE '" } ], "operator": "=" }, "source": { "scan": 2 } } } } }, "target": [ { "column": 2, "type": "REAL" }, { "column": 3, "type": "VARCHAR" }, { "column": 7, "type": "VARCHAR" }, { "column": 0, "type": "INTEGER" }, { "column": 1, "type": "VARCHAR" }, { "column": 4, "type": "VARCHAR" }, { "column": 5, "type": "VARCHAR" }, { "column": 6, "type": "VARCHAR" } ] } }, "collation": [ [ 0, "REAL", "DESCENDING" ], [ 2, "VARCHAR", "ASCENDING" ], [ 1, "VARCHAR", "ASCENDING" ], [ 3, "INTEGER", "ASCENDING" ] ] } }, { "sort": { "offset": null, "limit": { "type": "INTEGER", "operand": [], "operator": "100" }, "source": { "project": { "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "type": "BOOLEAN", "operand": [ { "column": 23, "type": "INTEGER" }, { "column": 25, "type": "INTEGER" } ], "operator": "=" }, { "type": "BOOLEAN", "operand": [ { "type": "BOOLEAN", "operand": [ { "column": 5, "type": "INTEGER" }, { "type": "INTEGER", "operand": [], "operator": "15" } ], "operator": "=" }, { "type": "BOOLEAN", "operand": [ { "type": "VARCHAR", "operand": [ { "column": 4, "type": "VARCHAR" } ], "operator": "CAST" }, { "type": "VARCHAR", "operand": [], "operator": "'SMALL%'" } ], "operator": "LIKE" }, { "type": "BOOLEAN", "operand": [ { "column": 26, "type": "VARCHAR" }, { "type": "VARCHAR", "operand": [], "operator": "'EUROPE '" } ], "operator": "=" }, { "type": "BOOLEAN", "operand": [ { "column": 19, "type": "REAL" }, { "type": "REAL", "operand": [], "operator": "$SCALAR_QUERY", "query": { "aggregate": { "function": [ { "operator": "MIN", "operand": [ { "column": 31, "type": "REAL" } ], "distinct": false, "ignoreNulls": true, "type": "REAL" } ], "source": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "type": "BOOLEAN", "operand": [ { "column": 42, "type": "INTEGER" }, { "column": 44, "type": "INTEGER" } ], "operator": "=" }, { "type": "BOOLEAN", "operand": [ { "column": 45, "type": "VARCHAR" }, { "type": "VARCHAR", "operand": [], "operator": "'EUROPE '" } ], "operator": "=" } ], "operator": "AND" }, "left": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 36, "type": "INTEGER" }, { "column": 40, "type": "INTEGER" } ], "operator": "=" }, "left": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 29, "type": "INTEGER" }, { "column": 33, "type": "INTEGER" } ], "operator": "=" }, "left": { "filter": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 0, "type": "INTEGER" }, { "column": 28, "type": "INTEGER" } ], "operator": "=" }, "source": { "scan": 0 } } }, "kind": "INNER", "right": { "scan": 4 } } }, "kind": "INNER", "right": { "scan": 3 } } }, "kind": "INNER", "right": { "scan": 2 } } } } } } ], "operator": "=" } ], "operator": "AND" } ], "operator": "AND" }, "left": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "column": 12, "type": "INTEGER" }, { "column": 21, "type": "INTEGER" } ], "operator": "=" }, "left": { "join": { "condition": { "type": "BOOLEAN", "operand": [ { "type": "BOOLEAN", "operand": [ { "column": 0, "type": "INTEGER" }, { "column": 16, "type": "INTEGER" } ], "operator": "=" }, { "type": "BOOLEAN", "operand": [ { "column": 9, "type": "INTEGER" }, { "column": 17, "type": "INTEGER" } ], "operator": "=" } ], "operator": "AND" }, "left": { "join": { "condition": { "type": "BOOLEAN", "operand": [], "operator": "true" }, "left": { "scan": 1 }, "kind": "INNER", "right": { "scan": 4 } } }, "kind": "INNER", "right": { "scan": 0 } } }, "kind": "INNER", "right": { "scan": 3 } } }, "kind": "INNER", "right": { "scan": 2 } } }, "target": [ { "column": 14, "type": "REAL" }, { "column": 10, "type": "VARCHAR" }, { "column": 22, "type": "VARCHAR" }, { "column": 0, "type": "INTEGER" }, { "column": 2, "type": "VARCHAR" }, { "column": 11, "type": "VARCHAR" }, { "column": 13, "type": "VARCHAR" }, { "column": 15, "type": "VARCHAR" } ] } }, "collation": [ [ 0, "REAL", "DESCENDING" ], [ 2, "VARCHAR", "ASCENDING" ], [ 1, "VARCHAR", "ASCENDING" ], [ 3, "INTEGER", "ASCENDING" ] ] } } ], "help": [ "native: root=Limit, targetlist=8", "optimized: root=Limit, targetlist=8" ] }##output
The original prover output is a panic:
Suspected fix
I suspect the panic is related to a mismatch between the scope permutation logic and the substitution logic in Unify.
The permutation logic appears to rebuild the permuted variables according to the source/left scope order only. However, when extending the right-hand substitution, the permuted variable list should be reconstructed according to the target/right scope order.
Observed behavior after local experimental fix