Commit c4d685c7 authored by Maxime Folschette's avatar Maxime Folschette
Browse files

remove boundary axioms from phi expressions

parent 1c9b0065
......@@ -776,10 +776,8 @@ struct
| [] -> raise (Invalid_argument "conj_phi_param: Empty powerset (should contain at least [])")
| h :: [] -> PropBin(Impl, phi v h, Rel(comp, ExprParam(v, h), ExprVar v))
| h :: t -> PropBin(And, PropBin(Impl, phi v h, Rel(comp, ExprParam(v, h), ExprVar v)), conj_phi_param v t comp) ;;
let phi_incr v = PropBin(And, PropBin(And, Rel(LE, ExprConst 0, ExprVar v), Rel(LT, ExprVar v, ExprConst (BRNinfo.getbound v))),
conj_phi_param v (powerset (BRNinfo.getpredec v)) GT) ;;
let phi_decr v = PropBin(And, PropBin(And, Rel(LT, ExprConst 0, ExprVar v), Rel(LE, ExprVar v, ExprConst (BRNinfo.getbound v))),
conj_phi_param v (powerset (BRNinfo.getpredec v)) LT) ;;
let phi_incr v = conj_phi_param v (powerset (BRNinfo.getpredec v)) GT ;;
let phi_decr v = conj_phi_param v (powerset (BRNinfo.getpredec v)) LT ;;
(** Plus faible pré-condition *)
let incr_formula v = ExprBin(Plus, ExprVar v, ExprConst 1) ;;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment