1(* Copyright (c) 2010 Tjark Weber. All rights reserved. *) 2 3structure QbfTrace = 4struct 5 6 (* possible values: 7 0 - no output at all (except for fatal errors) 8 1 - warnings only 9 2 - also diagnostic messages of constant length 10 3 - also diagnostic messages that are potentially lengthy (e.g., terms, 11 models, proofs) 12 4 - moreover, temporary files (for communication with the QBF solver) are 13 not removed after solver invocation *) 14 val trace = ref 2 15 16 val _ = Feedback.register_trace ("HolQbfLib", trace, 4) 17 18end 19