module Shostak: sig end
Inference system for Shostak theories.
Author(s): Harald Ruess
module type T = sig end
A Shostak theory th is specified by means of a replacement map f a for replacing uninterpreted
subterms of a with f a and canonizing the result, and, a solver solve. , an extended canonizer map f a for replacing uninterpreted
positions x of a with f b followed by canonization in the
given theory, and, a branching function disjunction. If disjunction always returns Not_found,
then th is also said to be a convex Shostak theory.
module Make: functor (Sh : T) -> sig end
Constructing an inference system from a Shostak theory Th.