to the preamble of a .smt2 (HORN) format query, after which
all bindings of the form (n Apple) are represented in smt as int and support numeric ops
comparisons of the form n == m where n and m are differentnumeric sorts should be wrapped with an int cast , so written as (n:int) == m
The goal is to allow more fine-grained distinction between binders in qualifier instantiation (e.g. write qualifiers that only compare someint not any of (many) params that may be int as may happen when you have a kvar with many "plain" int params with qualifiers which also have many int params.
This PR allows one to add a declaration
to the preamble of a
.smt2(HORN) format query, after which(n Apple)are represented in smt asintand support numeric opsn == mwherenandmare differentnumericsorts should be wrapped with anintcast , so written as(n:int) == mThe goal is to allow more fine-grained distinction between binders in qualifier instantiation (e.g. write qualifiers that only compare some
intnot any of (many) params that may beintas may happen when you have a kvar with many "plain"intparams with qualifiers which also have manyintparams.