using System.Console using Nemerle.Collections using Nemerle.Utility using Nemerle.Logging using Nemerle.Imperative using Nemerle.Profiling set namespace Fx7 public class Driver internal mutable static PrintResult : bool internal mutable static Verbose : bool internal mutable static NoStats : bool internal mutable static NoProgress : bool internal mutable static LogAfter : int internal mutable static LoggingEnabled : bool = true internal mutable static SimplifySyntax : bool internal mutable static ExpectAllValid : bool internal mutable static ExpectAllInvalid : bool internal mutable static PrettyPrint : bool internal mutable static Mechanical : bool internal mutable static Translate : bool internal mutable static SmtStartNo : int internal mutable static CsvName : string = null internal mutable static Strategies : list [int] // = [3] internal mutable static DoubleCheck : int = 0 [Option ("Display profile information")] \ Profile = true [Option ("Dump statistics for quantifier instantiations")] \ DumpQuantStats = false [Option ("Display additional quantifier information")] \ VerboseQuant = false [Option ("Use DPLL(T) solver")] DPLL = true [Option] SatLevels = 2 [Option] EnableLinearTheory = true [Option] EnableTcTheory = true [Option] EnableArrayTheory = false [Option ("Allow at most N instantiation rounds in the quantifier loop")] \ MaxInstRounds = 12 [Option ("Allow at most N iterations in the quantifier loop")] \ MaxQuantIters = 500 [Option ("Allow at most N conflicts to be extracted from one monome")] \ MaxMultiRefutations = 5 MaxInstancesPerCheapRound = 30000 [Option] TimeLimit = 0 [Option] InstanceBumpMult = 0.5 [Option] TheoryBumpMult = 1.1 [Option] QuantTheoryBumpMult = 0.8 [Option] InstanceBump = 0.1 [Option] TheoryBump = 10.0 [Option] BaseBump = 100.0 [Option] InstantatiateEvery = 0 [Option] ImportantOnlyIters = 1 [Option] ImportantOnlyStep = 2 [Option] SelfChecks = false [Option] DumpSkol = false // matcher flags [Option] FlatMatching = true [Option] SimplifyMatching = false [Option] IncrementalSimplifyMatching = false [Option] LastMerge = false [Option] FnLastMerge = false // cannot be set to true currently! // Grinder flags [Option] EqProp = true [Option] GrindForall = false [Option] RealCNFThreshold = 5 // SMT translation [Option] SmtComment = "" [Option ("Display information about monomes taking more than N seconds to prove")] \ HardMonomeLimit = 10000 [Option] IgnoreTriggers = false [Option] LoopTest = true [Option] MultiRefutation = false [Option] QuantInstances = true [Option] ImportantQuantOpt = true [Option] NewLiteralExplanation = true [Option] SubtriggerMatcher = true [Option] MinimizeConflictClause = false [Option] ImportantOnce = false [Option] DetectTc = true [Option] SortQuery = false [Option] UseLevels = true [Option] InstanceLife = 3 [Option] LogConflicts = "" // dumps [Option] DumpImportantQuant = false internal mutable static Instance : Driver mutable static axiom_files : list [string] = [] internal mutable static file_name : string = "stdin" mutable static cmd_line_options : string class TimeoutException : System.Exception {} start_time : int end_time : int // used by Run and stats only mutable cnf_converter : ExternalCNF // ForParser and Run mutable core : Core mutable result : string mutable status : string #region stats internal mutable clause_count : int internal mutable last_stat_at_tick : int = System.Environment.TickCount internal mutable last_stat_at_iter : int mutable quant_loop_start : int mutable quant_loop_start_instances : int problem_name : string internal sizes : array [long] = array (4) total_sizes : array [long] = array (4) [AutoStats] num_main_iters : int [AutoStats] num_quant_loops : int [AutoStats] num_quant_iters : int [AutoStats] instance_count : int [AutoStats] num_inst_rounds : int [AutoStats] max_inst_rounds : int [AutoStats] max_instances_per_round : int [AutoStats] max_quant_iters : int [AutoStats] num_noskips : int [AutoStats] num_asserts : int [AutoStats] num_clauses : int [AutoStats] num_matchings : int [AutoStats] total_main_monome_size : int [AutoStats] total_quant_monome_size : int [AutoStats] total_monome_size : int [AutoStats] DPLL_saved_monome_size : int [AutoStats] subtrigger_hits : int [AutoStats] subtrigger_misses : int [AutoStats] num_merges : int [AutoStats] num_non_unit_merges : int [AutoStats] num_merge_hits : int [AutoStats] num_merge_misses : int [AutoStats] subtrigger_sub_misses : int [AutoStats] subtrigger_sub_hits : int [AutoStats] subtrigger_anything : int [AutoStats] subtrigger_nothing : int [AutoStats] subtrigger_flats : int // both filled by the AutoStats macro [AutoStats] internal GetStats () : list [string * string] {} internal class StatsRec { } [ProfDump] static DumpProf () : void {} #region prover option book-keeping static RegisterOptions () : void { // filled by [Options] macros } static Parse (s : string, o : ref bool) : void match (s) | "1" | "t" | "true" | "True" => o = true | "0" | "f" | "false" | "False" => o = false | _ => throw FatalError ($"invalid format for boolean option: `$s'") static Parse (s : string, o : ref int) : void o = int.Parse (s) static Parse (s : string, o : ref double) : void o = double.Parse (s) static Parse (s : string, o : ref string) : void o = s static TypeName (_ : ref string) : string "string" static TypeName (_ : ref double) : string "double" static TypeName (_ : ref bool) : string "bool" static TypeName (_ : ref int) : string "int" [Record] \ class TheOption public Name : string public Aliases : list [string] public Description : string public Setter : string -> void static options : Hashtable [string, TheOption] = Hashtable () static mutable option_list : list [TheOption] = [] static AddOption (opt : TheOption) : void foreach (name in opt.Name :: opt.Aliases) options [name.ToLower ().Replace ("_", "")] = opt option_list ::= opt static DescribeOptions () : string def res = System.Text.StringBuilder () foreach (opt in option_list.Rev ()) _ = res.AppendFormat (" {0,-25} {1}\n", opt.Name, opt.Description) res.ToString () static SetOptions (s : string) : void foreach (o in s.Split (',')) def spl = o.Split ('=') if (spl.Length != 2) throw FatalError ($"invalid option format: `$o'") else def name = spl [0].ToLower ().Replace ("_", "") if (options.Contains (name)) options [name].Setter (spl [1]) else throw FatalError ($"unknown option name: `$(spl[0])'") static this () RegisterOptions () #endregion mutable usersys_time = 0 mutable peak_memory = 0 ReadProcStats () : void when (System.IO.File.Exists ("/proc/self/stat") && System.IO.File.Exists ("/proc/self/status")) def lines = System.IO.File.ReadAllLines ("/proc/self/stat") def words = lines [0].Substring (lines [0].LastIndexOf (") ") + 2).Split (' ') def user = int.Parse (words [11]) def sys = int.Parse (words [12]) mutable vmpk = 0 foreach (l in System.IO.File.ReadAllLines ("/proc/self/status")) when (l.StartsWith ("VmPeak:")) vmpk = int.Parse (l.Substring (8).Replace ("kB", "")) usersys_time = (user + sys) * 10 peak_memory = vmpk DumpStats () : void unless (NoStats) def running_time = System.Environment.TickCount - start_time def running_time = if (running_time == 0) 1 else running_time def time (t) string.Format ("{0:0.00}s", t / 1000.0) def csv_time (t) string.Format ("{0:0.00}", t / 1000.0) ReadProcStats () def cpu_usage = usersys_time * 100 / running_time WriteLine ("*** STATS ***") WriteLine ($ "running time [$problem_name]: $(time(running_time)) / $(time(usersys_time)) $(cpu_usage)% CPU $(peak_memory) kB") def totals = GetStats () foreach ((n, v) in totals) WriteLine ("{0,40} : {1}", n, v) WriteLine ($ "clause count: $clause_count") def line = CSV.Line ( file_name, problem_name, csv_time (running_time), csv_time (usersys_time), cpu_usage, status, result, cmd_line_options); def line = line + $[v | (_, v) in totals] when (CsvName != null) when (!System.IO.File.Exists (CsvName)) CSV.WriteFile (CsvName, [["File name", "Problem", "Time", "user/sys time", "% CPU", "Status", "Result", "Cmd line"] + $[ n | (n, _) in totals ]], append = true) CSV.WriteFile (CsvName, [line], append = true) WriteLine (ReportSizes (num_quant_iters, total_sizes)) when (Profile) DumpProf () when (DumpQuantStats) core.TermPool.DumpStats () static public mutable LogPrefix : string = "" static public DoLog (msg : string) : void System.Console.WriteLine (LogPrefix + msg) ReportSizes (every : int, sz : array [long]) : string def nz (n : long) if (n == 0) -1L else n def every = nz (every) mutable s = string.Format ("sizes:{0,5} ", sz [0] / every) for (mutable i = 1; i < sz.Length; ++i) s += string.Format ("{0,5} ({1,2}%)", sz [i] / every, sz [i] * 100 / nz (sz [i - 1])) s #endregion internal CheckTimeout () : void when (end_time != 0 && System.Environment.TickCount > end_time) result = "TIMEOUT" log (ANSWER, "TIMEOUT") throw TimeoutException () public this (name = "") problem_name = name when (TimeLimit != 0) end_time = TimeLimit * 1000 + System.Environment.TickCount start_time = System.Environment.TickCount core = Core (this) internal QuantCallback () : bool CheckTimeout () num_quant_iters++ if (CheckMqi (num_quant_iters - quant_loop_start, instance_count - quant_loop_start_instances)) true else when (!Verbose) StatLine () false internal mutable CurMaxInstRounds : int = 12 internal mutable CurMaxQuantIters : int = 500 internal mutable CurLimitLow : bool internal mutable CurMaxInstances = int.MaxValue internal SetQuantLimits (low : bool) : void CurLimitLow = low def div = if (low) 3 else 1 CurMaxInstRounds = MaxInstRounds / div CurMaxQuantIters = MaxQuantIters / div CurMaxInstances = if (low) MaxInstancesPerCheapRound else int.MaxValue internal CheckMir (iters : int) : bool when (iters > max_inst_rounds) max_inst_rounds = iters if (CurMaxInstRounds != 0 && iters >= CurMaxInstRounds) unless (CurLimitLow) result = $"hit mir=$MaxInstRounds" log (INFO, $"hit mir=$MaxInstRounds") true else false internal CheckMqi (iters : int, instances : int) : bool when (iters > max_quant_iters) max_quant_iters = iters if (CurMaxQuantIters != 0 && iters >= CurMaxQuantIters) unless (CurLimitLow) result = $"hit mqi=$MaxQuantIters" log (INFO, $"hit mqi=$MaxQuantIters") true else if (instances > CurMaxInstances) true else false internal StartQuantLoop () : void quant_loop_start = num_quant_iters quant_loop_start_instances = instance_count internal StatLine () : void when (System.Environment.TickCount - last_stat_at_tick > 500) def every = (num_main_iters + num_quant_iters) - last_stat_at_iter last_stat_at_tick = System.Environment.TickCount last_stat_at_iter = num_main_iters + num_quant_iters when (!NoStats && !NoProgress) def s = string.Format ("\ri: {0,-4}+{1,-4}/{2,-4} t:{3,7:0.00}s ", num_main_iters, num_quant_iters, instance_count, (System.Environment.TickCount - start_time) / 1000.0) Write (s + ReportSizes (every, sizes) + " \r") for (mutable i = 0; i < sizes.Length; ++i) total_sizes [i] += sizes [i] sizes [i] = 0 internal MainLoopCallback () : void CheckTimeout () num_main_iters++ LoggingEnabled = num_main_iters >= LogAfter when (!Verbose) StatLine () [Profile] \ public Run (formula : Term) : bool def grinder = Grinder (core) def formula = grinder.Skolemize (formula) when (DPLL) def d = DPLLSolver (core, this) return d.Search (formula) // when (Verbose) // WriteLine ($ "formula: $formula") cnf_converter = ExternalCNF (core, null) cnf_converter.AssertFormula (formula) // XXX while (true) MainLoopCallback () when (!cnf_converter.Solve ()) // XXX when (Verbose) WriteLine ("unsatisfable") return false // XXX def lits = cnf_converter.GetMonome () // XXX when (Verbose) WriteLine ($"possibly satisfable,\nlits: $lits") total_main_monome_size += lits.Length match (core.GetConflicts (lits, leave_open = true)) // XXX | [] => when (Verbose) WriteLine ("theories OK!") def ql = QuantLoop (core, lits, cnf_converter) if (ql.Run ()) when (Verbose) WriteLine ("quantifiers say: conflict") else when (PrintResult) WriteLine ($"result:\n$lits") return true // XXX | lst => cnf_converter.AddConflicts (lst) // XXX true // not reached static mutable error_cnt = 0 static ForParser (parser : Parser) : void when (SmtStartNo > 0) SmtStartNo = 1 LoggingEnabled = 0 >= LogAfter foreach (ax in axiom_files.Rev ()) parser.ReadAxioms (ax) def write (s : string) if (Mechanical) log (INFO, s) else Write (s) mutable cnt = 0 def run (cmd, mkform, expect_sat, expect_unsat) ++cnt def d = Driver (cmd.name) Instance = d d.core.PlainPredicates = parser.PlainPredicates def formula = mkform (d.core) def end = if (NoStats) "" else "\n" if (Translate) return else if (expect_sat) write ($ "ExpectSAT [$(cmd.name)]...\n") d.status = "SAT" else if (expect_unsat) write ($ "ExpectUnSAT [$(cmd.name)]...\n") d.status = "UNSAT" else write ($ "CheckSAT [$(cmd.name)]...\n") d.status = "unknown" try def sat = d.Run (formula) when (DoubleCheck > 0) d.core.DoubleCheck () if ((expect_sat && !sat) || (expect_unsat && sat)) error_cnt++ if (Mechanical) log (ERR, "wrong answer") else write ("\n\x1b[31;1mwrong answer\x1b[0m\n\n") when (d.result == null) d.result = "wrong answer" else if (expect_sat || expect_unsat) if (Mechanical) log (INFO, "correct answer") else write (end + $ "\x1b[32;1mOK\x1b[0m, SAT=$sat (i=$(d.instance_count))\n") d.result = $"OK:SAT=$sat" else unless (Mechanical) write ($"\nok, SAT=$sat\n") d.result = $"OK:SAT=$sat" d.DumpStats () catch | _ is TimeoutException => d.DumpStats () if (Driver.Mechanical) log (INFO, "not exiting after timeout") else System.Environment.Exit (3) foreach (c in parser.Run ()) | CheckSAT (f) => run (c, f, false, false) | ExpectSAT (f) => run (c, f, true, false) | ExpectUnSAT (f) => run (c, f, false, true) | Pragma ([opt, val]) => def opt = opt.ToLower ().Replace ("_", "") if (options.Contains (opt)) try options [opt].Setter (val) log (INFO, $"set $opt := $val") catch | _ => log (WARN, $"error setting $opt := $val") else log (WARN, $ "no such option $opt (args $val)") | Pragma (lst) => log (WARN, $ "unknown pragma ignored: $lst") public static mutable alloc_block : string public static Main () : int mutable help_opts = [] def print_help () WriteLine (Getopt.Usage (help_opts)) WriteLine ("Exit codes:\n" "0 - OK\n" "1 - wrong answer\n" "2 - FatalError exception\n" "3 - timeout\n" "4 - other exception\n" "5 - non-UTVPI/non-linear\n" ) System.Environment.Exit (0) mutable files = [] cmd_line_options = System.Environment.CommandLine def opts = [ Getopt.CliOption.Flag (name = "-verbose", aliases = ["-v"], help = "Be noisy", handler = fun () { Verbose = true }), Getopt.CliOption.Flag (name = "-verbose-quant", aliases = ["-vq"], help = "Be noisy about quantifiers", handler = fun () { VerboseQuant = true }), Getopt.CliOption.Flag (name = "-smt", aliases = [], help = "Translate input to SMT-LIB format", handler = fun () { Translate = true }), Getopt.CliOption.Int (name = "-smt-no", aliases = [], help = "Start numerating SMT-LIB dumps with INT", handler = fun (n) { Translate = true; SmtStartNo = n }), Getopt.CliOption.Flag (name = "-print-result", aliases = ["-p"], help = "Print the final assignment", handler = fun () { PrintResult = true }), Getopt.CliOption.Int (name = "-time-limit", aliases = ["-t"], help = "Time limit in seconds", handler = fun (i) { TimeLimit = i }), Getopt.CliOption.Int (name = "-log-after", aliases = [], help = "Enable logging only during and after iteration INT", handler = fun (i) { LogAfter = i }), Getopt.CliOption.Flag (name = "-no-stats", aliases = ["-n"], help = "Disable stats", handler = fun () { NoStats = true }), Getopt.CliOption.Flag (name = "-no-progress", aliases = ["-npb"], help = "Disable progress display", handler = fun () { NoProgress = true }), Getopt.CliOption.Flag (name = "-simplify-syntax", aliases = ["-s"], help = "Use Simplify's syntax.", handler = fun () { SimplifySyntax = true }), Getopt.CliOption.String (name = "-axioms", aliases = ["-ax"], help = "Read axioms from specified file.", handler = fun (s) { axiom_files ::= s }), Getopt.CliOption.Flag (name = "-expect-all-valid", aliases = ["-valid"], help = "Expect all formulas to be valid.", handler = fun () { ExpectAllValid = true }), Getopt.CliOption.Flag (name = "-expect-all-invalid", aliases = ["-invalid"], help = "Expect all formulas to be invalid.", handler = fun () { ExpectAllInvalid = true }), Getopt.CliOption.Flag (name = "-mechanical", aliases = ["-M"], help = "Use machine-readable output, supress stats.", handler = fun () { NoStats = true; NoProgress = true; Mechanical = true }), Getopt.CliOption.String (name = "-options", aliases = ["-o", "-opt"], help = "Set search options, possible options are:\n" + DescribeOptions (), handler = SetOptions), Getopt.CliOption.Flag (name = "-no-profile", aliases = ["-np"], help = "Don't display profile data", handler = fun () { Profile = false }), Getopt.CliOption.Int (name = "-doublecheck", aliases = ["-dc"], help = "Check theory conflict clauses again (INT times)", handler = fun (x) { DoubleCheck = x }), Getopt.CliOption.Flag (name = "-pretty-print", aliases = ["-pp"], help = "Display the first formula pretty printed, using Unicode", handler = fun () { PrettyPrint = true }), Getopt.CliOption.Int (name = "-alloc", aliases = [], help = "Voodoo", handler = fun (x) { alloc_block = string ('x', x) }), Getopt.CliOption.String (name = "-csv-name", aliases = [], help = "Set the name of the CSV stats file", handler = fun (x) { CsvName = x }), Getopt.CliOption.String (name = "-strategies", aliases = ["-st"], help = "List of strategy numbers to try, like 1,2", handler = fun (x) { Strategies = $[int.Parse (k) | k in x.Split (',', ';', ' ', ':')] }), Getopt.CliOption.Flag (name = "-help", aliases = ["-h"], help = "Display this usage message and exit", handler = print_help), Getopt.CliOption.NonOption (name = "", help = "Specify file to check (omit to use stdin)", handler = fun (s) { files ::= s }) ] try help_opts = opts Getopt.Parse (opts) match (files) | [] => ForParser (Parser ()) | xs => foreach (x in xs.Rev ()) file_name = x ForParser (Parser (x)) if (error_cnt == 0) log (INFO, "All tests passed.") 0 else log (INFO, $ "$error_cnt tests failed.") 1 catch | e is FatalError => def msg = e.Message log (ERR, $ "Fatal error: $msg") if (msg.IndexOf ("not UTVPI") != -1 || msg.IndexOf ("non-linear subterm") != -1) 5 else 2 | e => log (ERR, $ "Internal Prover Error:\n$e") 4