mcBV/BoundInference.fs at master · microsoft/mcBV · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
module BoundInference
open System.Collections.Generic
open Microsoft.Z3
open GlobalOptions
open Util
open Numeral
open Literal
open BooleanValuation
open Clause
open Trail
open State
open WatchManager
open VariableDB
open ClauseDB
open TheoryDB
open ThRel
open BitVector
open BitVectorValuation
open Explain
open Learning

// 1 Determine the relation
// 2 Determine reverse operation
// 3 Evaluate

//
//let inferByRelations (s:State) (v:int) (tRel:internalThRel) =
//    assert (List.exists (fun x -> x = v) tRel.distinctArgs)
//
//    if tRel.getRhs

// Assume" x_l,x_u <= op args_l args_u (rhs)
// We will evaluate the op args_l args_u
// And based on that update the x_l, x_u
// rhs_l <= x_l <= x_u <= rhs_u
//
//let inferBounds (s:State) (v:int) (tRel:internalThRel) =
//    let (currentL, currentU) = (!s.partAssignment).getBounds v
//    if BitVector.bvEQ currentL currentU then
//        None
//    else
//        let (inferredL,inferredU) = inferByRelations s v tRel
//
//        let resL = if not (BitVector.bvULEQ inferredL currentL) then
//                        inferredL
//                   else
//                        currentL
//
//        let resU = if not (BitVector.bvULEQ currentU inferredU) then
//                        inferredU
//                   else
//                        currentU
//        Some (relL,resU)
//
//