diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-15 11:35:12 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-15 11:35:12 +0200 |
| commit | 4e66de932b91e91e4cadd943ff8859d6f69f57e1 (patch) | |
| tree | ced73719216f2f1fd2eb9057001079a39dbad68e /abstract/nonrelational.ml | |
| parent | 7205927e18ea355a619e95b1036aac9b94a22667 (diff) | |
| download | scade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.tar.gz scade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.zip | |
Clean up & comment a bit.
Diffstat (limited to 'abstract/nonrelational.ml')
| -rw-r--r-- | abstract/nonrelational.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index efa30dd..ed029da 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -5,9 +5,11 @@ open Ast open Value_domain open Num_domain -let debug = false +(* + Implementation of a nonrelationnal domain for numerical values. -(* Restricted domain, only support integers *) + Restricted implementation, only support integers. +*) module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct type env = V.t VarMap.t @@ -160,11 +162,6 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | AST_LT -> let u, _ = V.leq v1 (V.sub v2 (V.const 1)) in u | AST_GT -> let _, v = V.leq (V.add v2 (V.const 1)) v1 in v in - if debug then Format.printf - "restrict %s %s @[<hv>%a@] : %s %s -> %s@." i - (Formula_printer.string_of_binary_rel op) - Formula_printer.print_num_expr expr - (V.to_string v1) (V.to_string v2) (V.to_string v1'); Env (VarMap.add i v1' env)) env in |