using Nemerle using Nemerle.Utility using Nemerle.Logging using Nemerle.Collections using Nemerle.Imperative using Nemerle.Profiling set namespace Fx7 public enum ClauseKind | Current = 0 | Conflict = 1 | Pending = 2 [CreateMemento] \ public class SimpleSolver core : Core pool : Term.Pool driver : Driver internal mutable current_level = 0 [Copy] mutable current_clauses : list [Clause] = [] [Copy] mutable pending_clauses : list [Clause] = [] [Copy] mutable active_qatoms : list [QAtom] = [] [Copy] mutable matching_depth : int = 1 [Copy] mutable checked_matching_depth : int = 1 [Copy] mutable rollback_queue : list [Literal] = [] [Copy] mutable trail : list [Literal] = [] [Copy] mutable conflict_cnt : int [Copy] mutable current_conflicts : list [Clause] = [] mutable conflicts : list [Clause] = [] mutable is_sat : bool mutable sat_context : list [Literal] mutable num_conflicts_at_last_restart : int mutable lev0_size : int mutable proof_root : Clause #region theory bookkeeping (push, pop, rollbacks, ctor) public QueueRollback (t : Literal) : void rollback_queue ::= t public PushState () : void current_level++ when (current_level <= 2) lev0_size = trail.Length SaveMemento () rollback_queue = [] //Driver.LogPrefix = string (' ', current_level * 2) public PopState () : void current_level-- foreach (r in rollback_queue) r.Rollback () RestoreMemento () if (Driver.MixConflicts) current_clauses = conflicts.FirstN (conflicts.Length - conflict_cnt) + current_clauses else current_conflicts = conflicts.FirstN (conflicts.Length - conflict_cnt) + current_conflicts conflict_cnt = conflicts.Length refinement_enabled = true //Driver.LogPrefix = string (' ', current_level * 2) public this (c : Core, d : Driver) ResetScores () global_mult = 1.0 core = c pool = c.TermPool c.LiteralPool = this driver = d prev_stats = Driver.StatsRec (driver) core.OnPush += PushState core.OnPop += PopState #endregion #region Assert + expand Expand (kind : ClauseKind, l : Literal) : void def kind = if (Driver.LeakConflictExpansions) ClauseKind.Current else kind when (!l.IsExpanded [kind] && !l.IsNeg) l.IsExpanded [kind] = true def p = l.atom :> PAtom def clauses = p.GetDefiningClauses (l.IsNeg) log (VSIMPL, $ "expand $l -> $clauses") match (kind) | Current => current_clauses = clauses + current_clauses refinement_enabled = true | Conflict => current_conflicts = clauses + current_conflicts refinement_enabled = true | _ => assert (false) [Profile] \ Assert (kind : ClauseKind, l : Literal, reason : Clause, is_case_split : bool, skip_expand = false) : void log (SIMPL, $ "assert $l") // $(System.Environment.StackTrace)") // we require the literal to be part of the clause, except in case of // post-case-split subsumption, where we want the negation of the literal // to be there mutable ok = false foreach (l' in reason.Lits) when (l' === l) ok = true when (is_case_split && skip_expand && l' === ~l) ok = true assert (ok) if (l.IsTrue) when (!skip_expand && !l.IsExpanded [kind]) Expand (kind, l) else if (l.IsFalse) assert (!is_case_split) foreach (l in reason.Lits) assert (l.IsFalse) //log (TEMP, $"ref: $reason") ClauseIsFalse (reason) else trail ::= l l.MakeTrue (is_case_split, reason) unless (skip_expand) Expand (kind, l) match (l.atom) | _ is PAtom => {} | q is QAtom => if (l.IsNeg) def skol = ~q.Skolemize () def c = MakeHelperClause ([q.PosLit, skol], Rule.Skolemize ()) Assert (kind, skol, c, is_case_split = false) else if (q.Vars is []) def skol = q.Skolemize () // really just take the formula inside def c = MakeHelperClause ([q.NegLit, skol], Rule.Instantiate ()) Assert (kind, skol, c, is_case_split = false) else matching_enabled = true active_qatoms ::= q | _ => matching_enabled = true core.Assert (l) refinement_enabled = true #endregion #region instantiation clause_cache : Hashtable [list [Literal], Clause] = Hashtable () [Profile] \ MakeHelperClause (lits : list [Literal], rule : Rule) : Clause unless (clause_cache.Contains (lits)) clause_cache [lits] = core.MakeClause (lits.ToArray (), rule) clause_cache [lits] HighRankingQAtoms () : list [QAtom] if (Driver.MaxHighRankingQA == 0) null else mutable cnt_non_zero = 0 foreach (a in active_qatoms) def s = a.Score when (s > 0) cnt_non_zero++ if (cnt_non_zero < Driver.MinHighRankingQA) null else def scores = array (cnt_non_zero) mutable i = 0 foreach (a in active_qatoms) def s = a.Score when (s > 0) scores [i] = s i++ System.Array.Sort (scores) i = scores.Length - Driver.MaxHighRankingQA when (i < 0) i = 0 def min_score = scores [i] $[a | a in active_qatoms, a.Score >= min_score] [Profile] \ KeepInstClause (kind : ClauseKind, c : Clause) : bool KeepClause (kind, c, no_proxies = true, plunge = true) [Profile] \ AssertInst (kind : ClauseKind, l : Literal, reason : Clause, is_case_split : bool, skip_expand = false) : void Assert (kind, l, reason, is_case_split, skip_expand) mutable high_ranking_promotion_countdown : int = Driver.HighRankingPromotion [Profile] \ Instantiate (last_resort = false) : void if (checked_matching_depth > Driver.MatchingDepth) MarkSat ("matching depth exceeded") else full_instantiation_countdown-- def atoms = if (last_resort || full_instantiation_countdown < 0) full_instantiation_countdown = Driver.FullInstantiationEvery active_qatoms else def tmp = HighRankingQAtoms () if (tmp == null) full_instantiation_countdown = Driver.FullInstantiationEvery active_qatoms else tmp def restricted = !(active_qatoms === atoms) if (restricted) when (high_ranking_promotion_countdown > 0) high_ranking_promotion_countdown-- else full_instantiations_since_matching_depth++ //log (TEMP, $"inst, $matching_depth") Term.Matcher.Start (pool, restricted) driver.num_inst_rounds++ def matchers = array (atoms.Length) def results = array (matchers.Length) mutable i = 0 foreach (a in atoms) matchers [i] = Term.Matcher (a) matchers [i].Prepare () i++ for (i = 0; i < results.Length; ++i) def m = matchers [i] results [i] = (m.Qatom, m.Run ()) mutable did = false def _prev = driver.instance_count foreach ((atom, instances) in results) //log (SIMPL, $"for: $atom, prev=$prev, inst=$instances") assert (atom.PosLit.IsTrue) foreach (t in instances) did = true def l = core.TermToLiteral (matching_depth, t) when (core.Refuted) return //log (TEMP, $"instance: $atom -> $l") log (SIMPL, $"instance: $atom -> $l") driver.instance_count++ def inst_clause = MakeHelperClause ([atom.NegLit, l], Rule.Instantiate ()) match (l.atom) | p is PAtom => mutable kind = ClauseKind.Pending foreach (c in p.GetDefiningClauses (l.IsNeg)) when (KeepInstClause (ClauseKind.Pending, c)) when (core.Refuted) return if ((high_ranking_promotion_countdown != 0 && restricted) || c.Promoted > promoted_threshold) //log (TEMP, $"promote: $c") current_clauses ::= c refinement_enabled = true kind = ClauseKind.Current else pending_clauses ::= c AssertInst (kind, l, inst_clause, is_case_split = false, skip_expand = true) | _ => AssertInst (ClauseKind.Pending, l, inst_clause, is_case_split = false) unless (did) driver.num_empty_inst_rounds++ Term.Matcher.Stop (pool) log (PROG, $"did instantiation, restricted=$restricted, $(driver.instance_count - _prev) instances") #endregion #region conflict analisis #region conflict logging variant ConflictLogEntry | String s : string | Clause c : Fx7.Clause mutable conflict_log_entries : list [ConflictLogEntry] = [] conflicts_log : System.IO.StreamWriter = if (Driver.LogConflicts != "") log (INFO, $ "opening conflict log file: $(Driver.LogConflicts)") def sw = System.IO.File.CreateText (Driver.LogConflicts) sw.Write ($ "; starting conflict log for $(Driver.file_name)\n") sw else null LogConflictComment (s : string) : void assert (conflicts_log != null) conflict_log_entries ::= ConflictLogEntry.String (s) LogConflict (c : Clause) : void assert (conflicts_log != null) conflict_log_entries ::= ConflictLogEntry.String ($[l.atom.MinDepth | l in c.Lits].ToString ()) conflict_log_entries ::= ConflictLogEntry.Clause (c) prev_stats : Driver.StatsRec ConflictTime () : string def s = prev_stats s.MakeDelta () def res = string.Format ("{0:0.00}Mcyc, ", s.tsc / 1_000_000.0) + $ "lev $current_level, $(s.num_case_splits) spl, $(s.num_asserts) asserts, " + $ "$(s.num_matchings) mtchs => $(s.instance_count) inst. in $(s.num_inst_rounds) rds" s.SaveNow () res MaybeProofRoot (c : Clause) : void when (current_level <= 2) assert (proof_root == null) def rule = AnalyzeConflict (_ => true, c) proof_root = Clause (array [], rule) #endregion #region scoring mutable pos_lit_score : double mutable neg_lit_score : double mutable depth_bonus : double mutable global_mult : double ResetScores () : void pos_lit_score = Driver.PosLitScore neg_lit_score = Driver.NegLitScore depth_bonus = Driver.DepthBonus global_mult = 1.0 IncreaseScores () : void pos_lit_score *= Driver.ScoreMult neg_lit_score *= Driver.ScoreMult depth_bonus *= Driver.ScoreMult global_mult *= Driver.ScoreMult when (global_mult > 1e300) def mult = 1.0 / global_mult ResetScores () foreach (c in core.all_atoms) c.PosLit.Score *= mult c.NegLit.Score *= mult Rescale () : void mutable max = 0.0 foreach (c in core.all_clauses) when (c.Score > max) max = c.Score def mult = if (max == 0.0) 1.0 else 1 / max foreach (c in core.all_clauses) c.Score *= mult mutable promoted_threshold = 1 BumpScores (proof : Clause) : void //def levs = Hashtable () def bump (l : Literal, score) l.Score += pos_lit_score * score (~l).Score += neg_lit_score * score //if (levs.Contains (score)) levs[score]++ //else levs[score] = 1 def c = l.Reason c.Score++ when (c.Score > 30) Rescale () c.Promoted = promoted_threshold + Driver.PromoteBackLog if (l.IsCaseSplit) None () else Some (score * Driver.DeepConflictMult) //else Some (score + 1) IncreaseScores () _ = AnalyzeConflict (bump, 1.0, proof) promoted_threshold++ //mutable res = [] //foreach (i in [0 .. 20000]) // if (levs.Contains (i)) res ::= levs [i] // else break //log (TEMP, $"bump scores, $(proof.Length) $(res.Rev())") #endregion AnalyzeConflict (fn : Literal -> bool, proof : Clause) : Rule AnalyzeConflict ((l, _) => if (fn (l)) Some (null) else None (), null, proof) AnalyzeConflict['a] (fn : Literal * 'a -> option ['a], ini : 'a, initial : Clause) : Rule def q = Queue () def seen = Hashtable () mutable steps = [] foreach (l in initial.Lits) q.Add ((~l, ini)) log (SIMPL, $"analyze: $initial") while (!q.IsEmpty) def (l, v) = q.Take () when (seen.Contains (l)) continue seen [l] = true log (SIMPL, $"lit $l / $(l.IsTrue) $(l.IsFalse)") assert (l.IsTrue) match (fn (l, v)) | Some (v) => assert (!l.IsCaseSplit) when (Driver.ProofLogging) steps ::= (l, l.Reason) log (SIMPL, $"reason lit $l -> $(l.Reason)") foreach (l' in l.Reason.Lits) if (l' === l) {} else assert (l'.IsFalse) unless (seen.Contains (~l')) q.Add ((~l', v)) | None => {} if (Driver.ProofLogging) Rule.Resolution (initial, steps) else null SaveConflicts () : void when (conflicts_log != null) def loop (_ : list [ConflictLogEntry]) | String (s) :: Clause (c) :: rest \ | Clause (c) :: rest with s = "" => conflicts_log.Write ($ "(not (and ; $s (final score: $(c.Score), usefulness: $(c.Usefulness))\n") foreach (l in c.Lits) conflicts_log.Write ($" $(~l)\n") conflicts_log.Write ("))\n") loop (rest) | String (s) :: rest => conflicts_log.Write ($"; $s\n") loop (rest) | [] => {} loop (conflict_log_entries.Rev ()) conflicts_log.Close () AddConflictClause (clause : Clause, msg : string) : void driver.conflicts_attempted++ clause.Promoted = promoted_threshold + Driver.PromoteBackLog if (List.ContainsRef (conflicts, clause)) log (CONFL, $"failed to add: $msg/$clause") else log (CONFL, $"add conflict: $msg: $($[l.atom.MinDepth | l in clause.Lits]) $clause") driver.conflicts_added++ when (conflicts_log != null) LogConflictComment (msg) LogConflict (clause) conflicts ::= clause BuildConflict (depth : int, proof : Clause) : void mutable conflict = [] mutable max_depth = 0 mutable something_changed = false def add (l) when (l.atom.MinDepth > max_depth) max_depth = l.atom.MinDepth if (l.IsCaseSplit || l.atom.MinDepth <= depth) conflict ::= ~l false else something_changed = true true def rule = AnalyzeConflict (add, proof) when (something_changed && max_depth >= depth) def clause = MakeHelperClause (conflict, rule) AddConflictClause (clause, $ "at $depth") mutable prev_conflict_count = -1 mutable prev_split_count = 0 mutable top_speed = 0 mutable global_top_speed = 0 AccountConflict () : void when (conflicts_log != null) LogConflictComment ("------------------------------------------------" "----------------------------------") LogConflictComment (ConflictTime ()) driver.num_conflicts++ high_ranking_promotion_countdown = Driver.HighRankingPromotion when (Driver.SpeedBasedRestarts) if (prev_conflict_count < 0) prev_conflict_count = driver.num_conflicts prev_split_count = driver.num_case_splits else def new_cfl = driver.num_conflicts - prev_conflict_count when (new_cfl >= Driver.SBR_Sample) def new_spl = driver.num_case_splits - prev_split_count def new_spl = if (new_spl == 0) 1 else new_spl // avoid division by zero def speed = 10000 * new_cfl / new_spl log (INFO, $"conflicts: $(driver.num_conflicts), $new_cfl / $new_spl = $(speed) (max: $top_speed)") prev_conflict_count = driver.num_conflicts prev_split_count = driver.num_case_splits if (speed > top_speed) top_speed = (Driver.SBR_Flattening * top_speed + speed) / (Driver.SBR_Flattening + 1) else if (Driver.SBR_Threshold * speed < top_speed) log (INFO, "restarting") restarting = true prev_conflict_count = -1 top_speed /= Driver.SBR_Fadeout else {} [Profile] \ MaybeAnalyzeConflict () : void when (core.Refuted && !(core.RefutationProof is [])) AccountConflict () def clause = MakeHelperClause ( $[~l | l in core.RefutationProof.Rev ()], Rule.TheoryConflict ()) BumpScores (clause) AddConflictClause (clause, "theory conflict") BuildConflict (-1, clause) BuildConflict (0, clause) BuildConflict (1, clause) MaybeProofRoot (clause) ClauseIsFalse (c : Clause) : void AccountConflict () AddConflictClause (c, "false clause") BumpScores (c) BuildConflict (-1, c) BuildConflict (0, c) BuildConflict (1, c) MaybeProofRoot (c) core.Refute (Proof.True ()) #endregion #region refinement KeepClause (kind : ClauseKind, c : Clause, no_proxies = false, plunge = false) : bool mutable the_one = null mutable cnt_maybe = 0 when (core.Refuted) return true foreach (l in c.Lits) if (l.IsTrue) if (no_proxies && !l.IsExpanded [kind]) log (VSIMPL, $ "refine $c -> true but cannot expand") return true // the clause is true, but we cannot drop it else when (! l.IsExpanded [kind]) Expand (kind, l) log (VSIMPL, $ "refine $c -> true") return false else if (l.IsFalse) {} else cnt_maybe++ when (cnt_maybe == 1) the_one = l when (cnt_maybe > 1 && plunge) cnt_maybe = 0 foreach (l in c.Lits) if (l.IsTrue) assert (refinement_enabled) log (VSIMPL, $ "rerun refine $c") return KeepClause (kind, c, no_proxies, plunge) else if (l.IsFalse) {} else if (!l.IsExpanded [kind]) cnt_maybe++ the_one = l else core.PushState () Assert (kind, l, c, is_case_split = true) def refuted = core.Refuted def proof = core.RefutationProof core.PopState () if (refuted) //log (TEMP, $ "plunge $l from $c") def neg_proof = $[~l | l in proof] def clause = if (proof.Contains (l)) neg_proof else ~l :: neg_proof def expl = MakeHelperClause (clause, Rule.TheoryConflict ()) Assert (kind, ~l, expl, is_case_split = false, skip_expand = true) when (core.Refuted) return true else cnt_maybe++ the_one = l if (cnt_maybe == 1 && !(no_proxies && the_one.atom is PAtom)) log (VSIMPL, $ "refine $c -> assert $the_one") c.Usefulness++ Assert (kind, the_one, c, is_case_split = false) false else if (cnt_maybe == 0) c.Usefulness += 1000 log (VSIMPL, $ "refine $c -> empty clause") foreach (l in c.Lits) assert (l.IsFalse, l.ToString()) //log (TEMP, $"ref2: $c") ClauseIsFalse (c) true else log (VSIMPL, $ "refine $c -> $cnt_maybe possible splits") true [Copy] mutable refinement_enabled = true [Copy] mutable matching_enabled = true [Copy] mutable full_instantiation_countdown : int [Copy] mutable full_instantiations_since_matching_depth : int [Copy] mutable full_checks_since_matching_depth : int FilterClauses (lst : ref list [Clause], pred : Clause -> bool) : void def tmp = lst lst = [] def res = tmp.Filter (pred) def add = lst lst = add + res [Profile] \ Refine () : void def (prom, non_prom) = pending_clauses.Partition (c => c.Promoted > promoted_threshold) //log (TEMP, $"promote: $prom") current_clauses = prom + current_clauses pending_clauses = non_prom log (VSIMPL, $"enter refine, enbl=$refinement_enabled") while (!core.Refuted && refinement_enabled) log (VSIMPL, "start of refine loop") refinement_enabled = false FilterClauses (ref current_clauses, c => KeepClause (ClauseKind.Current, c)) log (VSIMPL, "refine conflicts") FilterClauses (ref current_conflicts, c => KeepClause (ClauseKind.Conflict, c)) when (Driver.ConflictPromotion) def (prom, non_prom) = current_conflicts.Partition (c => c.Promoted > promoted_threshold) when (!(prom is [])) current_clauses = prom + current_clauses current_conflicts = non_prom refinement_enabled = true when (!core.Refuted && matching_enabled && !refinement_enabled) matching_enabled = false Instantiate () log (VSIMPL, $"end of refine, ref=$(core.Refuted) enbl=$refinement_enabled") #endregion #region main Sat() loop, split literal selection MarkSat (msg : string) : void log (INFO, $"mark sat: $msg") log (SIMPL, $"trail=$trail") sat_context = trail is_sat = true mutable clause_selection_countdown : int = Driver.AlternatingLiteralSelection - 1 [Profile] \ SelectLiteral () : Clause * Literal mutable max = null mutable max_s = 0.0 mutable max_c = null if (clause_selection_countdown == 0) clause_selection_countdown = Driver.AlternatingLiteralSelection foreach (c in current_clauses) when (max_c == null || c.Score > max_c.Score) foreach (l in c.Lits) def s = l.Score - l.atom.MinDepth * Driver.DepthBonus when (l.IsUnset && (max == null || max_s < s)) max = l max_c = c max_s = s else clause_selection_countdown-- foreach (c in current_clauses) foreach (l in c.Lits) def s = l.Score - l.atom.MinDepth * Driver.DepthBonus when (l.IsUnset && (max == null || max_s < s)) max = l max_c = c max_s = s (max_c, max) //mutable split_seq = 1 //mutable parent_split = 0 mutable restarting = false mutable next_restart_in : int = Driver.NextRestartIn mutable restart_horizon : int = Driver.FirstRestart mutable full_check_useful : bool = !Driver.CheapFullCheck mutable full_check_cnt = 0 Sat () : void unless (restarting || is_sat) Refine () unless (restarting || core.Refuted) if (current_clauses is []) def full_check = full_check_useful || (full_check_cnt % 5) == 2 full_check_cnt++ when (full_check) full_checks_since_matching_depth++ if (full_check && !full_check_useful) core.FinalCheck (false) unless (core.Refuted) log (PROG, $"doing full check $full_check") log (TEMP, "doing full check") core.FinalCheck (full_check) when (core.Refuted) log (INFO, "full linear theory checked proven useful") full_check_useful = core.Refuted else log (PROG, $"doing full check $full_check") core.FinalCheck (full_check) unless (core.Refuted) when (pending_clauses is []) Instantiate (last_resort = true) when (pending_clauses is [] && !full_check) core.FinalCheck (full_check = true) when (core.Refuted) log (INFO, "full linear theory checked proven useful (as a last resort)") full_check_useful = core.Refuted unless (core.Refuted) if (pending_clauses is []) MarkSat ("no instances generated") else core.PushState () current_clauses = pending_clauses pending_clauses = [] log (PROG, $"increasing matching depth, $(current_clauses.Length) new clauses") when (full_instantiations_since_matching_depth > 0 && full_checks_since_matching_depth > 0) full_instantiations_since_matching_depth = 0 full_checks_since_matching_depth = 0 checked_matching_depth++ matching_depth++ refinement_enabled = true Sat () MaybeAnalyzeConflict () core.PopState () else driver.ProgressCallback () driver.sizes [0] += trail.Length driver.sizes [1] += lev0_size driver.sizes [2] += matching_depth * 10 driver.sizes [3] += checked_matching_depth * 10 def iters = driver.num_case_splits when (restart_horizon != 0 && iters >= restart_horizon) restart_horizon += next_restart_in next_restart_in = next_restart_in * Driver.RestartHorizonMult / 100 if (num_conflicts_at_last_restart == driver.num_conflicts) // if there were no conflicts, there is no point in restarting log (INFO, $"would restart, but no new conflicts, next restart at $restart_horizon") else num_conflicts_at_last_restart = driver.num_conflicts restarting = true log (INFO, $"restarting the solver at $iters, next restart at $restart_horizon") //repeat (10) IncreaseScores () return core.PushState () def (c, l) = SelectLiteral () //split_seq++ //def backup = parent_split //log (TEMP, $"$backup -> $split_seq;") //parent_split = split_seq log (SIMPL, $ "(split on $l") Assert (ClauseKind.Current, l, c, is_case_split = true) Sat () log (SIMPL, $ "done $l )") MaybeAnalyzeConflict () core.PopState () when (restarting) return // check first few conflicts, to see if we want an early return mutable cnt = 0 foreach (c in conflicts) mutable num_non_false = 0 foreach (l in c.Lits) when (!l.IsFalse) num_non_false++ when (num_non_false == 0) MaybeProofRoot (c) core.Refute (Proof.True ()) return cnt++ when (cnt > 4) break Sat () //parent_split = backup #endregion #region entry point -- Search public Search (f : Term) : bool def (lemmas, f) = if (Driver.ProofLogging && Driver.SkolProofs) def g = ProvingGrinder (core) def f = g.Skolemize (f) (g.Lemmas, f) else ([], Grinder (core).Skolemize (f)) //log (TEMP, $"after skol: $f") def initial = core.MakeClause (array [core.TermToLiteral (0, f)], Rule.InitialFormula ()) current_clauses ::= initial refinement_enabled = true try mutable keep_going = true core.PushState () while (keep_going) Refine () if (core.Refuted) keep_going = false else core.PushState () restarting = false Sat () keep_going = !is_sat && !core.Refuted MaybeAnalyzeConflict () core.PopState () MaybeAnalyzeConflict () core.PopState () assert (is_sat || proof_root != null) log (ANSWER, if (is_sat) "SAT" else "UNSAT") when (is_sat && Driver.Mechanical) // dump error variables def sb = System.Text.StringBuilder ("labels:") foreach (l in sat_context) def name = if (l.atom.term1.Arity == 0 && l.atom.term1 !== pool.True) l.atom.term1.Name else if (l.atom.term2 != null && l.atom.term2.Arity == 0) l.atom.term2.Name else null when (name != null && (((name.StartsWith ("ErrVarPos_") || name.StartsWith ("|EvP@")) && l.IsPos) || ((name.StartsWith ("ErrVarNeg_") || name.StartsWith ("|EvN@")) && l.IsNeg))) _ = sb.Append (" ").Append (name) log (INFO, sb.ToString ()) is_sat finally SaveConflicts () when (proof_root != null && Driver.ProofLogging) def dumper = Trew (lemmas, core) System.IO.File.WriteAllText (Driver.ProofFile, dumper.DumpProof (proof_root, initial)) when (Driver.ProofLogging && Driver.RunChecker) def start = Core.read_tsc () using (proc = System.Diagnostics.Process.Start ("trew/trew", "-t prelude.rw -t " + Driver.ProofFile)) _ = proc.WaitForExit (int.MaxValue) when (proc.ExitCode != 0) throw FatalError ("trew verify failed") log (INFO, $"trew OK, time: $((Core.read_tsc () - start) / 1000000.0)") #endregion