simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-05 19:00:33 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

small changes in smt

Browse source
This commit is contained in:
Simon Cruanes 2022-08-07 22:41:13 -04:00
parent 86bc9453d5
commit 4dcc3ea4ad
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/solver.ml
View file

@ -103,8 +103,8 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
last_res = None;
solver = Sat_solver.create ~proof ?size ~stat (SI.to_sat_plugin si);
stat;
count_clause = Stat.mk_int stat "solver.add-clause";
count_solve = Stat.mk_int stat "solver.solve";
count_clause = Stat.mk_int stat "smt.solver.add-clause";
count_solve = Stat.mk_int stat "smt.solver.solve";
}
in
add_theory_l self theories;

8
src/smt/solver_internal.ml
View file

@ -607,10 +607,10 @@ let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t =
registry = Registry.create ();
preprocessed = Term.Tbl.create 32;
delayed_actions = Queue.create ();
count_axiom = Stat.mk_int stat "solver.th-axioms";
count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause";
count_propagate = Stat.mk_int stat "solver.th-propagations";
count_conflict = Stat.mk_int stat "solver.th-conflicts";
count_axiom = Stat.mk_int stat "smt.solver.th-axioms";
count_preprocess_clause = Stat.mk_int stat "smt.solver.preprocess-clause";
count_propagate = Stat.mk_int stat "smt.solver.th-propagations";
count_conflict = Stat.mk_int stat "smt.solver.th-conflicts";
on_partial_check = [];
on_final_check = [];
on_th_combination = [];