schema s1 : t schema s2 : t constraints c1 : s1 constraints c2 : s2 query q : s1 -> s2 ---------------------------------- command (check_query q c1 c2)