diff --git a/sources/lib/reasoners/fun_sat.ml b/sources/lib/reasoners/fun_sat.ml index a254ea3a3..a835d6b2b 100644 --- a/sources/lib/reasoners/fun_sat.ml +++ b/sources/lib/reasoners/fun_sat.ml @@ -845,7 +845,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct in let utbox = if env.dlevel = 0 then tbox else utbox in let inst = Inst.add_terms inst new_terms (mk_gf E.vrai "" mf gf) in - Steps.incr (Naive cpt); + Steps.incr (Th_assumed cpt); { env with tbox = tbox; unit_tbox = utbox; inst = inst } let propagations ((env, bcp, tcp, ap_delta, lits) as result) = diff --git a/sources/lib/reasoners/intervalCalculus.ml b/sources/lib/reasoners/intervalCalculus.ml index 4c4400321..4a581f9ec 100644 --- a/sources/lib/reasoners/intervalCalculus.ml +++ b/sources/lib/reasoners/intervalCalculus.ml @@ -1494,10 +1494,10 @@ let assume ~query env uf la = (fun ((env, eqs, new_ineqs, rm) as acc) (a, root, expl, orig) -> let a = normal_form a in Debug.assume a expl; + Steps.incr (Interval_Calculus); try match a with | L.Builtin(_, ((L.LE | L.LT) as n), [r1;r2]) -> - Steps.incr (Builtin); incr nb_num; let p1 = poly_of r1 in let p2 = poly_of r2 in diff --git a/sources/lib/reasoners/satml.ml b/sources/lib/reasoners/satml.ml index 9fca69561..71b9de62c 100644 --- a/sources/lib/reasoners/satml.ml +++ b/sources/lib/reasoners/satml.ml @@ -768,7 +768,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct Th.assume ~ordered:false (List.rev facts) env.unit_tenv in - Steps.incr (Steps.Naive cpt); + Steps.incr (Steps.Th_assumed cpt); env.unit_tenv <- t; C_none with Ex.Inconsistent (dep, _terms) -> @@ -832,7 +832,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct Th.assume ~ordered:(not (Options.cdcl_tableaux_th ())) (List.rev !facts) env.tenv in - Steps.incr (Naive cpt); + Steps.incr (Steps.Th_assumed cpt); env.tenv <- t; do_case_split env Util.AfterTheoryAssume (*if full_model then expensive_theory_propagate () diff --git a/sources/lib/util/steps.ml b/sources/lib/util/steps.ml index ed8d313d9..c01b88820 100644 --- a/sources/lib/util/steps.ml +++ b/sources/lib/util/steps.ml @@ -1,16 +1,44 @@ +(******************************************************************************) +(* *) +(* The Alt-Ergo theorem prover *) +(* Copyright (C) 2006-2013 *) +(* *) +(* Sylvain Conchon *) +(* Evelyne Contejean *) +(* *) +(* Francois Bobot *) +(* Mohamed Iguernelala *) +(* Stephane Lescuyer *) +(* Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* This file is distributed under the terms of the Apache Software *) +(* License version 2.0 *) +(* *) +(* ------------------------------------------------------------------------ *) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2018 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the Apache Software *) +(* License version 2.0 *) +(* *) +(******************************************************************************) + open Options open Format -(** Define the type of increment *) +(* Define the type of increment *) type incr_kind = - Matching (* Matching step increment *) - | Omega (* Step of Arith on Real and Int *) - | Fourier (* FourierMotzkin step increment *) - | Uf (* UF step increment *) - | Builtin (* Inequalities increment *) - | Ac (* AC step reasoning *) - | Naive of int (* Naive cpt increment the counter for cpt term assumed in the - * theories environment *) + Matching (* Matching step increment *) + | Interval_Calculus (* Arith : Interval Calculus increment *) + | Fourier (* Arith : FourierMotzkin step increment *) + | Omega (* Arith : number of omega procedure on Real and Int *) + | Uf (* UF step increment *) + | Ac (* AC step reasoning *) + | Th_assumed of int (* Increment the counter for each term assumed in the + theories environment *) let naive_steps = ref 0 let steps = ref 0 @@ -21,7 +49,7 @@ let mult_uf = ref 0 let mult_b = ref 0 let mult_a = ref 0 -(** Multipliers are here to homogeneize the global step counter *) +(* Multipliers are here to homogeneize the global step counter *) let incr k = begin match k with @@ -41,7 +69,7 @@ let incr k = if !mult_a = 1 then (steps := !steps + 1; mult_a := 0) - | Builtin -> mult_b := !mult_b + 1; + | Interval_Calculus -> mult_b := !mult_b + 1; if !mult_b = 5 then (steps := !steps + 1; mult_b := 0) @@ -49,7 +77,7 @@ let incr k = if !mult_f = 40 then (steps := !steps + 1; mult_f := 0); - | Naive n -> + | Th_assumed n -> (* Since n refers to the number of terms sent to the theories no * multiplier is needed here *) if n < 0 then @@ -81,9 +109,9 @@ let reset_steps () = mult_b := 0; mult_a := 0 -(** Return the max steps between naive and refine steps counting. Both counter - ** are compute at execution. The first one count the number of terms sent to - ** the thories environment, the second one count steps depending of the - ** theories used *) +(* Return the max steps between naive and refine steps counting. Both counter + * are compute at execution. The first one count the number of terms sent to the + * theories environment, the second one count steps depending of the theories + * used *) let get_steps () = max !naive_steps !steps diff --git a/sources/lib/util/steps.mli b/sources/lib/util/steps.mli index 600f30a41..89dc072e0 100644 --- a/sources/lib/util/steps.mli +++ b/sources/lib/util/steps.mli @@ -1,12 +1,48 @@ +(******************************************************************************) +(* *) +(* The Alt-Ergo theorem prover *) +(* Copyright (C) 2006-2013 *) +(* *) +(* Sylvain Conchon *) +(* Evelyne Contejean *) +(* *) +(* Francois Bobot *) +(* Mohamed Iguernelala *) +(* Stephane Lescuyer *) +(* Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* This file is distributed under the terms of the Apache Software *) +(* License version 2.0 *) +(* *) +(* ------------------------------------------------------------------------ *) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2018 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the Apache Software *) +(* License version 2.0 *) +(* *) +(******************************************************************************) + +(** Module_Name + + This module aims to count the number of steps in the theories used to solve + the problem. +*) + +(** {1 Steps counters} *) + type incr_kind = - Matching (* Matching step increment *) - | Omega (* Step of Arith on Real and Int *) - | Fourier (* FourierMotzkin step increment *) - | Uf (* UF step increment *) - | Builtin (* Inequalities increment *) - | Ac (* AC step reasoning *) - | Naive of int (* Naive way of counting steps is to increment the counter for - * each term assumed in the theories environment *) + Matching (** Matching step increment *) + | Interval_Calculus (** Arith : Interval Calculus increment *) + | Fourier (** Arith : FourierMotzkin step increment *) + | Omega (** Arith : number of omega procedure on Real and Int *) + | Uf (** UF step increment *) + | Ac (** AC step reasoning *) + | Th_assumed of int (** Increment the counter for each term assumed in the + theories environment *) (** Define the type of increment *) val incr : incr_kind -> unit