th_util.ml1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43(******************************************************************************) (* *) (* The Alt-Ergo theorem prover *) (* Copyright (C) 2006-2013 *) (* *) (* Sylvain Conchon *) (* Evelyne Contejean *) (* *) (* Francois Bobot *) (* Mohamed Iguernelala *) (* Stephane Lescuyer *) (* Alain Mebsout *) (* *) (* CNRS - INRIA - Universite Paris Sud *) (* *) (* This file is distributed under the terms of the Apache Software *) (* License version 2.0 *) (* *) (* ------------------------------------------------------------------------ *) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) (* Copyright (C) 2013-2018 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of the Apache Software *) (* License version 2.0 *) (* *) (******************************************************************************) type answer = (Explanation.t * Expr.Set.t list) option type theory = | Th_arith | Th_sum | Th_adt | Th_arrays | Th_UF type lit_origin = | Subst | CS of theory * Numbers.Q.t | NCS of theory * Numbers.Q.t | Other