1 files changed, 101 insertions, 0 deletions
diff --git a/vendor/varisat/src/schedule.rs b/vendor/varisat/src/schedule.rs
new file mode 100644
index 000000000..1e1b04e57
--- /dev/null
+++ b/vendor/varisat/src/schedule.rs
@@ -0,0 +1,101 @@
+//! Scheduling of processing and solving steps.
+//!
+//! The current implementation is temporary and will be replaced with something more flexible.
+use log::info;
+
+use partial_ref::{partial, PartialRef};
+
+use crate::{
+    cdcl::conflict_step,
+    clause::{
+        collect_garbage,
+        reduce::{reduce_locals, reduce_mids},
+        Tier,
+    },
+    context::{parts::*, Context},
+    prop::restart,
+    state::SatState,
+};
+
+mod luby;
+
+use luby::LubySequence;
+
+/// Scheduling of processing and solving steps.
+#[derive(Default)]
+pub struct Schedule {
+    conflicts: u64,
+    next_restart: u64,
+    restarts: u64,
+    luby: LubySequence,
+}
+
+/// Perform one step of the schedule.
+pub fn schedule_step<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut AnalyzeConflictP,
+        mut AssignmentP,
+        mut AssumptionsP,
+        mut BinaryClausesP,
+        mut ClauseActivityP,
+        mut ClauseAllocP,
+        mut ClauseDbP,
+        mut ImplGraphP,
+        mut ModelP,
+        mut ProofP<'a>,
+        mut ScheduleP,
+        mut SolverStateP,
+        mut TmpDataP,
+        mut TmpFlagsP,
+        mut TrailP,
+        mut VariablesP,
+        mut VsidsP,
+        mut WatchlistsP,
+        SolverConfigP,
+    ),
+) -> bool {
+    let (schedule, mut ctx) = ctx.split_part_mut(ScheduleP);
+    let (config, mut ctx) = ctx.split_part(SolverConfigP);
+
+    if ctx.part(SolverStateP).sat_state != SatState::Unknown
+        || ctx.part(SolverStateP).solver_error.is_some()
+    {
+        false
+    } else {
+        if schedule.conflicts > 0 && schedule.conflicts % 5000 == 0 {
+            let db = ctx.part(ClauseDbP);
+            let units = ctx.part(TrailP).top_level_assignment_count();
+            info!(
+                "confl: {}k rest: {} vars: {} bin: {} irred: {} core: {} mid: {} local: {}",
+                schedule.conflicts / 1000,
+                schedule.restarts,
+                ctx.part(AssignmentP).assignment().len() - units,
+                ctx.part(BinaryClausesP).count(),
+                db.count_by_tier(Tier::Irred),
+                db.count_by_tier(Tier::Core),
+                db.count_by_tier(Tier::Mid),
+                db.count_by_tier(Tier::Local)
+            );
+        }
+
+        if schedule.next_restart == schedule.conflicts {
+            restart(ctx.borrow());
+            schedule.restarts += 1;
+            schedule.next_restart += config.luby_restart_interval_scale * schedule.luby.advance();
+        }
+
+        if schedule.conflicts % config.reduce_locals_interval == 0 {
+            reduce_locals(ctx.borrow());
+        }
+        if schedule.conflicts % config.reduce_mids_interval == 0 {
+            reduce_mids(ctx.borrow());
+        }
+
+        collect_garbage(ctx.borrow());
+
+        conflict_step(ctx.borrow());
+        schedule.conflicts += 1;
+        true
+    }
+}