Skip to content

Commit

Permalink
Builtin steps know counted for all formulas assumed in Interval_calculus
Browse files Browse the repository at this point in the history
  • Loading branch information
@ACoquereau
ACoquereau committed Feb 26, 2020
1 parent 562c7af commit 2dab74e
Show file tree
Hide file tree
Showing 5 changed files with 92 additions and 28 deletions.
2 changes: 1 addition & 1 deletion sources/lib/reasoners/fun_sat.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) =
Expand Down
2 changes: 1 addition & 1 deletion sources/lib/reasoners/intervalCalculus.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions sources/lib/reasoners/satml.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand Down Expand Up @@ -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 ()
Expand Down
60 changes: 44 additions & 16 deletions sources/lib/util/steps.ml
View file
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
Expand All @@ -41,15 +69,15 @@ 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)
| Fourier -> mult_f := !mult_f + 1;
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
Expand Down Expand Up @@ -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
52 changes: 44 additions & 8 deletions sources/lib/util/steps.mli
View file
Original file line number Diff line number Diff line change
@@ -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
Expand Down

0 comments on commit 2dab74e

Please sign in to comment.