using Nemerle.Logging using Nemerle.Profiling [assembly: ProfSetup (Divisor = 1000, GetTime = Core.read_tsc (), TimeType = long)] [assembly: LogCondition (Fx7.Driver.LoggingEnabled)] [assembly: LogFormat (PrependFlag)] [assembly: LogFunction (Fx7.Driver.DoLog)] [assembly: LogFlag (CNF, 0)] // ToCNF.n [assembly: LogFlag (CNFQ, 0)] // ToCNF.n [assembly: LogFlag (TC, 0)] // TcTheory.n [assembly: LogFlag (CNT, 0)] // UtvpiTheory.n [assembly: LogFlag (CORE, 0)] // Core.n [assembly: LogFlag (COREV, 0)] // Core.n [assembly: LogFlag (MATCH, 0)] // Term.Matcher.n [assembly: LogFlag (SMATCH, 0)] // Term.Matcher.n [assembly: LogFlag (PARSER, 0)] // Parser.n (not used) [assembly: LogFlag (QUANT, 0)] // QuantLoop.n [assembly: LogFlag (SAT, 0)] // SatSolver.n [assembly: LogFlag (TERM, 0)] // Term.n [assembly: LogFlag (SUBT, 0)] // SubTrigger.n [assembly: LogFlag (MSAT, 0)] // Term.n [assembly: LogFlag (VTERM, 0)] // Term.n, more [assembly: LogFlag (DPLL, 0)] // DPLLSolver.n [assembly: LogFlag (QDPLL, 0)] // QuantDPLLSolver.n [assembly: LogFlag (DPLLO, 0)] // DPLLSolver.n :: VarOrder [assembly: LogFlag (LIN, 0)] // LinearTheory.n [assembly: LogFlag (ARR, 0)] // ArrayTheory.n [assembly: LogFlag (CONFL, 0)] // SimpleSolver.n [assembly: LogFlag (SIMPL, 0)] // SimpleSolver.n [assembly: LogFlag (VSIMPL, 0)] // SimpleSolver.n [assembly: LogFlag (PROG, 0)] // SimpleSolver.n [assembly: LogFlag (GRIND, 1)] // Grind.n [assembly: LogFlag (COQ, 0)] // Coq.n [assembly: LogFlag (APROOF, 0)] // ArithProofs.n [assembly: LogFlag (PRUNE, 0)] // Pruner.n [assembly: LogFlag (INFO, 1)] // general information [assembly: LogFlag (WARN, 1)] // warnings [assembly: LogFlag (ERR, 1)] // errors [assembly: LogFlag (ANSWER, 1)] // answers to commands [assembly: LogFlag (TEMP, 1)] // for debugging, not in release